Documentation

LeanPool.RareSubtreePatterns.Stable.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 PoissonDeclumping.Stable.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 PoissonDeclumping.Stable.Analytic (this replaces the contour rotation).

source
noncomputable def PoissonDeclumping.Stable.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 PoissonDeclumping.Stable.norm_cexp_neg_mul_I (θ x : ℝ) :
    ‖Complex.exp (-(↑θ * ↑x * Complex.I))‖ = 1
    source
    theorem PoissonDeclumping.Stable.integrable_stableCF_mul_cexp {α : ℝ} (hα : 1 < α ∧ α ≤ 2) (x : ℝ) :
    MeasureTheory.Integrable (fun (θ : ℝ) => stableCF α θ * Complex.exp (-(↑θ * ↑x * Complex.I))) MeasureTheory.volume
    source
    theorem PoissonDeclumping.Stable.abs_stableDensity_le {α : ℝ} (x : ℝ) :
    |stableDensity α x| ≤ 1 / (2 * Real.pi) * ∫ (θ : ℝ), ‖stableCF α θ‖

    d_α is bounded.

    source
    theorem PoissonDeclumping.Stable.norm_cexp_sub_cexp_le (θ x y : ℝ) :
    ‖Complex.exp (-(↑θ * ↑x * Complex.I)) - Complex.exp (-(↑θ * ↑y * Complex.I))‖ ≤ |θ| * |x - y|
    source
    theorem PoissonDeclumping.Stable.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 PoissonDeclumping.Stable.lipschitzWith_stableDensity {α : ℝ} (hα : 1 < α ∧ α ≤ 2) :
    LipschitzWith (1 / (2 * Real.pi) * ∫ (θ : ℝ), |θ| * ‖stableCF α θ‖).toNNReal (stableDensity α)
    source
    theorem PoissonDeclumping.Stable.uniformContinuous_stableDensity {α : ℝ} (hα : 1 < α ∧ α ≤ 2) :
    UniformContinuous (stableDensity α)

    d_α is uniformly continuous.

    source
    theorem PoissonDeclumping.Stable.continuous_stableDensity {α : ℝ} (hα : 1 < α ∧ α ≤ 2) :
    Continuous (stableDensity α)

    d_α is continuous.

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

    d_α is bounded.

    source
    theorem PoissonDeclumping.Stable.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 PoissonDeclumping.Stable.stableDensity_zero_pos {α : ℝ} (hα : 1 < α ∧ α ≤ 2) :
    0 < stableDensity α 0

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