Crossings: Pathwise Reversal Lemmas

Pathwise reversal lemmas relating upcrossings of a process to downcrossings of its time reversal. No filtration / integrability content here — this file is the purely combinatorial / pathwise layer.

Main Definitions

• downcrossingsBefore: Downcrossings before time N
• downcrossings: Total downcrossings (supremum over all time horizons)

Main Results

• up_neg_flip_eq_down: up(-b, -a, -X) = down(a, b, X)
• down_neg_flip_eq_up: down(-b, -a, -X) = up(a, b, X)
• upBefore_le_downBefore_rev_succ: upcrossing–downcrossing inequality

noncomputable def Exchangeability.Probability.downcrossingsBefore {Ω : Type u_2} (a b : ℝ) (X : ℕ → Ω → ℝ) (N : ℕ) : Ω → ℕ

Downcrossings before N: defined as upcrossings of negated process with flipped interval. Returns a random variable Ω → ℕ.

Equations

• Exchangeability.Probability.downcrossingsBefore a b X N = MeasureTheory.upcrossingsBefore (-b) (-a) (negProcess X) N

noncomputable def Exchangeability.Probability.downcrossings {Ω : Type u_2} (a b : ℝ) (X : ℕ → Ω → ℝ) : Ω → ENNReal

Total downcrossings: supremum over all time horizons.

Equations

• Exchangeability.Probability.downcrossings a b X ω = ⨆ (N : ℕ), ↑(Exchangeability.Probability.downcrossingsBefore a b X N ω)

theorem Exchangeability.Probability.up_neg_flip_eq_down {Ω : Type u_2} (a b : ℝ) (X : ℕ → Ω → ℝ) : MeasureTheory.upcrossings (-b) (-a) (negProcess X) = downcrossings a b X

Identity 1: Upcrossings of negated process = downcrossings of original. Negation flips crossing direction: up(-b, -a, -X) = down(a, b, X).

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

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

theorem Exchangeability.Probability.upBefore_le_downBefore_rev_succ {Ω : Type u_2} (X : ℕ → Ω → ℝ) (a b : ℝ) (hab : a < b) (N : ℕ) : (fun (ω : Ω) => MeasureTheory.upcrossingsBefore a b X N ω) ≤ fun (ω : Ω) => downcrossingsBefore a b (revProcess X N) (N + 1) ω

Corrected one-way inequality with shifted horizon on the reversed side.

The bijection (τ, σ) ↦ (N-σ, N-τ) maps X upcrossings to Y upcrossings. When τ = 0, the reversed crossing completes at time N. With "before N+1" on the reversed side, this crossing is counted (since N < N+1).

This fixes the boundary issue in upBefore_le_downBefore_rev.