The limit law Y_α: characteristic function and uniqueness (Stage 1)

Source lines 174–178 and 846: Y_α has Laplace transform E exp(-λ Y_α) = exp(λ^α) for λ > 0, with α ∈ (1,2]. We prove:

• BGW.StableTrees.Scalar.charFun_eq_stableCF: E exp(iθY_α) = exp((-iθ)^α) (principal complex power), by analytic continuation of the Laplace transform to {Re z < 0} (identity theorem for the complex moment generating function) and dominated convergence to the boundary Re z = 0;
• BGW.StableTrees.Scalar.norm_stableCF: |E exp(iθY_α)| = exp(cos(πα/2) |θ|^α), where cos(πα/2) < 0 for α ∈ (1,2] (cos(πα/2) = -1 for α = 2);
• BGW.StableTrees.Scalar.integrable_stableCF: the characteristic function is integrable;
• BGW.StableTrees.Scalar.limitLaw_unique: the law with this Laplace transform is unique.

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

noncomputable def BGW.StableTrees.Scalar.stableCF (α θ : ℝ) : ℂ

The characteristic function θ ↦ exp((-iθ)^α) of the limit law (principal power).

Equations

• BGW.StableTrees.Scalar.stableCF α θ = Complex.exp ((-(↑θ * Complex.I)) ^ ↑α)

theorem BGW.StableTrees.Scalar.stableCF_zero {α : ℝ} (hα : α ≠ 0) : stableCF α 0 = 1

theorem BGW.StableTrees.Scalar.neg_mul_I_cpow_of_pos {θ : ℝ} (hθ : 0 < θ) (α : ℝ) : (-(↑θ * Complex.I)) ^ ↑α = ↑(θ ^ α) * Complex.exp (↑(-(Real.pi * α / 2)) * Complex.I)

theorem BGW.StableTrees.Scalar.neg_mul_I_cpow_of_neg {θ : ℝ} (hθ : θ < 0) (α : ℝ) : (-(↑θ * Complex.I)) ^ ↑α = ↑((-θ) ^ α) * Complex.exp (↑(Real.pi * α / 2) * Complex.I)

theorem BGW.StableTrees.Scalar.re_neg_mul_I_cpow {α : ℝ} (hα : α ≠ 0) (θ : ℝ) : ((-(↑θ * Complex.I)) ^ ↑α).re = |θ| ^ α * Real.cos (Real.pi * α / 2)

theorem BGW.StableTrees.Scalar.norm_stableCF {α : ℝ} (hα : α ≠ 0) (θ : ℝ) : ‖stableCF α θ‖ = Real.exp (Real.cos (Real.pi * α / 2) * |θ| ^ α)

theorem BGW.StableTrees.Scalar.stableCF_neg {α : ℝ} (hα : α ≠ 0) (θ : ℝ) : stableCF α (-θ) = (starRingEnd ℂ) (stableCF α θ)

theorem BGW.StableTrees.Scalar.cos_pi_mul_div_two_neg {α : ℝ} (hα : 1 < α ∧ α ≤ 2) : Real.cos (Real.pi * α / 2) < 0

theorem BGW.StableTrees.Scalar.continuous_stableCF {α : ℝ} (hα : 0 < α) : Continuous (stableCF α)

theorem BGW.StableTrees.Scalar.integrable_exp_neg_mul_of_laplace {ν : MeasureTheory.Measure ℝ} {α : ℝ} (hL : ∀ (lam : ℝ), 0 < lam → ∫ (y : ℝ), Real.exp (-lam * y) ∂ν = Real.exp (lam ^ α)) {lam : ℝ} (hlam : 0 < lam) : MeasureTheory.Integrable (fun (y : ℝ) => Real.exp (-lam * y)) ν

theorem BGW.StableTrees.Scalar.Iio_subset_interior_integrableExpSet {ν : MeasureTheory.Measure ℝ} {α : ℝ} (hL : ∀ (lam : ℝ), 0 < lam → ∫ (y : ℝ), Real.exp (-lam * y) ∂ν = Real.exp (lam ^ α)) : Set.Iio 0 ⊆ interior (ProbabilityTheory.integrableExpSet id ν)

theorem BGW.StableTrees.Scalar.complexMGF_eq_of_re_neg {ν : MeasureTheory.Measure ℝ} {α : ℝ} (hL : ∀ (lam : ℝ), 0 < lam → ∫ (y : ℝ), Real.exp (-lam * y) ∂ν = Real.exp (lam ^ α)) {z : ℂ} (hz : z.re < 0) : ProbabilityTheory.complexMGF id ν z = Complex.exp ((-z) ^ ↑α)

theorem BGW.StableTrees.Scalar.tendsto_complexMGF_boundary {ν : MeasureTheory.Measure ℝ} {α : ℝ} [MeasureTheory.IsProbabilityMeasure ν] (hL : ∀ (lam : ℝ), 0 < lam → ∫ (y : ℝ), Real.exp (-lam * y) ∂ν = Real.exp (lam ^ α)) (θ : ℝ) : Filter.Tendsto (fun (ε : ℝ) => ProbabilityTheory.complexMGF id ν (-↑ε + ↑θ * Complex.I)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (ProbabilityTheory.complexMGF id ν (↑θ * Complex.I)))

theorem BGW.StableTrees.Scalar.charFun_eq_stableCF {ν : MeasureTheory.Measure ℝ} {α : ℝ} [MeasureTheory.IsProbabilityMeasure ν] (hα : 0 < α) (hL : ∀ (lam : ℝ), 0 < lam → ∫ (y : ℝ), Real.exp (-lam * y) ∂ν = Real.exp (lam ^ α)) (θ : ℝ) : MeasureTheory.charFun ν θ = stableCF α θ

Characteristic function of the limit law. If ν is a probability measure with ∫ e^{-λ y} dν = e^{λ^α} for all λ > 0, then E e^{iθY} = exp((-iθ)^α).

theorem BGW.StableTrees.Scalar.integrable_stableCF {α : ℝ} (hα : 1 < α ∧ α ≤ 2) : MeasureTheory.Integrable (stableCF α) MeasureTheory.volume

theorem BGW.StableTrees.Scalar.integrable_abs_mul_norm_stableCF {α : ℝ} (hα : 1 < α ∧ α ≤ 2) : MeasureTheory.Integrable (fun (θ : ℝ) => |θ| * ‖stableCF α θ‖) MeasureTheory.volume

theorem BGW.StableTrees.Scalar.limitLaw_unique {α : ℝ} (hα : 0 < α) {ν₁ ν₂ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν₁] [MeasureTheory.IsProbabilityMeasure ν₂] (h₁ : ∀ (lam : ℝ), 0 < lam → ∫ (y : ℝ), Real.exp (-lam * y) ∂ν₁ = Real.exp (lam ^ α)) (h₂ : ∀ (lam : ℝ), 0 < lam → ∫ (y : ℝ), Real.exp (-lam * y) ∂ν₂ = Real.exp (lam ^ α)) : ν₁ = ν₂

Uniqueness of the limit law: a probability measure on ℝ is determined by the Laplace identity ∫ e^{-λy} dν = e^{λ^α} (λ > 0).