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.

Main results

• upcrossings_bdd_uniform: uniform-in-N bound on the expected number of upcrossings for the reverse martingale of an L¹-bounded f along an antitone filtration

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

Uniform (in N) bound on upcrossings for the reverse martingale.

For an L¹-bounded martingale obtained by reversing an antitone filtration, the expected number of upcrossings is uniformly bounded, independent of the time horizon N.