Documentation

BGW.StableTrees.Scalar.Density

The stable density d_α (Stage 1, continued) #

Source lines 862–864 and the uses of d_α at lines 1029–1041, 1640–1647, 1987–1994. The density of Y_α is defined by Fourier inversion of the (integrable) characteristic function exp((-iθ)^α) from BGW.StableTrees.Scalar.LimitLaw:

d_α(x) = (1/2π) Re ∫ exp((-iθ)^α) e^{-iθx} dθ.

We prove that d_α is bounded and Lipschitz (hence continuous and uniformly continuous), and compute its value at zero, d_α(0) = Γ(1 + 1/α) sin(π/α) / π > 0, using the complex Gamma integral of BGW.StableTrees.Scalar.Analytic (this replaces the contour rotation).

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

source
noncomputable def BGW.StableTrees.Scalar.stableDensity (α x : ℝ) :
ℝ

The density d_α of the limit law Y_α, defined by Fourier inversion of its characteristic function exp((-iθ)^α).

Equations
Instances For
    source
    theorem BGW.StableTrees.Scalar.norm_cexp_neg_mul_I (θ x : ℝ) :
    ‖Complex.exp (-(↑θ * ↑x * Complex.I))‖ = 1
    source
    theorem BGW.StableTrees.Scalar.integrable_stableCF_mul_cexp {α : ℝ} (hα : 1 < α ∧ α ≤ 2) (x : ℝ) :
    MeasureTheory.Integrable (fun (θ : ℝ) => stableCF α θ * Complex.exp (-(↑θ * ↑x * Complex.I))) MeasureTheory.volume
    source
    theorem BGW.StableTrees.Scalar.abs_stableDensity_le {α : ℝ} (x : ℝ) :
    |stableDensity α x| ≤ 1 / (2 * Real.pi) * ∫ (θ : ℝ), ‖stableCF α θ‖

    d_α is bounded.

    source
    theorem BGW.StableTrees.Scalar.norm_cexp_sub_cexp_le (θ x y : ℝ) :
    ‖Complex.exp (-(↑θ * ↑x * Complex.I)) - Complex.exp (-(↑θ * ↑y * Complex.I))‖ ≤ |θ| * |x - y|
    source
    theorem BGW.StableTrees.Scalar.abs_stableDensity_sub_le {α : ℝ} (hα : 1 < α ∧ α ≤ 2) (x y : ℝ) :
    |stableDensity α x - stableDensity α y| ≤ (1 / (2 * Real.pi) * ∫ (θ : ℝ), |θ| * ‖stableCF α θ‖) * |x - y|

    d_α is Lipschitz, with constant (1/2π) ∫ |θ| |exp((-iθ)^α)| dθ.

    source
    theorem BGW.StableTrees.Scalar.lipschitzWith_stableDensity {α : ℝ} (hα : 1 < α ∧ α ≤ 2) :
    LipschitzWith (1 / (2 * Real.pi) * ∫ (θ : ℝ), |θ| * ‖stableCF α θ‖).toNNReal (stableDensity α)
    source
    theorem BGW.StableTrees.Scalar.uniformContinuous_stableDensity {α : ℝ} (hα : 1 < α ∧ α ≤ 2) :
    UniformContinuous (stableDensity α)

    d_α is uniformly continuous.

    source
    theorem BGW.StableTrees.Scalar.continuous_stableDensity {α : ℝ} (hα : 1 < α ∧ α ≤ 2) :
    Continuous (stableDensity α)

    d_α is continuous.

    source
    theorem BGW.StableTrees.Scalar.exists_stableDensity_le {α : ℝ} :
    ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x : ℝ), |stableDensity α x| ≤ M

    d_α is bounded.

    source
    theorem BGW.StableTrees.Scalar.stableDensity_zero {α : ℝ} (hα : 1 < α ∧ α ≤ 2) :
    stableDensity α 0 = Real.Gamma (1 / α + 1) * Real.sin (Real.pi / α) / Real.pi

    The value of d_α at zero: d_α(0) = Γ(1 + 1/α) sin(π/α) / π.

    source
    theorem BGW.StableTrees.Scalar.stableDensity_zero_pos {α : ℝ} (hα : 1 < α ∧ α ≤ 2) :
    0 < stableDensity α 0

    Positivity of the stable density at zero, d_α(0) > 0.