Characteristic function of the walk and Fourier inversion on ℤ

For the step law X = K - 1 (BGW.StableTrees.stepLaw) and the walk law BGW.StableTrees.walkLaw μ n (an n-fold convolution, source lines 174–181, 842–845):

• BGW.StableTrees.Scalar.walkCF_eq_pow: E e^{iθ S_n} = φ(θ)^n with φ = stepCF μ;
• BGW.StableTrees.Scalar.charFun_walkLaw_map_div: the characteristic function of S_n / c is φ(t/c)^n;
• BGW.StableTrees.Scalar.walkLaw_real_singleton: Fourier inversion on ℤ, P(S_n = k) = (1/2π) ∫_{-π}^{π} φ(θ)^n e^{-ikθ} dθ.

Adapted from PoissonDeclumping/Stable/WalkCF.lean in igor-kortchemski/rare-subtree-patterns, commit fc5ef722392b1af41e8b9d5fc45d5a521b7823dd (Apache-2.0).

instance BGW.StableTrees.Scalar.isProbabilityMeasure_stepLaw (μ : PMF ℕ) : MeasureTheory.IsProbabilityMeasure (stepLaw μ)

instance BGW.StableTrees.Scalar.isProbabilityMeasure_walkLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (walkLaw μ n)

noncomputable def BGW.StableTrees.Scalar.stepCF (μ : PMF ℕ) (θ : ℝ) : ℂ

The characteristic function φ(θ) = E e^{iθX} of one step.

Equations

• BGW.StableTrees.Scalar.stepCF μ θ = ∫ (z : ℤ), Complex.exp (↑θ * ↑z * Complex.I) ∂BGW.StableTrees.stepLaw μ

noncomputable def BGW.StableTrees.Scalar.walkCF (μ : PMF ℕ) (n : ℕ) (θ : ℝ) : ℂ

The characteristic function E e^{iθ S_n} of the walk at time n.

Equations

• BGW.StableTrees.Scalar.walkCF μ n θ = ∫ (z : ℤ), Complex.exp (↑θ * ↑z * Complex.I) ∂BGW.StableTrees.walkLaw μ n

theorem BGW.StableTrees.Scalar.integral_conv_int {W P : MeasureTheory.Measure ℤ} (F : ℤ → ℂ) : ∫ (z : ℤ), F z ∂W.conv P = ∫ (p : ℤ × ℤ), F (p.1 + p.2) ∂W.prod P

theorem BGW.StableTrees.Scalar.walkCF_eq_pow (μ : PMF ℕ) (n : ℕ) (θ : ℝ) : walkCF μ n θ = stepCF μ θ ^ n

theorem BGW.StableTrees.Scalar.norm_walkCF_le (μ : PMF ℕ) (n : ℕ) (θ : ℝ) : ‖walkCF μ n θ‖ ≤ 1

theorem BGW.StableTrees.Scalar.norm_stepCF_le (μ : PMF ℕ) (θ : ℝ) : ‖stepCF μ θ‖ ≤ 1

theorem BGW.StableTrees.Scalar.continuous_stepCF (μ : PMF ℕ) : Continuous (stepCF μ)

theorem BGW.StableTrees.Scalar.charFun_walkLaw_map_div (μ : PMF ℕ) (n : ℕ) (c t : ℝ) : MeasureTheory.charFun (MeasureTheory.Measure.map (fun (z : ℤ) => ↑z / c) (walkLaw μ n)) t = stepCF μ (t / c) ^ n

The characteristic function of S_n / c is φ(θ/c)^n.

theorem BGW.StableTrees.Scalar.intervalIntegral_cexp_int_mul_I (m : ℤ) : ∫ (θ : ℝ) in -Real.pi..Real.pi, Complex.exp (↑θ * ↑m * Complex.I) = if m = 0 then ↑(2 * Real.pi) else 0

theorem BGW.StableTrees.Scalar.walkLaw_real_singleton (μ : PMF ℕ) (n : ℕ) (k : ℤ) : ↑((walkLaw μ n).real {k}) = 1 / (2 * ↑Real.pi) * ∫ (θ : ℝ) in -Real.pi..Real.pi, stepCF μ θ ^ n * Complex.exp (-(↑θ * ↑k * Complex.I))

Fourier inversion on ℤ: P(S_n = k) = (1/2π) ∫_{-π}^{π} φ(θ)^n e^{-ikθ} dθ.