Strict positivity of the stable density

The convolution semigroup propagates positivity of p₁(y) to pₙ(n y) for every positive integer n. Scaling then propagates positivity to every real argument: n^(1/θ - 1) x tends to zero, where the density is continuous and strictly positive. This also proves strict positivity of the Gamma factor in Kendall's identity.

Reference: V. M. Zolotarev, One-dimensional Stable Distributions, AMS, 1986, Section 2.7.

theorem BGW.StableTrees.stableDensity_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : ℝ) : 0 < Scalar.stableDensity θ x

The stable density is strictly positive on all of ℝ.

theorem BGW.StableTrees.gammaA_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {a x : ℝ} (ha : a < 1) (hx : 0 < x) : 0 < gammaA θ a x

Strict positivity of the Gamma factor: Γ_a(x) > 0 for a < 1, x > 0; with continuousOn_gammaA (sealed) and gammaA_nonneg (sealed) this completes the item.