Tightness of real walk step paths

The laws of the floor-step paths of a real iid walk are tight on Skorokhod space. The proof transfers compact containment and modulus bounds from the walk to its path law.

This is the tightness half of the functional limit theorem for walks in a stable domain of attraction (item C17 of CLASSICAL_THEORY_INPUTS.md), through Billingsley's criterion with the modulus w' (P. Billingsley, Convergence of Probability Measures, 1999, Theorem 13.2).

theorem BGW.Skorokhod.continuous_realStepPath (T : ℝ) (n : ℕ) (b : ℝ) : Continuous (realStepPath T n b)

The step path depends continuously on the real walk with its product topology.

theorem BGW.Skorokhod.measurable_realStepPath (T : ℝ) (n : ℕ) (b : ℝ) : Measurable (realStepPath T n b)

The continuous step-path map is Borel measurable.

theorem BGW.Skorokhod.realStepPath_apply_zero {T : ℝ} (hT : 0 ≤ T) (n : ℕ) (b : ℝ) (ω : ℕ → ℝ) : (realStepPath T n b ω) ⟨0, ⋯⟩ = 0

The step path starts at zero whenever its time interval contains zero.

noncomputable def BGW.StableTrees.stepPathLaw (ν : MeasureTheory.ProbabilityMeasure ℝ) (T : ℝ) (B : ℕ → ℝ) (n : ℕ) : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)

The law of the floor-step path t ↦ S_{⌊n t⌋} / B n on [0,T], as the genuine pushforward of iidLaw ν under the canonical walk map. The normalizer B n is arbitrary; no attraction hypothesis is needed to define the law.

Equations

• BGW.StableTrees.stepPathLaw ν T B n = (BGW.Probability.RealWalk.iidLaw ν).map (BGW.Skorokhod.realStepPath T n (B n))

theorem BGW.StableTrees.coe_stepPathLaw (ν : MeasureTheory.ProbabilityMeasure ℝ) (T : ℝ) (B : ℕ → ℝ) (n : ℕ) : ↑(stepPathLaw ν T B n) = MeasureTheory.Measure.map (Skorokhod.realStepPath T n (B n)) ↑(Probability.RealWalk.iidLaw ν)

The coercion of stepPathLaw to a measure is the pushforward of the canonical walk measure.

theorem BGW.StableTrees.isTightMeasureSet_stepPathLaw_singleton (ν : MeasureTheory.ProbabilityMeasure ℝ) (T : ℝ) (B : ℕ → ℝ) (n : ℕ) : MeasureTheory.IsTightMeasureSet {↑(stepPathLaw ν T B n)}

Every individual step-path law is tight, independently of attraction assumptions.

theorem BGW.StableTrees.stepPathLaw_not_mem_Icc_le (ν : MeasureTheory.ProbabilityMeasure ℝ) {T : ℝ} (hT : 0 < T) (B : ℕ → ℝ) (n : ℕ) (hB : 0 < B n) (K : ℝ) : ↑(stepPathLaw ν T B n) {f : Skorokhod.D T ℝ | ∃ (t : ↑(Set.Icc 0 T)), f t ∉ Set.Icc (-K) K} ≤ ENNReal.ofReal (Probability.RealWalk.maxTail ν ⌊↑n * T⌋₊ (K * B n))

Compact containment of a step path is bounded by the walk's finite-horizon maximum tail.

theorem BGW.StableTrees.measureReal_initialBad_le (ν : MeasureTheory.ProbabilityMeasure ℝ) (T : ℝ) (n : ℕ) {b ε δ : ℝ} (hb : 0 < b) : (↑(Probability.RealWalk.iidLaw ν)).real {ω : ℕ → ℝ | Probability.RealWalk.initialBad T n b ε δ ω} ≤ Probability.RealWalk.maxTail ν ⌊2 * ↑n * δ⌋₊ (ε * b)

The initial-window bad event is bounded by the corresponding short-block maximum.

