Time-reversal crossing bound

Reverse-martingale infrastructure bounding the completion time of upcrossings in a time-reversed, negated process. This is a combinatorial ingredient of the reverse-martingale upcrossing argument.

Main definitions

• revProcess: time reversal of a stochastic process up to a horizon N.

Main results

• MeasureTheory.upperCrossingTime_neg_revProcess_le: for a process X with k upcrossings [a→b] completing before time N, the time-reversed negated process -(revProcess X N) has its k-th upcrossing [-b→-a] completing at time ≤ N.

Adapted from cameronfreer/exchangeability (Probability/TimeReversalCrossing.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22). Written Mathlib-shaped for eventual upstreaming.

def MeasureTheory.revProcess {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (N : ℕ) : ℕ → Ω → α

Time reversal of a stochastic process up to time N, using Mathlib's horizon reversal Polynomial.revAt. For n ≤ N this is X (N - n); see revProcess_apply_of_le.

Equations

• MeasureTheory.revProcess X N n ω = X ((Polynomial.revAt N) n) ω

@[simp]

theorem MeasureTheory.revProcess_apply {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (N n : ℕ) (ω : Ω) : revProcess X N n ω = X ((Polynomial.revAt N) n) ω

Defining equation for revProcess (whose body is deliberately not @[expose]d).

theorem MeasureTheory.revProcess_apply_of_le {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) {N n : ℕ} (h : n ≤ N) (ω : Ω) : revProcess X N n ω = X (N - n) ω

Below the horizon, Polynomial.revAt N is genuine subtraction, so revProcess reverses.

theorem MeasureTheory.upperCrossingTime_neg_revProcess_le {Ω : Type u_1} (X : ℕ → Ω → ℝ) (a b : ℝ) (hab : a < b) (N k : ℕ) (ω : Ω) (h_k : upperCrossingTime a b X N k ω < N) : upperCrossingTime (-b) (-a) (-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 -(revProcess X N) has its k-th upcrossing [-b→-a] completing at time ≤ N.