Downcrossings and Pathwise Reversal Lemmas

Downcrossings are upcrossings after negation and interval flip. These lemmas establish the relationship between upcrossings of a process and downcrossings of its time reversal.

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
• upcrossings_bdd_uniform: Uniform bound on reverse martingale upcrossings
• condExp_exists_ae_limit_antitone: A.S. limit existence for antitone filtrations
• uniformIntegrable_condexp_antitone: UI of conditional expectations
• aestronglyMeasurable_iInf_of_tendsto_ae_antitone: Limit is F_inf-measurable
• ae_limit_is_condexp_iInf: Limit equals condExp w.r.t. intersection σ-algebra

@[simp]

theorem Exchangeability.Probability.revProcess_apply {Ω : Type u_2} (X : ℕ → Ω → ℝ) (N n : ℕ) (ω : Ω) : revProcess X N n ω = X (N - n) ω

@[simp]

theorem Exchangeability.Probability.negProcess_apply {Ω : Type u_2} (X : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : negProcess X n ω = -X n ω

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).

@[simp]

theorem Exchangeability.Probability.negProcess_negProcess {Ω : Type u_2} (X : ℕ → Ω → ℝ) : negProcess (negProcess X) = X

Double negation is identity.

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

Identity 2: Downcrossings of negated process = upcrossings of original. Negation flips crossing direction: down(-b, -a, -X) = up(a, b, X).

theorem Exchangeability.Probability.revProcess_revProcess {Ω : Type u_2} (X : ℕ → Ω → ℝ) (N n : ℕ) (hn : n ≤ N) (ω : Ω) : revProcess (revProcess X N) N n ω = X n ω

Double reversal is identity when applied within bounds.

theorem Exchangeability.Probability.revProcess_negProcess_revProcess {Ω : Type u_2} (X : ℕ → Ω → ℝ) (N n : ℕ) (hn : n ≤ N) (ω : Ω) : revProcess (negProcess (revProcess X N)) N n ω = negProcess X n ω

Composition of reversal and negation simplifies: rev(neg(rev X)) = neg X

theorem Exchangeability.Probability.negProcess_revProcess_negProcess_revProcess {Ω : Type u_2} (X : ℕ → Ω → ℝ) (N n : ℕ) (hn : n ≤ N) (ω : Ω) : negProcess (revProcess (negProcess (revProcess X N)) N) n ω = X n ω

Full composition: neg(rev(neg(rev X))) = X

theorem Exchangeability.Probability.hitting_congr {Ω : Type u_2} {β : Type u_3} {u v : ℕ → Ω → β} {s : Set β} {n m : ℕ} {ω : Ω} (h : ∀ (k : ℕ), n ≤ k → k ≤ m → u k ω = v k ω) : MeasureTheory.hittingBtwn u s n m ω = MeasureTheory.hittingBtwn v s n m ω

Helper: hitting respects pointwise equality on [n, m]

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

Helper: upperCrossingTime respects pointwise equality on [0, N]

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.upperCrossingTime_lt_imp_index_lt {Ω : Type u_2} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω} (hab : a < b) (h : MeasureTheory.upperCrossingTime a b f N n ω < N) : n < N

Index is bounded by completion time when upperCrossingTime < N. If the n-th crossing completes before time N, then n < 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.

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.

theorem Exchangeability.Probability.condExp_exists_ae_limit_antitone {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {𝔽 : ℕ → MeasurableSpace Ω} (h_antitone : Antitone 𝔽) (h_le : ∀ (n : ℕ), 𝔽 n ≤ inferInstance) (f : Ω → ℝ) (hf : MeasureTheory.Integrable f μ) : ∃ (Xlim : Ω → ℝ), MeasureTheory.Integrable Xlim μ ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => μ[f|𝔽 n] ω) Filter.atTop (nhds (Xlim ω))

A.S. existence of the limit of μ[f | 𝔽 n] along an antitone filtration.

This uses the upcrossing inequality applied to the time-reversed martingales to show that the original sequence has finitely many upcrossings and downcrossings a.e., hence converges a.e.

theorem Exchangeability.Probability.uniformIntegrable_condexp_antitone {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {𝔽 : ℕ → MeasurableSpace Ω} (_h_antitone : Antitone 𝔽) (h_le : ∀ (n : ℕ), 𝔽 n ≤ inferInstance) (f : Ω → ℝ) (hf : MeasureTheory.Integrable f μ) : MeasureTheory.UniformIntegrable (fun (n : ℕ) => μ[f|𝔽 n]) 1 μ

Uniform integrability of {μ[f | 𝔽 n]}ₙ for antitone filtration.

This is a direct application of mathlib's Integrable.uniformIntegrable_condExp, which works for any family of sub-σ-algebras (not just filtrations).

theorem Exchangeability.Probability.aestronglyMeasurable_iInf_of_tendsto_ae_antitone {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {𝔽 : ℕ → MeasurableSpace Ω} (h_antitone : Antitone 𝔽) (_h_le : ∀ (n : ℕ), 𝔽 n ≤ inferInstance) {g : ℕ → Ω → ℝ} {Xlim : Ω → ℝ} (hg_meas : ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (g n)) (h_tendsto : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => g n ω) Filter.atTop (nhds (Xlim ω))) : MeasureTheory.AEStronglyMeasurable Xlim μ

Key lemma: A.e. limit of adapted sequence for antitone filtration is F_inf-AEStronglyMeasurable.

For antitone filtration 𝔽 with F_inf = ⨅ 𝔽, if each Xn is 𝔽 n-strongly-measurable and Xn → Xlim a.e., then Xlim is AEStronglyMeasurable[F_inf].

The key observation: For antitone 𝔽 (𝔽 n decreases as n increases):

• For n ≥ N: 𝔽 n ⊆ 𝔽 N (larger index = smaller σ-algebra)
• So {Xn > a} ∈ 𝔽 n ⊆ 𝔽 N for n ≥ N
• The lim sup set ⋂N ⋃{n≥N} {Xn > a} ∈ ⋂_N 𝔽 N = F_inf
• Hence Xlim is F_inf-measurable (up to a.e. equality)

This is crucial for showing that reverse martingale limits satisfy μ[Xlim | F_inf] = Xlim.

theorem Exchangeability.Probability.ae_limit_is_condexp_iInf {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {𝔽 : ℕ → MeasurableSpace Ω} (h_antitone : Antitone 𝔽) (h_le : ∀ (n : ℕ), 𝔽 n ≤ inferInstance) (f : Ω → ℝ) (hf : MeasureTheory.Integrable f μ) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => μ[f|𝔽 n] ω) Filter.atTop (nhds (μ[f|⨅ (n : ℕ), 𝔽 n] ω))

Identification: the a.s. limit equals μ[f | ⨅ n, 𝔽 n].

Uses uniform integrability to pass from a.e. convergence to L¹ convergence, then uses L¹-continuity of conditional expectation to identify the limit.