theorem BGW.StableTrees.measureReal_terminalBad_le (ν : MeasureTheory.ProbabilityMeasure ℝ) {T : ℝ} (n : ℕ) {b ε δ : ℝ} (hb : 0 < b) (hδ : 0 ≤ δ) (hδT : 2 * δ ≤ T) : (↑(Probability.RealWalk.iidLaw ν)).real {ω : ℕ → ℝ | Probability.RealWalk.terminalBad T n b ε δ ω} ≤ Probability.RealWalk.maxTail ν (⌊↑n * T⌋₊ - ⌊↑n * (T - 2 * δ)⌋₊) (ε * b)

The terminal-window bad event is bounded using a fresh start at its left endpoint.

theorem BGW.StableTrees.floor_sub_floor_le {T : ℝ} (n : ℕ) {δ : ℝ} (hδ : 0 ≤ δ) (hδT : 2 * δ ≤ T) : ↑(⌊↑n * T⌋₊ - ⌊↑n * (T - 2 * δ)⌋₊) ≤ 2 * ↑n * δ + 1

The terminal window spans at most 2 n δ + 1 discrete indices.

theorem BGW.StableTrees.stepPathLaw_modulus_le (ν : MeasureTheory.ProbabilityMeasure ℝ) {T : ℝ} (hT : 0 < T) (B : ℕ → ℝ) {n : ℕ} (hn : 1 ≤ n) (hB : 0 < B n) {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (hδT : 4 * δ < T) : ↑(stepPathLaw ν T B n) {f : Skorokhod.D T ℝ | 4 * ε < Skorokhod.cadlagModulus f δ} ≤ ENNReal.ofReal ((↑(Probability.RealWalk.iidLaw ν)).real {ω : ℕ → ℝ | Probability.RealWalk.closeExit ⌊↑n * T⌋₊ (ε * B n) ⌈2 * ↑n * δ + 2⌉₊ ω} + (↑(Probability.RealWalk.iidLaw ν)).real {ω : ℕ → ℝ | Probability.RealWalk.initialBad T n (B n) ε δ ω} + (↑(Probability.RealWalk.iidLaw ν)).real {ω : ℕ → ℝ | Probability.RealWalk.terminalBad T n (B n) ε δ ω})

The outer measure of the path modulus event is controlled by the three finite-coordinate bad events from the exit partition. Inner regularity on the walk space bridges the potentially nonmeasurable modulus event without applying Measure.map to it.

Eventual estimates and tightness for an attracted walk

theorem BGW.StableTrees.IsRealStableAttracted.stepPath_bounded_eventually {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {T : ℝ} (hT : 0 < T) (η : ℝ) : η > 0 → ∃ (K : Set ℝ), Bornology.IsBounded K ∧ ∃ (N : ℕ), ∀ n ≥ N, ↑(stepPathLaw ν T B n) {f : Skorokhod.D T ℝ | ∃ (t : ↑(Set.Icc 0 T)), f t ∉ K} ≤ ENNReal.ofReal η

For every positive tolerance, the step-path laws eventually stay in one bounded interval with all but that much mass.

theorem BGW.StableTrees.IsRealStableAttracted.stepPath_modulus_eventually {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {T : ℝ} (hT : 0 < T) (ε : ℝ) : ε > 0 → ∀ η > 0, ∃ (δ : ℝ), 0 < δ ∧ δ < T ∧ ∃ (N : ℕ), ∀ n ≥ N, ↑(stepPathLaw ν T B n) {f : Skorokhod.D T ℝ | ε < Skorokhod.cadlagModulus f δ} ≤ ENNReal.ofReal η

The step-path laws eventually have arbitrarily small Skorokhod modulus at a sufficiently short time scale.

theorem BGW.StableTrees.IsRealStableAttracted.isTightMeasureSet_stepPathLaw {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {T : ℝ} (hT : 0 < T) : MeasureTheory.IsTightMeasureSet (Set.range fun (n : ℕ) => ↑(stepPathLaw ν T B n))

The family of step-path laws of an attracted walk is tight in the Skorokhod space.