OrderDual Infrastructure for Martingale Convergence

This section shows why reindexing via OrderDual ℕ cannot convert Lévy's upward theorem into the downward theorem.

Main Results

• Filtration.ofAntitone: Package a decreasing sequence as an increasing filtration on ℕᵒᵈ
• iSup_ofAntitone_eq_F0: For antitone F, ⨆ i, F i.ofDual = F 0 (not ⨅ n, F n!)

def Exchangeability.Probability.Filtration.ofAntitone {Ω : Type u_1} [MeasurableSpace Ω] (F : ℕ → MeasurableSpace Ω) (hF : Antitone F) (hle : ∀ (n : ℕ), F n ≤ inferInstance) : MeasureTheory.Filtration ℕᵒᵈ inferInstance

Package a decreasing family of σ-algebras on ℕ as an increasing filtration on ℕᵒᵈ.

For a decreasing sequence (𝔽 n) of σ-algebras, this creates an increasing filtration on OrderDual ℕ where 𝔾 i := 𝔽 (ofDual i). Since i ≤ j in ℕᵒᵈ iff ofDual j ≤ ofDual i in ℕ, antitonicity of 𝔽 becomes monotonicity of 𝔾.

Equations

• Exchangeability.Probability.Filtration.ofAntitone F hF hle = { seq := fun (i : ℕᵒᵈ) => F (OrderDual.ofDual i), mono' := ⋯, le' := ⋯ }

@[simp]

theorem Exchangeability.Probability.Filtration.ofAntitone_apply {Ω : Type u_1} [MeasurableSpace Ω] (F : ℕ → MeasurableSpace Ω) (hF : Antitone F) (hle : ∀ (n : ℕ), F n ≤ inferInstance) (i : ℕᵒᵈ) : ↑(ofAntitone F hF hle) i = F (OrderDual.ofDual i)

theorem Exchangeability.Probability.iSup_ofAntitone_eq_F0 {Ω : Type u_1} (F : ℕ → MeasurableSpace Ω) (hF : Antitone F) : ⨆ (i : ℕᵒᵈ), F (OrderDual.ofDual i) = F 0

For an antitone chain of σ-algebras, the supremum equals the first term.

Key insight: For an antitone sequence F : ℕ → MeasurableSpace Ω, we have ⨆ i : ℕᵒᵈ, F i.ofDual = F 0 because F n ≤ F 0 for all n (by antitonicity), and F 0 is one of the terms.

Why the OrderDual approach fails: This shows that reindexing via ℕᵒᵈ cannot turn ⨆ into ⨅. For example, if F 0 = ⊤ and F n = ⊥ for n > 0, then: ⨆ i, F i.ofDual = ⊤ but ⨅ n, F n = ⊥ Therefore, applying Lévy's upward theorem to the OrderDual filtration would give convergence to μ[f | F 0], not μ[f | ⨅ n, F n].