Sign probabilities of the spectrally positive stable law

Kendall's density at level one has total mass one. Substituting u = s^(-1/θ) identifies this mass with θ times the negative half-line mass of the stable density. The positive half-line probability follows by complementation, and positive spatial scaling preserves the sign probabilities of every positive-time marginal.

References: J. Bertoin, Lévy Processes (1996), Chapter VIII; V. M. Zolotarev, One-dimensional Stable Distributions (1986), Chapter I.4.

theorem BGW.StableTrees.stableLaw_singleton_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ↑(stableLaw θ) {0} = 0

No atom at 0.

theorem BGW.StableTrees.integral_stableDensity_neg_Ioi {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∫ (u : ℝ) in Set.Ioi 0, Scalar.stableDensity θ (-u) = 1 / θ

Density form: ∫_{u>0} p_1(-u) du = 1/θ.

theorem BGW.StableTrees.stableLaw_Iio_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ↑(stableLaw θ) (Set.Iio 0) = ENNReal.ofReal (1 / θ)

P(X_1 < 0) = 1/θ for the spectrally positive stable law.

theorem BGW.StableTrees.stableLaw_Ioi_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ↑(stableLaw θ) (Set.Ioi 0) = ENNReal.ofReal (1 - 1 / θ)

P(X_1 > 0) = 1 - 1/θ for the spectrally positive stable law.

theorem BGW.StableTrees.stableLawAt_Iio_zero {θ t : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ht : 0 < t) : ↑(stableLawAt θ t) (Set.Iio 0) = ENNReal.ofReal (1 / θ)

Every time marginal has the same sign probabilities (scaling).