Analytic helpers for the stable toolbox

• BGW.StableTrees.Scalar.eqOn_halfPlane_of_eq_real: identity theorem on a left half-plane {Re z < c} from agreement at real points.
• BGW.StableTrees.Scalar.integral_cexp_neg_mul_rpow: the complex Gamma integral ∫_0^∞ exp(-r θ^p) dθ = Γ(1/p + 1) r^{-1/p} for Re r > 0 (mathlib only has real r); proved by analytic continuation in r, through the complex moment generating function of θ ↦ θ^p under the finite measure e^{-θ^p} dθ on (0,∞).
• integrability on ℝ of |θ|^s exp(-c|θ|^p).

These are used to identify the characteristic function and the density of the limit law (source lines 846–864).

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

theorem BGW.StableTrees.Scalar.eqOn_halfPlane_of_eq_real {f g : ℂ → ℂ} {c : ℝ} (hf : AnalyticOnNhd ℂ f {z : ℂ | z.re < c}) (hg : AnalyticOnNhd ℂ g {z : ℂ | z.re < c}) (h : ∀ t < c, f ↑t = g ↑t) : Set.EqOn f g {z : ℂ | z.re < c}

Identity theorem on a left half-plane: analytic functions agreeing on the real points of {Re z < c} agree on the half-plane.

noncomputable def BGW.StableTrees.Scalar.gammaMeasure (p : ℝ) : MeasureTheory.Measure ℝ

The finite measure e^{-θ^p} dθ on (0,∞).

Equations

• BGW.StableTrees.Scalar.gammaMeasure p = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (θ : ℝ) => ↑(Real.exp (-θ ^ p)).toNNReal

theorem BGW.StableTrees.Scalar.measurable_gammaDensity (p : ℝ) : Measurable fun (θ : ℝ) => (Real.exp (-θ ^ p)).toNNReal

theorem BGW.StableTrees.Scalar.complexMGF_gammaMeasure {p : ℝ} (z : ℂ) : ProbabilityTheory.complexMGF (fun (θ : ℝ) => θ ^ p) (gammaMeasure p) z = ∫ (θ : ℝ) in Set.Ioi 0, Complex.exp ((z - 1) * ↑(θ ^ p))

theorem BGW.StableTrees.Scalar.Iio_one_subset_integrableExpSet_gamma {p : ℝ} (hp : 0 < p) : Set.Iio 1 ⊆ ProbabilityTheory.integrableExpSet (fun (θ : ℝ) => θ ^ p) (gammaMeasure p)

theorem BGW.StableTrees.Scalar.integral_cexp_neg_mul_rpow {p : ℝ} (hp : 0 < p) {r : ℂ} (hr : 0 < r.re) : ∫ (θ : ℝ) in Set.Ioi 0, Complex.exp (-r * ↑(θ ^ p)) = ↑(Real.Gamma (1 / p + 1)) * r ^ (-↑(1 / p))

∫_0^∞ exp(-r θ^p) dθ = Γ(1/p + 1) r^{-1/p} for complex r with Re r > 0.

theorem BGW.StableTrees.Scalar.integrable_comp_abs_of_integrableOn_Ioi {g : ℝ → ℝ} (hg : MeasureTheory.IntegrableOn g (Set.Ioi 0) MeasureTheory.volume) : MeasureTheory.Integrable (fun (θ : ℝ) => g |θ|) MeasureTheory.volume

An even function built from a function integrable on (0,∞) is integrable.

theorem BGW.StableTrees.Scalar.integrable_rpow_abs_mul_exp_neg {s p c : ℝ} (hs : -1 < s) (hp : 0 < p) (hc : 0 < c) : MeasureTheory.Integrable (fun (θ : ℝ) => |θ| ^ s * Real.exp (-c * |θ| ^ p)) MeasureTheory.volume