Quantile analysis

Ported from BGWLeaves/StableAnalysis/QuantileAnalysis.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

theorem BGW.StableTrees.Attraction.QuantileAnalysis.truncSecondMoment_nonneg (ν : MeasureTheory.Measure ℤ) (x : ℝ) : 0 ≤ truncSecondMoment ν x

theorem BGW.StableTrees.Attraction.QuantileAnalysis.truncSecondMoment_mono_nonneg {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {x y : ℝ} (hx : 0 ≤ x) (hxy : x ≤ y) : truncSecondMoment ν x ≤ truncSecondMoment ν y

theorem BGW.StableTrees.Attraction.QuantileAnalysis.norming_monotone_of_infinite_variance {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hinf : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) (θ : ℝ) (hθ : 1 < θ ∧ θ ≤ 2) : Monotone (norming ν θ)

Under an infinite second moment and the paper's lower support bound, the explicit norming sequence is nondecreasing for every 1 < θ ≤ 2. Its n = 0 values use the stated sInf/sSup conventions.

theorem BGW.StableTrees.Attraction.QuantileAnalysis.locallimit_remark (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hDA : ∃ (b : ℕ → ℝ), IsStableAttracted ν 2 (mean ν) b) (hinf : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) : Filter.Tendsto (fun (n : ℕ) => norming ν 2 n / √↑n) Filter.atTop Filter.atTop ∧ Monotone fun (n : ℕ) => norming ν 2 n / √↑n

Remark after the strong local limit theorem: for infinite variance and θ = 2, h(n) = a_n/√n tends to ∞ and is nondecreasing, for the corrected norming a_n = √(n K(z_n)/2).