Public stable-density adapters

Public forms of the pointwise and integral facts about the stable transition density.

Reference: V. M. Zolotarev, One-dimensional Stable Distributions (1986); K. Sato (1999), §14.

theorem BGW.StableTrees.stableDensityAt_nonneg {θ t : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ht : 0 < t) (x : ℝ) : 0 ≤ stableDensityAt θ t x

The transition density is nonnegative at positive times.

theorem BGW.StableTrees.stableDensityAt_continuous {θ t : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : Continuous (stableDensityAt θ t)

The transition density is continuous in its spatial variable.

theorem BGW.StableTrees.integral_stableDensityAt {θ t : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ht : 0 < t) : ∫ (x : ℝ), stableDensityAt θ t x = 1

The transition density integrates to one at positive times.

theorem BGW.StableTrees.integrable_stableDensityAt {θ t : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ht : 0 < t) : MeasureTheory.Integrable (stableDensityAt θ t) MeasureTheory.volume

The transition density is integrable at every positive time.

theorem BGW.StableTrees.stableDensityAt_le_of_ge {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t₀ : ℝ} (ht₀ : 0 < t₀) : ∃ (C : ℝ), ∀ (t : ℝ), t₀ ≤ t → ∀ (x : ℝ), stableDensityAt θ t x ≤ C

For times bounded below by t₀ > 0, the transition densities have a common upper bound.

theorem BGW.StableTrees.stableLawAt_singleton {θ t : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ht : 0 < t) (x : ℝ) : ↑(stableLawAt θ t) {x} = 0

The stable transition law has no atoms at positive times.

theorem BGW.StableTrees.stableDensityAt_one (θ x : ℝ) : stableDensityAt θ 1 x = Scalar.stableDensity θ x

At time one, the transition density is the normalized stable density.

theorem BGW.StableTrees.stableDensityAt_jointContinuous {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ContinuousOn (fun (z : ℝ × ℝ) => stableDensityAt θ z.1 z.2) {z : ℝ × ℝ | 0 < z.1}

Joint continuity of the transition density in positive time and space.