Characteristic functions and generating functions

Characteristic functions, probability generating functions and positive-definite functions (Bochner), Taylor bounds for characteristic functions, lattice support, Lévy's continuity theorem and Cramér's decomposition theorem for the normal law.

TheoremCramér's decomposition theorem#✓fully proved

Let \(X\) and \(Y\) be measurable real random variables on a probability space. If \(X\) and \(Y\) are independent and \(X + Y\) has a Gaussian law, then \(X\) and \(Y\) each have a Gaussian law. Here a Gaussian law may be degenerate, that is, a point mass.

theorem cramer_decomposition
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X Y : Ω → ℝ} (hX : Measurable X) (hY : Measurable Y)
    (hXY : IndepFun X Y μ)
    (hAdd : HasGaussianLaw (fun ω => X ω + Y ω) μ) :
    HasGaussianLaw X μ ∧ HasGaussianLaw Y μ
Sources
  • H. Cramér, "Über eine Eigenschaft der normalen Verteilungsfunktion", Mathematische Zeitschrift 41 (1936), 405–414, DOI 10.1007/BF01180430.

TheoremLévy's continuity theorem#✓fully proved

Let \(d \in \mathbb{N}\), let \((\mu_n)_{n \in \mathbb{N}}\) be a sequence of probability measures on the Euclidean space \(\mathbb{R}^d\), and let \(\varphi : \mathbb{R}^d \to \mathbb{C}\). Suppose that for every \(t \in \mathbb{R}^d\) the characteristic functions \(\hat\mu_n\) of the \(\mu_n\) satisfy \(\hat\mu_n(t) \to \varphi(t)\) as \(n \to \infty\), and that \(\varphi\) is continuous at \(0\). Then there is a probability measure \(\mu\) on \(\mathbb{R}^d\) whose characteristic function is \(\varphi\), that is, \(\varphi(t) = \hat\mu(t)\) for every \(t \in \mathbb{R}^d\), and \(\mu_n\) converges weakly to \(\mu\).

theorem levy_continuity_of_charFun
    {d : ℕ} {μn : ℕ → ProbabilityMeasure (EuclideanSpace ℝ (Fin d))}
    {φ : EuclideanSpace ℝ (Fin d) → ℂ}
    (hφ : ∀ t, Tendsto (fun n => charFun (μn n : Measure _) t) atTop
      (nhds (φ t)))
    (hcont : ContinuousAt φ (0 : EuclideanSpace ℝ (Fin d))) :
    ∃ μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin d)),
      (∀ t, φ t = charFun (μ : Measure _) t) ∧
      Tendsto (fun n => μn n) atTop (nhds μ)
Sources
  • P. Billingsley, Probability and Measure, 3rd ed., Section 26.
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.