Time-Reversal Crossing Bound

This file proves that upcrossings in a time-reversed and negated process complete within the expected time bound, which is key to martingale convergence proofs.

Main Results

• timeReversal_crossing_bound: For a process X with upcrossings [a→b] before time N, the time-reversed negated process Y has its upcrossings [-b→-a] completing at time ≤ N.

Mathematical Background

The bijection (τ, σ) ↦ (N-σ, N-τ) maps upcrossings of X to upcrossings of the negated reversed process Y = -X(N-·). The key bound is:

• If X's crossing is at times (τ, σ) with 0 ≤ τ < σ < N
• Then Y's crossing is at times (N-σ, N-τ) with 0 < N-σ < N-τ ≤ N

Since τ ≥ 0, we have N-τ ≤ N, giving the desired bound.

The proof uses induction on the crossing index m, tracking that Y's m-th crossing completes by time N - lowerCrossingTime X (k-m), which is ≤ N for m = k.

Key Technique

The proof relies on hittingBtwn_le_of_mem to bound hitting times: if the target set is reached at time t with the search starting at s ≤ t ≤ horizon, then hitting ≤ t.

References

• Williams (1991), Probability with Martingales, Theorem 11.9 (upcrossing lemma)
• Durrett (2019), Probability: Theory and Examples, Section 5.5

def negProcess {Ω : Type u_1} (X : ℕ → Ω → ℝ) : ℕ → Ω → ℝ

Negation of a stochastic process.

Equations

• negProcess X n ω = -X n ω

def revProcess {Ω : Type u_1} (X : ℕ → Ω → ℝ) (N : ℕ) : ℕ → Ω → ℝ

Time reversal of a stochastic process up to time N.

Equations

• revProcess X N n ω = X (N - n) ω

theorem timeReversal_crossing_bound {Ω : Type u_1} (X : ℕ → Ω → ℝ) (a b : ℝ) (hab : a < b) (N k : ℕ) (ω : Ω) (h_k : MeasureTheory.upperCrossingTime a b X N k ω < N) (_h_neg : -b < -a) : MeasureTheory.upperCrossingTime (-b) (-a) (negProcess (revProcess X N)) (N + 1) k ω ≤ N

Time-reversal crossing bound.

For a process X with k upcrossings [a→b] completing before time N, the time-reversed negated process Y = negProcess (revProcess X N) has its k upcrossings [-b→-a] completing at time ≤ N.

The proof uses the bijection (τ, σ) ↦ (N-σ, N-τ) which maps X's crossings to Y's crossings in reverse order. The greedy upcrossing algorithm finds these crossings with completion times bounded by hittingBtwn_le_of_mem.