Tightness and maximal estimates for real stable-attracted walks

Uniform tightness of the scaled sums yields safe-remainder estimates for Ottaviani's inequality. Together with the normalizer ratio bounds, this gives small-block and finite-horizon maximum control for arbitrary real iid increments.

Reference: P. Billingsley, Convergence of Probability Measures, 2nd ed., 1999, Theorem 9.7 (Ottaviani) and §16 (tightness for processes with independent increments).

theorem BGW.StableTrees.IsRealStableAttracted.isTightMeasureSet_scaledSumLaw {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) : MeasureTheory.IsTightMeasureSet (Set.range fun (n : ℕ) => ↑(Probability.RealWalk.scaledSumLaw ν B n))

The whole sequence of scaled sum laws is uniformly tight (a convergent sequence in the space of probability measures on ℝ has compact closure; Mathlib's isTightMeasureSet_of_isCompact_closure). This absorbs the finite beginning of the sequence.

theorem BGW.StableTrees.IsRealStableAttracted.uniform_tight_partial_sums {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) (η : ℝ) : η > 0 → ∃ K > 0, ∃ (N : ℕ), ∀ n ≥ N, ∀ j ≤ n, (↑(Probability.RealWalk.sumLaw ν j)).real {x : ℝ | K * B n < |x|} ≤ η

Uniform tightness of S_j / B_n, j ≤ n (audit item 7), quantitative form: the exceedance probability of the level K B n is small, for all j ≤ n simultaneously, once n is large.

theorem BGW.StableTrees.IsRealStableAttracted.small_block_max {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) (ε : ℝ) : ε > 0 → ∀ η > 0, ∃ δ > 0, ∃ (N : ℕ), ∀ n ≥ N, ∀ (m : ℕ), ↑m ≤ δ * ↑n + 2 → Probability.RealWalk.maxTail ν m (ε * B n) ≤ η

Small-block maxima (Node 6): maxima over blocks of length ≤ δ n + 2 exceed ε B n with probability at most η, uniformly for large n. The threshold is ε * B n for B n > 0 (eventually). Proof: Ottaviani at half the threshold, with the safe-remainder hypothesis from small_index_ratio and tightness of the full scaled sequence.

theorem BGW.StableTrees.IsRealStableAttracted.horizon_max_tight {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {T : ℝ} (hT : 0 < T) (η : ℝ) : η > 0 → ∃ K > 0, ∃ (N : ℕ), ∀ n ≥ N, Probability.RealWalk.maxTail ν ⌊↑n * T⌋₊ (K * B n) ≤ η

Compact containment on a finite horizon (Node 6): maxima up to ⌊n T⌋₊ stay below K * B n with probability at least 1 - η, for all large n.

theorem BGW.StableTrees.IsRealStableAttracted.isTightMeasureSet_scaled_partial_sums {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) : MeasureTheory.IsTightMeasureSet {μ : MeasureTheory.Measure ℝ | ∃ (n : ℕ), ∃ j ≤ n, μ = MeasureTheory.Measure.map (fun (x : ℝ) => x / B n) ↑(Probability.RealWalk.sumLaw ν j)}

The family {law of S_j / B_n : j ≤ n} over all n is tight (as a set of measures). The finitely many n with small N contribute finitely many tight laws; B n ≤ 0 is harmless because the division by B n is then still a measurable map and each law is a single tight law.