Crossings: uniform upcrossing bound for reverse martingales

The L¹-uniform upcrossing bound used in the reverse-martingale antitone-limit argument. Built on top of Pathwise.lean and Reverse.lean.

Main results

• exists_lintegral_upcrossings_condExp_le: a uniform crossing bound for the antitone conditional-expectation sequence n ↦ μ[f | 𝔽 n], for integrable f.

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

theorem MeasureTheory.exists_lintegral_upcrossings_condExp_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : Measure Ω} {𝔽 : ℕ → MeasurableSpace Ω} [IsFiniteMeasure μ] (h_antitone : Antitone 𝔽) (h_le : ∀ (n : ℕ), 𝔽 n ≤ inferInstance) (f : Ω → ℝ) (hf : Integrable f μ) (a b : ℝ) (hab : a < b) : ∃ C < ⊤, ∫⁻ (ω : Ω), upcrossings a b (fun (n : ℕ) => μ[f | 𝔽 n]) ω ∂μ ≤ C

Uniform crossing bound for the antitone conditional-expectation sequence.

For an antitone filtration 𝔽 and integrable f, the expected number of upcrossings of the conditional-expectation process n ↦ μ[f | 𝔽 n] on any interval [a, b] is finite — the L¹ reverse-martingale upcrossing bound. This is the crossing bound consumed by the antitone-limit (Lévy downward) argument.