Martingale Helper Lemmas (Fully Proved)

This file contains fully-proved helper lemmas related to martingales and conditional expectations. These are extracted from exploratory work and may be useful for future developments.

All lemmas here are complete - no axioms, no sorries.

Contents

1. Reverse conditional expectation helpers:

   • revCE: Definition of reverse martingale along decreasing filtration
   • revCE_tower: Tower property for reverse conditional expectations
   • revCE_L1_bdd: L¹ boundedness

2. de la Vallée-Poussin infrastructure:

   • deLaValleePoussin_eventually_ge_id: Extract threshold from superlinear growth

3. Fatou-type lemmas:

   • lintegral_fatou_ofReal_norm: Fatou's lemma for ENNReal.ofReal ∘ ‖·‖

Note: Incomplete conditional distribution lemmas have been moved to MartingaleUnused.lean.

References

• Durrett, Probability: Theory and Examples (2019), Section 5.5
• Williams, Probability with Martingales (1991)

Reverse Conditional Expectation Helpers

def Exchangeability.Probability.revCE {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (F : ℕ → MeasurableSpace Ω) (f : Ω → ℝ) (n : ℕ) : Ω → ℝ

Reverse martingale along a decreasing chain: X n := condExp μ (F n) f.

Equations

• Exchangeability.Probability.revCE μ F f n = μ[f|F n]

theorem Exchangeability.Probability.revCE_tower {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {F : ℕ → MeasurableSpace Ω} (hF : Antitone F) (h_le : ∀ (n : ℕ), F n ≤ inferInstance) (f : Ω → ℝ) {n m : ℕ} (hmn : n ≤ m) : μ[revCE μ F f n|F m] =ᵐ[μ] revCE μ F f m

Tower property in the reverse direction: for m ≥ n, E[X_n | F_m] = X_m.

theorem Exchangeability.Probability.revCE_L1_bdd {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {F : ℕ → MeasurableSpace Ω} (_h_le : ∀ (n : ℕ), F n ≤ inferInstance) (f : Ω → ℝ) (_hf : MeasureTheory.Integrable f μ) (n : ℕ) : MeasureTheory.eLpNorm (revCE μ F f n) 1 μ ≤ MeasureTheory.eLpNorm f 1 μ

L¹ boundedness of the reverse martingale.

de la Vallée-Poussin Infrastructure

theorem Exchangeability.Probability.deLaValleePoussin_eventually_ge_id (Φ : ℝ → ℝ) (hΦ_tail : Filter.Tendsto (fun (t : ℝ) => Φ t / t) Filter.atTop Filter.atTop) : ∃ R > 0, ∀ ⦃t : ℝ⦄, t ≥ R → t ≤ Φ t

From the de la Vallée-Poussin tail condition Φ(t)/t → ∞, extract a threshold R > 0 such that t ≤ Φ t for all t ≥ R.

This is used to control the small-values region when applying the de la Vallée-Poussin criterion for uniform integrability.

Fatou-Type Lemmas

theorem Exchangeability.Probability.lintegral_fatou_ofReal_norm {α : Type u_2} {β : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasurableSpace β] [NormedAddCommGroup β] [BorelSpace β] {u : ℕ → α → β} {g : α → β} (hae : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => u n x) Filter.atTop (nhds (g x))) (hu_meas : ∀ (n : ℕ), AEMeasurable (fun (x : α) => ENNReal.ofReal ‖u n x‖) μ) (_hg_meas : AEMeasurable (fun (x : α) => ENNReal.ofReal ‖g x‖) μ) : ∫⁻ (x : α), ENNReal.ofReal ‖g x‖ ∂μ ≤ Filter.liminf (fun (n : ℕ) => ∫⁻ (x : α), ENNReal.ofReal ‖u n x‖ ∂μ) Filter.atTop

Fatou's lemma on ENNReal.ofReal ∘ ‖·‖ along an a.e. pointwise limit.

If u n x → g x a.e., then ∫⁻ ‖g‖ ≤ liminf (∫⁻ ‖u n‖).