d_α is the density of Y_α (Stage 1, completed)

Source line 864 ("d_α is the density of Y_α"). The function BGW.StableTrees.Scalar.stableDensity α is defined by Fourier inversion of exp((-iθ)^α); here we prove that it is indeed the density of the limit law:

• BGW.StableTrees.Scalar.stableDensity_nonneg: d_α ≥ 0 (from the local limit theorem);
• BGW.StableTrees.Scalar.integral_stableDensity_mul_gaussian_le: ∫ d_α(x) e^{-bx²} dx ≤ 1 (Fubini and the Gaussian Fourier transform);
• BGW.StableTrees.Scalar.integrable_stableDensity: d_α ∈ L¹ (monotone convergence);
• BGW.StableTrees.Scalar.charFun_withDensity_stableDensity: the characteristic function of d_α(x) dx is exp((-iθ)^α) (mathlib's Fourier inversion theorem);
• BGW.StableTrees.Scalar.limitLaw_eq_withDensity: ν = d_α(x) dx;
• BGW.StableTrees.Scalar.integral_stableDensity: ∫ d_α = 1.

The hypothesis StableDomain μ α a is used only through d_α ≥ 0 (a property of α alone, obtained here from the local limit theorem of any walk in the domain).

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

theorem BGW.StableTrees.Scalar.norm_stableCF_le_one {α : ℝ} (hα : 1 < α ∧ α ≤ 2) (θ : ℝ) : ‖stableCF α θ‖ ≤ 1

theorem BGW.StableTrees.Scalar.stableDensity_nonneg {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) (x : ℝ) : 0 ≤ stableDensity α x

d_α ≥ 0 (a consequence of the local limit theorem: d · d_α is a limit of a_n P(S_n=k_n)).

theorem BGW.StableTrees.Scalar.integral_cexp_mul_gaussian {b : ℝ} (hb : 0 < b) (θ : ℝ) : ∫ (x : ℝ), Complex.exp (-(↑θ * ↑x * Complex.I)) * ↑(Real.exp (-b * x ^ 2)) = ↑√(Real.pi / b) * ↑(Real.exp (-θ ^ 2 / (4 * b)))

theorem BGW.StableTrees.Scalar.integral_stableDensity_mul_gaussian_le {α : ℝ} (hα : 1 < α ∧ α ≤ 2) {b : ℝ} (hb : 0 < b) : ∫ (x : ℝ), stableDensity α x * Real.exp (-b * x ^ 2) ≤ 1

∫ d_α(x) e^{-b x²} dx ≤ 1 for every b > 0 (Fubini and the Gaussian Fourier transform: the left side is (1/2π) ∫ exp((-iθ)^α) √(π/b) e^{-θ²/4b} dθ).

theorem BGW.StableTrees.Scalar.integrable_stableDensity {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : MeasureTheory.Integrable (stableDensity α) MeasureTheory.volume

d_α is integrable (with ∫ d_α ≤ 1 from the Gaussian bound and monotone convergence).

theorem BGW.StableTrees.Scalar.integral_stableCF_mul_cexp_real {α : ℝ} (hα : 1 < α ∧ α ≤ 2) (x : ℝ) : ↑(∫ (θ : ℝ), stableCF α θ * Complex.exp (-(↑θ * ↑x * Complex.I))).re = ∫ (θ : ℝ), stableCF α θ * Complex.exp (-(↑θ * ↑x * Complex.I))

theorem BGW.StableTrees.Scalar.fourier_stableCF_scaled {α : ℝ} (hα : 1 < α ∧ α ≤ 2) : (FourierTransform.fourier fun (ξ : ℝ) => stableCF α (2 * Real.pi * ξ)) = fun (x : ℝ) => ↑(stableDensity α x)

The Fourier transform (mathlib normalization 𝓕 g(x) = ∫ e^{-2πiξx} g(ξ) dξ) of the rescaled characteristic function ξ ↦ exp((-2πiξ)^α) is d_α.

theorem BGW.StableTrees.Scalar.charFun_withDensity_stableDensity {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) (t : ℝ) : MeasureTheory.charFun (MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (stableDensity α x)) t = stableCF α t

charFun of the measure d_α(x) dx is exp((-iθ)^α).

theorem BGW.StableTrees.Scalar.limitLaw_eq_withDensity {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] (hL : ∀ (lam : ℝ), 0 < lam → ∫ (y : ℝ), Real.exp (-lam * y) ∂ν = Real.exp (lam ^ α)) : ν = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (stableDensity α x)

d_α is the density of Y_α (source line 864): under (H_α), the limit law ν (any probability measure with ∫ e^{-λy} dν = e^{λ^α}) is d_α(x) dx.

theorem BGW.StableTrees.Scalar.integral_stableDensity {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : ∫ (x : ℝ), stableDensity α x = 1

∫ d_α = 1.