diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
index 22bdc710..4a721bd5 100644
--- a/.github/workflows/blueprint.yml
+++ b/.github/workflows/blueprint.yml
@@ -44,6 +44,15 @@ jobs:
run: |
lake build
+ - name: Check axioms
+ run: |
+ printf 'import Exchangeability\n#print axioms Exchangeability.DeFinetti.deFinetti\n' \
+ | lake env lean --stdin > /tmp/axioms.out
+ # Exact full-output comparison: an extra axiom or extra line fails the step.
+ diff /tmp/axioms.out - <<'EOF'
+ 'Exchangeability.DeFinetti.deFinetti' depends on axioms: [propext, Classical.choice, Quot.sound]
+ EOF
+
- name: Check declarations
run: |
~/.elan/bin/lake exe checkdecls blueprint/lean_decls
diff --git a/DEVELOPMENT_CHRONOLOGY.md b/DEVELOPMENT_CHRONOLOGY.md
index 57a5f6bb..68f70ada 100644
--- a/DEVELOPMENT_CHRONOLOGY.md
+++ b/DEVELOPMENT_CHRONOLOGY.md
@@ -1,6 +1,7 @@
# Development Chronology
-A narrative history of this Lean 4 formalization, based on 4,024 commits (3,166 non-merge) from Sept 29, 2025 - Jan 8, 2026.
+A narrative history of this Lean 4 formalization, based on 4,247 commits (3,373 non-merge,
+counted on `main` including merges in the total) from Sept 29, 2025 - June 8, 2026.
## Phase 0: Project Initialization (Sept 29 - Oct 1, 2025)
@@ -150,6 +151,25 @@ Created `DirectingMeasure.lean` infrastructure for the identification chain: a s
2. Prepares for potential mathlib integration
3. Professional code quality standards
+## Phase 11: Maintenance & Hardening (Jan 9 - June 8, 2026)
+
+**226 commits (208 non-merge, `--since="2026-01-09 00:00"` on `main`) of post-completion upkeep**
+
+- `886550af` Toolchain upgrade to Lean 4.27.0-rc1, then `8ab88df2` to v4.30.0-rc2 with
+ matching mathlib
+- Cross-tree dead-code sweeps, e.g. `b642382e` (−1,713 lines) and follow-ups — several
+ thousand lines of abandoned scaffolding removed
+- Linter hygiene: `3c40bcbf` cleared all 44 remaining linter warnings; suppressions pruned
+ in stages until `3e7b30d7` dropped the last ones (0 remaining)
+- Term-mode golf batches, e.g. `ef4e47b1` collapsing 32 `by exact` wrappers
+- `93961e6f` Canonical `Contractable.{comp, map_pair}` API; call sites migrated and the old
+ L2Helpers wrappers dropped
+- Blueprint/CI: `8f848259` PR-triggered blueprint consistency check; web + pdf artifact
+ refreshes; `289affe8` doc count/date refresh ahead of the v1.3 release
+
+**Pattern:** With all three proofs complete, work shifted from proving to curation —
+keeping the tree warning-free, current with mathlib, and honest in its documentation.
+
---
## Key Patterns
diff --git a/Exchangeability/Contractability.lean b/Exchangeability/Contractability.lean
index fa1dba7c..304ea3d3 100644
--- a/Exchangeability/Contractability.lean
+++ b/Exchangeability/Contractability.lean
@@ -290,10 +290,8 @@ lemma exists_perm_extending_strictMono {m n : ℕ} (k : Fin m → ℕ)
-- and `g` = the strictly monotone embedding via `k`.
let f : Fin m → Fin n := Fin.castLE hmn
let g : Fin m → Fin n := fun i => ⟨k i, hk_bound i⟩
- have hf : Function.Injective f := Fin.castLE_injective hmn
- have hg : Function.Injective g := fun i j hij =>
- hk_mono.injective (Fin.mk.inj hij)
- obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_pair f g hf hg
+ obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_pair f g (Fin.castLE_injective hmn)
+ (fun i j hij => hk_mono.injective (Fin.mk.inj hij))
exact ⟨σ, fun i => congrArg Fin.val (hσ i)⟩
/- Helper: relabeling coordinates by a finite permutation is measurable as a map
@@ -385,9 +383,8 @@ This follows from monotonicity and the fact that any `i` is at most `last`.
-/
private lemma strictMono_all_lt_succ_last {m : ℕ} (k : Fin m → ℕ) (hk : StrictMono k)
(i : Fin m) (last : Fin m) (h_last : ∀ j, j ≤ last) :
- k i ≤ k last := by
- apply StrictMono.monotone hk
- exact h_last i
+ k i ≤ k last :=
+ hk.monotone (h_last i)
/--
Helper lemma: The length of the domain is bounded by the maximum value plus one.
@@ -398,9 +395,8 @@ This uses the fact that strictly monotone functions satisfy `i ≤ k(i)` for all
private lemma strictMono_length_le_max_succ {m : ℕ} (k : Fin m → ℕ) (hk : StrictMono k)
(last : Fin m) (h_last_is_max : last.val + 1 = m) :
m ≤ k last + 1 := by
- have h_mono : last.val ≤ k last := strictMono_Fin_ge_id hk last
calc m = last.val + 1 := h_last_is_max.symm
- _ ≤ k last + 1 := Nat.add_le_add_right h_mono 1
+ _ ≤ k last + 1 := Nat.add_le_add_right (strictMono_Fin_ge_id hk last) 1
/--
**Main theorem:** Every exchangeable sequence is contractable.
diff --git a/Exchangeability/Core.lean b/Exchangeability/Core.lean
index 4912dbc5..82e924ad 100644
--- a/Exchangeability/Core.lean
+++ b/Exchangeability/Core.lean
@@ -208,15 +208,11 @@ private lemma cylinder_subset_prefixCylinders {s : Finset ℕ} {S : Set (∀ _ :
intro i hi
have hle : i ≤ s.sup id := by convert Finset.le_sup (f := id) hi
omega
- -- Transport `S` along the inclusion into the initial segment.
- 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)
+ -- Transport `S` along the inclusion into the initial segment; the cylinder is
+ -- definitionally the prefix cylinder of the pulled-back set.
+ let pull : (Fin N → α) → (∀ i : s, α) := fun x => fun y => x ⟨y.1, h_mem y.1 y.2⟩
have hpull_meas : Measurable pull := by fun_prop
- have hs_eq :
- MeasureTheory.cylinder (α:=fun _ : ℕ => α) s S =
- prefixCylinder (α:=α) (pull ⁻¹' S) := rfl
- refine hs_eq ▸ prefixCylinder_mem_prefixCylinders (α:=α) ?_
- exact hpull_meas hS
+ exact prefixCylinder_mem_prefixCylinders (α:=α) (hpull_meas hS)
/--
The σ-algebra generated by prefix cylinders is the product σ-algebra.
diff --git a/Exchangeability/DeFinetti/CommonEnding.lean b/Exchangeability/DeFinetti/CommonEnding.lean
index ab07ac44..0d82deb9 100644
--- a/Exchangeability/DeFinetti/CommonEnding.lean
+++ b/Exchangeability/DeFinetti/CommonEnding.lean
@@ -425,8 +425,6 @@ theorem conditional_iid_from_directing_measure
exact fidi_eq_avg_product X hX_meas ν hν_prob hν_meas m k B hB_meas
(h_bridge (k := k) hk_strict.injective (B := B) hB_meas)
--- *Monotone-class remark.* Earlier drafts included an explicit monotone-class lemma
--- (`monotone_class_product_extension`) proving the π-λ step described above. The sole
--- remaining use of that lemma is captured abstractly by the `h_bridge` hypothesis, so the
--- sketch is retained only as commentary.
+-- *Monotone-class remark.* The π-λ step described above is captured abstractly by the
+-- `h_bridge` hypothesis, so no explicit monotone-class lemma is needed here.
end Exchangeability.DeFinetti.CommonEnding
diff --git a/Exchangeability/DeFinetti/L2Helpers.lean b/Exchangeability/DeFinetti/L2Helpers.lean
index 43520262..384e39bc 100644
--- a/Exchangeability/DeFinetti/L2Helpers.lean
+++ b/Exchangeability/DeFinetti/L2Helpers.lean
@@ -24,8 +24,8 @@ All lemmas here are complete (no sorries) and compile cleanly.
- Various arithmetic bounds for convergence rates (e.g. `sqrt_div_lt_half_eps_of_nat`)
- Fin index reindexing lemmas for filtered sums
-The contractability/covariance helpers that previously lived here have moved to the
-canonical `Exchangeability.Contractable.{map_single, map_pair, comp}` API in
+For contractability/covariance helpers, see the canonical
+`Exchangeability.Contractable.{map_single, map_pair, comp}` API in
`Exchangeability/Contractability.lean`.
-/
diff --git a/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean b/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean
index 5c7add21..d1a83232 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Cameron Freer
-/
import Exchangeability.DeFinetti.ViaKoopman.Infrastructure
-import Exchangeability.DeFinetti.ViaKoopman.LpCondExpHelpers
+import Exchangeability.Probability.LpNormHelpers
/-! # Cesàro Helper Lemmas
@@ -36,6 +36,25 @@ variable {α : Type*} [MeasurableSpace α]
-- Short notation for shift-invariant σ-algebra (used throughout this file)
local notation "mSI" => shiftInvariantSigma (α := α)
+/-- Finite sum linearity of conditional expectation, stated with the sum applied
+pointwise (`fun ω => ∑ i ∈ s, f i ω`) as it appears in the Cesàro averages below.
+η-expands to mathlib's `condExp_finset_sum`. -/
+private lemma condExp_sum_finset
+ {Ω : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
+ {m : MeasurableSpace Ω} (_hm : m ≤ mΩ)
+ {ι : Type*} (s : Finset ι) (f : ι → Ω → ℝ)
+ (hint : ∀ i ∈ s, Integrable (f i) μ) :
+ μ[(fun ω => s.sum (fun i => f i ω)) | m]
+ =ᵐ[μ] (fun ω => s.sum (fun i => μ[f i | m] ω)) := by
+ classical
+ have h_sum_eta : (fun ω => ∑ i ∈ s, f i ω) = ∑ i ∈ s, f i := by
+ funext ω
+ simp only [Finset.sum_apply]
+ have h_ce_sum_eta : (fun ω => ∑ i ∈ s, μ[f i | m] ω) = ∑ i ∈ s, μ[f i | m] := by
+ funext ω
+ simp only [Finset.sum_apply]
+ rw [h_sum_eta, h_ce_sum_eta]
+ exact condExp_finset_sum hint m
lemma condexp_precomp_iterate_eq
{μ : Measure (Ω[α])} [IsProbabilityMeasure μ]
@@ -321,8 +340,8 @@ lemma product_ce_constant_of_lag_const
= (fun ω => (1 / ((n + 1) : ℝ)) * (Finset.range (n + 1)).sum (fun j => f (ω 0) * g (ω j))) := by
funext ω; simp [A, Finset.mul_sum, mul_comm, mul_left_comm, mul_assoc]
rw [this]
- exact condExp_const_mul (shiftInvariantSigma_le (α := α))
- (1 / ((n + 1) : ℝ)) (fun ω => (Finset.range (n + 1)).sum (fun j => f (ω 0) * g (ω j)))
+ simpa [Pi.mul_apply, smul_eq_mul] using condExp_smul (μ := μ)
+ (1 / ((n + 1) : ℝ)) (fun ω => (Finset.range (n + 1)).sum (fun j => f (ω 0) * g (ω j))) mSI
-- Push CE through the finite sum
have h_sum :
@@ -460,8 +479,8 @@ lemma product_ce_constant_of_lag_const_from_one
= (fun ω => (1 / (n : ℝ)) * (Finset.range n).sum (fun j => f (ω 0) * g (ω (j + 1)))) := by
funext ω; simp [A', Finset.mul_sum, mul_left_comm]
rw [this]
- exact condExp_const_mul (shiftInvariantSigma_le (α := α))
- (1 / (n : ℝ)) (fun ω => (Finset.range n).sum (fun j => f (ω 0) * g (ω (j + 1))))
+ simpa [Pi.mul_apply, smul_eq_mul] using condExp_smul (μ := μ)
+ (1 / (n : ℝ)) (fun ω => (Finset.range n).sum (fun j => f (ω 0) * g (ω (j + 1)))) mSI
-- Push CE through the finite sum
have h_sum :
diff --git a/Exchangeability/DeFinetti/ViaKoopman/LpCondExpHelpers.lean b/Exchangeability/DeFinetti/ViaKoopman/LpCondExpHelpers.lean
deleted file mode 100644
index 0af2a937..00000000
--- a/Exchangeability/DeFinetti/ViaKoopman/LpCondExpHelpers.lean
+++ /dev/null
@@ -1,116 +0,0 @@
-/-
-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.Function.LpSpace.Basic
-
-/-!
-# Conditional Expectation and Lp Helper Lemmas
-
-This file contains utility lemmas for conditional expectation and Lp norm manipulation.
-
-## Main Definitions
-
-None - this file only contains helper lemmas.
-
-## Main Results
-
-* `condExp_const_mul`: Scalar linearity of conditional expectation
-* `condExp_sum_finset`: Finite sum linearity of conditional expectation
-* `integrable_of_bounded_measurable`: Bounded measurable functions are integrable on finite measure spaces
-* `eLpNorm_one_le_eLpNorm_two_toReal`: L¹ norm bounded by L² norm on probability spaces
--/
-
-open MeasureTheory Filter
-open scoped Topology
-
-noncomputable section
-
-/-! ### Lp norm placeholder -/
-
-/-! ### Lp seminorm: use mathlib's `eLpNorm` -/
-
-/-! ### Conditional expectation linearity helpers -/
-
-/-- Scalar linearity of conditional expectation.
-**Mathematical content**: CE[c·f| mSI] = c·CE[f| mSI]
-**Mathlib source**: `MeasureTheory.condexp_smul` for scalar multiplication. -/
-lemma condExp_const_mul
- {Ω : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
- {m : MeasurableSpace Ω} (_hm : m ≤ mΩ)
- (c : ℝ) (f : Ω → ℝ) :
- μ[(fun ω => c * f ω) | m] =ᵐ[μ] (fun ω => c * μ[f | m] ω) := by
- -- `condExp_smul` in mathlib takes m as explicit positional parameter
- simpa [Pi.mul_apply, smul_eq_mul] using
- (MeasureTheory.condExp_smul c f m)
-
-/-- Finite sum linearity of conditional expectation.
-**Mathematical content**: CE[Σᵢfᵢ| mSI] = ΣᵢCE[fᵢ| mSI]
-**Mathlib source**: Direct application of `MeasureTheory.condExp_finset_sum`.
-NOTE: Uses η-expansion to work around notation elaboration issues with `∑ i ∈ s, f i` vs `fun ω => ∑ i ∈ s, f i ω`. -/
-lemma condExp_sum_finset
- {Ω : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
- {m : MeasurableSpace Ω} (_hm : m ≤ mΩ)
- {ι : Type*} (s : Finset ι) (f : ι → Ω → ℝ)
- (hint : ∀ i ∈ s, Integrable (f i) μ) :
- μ[(fun ω => s.sum (fun i => f i ω)) | m]
- =ᵐ[μ] (fun ω => s.sum (fun i => μ[f i | m] ω)) := by
- classical
- -- Rewrite using η-reduction: (fun ω => ∑ i ∈ s, f i ω) = ∑ i ∈ s, f i
- have h_sum_eta : (fun ω => ∑ i ∈ s, f i ω) = ∑ i ∈ s, f i := by
- funext ω
- simp only [Finset.sum_apply]
- have h_ce_sum_eta : (fun ω => ∑ i ∈ s, μ[f i | m] ω) = ∑ i ∈ s, μ[f i | m] := by
- funext ω
- simp only [Finset.sum_apply]
- -- Rewrite goal using η-reduction
- rw [h_sum_eta, h_ce_sum_eta]
- -- Apply condExp_finset_sum
- exact condExp_finset_sum hint m
-
-/-- On a finite measure space, a bounded measurable real function is integrable. -/
-lemma integrable_of_bounded_measurable
- {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
- {f : Ω → ℝ} (hf_meas : Measurable f) (C : ℝ) (hf_bd : ∀ ω, |f ω| ≤ C) :
- Integrable f μ :=
- ⟨hf_meas.aestronglyMeasurable, HasFiniteIntegral.of_bounded (by
- filter_upwards with ω; simpa [Real.norm_eq_abs] using hf_bd ω)⟩
-
-/-- On a probability space, `‖f‖₁ ≤ ‖f‖₂`. Version with real integral on the left.
-We assume `MemLp f 2 μ` so the right-hand side is finite; this matches all uses below
-where the function is bounded (hence in L²).
-
-**Proof strategy** (from user's specification):
-- Use `snorm_mono_exponent` or `memℒp_one_of_memℒp_two` to get `MemLp f 1 μ` from `MemLp f 2 μ`
-- Show both `eLpNorm f 1 μ` and `eLpNorm f 2 μ` are finite
-- Apply exponent monotonicity: `eLpNorm f 1 μ ≤ eLpNorm f 2 μ` on probability spaces
-- Convert `∫|f|` to `(eLpNorm f 1 μ).toReal` and apply `ENNReal.toReal_le_toReal`
--/
-lemma eLpNorm_one_le_eLpNorm_two_toReal
- {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
- (f : Ω → ℝ) (hL1 : Integrable f μ) (hL2 : MemLp f 2 μ) :
- (∫ ω, |f ω| ∂μ) ≤ (eLpNorm f 2 μ).toReal := by
- -- Step 1: Connect ∫|f| to eLpNorm f 1 μ using norm
- have h_eq : ENNReal.ofReal (∫ ω, |f ω| ∂μ) = eLpNorm f 1 μ := by
- have h_norm : ∫ ω, |f ω| ∂μ = ∫ ω, ‖f ω‖ ∂μ := integral_congr_ae (ae_of_all μ (fun ω => (Real.norm_eq_abs (f ω)).symm))
- rw [h_norm, ofReal_integral_norm_eq_lintegral_enorm hL1]
- exact eLpNorm_one_eq_lintegral_enorm.symm
-
- -- Step 2: eLpNorm f 1 μ ≤ eLpNorm f 2 μ on probability spaces
- have h_mono : eLpNorm f 1 μ ≤ eLpNorm f 2 μ := by
- have h_ae : AEStronglyMeasurable f μ := hL1.aestronglyMeasurable
- refine eLpNorm_le_eLpNorm_of_exponent_le ?_ h_ae
- norm_num
-
- -- Step 3: Convert to toReal inequality
- have h_fin : eLpNorm f 2 μ ≠ ⊤ := hL2.eLpNorm_ne_top
- have h_nonneg : 0 ≤ ∫ ω, |f ω| ∂μ := integral_nonneg (fun ω => abs_nonneg _)
- calc (∫ ω, |f ω| ∂μ)
- = (ENNReal.ofReal (∫ ω, |f ω| ∂μ)).toReal := by
- rw [ENNReal.toReal_ofReal h_nonneg]
- _ = (eLpNorm f 1 μ).toReal := by rw [h_eq]
- _ ≤ (eLpNorm f 2 μ).toReal := ENNReal.toReal_mono h_fin h_mono
-
diff --git a/Exchangeability/DeFinetti/ViaKoopman/README.md b/Exchangeability/DeFinetti/ViaKoopman/README.md
index bdd82c2a..d655ddc3 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/README.md
+++ b/Exchangeability/DeFinetti/ViaKoopman/README.md
@@ -32,7 +32,6 @@ This directory contains Kallenberg's "first proof" of de Finetti's theorem, usin
| `BlockInjection.lean` | Block injection lemmas |
| `KernelBridge.lean` | Bridge lemma for kernel measures |
| `CylinderFunctions.lean` | Cylinder function definitions |
-| `LpCondExpHelpers.lean` | Lᵖ conditional expectation helpers |
| `DirectingKernel.lean` | Directing measure from CE kernel |
| `Quantization.lean` | Quantization machinery |
| `Infrastructure.lean` | Basic definitions |
diff --git a/Exchangeability/DeFinetti/ViaL2/AlphaConvergence/AlphaIicEq.lean b/Exchangeability/DeFinetti/ViaL2/AlphaConvergence/AlphaIicEq.lean
index 5a5184ea..365841b8 100644
--- a/Exchangeability/DeFinetti/ViaL2/AlphaConvergence/AlphaIicEq.lean
+++ b/Exchangeability/DeFinetti/ViaL2/AlphaConvergence/AlphaIicEq.lean
@@ -34,8 +34,8 @@ variable {Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpace α]
/-- Clipping `b` to `[0,1]` can only bring it closer to anything already in `[0,1]`.
-Internal helper: factors out the case analysis that previously appeared in
-`alphaIic_ae_eq_alphaIicCE`. The cleanest route is via mathlib's
+Internal helper for the case analysis in `alphaIic_ae_eq_alphaIicCE`.
+The cleanest route is via mathlib's
`LipschitzWith.projIcc`: `Set.projIcc 0 1` is `1`-Lipschitz, equals
`max 0 (min 1 ·)` after coercion, and fixes any input already in `[0,1]`. -/
private lemma abs_sub_clip01_le_of_mem {a b : ℝ} (ha : a ∈ Set.Icc (0 : ℝ) 1) :
diff --git a/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean b/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean
index c07f3962..5afaa5d9 100644
--- a/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean
+++ b/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean
@@ -78,10 +78,9 @@ noncomputable def alphaIicCE
/-- Measurability of alphaIicCE.
-Note: Previously had BorelSpace typeclass instance resolution issues.
-The conditional expectation `condExp μ (tailSigma X) f` is measurable by
-`stronglyMeasurable_condExp.measurable`, but Lean can't synthesize the required
-`BorelSpace` instance automatically. This should be straightforward to fix. -/
+The conditional expectation is strongly measurable with respect to the tail σ-algebra
+(`stronglyMeasurable_condExp`), and `Measurable.mono` lifts this to the ambient
+σ-algebra via `tailProcess_le_ambient`. -/
@[measurability, fun_prop]
lemma alphaIicCE_measurable
{μ : Measure Ω} [IsProbabilityMeasure μ]
diff --git a/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean b/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean
index 1d8fb7f9..3c04734c 100644
--- a/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean
+++ b/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean
@@ -44,8 +44,8 @@ variable {Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpace α]
The proof routes through the kernel-level bridge
`directing_measure_ae_eq_condExpKernel_map` and mathlib's
-`condExp_ae_eq_integral_condExpKernel`, replacing what was previously a hand-built
-monotone-class extension from `Iic` indicators.
+`condExp_ae_eq_integral_condExpKernel`, so no monotone-class extension from `Iic`
+indicators is needed.
The `[StandardBorelSpace Ω]` assumption comes from `condExpKernel`. -/
lemma directing_measure_integral_eq_condExp
diff --git a/Exchangeability/Probability/IntegrationHelpers.lean b/Exchangeability/Probability/IntegrationHelpers.lean
index 21197e01..0ddd0daf 100644
--- a/Exchangeability/Probability/IntegrationHelpers.lean
+++ b/Exchangeability/Probability/IntegrationHelpers.lean
@@ -193,4 +193,30 @@ lemma integral_pushforward_sq_diff
rw [integral_map hf.aemeasurable]
exact (continuous_id.sub continuous_const).pow 2 |>.aestronglyMeasurable
+/-! ## Fatou-Type Lemmas -/
+
+/-- Fatou's lemma on `ENNReal.ofReal ∘ ‖·‖` along an a.e. pointwise limit.
+
+If `u n x → g x` a.e., then `∫⁻ ‖g‖ ≤ liminf (∫⁻ ‖u n‖)`. -/
+lemma lintegral_fatou_ofReal_norm
+ {α β : Type*} [MeasurableSpace α] {μ : Measure α}
+ [MeasurableSpace β] [NormedAddCommGroup β] [BorelSpace β]
+ {u : ℕ → α → β} {g : α → β}
+ (hae : ∀ᵐ x ∂μ, Tendsto (fun n => u n x) atTop (nhds (g x)))
+ (hu_meas : ∀ n, AEMeasurable (fun x => ENNReal.ofReal ‖u n x‖) μ)
+ (_hg_meas : AEMeasurable (fun x => ENNReal.ofReal ‖g x‖) μ) :
+ ∫⁻ x, ENNReal.ofReal ‖g x‖ ∂μ
+ ≤ liminf (fun n => ∫⁻ x, ENNReal.ofReal ‖u n x‖ ∂μ) atTop := by
+ have hae_ofReal :
+ ∀ᵐ x ∂μ,
+ Tendsto (fun n => ENNReal.ofReal ‖u n x‖) atTop
+ (nhds (ENNReal.ofReal ‖g x‖)) :=
+ hae.mono (fun x hx =>
+ ((ENNReal.continuous_ofReal.comp continuous_norm).tendsto _).comp hx)
+ calc ∫⁻ x, ENNReal.ofReal ‖g x‖ ∂μ
+ = ∫⁻ x, liminf (fun n => ENNReal.ofReal ‖u n x‖) atTop ∂μ :=
+ lintegral_congr_ae (hae_ofReal.mono fun x hx => hx.liminf_eq.symm)
+ _ ≤ liminf (fun n => ∫⁻ x, ENNReal.ofReal ‖u n x‖ ∂μ) atTop :=
+ lintegral_liminf_le' hu_meas
+
end Exchangeability.Probability.IntegrationHelpers
diff --git a/Exchangeability/Probability/LpNormHelpers.lean b/Exchangeability/Probability/LpNormHelpers.lean
index 0c5e8a59..293b3201 100644
--- a/Exchangeability/Probability/LpNormHelpers.lean
+++ b/Exchangeability/Probability/LpNormHelpers.lean
@@ -5,6 +5,7 @@ Authors: Cameron Freer
-/
import Mathlib.MeasureTheory.Function.L2Space
import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+import Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
import Mathlib.Analysis.SpecialFunctions.Pow.Real
/-!
@@ -157,5 +158,43 @@ lemma memLp_two_of_bounded
filter_upwards with ω
exact (Real.norm_eq_abs _).le.trans (hf_bdd ω)
+/-- On a finite measure space, a bounded measurable real function is integrable.
+
+Unlike mathlib's `Integrable.of_bound`, this takes `Measurable` and a pointwise
+absolute-value bound, the shape produced by the block-average constructions. -/
+lemma integrable_of_bounded_measurable
+ [IsFiniteMeasure μ]
+ {f : Ω → ℝ} (hf_meas : Measurable f) (C : ℝ) (hf_bd : ∀ ω, |f ω| ≤ C) :
+ Integrable f μ :=
+ ⟨hf_meas.aestronglyMeasurable, HasFiniteIntegral.of_bounded (by
+ filter_upwards with ω; simpa [Real.norm_eq_abs] using hf_bd ω)⟩
+
+/-- On a probability space, `‖f‖₁ ≤ ‖f‖₂`. Version with real integral on the left.
+We assume `MemLp f 2 μ` so the right-hand side is finite; this matches the uses
+where the function is bounded (hence in L²). -/
+lemma eLpNorm_one_le_eLpNorm_two_toReal
+ [IsProbabilityMeasure μ]
+ (f : Ω → ℝ) (hL1 : Integrable f μ) (hL2 : MemLp f 2 μ) :
+ (∫ ω, |f ω| ∂μ) ≤ (eLpNorm f 2 μ).toReal := by
+ -- Step 1: Connect ∫|f| to eLpNorm f 1 μ using norm
+ have h_eq : ENNReal.ofReal (∫ ω, |f ω| ∂μ) = eLpNorm f 1 μ := by
+ have h_norm : ∫ ω, |f ω| ∂μ = ∫ ω, ‖f ω‖ ∂μ :=
+ integral_congr_ae (ae_of_all μ (fun ω => (Real.norm_eq_abs (f ω)).symm))
+ rw [h_norm, ofReal_integral_norm_eq_lintegral_enorm hL1]
+ exact eLpNorm_one_eq_lintegral_enorm.symm
+ -- Step 2: eLpNorm f 1 μ ≤ eLpNorm f 2 μ on probability spaces
+ have h_mono : eLpNorm f 1 μ ≤ eLpNorm f 2 μ := by
+ have h_ae : AEStronglyMeasurable f μ := hL1.aestronglyMeasurable
+ refine eLpNorm_le_eLpNorm_of_exponent_le ?_ h_ae
+ norm_num
+ -- Step 3: Convert to toReal inequality
+ have h_fin : eLpNorm f 2 μ ≠ ⊤ := hL2.eLpNorm_ne_top
+ have h_nonneg : 0 ≤ ∫ ω, |f ω| ∂μ := integral_nonneg (fun ω => abs_nonneg _)
+ calc (∫ ω, |f ω| ∂μ)
+ = (ENNReal.ofReal (∫ ω, |f ω| ∂μ)).toReal := by
+ rw [ENNReal.toReal_ofReal h_nonneg]
+ _ = (eLpNorm f 1 μ).toReal := by rw [h_eq]
+ _ ≤ (eLpNorm f 2 μ).toReal := ENNReal.toReal_mono h_fin h_mono
+
end MeasureTheory
diff --git a/Exchangeability/Probability/Martingale/Crossings/AntitoneLimit.lean b/Exchangeability/Probability/Martingale/Crossings/AntitoneLimit.lean
index 3f2d7931..dbf8e268 100644
--- a/Exchangeability/Probability/Martingale/Crossings/AntitoneLimit.lean
+++ b/Exchangeability/Probability/Martingale/Crossings/AntitoneLimit.lean
@@ -5,7 +5,7 @@ Authors: Cameron Freer
-/
import Mathlib.Probability.Martingale.Convergence
-import Exchangeability.Probability.MartingaleExtras
+import Exchangeability.Probability.IntegrationHelpers
import Exchangeability.Probability.SigmaAlgebraHelpers
import Exchangeability.Probability.Martingale.Crossings.Bounds
@@ -238,7 +238,7 @@ lemma condExp_exists_ae_limit_antitone
calc
∫⁻ ω, ENNReal.ofReal ‖Xlim ω‖ ∂μ
≤ liminf (fun n => ∫⁻ ω, ENNReal.ofReal ‖μ[f | 𝔽 n] ω‖ ∂μ) atTop :=
- lintegral_fatou_ofReal_norm h_ae_tendsto hmeas_n hmeas_lim
+ IntegrationHelpers.lintegral_fatou_ofReal_norm h_ae_tendsto hmeas_n hmeas_lim
_ ≤ ↑R := by
rw [liminf_le_iff]
intro b hb
diff --git a/Exchangeability/Probability/MartingaleExtras.lean b/Exchangeability/Probability/MartingaleExtras.lean
deleted file mode 100644
index 79ab0c12..00000000
--- a/Exchangeability/Probability/MartingaleExtras.lean
+++ /dev/null
@@ -1,61 +0,0 @@
-/-
-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.Martingale.Basic
-import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import Mathlib.MeasureTheory.Integral.Bochner.Basic
-import Mathlib.Probability.Kernel.CondDistrib
-import Mathlib.Probability.Kernel.Composition.Comp
-import Mathlib.MeasureTheory.MeasurableSpace.Prod
-import Mathlib.MeasureTheory.Function.FactorsThrough
-
-/-!
-# Martingale Helper Lemmas
-
-## Contents
-
-* `lintegral_fatou_ofReal_norm`: Fatou's lemma for `ENNReal.ofReal ∘ ‖·‖`
-
-## References
-
-* Durrett, *Probability: Theory and Examples* (2019), Section 5.5
-* Williams, *Probability with Martingales* (1991)
--/
-
-noncomputable section
-open scoped MeasureTheory ProbabilityTheory Topology
-open MeasureTheory Filter Set Function
-
-namespace Exchangeability.Probability
-
-variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
-
-/-! ## Fatou-Type Lemmas -/
-
-/-- Fatou's lemma on `ENNReal.ofReal ∘ ‖·‖` along an a.e. pointwise limit.
-
-If `u n x → g x` a.e., then `∫⁻ ‖g‖ ≤ liminf (∫⁻ ‖u n‖)`. -/
-lemma lintegral_fatou_ofReal_norm
- {α β : Type*} [MeasurableSpace α] {μ : Measure α}
- [MeasurableSpace β] [NormedAddCommGroup β] [BorelSpace β]
- {u : ℕ → α → β} {g : α → β}
- (hae : ∀ᵐ x ∂μ, Tendsto (fun n => u n x) atTop (nhds (g x)))
- (hu_meas : ∀ n, AEMeasurable (fun x => ENNReal.ofReal ‖u n x‖) μ)
- (_hg_meas : AEMeasurable (fun x => ENNReal.ofReal ‖g x‖) μ) :
- ∫⁻ x, ENNReal.ofReal ‖g x‖ ∂μ
- ≤ liminf (fun n => ∫⁻ x, ENNReal.ofReal ‖u n x‖ ∂μ) atTop := by
- have hae_ofReal :
- ∀ᵐ x ∂μ,
- Tendsto (fun n => ENNReal.ofReal ‖u n x‖) atTop
- (nhds (ENNReal.ofReal ‖g x‖)) :=
- hae.mono (fun x hx =>
- ((ENNReal.continuous_ofReal.comp continuous_norm).tendsto _).comp hx)
- calc ∫⁻ x, ENNReal.ofReal ‖g x‖ ∂μ
- = ∫⁻ x, liminf (fun n => ENNReal.ofReal ‖u n x‖) atTop ∂μ :=
- lintegral_congr_ae (hae_ofReal.mono fun x hx => hx.liminf_eq.symm)
- _ ≤ liminf (fun n => ∫⁻ x, ENNReal.ofReal ‖u n x‖ ∂μ) atTop :=
- lintegral_liminf_le' hu_meas
-
-end Exchangeability.Probability
diff --git a/README.md b/README.md
index 3baebfcb..6ed0ee91 100644
--- a/README.md
+++ b/README.md
@@ -27,7 +27,7 @@ We implement **all three proofs** from Kallenberg (2005) of the key implication
3. **Koopman Approach**
- Kallenberg's "first proof" - Mean Ergodic Theorem
- Deep connection to dynamical systems and ergodic theory
- - [`Exchangeability/DeFinetti/ViaKoopman/`](Exchangeability/DeFinetti/ViaKoopman/) (16 files)
+ - [`Exchangeability/DeFinetti/ViaKoopman/`](Exchangeability/DeFinetti/ViaKoopman/) (15 files)
### Import Graph
@@ -94,7 +94,7 @@ Exchangeability/
│ ├── Theorem.lean # Public API (exports ViaMartingale)
│ ├── ViaMartingale/ # Martingale proof (12 files)
│ ├── ViaL2/ # L² proof (24 files)
-│ ├── ViaKoopman/ # Ergodic proof (16 files)
+│ ├── ViaKoopman/ # Ergodic proof (15 files)
│ ├── CommonEnding.lean # Shared final step
│ └── L2Helpers.lean # L² utility and Fin index lemmas
├── Ergodic/ # Ergodic theory (for Koopman)
diff --git a/STATUS.md b/STATUS.md
index 9d8b33e6..f6f93b46 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -1,6 +1,6 @@
# Project Status: de Finetti Theorem Formalization
-**Last Updated:** 2026-05-27
+**Last Updated:** 2026-06-09
## Executive Summary
@@ -10,10 +10,10 @@ LOC counts below cover the `Exchangeability/` library tree (excluding the top-le
| Proof Approach | Lines | Build | Status |
|---------------|------:|-------|--------|
| **ViaMartingale** | 2,804 | Pass | **COMPLETE** |
-| **ViaL2** | 7,444 | Pass | **COMPLETE** |
-| **ViaKoopman** | 5,402 | Pass | **COMPLETE** |
-| *Shared infrastructure* | 11,117 | — | — |
-| **Total** | **26,767** | Pass | **COMPLETE** |
+| **ViaL2** | 7,443 | Pass | **COMPLETE** |
+| **ViaKoopman** | 5,305 | Pass | **COMPLETE** |
+| *Shared infrastructure* | 11,111 | — | — |
+| **Total** | **26,663** | Pass | **COMPLETE** |
**All three proofs complete.**
diff --git a/blueprint/web/import_graph_colored.html b/blueprint/web/import_graph_colored.html
index 5c743d76..f5ce0a05 100644
--- a/blueprint/web/import_graph_colored.html
+++ b/blueprint/web/import_graph_colored.html
@@ -501,7 +501,7 @@
Import Graph for Exchangeability
// NOTE: currently the Lean script searches for this line to replace it (exact search)!
// If you modify it, modify the Lean script (ImportGraph/Cli.lean) accordingly!
-render_gexf(" Lean ImportGraph ")
+render_gexf(" Lean ImportGraph ")
container.addEventListener("dragover", ev => {
event.preventDefault();
diff --git a/blueprint/web/import_graph_colored.png b/blueprint/web/import_graph_colored.png
index 47b6d3fa..6112f93b 100644
Binary files a/blueprint/web/import_graph_colored.png and b/blueprint/web/import_graph_colored.png differ
diff --git a/blueprint/web/import_graph_colored.svg b/blueprint/web/import_graph_colored.svg
index 1562684e..6ab2e3cb 100644
--- a/blueprint/web/import_graph_colored.svg
+++ b/blueprint/web/import_graph_colored.svg
@@ -4,1762 +4,1746 @@
-