Crossings: pathwise reversal lemmas

Pathwise reversal lemmas relating upcrossings of a process to upcrossings of its negated time reversal. Downcrossings are not reintroduced here: Mathlib's upcrossings (-b) (-a) (-X) already is the downcrossing count, so we phrase everything through Mathlib's upcrossings / upcrossingsBefore of the negated process. No filtration / integrability content here — this is the purely combinatorial / pathwise layer.

Main results

• upcrossingsBefore_congr / upcrossingsBefore_succ_congr: upcrossingsBefore (at horizon N, resp. the free-boundary horizon N + 1) depends only on the path values on [0, N].
• upcrossingsBefore_le_upcrossingsBefore_neg_revProcess_succ: the reversal bound — upcrossings of X on [a, b] before time N are bounded by upcrossings of the negated time reversal -(revProcess X N) on [-b, -a] before time N + 1.

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

theorem MeasureTheory.upcrossingsBefore_congr {Ω : Type u_2} {ι : Type u_3} [Preorder ι] [OrderBot ι] [InfSet ι] {a b : ℝ} {f g : ι → Ω → ℝ} {N : ι} {ω : Ω} (h : ∀ n ≤ N, f n ω = g n ω) : upcrossingsBefore a b f N ω = upcrossingsBefore a b g N ω

Helper: upcrossingsBefore is invariant under pointwise equality on [0, N].

theorem MeasureTheory.upcrossingsBefore_succ_congr {Ω : Type u_2} {a b : ℝ} {f g : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω} (h : ∀ n ≤ N, f n ω = g n ω) : upcrossingsBefore a b f (N + 1) ω = upcrossingsBefore a b g (N + 1) ω

Helper: upcrossingsBefore at horizon N + 1 is invariant under pointwise equality on [0, N]. The extra index N + 1 is a "free boundary" that never affects the crossing count.

theorem MeasureTheory.upcrossingsBefore_le_upcrossingsBefore_neg_revProcess_succ {Ω : Type u_2} (X : ℕ → Ω → ℝ) (a b : ℝ) (hab : a < b) (N : ℕ) (ω : Ω) : upcrossingsBefore a b X N ω ≤ upcrossingsBefore (-b) (-a) (-revProcess X N) (N + 1) ω

Reversed-crossing bound: the upcrossings of X on [a, b] before time N are bounded by the upcrossings of the negated time-reversed process -(revProcess X N) on [-b, -a] before time N + 1. The extra N + 1 horizon on the reversed side is what makes crossings completing exactly at time N count.