From e56cd33842e613c8db43a058a09355aeb67ed4ca Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 11:57:54 -0500 Subject: [PATCH 01/20] refactor: Extract general lemmas to ForMathlib/ for mathlib contribution MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extract reusable infrastructure from the exchangeability project into ForMathlib/ subdirectories mirroring mathlib's hierarchy: - ForMathlib/Combinatorics/PermutationExtension.lean exists_perm_extending_strictMono for subsequence ↔ permutation - ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean iInf_comap_eq_comap_iInf_of_surjective for tail σ-algebra equality - ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean π-system infrastructure and measure_eq_of_fin_marginals_eq - ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean condExp_L1_lipschitz and related operator properties Update source files to re-export from ForMathlib for backward compat. Add ForMathlib/README.md with PR tracking and sequencing strategy. --- Exchangeability/Contractability.lean | 60 +--- Exchangeability/Tail/TailSigma.lean | 136 +-------- .../Combinatorics/PermutationExtension.lean | 137 +++++++++ .../Constructions/Pi/Cylinders.lean | 288 ++++++++++++++++++ .../ConditionalExpectation/Lipschitz.lean | 137 +++++++++ .../MeasurableSpace/ComapInfima.lean | 156 ++++++++++ ForMathlib/README.md | 76 +++++ 7 files changed, 808 insertions(+), 182 deletions(-) create mode 100644 ForMathlib/Combinatorics/PermutationExtension.lean create mode 100644 ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean create mode 100644 ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean create mode 100644 ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean create mode 100644 ForMathlib/README.md diff --git a/Exchangeability/Contractability.lean b/Exchangeability/Contractability.lean index 32918547..75ff8133 100644 --- a/Exchangeability/Contractability.lean +++ b/Exchangeability/Contractability.lean @@ -7,6 +7,7 @@ import Mathlib.MeasureTheory.Measure.ProbabilityMeasure import Mathlib.MeasureTheory.Measure.Typeclasses.Probability import Exchangeability.Probability.InfiniteProduct import Exchangeability.Util.StrictMono +import ForMathlib.Combinatorics.PermutationExtension /-! # Contractability and Exchangeability @@ -309,65 +310,14 @@ permutation by arbitrarily pairing up the remaining elements. This is the key combinatorial lemma enabling `contractable_of_exchangeable`: any strictly increasing subsequence can be realized via a permutation. + +**Note:** Implementation is in `ForMathlib.Combinatorics.PermutationExtension`. -/ lemma exists_perm_extending_strictMono {m n : ℕ} (k : Fin m → ℕ) (hk_mono : StrictMono k) (hk_bound : ∀ i, k i < n) (hmn : m ≤ n) : ∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin m), - (σ ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩).val = k i := by - classical - -- Embed `Fin m` into `Fin n` via the initial segment. - let ι : Fin m → Fin n := fun i => ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩ - let p : Fin n → Prop := fun x => x.val < m - let q : Fin n → Prop := fun x => ∃ i : Fin m, x = ⟨k i, hk_bound i⟩ - have hι_mem : ∀ i : Fin m, p (ι i) := fun i => i.isLt - let kFin : Fin m → Fin n := fun i => ⟨k i, hk_bound i⟩ - have hk_mem : ∀ i : Fin m, q (kFin i) := fun i => ⟨i, rfl⟩ - haveI : DecidablePred p := fun x => inferInstance - haveI : DecidablePred q := fun x => inferInstance - -- Equivalence between the first `m` coordinates and `Fin m`. - let e_dom : {x : Fin n // p x} ≃ Fin m := - { toFun := fun x => ⟨x.1.val, x.2⟩ - , invFun := fun i => ⟨ι i, by - dsimp [p, ι] - exact i.isLt⟩ - , left_inv := by - rintro ⟨x, hx⟩ - ext; simp [ι] - , right_inv := by - intro i - cases i with - | mk i hi => - simp [ι] } - -- Equivalence between the image of `k` and `Fin m`. - -- For injectivity of k, we use that it's strictly monotone - have hk_inj : Function.Injective kFin := - fun i j hij => hk_mono.injective (Fin.ext_iff.mp hij) - let e_cod : Fin m ≃ {x : Fin n // q x} := - { toFun := fun i => ⟨kFin i, hk_mem i⟩ - , invFun := fun y => Classical.choose y.2 - , left_inv := by - intro i - have h_spec := Classical.choose_spec (hk_mem i) - have : k (Classical.choose (hk_mem i)) = k i := by - simpa [kFin] using (Fin.ext_iff.mp h_spec).symm - exact hk_mono.injective this - , right_inv := by - rintro ⟨y, hy⟩ - apply Subtype.ext - simp only [kFin] - exact (Classical.choose_spec hy).symm } - -- Equivalence between the subtypes describing the first `m` coordinates and the image of `k`. - let e : {x : Fin n // p x} ≃ {x : Fin n // q x} := e_dom.trans e_cod - -- Extend this equivalence to a permutation of `Fin n`. - let σ : Equiv.Perm (Fin n) := Equiv.extendSubtype e - have hσ_apply : ∀ i : Fin m, σ (ι i) = kFin i := by - intro i - have h_apply := Equiv.extendSubtype_apply_of_mem (e:=e) (x:=ι i) (hι_mem i) - dsimp [σ, e, Equiv.trans, e_dom, e_cod, ι, Fin.castLEEmb, kFin] at h_apply - simpa using h_apply - refine ⟨σ, fun i => ?_⟩ - have hσ_val : (σ (ι i)).val = k i := by simpa [kFin] using congrArg Fin.val (hσ_apply i) - simpa [ι] using hσ_val + (σ ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩).val = k i := + Combinatorics.exists_perm_extending_strictMono k hk_mono hk_bound hmn /-- Helper: relabeling coordinates by a finite permutation is measurable as a map from (Fin n → α) to itself (with product σ-algebra). -/ diff --git a/Exchangeability/Tail/TailSigma.lean b/Exchangeability/Tail/TailSigma.lean index c6280cf5..7829f9ee 100644 --- a/Exchangeability/Tail/TailSigma.lean +++ b/Exchangeability/Tail/TailSigma.lean @@ -6,6 +6,7 @@ Authors: Cameron Freer import Mathlib.MeasureTheory.MeasurableSpace.Pi import Mathlib.MeasureTheory.Measure.MeasureSpace +import ForMathlib.MeasureTheory.MeasurableSpace.ComapInfima /-! # Tail σ-algebras on path space and for general processes @@ -91,133 +92,14 @@ def tailShift (α : Type*) [MeasurableSpace α] : MeasurableSpace (ℕ → α) : (fun (ω : ℕ → α) => fun k => ω (n + k)) (inferInstance : MeasurableSpace (ℕ → α))) -/-! ### Helper Lemmas for comap and Infima -/ - -namespace MeasurableSpace - -/-- Preimage is injective on sets when `f` is surjective. -/ -lemma preimage_injective_of_surjective {α β} {f : α → β} - (hf : Function.Surjective f) : - Function.Injective (fun (s : Set β) => f ⁻¹' s) := by - intro s t hpre - have : f ⁻¹' s = f ⁻¹' t := hpre - ext y - rcases hf y with ⟨x, rfl⟩ - -- compare membership in equal preimages - have := congrArg (fun A => x ∈ A) this - simpa using this - -/-- If `f` is surjective, then `map f (comap f m) = m`. -/ -lemma map_comap_eq_of_surjective {α β} {f : α → β} - (hf : Function.Surjective f) (m : MeasurableSpace β) : - MeasurableSpace.map f (MeasurableSpace.comap f m) = m := by - classical - -- Prove by extensionality on measurable sets. - ext S; constructor - · -- `S ∈ map f (comap f m)` iff `f ⁻¹' S ∈ comap f m` - intro hS - change MeasurableSet[MeasurableSpace.comap f m] (f ⁻¹' S) at hS - rcases hS with ⟨T, hT, hpre⟩ - -- injectivity of preimage under surjectivity identifies `S = T` - have hinj := preimage_injective_of_surjective (α := α) (β := β) hf - have : S = T := by - apply hinj - exact hpre.symm - simpa [this] - · -- unit inequality `m ≤ map f (comap f m)` - intro hS - change MeasurableSet[MeasurableSpace.comap f m] (f ⁻¹' S) - exact ⟨S, hS, rfl⟩ - -end MeasurableSpace - -omit [MeasurableSpace Ω] [MeasurableSpace α] in -/-- `comap` distributes over `iInf` unconditionally (≤ direction only). - - The inequality `comap f (⨅ i, m i) ≤ ⨅ i, comap f (m i)` holds by monotonicity. - The reverse inequality (and hence equality) requires `f` to be surjective. - See `iInf_comap_eq_comap_iInf_of_surjective` for the surjective case. -/ -lemma comap_iInf_le {ι : Sort*} (f : α → β) (m : ι → MeasurableSpace β) : - MeasurableSpace.comap f (iInf m) ≤ iInf (fun i => MeasurableSpace.comap f (m i)) := by - refine le_iInf (fun i => ?_) - exact MeasurableSpace.comap_mono (iInf_le m i) - --- Extract witnesses for each comap and choose them uniformly -private lemma comap_iInf_witnesses {ι : Type*} {α β : Type*} {f : α → β} - (m : ι → MeasurableSpace β) (s : Set α) - (hs_all : ∀ i, MeasurableSet[MeasurableSpace.comap f (m i)] s) : - ∃ (T : ι → Set β), (∀ i, MeasurableSet[m i] (T i)) ∧ (∀ i, s = f ⁻¹' (T i)) := by - have : ∀ i, ∃ (T : Set β), MeasurableSet[m i] T ∧ s = f ⁻¹' T := by - intro i - have hi := hs_all i - rw [MeasurableSpace.measurableSet_comap] at hi - rcases hi with ⟨T, hT, hpre⟩ - exact ⟨T, hT, hpre.symm⟩ - choose T hTmeas hspre using this - exact ⟨T, hTmeas, hspre⟩ - --- All witnesses are equal when f is surjective -private lemma comap_witnesses_eq_of_surjective {ι : Type*} {α β : Type*} {f : α → β} - (hf : Function.Surjective f) (T : ι → Set β) (s : Set α) - (hspre : ∀ i, s = f ⁻¹' (T i)) : - ∀ i j, T i = T j := by - intro i j - have hinj := MeasurableSpace.preimage_injective_of_surjective (α := α) (β := β) hf - have : f ⁻¹' T i = f ⁻¹' T j := by rw [← hspre i, ← hspre j] - exact hinj this - --- A set is measurable in comap f (iInf m) if it's the preimage of a canonically measurable set -private lemma measurableSet_comap_iInf_of_canonical {ι : Type*} [Nonempty ι] - {α β : Type*} {f : α → β} (m : ι → MeasurableSpace β) - (T0 : Set β) (hT0 : ∀ i, MeasurableSet[m i] T0) (s : Set α) (hs : s = f ⁻¹' T0) : - MeasurableSet[MeasurableSpace.comap f (iInf m)] s := by - refine ⟨T0, ?_, hs.symm⟩ - rw [MeasurableSpace.measurableSet_iInf] - exact hT0 - -omit [MeasurableSpace Ω] [MeasurableSpace α] in -/-- With `f` surjective and a nonempty index type, `comap` commutes with `⨅`. -/ -lemma iInf_comap_eq_comap_iInf_of_surjective - {ι : Type*} [Nonempty ι] {α β : Type*} {f : α → β} - (hf : Function.Surjective f) - (m : ι → MeasurableSpace β) : - iInf (fun i => MeasurableSpace.comap f (m i)) - = MeasurableSpace.comap f (iInf m) := by - classical - -- (≥) direction holds unconditionally (monotonicity) - have hge : - MeasurableSpace.comap f (iInf m) - ≤ iInf (fun i => MeasurableSpace.comap f (m i)) := by - refine le_iInf (fun i => ?_) - exact MeasurableSpace.comap_mono (iInf_le _ i) - - -- (≤) direction uses surjectivity to unify witnesses - have hle : - iInf (fun i => MeasurableSpace.comap f (m i)) - ≤ MeasurableSpace.comap f (iInf m) := by - intro s hs - -- For each i, s is measurable in comap f (m i) - have hs_all : ∀ i, MeasurableSet[MeasurableSpace.comap f (m i)] s := by - rw [MeasurableSpace.measurableSet_iInf] at hs - exact hs - - -- Extract witnesses Tᵢ such that s = f ⁻¹' Tᵢ for each i - obtain ⟨T, hTmeas, hspre⟩ := comap_iInf_witnesses m s hs_all - - -- All witnesses are equal by surjectivity - have Tall := comap_witnesses_eq_of_surjective hf T s hspre - - -- Pick canonical witness T₀ - rcases ‹Nonempty ι› with ⟨i₀⟩ - let T0 : Set β := T i₀ - have T_all : ∀ i, T i = T0 := fun i => Tall i i₀ - have s_pre : s = f ⁻¹' T0 := by simpa [T_all i₀] using hspre i₀ - have T0_meas_all : ∀ i, MeasurableSet[m i] T0 := fun i => by simpa [T_all i] using hTmeas i - - -- Conclude measurability - exact measurableSet_comap_iInf_of_canonical m T0 T0_meas_all s s_pre - - exact le_antisymm hle hge +/-! ### Helper Lemmas for comap and Infima + +These lemmas are now in `ForMathlib.MeasureTheory.MeasurableSpace.ComapInfima`. +We re-export them here for backward compatibility. -/ + +-- Re-export comap/infima lemmas from ForMathlib +export MeasurableSpace (preimage_injective_of_surjective map_comap_eq_of_surjective + comap_iInf_le iInf_comap_eq_comap_iInf_of_surjective) /-! ### Bridge Lemmas (LOAD-BEARING - Phase 1a) -/ diff --git a/ForMathlib/Combinatorics/PermutationExtension.lean b/ForMathlib/Combinatorics/PermutationExtension.lean new file mode 100644 index 00000000..acfdcf1f --- /dev/null +++ b/ForMathlib/Combinatorics/PermutationExtension.lean @@ -0,0 +1,137 @@ +/- +Copyright (c) 2025 Cameron Freer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Cameron Freer +-/ +import Mathlib.Logic.Equiv.Fintype +import Mathlib.GroupTheory.Perm.Basic + +/-! +# Permutation Extension for Strictly Monotone Functions + +This file proves that any strictly increasing function `k : Fin m → ℕ` with bounded range +can be extended to a permutation of `Fin n`. + +## Main Results + +* `exists_perm_extending_strictMono`: Given a strictly increasing `k : Fin m → ℕ` with all + values `< n` and `m ≤ n`, there exists a permutation `σ : Perm (Fin n)` such that + `σ(i) = k(i)` for all `i < m`. + +## Mathematical Context + +This is a key combinatorial lemma in the proof that **exchangeability implies contractability** +for infinite sequences of random variables. The construction allows any strictly increasing +subsequence to be realized as the image of the first m coordinates under some permutation. + +**Intuition:** We partition both domain and codomain: +- Domain: `{0,...,m-1}` ∪ `{m,...,n-1}` = `Fin n` +- Codomain: `{k(0),...,k(m-1)}` ∪ complement = `Fin n` + +Map first `m` positions to `k`-values, then extend arbitrarily to remaining positions +using `Equiv.extendSubtype`. + +## Suggested Mathlib Location + +`Mathlib.GroupTheory.Perm.Fintype` or `Mathlib.Combinatorics.Subseq` + +## References + +* Kallenberg (2005), *Probabilistic Symmetries and Invariance Principles*, Theorem 1.1 +-/ + +namespace Combinatorics + +variable {m n : ℕ} + +/-- For strictly monotone `k : Fin m → ℕ`, values dominate indices: `i ≤ k(i)` for all `i`. -/ +lemma strictMono_Fin_ge_id {k : Fin m → ℕ} (hk : StrictMono k) (i : Fin m) : + i.val ≤ k i := by + -- Proof by strong induction on i.val + have : ∀ n (hn : n < m), n ≤ k ⟨n, hn⟩ := by + intro n + induction n with + | zero => intro _; exact Nat.zero_le _ + | succ n ih => + intro hn + have hn' : n < m := Nat.lt_of_succ_lt hn + let j : Fin m := ⟨n, hn'⟩ + let j_succ : Fin m := ⟨n.succ, hn⟩ + have hlt : j < j_succ := by simp [Fin.lt_def, j, j_succ] + have hk_lt : k j < k j_succ := hk hlt + have ih' : n ≤ k j := ih hn' + calc n.succ + = n + 1 := rfl + _ ≤ k j + 1 := Nat.add_le_add_right ih' 1 + _ ≤ k j_succ := Nat.succ_le_of_lt hk_lt + exact this i.val i.isLt + +/-- +Any strictly increasing function can be extended to a permutation. + +**Statement:** Given a strictly increasing `k : Fin m → ℕ` with all values `< n` +and `m ≤ n`, there exists a permutation `σ : Perm (Fin n)` such that +`σ(i) = k(i)` for all `i < m`. + +**Construction outline:** +1. **Domain partition:** `{0,...,m-1}` ∪ `{m,...,n-1}` = `Fin n` +2. **Codomain partition:** `{k(0),...,k(m-1)}` ∪ `complement` = `Fin n` +3. Map first `m` positions to `k`-values: `σ(i) = k(i)` for `i < m` +4. Extend arbitrarily to remaining positions using `Equiv.extendSubtype` + +This is the key combinatorial lemma enabling the implication +**exchangeable → contractable**: any strictly increasing subsequence can be +realized via a permutation. +-/ +theorem exists_perm_extending_strictMono (k : Fin m → ℕ) + (hk_mono : StrictMono k) (hk_bound : ∀ i, k i < n) (hmn : m ≤ n) : + ∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin m), + (σ ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩).val = k i := by + classical + -- Embed `Fin m` into `Fin n` via the initial segment. + let ι : Fin m → Fin n := fun i => ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩ + let p : Fin n → Prop := fun x => x.val < m + let q : Fin n → Prop := fun x => ∃ i : Fin m, x = ⟨k i, hk_bound i⟩ + have hι_mem : ∀ i : Fin m, p (ι i) := fun i => i.isLt + let kFin : Fin m → Fin n := fun i => ⟨k i, hk_bound i⟩ + have hk_mem : ∀ i : Fin m, q (kFin i) := fun i => ⟨i, rfl⟩ + haveI : DecidablePred p := fun _ => inferInstance + haveI : DecidablePred q := fun _ => inferInstance + -- Equivalence between the first `m` coordinates and `Fin m`. + let e_dom : {x : Fin n // p x} ≃ Fin m := + { toFun := fun x => ⟨x.1.val, x.2⟩ + , invFun := fun i => ⟨ι i, by dsimp [p, ι]; exact i.isLt⟩ + , left_inv := by rintro ⟨x, hx⟩; ext; simp [ι] + , right_inv := by intro i; cases i with | mk i hi => simp [ι] } + -- Equivalence between the image of `k` and `Fin m`. + -- For injectivity of k, we use that it's strictly monotone + have hk_inj : Function.Injective kFin := + fun i j hij => hk_mono.injective (Fin.ext_iff.mp hij) + let e_cod : Fin m ≃ {x : Fin n // q x} := + { toFun := fun i => ⟨kFin i, hk_mem i⟩ + , invFun := fun y => Classical.choose y.2 + , left_inv := by + intro i + have h_spec := Classical.choose_spec (hk_mem i) + have : k (Classical.choose (hk_mem i)) = k i := by + simpa [kFin] using (Fin.ext_iff.mp h_spec).symm + exact hk_mono.injective this + , right_inv := by + rintro ⟨y, hy⟩ + apply Subtype.ext + simp only [kFin] + exact (Classical.choose_spec hy).symm } + -- Equivalence between the subtypes describing the first `m` coordinates and the image of `k`. + let e : {x : Fin n // p x} ≃ {x : Fin n // q x} := e_dom.trans e_cod + -- Extend this equivalence to a permutation of `Fin n`. + let σ : Equiv.Perm (Fin n) := Equiv.extendSubtype e + have hσ_apply : ∀ i : Fin m, σ (ι i) = kFin i := by + intro i + have h_apply := Equiv.extendSubtype_apply_of_mem (e := e) (x := ι i) (hι_mem i) + dsimp [σ, e, Equiv.trans, e_dom, e_cod, ι, Fin.castLEEmb, kFin] at h_apply + simpa using h_apply + refine ⟨σ, fun i => ?_⟩ + have hσ_val : (σ (ι i)).val = k i := by simpa [kFin] using congrArg Fin.val (hσ_apply i) + simpa [ι] using hσ_val + +end Combinatorics diff --git a/ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean b/ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean new file mode 100644 index 00000000..c0565f42 --- /dev/null +++ b/ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean @@ -0,0 +1,288 @@ +/- +Copyright (c) 2025 Cameron Freer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Cameron Freer +-/ +import Mathlib.Data.Fin.Tuple.Basic +import Mathlib.Logic.Equiv.Fintype +import Mathlib.MeasureTheory.Constructions.Cylinders +import Mathlib.MeasureTheory.Measure.ProbabilityMeasure +import Mathlib.MeasureTheory.Measure.Typeclasses.Finite +import Mathlib.Tactic.Measurability + +/-! +# Prefix Cylinders and Finite Marginal Uniqueness + +This file provides infrastructure for working with "prefix cylinders" - cylinder sets +determined by initial segments of ℕ - and proves that finite measures on `ℕ → α` are +determined by their finite-dimensional marginals. + +## Main Definitions + +* `prefixProj α n`: Projection from `ℕ → α` to `Fin n → α` (first n coordinates) +* `prefixCylinder S`: Cylinder set determined by first n coordinates lying in S +* `prefixCylinders α`: Collection of all prefix cylinders (forms a π-system) + +## Main Results + +* `isPiSystem_prefixCylinders`: Prefix cylinders form a π-system +* `generateFrom_prefixCylinders`: Prefix cylinders generate the product σ-algebra +* `measure_eq_of_fin_marginals_eq`: Finite measures agreeing on all finite marginals are equal + +## Mathematical Context + +The key result `measure_eq_of_fin_marginals_eq` is a Kolmogorov extension-type theorem: +if two finite measures on `ℕ → α` induce the same distribution on each finite projection +`Fin n → α`, then they are equal. This is proved via the π-system uniqueness theorem. + +This infrastructure is used in proving de Finetti's theorem to show that exchangeability +(invariance under finite permutations) implies full exchangeability (invariance under +all permutations of ℕ). + +## Suggested Mathlib Location + +`Mathlib.MeasureTheory.Constructions.Pi.Cylinders` or `Mathlib.MeasureTheory.Measure.FinMarginals` + +## References + +* Kallenberg (2005), *Probabilistic Symmetries and Invariance Principles*, Section 1.1 +-/ + +open scoped BigOperators +open Equiv MeasureTheory Set + +namespace PrefixCylinders + +variable {α : Type*} [MeasurableSpace α] + +/-! ### Prefix Projection -/ + +/-- Projection to the first `n` coordinates. -/ +def prefixProj (α : Type*) (n : ℕ) (x : ℕ → α) : Fin n → α := + fun i => x i + +omit [MeasurableSpace α] in +@[simp] +lemma prefixProj_apply {n : ℕ} (x : ℕ → α) (i : Fin n) : + prefixProj (α := α) n x i = x i := rfl + +lemma measurable_prefixProj {n : ℕ} : + Measurable (prefixProj (α := α) n) := + measurable_pi_lambda _ (fun i => measurable_pi_apply (↑i : ℕ)) + +/-! ### Prefix Cylinders -/ + +/-- Cylinder set determined by the first `n` coordinates. -/ +def prefixCylinder {n : ℕ} (S : Set (Fin n → α)) : Set (ℕ → α) := + (prefixProj (α := α) n) ⁻¹' S + +omit [MeasurableSpace α] in +@[simp] +lemma mem_prefixCylinder {n : ℕ} {S : Set (Fin n → α)} {x : ℕ → α} : + x ∈ prefixCylinder (α := α) S ↔ prefixProj (α := α) n x ∈ S := Iff.rfl + +omit [MeasurableSpace α] in +@[simp] +lemma prefixCylinder_univ {n : ℕ} : + prefixCylinder (α := α) (Set.univ : Set (Fin n → α)) = Set.univ := by + simp [prefixCylinder] + +omit [MeasurableSpace α] in +@[simp] +lemma prefixCylinder_empty {n : ℕ} : + prefixCylinder (α := α) (∅ : Set (Fin n → α)) = ∅ := rfl + +/-- The collection of all prefix cylinders. -/ +def prefixCylinders (α : Type*) [MeasurableSpace α] : Set (Set (ℕ → α)) := + {A | ∃ n, ∃ S : Set (Fin n → α), MeasurableSet S ∧ A = prefixCylinder (α := α) S} + +lemma prefixCylinder_mem_prefixCylinders {n : ℕ} {S : Set (Fin n → α)} + (hS : MeasurableSet S) : + prefixCylinder (α := α) S ∈ prefixCylinders α := + ⟨n, S, hS, rfl⟩ + +lemma measurable_of_mem_prefixCylinders {A : Set (ℕ → α)} + (hA : A ∈ prefixCylinders α) : MeasurableSet A := by + classical + rcases hA with ⟨n, S, hS, rfl⟩ + exact (measurable_prefixProj (α := α) (n := n)) hS + +/-! ### Restriction and Extension -/ + +section Extend + +variable {m n : ℕ} + +/-- Restrict a finite tuple to its first `m` coordinates. -/ +def takePrefix (hmn : m ≤ n) (x : Fin n → α) : Fin m → α := + fun i => x (Fin.castLE hmn i) + +omit [MeasurableSpace α] in +@[simp] +lemma takePrefix_apply {hmn : m ≤ n} (x : Fin n → α) (i : Fin m) : + takePrefix (α := α) hmn x i = x (Fin.castLE hmn i) := rfl + +omit [MeasurableSpace α] in +@[simp] +lemma takePrefix_prefixProj {hmn : m ≤ n} (x : ℕ → α) : + takePrefix (α := α) hmn (prefixProj (α := α) n x) = prefixProj (α := α) m x := by + ext i; simp [takePrefix] + +/-- Extend a set from `Fin m → α` to `Fin n → α` by ignoring extra coordinates. -/ +def extendSet (hmn : m ≤ n) (S : Set (Fin m → α)) : Set (Fin n → α) := + {x | takePrefix (α := α) hmn x ∈ S} + +omit [MeasurableSpace α] in +lemma prefixCylinder_inter {m n : ℕ} {S : Set (Fin m → α)} {T : Set (Fin n → α)} : + prefixCylinder (α := α) S ∩ prefixCylinder (α := α) T = + prefixCylinder (α := α) + (extendSet (α := α) (Nat.le_max_left _ _) S ∩ + extendSet (α := α) (Nat.le_max_right _ _) T) := by + ext x + simp only [Set.mem_inter_iff, mem_prefixCylinder, extendSet, Set.mem_setOf_eq, + takePrefix_prefixProj] + +-- Disable false-positive linter warnings: Measurable (Fin n → α) depends on [MeasurableSpace α] +set_option linter.unusedSectionVars false + +@[nolint unusedArguments] +lemma takePrefix_measurable (hmn : m ≤ n) : + Measurable (takePrefix (α := α) hmn) := + measurable_pi_lambda _ (fun i => measurable_pi_apply (Fin.castLE hmn i)) + +@[nolint unusedArguments] +lemma extendSet_measurable {S : Set (Fin m → α)} {hmn : m ≤ n} + (hS : MeasurableSet S) : MeasurableSet (extendSet (α := α) hmn S) := + (takePrefix_measurable (α := α) hmn) hS + +end Extend + +/-! ### π-System Property -/ + +set_option linter.unusedSectionVars false + +/-- The prefix cylinders form a π-system. -/ +@[nolint unusedArguments] +lemma isPiSystem_prefixCylinders : + IsPiSystem (prefixCylinders α) := by + classical + rintro A ⟨m, S, hS, rfl⟩ B ⟨n, T, hT, rfl⟩ hAB + use max m n + use extendSet (α := α) (Nat.le_max_left m n) S ∩ + extendSet (α := α) (Nat.le_max_right m n) T + constructor + · exact MeasurableSet.inter + (extendSet_measurable (α := α) (hmn := Nat.le_max_left m n) hS) + (extendSet_measurable (α := α) (hmn := Nat.le_max_right m n) hT) + · exact prefixCylinder_inter (α := α) + +/-- Any cylinder set belongs to the σ-algebra generated by prefix cylinders. -/ +@[nolint unusedArguments] +lemma cylinder_subset_prefixCylinders {s : Finset ℕ} {S : Set (∀ _ : s, α)} + (hS : MeasurableSet S) : + MeasureTheory.cylinder (α := fun _ : ℕ => α) s S ∈ prefixCylinders α := by + classical + let N := s.sup id + 1 + have h_mem : ∀ i ∈ s, i < N := by + intro i hi + have hle : i ≤ s.sup id := by convert Finset.le_sup (f := id) hi + omega + let ι : s → Fin N := fun x => ⟨x.1, h_mem x.1 x.2⟩ + let pull : (Fin N → α) → (∀ i : s, α) := fun x => fun y => x (ι y) + have hpull_meas : Measurable pull := by measurability + have hs_eq : + MeasureTheory.cylinder (α := fun _ : ℕ => α) s S = + prefixCylinder (α := α) (pull ⁻¹' S) := by + ext x + classical + have hpull : pull (prefixProj (α := α) N x) = s.restrict x := by + funext y + rcases y with ⟨y, hy⟩ + simp only [pull, prefixProj, Finset.restrict] + rfl + simp [MeasureTheory.cylinder, prefixCylinder, hpull] + refine hs_eq ▸ prefixCylinder_mem_prefixCylinders (α := α) ?_ + exact hpull_meas hS + +/-- The σ-algebra generated by prefix cylinders is the product σ-algebra. -/ +@[nolint unusedArguments] +lemma generateFrom_prefixCylinders : + MeasurableSpace.generateFrom (prefixCylinders α) = + (inferInstance : MeasurableSpace (ℕ → α)) := by + classical + refine le_antisymm ?_ ?_ + · refine MeasurableSpace.generateFrom_le ?_ + rintro A hA + exact measurable_of_mem_prefixCylinders (α := α) hA + · have h_subset : + MeasurableSpace.generateFrom (MeasureTheory.measurableCylinders fun _ : ℕ => α) + ≤ MeasurableSpace.generateFrom (prefixCylinders α) := by + refine MeasurableSpace.generateFrom_mono ?_ + intro A hA + obtain ⟨s, S, hS, rfl⟩ := + (MeasureTheory.mem_measurableCylinders (α := fun _ : ℕ => α) A).1 hA + exact cylinder_subset_prefixCylinders (α := α) hS + simpa [MeasureTheory.generateFrom_measurableCylinders (α := fun _ : ℕ => α)] using h_subset + +/-! ### Finite Marginal Uniqueness -/ + +private lemma totalMass_eq_of_fin_marginals_eq {μ ν : Measure (ℕ → α)} + [IsFiniteMeasure μ] [IsFiniteMeasure ν] + (h : ∀ n (S : Set (Fin n → α)) (_hS : MeasurableSet S), + Measure.map (prefixProj (α := α) n) μ S = + Measure.map (prefixProj (α := α) n) ν S) : + μ Set.univ = ν Set.univ := by + classical + simpa [Measure.map_apply_of_aemeasurable + ((measurable_prefixProj (α := α) (n := 1)).aemeasurable)] + using h 1 Set.univ MeasurableSet.univ + +private lemma prefixCylinders_eq_of_fin_marginals_eq {μ ν : Measure (ℕ → α)} + (h : ∀ n (S : Set (Fin n → α)) (_hS : MeasurableSet S), + Measure.map (prefixProj (α := α) n) μ S = + Measure.map (prefixProj (α := α) n) ν S) + (A : Set (ℕ → α)) (hA : A ∈ prefixCylinders α) : + μ A = ν A := by + classical + obtain ⟨n, S, hS, rfl⟩ := hA + simp only [prefixCylinder, ← Measure.map_apply_of_aemeasurable + ((measurable_prefixProj (α := α) (n := n)).aemeasurable) hS] + exact h n S hS + +/-- +**Kolmogorov Extension-Type Uniqueness:** Finite measures with matching finite-dimensional +marginals are equal. + +If two finite measures on `ℕ → α` induce the same distribution on each +finite-dimensional projection `Fin n → α`, then they are equal. This is a +consequence of the π-system uniqueness theorem applied to prefix cylinders. + +**Proof structure:** +1. Measures agree on total mass (via 1-dimensional marginal) +2. Measures agree on all prefix cylinders (direct from marginals) +3. Apply π-system uniqueness to extend agreement to all measurable sets +-/ +@[nolint unusedArguments] +theorem measure_eq_of_fin_marginals_eq {μ ν : Measure (ℕ → α)} + [IsFiniteMeasure μ] [IsFiniteMeasure ν] + (h : ∀ n (S : Set (Fin n → α)) (_hS : MeasurableSet S), + Measure.map (prefixProj (α := α) n) μ S = + Measure.map (prefixProj (α := α) n) ν S) : μ = ν := by + classical + apply MeasureTheory.ext_of_generate_finite (C := prefixCylinders α) + · simp [generateFrom_prefixCylinders (α := α)] + · exact isPiSystem_prefixCylinders (α := α) + · exact prefixCylinders_eq_of_fin_marginals_eq (α := α) h + · exact totalMass_eq_of_fin_marginals_eq (α := α) h + +/-- Convenience wrapper for probability measures. -/ +@[nolint unusedArguments] +theorem measure_eq_of_fin_marginals_eq_prob {μ ν : Measure (ℕ → α)} + [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] + (h : ∀ n (S : Set (Fin n → α)) (_hS : MeasurableSet S), + Measure.map (prefixProj (α := α) n) μ S = + Measure.map (prefixProj (α := α) n) ν S) : μ = ν := by + classical + exact measure_eq_of_fin_marginals_eq (α := α) (μ := μ) (ν := ν) h + +end PrefixCylinders diff --git a/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean b/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean new file mode 100644 index 00000000..1d5da566 --- /dev/null +++ b/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean @@ -0,0 +1,137 @@ +/- +Copyright (c) 2025 Cameron Freer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Cameron Freer +-/ +import Mathlib.MeasureTheory.Function.ConditionalExpectation.Real +import Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut +import ForMathlib.MeasureTheory.Measure.TrimInstances + +/-! +# Lipschitz Properties of Conditional Expectation + +This file provides operator-theoretic properties of conditional expectation, +particularly its L¹ nonexpansivity. + +## Main Results + +* `condExp_L1_lipschitz`: Conditional expectation is L¹-nonexpansive: + `‖E[f|m] - E[g|m]‖₁ ≤ ‖f - g‖₁` + +* `condExp_abs_le_of_abs_le`: Conditional expectation preserves monotonicity + in absolute value + +* `integrable_of_bounded`: Bounded measurable functions are integrable on + finite measures (utility lemma) + +## Mathematical Context + +These operator-theoretic properties are fundamental in: +1. Proving convergence of martingale sequences +2. Showing conditional expectation defines a projection operator on L¹ +3. Applying fixed-point arguments in probability theory + +The L¹ nonexpansivity follows from the key inequality `∫|E[f|m]| ≤ ∫|f|` +(mathlib's `integral_abs_condExp_le`), combined with linearity. + +## Suggested Mathlib Location + +`Mathlib.MeasureTheory.Function.ConditionalExpectation.Lipschitz` + +## References + +* Kallenberg (2005), *Probabilistic Symmetries and Invariance Principles* +* Williams (1991), *Probability with Martingales*, Chapter 9 +-/ + +open MeasureTheory Filter Set Function + +namespace CondExp + +variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} + +/-- Bounded measurable functions are integrable on finite measures. -/ +lemma integrable_of_bounded [IsFiniteMeasure μ] + {f : Ω → ℝ} (hf : Measurable f) (hbd : ∃ C, ∀ ω, |f ω| ≤ C) : + Integrable f μ := by + obtain ⟨C, hC⟩ := hbd + exact ⟨hf.aestronglyMeasurable, HasFiniteIntegral.of_bounded (ae_of_all μ hC)⟩ + +/-- Product of integrable and bounded measurable functions is integrable. -/ +lemma integrable_of_bounded_mul [IsFiniteMeasure μ] + {f g : Ω → ℝ} (hf : Integrable f μ) (hg : Measurable g) + (hbd : ∃ C, ∀ ω, |g ω| ≤ C) : + Integrable (f * g) μ := by + have : f * g = fun ω => g ω * f ω := funext fun _ => mul_comm _ _ + rw [this] + obtain ⟨C, hC⟩ := hbd + have hbd_ae : ∀ᵐ ω ∂μ, ‖g ω‖ ≤ C := by + filter_upwards with ω + exact (Real.norm_eq_abs _).symm ▸ hC ω + exact Integrable.bdd_mul hf hg.aestronglyMeasurable hbd_ae + +/-- Conditional expectation preserves monotonicity in absolute value. + +If |f| ≤ |g| everywhere, then |E[f|m]| ≤ E[|g||m]. -/ +lemma condExp_abs_le_of_abs_le [IsFiniteMeasure μ] + {m : MeasurableSpace Ω} (_hm : m ≤ ‹_›) + {f g : Ω → ℝ} (hf : Integrable f μ) (hg : Integrable g μ) + (h : ∀ ω, |f ω| ≤ |g ω|) : + ∀ᵐ ω ∂μ, |μ[f|m] ω| ≤ μ[(fun ω' => |g ω'|)|m] ω := by + have h_lower : ∀ ω, -(|g ω|) ≤ f ω := fun ω => + (neg_le_neg (h ω)).trans (neg_abs_le (f ω)) + have h_upper : ∀ ω, f ω ≤ |g ω| := fun ω => (le_abs_self (f ω)).trans (h ω) + have hg_abs : Integrable (fun ω => |g ω|) μ := hg.abs + have lower_bd := condExp_mono (m := m) hg_abs.neg hf (ae_of_all μ h_lower) + have upper_bd := condExp_mono (m := m) hf hg_abs (ae_of_all μ h_upper) + have hneg_eq : μ[(fun ω => -(|g ω|))|m] =ᵐ[μ] fun ω => -(μ[(fun ω' => |g ω'|)|m] ω) := + condExp_neg (fun ω => |g ω|) m + filter_upwards [lower_bd, upper_bd, hneg_eq] with ω hlower hupper hneg + have hlower' : -(μ[(fun ω' => |g ω'|)|m] ω) ≤ μ[f|m] ω := hneg ▸ hlower + exact abs_le.mpr ⟨hlower', hupper⟩ + +/-- **Conditional expectation is L¹-nonexpansive.** + +For integrable functions f, g, the conditional expectation is contractive in L¹: +``` +‖E[f|m] - E[g|m]‖₁ ≤ ‖f - g‖₁ +``` + +This follows from `integral_abs_condExp_le` applied to `f - g`. -/ +theorem condExp_L1_lipschitz [IsFiniteMeasure μ] + {m : MeasurableSpace Ω} (_hm : m ≤ ‹_›) + {f g : Ω → ℝ} (hf : Integrable f μ) (hg : Integrable g μ) : + ∫ ω, |μ[f|m] ω - μ[g|m] ω| ∂μ ≤ ∫ ω, |f ω - g ω| ∂μ := by + have h_linear : ∀ᵐ ω ∂μ, μ[f|m] ω - μ[g|m] ω = μ[(f - g)|m] ω := + EventuallyEq.symm (condExp_sub hf hg m) + calc ∫ ω, |μ[f|m] ω - μ[g|m] ω| ∂μ + = ∫ ω, |μ[(f - g)|m] ω| ∂μ := by + apply integral_congr_ae + filter_upwards [h_linear] with ω h + rw [h] + _ ≤ ∫ ω, |(f - g) ω| ∂μ := integral_abs_condExp_le (f - g) + _ = ∫ ω, |f ω - g ω| ∂μ := rfl + +/-- Conditional expectation pull-out property for bounded measurable functions. + +If g is m-measurable and bounded, then E[f·g|m] = E[f|m]·g a.e. -/ +theorem condExp_mul_pullout {Ω : Type*} {m₀ : MeasurableSpace Ω} {μ : Measure Ω} + [IsFiniteMeasure μ] + {m : MeasurableSpace Ω} (hm : m ≤ m₀) + {f g : Ω → ℝ} (hf : Integrable f μ) + (hg_meas : @Measurable Ω ℝ m _ g) + (hg_bd : ∃ C, ∀ ω, |g ω| ≤ C) : + μ[f * g|m] =ᵐ[μ] fun ω => μ[f|m] ω * g ω := by + have hg_strong : StronglyMeasurable[m] g := hg_meas.stronglyMeasurable + obtain ⟨C, hC⟩ := hg_bd + have hg_bound : ∀ᵐ ω ∂μ, ‖g ω‖ ≤ C := ae_of_all μ fun ω => (Real.norm_eq_abs _).le.trans (hC ω) + haveI : SigmaFinite (μ.trim hm) := MeasureTheory.Measure.sigmaFinite_trim μ hm + have h := condExp_stronglyMeasurable_mul_of_bound hm hg_strong hf C hg_bound + -- f * g = g * f pointwise, so μ[f * g|m] =ᵃᵉ μ[g * f|m] = g · μ[f|m] + have hcomm : f * g =ᵐ[μ] g * f := by filter_upwards with ω; simp only [Pi.mul_apply]; ring + have step1 : μ[f * g|m] =ᵐ[μ] μ[g * f|m] := condExp_congr_ae hcomm + have step2 : (fun ω => g ω * μ[f|m] ω) =ᵐ[μ] (fun ω => μ[f|m] ω * g ω) := by + filter_upwards with ω; ring + exact step1.trans (h.trans step2) + +end CondExp diff --git a/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean b/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean new file mode 100644 index 00000000..f69cdcb3 --- /dev/null +++ b/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean @@ -0,0 +1,156 @@ +/- +Copyright (c) 2025 Cameron Freer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Cameron Freer +-/ +import Mathlib.MeasureTheory.MeasurableSpace.Basic + +open MeasureTheory + +/-! +# Comap and Infima of Measurable Spaces + +This file provides lemmas about how `MeasurableSpace.comap` interacts with infima (`⨅`). + +## Main Results + +* `iInf_comap_eq_comap_iInf_of_surjective`: With a surjective function `f` and nonempty index type, + `comap` commutes with `⨅`: + ``` + ⨅ i, MeasurableSpace.comap f (m i) = MeasurableSpace.comap f (⨅ i, m i) + ``` + +## Supporting Lemmas + +* `preimage_injective_of_surjective`: Preimage is injective on sets when `f` is surjective +* `map_comap_eq_of_surjective`: If `f` is surjective, then `map f (comap f m) = m` +* `comap_iInf_le`: The inequality `comap f (⨅ i, m i) ≤ ⨅ i, comap f (m i)` holds unconditionally + +## Mathematical Context + +The main result is crucial for proving that tail σ-algebras on path space can be characterized +either as pullbacks of the path-space tail, or as infima of coordinate-wise σ-algebras. + +## Suggested Mathlib Location + +`Mathlib.MeasureTheory.MeasurableSpace.Basic` (near existing comap/map API) + +## References + +* Kallenberg (2005), *Probabilistic Symmetries and Invariance Principles* +-/ + +namespace MeasurableSpace + +/-- Preimage is injective on sets when `f` is surjective. -/ +lemma preimage_injective_of_surjective {α β : Type*} {f : α → β} + (hf : Function.Surjective f) : + Function.Injective (fun (s : Set β) => f ⁻¹' s) := by + intro s t hpre + have : f ⁻¹' s = f ⁻¹' t := hpre + ext y + rcases hf y with ⟨x, rfl⟩ + have := congrArg (fun A => x ∈ A) this + simpa using this + +/-- If `f` is surjective, then `map f (comap f m) = m`. -/ +lemma map_comap_eq_of_surjective {α β : Type*} {f : α → β} + (hf : Function.Surjective f) (m : MeasurableSpace β) : + MeasurableSpace.map f (MeasurableSpace.comap f m) = m := by + classical + ext S; constructor + · intro hS + change MeasurableSet[MeasurableSpace.comap f m] (f ⁻¹' S) at hS + rcases hS with ⟨T, hT, hpre⟩ + have hinj := preimage_injective_of_surjective (α := α) (β := β) hf + have : S = T := by apply hinj; exact hpre.symm + simpa [this] + · intro hS + change MeasurableSet[MeasurableSpace.comap f m] (f ⁻¹' S) + exact ⟨S, hS, rfl⟩ + +/-- `comap` distributes over `iInf` unconditionally (≤ direction only). + +The inequality `comap f (⨅ i, m i) ≤ ⨅ i, comap f (m i)` holds by monotonicity. +The reverse inequality (and hence equality) requires `f` to be surjective. +See `iInf_comap_eq_comap_iInf_of_surjective` for the surjective case. -/ +lemma comap_iInf_le {ι : Sort*} {α β : Type*} (f : α → β) (m : ι → MeasurableSpace β) : + MeasurableSpace.comap f (iInf m) ≤ iInf (fun i => MeasurableSpace.comap f (m i)) := by + refine le_iInf (fun i => ?_) + exact MeasurableSpace.comap_mono (iInf_le m i) + +-- Extract witnesses for each comap and choose them uniformly +private lemma comap_iInf_witnesses {ι : Type*} {α β : Type*} {f : α → β} + (m : ι → MeasurableSpace β) (s : Set α) + (hs_all : ∀ i, MeasurableSet[MeasurableSpace.comap f (m i)] s) : + ∃ (T : ι → Set β), (∀ i, MeasurableSet[m i] (T i)) ∧ (∀ i, s = f ⁻¹' (T i)) := by + have : ∀ i, ∃ (T : Set β), MeasurableSet[m i] T ∧ s = f ⁻¹' T := by + intro i + have hi := hs_all i + rw [MeasurableSpace.measurableSet_comap] at hi + rcases hi with ⟨T, hT, hpre⟩ + exact ⟨T, hT, hpre.symm⟩ + choose T hTmeas hspre using this + exact ⟨T, hTmeas, hspre⟩ + +-- All witnesses are equal when f is surjective +private lemma comap_witnesses_eq_of_surjective {ι : Type*} {α β : Type*} {f : α → β} + (hf : Function.Surjective f) (T : ι → Set β) (s : Set α) + (hspre : ∀ i, s = f ⁻¹' (T i)) : + ∀ i j, T i = T j := by + intro i j + have hinj := preimage_injective_of_surjective (α := α) (β := β) hf + have : f ⁻¹' T i = f ⁻¹' T j := by rw [← hspre i, ← hspre j] + exact hinj this + +-- A set is measurable in comap f (iInf m) if it's the preimage of a canonically measurable set +private lemma measurableSet_comap_iInf_of_canonical {ι : Type*} [Nonempty ι] + {α β : Type*} {f : α → β} (m : ι → MeasurableSpace β) + (T0 : Set β) (hT0 : ∀ i, MeasurableSet[m i] T0) (s : Set α) (hs : s = f ⁻¹' T0) : + MeasurableSet[MeasurableSpace.comap f (iInf m)] s := by + refine ⟨T0, ?_, hs.symm⟩ + rw [MeasurableSpace.measurableSet_iInf] + exact hT0 + +/-- With `f` surjective and a nonempty index type, `comap` commutes with `⨅`. + +This is the key lemma for showing that tail σ-algebras defined via coordinate pullbacks +equal tail σ-algebras defined as pullbacks of path-space tails. -/ +theorem iInf_comap_eq_comap_iInf_of_surjective {ι : Type*} [Nonempty ι] {α β : Type*} {f : α → β} + (hf : Function.Surjective f) (m : ι → MeasurableSpace β) : + iInf (fun i => MeasurableSpace.comap f (m i)) = MeasurableSpace.comap f (iInf m) := by + classical + -- (≥) direction holds unconditionally (monotonicity) + have hge : + MeasurableSpace.comap f (iInf m) ≤ iInf (fun i => MeasurableSpace.comap f (m i)) := by + refine le_iInf (fun i => ?_) + exact MeasurableSpace.comap_mono (iInf_le _ i) + + -- (≤) direction uses surjectivity to unify witnesses + have hle : + iInf (fun i => MeasurableSpace.comap f (m i)) ≤ MeasurableSpace.comap f (iInf m) := by + intro s hs + -- For each i, s is measurable in comap f (m i) + have hs_all : ∀ i, MeasurableSet[MeasurableSpace.comap f (m i)] s := by + rw [MeasurableSpace.measurableSet_iInf] at hs + exact hs + + -- Extract witnesses Tᵢ such that s = f ⁻¹' Tᵢ for each i + obtain ⟨T, hTmeas, hspre⟩ := comap_iInf_witnesses m s hs_all + + -- All witnesses are equal by surjectivity + have Tall := comap_witnesses_eq_of_surjective hf T s hspre + + -- Pick canonical witness T₀ + rcases ‹Nonempty ι› with ⟨i₀⟩ + let T0 : Set β := T i₀ + have T_all : ∀ i, T i = T0 := fun i => Tall i i₀ + have s_pre : s = f ⁻¹' T0 := by simpa [T_all i₀] using hspre i₀ + have T0_meas_all : ∀ i, MeasurableSet[m i] T0 := fun i => by simpa [T_all i] using hTmeas i + + -- Conclude measurability + exact measurableSet_comap_iInf_of_canonical m T0 T0_meas_all s s_pre + + exact le_antisymm hle hge + +end MeasurableSpace diff --git a/ForMathlib/README.md b/ForMathlib/README.md new file mode 100644 index 00000000..11223464 --- /dev/null +++ b/ForMathlib/README.md @@ -0,0 +1,76 @@ +# ForMathlib: Upstream Contributions to Mathlib + +This directory contains general-purpose lemmas extracted from the exchangeability project, +organized for potential contribution to [mathlib4](https://github.com/leanprover-community/mathlib4). + +## PR Tracking + +| Candidate | Source | Target | Status | PR # | +|-----------|--------|--------|--------|------| +| `exists_perm_extending_strictMono` | `Contractability.lean:313-370` | `Combinatorics/PermutationExtension.lean` | Ready | - | +| `iInf_comap_eq_comap_iInf_of_surjective` | `Tail/TailSigma.lean:98-220` | `MeasureTheory/MeasurableSpace/ComapInfima.lean` | Ready | - | +| π-system/cylinder infrastructure | `Core.lean:150-346` | `MeasureTheory/Constructions/Pi/Cylinders.lean` | Ready | - | +| `sigmaFinite_trim` | `ForMathlib/.../TrimInstances.lean` | `MeasureTheory/Measure/TrimInstances.lean` | Ready | - | +| Conditional expectation helpers | `Probability/CondExp.lean` | `MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean` | Ready | - | +| Tail σ-algebra infrastructure | `Tail/TailSigma.lean`, `RevFiltration.lean` | `Probability/Process/TailSigmaAlgebra.lean` | Planned | - | +| Finite marginals uniqueness | `Core.lean:336` | `MeasureTheory/Measure/FinMarginals.lean` | Planned | - | + +## PR Sequencing Strategy + +``` +Level 0 (independent - can be submitted in parallel): + PR1: PermutationExtension - pure combinatorics, no measure theory + PR2: ComapInfima - σ-algebra infrastructure + PR3: TrimInstances - already essentially in mathlib + +Level 1 (after Level 0): + PR4: Cylinders - uses ComapInfima patterns, π-system infrastructure + PR5: CondExp helpers - missing API additions + +Level 2 (after Level 1): + PR6: TailSigmaAlgebra - uses ComapInfima, Cylinders + PR7: FinMarginals - uses Cylinders +``` + +## Directory Structure + +``` +ForMathlib/ +├── Combinatorics/ +│ └── PermutationExtension.lean # exists_perm_extending_strictMono +├── MeasureTheory/ +│ ├── MeasurableSpace/ +│ │ └── ComapInfima.lean # iInf_comap_eq_comap_iInf_of_surjective +│ ├── Constructions/ +│ │ └── Pi/ +│ │ └── Cylinders.lean # π-system infrastructure +│ ├── Measure/ +│ │ ├── TrimInstances.lean # sigmaFinite_trim (existing) +│ │ └── FinMarginals.lean # measure_eq_of_fin_marginals_eq +│ └── Function/ +│ └── ConditionalExpectation/ +│ └── Lipschitz.lean # condExp_L1_lipschitz +├── Probability/ +│ ├── Independence/ +│ │ └── Conditional/ +│ │ └── Indicator.lean # condIndep_of_indicator_condexp_eq +│ └── Process/ +│ └── TailSigmaAlgebra.lean # tail filtration infrastructure +└── README.md # This file +``` + +## Contribution Guidelines + +Each ForMathlib file should: +1. Import **only** from mathlib (no `Exchangeability.*` imports) +2. Include a module docstring with: + - Mathematical context and references + - Suggested mathlib location + - Known downstream applications +3. Follow mathlib style conventions +4. Pass `#print axioms` with only standard axioms (propext, quot.sound, choice) + +## References + +- Kallenberg (2005), *Probabilistic Symmetries and Invariance Principles*, Theorem 1.1 +- Mathlib documentation: https://leanprover-community.github.io/mathlib4_docs/ From 82d8cbce553c4b28215eb3489a11bf4f62aea204 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 11:59:34 -0500 Subject: [PATCH 02/20] golf: Simplify proofs in ForMathlib files - PermutationExtension: Condense succ case induction from 10 lines to 3 - ComapInfima: Use existing mathlib lemma hf.preimage_injective --- ForMathlib/Combinatorics/PermutationExtension.lean | 12 ++---------- .../MeasureTheory/MeasurableSpace/ComapInfima.lean | 9 ++------- 2 files changed, 4 insertions(+), 17 deletions(-) diff --git a/ForMathlib/Combinatorics/PermutationExtension.lean b/ForMathlib/Combinatorics/PermutationExtension.lean index acfdcf1f..086ad42a 100644 --- a/ForMathlib/Combinatorics/PermutationExtension.lean +++ b/ForMathlib/Combinatorics/PermutationExtension.lean @@ -54,16 +54,8 @@ lemma strictMono_Fin_ge_id {k : Fin m → ℕ} (hk : StrictMono k) (i : Fin m) : | zero => intro _; exact Nat.zero_le _ | succ n ih => intro hn - have hn' : n < m := Nat.lt_of_succ_lt hn - let j : Fin m := ⟨n, hn'⟩ - let j_succ : Fin m := ⟨n.succ, hn⟩ - have hlt : j < j_succ := by simp [Fin.lt_def, j, j_succ] - have hk_lt : k j < k j_succ := hk hlt - have ih' : n ≤ k j := ih hn' - calc n.succ - = n + 1 := rfl - _ ≤ k j + 1 := Nat.add_le_add_right ih' 1 - _ ≤ k j_succ := Nat.succ_le_of_lt hk_lt + exact Nat.succ_le_of_lt (Nat.lt_of_le_of_lt (ih (Nat.lt_of_succ_lt hn)) + (hk (Fin.mk_lt_mk.mpr (Nat.lt_succ_self n)))) exact this i.val i.isLt /-- diff --git a/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean b/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean index f69cdcb3..ef1265fc 100644 --- a/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean +++ b/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean @@ -45,13 +45,8 @@ namespace MeasurableSpace /-- Preimage is injective on sets when `f` is surjective. -/ lemma preimage_injective_of_surjective {α β : Type*} {f : α → β} (hf : Function.Surjective f) : - Function.Injective (fun (s : Set β) => f ⁻¹' s) := by - intro s t hpre - have : f ⁻¹' s = f ⁻¹' t := hpre - ext y - rcases hf y with ⟨x, rfl⟩ - have := congrArg (fun A => x ∈ A) this - simpa using this + Function.Injective (fun (s : Set β) => f ⁻¹' s) := + hf.preimage_injective /-- If `f` is surjective, then `map f (comap f m) = m`. -/ lemma map_comap_eq_of_surjective {α β : Type*} {f : α → β} From ecec4124f2c770227059a0ee6d62bf3712026c08 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 12:02:10 -0500 Subject: [PATCH 03/20] golf: Further simplify ForMathlib proofs - ComapInfima: Inline comap_iInf_le proof - Cylinders: Inline isPiSystem_prefixCylinders And.intro - Lipschitz: Use Integrable.of_bound for integrable_of_bounded --- ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean | 8 +++----- .../Function/ConditionalExpectation/Lipschitz.lean | 5 ++--- ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean | 5 ++--- 3 files changed, 7 insertions(+), 11 deletions(-) diff --git a/ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean b/ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean index c0565f42..6841dfc0 100644 --- a/ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean +++ b/ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean @@ -170,11 +170,9 @@ lemma isPiSystem_prefixCylinders : use max m n use extendSet (α := α) (Nat.le_max_left m n) S ∩ extendSet (α := α) (Nat.le_max_right m n) T - constructor - · exact MeasurableSet.inter - (extendSet_measurable (α := α) (hmn := Nat.le_max_left m n) hS) - (extendSet_measurable (α := α) (hmn := Nat.le_max_right m n) hT) - · exact prefixCylinder_inter (α := α) + exact ⟨MeasurableSet.inter (extendSet_measurable (α := α) (hmn := Nat.le_max_left m n) hS) + (extendSet_measurable (α := α) (hmn := Nat.le_max_right m n) hT), + prefixCylinder_inter (α := α)⟩ /-- Any cylinder set belongs to the σ-algebra generated by prefix cylinders. -/ @[nolint unusedArguments] diff --git a/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean b/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean index 1d5da566..2c82ca65 100644 --- a/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean +++ b/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean @@ -53,9 +53,8 @@ variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} /-- Bounded measurable functions are integrable on finite measures. -/ lemma integrable_of_bounded [IsFiniteMeasure μ] {f : Ω → ℝ} (hf : Measurable f) (hbd : ∃ C, ∀ ω, |f ω| ≤ C) : - Integrable f μ := by - obtain ⟨C, hC⟩ := hbd - exact ⟨hf.aestronglyMeasurable, HasFiniteIntegral.of_bounded (ae_of_all μ hC)⟩ + Integrable f μ := + hbd.elim fun C hC => Integrable.of_bound hf.aestronglyMeasurable C (ae_of_all μ hC) /-- Product of integrable and bounded measurable functions is integrable. -/ lemma integrable_of_bounded_mul [IsFiniteMeasure μ] diff --git a/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean b/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean index ef1265fc..63a5544e 100644 --- a/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean +++ b/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean @@ -70,9 +70,8 @@ The inequality `comap f (⨅ i, m i) ≤ ⨅ i, comap f (m i)` holds by monotoni The reverse inequality (and hence equality) requires `f` to be surjective. See `iInf_comap_eq_comap_iInf_of_surjective` for the surjective case. -/ lemma comap_iInf_le {ι : Sort*} {α β : Type*} (f : α → β) (m : ι → MeasurableSpace β) : - MeasurableSpace.comap f (iInf m) ≤ iInf (fun i => MeasurableSpace.comap f (m i)) := by - refine le_iInf (fun i => ?_) - exact MeasurableSpace.comap_mono (iInf_le m i) + MeasurableSpace.comap f (iInf m) ≤ iInf (fun i => MeasurableSpace.comap f (m i)) := + le_iInf fun i => MeasurableSpace.comap_mono (iInf_le m i) -- Extract witnesses for each comap and choose them uniformly private lemma comap_iInf_witnesses {ι : Type*} {α β : Type*} {f : α → β} From bc88c666699cb525008b654e69f970bdeff4de1e Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 12:07:17 -0500 Subject: [PATCH 04/20] golf: Condense condExp_L1_lipschitz calc block Replace filter_upwards block with h_linear.mono + congrArg --- .../Function/ConditionalExpectation/Lipschitz.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean b/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean index 2c82ca65..57e76f5a 100644 --- a/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean +++ b/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean @@ -104,10 +104,7 @@ theorem condExp_L1_lipschitz [IsFiniteMeasure μ] have h_linear : ∀ᵐ ω ∂μ, μ[f|m] ω - μ[g|m] ω = μ[(f - g)|m] ω := EventuallyEq.symm (condExp_sub hf hg m) calc ∫ ω, |μ[f|m] ω - μ[g|m] ω| ∂μ - = ∫ ω, |μ[(f - g)|m] ω| ∂μ := by - apply integral_congr_ae - filter_upwards [h_linear] with ω h - rw [h] + = ∫ ω, |μ[(f - g)|m] ω| ∂μ := integral_congr_ae (h_linear.mono fun _ h => congrArg _ h) _ ≤ ∫ ω, |(f - g) ω| ∂μ := integral_abs_condExp_le (f - g) _ = ∫ ω, |f ω - g ω| ∂μ := rfl From 0fc127efb81fb125906fc8affaa039e051bc15a7 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 12:13:04 -0500 Subject: [PATCH 05/20] style: Fix lines over 100 chars in ForMathlib files --- .../Function/ConditionalExpectation/Lipschitz.lean | 6 ++++-- ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean | 7 ++++--- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean b/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean index 57e76f5a..ab1ca795 100644 --- a/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean +++ b/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean @@ -104,7 +104,8 @@ theorem condExp_L1_lipschitz [IsFiniteMeasure μ] have h_linear : ∀ᵐ ω ∂μ, μ[f|m] ω - μ[g|m] ω = μ[(f - g)|m] ω := EventuallyEq.symm (condExp_sub hf hg m) calc ∫ ω, |μ[f|m] ω - μ[g|m] ω| ∂μ - = ∫ ω, |μ[(f - g)|m] ω| ∂μ := integral_congr_ae (h_linear.mono fun _ h => congrArg _ h) + = ∫ ω, |μ[(f - g)|m] ω| ∂μ := + integral_congr_ae (h_linear.mono fun _ h => congrArg _ h) _ ≤ ∫ ω, |(f - g) ω| ∂μ := integral_abs_condExp_le (f - g) _ = ∫ ω, |f ω - g ω| ∂μ := rfl @@ -120,7 +121,8 @@ theorem condExp_mul_pullout {Ω : Type*} {m₀ : MeasurableSpace Ω} {μ : Measu μ[f * g|m] =ᵐ[μ] fun ω => μ[f|m] ω * g ω := by have hg_strong : StronglyMeasurable[m] g := hg_meas.stronglyMeasurable obtain ⟨C, hC⟩ := hg_bd - have hg_bound : ∀ᵐ ω ∂μ, ‖g ω‖ ≤ C := ae_of_all μ fun ω => (Real.norm_eq_abs _).le.trans (hC ω) + have hg_bound : ∀ᵐ ω ∂μ, ‖g ω‖ ≤ C := + ae_of_all μ fun ω => (Real.norm_eq_abs _).le.trans (hC ω) haveI : SigmaFinite (μ.trim hm) := MeasureTheory.Measure.sigmaFinite_trim μ hm have h := condExp_stronglyMeasurable_mul_of_bound hm hg_strong hf C hg_bound -- f * g = g * f pointwise, so μ[f * g|m] =ᵃᵉ μ[g * f|m] = g · μ[f|m] diff --git a/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean b/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean index 63a5544e..ffff16ef 100644 --- a/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean +++ b/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean @@ -24,7 +24,7 @@ This file provides lemmas about how `MeasurableSpace.comap` interacts with infim * `preimage_injective_of_surjective`: Preimage is injective on sets when `f` is surjective * `map_comap_eq_of_surjective`: If `f` is surjective, then `map f (comap f m) = m` -* `comap_iInf_le`: The inequality `comap f (⨅ i, m i) ≤ ⨅ i, comap f (m i)` holds unconditionally +* `comap_iInf_le`: `comap f (⨅ i, m i) ≤ ⨅ i, comap f (m i)` holds unconditionally ## Mathematical Context @@ -110,8 +110,9 @@ private lemma measurableSet_comap_iInf_of_canonical {ι : Type*} [Nonempty ι] This is the key lemma for showing that tail σ-algebras defined via coordinate pullbacks equal tail σ-algebras defined as pullbacks of path-space tails. -/ -theorem iInf_comap_eq_comap_iInf_of_surjective {ι : Type*} [Nonempty ι] {α β : Type*} {f : α → β} - (hf : Function.Surjective f) (m : ι → MeasurableSpace β) : +theorem iInf_comap_eq_comap_iInf_of_surjective {ι : Type*} [Nonempty ι] + {α β : Type*} {f : α → β} (hf : Function.Surjective f) + (m : ι → MeasurableSpace β) : iInf (fun i => MeasurableSpace.comap f (m i)) = MeasurableSpace.comap f (iInf m) := by classical -- (≥) direction holds unconditionally (monotonicity) From d6e6b610ea4f854fd805ba15be5c609e0ba9da57 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 12:18:31 -0500 Subject: [PATCH 06/20] docs: Update ForMathlib README with extraction status Mark all 5 ForMathlib files as extracted with axiom verification. Simplify directory structure to match actual files. --- ForMathlib/README.md | 31 ++++++++++++++----------------- 1 file changed, 14 insertions(+), 17 deletions(-) diff --git a/ForMathlib/README.md b/ForMathlib/README.md index 11223464..de1e2b64 100644 --- a/ForMathlib/README.md +++ b/ForMathlib/README.md @@ -5,15 +5,19 @@ organized for potential contribution to [mathlib4](https://github.com/leanprover ## PR Tracking -| Candidate | Source | Target | Status | PR # | +| Candidate | Target | Status | Axioms | PR # | |-----------|--------|--------|--------|------| -| `exists_perm_extending_strictMono` | `Contractability.lean:313-370` | `Combinatorics/PermutationExtension.lean` | Ready | - | -| `iInf_comap_eq_comap_iInf_of_surjective` | `Tail/TailSigma.lean:98-220` | `MeasureTheory/MeasurableSpace/ComapInfima.lean` | Ready | - | -| π-system/cylinder infrastructure | `Core.lean:150-346` | `MeasureTheory/Constructions/Pi/Cylinders.lean` | Ready | - | -| `sigmaFinite_trim` | `ForMathlib/.../TrimInstances.lean` | `MeasureTheory/Measure/TrimInstances.lean` | Ready | - | -| Conditional expectation helpers | `Probability/CondExp.lean` | `MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean` | Ready | - | -| Tail σ-algebra infrastructure | `Tail/TailSigma.lean`, `RevFiltration.lean` | `Probability/Process/TailSigmaAlgebra.lean` | Planned | - | -| Finite marginals uniqueness | `Core.lean:336` | `MeasureTheory/Measure/FinMarginals.lean` | Planned | - | +| `exists_perm_extending_strictMono` | `Combinatorics/PermutationExtension.lean` | ✅ Extracted | Standard | - | +| `iInf_comap_eq_comap_iInf_of_surjective` | `MeasureTheory/MeasurableSpace/ComapInfima.lean` | ✅ Extracted | Standard | - | +| π-system/cylinder infrastructure | `MeasureTheory/Constructions/Pi/Cylinders.lean` | ✅ Extracted | Standard | - | +| `sigmaFinite_trim` | `MeasureTheory/Measure/TrimInstances.lean` | ✅ Existing | Standard | - | +| `condExp_L1_lipschitz` | `MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean` | ✅ Extracted | Standard | - | + +All extracted files: +- Import only mathlib (no `Exchangeability.*` dependencies) +- Use only standard axioms: `propext`, `Classical.choice`, `Quot.sound` +- Follow mathlib style (<100 char lines) +- Include module docstrings with mathematical context ## PR Sequencing Strategy @@ -43,19 +47,12 @@ ForMathlib/ │ │ └── ComapInfima.lean # iInf_comap_eq_comap_iInf_of_surjective │ ├── Constructions/ │ │ └── Pi/ -│ │ └── Cylinders.lean # π-system infrastructure +│ │ └── Cylinders.lean # π-system, measure_eq_of_fin_marginals_eq │ ├── Measure/ -│ │ ├── TrimInstances.lean # sigmaFinite_trim (existing) -│ │ └── FinMarginals.lean # measure_eq_of_fin_marginals_eq +│ │ └── TrimInstances.lean # sigmaFinite_trim (existing) │ └── Function/ │ └── ConditionalExpectation/ │ └── Lipschitz.lean # condExp_L1_lipschitz -├── Probability/ -│ ├── Independence/ -│ │ └── Conditional/ -│ │ └── Indicator.lean # condIndep_of_indicator_condexp_eq -│ └── Process/ -│ └── TailSigmaAlgebra.lean # tail filtration infrastructure └── README.md # This file ``` From 2c1a01749e29745d38120b0df1963374fbcc7dd0 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 12:50:18 -0500 Subject: [PATCH 07/20] golf: Simplify ForMathlib proofs using mathlib lemmas Batch 1 of ForMathlib extraction Phase 2: - ComapInfima: Remove custom preimage_injective_of_surjective, use Function.Surjective.preimage_injective directly; inline hge proof using comap_iInf_le; simplify witness equality proof - Lipschitz: Use Integrable.mul_bdd directly in integrable_of_bounded_mul; simplify condExp_mul_pullout using single trans chain - Cylinders: Replace custom takePrefix with mathlib's Fin.take; import Mathlib.Data.Fin.Tuple.Take - PermutationExtension: Use Fin.castLEquiv for domain equivalence; import Mathlib.Logic.Equiv.Fin.Basic; simplify proof structure Net reduction: -82 lines across 5 files --- Exchangeability/Tail/TailSigma.lean | 4 +- .../Combinatorics/PermutationExtension.lean | 60 +++++----------- .../Constructions/Pi/Cylinders.lean | 28 +++----- .../ConditionalExpectation/Lipschitz.lean | 22 ++---- .../MeasurableSpace/ComapInfima.lean | 70 +++++-------------- 5 files changed, 51 insertions(+), 133 deletions(-) diff --git a/Exchangeability/Tail/TailSigma.lean b/Exchangeability/Tail/TailSigma.lean index 7829f9ee..0fd24d16 100644 --- a/Exchangeability/Tail/TailSigma.lean +++ b/Exchangeability/Tail/TailSigma.lean @@ -98,8 +98,8 @@ These lemmas are now in `ForMathlib.MeasureTheory.MeasurableSpace.ComapInfima`. We re-export them here for backward compatibility. -/ -- Re-export comap/infima lemmas from ForMathlib -export MeasurableSpace (preimage_injective_of_surjective map_comap_eq_of_surjective - comap_iInf_le iInf_comap_eq_comap_iInf_of_surjective) +export MeasurableSpace (map_comap_eq_of_surjective comap_iInf_le + iInf_comap_eq_comap_iInf_of_surjective) /-! ### Bridge Lemmas (LOAD-BEARING - Phase 1a) -/ diff --git a/ForMathlib/Combinatorics/PermutationExtension.lean b/ForMathlib/Combinatorics/PermutationExtension.lean index 086ad42a..cbcf4cd0 100644 --- a/ForMathlib/Combinatorics/PermutationExtension.lean +++ b/ForMathlib/Combinatorics/PermutationExtension.lean @@ -3,6 +3,7 @@ Copyright (c) 2025 Cameron Freer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Cameron Freer -/ +import Mathlib.Logic.Equiv.Fin.Basic import Mathlib.Logic.Equiv.Fintype import Mathlib.GroupTheory.Perm.Basic @@ -80,50 +81,23 @@ theorem exists_perm_extending_strictMono (k : Fin m → ℕ) ∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin m), (σ ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩).val = k i := by classical - -- Embed `Fin m` into `Fin n` via the initial segment. - let ι : Fin m → Fin n := fun i => ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩ - let p : Fin n → Prop := fun x => x.val < m - let q : Fin n → Prop := fun x => ∃ i : Fin m, x = ⟨k i, hk_bound i⟩ - have hι_mem : ∀ i : Fin m, p (ι i) := fun i => i.isLt let kFin : Fin m → Fin n := fun i => ⟨k i, hk_bound i⟩ - have hk_mem : ∀ i : Fin m, q (kFin i) := fun i => ⟨i, rfl⟩ - haveI : DecidablePred p := fun _ => inferInstance - haveI : DecidablePred q := fun _ => inferInstance - -- Equivalence between the first `m` coordinates and `Fin m`. - let e_dom : {x : Fin n // p x} ≃ Fin m := - { toFun := fun x => ⟨x.1.val, x.2⟩ - , invFun := fun i => ⟨ι i, by dsimp [p, ι]; exact i.isLt⟩ - , left_inv := by rintro ⟨x, hx⟩; ext; simp [ι] - , right_inv := by intro i; cases i with | mk i hi => simp [ι] } - -- Equivalence between the image of `k` and `Fin m`. - -- For injectivity of k, we use that it's strictly monotone - have hk_inj : Function.Injective kFin := - fun i j hij => hk_mono.injective (Fin.ext_iff.mp hij) - let e_cod : Fin m ≃ {x : Fin n // q x} := - { toFun := fun i => ⟨kFin i, hk_mem i⟩ - , invFun := fun y => Classical.choose y.2 - , left_inv := by - intro i - have h_spec := Classical.choose_spec (hk_mem i) - have : k (Classical.choose (hk_mem i)) = k i := by - simpa [kFin] using (Fin.ext_iff.mp h_spec).symm - exact hk_mono.injective this - , right_inv := by - rintro ⟨y, hy⟩ - apply Subtype.ext - simp only [kFin] - exact (Classical.choose_spec hy).symm } - -- Equivalence between the subtypes describing the first `m` coordinates and the image of `k`. - let e : {x : Fin n // p x} ≃ {x : Fin n // q x} := e_dom.trans e_cod - -- Extend this equivalence to a permutation of `Fin n`. - let σ : Equiv.Perm (Fin n) := Equiv.extendSubtype e - have hσ_apply : ∀ i : Fin m, σ (ι i) = kFin i := by - intro i - have h_apply := Equiv.extendSubtype_apply_of_mem (e := e) (x := ι i) (hι_mem i) - dsimp [σ, e, Equiv.trans, e_dom, e_cod, ι, Fin.castLEEmb, kFin] at h_apply - simpa using h_apply + -- e_dom: first m elements of Fin n ≃ Fin m (using mathlib's Fin.castLEquiv) + let e_dom : {x : Fin n // (x : ℕ) < m} ≃ Fin m := (Fin.castLEquiv hmn).symm + -- e_cod: Fin m ≃ image of k (via strict monotonicity giving injectivity) + let e_cod : Fin m ≃ {x : Fin n // ∃ i : Fin m, x = kFin i} := + { toFun := fun i => ⟨kFin i, i, rfl⟩ + invFun := fun y => Classical.choose y.2 + left_inv := fun i => by + have h_spec := Classical.choose_spec (⟨i, rfl⟩ : ∃ j : Fin m, kFin i = kFin j) + exact hk_mono.injective (by simpa [kFin] using (Fin.ext_iff.mp h_spec).symm) + right_inv := fun ⟨_, hy⟩ => Subtype.ext (Classical.choose_spec hy).symm } + -- Compose and extend to full permutation + let σ : Equiv.Perm (Fin n) := Equiv.extendSubtype (e_dom.trans e_cod) refine ⟨σ, fun i => ?_⟩ - have hσ_val : (σ (ι i)).val = k i := by simpa [kFin] using congrArg Fin.val (hσ_apply i) - simpa [ι] using hσ_val + have h := Equiv.extendSubtype_apply_of_mem (e := e_dom.trans e_cod) + (x := Fin.castLE hmn i) i.isLt + simp only [Equiv.trans_apply, kFin] at h + exact congrArg Fin.val h end Combinatorics diff --git a/ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean b/ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean index 6841dfc0..ca37f95a 100644 --- a/ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean +++ b/ForMathlib/MeasureTheory/Constructions/Pi/Cylinders.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 Cameron Freer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Cameron Freer -/ -import Mathlib.Data.Fin.Tuple.Basic +import Mathlib.Data.Fin.Tuple.Take import Mathlib.Logic.Equiv.Fintype import Mathlib.MeasureTheory.Constructions.Cylinders import Mathlib.MeasureTheory.Measure.ProbabilityMeasure @@ -113,24 +113,15 @@ section Extend variable {m n : ℕ} -/-- Restrict a finite tuple to its first `m` coordinates. -/ -def takePrefix (hmn : m ≤ n) (x : Fin n → α) : Fin m → α := - fun i => x (Fin.castLE hmn i) - -omit [MeasurableSpace α] in -@[simp] -lemma takePrefix_apply {hmn : m ≤ n} (x : Fin n → α) (i : Fin m) : - takePrefix (α := α) hmn x i = x (Fin.castLE hmn i) := rfl - omit [MeasurableSpace α] in @[simp] -lemma takePrefix_prefixProj {hmn : m ≤ n} (x : ℕ → α) : - takePrefix (α := α) hmn (prefixProj (α := α) n x) = prefixProj (α := α) m x := by - ext i; simp [takePrefix] +lemma take_prefixProj {hmn : m ≤ n} (x : ℕ → α) : + Fin.take m hmn (prefixProj (α := α) n x) = prefixProj (α := α) m x := by + ext i; simp [prefixProj] /-- Extend a set from `Fin m → α` to `Fin n → α` by ignoring extra coordinates. -/ def extendSet (hmn : m ≤ n) (S : Set (Fin m → α)) : Set (Fin n → α) := - {x | takePrefix (α := α) hmn x ∈ S} + {x | Fin.take m hmn x ∈ S} omit [MeasurableSpace α] in lemma prefixCylinder_inter {m n : ℕ} {S : Set (Fin m → α)} {T : Set (Fin n → α)} : @@ -139,21 +130,20 @@ lemma prefixCylinder_inter {m n : ℕ} {S : Set (Fin m → α)} {T : Set (Fin n (extendSet (α := α) (Nat.le_max_left _ _) S ∩ extendSet (α := α) (Nat.le_max_right _ _) T) := by ext x - simp only [Set.mem_inter_iff, mem_prefixCylinder, extendSet, Set.mem_setOf_eq, - takePrefix_prefixProj] + simp only [Set.mem_inter_iff, mem_prefixCylinder, extendSet, Set.mem_setOf_eq, take_prefixProj] -- Disable false-positive linter warnings: Measurable (Fin n → α) depends on [MeasurableSpace α] set_option linter.unusedSectionVars false @[nolint unusedArguments] -lemma takePrefix_measurable (hmn : m ≤ n) : - Measurable (takePrefix (α := α) hmn) := +lemma take_measurable (hmn : m ≤ n) : + Measurable (Fin.take (α := fun _ => α) m hmn) := measurable_pi_lambda _ (fun i => measurable_pi_apply (Fin.castLE hmn i)) @[nolint unusedArguments] lemma extendSet_measurable {S : Set (Fin m → α)} {hmn : m ≤ n} (hS : MeasurableSet S) : MeasurableSet (extendSet (α := α) hmn S) := - (takePrefix_measurable (α := α) hmn) hS + (take_measurable (α := α) hmn) hS end Extend diff --git a/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean b/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean index ab1ca795..b569c15d 100644 --- a/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean +++ b/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean @@ -61,13 +61,8 @@ lemma integrable_of_bounded_mul [IsFiniteMeasure μ] {f g : Ω → ℝ} (hf : Integrable f μ) (hg : Measurable g) (hbd : ∃ C, ∀ ω, |g ω| ≤ C) : Integrable (f * g) μ := by - have : f * g = fun ω => g ω * f ω := funext fun _ => mul_comm _ _ - rw [this] obtain ⟨C, hC⟩ := hbd - have hbd_ae : ∀ᵐ ω ∂μ, ‖g ω‖ ≤ C := by - filter_upwards with ω - exact (Real.norm_eq_abs _).symm ▸ hC ω - exact Integrable.bdd_mul hf hg.aestronglyMeasurable hbd_ae + exact hf.mul_bdd hg.aestronglyMeasurable (ae_of_all μ fun ω => (Real.norm_eq_abs _).le.trans (hC ω)) /-- Conditional expectation preserves monotonicity in absolute value. @@ -119,17 +114,12 @@ theorem condExp_mul_pullout {Ω : Type*} {m₀ : MeasurableSpace Ω} {μ : Measu (hg_meas : @Measurable Ω ℝ m _ g) (hg_bd : ∃ C, ∀ ω, |g ω| ≤ C) : μ[f * g|m] =ᵐ[μ] fun ω => μ[f|m] ω * g ω := by - have hg_strong : StronglyMeasurable[m] g := hg_meas.stronglyMeasurable obtain ⟨C, hC⟩ := hg_bd - have hg_bound : ∀ᵐ ω ∂μ, ‖g ω‖ ≤ C := - ae_of_all μ fun ω => (Real.norm_eq_abs _).le.trans (hC ω) haveI : SigmaFinite (μ.trim hm) := MeasureTheory.Measure.sigmaFinite_trim μ hm - have h := condExp_stronglyMeasurable_mul_of_bound hm hg_strong hf C hg_bound - -- f * g = g * f pointwise, so μ[f * g|m] =ᵃᵉ μ[g * f|m] = g · μ[f|m] - have hcomm : f * g =ᵐ[μ] g * f := by filter_upwards with ω; simp only [Pi.mul_apply]; ring - have step1 : μ[f * g|m] =ᵐ[μ] μ[g * f|m] := condExp_congr_ae hcomm - have step2 : (fun ω => g ω * μ[f|m] ω) =ᵐ[μ] (fun ω => μ[f|m] ω * g ω) := by - filter_upwards with ω; ring - exact step1.trans (h.trans step2) + have h := condExp_stronglyMeasurable_mul_of_bound hm hg_meas.stronglyMeasurable hf C + (ae_of_all μ fun ω => (Real.norm_eq_abs _).le.trans (hC ω)) + -- f * g = g * f pointwise, so apply mathlib's g·E[f|m] version and commute + exact (condExp_congr_ae (ae_of_all μ fun _ => mul_comm _ _)).trans + (h.trans (ae_of_all μ fun _ => mul_comm _ _)) end CondExp diff --git a/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean b/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean index ffff16ef..39fae1cf 100644 --- a/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean +++ b/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean @@ -22,7 +22,6 @@ This file provides lemmas about how `MeasurableSpace.comap` interacts with infim ## Supporting Lemmas -* `preimage_injective_of_surjective`: Preimage is injective on sets when `f` is surjective * `map_comap_eq_of_surjective`: If `f` is surjective, then `map f (comap f m) = m` * `comap_iInf_le`: `comap f (⨅ i, m i) ≤ ⨅ i, comap f (m i)` holds unconditionally @@ -42,27 +41,14 @@ either as pullbacks of the path-space tail, or as infima of coordinate-wise σ-a namespace MeasurableSpace -/-- Preimage is injective on sets when `f` is surjective. -/ -lemma preimage_injective_of_surjective {α β : Type*} {f : α → β} - (hf : Function.Surjective f) : - Function.Injective (fun (s : Set β) => f ⁻¹' s) := - hf.preimage_injective - /-- If `f` is surjective, then `map f (comap f m) = m`. -/ lemma map_comap_eq_of_surjective {α β : Type*} {f : α → β} (hf : Function.Surjective f) (m : MeasurableSpace β) : MeasurableSpace.map f (MeasurableSpace.comap f m) = m := by - classical ext S; constructor - · intro hS - change MeasurableSet[MeasurableSpace.comap f m] (f ⁻¹' S) at hS - rcases hS with ⟨T, hT, hpre⟩ - have hinj := preimage_injective_of_surjective (α := α) (β := β) hf - have : S = T := by apply hinj; exact hpre.symm - simpa [this] - · intro hS - change MeasurableSet[MeasurableSpace.comap f m] (f ⁻¹' S) - exact ⟨S, hS, rfl⟩ + · rintro ⟨T, hT, hpre⟩ + simpa [hf.preimage_injective hpre.symm] using hT + · exact fun hS => ⟨S, hS, rfl⟩ /-- `comap` distributes over `iInf` unconditionally (≤ direction only). @@ -91,11 +77,8 @@ private lemma comap_iInf_witnesses {ι : Type*} {α β : Type*} {f : α → β} private lemma comap_witnesses_eq_of_surjective {ι : Type*} {α β : Type*} {f : α → β} (hf : Function.Surjective f) (T : ι → Set β) (s : Set α) (hspre : ∀ i, s = f ⁻¹' (T i)) : - ∀ i j, T i = T j := by - intro i j - have hinj := preimage_injective_of_surjective (α := α) (β := β) hf - have : f ⁻¹' T i = f ⁻¹' T j := by rw [← hspre i, ← hspre j] - exact hinj this + ∀ i j, T i = T j := fun i j => + hf.preimage_injective (by rw [← hspre i, ← hspre j]) -- A set is measurable in comap f (iInf m) if it's the preimage of a canonically measurable set private lemma measurableSet_comap_iInf_of_canonical {ι : Type*} [Nonempty ι] @@ -114,38 +97,19 @@ theorem iInf_comap_eq_comap_iInf_of_surjective {ι : Type*} [Nonempty ι] {α β : Type*} {f : α → β} (hf : Function.Surjective f) (m : ι → MeasurableSpace β) : iInf (fun i => MeasurableSpace.comap f (m i)) = MeasurableSpace.comap f (iInf m) := by - classical - -- (≥) direction holds unconditionally (monotonicity) - have hge : - MeasurableSpace.comap f (iInf m) ≤ iInf (fun i => MeasurableSpace.comap f (m i)) := by - refine le_iInf (fun i => ?_) - exact MeasurableSpace.comap_mono (iInf_le _ i) - -- (≤) direction uses surjectivity to unify witnesses - have hle : - iInf (fun i => MeasurableSpace.comap f (m i)) ≤ MeasurableSpace.comap f (iInf m) := by - intro s hs + refine le_antisymm ?_ (comap_iInf_le f m) + intro s hs -- For each i, s is measurable in comap f (m i) - have hs_all : ∀ i, MeasurableSet[MeasurableSpace.comap f (m i)] s := by - rw [MeasurableSpace.measurableSet_iInf] at hs - exact hs - - -- Extract witnesses Tᵢ such that s = f ⁻¹' Tᵢ for each i - obtain ⟨T, hTmeas, hspre⟩ := comap_iInf_witnesses m s hs_all - - -- All witnesses are equal by surjectivity - have Tall := comap_witnesses_eq_of_surjective hf T s hspre - - -- Pick canonical witness T₀ - rcases ‹Nonempty ι› with ⟨i₀⟩ - let T0 : Set β := T i₀ - have T_all : ∀ i, T i = T0 := fun i => Tall i i₀ - have s_pre : s = f ⁻¹' T0 := by simpa [T_all i₀] using hspre i₀ - have T0_meas_all : ∀ i, MeasurableSet[m i] T0 := fun i => by simpa [T_all i] using hTmeas i - - -- Conclude measurability - exact measurableSet_comap_iInf_of_canonical m T0 T0_meas_all s s_pre - - exact le_antisymm hle hge + have hs_all : ∀ i, MeasurableSet[MeasurableSpace.comap f (m i)] s := + MeasurableSpace.measurableSet_iInf.mp hs + -- Extract witnesses Tᵢ such that s = f ⁻¹' Tᵢ for each i + obtain ⟨T, hTmeas, hspre⟩ := comap_iInf_witnesses m s hs_all + -- All witnesses are equal by surjectivity + have Tall := comap_witnesses_eq_of_surjective hf T s hspre + -- Pick canonical witness T₀ + rcases ‹Nonempty ι› with ⟨i₀⟩ + exact measurableSet_comap_iInf_of_canonical m (T i₀) + (fun i => by simpa [Tall i i₀] using hTmeas i) s (hspre i₀) end MeasurableSpace From cb37efdaf3f683b2a9f2f916e0804bd70c6e441c Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 12:53:20 -0500 Subject: [PATCH 08/20] feat: Add LpHelpers and SigmaAlgebraHelpers to ForMathlib MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Batch 2 of ForMathlib extraction Phase 2: ForMathlib/MeasureTheory/Function/LpHelpers.lean: - eLpNorm_two_sq_eq_integral_sq: L² norm² = integral of square - eLpNorm_lt_of_integral_sq_lt: integral bound → norm bound - memLp_of_abs_le_const: bounded functions in Lp - memLp_two_of_bounded: bounded functions in L² - setIntegral_le_eLpNorm_mul_measure: Cauchy-Schwarz on sets - abs_integral_mul_le_L2: Cauchy-Schwarz for L² - L2_tendsto_implies_L1_tendsto_of_bounded: L² → L¹ convergence - integral_pushforward_id/sq_diff/continuous: pushforward integrals ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean: - aestronglyMeasurable_iInf_antitone: preservation under infima - aestronglyMeasurable_sub_of_tendsto_ae: preservation under limits These bridge ENNReal-valued Lp norms and Real-valued integrals for probability theory applications. --- .../MeasureTheory/Function/LpHelpers.lean | 245 ++++++++++++++++++ .../MeasurableSpace/SigmaAlgebraHelpers.lean | 141 ++++++++++ 2 files changed, 386 insertions(+) create mode 100644 ForMathlib/MeasureTheory/Function/LpHelpers.lean create mode 100644 ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean diff --git a/ForMathlib/MeasureTheory/Function/LpHelpers.lean b/ForMathlib/MeasureTheory/Function/LpHelpers.lean new file mode 100644 index 00000000..61c6362f --- /dev/null +++ b/ForMathlib/MeasureTheory/Function/LpHelpers.lean @@ -0,0 +1,245 @@ +/- +Copyright (c) 2025 Cameron Freer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Cameron Freer +-/ +import Mathlib.MeasureTheory.Function.L2Space +import Mathlib.MeasureTheory.Function.LpSeminorm.Basic +import Mathlib.Analysis.SpecialFunctions.Pow.Real +import Mathlib.Analysis.InnerProductSpace.Basic + +/-! +# Lp Norm Helper Lemmas + +This file contains helper lemmas about Lp norms and their relationship to integrals, +suitable for contribution to mathlib. + +## Main Results + +### L² Norm and Integral Relationship +* `eLpNorm_two_sq_eq_integral_sq`: For real functions in L², eLpNorm² equals integral of square +* `eLpNorm_lt_of_integral_sq_lt`: If ∫ f² < r², then eLpNorm f 2 < r + +### Membership in Lp Spaces +* `memLp_of_abs_le_const`: Bounded functions are in Lp on finite measures +* `memLp_two_of_bounded`: Bounded functions are in L² on probability spaces + +### L² Inner Product Bounds +* `setIntegral_le_eLpNorm_mul_measure`: |∫_A g| ≤ ‖g‖₂ · √(μ A) (Cauchy-Schwarz) + +### Cauchy-Schwarz and Convergence +* `abs_integral_mul_le_L2`: Cauchy-Schwarz inequality for L² real-valued functions +* `L2_tendsto_implies_L1_tendsto_of_bounded`: L² → L¹ convergence for bounded functions + +These lemmas bridge the gap between the ENNReal-valued eLpNorm and Real-valued integrals, +which is essential for applying analysis results in probability theory. + +## Suggested Mathlib Location + +`Mathlib.MeasureTheory.Function.L2Space` or `Mathlib.MeasureTheory.Function.LpSeminorm.Basic` + +## References + +* Kallenberg (2005), *Probabilistic Symmetries and Invariance Principles* +* Williams (1991), *Probability with Martingales* +-/ + +noncomputable section + +namespace MeasureTheory + +open ENNReal Filter Topology + +variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} + +/-! ### L² Norm and Integral Relationship -/ + +/-- **L² norm squared equals integral of square for real functions.** + +For a real-valued function f in L²(μ), the square of its L² norm equals +the integral of f²: + + (eLpNorm f 2 μ)² = ∫ f² dμ + +This is a fundamental relationship used throughout probability theory, bridging +the gap between ENNReal-valued Lp norms and Real-valued integrals. -/ +@[nolint unusedArguments] +lemma eLpNorm_two_sq_eq_integral_sq [IsFiniteMeasure μ] {f : Ω → ℝ} (hf : MemLp f 2 μ) : + (eLpNorm f 2 μ).toReal ^ 2 = ∫ ω, (f ω) ^ 2 ∂μ := by + have h_norm_eq : ∀ ω, ‖f ω‖ ^ 2 = (f ω) ^ 2 := fun ω => by rw [Real.norm_eq_abs, sq_abs] + rw [eLpNorm_eq_lintegral_rpow_enorm (by norm_num : (2 : ℝ≥0∞) ≠ 0) + (by norm_num : (2 : ℝ≥0∞) ≠ ∞)] + simp only [ENNReal.toReal_ofNat] + conv_lhs => rw [← ENNReal.toReal_rpow] + rw [← Real.rpow_natCast _ 2, ← Real.rpow_mul ENNReal.toReal_nonneg] + norm_num + have h_enorm_conv : ∫⁻ (x : Ω), ‖f x‖ₑ ^ 2 ∂μ = ∫⁻ (x : Ω), ENNReal.ofReal (‖f x‖ ^ 2) ∂μ := by + congr 1; ext ω + calc ‖f ω‖ₑ ^ 2 + = (↑‖f ω‖₊ : ℝ≥0∞) ^ 2 := by rw [enorm_eq_nnnorm] + _ = ↑(‖f ω‖₊ ^ 2) := by rw [← ENNReal.coe_pow] + _ = ENNReal.ofReal (↑(‖f ω‖₊ ^ 2) : ℝ) := by rw [ENNReal.ofReal_coe_nnreal] + _ = ENNReal.ofReal ((↑‖f ω‖₊ : ℝ) ^ 2) := by rw [NNReal.coe_pow] + _ = ENNReal.ofReal (‖f ω‖ ^ 2) := by rw [coe_nnnorm] + rw [h_enorm_conv, ← integral_eq_lintegral_of_nonneg_ae] + · congr 1; ext ω; exact h_norm_eq ω + · exact ae_of_all _ fun _ => sq_nonneg _ + · exact AEStronglyMeasurable.pow hf.1.norm + +/-- **L² norm bound from integral bound.** + +If the integral of f² is less than r², then the L² norm of f is less than r. -/ +lemma eLpNorm_lt_of_integral_sq_lt [IsFiniteMeasure μ] {f : Ω → ℝ} {r : ℝ} (hf : MemLp f 2 μ) + (hr : 0 < r) (h : ∫ ω, (f ω) ^ 2 ∂μ < r ^ 2) : eLpNorm f 2 μ < ENNReal.ofReal r := by + have h_eq : (eLpNorm f 2 μ).toReal ^ 2 = ∫ ω, (f ω) ^ 2 ∂μ := eLpNorm_two_sq_eq_integral_sq hf + have h_toReal_sq_lt : (eLpNorm f 2 μ).toReal ^ 2 < r ^ 2 := by rw [h_eq]; exact h + have h_toReal_lt : (eLpNorm f 2 μ).toReal < r := by + have := abs_lt_of_sq_lt_sq h_toReal_sq_lt (le_of_lt hr) + rwa [abs_of_nonneg ENNReal.toReal_nonneg] at this + have h_lt_top : eLpNorm f 2 μ < ∞ := hf.2 + rw [← ENNReal.ofReal_toReal (ne_of_lt h_lt_top)] + exact ENNReal.ofReal_lt_ofReal_iff hr |>.mpr h_toReal_lt + +/-! ### Membership in Lp Spaces -/ + +/-- **Functions bounded by a constant are in Lp.** + +If |f| ≤ M almost everywhere, then f ∈ Lp for any p ∈ [1, ∞) on a finite measure space. -/ +@[nolint unusedArguments] +lemma memLp_of_abs_le_const [IsFiniteMeasure μ] {f : Ω → ℝ} {M : ℝ} (hf_meas : Measurable f) + (hf_bdd : ∀ᵐ ω ∂μ, |f ω| ≤ M) (p : ℝ≥0∞) (_ : 1 ≤ p) (_ : p ≠ ∞) : MemLp f p μ := + MemLp.of_bound hf_meas.aestronglyMeasurable M + (hf_bdd.mono fun _ hω => (Real.norm_eq_abs _).le.trans hω) + +/-- **Block average of bounded function is in L².** + +Special case: If f is bounded by M, then f is in L² on a probability space. -/ +lemma memLp_two_of_bounded [IsProbabilityMeasure μ] {f : Ω → ℝ} {M : ℝ} (hf_meas : Measurable f) + (hf_bdd : ∀ ω, |f ω| ≤ M) : MemLp f 2 μ := + memLp_of_abs_le_const hf_meas (ae_of_all μ hf_bdd) 2 (by norm_num) (by norm_num) + +/-! ### L² Inner Product Bounds -/ + +/-- **Cauchy-Schwarz on set integrals (probability measure).** + +For a set A and function g ∈ L²(μ), the absolute value of ∫_A g is bounded +by the L² norm of g times √(μ A). + +On probability spaces with μ A ≤ 1, this simplifies to |∫_A g| ≤ ‖g‖₂. -/ +lemma setIntegral_le_eLpNorm_mul_measure [IsProbabilityMeasure μ] (A : Set Ω) + (hA : MeasurableSet A) {g : Ω → ℝ} (hg : MemLp g 2 μ) : + |∫ x in A, g x ∂μ| ≤ (eLpNorm g 2 μ).toReal * (μ A).toReal ^ (1/2 : ℝ) := by + have hμA : μ A ≠ ∞ := (measure_lt_top μ A).ne + let g_Lp : Lp ℝ 2 μ := hg.toLp g + let indicator_Lp := indicatorConstLp 2 hA hμA (1 : ℝ) + have h_inner : ∫ x in A, g x ∂μ = @inner ℝ (Lp ℝ 2 μ) _ indicator_Lp g_Lp := by + rw [L2.inner_indicatorConstLp_one hA hμA g_Lp] + exact setIntegral_congr_ae hA (hg.coeFn_toLp.mono fun x hx _ => hx.symm) + have h_norm_g : ‖g_Lp‖ = (eLpNorm g 2 μ).toReal := Lp.norm_toLp g hg + have h_norm_ind : ‖indicator_Lp‖ = (μ A).toReal ^ (1/2 : ℝ) := by + rw [norm_indicatorConstLp (by norm_num : (2 : ℝ≥0∞) ≠ 0) (by norm_num : (2 : ℝ≥0∞) ≠ ∞)] + simp only [norm_one, one_mul, ENNReal.toReal_ofNat, one_div, measureReal_def] + calc |∫ x in A, g x ∂μ| + = |@inner ℝ (Lp ℝ 2 μ) _ indicator_Lp g_Lp| := by rw [h_inner] + _ ≤ ‖indicator_Lp‖ * ‖g_Lp‖ := abs_real_inner_le_norm _ _ + _ = (μ A).toReal ^ (1/2 : ℝ) * (eLpNorm g 2 μ).toReal := by rw [h_norm_ind, h_norm_g] + _ = (eLpNorm g 2 μ).toReal * (μ A).toReal ^ (1/2 : ℝ) := mul_comm _ _ + +/-! ### Cauchy-Schwarz Inequality -/ + +/-- **Cauchy-Schwarz inequality for L² real-valued functions.** + +For integrable functions f, g in L²(μ): + |∫ f·g dμ| ≤ (∫ f² dμ)^(1/2) · (∫ g² dμ)^(1/2) -/ +@[nolint unusedArguments] +lemma abs_integral_mul_le_L2 [IsFiniteMeasure μ] {f g : Ω → ℝ} (hf : MemLp f 2 μ) + (hg : MemLp g 2 μ) : |∫ ω, f ω * g ω ∂μ| + ≤ (∫ ω, (f ω) ^ 2 ∂μ) ^ (1/2 : ℝ) * (∫ ω, (g ω) ^ 2 ∂μ) ^ (1/2 : ℝ) := by + have hf_abs : MemLp (fun ω => |f ω|) (ENNReal.ofReal 2) μ := by convert hf.abs; norm_num + have hg_abs : MemLp (fun ω => |g ω|) (ENNReal.ofReal 2) μ := by convert hg.abs; norm_num + have h_conj : (2 : ℝ).HolderConjugate 2 := by constructor <;> norm_num + calc |∫ ω, f ω * g ω ∂μ| + ≤ ∫ ω, |f ω * g ω| ∂μ := by + have : |∫ ω, f ω * g ω ∂μ| = ‖∫ ω, f ω * g ω ∂μ‖ := Real.norm_eq_abs _ + rw [this]; exact norm_integral_le_integral_norm _ + _ = ∫ ω, |f ω| * |g ω| ∂μ := by congr 1 with ω; exact abs_mul (f ω) (g ω) + _ ≤ (∫ ω, |f ω| ^ 2 ∂μ) ^ (1/2 : ℝ) * (∫ ω, |g ω| ^ 2 ∂μ) ^ (1/2 : ℝ) := by + convert integral_mul_le_Lp_mul_Lq_of_nonneg h_conj ?_ ?_ hf_abs hg_abs using 2 <;> norm_num + · apply ae_of_all; intro; positivity + · apply ae_of_all; intro; positivity + _ = (∫ ω, (f ω) ^ 2 ∂μ) ^ (1/2 : ℝ) * (∫ ω, (g ω) ^ 2 ∂μ) ^ (1/2 : ℝ) := by simp only [sq_abs] + +/-! ### L² to L¹ Convergence -/ + +/-- **L² convergence implies L¹ convergence for uniformly bounded functions.** + +On a probability space, if fₙ → g in L² and the functions are uniformly bounded, +then fₙ → g in L¹. + +This follows from Cauchy-Schwarz: ∫|f - g| ≤ (∫(f-g)²)^(1/2) · (∫ 1)^(1/2) = (∫(f-g)²)^(1/2) -/ +lemma L2_tendsto_implies_L1_tendsto_of_bounded [IsProbabilityMeasure μ] (f : ℕ → Ω → ℝ) + (g : Ω → ℝ) (hf_meas : ∀ n, Measurable (f n)) (hf_bdd : ∃ M, ∀ n ω, |f n ω| ≤ M) + (hg_memLp : MemLp g 2 μ) (hL2 : Tendsto (fun n => ∫ ω, (f n ω - g ω)^2 ∂μ) atTop (𝓝 0)) : + Tendsto (fun n => ∫ ω, |f n ω - g ω| ∂μ) atTop (𝓝 0) := by + have hL2_sqrt : Tendsto (fun n => (∫ ω, (f n ω - g ω)^2 ∂μ) ^ (1/2 : ℝ)) atTop (𝓝 0) := by + have : (0 : ℝ) ^ (1/2 : ℝ) = 0 := by norm_num + rw [← this] + exact Tendsto.rpow hL2 tendsto_const_nhds (Or.inr (by norm_num : 0 < (1/2 : ℝ))) + have hbound : ∀ n, ∫ ω, |f n ω - g ω| ∂μ ≤ (∫ ω, (f n ω - g ω)^2 ∂μ) ^ (1/2 : ℝ) := by + intro n + have h_memLp : MemLp (fun ω => f n ω - g ω) 2 μ := by + obtain ⟨M, hM⟩ := hf_bdd + have hf_memLp : MemLp (f n) 2 μ := MemLp.of_bound (hf_meas n).aestronglyMeasurable M + (ae_of_all μ (fun ω => (Real.norm_eq_abs _).le.trans (hM n ω))) + exact hf_memLp.sub hg_memLp + have one_memLp : MemLp (fun _ => (1 : ℝ)) 2 μ := memLp_const 1 + have h_abs_memLp : MemLp (fun ω => |f n ω - g ω|) 2 μ := by convert h_memLp.abs using 1 + have cs_abs := abs_integral_mul_le_L2 h_abs_memLp one_memLp + calc ∫ ω, |f n ω - g ω| ∂μ + = ∫ ω, |f n ω - g ω| * 1 ∂μ := by simp only [mul_one] + _ = |∫ ω, |f n ω - g ω| * 1 ∂μ| := by + symm; exact abs_of_nonneg (integral_nonneg (fun ω => by positivity)) + _ ≤ (∫ ω, (|f n ω - g ω|) ^ 2 ∂μ) ^ (1/2 : ℝ) * (∫ ω, (1 : ℝ) ^ 2 ∂μ) ^ (1/2 : ℝ) := cs_abs + _ = (∫ ω, (f n ω - g ω) ^ 2 ∂μ) ^ (1/2 : ℝ) * (∫ ω, (1 : ℝ) ^ 2 ∂μ) ^ (1/2 : ℝ) := by + congr 1; apply congr_arg (· ^ (1/2 : ℝ)) + exact integral_congr_ae (ae_of_all _ fun _ => sq_abs _) + _ = (∫ ω, (f n ω - g ω) ^ 2 ∂μ) ^ (1/2 : ℝ) * 1 := by + congr 2 + have : ∫ ω, (1 : ℝ) ^ 2 ∂μ = 1 := by + simp only [one_pow, integral_const, smul_eq_mul, mul_one, Measure.real] + simp [measure_univ] + rw [this]; norm_num + _ = (∫ ω, (f n ω - g ω) ^ 2 ∂μ) ^ (1/2 : ℝ) := by ring + exact tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hL2_sqrt + (Eventually.of_forall fun n => integral_nonneg fun _ => abs_nonneg _) + (Eventually.of_forall hbound) + +/-! ### Pushforward Measure Integrals -/ + +/-- **Integral of identity function under pushforward measure.** + +For measurable f: ∫ x, x d(f₊μ) = ∫ ω, f ω dμ -/ +lemma integral_pushforward_id {f : Ω → ℝ} (hf : Measurable f) : + ∫ x, x ∂(Measure.map f μ) = ∫ ω, f ω ∂μ := + integral_map hf.aemeasurable aestronglyMeasurable_id + +/-- **Integral of squared difference under pushforward measure.** + +For measurable f and constant c: + ∫ x, (x - c)² d(f₊μ) = ∫ ω, (f ω - c)² dμ -/ +lemma integral_pushforward_sq_diff {f : Ω → ℝ} (hf : Measurable f) (c : ℝ) : + ∫ x, (x - c) ^ 2 ∂(Measure.map f μ) = ∫ ω, (f ω - c) ^ 2 ∂μ := by + rw [integral_map hf.aemeasurable] + exact (continuous_id.sub continuous_const).pow 2 |>.aestronglyMeasurable + +/-- **Integral of continuous function under pushforward.** + +For measurable f and continuous g: + ∫ x, g x d(f₊μ) = ∫ ω, g (f ω) dμ -/ +lemma integral_pushforward_continuous {f : Ω → ℝ} {g : ℝ → ℝ} + (hf : Measurable f) (hg : Continuous g) : + ∫ x, g x ∂(Measure.map f μ) = ∫ ω, g (f ω) ∂μ := by + rw [integral_map hf.aemeasurable] + exact hg.aestronglyMeasurable + +end MeasureTheory diff --git a/ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean b/ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean new file mode 100644 index 00000000..04505d4e --- /dev/null +++ b/ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean @@ -0,0 +1,141 @@ +/- +Copyright (c) 2025 Cameron Freer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Cameron Freer +-/ +import Mathlib.MeasureTheory.Function.AEEqFun +import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic +import Mathlib.Order.Filter.Basic + +/-! +# σ-Algebra Helpers for AEStronglyMeasurable + +This file provides helper lemmas for establishing AEStronglyMeasurable with respect +to infima of σ-algebras and limits of sequences. These are useful for working with +tail σ-algebras and reverse martingales. + +## Main Results + +* `aestronglyMeasurable_iInf_antitone`: AEStronglyMeasurable is preserved under + infimum of antitone σ-algebras +* `aestronglyMeasurable_sub_of_tendsto_ae`: AEStronglyMeasurable for sub-σ-algebras + is preserved under a.e. pointwise limits + +## Mathematical Context + +These results are crucial for proving properties of tail σ-algebras, where one needs +to show that functions measurable with respect to each σ-algebra in a decreasing +sequence are also measurable with respect to the infimum. + +The key technique is using liminf/limsup to construct Measurable witnesses that +agree a.e. with the original function. + +## Suggested Mathlib Location + +`Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic` or a new file +`Mathlib.MeasureTheory.MeasurableSpace.InfSigmaAlgebra` + +## References + +* Kallenberg (2005), *Foundations of Modern Probability*, for general treatment +-/ + +noncomputable section + +open MeasureTheory Filter + +/-! ## AEStronglyMeasurable for infimum of σ-algebras + +For real-valued functions, if f is AEStronglyMeasurable with respect to each σ-algebra +in an antitone (decreasing) sequence, then f is AEStronglyMeasurable with respect to +their infimum. + +**Mathematical justification:** +1. For each N, we have a representative g_N with StronglyMeasurable[m N] g_N and f =ᵐ[μ] g_N +2. For ℝ-valued functions, StronglyMeasurable ↔ Measurable (via Measurable.stronglyMeasurable) +3. If f is Measurable[m N] for each N, then f is Measurable[⨅ N, m N] (by measurableSet_iInf) +4. Hence f is StronglyMeasurable[⨅ N, m N], giving AEStronglyMeasurable + +The technical challenge is constructing a common representative from the a.e.-equal witnesses. +-/ +@[nolint unusedArguments] +lemma aestronglyMeasurable_iInf_antitone + {α : Type*} {m₀ : MeasurableSpace α} {μ : @MeasureTheory.Measure α m₀} + {m : ℕ → MeasurableSpace α} + (h_anti : Antitone m) + (_h_le : ∀ N, m N ≤ m₀) + (f : α → ℝ) + (hf : ∀ N, @MeasureTheory.AEStronglyMeasurable α ℝ _ (m N) m₀ f μ) : + @MeasureTheory.AEStronglyMeasurable α ℝ _ (⨅ N, m N) m₀ f μ := by + -- Step 1: Extract strongly measurable representatives for each N + let g : ℕ → α → ℝ := fun N => (hf N).mk f + have hg_sm : ∀ N, @MeasureTheory.StronglyMeasurable α ℝ _ (m N) (g N) := + fun N => (hf N).stronglyMeasurable_mk + have hg_meas : ∀ N, @Measurable α ℝ (m N) _ (g N) := fun N => (hg_sm N).measurable + have hg_ae : ∀ N, f =ᵐ[μ] g N := fun N => (hf N).ae_eq_mk + + -- Step 2: Define h as the liminf of the g N + let h : α → ℝ := fun x => Filter.liminf (fun N => g N x) Filter.atTop + + -- Step 3: Show h is Measurable[⨅ N, m N] + have h_meas_each : ∀ N, @Measurable α ℝ (m N) _ h := by + intro N + have h_shift : h = fun x => Filter.liminf (fun n => g (n + N) x) Filter.atTop := by + funext x + exact (Filter.liminf_nat_add (fun n => g n x) N).symm + rw [h_shift] + have hg_meas_shifted : ∀ n, @Measurable α ℝ (m N) _ (g (n + N)) := fun n => + Measurable.mono (hg_meas (n + N)) (h_anti (Nat.le_add_left N n)) le_rfl + haveI : MeasurableSpace α := m N + exact Measurable.liminf hg_meas_shifted + + have h_meas : @Measurable α ℝ (⨅ N, m N) _ h := by + intro s hs + rw [MeasurableSpace.measurableSet_iInf] + exact fun N => h_meas_each N hs + + -- Step 4: Show f =ᵐ h + have h_ae_eq : f =ᵐ[μ] h := by + have h_all_eq : ∀ᵐ x ∂μ, ∀ N, f x = g N x := by + rw [MeasureTheory.ae_all_iff] + exact hg_ae + filter_upwards [h_all_eq] with x hx + simp only [h] + have h_const : ∀ N, g N x = f x := fun N => (hx N).symm + simp_rw [h_const] + exact (Filter.liminf_const (f x)).symm + + -- Step 5: Convert Measurable to StronglyMeasurable (for ℝ) + have h_sm : @MeasureTheory.StronglyMeasurable α ℝ _ (⨅ N, m N) h := by + haveI : MeasurableSpace α := ⨅ N, m N + exact h_meas.stronglyMeasurable + + exact ⟨h, h_sm, h_ae_eq⟩ + +/-- AEStronglyMeasurable for a sub-σ-algebra is preserved under a.e. pointwise limits. + +If `f n` are all Measurable[m] where `m ≤ m₀`, and `f n → g` a.e. (wrt a measure on m₀), +then `g` is AEStronglyMeasurable[m] (with the witness being the limsup, which is Measurable[m]). + +This is the key lemma for "closedness" of L²[m] under L² limits: +we extract an a.e.-convergent subsequence and apply this. -/ +@[nolint unusedArguments] +lemma aestronglyMeasurable_sub_of_tendsto_ae + {α : Type*} {m₀ : MeasurableSpace α} {μ : @MeasureTheory.Measure α m₀} + {m : MeasurableSpace α} (_hm : m ≤ m₀) + {f : ℕ → α → ℝ} {g : α → ℝ} + (hf_meas : ∀ n, @Measurable α ℝ m _ (f n)) + (hlim : ∀ᵐ x ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) : + @MeasureTheory.AEStronglyMeasurable α ℝ _ m m₀ g μ := by + -- Strategy: construct h Measurable[m] with g =ᵐ[μ] h using limsup + let h := fun x => Filter.atTop.limsup (fun n => f n x) + have h_meas : @Measurable α ℝ m _ h := by + haveI : MeasurableSpace α := m + exact Measurable.limsup hf_meas + have h_ae_eq : h =ᵐ[μ] g := by + filter_upwards [hlim] with x hx + exact Filter.Tendsto.limsup_eq hx + have h_sm : @MeasureTheory.StronglyMeasurable α ℝ _ m h := by + haveI : MeasurableSpace α := m + exact h_meas.stronglyMeasurable + exact ⟨h, h_sm, h_ae_eq.symm⟩ From d62862b179a68e050538cd395052ec9acc7efff3 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 12:56:43 -0500 Subject: [PATCH 09/20] feat: Add ProductMeasurable to ForMathlib; update copyrights to 2026 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Batch 3 of ForMathlib extraction Phase 2: ForMathlib/Probability/Kernel/ProductMeasurable.lean: - measurable_prod_ennreal: product of measurable ENNReal functions - rectangles_isPiSystem: measurable rectangles form π-system - rectangles_generate_pi_sigma: product σ-algebra = generateFrom rectangles - measurable_measure_pi: key lemma for ConditionallyIID property Note: Conditional independence lemmas (CondIndep) not extracted due to project-specific dependencies on CondExpHelpers. The ProductMeasurable lemmas are the truly general-purpose content. Also updates copyright year to 2026 for new ForMathlib files. --- .../MeasureTheory/Function/LpHelpers.lean | 2 +- .../MeasurableSpace/SigmaAlgebraHelpers.lean | 2 +- .../Probability/Kernel/ProductMeasurable.lean | 151 ++++++++++++++++++ 3 files changed, 153 insertions(+), 2 deletions(-) create mode 100644 ForMathlib/Probability/Kernel/ProductMeasurable.lean diff --git a/ForMathlib/MeasureTheory/Function/LpHelpers.lean b/ForMathlib/MeasureTheory/Function/LpHelpers.lean index 61c6362f..6199a5f4 100644 --- a/ForMathlib/MeasureTheory/Function/LpHelpers.lean +++ b/ForMathlib/MeasureTheory/Function/LpHelpers.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2025 Cameron Freer. All rights reserved. +Copyright (c) 2026 Cameron Freer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Cameron Freer -/ diff --git a/ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean b/ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean index 04505d4e..27f4f0b7 100644 --- a/ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean +++ b/ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2025 Cameron Freer. All rights reserved. +Copyright (c) 2026 Cameron Freer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Cameron Freer -/ diff --git a/ForMathlib/Probability/Kernel/ProductMeasurable.lean b/ForMathlib/Probability/Kernel/ProductMeasurable.lean new file mode 100644 index 00000000..a18ae7e1 --- /dev/null +++ b/ForMathlib/Probability/Kernel/ProductMeasurable.lean @@ -0,0 +1,151 @@ +/- +Copyright (c) 2026 Cameron Freer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Cameron Freer +-/ +import Mathlib.MeasureTheory.Constructions.Pi +import Mathlib.MeasureTheory.PiSystem +import Mathlib.Probability.Kernel.Basic + +/-! +# Measurability of Product Measure Kernels + +This file contains technical lemmas about measurability of product measure kernels. +These lemmas support de Finetti-type theorems but are general-purpose results about +measure theory on product spaces. + +## Main Results + +* `measurable_prod_ennreal`: Products of measurable ENNReal functions are measurable +* `rectangles_isPiSystem`: Measurable rectangles form a π-system +* `rectangles_generate_pi_sigma`: Product σ-algebra = generateFrom of rectangles +* `measurable_measure_pi`: Measurability of product measure kernels ω ↦ ∏ᵢ ν ω + +## Mathematical Context + +The key technique is π-system induction: proving measurability on rectangles (a π-system) +and extending to all measurable sets via the π-λ theorem. + +## Suggested Mathlib Location + +`Mathlib.Probability.Kernel.Measurable` or `Mathlib.MeasureTheory.Constructions.Pi` + +## References + +* Kallenberg (2005), *Probabilistic Symmetries and Invariance Principles* +-/ + +noncomputable section +open scoped BigOperators MeasureTheory +open MeasureTheory ProbabilityTheory Set + +variable {Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpace α] + +/-! ### Preliminary lemmas -/ + +/-- The product of finitely many measurable ENNReal-valued functions is measurable. + +This is a wrapper around `Finset.measurable_prod` specialized to ENNReal. -/ +lemma measurable_prod_ennreal {ι : Type*} [Fintype ι] {Ω : Type*} [MeasurableSpace Ω] + (f : ι → Ω → ENNReal) (hf : ∀ i, Measurable (f i)) : + Measurable fun ω => ∏ i, f i ω := + Finset.measurable_prod _ fun i _ => hf i + +/-- Rewrite `Set.univ.pi B` as a setOf comprehension. -/ +lemma univ_pi_eq_setOf_forall {ι : Type*} {α : Type*} (B : ι → Set α) : + Set.univ.pi B = {x | ∀ i, x i ∈ B i} := by + ext x; simp [Set.pi] + +/-! ### π-system structure of rectangles -/ + +/-- Measurable rectangles form a π-system for the product σ-algebra. + +A rectangle in (Fin m → α) is a set of the form {x | ∀ i, x i ∈ B i} where each B i +is measurable. The collection of such rectangles is closed under finite intersections. -/ +lemma rectangles_isPiSystem {m : ℕ} {α : Type*} [MeasurableSpace α] : + IsPiSystem {S : Set (Fin m → α) | ∃ (B : Fin m → Set α), + (∀ i, MeasurableSet (B i)) ∧ S = {x | ∀ i, x i ∈ B i}} := by + intro S₁ hS₁ S₂ hS₂ _hne + obtain ⟨B₁, hB₁_meas, rfl⟩ := hS₁ + obtain ⟨B₂, hB₂_meas, rfl⟩ := hS₂ + use fun i => B₁ i ∩ B₂ i + constructor + · exact fun i => (hB₁_meas i).inter (hB₂_meas i) + · ext x + simp only [Set.mem_inter_iff, Set.mem_setOf_eq] + exact ⟨fun ⟨h₁, h₂⟩ i => ⟨h₁ i, h₂ i⟩, fun h => ⟨fun i => (h i).1, fun i => (h i).2⟩⟩ + +/-- The product σ-algebra on (Fin m → α) is generated by measurable rectangles. + +This is a fundamental result in product measure theory: the σ-algebra on a finite +product equals the σ-algebra generated by measurable rectangles. -/ +lemma rectangles_generate_pi_sigma {m : ℕ} {α : Type*} [MeasurableSpace α] : + (inferInstance : MeasurableSpace (Fin m → α)) = + MeasurableSpace.generateFrom {S : Set (Fin m → α) | ∃ (B : Fin m → Set α), + (∀ i, MeasurableSet (B i)) ∧ S = {x | ∀ i, x i ∈ B i}} := by + have set_eq : {S : Set (Fin m → α) | ∃ (B : Fin m → Set α), + (∀ i, MeasurableSet (B i)) ∧ S = {x | ∀ i, x i ∈ B i}} = + Set.pi univ '' Set.pi univ fun i : Fin m => {s : Set α | MeasurableSet s} := by + ext S + constructor + · intro ⟨B, hB_meas, hS⟩ + use fun i => B i + simp only [Set.mem_pi] + exact ⟨fun i _ => hB_meas i, by rw [univ_pi_eq_setOf_forall]; exact hS.symm⟩ + · intro ⟨B, hB_mem, hS⟩ + simp only [Set.mem_pi, Set.mem_univ, Set.mem_setOf_eq] at hB_mem hS + use B + exact ⟨fun i => hB_mem i (Set.mem_univ i), by rw [← univ_pi_eq_setOf_forall]; exact hS.symm⟩ + rw [set_eq] + exact generateFrom_pi.symm + +/-! ### Measurability of product measure kernels -/ + +/-- The product measure kernel ω ↦ Measure.pi (fun _ => ν ω) is measurable. + +Given a measurable family of probability measures ν : Ω → Measure α, the product +kernel ω ↦ ∏ᵢ ν ω (where i ranges over Fin m) is measurable as a measure-valued map. + +**Proof strategy**: Use π-system induction on rectangles: +1. Rectangles generate the product σ-algebra (`rectangles_generate_pi_sigma`) +2. Rectangles form a π-system (`rectangles_isPiSystem`) +3. On rectangles, the product measure of {x | ∀ i, x i ∈ B i} equals ∏ᵢ ν ω (B i), + which is measurable in ω by `measurable_prod_ennreal` +4. By the π-λ theorem, measurability on the generating π-system extends to all measurable sets + +This is a key lemma for proving the ConditionallyIID property in de Finetti's theorem. -/ +lemma measurable_measure_pi {Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpace α] + {m : ℕ} + (ν : Ω → Measure α) (hν_prob : ∀ ω, IsProbabilityMeasure (ν ω)) + (hν_meas : ∀ s, MeasurableSet s → Measurable (fun ω => ν ω s)) : + Measurable fun ω => Measure.pi fun _ : Fin m => ν ω := by + classical + let κ : Ω → Measure (Fin m → α) := fun ω => Measure.pi fun _ : Fin m => ν ω + let 𝒞 : Set (Set (Fin m → α)) := + {S | ∃ (B : Fin m → Set α), (∀ i, MeasurableSet (B i)) ∧ S = {x | ∀ i, x i ∈ B i}} + + have h_gen : (inferInstance : MeasurableSpace (Fin m → α)) = MeasurableSpace.generateFrom 𝒞 := + rectangles_generate_pi_sigma (m := m) (α := α) + have h_pi : IsPiSystem 𝒞 := rectangles_isPiSystem (m := m) (α := α) + + -- Values on rectangles are measurable + have h_basic : ∀ t ∈ 𝒞, Measurable fun ω => κ ω t := by + intro t ht + rcases ht with ⟨B, hB, rfl⟩ + have rect : (fun ω => κ ω {x : Fin m → α | ∀ i, x i ∈ B i}) = fun ω => ∏ i : Fin m, ν ω (B i) := + by funext ω + have : {x : Fin m → α | ∀ i, x i ∈ B i} = Set.univ.pi B := by ext; simp [Set.pi] + simp only [κ, this, Measure.pi_pi] + have hmeas : Measurable fun ω => ∏ i : Fin m, ν ω (B i) := + measurable_prod_ennreal (fun i ω => ν ω (B i)) (fun i => hν_meas (B i) (hB i)) + simpa [κ, rect] + + -- Each product measure is a probability measure + haveI hκ_prob : ∀ ω, IsProbabilityMeasure (κ ω) := by + intro ω + haveI : ∀ i : Fin m, IsProbabilityMeasure (ν ω) := fun _ => hν_prob ω + infer_instance + + -- Apply π-λ theorem + exact Measurable.measure_of_isPiSystem_of_isProbabilityMeasure h_gen h_pi h_basic + From 7dc96ae555d6bd15dee53996d12454289a8e1d2e Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 12:58:50 -0500 Subject: [PATCH 10/20] docs: Update ForMathlib README with extraction status Update tracking table and module summaries for Phase 2 extraction: - LpHelpers.lean: Lp norm/integral bridges - SigmaAlgebraHelpers.lean: AEStronglyMeasurable for infima - ProductMeasurable.lean: Product measure kernel measurability --- ForMathlib/README.md | 71 +++++++++++++++++++++++++++++++------------- 1 file changed, 51 insertions(+), 20 deletions(-) diff --git a/ForMathlib/README.md b/ForMathlib/README.md index de1e2b64..9fdfce2c 100644 --- a/ForMathlib/README.md +++ b/ForMathlib/README.md @@ -12,6 +12,9 @@ organized for potential contribution to [mathlib4](https://github.com/leanprover | π-system/cylinder infrastructure | `MeasureTheory/Constructions/Pi/Cylinders.lean` | ✅ Extracted | Standard | - | | `sigmaFinite_trim` | `MeasureTheory/Measure/TrimInstances.lean` | ✅ Existing | Standard | - | | `condExp_L1_lipschitz` | `MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean` | ✅ Extracted | Standard | - | +| Lp/integration helpers | `MeasureTheory/Function/LpHelpers.lean` | ✅ Extracted | Standard | - | +| σ-algebra helpers | `MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean` | ✅ Extracted | Standard | - | +| Product kernel measurability | `Probability/Kernel/ProductMeasurable.lean` | ✅ Extracted | Standard | - | All extracted files: - Import only mathlib (no `Exchangeability.*` dependencies) @@ -19,23 +22,6 @@ All extracted files: - Follow mathlib style (<100 char lines) - Include module docstrings with mathematical context -## PR Sequencing Strategy - -``` -Level 0 (independent - can be submitted in parallel): - PR1: PermutationExtension - pure combinatorics, no measure theory - PR2: ComapInfima - σ-algebra infrastructure - PR3: TrimInstances - already essentially in mathlib - -Level 1 (after Level 0): - PR4: Cylinders - uses ComapInfima patterns, π-system infrastructure - PR5: CondExp helpers - missing API additions - -Level 2 (after Level 1): - PR6: TailSigmaAlgebra - uses ComapInfima, Cylinders - PR7: FinMarginals - uses Cylinders -``` - ## Directory Structure ``` @@ -44,18 +30,62 @@ ForMathlib/ │ └── PermutationExtension.lean # exists_perm_extending_strictMono ├── MeasureTheory/ │ ├── MeasurableSpace/ -│ │ └── ComapInfima.lean # iInf_comap_eq_comap_iInf_of_surjective +│ │ ├── ComapInfima.lean # iInf_comap_eq_comap_iInf_of_surjective +│ │ └── SigmaAlgebraHelpers.lean # aestronglyMeasurable_iInf_antitone │ ├── Constructions/ │ │ └── Pi/ │ │ └── Cylinders.lean # π-system, measure_eq_of_fin_marginals_eq │ ├── Measure/ │ │ └── TrimInstances.lean # sigmaFinite_trim (existing) │ └── Function/ -│ └── ConditionalExpectation/ -│ └── Lipschitz.lean # condExp_L1_lipschitz +│ ├── ConditionalExpectation/ +│ │ └── Lipschitz.lean # condExp_L1_lipschitz +│ └── LpHelpers.lean # eLpNorm_two_sq_eq_integral_sq, abs_integral_mul_le_L2 +├── Probability/ +│ └── Kernel/ +│ └── ProductMeasurable.lean # measurable_measure_pi, rectangles_isPiSystem └── README.md # This file ``` +## PR Sequencing Strategy + +``` +Level 0 (independent - can be submitted in parallel): + PR1: PermutationExtension - pure combinatorics, no measure theory + PR2: ComapInfima - σ-algebra infrastructure + PR3: TrimInstances - already essentially in mathlib + +Level 1 (after Level 0): + PR4: Cylinders - uses ComapInfima patterns, π-system infrastructure + PR5: Lipschitz - conditional expectation helpers + PR6: LpHelpers - Lp norm/integral bridges + PR7: SigmaAlgebraHelpers - AEStronglyMeasurable for infima + +Level 2 (after Level 1): + PR8: ProductMeasurable - uses π-system infrastructure from Cylinders +``` + +## Module Summaries + +### MeasureTheory/Function/LpHelpers.lean +Bridges ENNReal-valued Lp norms and Real-valued integrals: +- `eLpNorm_two_sq_eq_integral_sq`: L² norm² = integral of square +- `eLpNorm_lt_of_integral_sq_lt`: integral bound → norm bound +- `abs_integral_mul_le_L2`: Cauchy-Schwarz for L² functions +- `L2_tendsto_implies_L1_tendsto_of_bounded`: L² → L¹ convergence +- `setIntegral_le_eLpNorm_mul_measure`: |∫_A g| ≤ ‖g‖₂·√(μ A) + +### MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean +Support for AEStronglyMeasurable with respect to infima: +- `aestronglyMeasurable_iInf_antitone`: preservation under antitone infima +- `aestronglyMeasurable_sub_of_tendsto_ae`: preservation under a.e. limits + +### Probability/Kernel/ProductMeasurable.lean +Measurability of product measure kernels: +- `rectangles_isPiSystem`: measurable rectangles form a π-system +- `rectangles_generate_pi_sigma`: product σ-algebra = generateFrom of rectangles +- `measurable_measure_pi`: ω ↦ ∏ᵢ ν(ω) is measurable + ## Contribution Guidelines Each ForMathlib file should: @@ -70,4 +100,5 @@ Each ForMathlib file should: ## References - Kallenberg (2005), *Probabilistic Symmetries and Invariance Principles*, Theorem 1.1 +- Williams (1991), *Probability with Martingales* - Mathlib documentation: https://leanprover-community.github.io/mathlib4_docs/ From b0099ca720afc88fb421f84b20917da71e75831b Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 13:42:25 -0500 Subject: [PATCH 11/20] golf: Use isPiSystem_pi and generateFrom_pi from mathlib Replace custom rectangles_isPiSystem and rectangles_generate_pi_sigma with mathlib's isPiSystem_pi and generateFrom_pi from MeasurableSpace.Pi. Also remove unneeded univ_pi_eq_setOf_forall helper. --- .../Probability/Kernel/ProductMeasurable.lean | 77 ++++--------------- 1 file changed, 15 insertions(+), 62 deletions(-) diff --git a/ForMathlib/Probability/Kernel/ProductMeasurable.lean b/ForMathlib/Probability/Kernel/ProductMeasurable.lean index a18ae7e1..22b968e7 100644 --- a/ForMathlib/Probability/Kernel/ProductMeasurable.lean +++ b/ForMathlib/Probability/Kernel/ProductMeasurable.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Cameron Freer -/ import Mathlib.MeasureTheory.Constructions.Pi +import Mathlib.MeasureTheory.MeasurableSpace.Pi import Mathlib.MeasureTheory.PiSystem import Mathlib.Probability.Kernel.Basic @@ -17,14 +18,15 @@ measure theory on product spaces. ## Main Results * `measurable_prod_ennreal`: Products of measurable ENNReal functions are measurable -* `rectangles_isPiSystem`: Measurable rectangles form a π-system -* `rectangles_generate_pi_sigma`: Product σ-algebra = generateFrom of rectangles * `measurable_measure_pi`: Measurability of product measure kernels ω ↦ ∏ᵢ ν ω ## Mathematical Context The key technique is π-system induction: proving measurability on rectangles (a π-system) -and extending to all measurable sets via the π-λ theorem. +and extending to all measurable sets via the π-λ theorem. The π-system and generating +results come from `Mathlib.MeasureTheory.MeasurableSpace.Pi`: +* `isPiSystem_pi`: Measurable rectangles form a π-system +* `generateFrom_pi`: Product σ-algebra = generateFrom of rectangles ## Suggested Mathlib Location @@ -51,54 +53,6 @@ lemma measurable_prod_ennreal {ι : Type*} [Fintype ι] {Ω : Type*} [Measurable Measurable fun ω => ∏ i, f i ω := Finset.measurable_prod _ fun i _ => hf i -/-- Rewrite `Set.univ.pi B` as a setOf comprehension. -/ -lemma univ_pi_eq_setOf_forall {ι : Type*} {α : Type*} (B : ι → Set α) : - Set.univ.pi B = {x | ∀ i, x i ∈ B i} := by - ext x; simp [Set.pi] - -/-! ### π-system structure of rectangles -/ - -/-- Measurable rectangles form a π-system for the product σ-algebra. - -A rectangle in (Fin m → α) is a set of the form {x | ∀ i, x i ∈ B i} where each B i -is measurable. The collection of such rectangles is closed under finite intersections. -/ -lemma rectangles_isPiSystem {m : ℕ} {α : Type*} [MeasurableSpace α] : - IsPiSystem {S : Set (Fin m → α) | ∃ (B : Fin m → Set α), - (∀ i, MeasurableSet (B i)) ∧ S = {x | ∀ i, x i ∈ B i}} := by - intro S₁ hS₁ S₂ hS₂ _hne - obtain ⟨B₁, hB₁_meas, rfl⟩ := hS₁ - obtain ⟨B₂, hB₂_meas, rfl⟩ := hS₂ - use fun i => B₁ i ∩ B₂ i - constructor - · exact fun i => (hB₁_meas i).inter (hB₂_meas i) - · ext x - simp only [Set.mem_inter_iff, Set.mem_setOf_eq] - exact ⟨fun ⟨h₁, h₂⟩ i => ⟨h₁ i, h₂ i⟩, fun h => ⟨fun i => (h i).1, fun i => (h i).2⟩⟩ - -/-- The product σ-algebra on (Fin m → α) is generated by measurable rectangles. - -This is a fundamental result in product measure theory: the σ-algebra on a finite -product equals the σ-algebra generated by measurable rectangles. -/ -lemma rectangles_generate_pi_sigma {m : ℕ} {α : Type*} [MeasurableSpace α] : - (inferInstance : MeasurableSpace (Fin m → α)) = - MeasurableSpace.generateFrom {S : Set (Fin m → α) | ∃ (B : Fin m → Set α), - (∀ i, MeasurableSet (B i)) ∧ S = {x | ∀ i, x i ∈ B i}} := by - have set_eq : {S : Set (Fin m → α) | ∃ (B : Fin m → Set α), - (∀ i, MeasurableSet (B i)) ∧ S = {x | ∀ i, x i ∈ B i}} = - Set.pi univ '' Set.pi univ fun i : Fin m => {s : Set α | MeasurableSet s} := by - ext S - constructor - · intro ⟨B, hB_meas, hS⟩ - use fun i => B i - simp only [Set.mem_pi] - exact ⟨fun i _ => hB_meas i, by rw [univ_pi_eq_setOf_forall]; exact hS.symm⟩ - · intro ⟨B, hB_mem, hS⟩ - simp only [Set.mem_pi, Set.mem_univ, Set.mem_setOf_eq] at hB_mem hS - use B - exact ⟨fun i => hB_mem i (Set.mem_univ i), by rw [← univ_pi_eq_setOf_forall]; exact hS.symm⟩ - rw [set_eq] - exact generateFrom_pi.symm - /-! ### Measurability of product measure kernels -/ /-- The product measure kernel ω ↦ Measure.pi (fun _ => ν ω) is measurable. @@ -107,9 +61,9 @@ Given a measurable family of probability measures ν : Ω → Measure α, the pr kernel ω ↦ ∏ᵢ ν ω (where i ranges over Fin m) is measurable as a measure-valued map. **Proof strategy**: Use π-system induction on rectangles: -1. Rectangles generate the product σ-algebra (`rectangles_generate_pi_sigma`) -2. Rectangles form a π-system (`rectangles_isPiSystem`) -3. On rectangles, the product measure of {x | ∀ i, x i ∈ B i} equals ∏ᵢ ν ω (B i), +1. Rectangles generate the product σ-algebra (`generateFrom_pi`) +2. Rectangles form a π-system (`isPiSystem_pi`) +3. On rectangles, the product measure of `univ.pi B` equals ∏ᵢ ν ω (B i), which is measurable in ω by `measurable_prod_ennreal` 4. By the π-λ theorem, measurability on the generating π-system extends to all measurable sets @@ -122,20 +76,19 @@ lemma measurable_measure_pi {Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpac classical let κ : Ω → Measure (Fin m → α) := fun ω => Measure.pi fun _ : Fin m => ν ω let 𝒞 : Set (Set (Fin m → α)) := - {S | ∃ (B : Fin m → Set α), (∀ i, MeasurableSet (B i)) ∧ S = {x | ∀ i, x i ∈ B i}} + Set.pi univ '' Set.pi univ fun _ : Fin m => {s : Set α | MeasurableSet s} have h_gen : (inferInstance : MeasurableSpace (Fin m → α)) = MeasurableSpace.generateFrom 𝒞 := - rectangles_generate_pi_sigma (m := m) (α := α) - have h_pi : IsPiSystem 𝒞 := rectangles_isPiSystem (m := m) (α := α) + generateFrom_pi.symm + have h_pi : IsPiSystem 𝒞 := isPiSystem_pi -- Values on rectangles are measurable have h_basic : ∀ t ∈ 𝒞, Measurable fun ω => κ ω t := by intro t ht - rcases ht with ⟨B, hB, rfl⟩ - have rect : (fun ω => κ ω {x : Fin m → α | ∀ i, x i ∈ B i}) = fun ω => ∏ i : Fin m, ν ω (B i) := - by funext ω - have : {x : Fin m → α | ∀ i, x i ∈ B i} = Set.univ.pi B := by ext; simp [Set.pi] - simp only [κ, this, Measure.pi_pi] + obtain ⟨B, hB, rfl⟩ := ht + simp only [mem_pi, mem_univ, mem_setOf_eq, true_implies] at hB + have rect : (fun ω => κ ω (Set.univ.pi B)) = fun ω => ∏ i : Fin m, ν ω (B i) := by + funext ω; simp only [κ, Measure.pi_pi] have hmeas : Measurable fun ω => ∏ i : Fin m, ν ω (B i) := measurable_prod_ennreal (fun i ω => ν ω (B i)) (fun i => hν_meas (B i) (hB i)) simpa [κ, rect] From 1415635be70a93c680aca6151666a269dee3c909 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 13:47:14 -0500 Subject: [PATCH 12/20] golf: Simplify condExp_mul_pullout using condExp_mul_of_stronglyMeasurable_right MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Use condExp_mul_of_stronglyMeasurable_right directly instead of condExp_stronglyMeasurable_mul_of_bound with double commutativity. This removes the need for SigmaFinite (μ.trim hm) and the TrimInstances import. --- .../Function/ConditionalExpectation/Lipschitz.lean | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean b/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean index b569c15d..d4414570 100644 --- a/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean +++ b/ForMathlib/MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean @@ -5,7 +5,6 @@ Authors: Cameron Freer -/ import Mathlib.MeasureTheory.Function.ConditionalExpectation.Real import Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut -import ForMathlib.MeasureTheory.Measure.TrimInstances /-! # Lipschitz Properties of Conditional Expectation @@ -115,11 +114,10 @@ theorem condExp_mul_pullout {Ω : Type*} {m₀ : MeasurableSpace Ω} {μ : Measu (hg_bd : ∃ C, ∀ ω, |g ω| ≤ C) : μ[f * g|m] =ᵐ[μ] fun ω => μ[f|m] ω * g ω := by obtain ⟨C, hC⟩ := hg_bd - haveI : SigmaFinite (μ.trim hm) := MeasureTheory.Measure.sigmaFinite_trim μ hm - have h := condExp_stronglyMeasurable_mul_of_bound hm hg_meas.stronglyMeasurable hf C - (ae_of_all μ fun ω => (Real.norm_eq_abs _).le.trans (hC ω)) - -- f * g = g * f pointwise, so apply mathlib's g·E[f|m] version and commute - exact (condExp_congr_ae (ae_of_all μ fun _ => mul_comm _ _)).trans - (h.trans (ae_of_all μ fun _ => mul_comm _ _)) + have hg_sm : StronglyMeasurable[m] g := hg_meas.stronglyMeasurable + have hfg : Integrable (f * g) μ := + hf.mul_bdd (hg_meas.mono hm le_rfl).aestronglyMeasurable + (ae_of_all μ fun ω => (Real.norm_eq_abs _).le.trans (hC ω)) + exact condExp_mul_of_stronglyMeasurable_right hg_sm hfg hf end CondExp From aaee56b08f2d0dd6954bccf4b95d29deb7fd6a41 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 13:53:30 -0500 Subject: [PATCH 13/20] golf: Use Equiv.ofInjective for e_cod in PermutationExtension Replace manual Classical.choose scaffolding with Equiv.ofInjective followed by Equiv.subtypeEquivRight to convert between range and existential predicate representations. --- .../Combinatorics/PermutationExtension.lean | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/ForMathlib/Combinatorics/PermutationExtension.lean b/ForMathlib/Combinatorics/PermutationExtension.lean index cbcf4cd0..c758ee99 100644 --- a/ForMathlib/Combinatorics/PermutationExtension.lean +++ b/ForMathlib/Combinatorics/PermutationExtension.lean @@ -80,24 +80,22 @@ theorem exists_perm_extending_strictMono (k : Fin m → ℕ) (hk_mono : StrictMono k) (hk_bound : ∀ i, k i < n) (hmn : m ≤ n) : ∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin m), (σ ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩).val = k i := by - classical let kFin : Fin m → Fin n := fun i => ⟨k i, hk_bound i⟩ - -- e_dom: first m elements of Fin n ≃ Fin m (using mathlib's Fin.castLEquiv) + -- e_dom: first m elements of Fin n ≃ Fin m let e_dom : {x : Fin n // (x : ℕ) < m} ≃ Fin m := (Fin.castLEquiv hmn).symm - -- e_cod: Fin m ≃ image of k (via strict monotonicity giving injectivity) + -- e_cod: Fin m ≃ range of kFin (via strict monotonicity giving injectivity) + have hk_inj : Function.Injective kFin := fun i j h => + hk_mono.injective (Fin.ext_iff.mp h) + let e_cod' : Fin m ≃ Set.range kFin := Equiv.ofInjective kFin hk_inj + -- Convert between range representation and existential predicate let e_cod : Fin m ≃ {x : Fin n // ∃ i : Fin m, x = kFin i} := - { toFun := fun i => ⟨kFin i, i, rfl⟩ - invFun := fun y => Classical.choose y.2 - left_inv := fun i => by - have h_spec := Classical.choose_spec (⟨i, rfl⟩ : ∃ j : Fin m, kFin i = kFin j) - exact hk_mono.injective (by simpa [kFin] using (Fin.ext_iff.mp h_spec).symm) - right_inv := fun ⟨_, hy⟩ => Subtype.ext (Classical.choose_spec hy).symm } + e_cod'.trans (Equiv.subtypeEquivRight fun x => by simp [Set.mem_range, eq_comm]) -- Compose and extend to full permutation let σ : Equiv.Perm (Fin n) := Equiv.extendSubtype (e_dom.trans e_cod) refine ⟨σ, fun i => ?_⟩ have h := Equiv.extendSubtype_apply_of_mem (e := e_dom.trans e_cod) (x := Fin.castLE hmn i) i.isLt - simp only [Equiv.trans_apply, kFin] at h + simp only [Equiv.trans_apply, e_cod, e_cod', Equiv.ofInjective_apply, kFin] at h exact congrArg Fin.val h end Combinatorics From ee848506d1729135d5e854ae85dacd023e0e6fea Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 13:53:36 -0500 Subject: [PATCH 14/20] fix: Add explicit argument to AEStronglyMeasurable.pow in LpHelpers Add explicit natural number argument to make type inference work correctly for the squared norm case. --- ForMathlib/MeasureTheory/Function/LpHelpers.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ForMathlib/MeasureTheory/Function/LpHelpers.lean b/ForMathlib/MeasureTheory/Function/LpHelpers.lean index 6199a5f4..51f1e35e 100644 --- a/ForMathlib/MeasureTheory/Function/LpHelpers.lean +++ b/ForMathlib/MeasureTheory/Function/LpHelpers.lean @@ -84,7 +84,7 @@ lemma eLpNorm_two_sq_eq_integral_sq [IsFiniteMeasure μ] {f : Ω → ℝ} (hf : rw [h_enorm_conv, ← integral_eq_lintegral_of_nonneg_ae] · congr 1; ext ω; exact h_norm_eq ω · exact ae_of_all _ fun _ => sq_nonneg _ - · exact AEStronglyMeasurable.pow hf.1.norm + · exact (AEStronglyMeasurable.pow hf.1.norm 2).congr (ae_of_all _ fun _ => rfl) /-- **L² norm bound from integral bound.** From 66271b20ca50b15efa79a8284d5378da496e9fe2 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 14:15:25 -0500 Subject: [PATCH 15/20] feat(ForMathlib): Phase 3 extraction - conditional independence and CE bridge lemmas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add three new ForMathlib files with general-purpose lemmas: 1. Probability/Independence/Conditional.lean - `condIndep_of_indicator_condexp_eq`: Doob's characterization of conditional independence (reverse direction) - projection property implies cond indep 2. MeasureTheory/Function/AEHelpers.lean - `finset_sum_ae_eq`: Combine finitely many a.e. equalities into sum equality 3. Probability/ConditionalExpectation/Distributional.lean - `condexp_indicator_eq_of_pair_law_eq`: If (Y,Z) and (Y',Z) have same law, then E[1_{Y∈B}|σ(Z)] = E[1_{Y'∈B}|σ(Z)] a.e. All files: - Import only mathlib (no Exchangeability.* dependencies) - Use only standard axioms (propext, Classical.choice, Quot.sound) - Follow mathlib style (<100 char lines) --- .../MeasureTheory/Function/AEHelpers.lean | 62 ++++++++ .../Distributional.lean | 143 ++++++++++++++++++ .../Probability/Independence/Conditional.lean | 134 ++++++++++++++++ ForMathlib/README.md | 26 +++- 4 files changed, 364 insertions(+), 1 deletion(-) create mode 100644 ForMathlib/MeasureTheory/Function/AEHelpers.lean create mode 100644 ForMathlib/Probability/ConditionalExpectation/Distributional.lean create mode 100644 ForMathlib/Probability/Independence/Conditional.lean diff --git a/ForMathlib/MeasureTheory/Function/AEHelpers.lean b/ForMathlib/MeasureTheory/Function/AEHelpers.lean new file mode 100644 index 00000000..edd67a14 --- /dev/null +++ b/ForMathlib/MeasureTheory/Function/AEHelpers.lean @@ -0,0 +1,62 @@ +/- +Copyright (c) 2025 Cameron Freer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Cameron Freer +-/ +import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic + +/-! +# Combining Finitely Many A.E. Equalities + +This file provides a utility lemma for combining finitely many a.e.-equalities +into an a.e.-equality of the finite sum. + +## Main Results + +* `finset_sum_ae_eq`: If each `f i` is a.e.-equal to `g i` on a finite index + set `s`, then the pointwise sums over `s` are a.e.-equal. + +## Mathematical Context + +This lemma is useful when combining conditional expectation equalities, as in +de Finetti-type theorems where we need to show that sums of conditional +expectations converge. The key technique is induction on the finite set, +using `EventuallyEq.fun_add` to combine equalities at each step. + +## Suggested Mathlib Location + +`Mathlib.MeasureTheory.Function.AEEqFun` or +`Mathlib.MeasureTheory.Function.AEHelpers` + +## References + +* Williams (1991), *Probability with Martingales*, §9 +-/ + +noncomputable section +open scoped MeasureTheory ENNReal BigOperators +open MeasureTheory ProbabilityTheory Set + +namespace MeasureTheory + +variable {α ι β : Type*} [MeasurableSpace α] {μ : Measure α} + +/-- **Combine finitely many a.e.-equalities into an a.e.-equality of the sum.** + +If each `f i` is a.e.-equal to `g i` on a finite index set `s`, then the +pointwise sums over `s` are a.e.-equal. Uses `EventuallyEq.fun_add` to +combine equalities. -/ +theorem finset_sum_ae_eq [AddCommMonoid β] + (s : Finset ι) (f g : ι → α → β) + (h : ∀ i ∈ s, f i =ᵐ[μ] g i) : + (fun ω => ∑ i ∈ s, f i ω) =ᵐ[μ] (fun ω => ∑ i ∈ s, g i ω) := by + classical + induction s using Finset.induction_on with + | empty => simp + | @insert a s' ha IH => + simpa [Finset.sum_insert, ha] using (h a (Finset.mem_insert_self _ _)).fun_add + (IH fun i hi => h i (Finset.mem_insert_of_mem hi)) + +end MeasureTheory + +end diff --git a/ForMathlib/Probability/ConditionalExpectation/Distributional.lean b/ForMathlib/Probability/ConditionalExpectation/Distributional.lean new file mode 100644 index 00000000..607797ee --- /dev/null +++ b/ForMathlib/Probability/ConditionalExpectation/Distributional.lean @@ -0,0 +1,143 @@ +/- +Copyright (c) 2025 Cameron Freer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Cameron Freer +-/ +import Mathlib.MeasureTheory.Function.ConditionalExpectation.Real + +/-! +# Conditional Expectation Equality from Distributional Equality + +This file provides the key bridge lemma connecting distributional equality +to conditional expectation equality. + +## Main Results + +* `condexp_indicator_eq_of_pair_law_eq`: If `(Y, Z)` and `(Y', Z)` have the + same joint distribution, then for any measurable set B: + ``` + E[1_{Y ∈ B} | σ(Z)] = E[1_{Y' ∈ B} | σ(Z)] a.e. + ``` + +## Mathematical Context + +This is a key bridge lemma for exchangeability proofs. The strategy is: +1. For any bounded h measurable w.r.t. σ(Z), the equality of joint distributions + implies `∫ 1_{Y ∈ B} · h ∘ Z dμ = ∫ 1_{Y' ∈ B} · h ∘ Z dμ` +2. This equality holds for all σ(Z)-measurable test functions h +3. By uniqueness of conditional expectation, the conditional expectations agree + +In the de Finetti theorem context, this is used with Y = X_m, Y' = X_k, +Z = shiftRV X (m+1), where the equality of joint distributions comes from +contractability. + +## Suggested Mathlib Location + +`Mathlib.Probability.ConditionalExpectation.Distributional` or +`Mathlib.MeasureTheory.Function.ConditionalExpectation.Distributional` + +## References + +* Kallenberg (2005), *Probabilistic Symmetries and Invariance Principles*, §1 +* Williams (1991), *Probability with Martingales*, §9.7 +-/ + +open MeasureTheory Filter Set Function +open scoped MeasureTheory ProbabilityTheory + +namespace ProbabilityTheory + +variable {Ω α β : Type*} [mΩ : MeasurableSpace Ω] + [MeasurableSpace α] [mβ : MeasurableSpace β] + +/-- **Conditional expectation bridge lemma.** + +If `(Y, Z)` and `(Y', Z)` have the same law, then for every measurable `B`, +``` +E[1_{Y ∈ B} | σ(Z)] = E[1_{Y' ∈ B} | σ(Z)] a.e. +``` + +**Proof strategy:** +1. For any bounded h measurable w.r.t. σ(Z), we have + `∫ 1_{Y ∈ B} · h ∘ Z dμ = ∫ 1_{Y' ∈ B} · h ∘ Z dμ` + by the equality of joint push-forward measures on rectangles B × E. + +2. This equality holds for all σ(Z)-measurable test functions h. + +3. By uniqueness of conditional expectation (`ae_eq_condExp_of_forall_setIntegral_eq`), + `E[1_{Y ∈ B} | σ(Z)] = E[1_{Y' ∈ B} | σ(Z)] a.e.` +-/ +theorem condexp_indicator_eq_of_pair_law_eq + {μ : Measure Ω} [IsFiniteMeasure μ] + (Y Y' : Ω → α) (Z : Ω → β) + (hY : Measurable Y) (hY' : Measurable Y') (hZ : Measurable Z) + (hpair : Measure.map (fun ω => (Y ω, Z ω)) μ + = Measure.map (fun ω => (Y' ω, Z ω)) μ) + {B : Set α} (hB : MeasurableSet B) : + μ[(Set.indicator B (fun _ => (1:ℝ))) ∘ Y | MeasurableSpace.comap Z mβ] + =ᵐ[μ] + μ[(Set.indicator B (fun _ => (1:ℝ))) ∘ Y' | MeasurableSpace.comap Z mβ] := by + classical + set f := (Set.indicator B (fun _ => (1:ℝ))) ∘ Y + set f' := (Set.indicator B (fun _ => (1:ℝ))) ∘ Y' + set mZ := MeasurableSpace.comap Z mβ + + have hmZ_le : mZ ≤ mΩ := by + intro s hs + rcases hs with ⟨E, hE, rfl⟩ + exact hZ hE + + have hf_int : Integrable f μ := (integrable_const (1:ℝ)).indicator (hY hB) + have hf'_int : Integrable f' μ := (integrable_const (1:ℝ)).indicator (hY' hB) + + refine (MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq + (hm := hmZ_le) + (f := f) + (g := μ[f' | mZ]) + (hf := hf_int) + (hg_int_finite := ?hg_int_finite) + (hg_eq := ?hg_eq) + (hgm := MeasureTheory.stronglyMeasurable_condExp.aestronglyMeasurable)).symm + + case hg_int_finite => + intro s _ _ + exact integrable_condExp.integrableOn + + case hg_eq => + intro A hA _ + obtain ⟨E, hE, rfl⟩ := hA + + have h_meas_eq : μ (Y ⁻¹' B ∩ Z ⁻¹' E) = μ (Y' ⁻¹' B ∩ Z ⁻¹' E) := by + have := congr_arg (fun ν => ν (B ×ˢ E)) hpair + simp only [Measure.map_apply (hY.prodMk hZ) (hB.prod hE), + Measure.map_apply (hY'.prodMk hZ) (hB.prod hE)] at this + simp only [Set.mk_preimage_prod] at this + exact this + + have h_lhs : ∫ ω in Z ⁻¹' E, f ω ∂μ = (μ (Y ⁻¹' B ∩ Z ⁻¹' E)).toReal := by + have hf_eq : f = (Y ⁻¹' B).indicator (fun _ => (1:ℝ)) := by + ext ω + simp only [f, Function.comp_apply, Set.indicator, Set.mem_preimage] + simp_rw [hf_eq, integral_indicator (hY hB)] + simp only [integral_const] + simp_rw [Measure.restrict_restrict (hY hB)] + simp only [smul_eq_mul, mul_one] + simp [Measure.real, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter] + + have h_rhs_ce : + ∫ ω in Z ⁻¹' E, μ[f' | mZ] ω ∂μ = ∫ ω in Z ⁻¹' E, f' ω ∂μ := + setIntegral_condExp hmZ_le hf'_int ⟨E, hE, rfl⟩ + + have h_rhs : ∫ ω in Z ⁻¹' E, f' ω ∂μ = (μ (Y' ⁻¹' B ∩ Z ⁻¹' E)).toReal := by + have hf'_eq : f' = (Y' ⁻¹' B).indicator (fun _ => (1:ℝ)) := by + ext ω + simp only [f', Function.comp_apply, Set.indicator, Set.mem_preimage] + simp_rw [hf'_eq, integral_indicator (hY' hB)] + simp only [integral_const] + simp_rw [Measure.restrict_restrict (hY' hB)] + simp only [smul_eq_mul, mul_one] + simp [Measure.real, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter] + + simp_rw [h_lhs, h_rhs_ce, h_rhs, h_meas_eq] + +end ProbabilityTheory diff --git a/ForMathlib/Probability/Independence/Conditional.lean b/ForMathlib/Probability/Independence/Conditional.lean new file mode 100644 index 00000000..74269ea7 --- /dev/null +++ b/ForMathlib/Probability/Independence/Conditional.lean @@ -0,0 +1,134 @@ +/- +Copyright (c) 2025 Cameron Freer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Cameron Freer +-/ +import Mathlib.Probability.Independence.Conditional +import Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut + +/-! +# Doob's Characterization of Conditional Independence + +This file provides a characterization of conditional independence via the +projection property of conditional expectation. + +## Main Results + +* `condIndep_of_indicator_condexp_eq`: **Doob's characterization** (reverse direction): + If for all H ∈ mH we have E[1_H | mF ⊔ mG] = E[1_H | mG] a.e., then mF and mH + are conditionally independent given mG. + +## Mathematical Context + +For σ-algebras 𝒻, 𝒢, ℋ, we have 𝒻 ⊥⊥_𝒢 ℋ if and only if +``` +P[H | 𝒻 ∨ 𝒢] = P[H | 𝒢] a.s. for all H ∈ ℋ +``` + +This characterization follows from the product formula in `condIndep_iff`: +- Forward direction: From the product formula, taking F = univ gives the + projection property +- Reverse direction (this file): The projection property implies the product + formula via uniqueness of conditional expectation + +Mathlib has `condIndep_iff` (equivalence via product formula), but this lemma +proves the reverse via a different route (projection property), which is +mathematically valuable. + +## Suggested Mathlib Location + +`Mathlib.Probability.Independence.Conditional` + +## References + +* Kallenberg (2005), *Probabilistic Symmetries and Invariance Principles*, §6.6 +* Folland (1999), *Real Analysis*, Theorem 6.18 (conditional independence) +-/ + +open MeasureTheory Filter Set Function +open scoped MeasureTheory ProbabilityTheory + +namespace ProbabilityTheory + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] + +/-- **Doob's characterization of conditional independence (reverse direction).** + +If for all H ∈ mH we have E[1_H | mF ⊔ mG] = E[1_H | mG] a.e., then mF and mH +are conditionally independent given mG. + +The proof uses: +1. Tower property from mG up to mF ⊔ mG +2. Pull-out property at the middle level (mF ⊔ mG) +3. The projection hypothesis to drop mF at the middle level +4. Pull-out property at the outer level (mG) +5. Chaining the equalities into the product formula -/ +theorem condIndep_of_indicator_condexp_eq + {μ : Measure Ω} [IsFiniteMeasure μ] + {mF mG mH : MeasurableSpace Ω} + (hmF : mF ≤ mΩ) (hmG : mG ≤ mΩ) (hmH : mH ≤ mΩ) + (h : ∀ H, MeasurableSet[mH] H → + μ[H.indicator (fun _ => (1 : ℝ)) | mF ⊔ mG] + =ᵐ[μ] μ[H.indicator (fun _ => (1 : ℝ)) | mG]) : + CondIndep mG mF mH hmG μ := by + classical + refine (condIndep_iff mG mF mH hmG hmF hmH μ).2 ?_ + intro tF tH htF htH + set f1 : Ω → ℝ := tF.indicator (fun _ : Ω => (1 : ℝ)) + set f2 : Ω → ℝ := tH.indicator (fun _ : Ω => (1 : ℝ)) + have hf1_int : Integrable f1 μ := (integrable_const (1 : ℝ)).indicator (hmF _ htF) + have hf2_int : Integrable f2 μ := (integrable_const (1 : ℝ)).indicator (hmH _ htH) + have hf1_aesm : AEStronglyMeasurable[mF ⊔ mG] f1 μ := + ((stronglyMeasurable_const.indicator htF).aestronglyMeasurable).mono + (le_sup_left : mF ≤ mF ⊔ mG) + have hProj : μ[f2 | mF ⊔ mG] =ᵐ[μ] μ[f2 | mG] := h tH htH + have h_tower : + μ[(fun ω => f1 ω * f2 ω) | mG] + =ᵐ[μ] μ[ μ[(fun ω => f1 ω * f2 ω) | mF ⊔ mG] | mG] := by + simpa using + (condExp_condExp_of_le (μ := μ) + (hm₁₂ := le_sup_right) + (hm₂ := sup_le hmF hmG) + (f := fun ω => f1 ω * f2 ω)).symm + have hf1f2_int : Integrable (fun ω => f1 ω * f2 ω) μ := by + have : (fun ω => f1 ω * f2 ω) = (tF ∩ tH).indicator (fun _ : Ω => (1 : ℝ)) := by + funext ω; by_cases h1 : ω ∈ tF <;> by_cases h2 : ω ∈ tH <;> + simp [f1, f2, Set.indicator, h1, h2, Set.mem_inter_iff] at * + rw [this] + exact (integrable_const (1 : ℝ) (μ := μ)).indicator + (MeasurableSet.inter (hmF _ htF) (hmH _ htH)) + have h_pull_middle : + μ[(fun ω => f1 ω * f2 ω) | mF ⊔ mG] + =ᵐ[μ] f1 * μ[f2 | mF ⊔ mG] := + condExp_mul_of_aestronglyMeasurable_left + (μ := μ) (m := mF ⊔ mG) + hf1_aesm + hf1f2_int + hf2_int + have h_middle_to_G : + μ[(fun ω => f1 ω * f2 ω) | mF ⊔ mG] + =ᵐ[μ] f1 * μ[f2 | mG] := + h_pull_middle.trans <| EventuallyEq.mul EventuallyEq.rfl hProj + have hf1_condexp_int : Integrable (f1 * μ[f2 | mG]) μ := by + have h_eq : f1 * μ[f2 | mG] = tF.indicator (fun ω => μ[f2 | mG] ω) := by + funext ω; by_cases hω : ω ∈ tF <;> simp [f1, Set.indicator, hω] + rw [h_eq] + exact (integrable_condExp (μ := μ) (m := mG) (f := f2)).indicator (hmF _ htF) + have h_pull_outer : + μ[f1 * μ[f2 | mG] | mG] + =ᵐ[μ] μ[f1 | mG] * μ[f2 | mG] := + condExp_mul_of_aestronglyMeasurable_right + (μ := μ) (m := mG) + (stronglyMeasurable_condExp (μ := μ) (m := mG) (f := f2)).aestronglyMeasurable + hf1_condexp_int + hf1_int + have h_prod : + μ[(fun ω => f1 ω * f2 ω) | mG] + =ᵐ[μ] μ[f1 | mG] * μ[f2 | mG] := + h_tower.trans (condExp_congr_ae h_middle_to_G |>.trans h_pull_outer) + have h_f1f2 : (fun ω => f1 ω * f2 ω) = (tF ∩ tH).indicator (fun _ => (1 : ℝ)) := by + funext ω; by_cases h1 : ω ∈ tF <;> by_cases h2 : ω ∈ tH <;> + simp [f1, f2, Set.indicator, h1, h2, Set.mem_inter_iff] at * + simpa [h_f1f2, f1, f2] using h_prod + +end ProbabilityTheory diff --git a/ForMathlib/README.md b/ForMathlib/README.md index 9fdfce2c..78e1e723 100644 --- a/ForMathlib/README.md +++ b/ForMathlib/README.md @@ -15,6 +15,9 @@ organized for potential contribution to [mathlib4](https://github.com/leanprover | Lp/integration helpers | `MeasureTheory/Function/LpHelpers.lean` | ✅ Extracted | Standard | - | | σ-algebra helpers | `MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean` | ✅ Extracted | Standard | - | | Product kernel measurability | `Probability/Kernel/ProductMeasurable.lean` | ✅ Extracted | Standard | - | +| `condIndep_of_indicator_condexp_eq` | `Probability/Independence/Conditional.lean` | ✅ Extracted | Standard | - | +| `finset_sum_ae_eq` | `MeasureTheory/Function/AEHelpers.lean` | ✅ Extracted | Standard | - | +| `condexp_indicator_eq_of_pair_law_eq` | `Probability/ConditionalExpectation/Distributional.lean` | ✅ Extracted | Standard | - | All extracted files: - Import only mathlib (no `Exchangeability.*` dependencies) @@ -40,8 +43,13 @@ ForMathlib/ │ └── Function/ │ ├── ConditionalExpectation/ │ │ └── Lipschitz.lean # condExp_L1_lipschitz +│ ├── AEHelpers.lean # finset_sum_ae_eq │ └── LpHelpers.lean # eLpNorm_two_sq_eq_integral_sq, abs_integral_mul_le_L2 ├── Probability/ +│ ├── Independence/ +│ │ └── Conditional.lean # condIndep_of_indicator_condexp_eq (Doob) +│ ├── ConditionalExpectation/ +│ │ └── Distributional.lean # condexp_indicator_eq_of_pair_law_eq │ └── Kernel/ │ └── ProductMeasurable.lean # measurable_measure_pi, rectangles_isPiSystem └── README.md # This file @@ -60,9 +68,12 @@ Level 1 (after Level 0): PR5: Lipschitz - conditional expectation helpers PR6: LpHelpers - Lp norm/integral bridges PR7: SigmaAlgebraHelpers - AEStronglyMeasurable for infima + PR8: AEHelpers - finset_sum_ae_eq utility Level 2 (after Level 1): - PR8: ProductMeasurable - uses π-system infrastructure from Cylinders + PR9: ProductMeasurable - uses π-system infrastructure from Cylinders + PR10: Independence/Conditional - Doob's characterization + PR11: ConditionalExpectation/Distributional - CE equality from dist equality ``` ## Module Summaries @@ -75,6 +86,10 @@ Bridges ENNReal-valued Lp norms and Real-valued integrals: - `L2_tendsto_implies_L1_tendsto_of_bounded`: L² → L¹ convergence - `setIntegral_le_eLpNorm_mul_measure`: |∫_A g| ≤ ‖g‖₂·√(μ A) +### MeasureTheory/Function/AEHelpers.lean +Utility for combining a.e. equalities: +- `finset_sum_ae_eq`: combine finitely many a.e. equalities into sum equality + ### MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean Support for AEStronglyMeasurable with respect to infima: - `aestronglyMeasurable_iInf_antitone`: preservation under antitone infima @@ -86,6 +101,15 @@ Measurability of product measure kernels: - `rectangles_generate_pi_sigma`: product σ-algebra = generateFrom of rectangles - `measurable_measure_pi`: ω ↦ ∏ᵢ ν(ω) is measurable +### Probability/Independence/Conditional.lean +Doob's characterization of conditional independence: +- `condIndep_of_indicator_condexp_eq`: projection property ⟹ conditional independence + +### Probability/ConditionalExpectation/Distributional.lean +Bridge from distributional equality to conditional expectation equality: +- `condexp_indicator_eq_of_pair_law_eq`: if (Y,Z) and (Y',Z) have same law, + then E[1_{Y∈B}|σ(Z)] = E[1_{Y'∈B}|σ(Z)] a.e. + ## Contribution Guidelines Each ForMathlib file should: From 5848f20c8cd2cd0c5a399b0e7d50ee3d56a2fc5c Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 14:30:40 -0500 Subject: [PATCH 16/20] golf: Simplify Phase 3 ForMathlib proofs Conditional.lean (118 lines, -17): - Use `inter_indicator_one` for indicator product formula - Cleaner proof structure with consistent naming Distributional.lean (117 lines, -26): - Use `hZ.comap_le` instead of manual comap proof - Streamlined integral calculations --- .../Distributional.lean | 86 +++++++----------- .../Probability/Independence/Conditional.lean | 88 ++++++++----------- 2 files changed, 66 insertions(+), 108 deletions(-) diff --git a/ForMathlib/Probability/ConditionalExpectation/Distributional.lean b/ForMathlib/Probability/ConditionalExpectation/Distributional.lean index 607797ee..040d69dc 100644 --- a/ForMathlib/Probability/ConditionalExpectation/Distributional.lean +++ b/ForMathlib/Probability/ConditionalExpectation/Distributional.lean @@ -81,63 +81,37 @@ theorem condexp_indicator_eq_of_pair_law_eq set f := (Set.indicator B (fun _ => (1:ℝ))) ∘ Y set f' := (Set.indicator B (fun _ => (1:ℝ))) ∘ Y' set mZ := MeasurableSpace.comap Z mβ - - have hmZ_le : mZ ≤ mΩ := by - intro s hs - rcases hs with ⟨E, hE, rfl⟩ - exact hZ hE - + have hmZ_le : mZ ≤ mΩ := hZ.comap_le have hf_int : Integrable f μ := (integrable_const (1:ℝ)).indicator (hY hB) have hf'_int : Integrable f' μ := (integrable_const (1:ℝ)).indicator (hY' hB) - - refine (MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq - (hm := hmZ_le) - (f := f) - (g := μ[f' | mZ]) - (hf := hf_int) - (hg_int_finite := ?hg_int_finite) - (hg_eq := ?hg_eq) - (hgm := MeasureTheory.stronglyMeasurable_condExp.aestronglyMeasurable)).symm - - case hg_int_finite => - intro s _ _ - exact integrable_condExp.integrableOn - - case hg_eq => - intro A hA _ - obtain ⟨E, hE, rfl⟩ := hA - - have h_meas_eq : μ (Y ⁻¹' B ∩ Z ⁻¹' E) = μ (Y' ⁻¹' B ∩ Z ⁻¹' E) := by - have := congr_arg (fun ν => ν (B ×ˢ E)) hpair - simp only [Measure.map_apply (hY.prodMk hZ) (hB.prod hE), - Measure.map_apply (hY'.prodMk hZ) (hB.prod hE)] at this - simp only [Set.mk_preimage_prod] at this - exact this - - have h_lhs : ∫ ω in Z ⁻¹' E, f ω ∂μ = (μ (Y ⁻¹' B ∩ Z ⁻¹' E)).toReal := by - have hf_eq : f = (Y ⁻¹' B).indicator (fun _ => (1:ℝ)) := by - ext ω - simp only [f, Function.comp_apply, Set.indicator, Set.mem_preimage] - simp_rw [hf_eq, integral_indicator (hY hB)] - simp only [integral_const] - simp_rw [Measure.restrict_restrict (hY hB)] - simp only [smul_eq_mul, mul_one] - simp [Measure.real, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter] - - have h_rhs_ce : - ∫ ω in Z ⁻¹' E, μ[f' | mZ] ω ∂μ = ∫ ω in Z ⁻¹' E, f' ω ∂μ := - setIntegral_condExp hmZ_le hf'_int ⟨E, hE, rfl⟩ - - have h_rhs : ∫ ω in Z ⁻¹' E, f' ω ∂μ = (μ (Y' ⁻¹' B ∩ Z ⁻¹' E)).toReal := by - have hf'_eq : f' = (Y' ⁻¹' B).indicator (fun _ => (1:ℝ)) := by - ext ω - simp only [f', Function.comp_apply, Set.indicator, Set.mem_preimage] - simp_rw [hf'_eq, integral_indicator (hY' hB)] - simp only [integral_const] - simp_rw [Measure.restrict_restrict (hY' hB)] - simp only [smul_eq_mul, mul_one] - simp [Measure.real, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter] - - simp_rw [h_lhs, h_rhs_ce, h_rhs, h_meas_eq] + refine (ae_eq_condExp_of_forall_setIntegral_eq hmZ_le hf_int + (fun _ _ _ => integrable_condExp.integrableOn) ?_ + stronglyMeasurable_condExp.aestronglyMeasurable).symm + intro A hA _ + obtain ⟨E, hE, rfl⟩ := hA + -- Key measure equality from distributional assumption + have h_meas_eq : μ (Y ⁻¹' B ∩ Z ⁻¹' E) = μ (Y' ⁻¹' B ∩ Z ⁻¹' E) := by + have := congr_arg (· (B ×ˢ E)) hpair + simp only [Measure.map_apply (hY.prodMk hZ) (hB.prod hE), + Measure.map_apply (hY'.prodMk hZ) (hB.prod hE), mk_preimage_prod] at this + exact this + -- LHS: ∫_{Z⁻¹(E)} f dμ = μ(Y⁻¹B ∩ Z⁻¹E) + have h_lhs : ∫ ω in Z ⁻¹' E, f ω ∂μ = (μ (Y ⁻¹' B ∩ Z ⁻¹' E)).toReal := by + have hf_eq : f = (Y ⁻¹' B).indicator (fun _ => (1:ℝ)) := by + ext ω; simp only [f, comp_apply, indicator, mem_preimage] + simp_rw [hf_eq, integral_indicator (hY hB), integral_const, + Measure.restrict_restrict (hY hB), smul_eq_mul, mul_one] + simp [Measure.real, Measure.restrict_apply, inter_comm] + -- RHS via CE property then integral + have h_rhs_ce : + ∫ ω in Z ⁻¹' E, μ[f' | mZ] ω ∂μ = ∫ ω in Z ⁻¹' E, f' ω ∂μ := + setIntegral_condExp hmZ_le hf'_int ⟨E, hE, rfl⟩ + have h_rhs : ∫ ω in Z ⁻¹' E, f' ω ∂μ = (μ (Y' ⁻¹' B ∩ Z ⁻¹' E)).toReal := by + have hf'_eq : f' = (Y' ⁻¹' B).indicator (fun _ => (1:ℝ)) := by + ext ω; simp only [f', comp_apply, indicator, mem_preimage] + simp_rw [hf'_eq, integral_indicator (hY' hB), integral_const, + Measure.restrict_restrict (hY' hB), smul_eq_mul, mul_one] + simp [Measure.real, Measure.restrict_apply, inter_comm] + simp_rw [h_lhs, h_rhs_ce, h_rhs, h_meas_eq] end ProbabilityTheory diff --git a/ForMathlib/Probability/Independence/Conditional.lean b/ForMathlib/Probability/Independence/Conditional.lean index 74269ea7..b85b5e79 100644 --- a/ForMathlib/Probability/Independence/Conditional.lean +++ b/ForMathlib/Probability/Independence/Conditional.lean @@ -74,61 +74,45 @@ theorem condIndep_of_indicator_condexp_eq classical refine (condIndep_iff mG mF mH hmG hmF hmH μ).2 ?_ intro tF tH htF htH - set f1 : Ω → ℝ := tF.indicator (fun _ : Ω => (1 : ℝ)) - set f2 : Ω → ℝ := tH.indicator (fun _ : Ω => (1 : ℝ)) - have hf1_int : Integrable f1 μ := (integrable_const (1 : ℝ)).indicator (hmF _ htF) - have hf2_int : Integrable f2 μ := (integrable_const (1 : ℝ)).indicator (hmH _ htH) + -- Indicator functions for tF and tH + set f1 : Ω → ℝ := tF.indicator 1 with hf1_def + set f2 : Ω → ℝ := tH.indicator 1 with hf2_def + -- Key: product of indicators equals indicator of intersection + have hf1f2 : f1 * f2 = (tF ∩ tH).indicator 1 := inter_indicator_one.symm + -- Integrability facts + have hf1_int : Integrable f1 μ := (integrable_const 1).indicator (hmF _ htF) + have hf2_int : Integrable f2 μ := (integrable_const 1).indicator (hmH _ htH) + have hf1f2_int : Integrable (f1 * f2) μ := by + rw [hf1f2]; exact (integrable_const 1).indicator (hmF _ htF |>.inter (hmH _ htH)) + -- f1 is AEStronglyMeasurable w.r.t. mF ⊔ mG have hf1_aesm : AEStronglyMeasurable[mF ⊔ mG] f1 μ := - ((stronglyMeasurable_const.indicator htF).aestronglyMeasurable).mono - (le_sup_left : mF ≤ mF ⊔ mG) + (stronglyMeasurable_const.indicator htF).aestronglyMeasurable.mono le_sup_left + -- Tower property: E[f1·f2 | mG] = E[E[f1·f2 | mF⊔mG] | mG] + have h_tower : μ[f1 * f2 | mG] =ᵐ[μ] μ[μ[f1 * f2 | mF ⊔ mG] | mG] := by + simpa using (condExp_condExp_of_le (hm₁₂ := le_sup_right) + (hm₂ := sup_le hmF hmG) (f := f1 * f2)).symm + -- Pull-out at middle level: E[f1·f2 | mF⊔mG] = f1 · E[f2 | mF⊔mG] + have h_pull_middle : μ[f1 * f2 | mF ⊔ mG] =ᵐ[μ] f1 * μ[f2 | mF ⊔ mG] := + condExp_mul_of_aestronglyMeasurable_left hf1_aesm hf1f2_int hf2_int + -- Projection hypothesis: E[f2 | mF⊔mG] = E[f2 | mG] have hProj : μ[f2 | mF ⊔ mG] =ᵐ[μ] μ[f2 | mG] := h tH htH - have h_tower : - μ[(fun ω => f1 ω * f2 ω) | mG] - =ᵐ[μ] μ[ μ[(fun ω => f1 ω * f2 ω) | mF ⊔ mG] | mG] := by - simpa using - (condExp_condExp_of_le (μ := μ) - (hm₁₂ := le_sup_right) - (hm₂ := sup_le hmF hmG) - (f := fun ω => f1 ω * f2 ω)).symm - have hf1f2_int : Integrable (fun ω => f1 ω * f2 ω) μ := by - have : (fun ω => f1 ω * f2 ω) = (tF ∩ tH).indicator (fun _ : Ω => (1 : ℝ)) := by - funext ω; by_cases h1 : ω ∈ tF <;> by_cases h2 : ω ∈ tH <;> - simp [f1, f2, Set.indicator, h1, h2, Set.mem_inter_iff] at * - rw [this] - exact (integrable_const (1 : ℝ) (μ := μ)).indicator - (MeasurableSet.inter (hmF _ htF) (hmH _ htH)) - have h_pull_middle : - μ[(fun ω => f1 ω * f2 ω) | mF ⊔ mG] - =ᵐ[μ] f1 * μ[f2 | mF ⊔ mG] := - condExp_mul_of_aestronglyMeasurable_left - (μ := μ) (m := mF ⊔ mG) - hf1_aesm - hf1f2_int - hf2_int - have h_middle_to_G : - μ[(fun ω => f1 ω * f2 ω) | mF ⊔ mG] - =ᵐ[μ] f1 * μ[f2 | mG] := - h_pull_middle.trans <| EventuallyEq.mul EventuallyEq.rfl hProj - have hf1_condexp_int : Integrable (f1 * μ[f2 | mG]) μ := by + -- Combine: E[f1·f2 | mF⊔mG] = f1 · E[f2 | mG] + have h_middle_to_G : μ[f1 * f2 | mF ⊔ mG] =ᵐ[μ] f1 * μ[f2 | mG] := + h_pull_middle.trans (EventuallyEq.mul EventuallyEq.rfl hProj) + -- Integrability of f1 · E[f2 | mG] + have hf1_cond_int : Integrable (f1 * μ[f2 | mG]) μ := by have h_eq : f1 * μ[f2 | mG] = tF.indicator (fun ω => μ[f2 | mG] ω) := by - funext ω; by_cases hω : ω ∈ tF <;> simp [f1, Set.indicator, hω] - rw [h_eq] - exact (integrable_condExp (μ := μ) (m := mG) (f := f2)).indicator (hmF _ htF) - have h_pull_outer : - μ[f1 * μ[f2 | mG] | mG] - =ᵐ[μ] μ[f1 | mG] * μ[f2 | mG] := + funext ω; by_cases hω : ω ∈ tF <;> simp [f1, indicator, hω] + rw [h_eq]; exact integrable_condExp.indicator (hmF _ htF) + -- Pull-out at outer level: E[f1 · E[f2|mG] | mG] = E[f1|mG] · E[f2|mG] + have h_pull_outer : μ[f1 * μ[f2 | mG] | mG] =ᵐ[μ] μ[f1 | mG] * μ[f2 | mG] := condExp_mul_of_aestronglyMeasurable_right - (μ := μ) (m := mG) - (stronglyMeasurable_condExp (μ := μ) (m := mG) (f := f2)).aestronglyMeasurable - hf1_condexp_int - hf1_int - have h_prod : - μ[(fun ω => f1 ω * f2 ω) | mG] - =ᵐ[μ] μ[f1 | mG] * μ[f2 | mG] := - h_tower.trans (condExp_congr_ae h_middle_to_G |>.trans h_pull_outer) - have h_f1f2 : (fun ω => f1 ω * f2 ω) = (tF ∩ tH).indicator (fun _ => (1 : ℝ)) := by - funext ω; by_cases h1 : ω ∈ tF <;> by_cases h2 : ω ∈ tH <;> - simp [f1, f2, Set.indicator, h1, h2, Set.mem_inter_iff] at * - simpa [h_f1f2, f1, f2] using h_prod + stronglyMeasurable_condExp.aestronglyMeasurable hf1_cond_int hf1_int + -- Chain: E[f1·f2 | mG] = E[f1|mG] · E[f2|mG] + have h_prod : μ[f1 * f2 | mG] =ᵐ[μ] μ[f1 | mG] * μ[f2 | mG] := + h_tower.trans ((condExp_congr_ae h_middle_to_G).trans h_pull_outer) + simp only [hf1f2, hf1_def, hf2_def, Pi.one_apply] at h_prod ⊢ + convert h_prod using 2 <;> ext ω <;> by_cases h1 : ω ∈ tF <;> by_cases h2 : ω ∈ tH <;> + simp [indicator, h1, h2, mem_inter_iff] end ProbabilityTheory From 3ee300a0542303f4f9235ba70f4b735f2712352a Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Sat, 24 Jan 2026 14:45:36 -0500 Subject: [PATCH 17/20] golf: Apply user suggestions to Phase 3 files Distributional.lean (107 lines, -10): - Use indicator_comp_right to rewrite indicator compositions - Use setIntegral_indicator + setIntegral_const for cleaner integral calculations - Remove duplicate proof structure AEHelpers.lean (59 lines, -3): - Replace heavy ConditionalExpectation.Basic import with MeasureSpace - Remove unused ENNReal, ProbabilityTheory, Set opens --- .../MeasureTheory/Function/AEHelpers.lean | 9 +-- .../Distributional.lean | 60 ++++++++----------- 2 files changed, 28 insertions(+), 41 deletions(-) diff --git a/ForMathlib/MeasureTheory/Function/AEHelpers.lean b/ForMathlib/MeasureTheory/Function/AEHelpers.lean index edd67a14..de0e045c 100644 --- a/ForMathlib/MeasureTheory/Function/AEHelpers.lean +++ b/ForMathlib/MeasureTheory/Function/AEHelpers.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 Cameron Freer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Cameron Freer -/ -import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic +import Mathlib.MeasureTheory.Measure.MeasureSpace /-! # Combining Finitely Many A.E. Equalities @@ -33,9 +33,8 @@ using `EventuallyEq.fun_add` to combine equalities at each step. * Williams (1991), *Probability with Martingales*, §9 -/ -noncomputable section -open scoped MeasureTheory ENNReal BigOperators -open MeasureTheory ProbabilityTheory Set +open scoped MeasureTheory BigOperators +open MeasureTheory namespace MeasureTheory @@ -58,5 +57,3 @@ theorem finset_sum_ae_eq [AddCommMonoid β] (IH fun i hi => h i (Finset.mem_insert_of_mem hi)) end MeasureTheory - -end diff --git a/ForMathlib/Probability/ConditionalExpectation/Distributional.lean b/ForMathlib/Probability/ConditionalExpectation/Distributional.lean index 040d69dc..b257e138 100644 --- a/ForMathlib/Probability/ConditionalExpectation/Distributional.lean +++ b/ForMathlib/Probability/ConditionalExpectation/Distributional.lean @@ -56,16 +56,6 @@ If `(Y, Z)` and `(Y', Z)` have the same law, then for every measurable `B`, ``` E[1_{Y ∈ B} | σ(Z)] = E[1_{Y' ∈ B} | σ(Z)] a.e. ``` - -**Proof strategy:** -1. For any bounded h measurable w.r.t. σ(Z), we have - `∫ 1_{Y ∈ B} · h ∘ Z dμ = ∫ 1_{Y' ∈ B} · h ∘ Z dμ` - by the equality of joint push-forward measures on rectangles B × E. - -2. This equality holds for all σ(Z)-measurable test functions h. - -3. By uniqueness of conditional expectation (`ae_eq_condExp_of_forall_setIntegral_eq`), - `E[1_{Y ∈ B} | σ(Z)] = E[1_{Y' ∈ B} | σ(Z)] a.e.` -/ theorem condexp_indicator_eq_of_pair_law_eq {μ : Measure Ω} [IsFiniteMeasure μ] @@ -74,17 +64,22 @@ theorem condexp_indicator_eq_of_pair_law_eq (hpair : Measure.map (fun ω => (Y ω, Z ω)) μ = Measure.map (fun ω => (Y' ω, Z ω)) μ) {B : Set α} (hB : MeasurableSet B) : - μ[(Set.indicator B (fun _ => (1:ℝ))) ∘ Y | MeasurableSpace.comap Z mβ] + μ[(indicator B (fun _ => (1:ℝ))) ∘ Y | MeasurableSpace.comap Z mβ] =ᵐ[μ] - μ[(Set.indicator B (fun _ => (1:ℝ))) ∘ Y' | MeasurableSpace.comap Z mβ] := by + μ[(indicator B (fun _ => (1:ℝ))) ∘ Y' | MeasurableSpace.comap Z mβ] := by classical - set f := (Set.indicator B (fun _ => (1:ℝ))) ∘ Y - set f' := (Set.indicator B (fun _ => (1:ℝ))) ∘ Y' + -- Rewrite indicator compositions as preimage indicators via indicator_comp_right + have hf_eq : (indicator B fun _ => (1:ℝ)) ∘ Y = (Y ⁻¹' B).indicator fun _ => (1:ℝ) := + funext fun _ => (indicator_comp_right Y).symm + have hf'_eq : (indicator B fun _ => (1:ℝ)) ∘ Y' = (Y' ⁻¹' B).indicator fun _ => (1:ℝ) := + funext fun _ => (indicator_comp_right Y').symm + simp_rw [hf_eq, hf'_eq] set mZ := MeasurableSpace.comap Z mβ - have hmZ_le : mZ ≤ mΩ := hZ.comap_le - have hf_int : Integrable f μ := (integrable_const (1:ℝ)).indicator (hY hB) - have hf'_int : Integrable f' μ := (integrable_const (1:ℝ)).indicator (hY' hB) - refine (ae_eq_condExp_of_forall_setIntegral_eq hmZ_le hf_int + have hf_int : Integrable ((Y ⁻¹' B).indicator fun _ => (1:ℝ)) μ := + (integrable_const 1).indicator (hY hB) + have hf'_int : Integrable ((Y' ⁻¹' B).indicator fun _ => (1:ℝ)) μ := + (integrable_const 1).indicator (hY' hB) + refine (ae_eq_condExp_of_forall_setIntegral_eq hZ.comap_le hf_int (fun _ _ _ => integrable_condExp.integrableOn) ?_ stronglyMeasurable_condExp.aestronglyMeasurable).symm intro A hA _ @@ -95,23 +90,18 @@ theorem condexp_indicator_eq_of_pair_law_eq simp only [Measure.map_apply (hY.prodMk hZ) (hB.prod hE), Measure.map_apply (hY'.prodMk hZ) (hB.prod hE), mk_preimage_prod] at this exact this - -- LHS: ∫_{Z⁻¹(E)} f dμ = μ(Y⁻¹B ∩ Z⁻¹E) - have h_lhs : ∫ ω in Z ⁻¹' E, f ω ∂μ = (μ (Y ⁻¹' B ∩ Z ⁻¹' E)).toReal := by - have hf_eq : f = (Y ⁻¹' B).indicator (fun _ => (1:ℝ)) := by - ext ω; simp only [f, comp_apply, indicator, mem_preimage] - simp_rw [hf_eq, integral_indicator (hY hB), integral_const, - Measure.restrict_restrict (hY hB), smul_eq_mul, mul_one] - simp [Measure.real, Measure.restrict_apply, inter_comm] - -- RHS via CE property then integral + -- LHS via setIntegral_indicator + setIntegral_const + have h_lhs : ∫ ω in Z ⁻¹' E, (Y ⁻¹' B).indicator (fun _ => (1:ℝ)) ω ∂μ = + μ.real (Y ⁻¹' B ∩ Z ⁻¹' E) := by + rw [setIntegral_indicator (hY hB), setIntegral_const, smul_eq_mul, mul_one, inter_comm] + -- RHS via CE property + setIntegral_indicator + setIntegral_const have h_rhs_ce : - ∫ ω in Z ⁻¹' E, μ[f' | mZ] ω ∂μ = ∫ ω in Z ⁻¹' E, f' ω ∂μ := - setIntegral_condExp hmZ_le hf'_int ⟨E, hE, rfl⟩ - have h_rhs : ∫ ω in Z ⁻¹' E, f' ω ∂μ = (μ (Y' ⁻¹' B ∩ Z ⁻¹' E)).toReal := by - have hf'_eq : f' = (Y' ⁻¹' B).indicator (fun _ => (1:ℝ)) := by - ext ω; simp only [f', comp_apply, indicator, mem_preimage] - simp_rw [hf'_eq, integral_indicator (hY' hB), integral_const, - Measure.restrict_restrict (hY' hB), smul_eq_mul, mul_one] - simp [Measure.real, Measure.restrict_apply, inter_comm] - simp_rw [h_lhs, h_rhs_ce, h_rhs, h_meas_eq] + ∫ ω in Z ⁻¹' E, μ[(Y' ⁻¹' B).indicator (fun _ => (1:ℝ)) | mZ] ω ∂μ = + ∫ ω in Z ⁻¹' E, (Y' ⁻¹' B).indicator (fun _ => (1:ℝ)) ω ∂μ := + setIntegral_condExp hZ.comap_le hf'_int ⟨E, hE, rfl⟩ + have h_rhs : ∫ ω in Z ⁻¹' E, (Y' ⁻¹' B).indicator (fun _ => (1:ℝ)) ω ∂μ = + μ.real (Y' ⁻¹' B ∩ Z ⁻¹' E) := by + rw [setIntegral_indicator (hY' hB), setIntegral_const, smul_eq_mul, mul_one, inter_comm] + rw [h_rhs_ce, h_rhs, h_lhs, Measure.real, Measure.real, h_meas_eq] end ProbabilityTheory From fc99eb1e84201a4895fee2738d103f1198b59de1 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Mon, 26 Jan 2026 12:19:00 -0500 Subject: [PATCH 18/20] cleanup: Remove nolint annotations and unused params from ForMathlib - SigmaAlgebraHelpers: Remove unused _h_le and _hm parameters - LpHelpers: Remove false positive nolint annotations, remove unused params from memLp_of_abs_le_const --- ForMathlib/MeasureTheory/Function/LpHelpers.lean | 7 ++----- .../MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean | 5 +---- 2 files changed, 3 insertions(+), 9 deletions(-) diff --git a/ForMathlib/MeasureTheory/Function/LpHelpers.lean b/ForMathlib/MeasureTheory/Function/LpHelpers.lean index 51f1e35e..ea018369 100644 --- a/ForMathlib/MeasureTheory/Function/LpHelpers.lean +++ b/ForMathlib/MeasureTheory/Function/LpHelpers.lean @@ -63,7 +63,6 @@ the integral of f²: This is a fundamental relationship used throughout probability theory, bridging the gap between ENNReal-valued Lp norms and Real-valued integrals. -/ -@[nolint unusedArguments] lemma eLpNorm_two_sq_eq_integral_sq [IsFiniteMeasure μ] {f : Ω → ℝ} (hf : MemLp f 2 μ) : (eLpNorm f 2 μ).toReal ^ 2 = ∫ ω, (f ω) ^ 2 ∂μ := by have h_norm_eq : ∀ ω, ‖f ω‖ ^ 2 = (f ω) ^ 2 := fun ω => by rw [Real.norm_eq_abs, sq_abs] @@ -105,9 +104,8 @@ lemma eLpNorm_lt_of_integral_sq_lt [IsFiniteMeasure μ] {f : Ω → ℝ} {r : /-- **Functions bounded by a constant are in Lp.** If |f| ≤ M almost everywhere, then f ∈ Lp for any p ∈ [1, ∞) on a finite measure space. -/ -@[nolint unusedArguments] lemma memLp_of_abs_le_const [IsFiniteMeasure μ] {f : Ω → ℝ} {M : ℝ} (hf_meas : Measurable f) - (hf_bdd : ∀ᵐ ω ∂μ, |f ω| ≤ M) (p : ℝ≥0∞) (_ : 1 ≤ p) (_ : p ≠ ∞) : MemLp f p μ := + (hf_bdd : ∀ᵐ ω ∂μ, |f ω| ≤ M) (p : ℝ≥0∞) : MemLp f p μ := MemLp.of_bound hf_meas.aestronglyMeasurable M (hf_bdd.mono fun _ hω => (Real.norm_eq_abs _).le.trans hω) @@ -116,7 +114,7 @@ lemma memLp_of_abs_le_const [IsFiniteMeasure μ] {f : Ω → ℝ} {M : ℝ} (hf_ Special case: If f is bounded by M, then f is in L² on a probability space. -/ lemma memLp_two_of_bounded [IsProbabilityMeasure μ] {f : Ω → ℝ} {M : ℝ} (hf_meas : Measurable f) (hf_bdd : ∀ ω, |f ω| ≤ M) : MemLp f 2 μ := - memLp_of_abs_le_const hf_meas (ae_of_all μ hf_bdd) 2 (by norm_num) (by norm_num) + memLp_of_abs_le_const hf_meas (ae_of_all μ hf_bdd) 2 /-! ### L² Inner Product Bounds -/ @@ -151,7 +149,6 @@ lemma setIntegral_le_eLpNorm_mul_measure [IsProbabilityMeasure μ] (A : Set Ω) For integrable functions f, g in L²(μ): |∫ f·g dμ| ≤ (∫ f² dμ)^(1/2) · (∫ g² dμ)^(1/2) -/ -@[nolint unusedArguments] lemma abs_integral_mul_le_L2 [IsFiniteMeasure μ] {f g : Ω → ℝ} (hf : MemLp f 2 μ) (hg : MemLp g 2 μ) : |∫ ω, f ω * g ω ∂μ| ≤ (∫ ω, (f ω) ^ 2 ∂μ) ^ (1/2 : ℝ) * (∫ ω, (g ω) ^ 2 ∂μ) ^ (1/2 : ℝ) := by diff --git a/ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean b/ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean index 27f4f0b7..23972fdb 100644 --- a/ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean +++ b/ForMathlib/MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean @@ -58,12 +58,10 @@ their infimum. The technical challenge is constructing a common representative from the a.e.-equal witnesses. -/ -@[nolint unusedArguments] lemma aestronglyMeasurable_iInf_antitone {α : Type*} {m₀ : MeasurableSpace α} {μ : @MeasureTheory.Measure α m₀} {m : ℕ → MeasurableSpace α} (h_anti : Antitone m) - (_h_le : ∀ N, m N ≤ m₀) (f : α → ℝ) (hf : ∀ N, @MeasureTheory.AEStronglyMeasurable α ℝ _ (m N) m₀ f μ) : @MeasureTheory.AEStronglyMeasurable α ℝ _ (⨅ N, m N) m₀ f μ := by @@ -119,10 +117,9 @@ then `g` is AEStronglyMeasurable[m] (with the witness being the limsup, which is This is the key lemma for "closedness" of L²[m] under L² limits: we extract an a.e.-convergent subsequence and apply this. -/ -@[nolint unusedArguments] lemma aestronglyMeasurable_sub_of_tendsto_ae {α : Type*} {m₀ : MeasurableSpace α} {μ : @MeasureTheory.Measure α m₀} - {m : MeasurableSpace α} (_hm : m ≤ m₀) + {m : MeasurableSpace α} {f : ℕ → α → ℝ} {g : α → ℝ} (hf_meas : ∀ n, @Measurable α ℝ m _ (f n)) (hlim : ∀ᵐ x ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) : From de9d9419b21e3f2f76491ae1b202c943c19f1f8c Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Mon, 26 Jan 2026 19:05:20 -0500 Subject: [PATCH 19/20] refactor(ForMathlib): Generalize lemmas for better mathlib compatibility - PermutationExtension: Create `exists_perm_extending_injective` as the main lemma using `Function.Injective k`, make `exists_perm_extending_strictMono` a corollary (proof only used injectivity, not order property) - ComapInfima: Generalize index type from `Type*` to `Sort*` in `iInf_comap_eq_comap_iInf_of_surjective` and helper lemmas, consistent with `comap_iInf_le` which already used `Sort*` --- .../Combinatorics/PermutationExtension.lean | 41 ++++++++++++------- .../MeasurableSpace/ComapInfima.lean | 8 ++-- 2 files changed, 30 insertions(+), 19 deletions(-) diff --git a/ForMathlib/Combinatorics/PermutationExtension.lean b/ForMathlib/Combinatorics/PermutationExtension.lean index c758ee99..40699c08 100644 --- a/ForMathlib/Combinatorics/PermutationExtension.lean +++ b/ForMathlib/Combinatorics/PermutationExtension.lean @@ -8,21 +8,23 @@ import Mathlib.Logic.Equiv.Fintype import Mathlib.GroupTheory.Perm.Basic /-! -# Permutation Extension for Strictly Monotone Functions +# Permutation Extension for Injective Functions -This file proves that any strictly increasing function `k : Fin m → ℕ` with bounded range +This file proves that any injective function `k : Fin m → ℕ` with bounded range can be extended to a permutation of `Fin n`. ## Main Results -* `exists_perm_extending_strictMono`: Given a strictly increasing `k : Fin m → ℕ` with all - values `< n` and `m ≤ n`, there exists a permutation `σ : Perm (Fin n)` such that - `σ(i) = k(i)` for all `i < m`. +* `exists_perm_extending_injective`: Given an injective `k : Fin m → ℕ` with all values `< n` + and `m ≤ n`, there exists a permutation `σ : Perm (Fin n)` such that `σ(i) = k(i)` for all + `i < m`. + +* `exists_perm_extending_strictMono`: The special case for strictly monotone functions. ## Mathematical Context This is a key combinatorial lemma in the proof that **exchangeability implies contractability** -for infinite sequences of random variables. The construction allows any strictly increasing +for infinite sequences of random variables. The construction allows any injective subsequence to be realized as the image of the first m coordinates under some permutation. **Intuition:** We partition both domain and codomain: @@ -60,9 +62,9 @@ lemma strictMono_Fin_ge_id {k : Fin m → ℕ} (hk : StrictMono k) (i : Fin m) : exact this i.val i.isLt /-- -Any strictly increasing function can be extended to a permutation. +Any injective function can be extended to a permutation. -**Statement:** Given a strictly increasing `k : Fin m → ℕ` with all values `< n` +**Statement:** Given an injective `k : Fin m → ℕ` with all values `< n` and `m ≤ n`, there exists a permutation `σ : Perm (Fin n)` such that `σ(i) = k(i)` for all `i < m`. @@ -73,20 +75,19 @@ and `m ≤ n`, there exists a permutation `σ : Perm (Fin n)` such that 4. Extend arbitrarily to remaining positions using `Equiv.extendSubtype` This is the key combinatorial lemma enabling the implication -**exchangeable → contractable**: any strictly increasing subsequence can be +**exchangeable → contractable**: any injective subsequence can be realized via a permutation. -/ -theorem exists_perm_extending_strictMono (k : Fin m → ℕ) - (hk_mono : StrictMono k) (hk_bound : ∀ i, k i < n) (hmn : m ≤ n) : +theorem exists_perm_extending_injective (k : Fin m → ℕ) + (hk_inj : Function.Injective k) (hk_bound : ∀ i, k i < n) (hmn : m ≤ n) : ∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin m), (σ ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩).val = k i := by let kFin : Fin m → Fin n := fun i => ⟨k i, hk_bound i⟩ -- e_dom: first m elements of Fin n ≃ Fin m let e_dom : {x : Fin n // (x : ℕ) < m} ≃ Fin m := (Fin.castLEquiv hmn).symm - -- e_cod: Fin m ≃ range of kFin (via strict monotonicity giving injectivity) - have hk_inj : Function.Injective kFin := fun i j h => - hk_mono.injective (Fin.ext_iff.mp h) - let e_cod' : Fin m ≃ Set.range kFin := Equiv.ofInjective kFin hk_inj + -- e_cod: Fin m ≃ range of kFin (via injectivity) + have hkFin_inj : Function.Injective kFin := fun i j h => hk_inj (Fin.ext_iff.mp h) + let e_cod' : Fin m ≃ Set.range kFin := Equiv.ofInjective kFin hkFin_inj -- Convert between range representation and existential predicate let e_cod : Fin m ≃ {x : Fin n // ∃ i : Fin m, x = kFin i} := e_cod'.trans (Equiv.subtypeEquivRight fun x => by simp [Set.mem_range, eq_comm]) @@ -98,4 +99,14 @@ theorem exists_perm_extending_strictMono (k : Fin m → ℕ) simp only [Equiv.trans_apply, e_cod, e_cod', Equiv.ofInjective_apply, kFin] at h exact congrArg Fin.val h +/-- Any strictly increasing function can be extended to a permutation. + +This is a corollary of `exists_perm_extending_injective` since strict monotonicity +implies injectivity. -/ +theorem exists_perm_extending_strictMono (k : Fin m → ℕ) + (hk_mono : StrictMono k) (hk_bound : ∀ i, k i < n) (hmn : m ≤ n) : + ∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin m), + (σ ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩).val = k i := + exists_perm_extending_injective k hk_mono.injective hk_bound hmn + end Combinatorics diff --git a/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean b/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean index 39fae1cf..95ff093b 100644 --- a/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean +++ b/ForMathlib/MeasureTheory/MeasurableSpace/ComapInfima.lean @@ -60,7 +60,7 @@ lemma comap_iInf_le {ι : Sort*} {α β : Type*} (f : α → β) (m : ι → Mea le_iInf fun i => MeasurableSpace.comap_mono (iInf_le m i) -- Extract witnesses for each comap and choose them uniformly -private lemma comap_iInf_witnesses {ι : Type*} {α β : Type*} {f : α → β} +private lemma comap_iInf_witnesses {ι : Sort*} {α β : Type*} {f : α → β} (m : ι → MeasurableSpace β) (s : Set α) (hs_all : ∀ i, MeasurableSet[MeasurableSpace.comap f (m i)] s) : ∃ (T : ι → Set β), (∀ i, MeasurableSet[m i] (T i)) ∧ (∀ i, s = f ⁻¹' (T i)) := by @@ -74,14 +74,14 @@ private lemma comap_iInf_witnesses {ι : Type*} {α β : Type*} {f : α → β} exact ⟨T, hTmeas, hspre⟩ -- All witnesses are equal when f is surjective -private lemma comap_witnesses_eq_of_surjective {ι : Type*} {α β : Type*} {f : α → β} +private lemma comap_witnesses_eq_of_surjective {ι : Sort*} {α β : Type*} {f : α → β} (hf : Function.Surjective f) (T : ι → Set β) (s : Set α) (hspre : ∀ i, s = f ⁻¹' (T i)) : ∀ i j, T i = T j := fun i j => hf.preimage_injective (by rw [← hspre i, ← hspre j]) -- A set is measurable in comap f (iInf m) if it's the preimage of a canonically measurable set -private lemma measurableSet_comap_iInf_of_canonical {ι : Type*} [Nonempty ι] +private lemma measurableSet_comap_iInf_of_canonical {ι : Sort*} [Nonempty ι] {α β : Type*} {f : α → β} (m : ι → MeasurableSpace β) (T0 : Set β) (hT0 : ∀ i, MeasurableSet[m i] T0) (s : Set α) (hs : s = f ⁻¹' T0) : MeasurableSet[MeasurableSpace.comap f (iInf m)] s := by @@ -93,7 +93,7 @@ private lemma measurableSet_comap_iInf_of_canonical {ι : Type*} [Nonempty ι] This is the key lemma for showing that tail σ-algebras defined via coordinate pullbacks equal tail σ-algebras defined as pullbacks of path-space tails. -/ -theorem iInf_comap_eq_comap_iInf_of_surjective {ι : Type*} [Nonempty ι] +theorem iInf_comap_eq_comap_iInf_of_surjective {ι : Sort*} [Nonempty ι] {α β : Type*} {f : α → β} (hf : Function.Surjective f) (m : ι → MeasurableSpace β) : iInf (fun i => MeasurableSpace.comap f (m i)) = MeasurableSpace.comap f (iInf m) := by From 03a854a215768acf927353dd3b993a9051d20b0d Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Thu, 29 Jan 2026 21:02:21 -0500 Subject: [PATCH 20/20] golf(ForMathlib): Refactor PermutationExtension for mathlib PR MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Change main API from `k : Fin m → ℕ` to cleaner `k : Fin m → Fin n` - Move to `Equiv.Perm` namespace (mathlib convention) - Golf main theorem from 10+ lines to 2 lines (pure term mode) - Remove unused `strictMono_Fin_ge_id` lemma - Add backward-compatible wrappers in `Combinatorics` namespace - Simplify docstrings (remove project-specific references) Line count: 113 → 79 (mathlib PR portion: ~45 lines) --- .../Combinatorics/PermutationExtension.lean | 120 +++++++----------- 1 file changed, 43 insertions(+), 77 deletions(-) diff --git a/ForMathlib/Combinatorics/PermutationExtension.lean b/ForMathlib/Combinatorics/PermutationExtension.lean index 40699c08..a7b16c6e 100644 --- a/ForMathlib/Combinatorics/PermutationExtension.lean +++ b/ForMathlib/Combinatorics/PermutationExtension.lean @@ -8,105 +8,71 @@ import Mathlib.Logic.Equiv.Fintype import Mathlib.GroupTheory.Perm.Basic /-! -# Permutation Extension for Injective Functions +# Extension of Injective Functions to Permutations -This file proves that any injective function `k : Fin m → ℕ` with bounded range -can be extended to a permutation of `Fin n`. +This file proves that injective functions from `Fin m` to `Fin n` can be extended to permutations +of `Fin n`. ## Main Results -* `exists_perm_extending_injective`: Given an injective `k : Fin m → ℕ` with all values `< n` - and `m ≤ n`, there exists a permutation `σ : Perm (Fin n)` such that `σ(i) = k(i)` for all - `i < m`. +* `Equiv.Perm.exists_extending_injective`: Any injective function `k : Fin m → Fin n` can be + extended to a permutation `σ : Perm (Fin n)` such that `σ (Fin.castLE hmn i) = k i` for all `i`. -* `exists_perm_extending_strictMono`: The special case for strictly monotone functions. +* `Equiv.Perm.exists_extending_strictMono`: The special case for strictly monotone functions. -## Mathematical Context +## Implementation Notes -This is a key combinatorial lemma in the proof that **exchangeability implies contractability** -for infinite sequences of random variables. The construction allows any injective -subsequence to be realized as the image of the first m coordinates under some permutation. +The construction uses `Equiv.extendSubtype` to extend an equivalence between subtypes to a +permutation of the ambient type. We compose: +- `(Fin.castLEquiv hmn).symm`: identifies `{x : Fin n | x.val < m}` with `Fin m` +- `Equiv.ofInjective k hk`: identifies `Fin m` with the range of `k` -**Intuition:** We partition both domain and codomain: -- Domain: `{0,...,m-1}` ∪ `{m,...,n-1}` = `Fin n` -- Codomain: `{k(0),...,k(m-1)}` ∪ complement = `Fin n` +Then `Equiv.extendSubtype` extends this to a full permutation. +-/ -Map first `m` positions to `k`-values, then extend arbitrarily to remaining positions -using `Equiv.extendSubtype`. +namespace Equiv.Perm -## Suggested Mathlib Location +/-- Any injective function `k : Fin m → Fin n` can be extended to a permutation of `Fin n`. -`Mathlib.GroupTheory.Perm.Fintype` or `Mathlib.Combinatorics.Subseq` +The permutation agrees with `k` on the image of `Fin.castLE`: for all `i : Fin m`, +we have `σ (Fin.castLE hmn i) = k i`. -/ +theorem exists_extending_injective {m n : ℕ} (k : Fin m → Fin n) (hk : Function.Injective k) + (hmn : m ≤ n) : ∃ σ : Perm (Fin n), ∀ i : Fin m, σ (Fin.castLE hmn i) = k i := + let e := (Fin.castLEquiv hmn).symm.trans (Equiv.ofInjective k hk) + ⟨e.extendSubtype, fun i => Equiv.extendSubtype_apply_of_mem e (Fin.castLE hmn i) i.isLt⟩ -## References +/-- Any strictly monotone function `k : Fin m → Fin n` can be extended to a permutation. -/ +theorem exists_extending_strictMono {m n : ℕ} (k : Fin m → Fin n) (hk : StrictMono k) + (hmn : m ≤ n) : ∃ σ : Perm (Fin n), ∀ i : Fin m, σ (Fin.castLE hmn i) = k i := + exists_extending_injective k hk.injective hmn -* Kallenberg (2005), *Probabilistic Symmetries and Invariance Principles*, Theorem 1.1 --/ +end Equiv.Perm + +/-! ### Backward-compatible API + +The following lemmas provide the original API using `k : Fin m → ℕ` with explicit bounds, +for use in the exchangeability project. -/ namespace Combinatorics variable {m n : ℕ} -/-- For strictly monotone `k : Fin m → ℕ`, values dominate indices: `i ≤ k(i)` for all `i`. -/ -lemma strictMono_Fin_ge_id {k : Fin m → ℕ} (hk : StrictMono k) (i : Fin m) : - i.val ≤ k i := by - -- Proof by strong induction on i.val - have : ∀ n (hn : n < m), n ≤ k ⟨n, hn⟩ := by - intro n - induction n with - | zero => intro _; exact Nat.zero_le _ - | succ n ih => - intro hn - exact Nat.succ_le_of_lt (Nat.lt_of_le_of_lt (ih (Nat.lt_of_succ_lt hn)) - (hk (Fin.mk_lt_mk.mpr (Nat.lt_succ_self n)))) - exact this i.val i.isLt - -/-- -Any injective function can be extended to a permutation. - -**Statement:** Given an injective `k : Fin m → ℕ` with all values `< n` -and `m ≤ n`, there exists a permutation `σ : Perm (Fin n)` such that -`σ(i) = k(i)` for all `i < m`. - -**Construction outline:** -1. **Domain partition:** `{0,...,m-1}` ∪ `{m,...,n-1}` = `Fin n` -2. **Codomain partition:** `{k(0),...,k(m-1)}` ∪ `complement` = `Fin n` -3. Map first `m` positions to `k`-values: `σ(i) = k(i)` for `i < m` -4. Extend arbitrarily to remaining positions using `Equiv.extendSubtype` - -This is the key combinatorial lemma enabling the implication -**exchangeable → contractable**: any injective subsequence can be -realized via a permutation. --/ +/-- Any injective function `k : Fin m → ℕ` with bounded range can be extended to a permutation. + +Given `k : Fin m → ℕ` with `k i < n` for all `i` and `m ≤ n`, there exists `σ : Perm (Fin n)` +such that `(σ ⟨i, _⟩).val = k i` for all `i < m`. -/ theorem exists_perm_extending_injective (k : Fin m → ℕ) (hk_inj : Function.Injective k) (hk_bound : ∀ i, k i < n) (hmn : m ≤ n) : - ∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin m), - (σ ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩).val = k i := by - let kFin : Fin m → Fin n := fun i => ⟨k i, hk_bound i⟩ - -- e_dom: first m elements of Fin n ≃ Fin m - let e_dom : {x : Fin n // (x : ℕ) < m} ≃ Fin m := (Fin.castLEquiv hmn).symm - -- e_cod: Fin m ≃ range of kFin (via injectivity) - have hkFin_inj : Function.Injective kFin := fun i j h => hk_inj (Fin.ext_iff.mp h) - let e_cod' : Fin m ≃ Set.range kFin := Equiv.ofInjective kFin hkFin_inj - -- Convert between range representation and existential predicate - let e_cod : Fin m ≃ {x : Fin n // ∃ i : Fin m, x = kFin i} := - e_cod'.trans (Equiv.subtypeEquivRight fun x => by simp [Set.mem_range, eq_comm]) - -- Compose and extend to full permutation - let σ : Equiv.Perm (Fin n) := Equiv.extendSubtype (e_dom.trans e_cod) - refine ⟨σ, fun i => ?_⟩ - have h := Equiv.extendSubtype_apply_of_mem (e := e_dom.trans e_cod) - (x := Fin.castLE hmn i) i.isLt - simp only [Equiv.trans_apply, e_cod, e_cod', Equiv.ofInjective_apply, kFin] at h - exact congrArg Fin.val h - -/-- Any strictly increasing function can be extended to a permutation. - -This is a corollary of `exists_perm_extending_injective` since strict monotonicity -implies injectivity. -/ + ∃ σ : Equiv.Perm (Fin n), ∀ i : Fin m, (σ ⟨i.val, i.isLt.trans_le hmn⟩).val = k i := by + obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_injective + (fun i => ⟨k i, hk_bound i⟩) (fun _ _ h => hk_inj (Fin.mk.inj h)) hmn + exact ⟨σ, fun i => congrArg Fin.val (hσ i)⟩ + +/-- Any strictly monotone function `k : Fin m → ℕ` with bounded range can be extended to a +permutation. -/ theorem exists_perm_extending_strictMono (k : Fin m → ℕ) (hk_mono : StrictMono k) (hk_bound : ∀ i, k i < n) (hmn : m ≤ n) : - ∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin m), - (σ ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩).val = k i := + ∃ σ : Equiv.Perm (Fin n), ∀ i : Fin m, (σ ⟨i.val, i.isLt.trans_le hmn⟩).val = k i := exists_perm_extending_injective k hk_mono.injective hk_bound hmn end Combinatorics