Tightness of the actual maximum of the walk's partial sums

The maximum here is evaluated on a single product-law walk path, rather than a maximum of marginal probabilities. An Ottaviani first-exit decomposition and fresh-increment independence upgrade the scalar tightness derived from (H_α) to maximal tightness. This is a consequence of the functional convergence asserted at source lines 846–850, not a proof of that full Skorokhod-topology convergence.

Adapted from PoissonDeclumping/Stable/MaximalTightness.lean in igor-kortchemski/rare-subtree-patterns, commit fc5ef722392b1af41e8b9d5fc45d5a521b7823dd (Apache-2.0).

def BGW.StableTrees.Scalar.FirstExit (R : ℝ) (x : List ℤ) : Prop

A finite prefix first crosses the absolute threshold at its final position.

Equations

• BGW.StableTrees.Scalar.FirstExit R x = (R < |↑x.sum| ∧ ∀ j < x.length, |↑(List.take j x).sum| ≤ R)

theorem BGW.StableTrees.Scalar.maximal_le_two_mul_tail (μ : PMF ℕ) (m : ℕ) (R : ℝ) (hsafe : ∀ j ≤ m, 1 / 2 ≤ (walkLaw μ j).real {z : ℤ | |↑z| ≤ R}) : (walkVecLaw μ m).real {ω : Fin m → ℤ | ∃ k ≤ m, 2 * R < |↑(List.take k (List.ofFn ω)).sum|} ≤ 2 * (walkLaw μ m).real {z : ℤ | R < |↑z|}

Ottaviani's bound for the actual partial-sum maximum. The fresh remainder is within R with probability at least 1/2, uniformly over every possible first-exit time.

theorem BGW.StableTrees.Scalar.maximal_tight {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℝ), 0 < K ∧ ∀ (m : ℕ), 1 ≤ m → (walkVecLaw μ m).real {ω : Fin m → ℤ | ∃ k ≤ m, K * a m < |↑(List.take k (List.ofFn ω)).sum|} ≤ ε

Actual maximal tightness of the Łukasiewicz walk: all partial sums are evaluated on the same product-law path. The constant is uniform over every positive path length.

theorem BGW.StableTrees.Scalar.tendsto_maximal_tail {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {M : ℕ → ℕ} {r : ℕ → ℝ} (hM : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ M n) (hr : Filter.Tendsto (fun (n : ℕ) => r n / a (M n)) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => (walkVecLaw μ (M n)).real {ω : Fin (M n) → ℤ | ∃ k ≤ M n, r n < |↑(List.take k (List.ofFn ω)).sum|}) Filter.atTop (nhds 0)

Maxima stay below any radius that diverges relative to the normalizing scale. This strengthens the marginal-probability consequence used at source lines 1763–1770 and 1912.