Reverse Martingale Infrastructure

To prove Lévy's downward theorem, we reverse time on finite horizons to obtain forward martingales, then apply the upcrossing inequality.

Main Definitions

• revFiltration: Time-reversed filtration on a finite horizon
• revCEFinite: Time-reversed conditional expectation process

Main Results

• revCEFinite_martingale: The reversed process is a forward martingale
• eLpNorm_one_condExp_le_of_integrable: L¹ boundedness of conditional expectations

def Exchangeability.Probability.revFiltration {Ω : Type u_1} [MeasurableSpace Ω] (𝔽 : ℕ → MeasurableSpace Ω) (h_antitone : Antitone 𝔽) (h_le : ∀ (n : ℕ), 𝔽 n ≤ inferInstance) (N : ℕ) : MeasureTheory.Filtration ℕ inferInstance

Reverse filtration on a finite horizon N.

For an antitone filtration 𝔽, define 𝔾ⁿ_k := 𝔽_{N-k}. Since k ≤ ℓ implies N - ℓ ≤ N - k, and 𝔽 is antitone, we get 𝔽_{N-k} ≤ 𝔽_{N-ℓ}, so 𝔾ⁿ is a (forward) increasing filtration.

Equations

• Exchangeability.Probability.revFiltration 𝔽 h_antitone h_le N = { seq := fun (n : ℕ) => 𝔽 (N - n), mono' := ⋯, le' := ⋯ }

noncomputable def Exchangeability.Probability.revCEFinite {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (f : Ω → ℝ) (𝔽 : ℕ → MeasurableSpace Ω) (N n : ℕ) : Ω → ℝ

Reverse conditional expectation process at finite horizon N.

For n ≤ N, this is just μ[f | 𝔽_{N-n}].

Equations

• Exchangeability.Probability.revCEFinite f 𝔽 N n = μ[f|𝔽 (N - n)]

theorem Exchangeability.Probability.revCEFinite_martingale {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {𝔽 : ℕ → MeasurableSpace Ω} [MeasureTheory.IsProbabilityMeasure μ] (h_antitone : Antitone 𝔽) (h_le : ∀ (n : ℕ), 𝔽 n ≤ inferInstance) (f : Ω → ℝ) (_hf : MeasureTheory.Integrable f μ) (N : ℕ) : MeasureTheory.Martingale (fun (n : ℕ) => revCEFinite f 𝔽 N n) (revFiltration 𝔽 h_antitone h_le N) μ

The reversed process revCEFinite f 𝔽 N is a martingale w.r.t. revFiltration 𝔽 N.

Proof: For i ≤ j, we have 𝔽 (N - j) ≤ 𝔽 (N - i), so by the tower property: E[revCEFinite N j | revFiltration N i] = E[μ[f | 𝔽_{N-j}] | 𝔽_{N-i}] = μ[f | 𝔽_{N-i}] = revCEFinite N i

theorem Exchangeability.Probability.eLpNorm_one_condExp_le_of_integrable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m : MeasurableSpace Ω} (f : Ω → ℝ) (_hf : MeasureTheory.Integrable f μ) : MeasureTheory.eLpNorm μ[f|m] 1 μ ≤ MeasureTheory.eLpNorm f 1 μ

L¹ boundedness of conditional expectations.

This is a standard property: ‖μ[f | m]‖₁ ≤ ‖f‖₁.