Lévy's downward theorem, L¹ version (R3 follow-up; Mathlib-upstream candidate, #24)

The narrow reverse-martingale convergence the relational extremality theory needs: along an antitone sequence of sub-σ-algebras, conditional expectations converge in L¹ to the conditional expectation on the intersection. Mathlib has Lévy's upward theorem (Mathlib/Probability/Martingale/Convergence.lean); this file provides the downward L¹ form by the orthogonal-projection route (no upcrossing/almost-everywhere machinery):

• Submodule.starProjection_tendsto_iInf — orthogonal projections onto an antitone sequence of subspaces converge to the projection onto the infimum (the antitone twin of starProjection_tendsto_closure_iSup, via orthogonal complements);
• MeasureTheory.lpMeas_iInf_of_antitone — the Lᵖ-subspace of an infimum σ-algebra is the intersection of the Lᵖ-subspaces (limsup representative trick);
• MeasureTheory.tendsto_eLpNorm_condExp_iInf — Lévy downward, L¹: for integrable f and antitone 𝒢, eLpNorm (μ[f|𝒢 n] − μ[f|⨅ n, 𝒢 n]) 1 μ → 0 (via the L² case and an ε/3 density argument).

Antitone projection convergence

theorem Submodule.starProjection_tendsto_iInf {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : ℕ → Submodule 𝕜 E) [∀ (i : ℕ), (U i).HasOrthogonalProjection] [(⨅ (i : ℕ), U i).HasOrthogonalProjection] (hU : Antitone U) (x : E) : Filter.Tendsto (fun (i : ℕ) => (U i).starProjection x) Filter.atTop (nhds ((⨅ (i : ℕ), U i).starProjection x))

Orthogonal projections along an antitone sequence of subspaces converge to the projection onto the infimum — the antitone twin of starProjection_tendsto_closure_iSup, by passing to orthogonal complements.

The L²-subspace of an infimum σ-algebra

theorem MeasureTheory.lpMeas_mono {α : Type u_1} {m m' m0 : MeasurableSpace α} {μ : Measure α} (h : m ≤ m') {p : ENNReal} : lpMeas ℝ ℝ m p μ ≤ lpMeas ℝ ℝ m' p μ

lpMeas is monotone in the σ-algebra. (m0 is the ambient σ-algebra of μ, following the {m m0} convention of the ConditionalExpectation files: it is determined by μ at application sites and is not required to relate to m or m', so the lemma applies with sub-σ-algebras of any common ambient.)

theorem MeasureTheory.lpMeas_iInf_of_antitone {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} (𝒢 : ℕ → MeasurableSpace α) (hanti : Antitone 𝒢) {p : ENNReal} : ⨅ (n : ℕ), lpMeas ℝ ℝ (𝒢 n) p μ = lpMeas ℝ ℝ (⨅ (n : ℕ), 𝒢 n) p μ

The Lᵖ-subspace of an infimum σ-algebra is the intersection of the subspaces along an antitone sequence: a function a.e.-measurable for every 𝒢 n has the a.e.-limsup representative, which is measurable for the infimum. (m0 is the ambient σ-algebra of μ, determined at application sites.)

Lévy downward, L² version

theorem MeasureTheory.tendsto_eLpNorm_condExp_iInf_of_memLp {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] (𝒢 : ℕ → MeasurableSpace α) (hanti : Antitone 𝒢) (h𝒢 : ∀ (n : ℕ), 𝒢 n ≤ m0) {f : α → ℝ} (hf : MemLp f 2 μ) : Filter.Tendsto (fun (n : ℕ) => eLpNorm (μ[f | 𝒢 n] - μ[f | ⨅ (n : ℕ), 𝒢 n]) 2 μ) Filter.atTop (nhds 0)

Lévy's downward theorem, L² version: for f ∈ L² and an antitone sequence of sub-σ-algebras 𝒢, the conditional expectations μ[f|𝒢 n] converge in L² to μ[f|⨅ n, 𝒢 n]. Conditional expectation on L² is the orthogonal projection onto lpMeas, so this is Submodule.starProjection_tendsto_iInf transported along lpMeas_iInf_of_antitone.

Lévy downward, L¹ version

theorem MeasureTheory.tendsto_eLpNorm_condExp_iInf {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ] (𝒢 : ℕ → MeasurableSpace α) (hanti : Antitone 𝒢) (h𝒢 : ∀ (n : ℕ), 𝒢 n ≤ m0) {f : α → ℝ} (hf : Integrable f μ) : Filter.Tendsto (fun (n : ℕ) => eLpNorm (μ[f | 𝒢 n] - μ[f | ⨅ (n : ℕ), 𝒢 n]) 1 μ) Filter.atTop (nhds 0)

Lévy's downward theorem, L¹ version: for integrable f and an antitone sequence of sub-σ-algebras 𝒢, the conditional expectations μ[f|𝒢 n] converge in L¹ to μ[f|⨅ n, 𝒢 n]. Proved by an ε/3 argument from the L² case (tendsto_eLpNorm_condExp_iInf_of_memLp), approximating f by a simple function.

theorem MeasureTheory.condExp_ae_eq_integral_of_forall_zero_or_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ] {m' : MeasurableSpace α} (hm' : m' ≤ m0) (htriv : ∀ (s : Set α), MeasurableSet s → μ s = 0 ∨ μ s = 1) {f : α → ℝ} (hf : Integrable f μ) : μ[f | m'] =ᵐ[μ] fun (x : α) => ∫ (x : α), f x ∂μ

Conditional expectation over a 0-1 σ-algebra is the mean: if every m'-measurable set has measure 0 or 1, the conditional expectation of an integrable function is a.e. the integral.