Deterministic exit partitions

Restart exit times give a finite partition with small oscillation on its half-open blocks. When successive exits of the walk are far apart and the initial and terminal windows are good, Billingsley's modulus w' of the rescaled step path t ↦ S_{⌊nt⌋} / b is at most 4ε (cadlagModulus_realStepPath_le). This is the deterministic step of the tightness argument for walks in a stable domain of attraction (Billingsley 1999, §12–13), following the campaign's audited plan (node 8).

noncomputable def BGW.Probability.RealWalk.nextExit (M : ℕ) (r : ℝ) (ω : ℕ → ℝ) (a : ℕ) : ℕ

The first index k ∈ (a, M] with |S_k - S_a| > r, and the sentinel M + 1 if none.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGW.Probability.RealWalk.exitTimes (M : ℕ) (r : ℝ) (ω : ℕ → ℝ) : ℕ → ℕ

Restart exit times: exitTimes M r ω 0 = 0 and the (j+1)-st exit is the first exit of the walk restarted at the j-th one; the sentinel M + 1 (absorbing) means "no further exit up to index M". Actual exits are ≤ M.

Equations

• One or more equations did not get rendered due to their size.
• BGW.Probability.RealWalk.exitTimes M r ω 0 = 0

noncomputable def BGW.Probability.RealWalk.exitCount (M : ℕ) (r : ℝ) (ω : ℕ → ℝ) : ℕ

The number of actual exits (indices ≤ M, not counting the starting point 0).

Equations

• BGW.Probability.RealWalk.exitCount M r ω = {j ∈ Finset.range (M + 1) | 1 ≤ j ∧ BGW.Probability.RealWalk.exitTimes M r ω j ≤ M}.card

def BGW.Probability.RealWalk.closeExit (M : ℕ) (r : ℝ) (l : ℕ) (ω : ℕ → ℝ) : Prop

Two successive actual exits (the first being a genuine exit, j ≥ 1) are at most l indices apart. The gap between the start 0 and the first exit is deliberately not covered (it is the initialBad event).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGW.Probability.RealWalk.stepValue (n : ℕ) (b : ℝ) (ω : ℕ → ℝ) (t : ℝ) : ℝ

The step path value S_{⌊n t⌋} / b at a real time t.

Equations

• BGW.Probability.RealWalk.stepValue n b ω t = BGW.Probability.RealWalk.partialSum ω ⌊↑n * t⌋₊ / b

def BGW.Probability.RealWalk.initialBad (T : ℝ) (n : ℕ) (b ε δ : ℝ) (ω : ℕ → ℝ) : Prop

Initial window: the path moves by more than ε from its start within time 2δ.

Equations

• BGW.Probability.RealWalk.initialBad T n b ε δ ω = ∃ (t : ℝ), 0 ≤ t ∧ t ≤ 2 * δ ∧ t ≤ T ∧ ε < |BGW.Probability.RealWalk.stepValue n b ω t - BGW.Probability.RealWalk.stepValue n b ω 0|

def BGW.Probability.RealWalk.terminalBad (T : ℝ) (n : ℕ) (b ε δ : ℝ) (ω : ℕ → ℝ) : Prop

Terminal window: after time T - 2δ the path moves by more than ε from its value at T - 2δ (measured from the left endpoint of the window, up to and including T).

Equations

• One or more equations did not get rendered due to their size.

def BGW.Probability.RealWalk.edgeBad (T : ℝ) (n : ℕ) (b ε δ : ℝ) (ω : ℕ → ℝ) : Prop

The walk oscillates by more than ε b in the initial window [0, 2δ] or in the terminal window [T - 2δ, T].

Equations

• BGW.Probability.RealWalk.edgeBad T n b ε δ ω = (BGW.Probability.RealWalk.initialBad T n b ε δ ω ∨ BGW.Probability.RealWalk.terminalBad T n b ε δ ω)

noncomputable def BGW.Skorokhod.realStepPath (T : ℝ) (n : ℕ) (b : ℝ) (ω : ℕ → ℝ) : D T ℝ

The càdlàg floor-step path t ↦ S_{⌊n t⌋} / b on [0,T] (Node 2). The same formula is used at T: if n T is an integer there is a genuine terminal jump.

Equations

• BGW.Skorokhod.realStepPath T n b ω = { toFun := fun (t : ↑(Set.Icc 0 T)) => BGW.Probability.RealWalk.partialSum ω ⌊↑n * ↑t⌋₊ / b, isCadlag' := ⋯ }

theorem BGW.Skorokhod.realStepPath_apply {T : ℝ} {n : ℕ} {b : ℝ} {ω : ℕ → ℝ} (t : ↑(Set.Icc 0 T)) : (realStepPath T n b ω) t = Probability.RealWalk.partialSum ω ⌊↑n * ↑t⌋₊ / b

Value of the step path: the partial sum up to ⌊n t⌋, divided by b.

theorem BGW.Skorokhod.realStepPath_apply_eq_stepValue {T : ℝ} {n : ℕ} {b : ℝ} {ω : ℕ → ℝ} (t : ↑(Set.Icc 0 T)) : (realStepPath T n b ω) t = Probability.RealWalk.stepValue n b ω ↑t

The step path agrees with stepValue.

theorem BGW.Skorokhod.cadlagModulus_realStepPath_le {T : ℝ} {n : ℕ} {b ε δ : ℝ} {ω : ℕ → ℝ} (hT : 0 < T) (hn : 1 ≤ n) (hb : 0 < b) (hε : 0 < ε) (hδ : 0 < δ) (hδT : 4 * δ < T) (hsep : ¬Probability.RealWalk.closeExit ⌊↑n * T⌋₊ (ε * b) ⌈2 * ↑n * δ + 2⌉₊ ω) (hinit : ¬Probability.RealWalk.initialBad T n b ε δ ω) (hterm : ¬Probability.RealWalk.terminalBad T n b ε δ ω) : cadlagModulus (realStepPath T n b ω) δ ≤ 4 * ε

Node 8, deterministic bound. Hypotheses (i) no close consecutive exits at scale ε b, with index gap l = ⌈2 n δ + 2⌉₊ (so that consecutive cuts are more than 2δ apart in time, the +2 absorbing the floors), (ii) no big initial move, (iii) no big terminal move. The exits live in the walk of length M = ⌊n T⌋₊. Conclusion: w'(δ) ≤ 4 ε for Billingsley's modulus (half-open blocks, all steps > δ, δ < T).