diff --git a/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean b/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean
index 5a33077e..373116f3 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean
@@ -173,7 +173,8 @@ lemma blockAvg_tendsto_condExp
-- Key fact 2: Y is shift-invariant (CE w.r.t. mSI is constant on shift orbits)
have hf_int : Integrable (fun ω : Ω[α] => f (ω 0)) μ :=
let ⟨C, hC⟩ := hf_bd
- integrable_of_bounded_measurable (hf.comp (measurable_pi_apply 0)) C fun ω => hC (ω 0)
+ Integrable.of_bound (hf.comp (measurable_pi_apply 0)).aestronglyMeasurable C
+ (ae_of_all _ fun ω => hC (ω 0))
have h_Y_shift_inv : ∀ p : ℕ, (fun ω => Y (shift^[p] ω)) =ᵐ[μ] Y := by
intro p
diff --git a/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean b/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean
index e9dfcf4a..e9942020 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean
@@ -193,16 +193,18 @@ lemma cesaro_ce_eq_condexp
(fun ω =>
(Finset.range (n + 1)).sum (fun j => μ[(fun ω => g (ω j)) | mSI] ω)) := by
have hint : ∀ j ∈ Finset.range (n + 1), Integrable (fun ω => g (ω j)) μ := fun j _ =>
- hg_bd.elim fun Cg hCg => integrable_of_bounded_measurable
- (hg_meas.comp (measurable_pi_apply j)) Cg (fun ω => hCg (ω j))
+ hg_bd.elim fun Cg hCg => Integrable.of_bound
+ (hg_meas.comp (measurable_pi_apply j)).aestronglyMeasurable Cg
+ (ae_of_all _ fun ω => hCg (ω j))
exact condExp_sum_finset (m := mSI) (_hm := hmSI)
(Finset.range (n + 1)) (fun j ω => g (ω j)) hint
-- Each term μ[g(ωⱼ)| mSI] =ᵐ μ[g(ω₀)| mSI]
have h_term : ∀ j, μ[(fun ω => g (ω j)) | mSI] =ᵐ[μ] μ[(fun ω => g (ω 0)) | mSI] := fun j => by
have hg_0_int : Integrable (fun ω => g (ω 0)) μ :=
- hg_bd.elim fun Cg hCg => integrable_of_bounded_measurable
- (hg_meas.comp (measurable_pi_apply 0)) Cg (fun ω => hCg (ω 0))
+ hg_bd.elim fun Cg hCg => Integrable.of_bound
+ (hg_meas.comp (measurable_pi_apply 0)).aestronglyMeasurable Cg
+ (ae_of_all _ fun ω => hCg (ω 0))
have h_shift : (fun ω => g (shift^[j] ω 0)) = (fun ω => g (ω j)) := by
ext ω; simp only [shift_iterate_apply, zero_add]
rw [← h_shift]; exact condexp_precomp_iterate_eq hσ hg_0_int
@@ -355,10 +357,12 @@ lemma product_ce_constant_of_lag_const
intro j _
obtain ⟨Cf, hCf⟩ := hf_bd
obtain ⟨Cg, hCg⟩ := hg_bd
- exact integrable_of_bounded_measurable
- (hf_meas.comp (measurable_pi_apply 0) |>.mul (hg_meas.comp (measurable_pi_apply j)))
- (Cf * Cg)
- (fun ω => by simpa [abs_mul] using mul_le_mul (hCf (ω 0)) (hCg (ω j)) (abs_nonneg _) (le_trans (abs_nonneg _) (hCf (ω 0))))
+ have hmeas : Measurable fun ω : Ω[α] => f (ω 0) * g (ω j) :=
+ (hf_meas.comp (measurable_pi_apply 0)).mul (hg_meas.comp (measurable_pi_apply j))
+ exact Integrable.of_bound hmeas.aestronglyMeasurable (Cf * Cg)
+ (ae_of_all _ fun ω => by
+ simpa [abs_mul, Real.norm_eq_abs] using mul_le_mul (hCf (ω 0)) (hCg (ω j))
+ (abs_nonneg _) (le_trans (abs_nonneg _) (hCf (ω 0))))
exact condExp_sum_finset (shiftInvariantSigma_le (α := α))
(Finset.range (n + 1)) (fun j => fun ω => f (ω 0) * g (ω j)) hint
@@ -494,10 +498,12 @@ lemma product_ce_constant_of_lag_const_from_one
intro j _
obtain ⟨Cf, hCf⟩ := hf_bd
obtain ⟨Cg, hCg⟩ := hg_bd
- exact integrable_of_bounded_measurable
- (hf_meas.comp (measurable_pi_apply 0) |>.mul (hg_meas.comp (measurable_pi_apply (j + 1))))
- (Cf * Cg)
- (fun ω => by simpa [abs_mul] using mul_le_mul (hCf (ω 0)) (hCg (ω (j + 1))) (abs_nonneg _) (le_trans (abs_nonneg _) (hCf (ω 0))))
+ have hmeas : Measurable fun ω : Ω[α] => f (ω 0) * g (ω (j + 1)) :=
+ (hf_meas.comp (measurable_pi_apply 0)).mul (hg_meas.comp (measurable_pi_apply (j + 1)))
+ exact Integrable.of_bound hmeas.aestronglyMeasurable (Cf * Cg)
+ (ae_of_all _ fun ω => by
+ simpa [abs_mul, Real.norm_eq_abs] using mul_le_mul (hCf (ω 0)) (hCg (ω (j + 1)))
+ (abs_nonneg _) (le_trans (abs_nonneg _) (hCf (ω 0))))
exact condExp_sum_finset (shiftInvariantSigma_le (α := α))
(Finset.range n) (fun j => fun ω => f (ω 0) * g (ω (j + 1))) hint
diff --git a/Exchangeability/DeFinetti/ViaKoopman/CesaroL1Bounded.lean b/Exchangeability/DeFinetti/ViaKoopman/CesaroL1Bounded.lean
index ed24719d..19c165e8 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/CesaroL1Bounded.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/CesaroL1Bounded.lean
@@ -198,16 +198,16 @@ lemma L1_cesaro_convergence
have h_integrable_diff : Integrable (fun ω => g (ω 0) - g_M M (ω 0)) μ := by
have h_g_M_int : Integrable (fun ω => g_M M (ω 0)) μ := by
obtain ⟨C, hC⟩ := hg_M_bd M
- refine Exchangeability.Probability.integrable_of_bounded ?_ ⟨C, fun ω => hC (ω 0)⟩
- exact (hg_M_meas M).comp (measurable_pi_apply 0)
+ exact Integrable.of_bound ((hg_M_meas M).comp (measurable_pi_apply 0)).aestronglyMeasurable
+ C (ae_of_all _ fun ω => hC (ω 0))
exact hg_int.sub h_g_M_int
have h_ce_lin : μ[(fun ω => g (ω 0) - g_M M (ω 0)) | mSI] =ᵐ[μ]
(fun ω => μ[(fun ω => g (ω 0)) | mSI] ω - μ[(fun ω => g_M M (ω 0)) | mSI] ω) := by
have h_int_g : Integrable (fun ω => g (ω 0)) μ := hg_int
have h_int_gM : Integrable (fun ω => g_M M (ω 0)) μ := by
obtain ⟨C, hC⟩ := hg_M_bd M
- refine Exchangeability.Probability.integrable_of_bounded ?_ ⟨C, fun ω => hC (ω 0)⟩
- exact (hg_M_meas M).comp (measurable_pi_apply 0)
+ exact Integrable.of_bound ((hg_M_meas M).comp (measurable_pi_apply 0)).aestronglyMeasurable
+ C (ae_of_all _ fun ω => hC (ω 0))
exact condExp_sub h_int_g h_int_gM mSI
calc ∫ ω, |μ[(fun ω => g (ω 0)) | mSI] ω - μ[(fun ω => g_M M (ω 0)) | mSI] ω| ∂μ
= ∫ ω, |μ[(fun ω => g (ω 0) - g_M M (ω 0)) | mSI] ω| ∂μ := by
@@ -252,8 +252,8 @@ lemma L1_cesaro_convergence
have h_int_ce_g : Integrable (μ[(fun ω => g (ω 0)) | mSI]) μ := integrable_condExp
have h_int_gM : Integrable (fun ω => g_M M₀ (ω 0)) μ := by
obtain ⟨C, hC⟩ := hg_M_bd M₀
- refine Exchangeability.Probability.integrable_of_bounded ?_ ⟨C, fun ω => hC (ω 0)⟩
- exact (hg_M_meas M₀).comp (measurable_pi_apply 0)
+ exact Integrable.of_bound ((hg_M_meas M₀).comp (measurable_pi_apply 0)).aestronglyMeasurable
+ C (ae_of_all _ fun ω => hC (ω 0))
have h_int_ce_gM : Integrable (μ[(fun ω => g_M M₀ (ω 0)) | mSI]) μ := integrable_condExp
have h_int_A : Integrable (A n) μ := by
@@ -275,8 +275,8 @@ lemma L1_cesaro_convergence
have h_each_int : ∀ j ∈ Finset.range (n + 1), Integrable (fun ω => g_M M₀ (ω j)) μ := by
intro j _
obtain ⟨C, hC⟩ := hg_M_bd M₀
- refine Exchangeability.Probability.integrable_of_bounded ?_ ⟨C, fun ω => hC (ω j)⟩
- exact (hg_M_meas M₀).comp (measurable_pi_apply j)
+ exact Integrable.of_bound ((hg_M_meas M₀).comp (measurable_pi_apply j)).aestronglyMeasurable
+ C (ae_of_all _ fun ω => hC (ω j))
exact integrable_finsetSum (Finset.range (n + 1)) h_each_int
exact h_int_sum.const_mul (1 / ((n + 1) : ℝ))
@@ -322,8 +322,8 @@ lemma L1_cesaro_convergence
exact (hσ.iterate j).integrable_comp_of_integrable hg_int
have h_int_gMj : Integrable (fun ω => g_M M₀ (ω j)) μ := by
obtain ⟨C, hC⟩ := hg_M_bd M₀
- refine Exchangeability.Probability.integrable_of_bounded ?_ ⟨C, fun ω => hC (ω j)⟩
- exact (hg_M_meas M₀).comp (measurable_pi_apply j)
+ exact Integrable.of_bound ((hg_M_meas M₀).comp (measurable_pi_apply j)).aestronglyMeasurable
+ C (ae_of_all _ fun ω => hC (ω j))
exact (h_int_gj.sub h_int_gMj).abs
exact h_sum_int.const_mul (1 / ((n + 1) : ℝ))
· filter_upwards with ω
@@ -340,8 +340,8 @@ lemma L1_cesaro_convergence
exact (hσ.iterate j).integrable_comp_of_integrable hg_int
have h_int_gMj : Integrable (fun ω => g_M M₀ (ω j)) μ := by
obtain ⟨C, hC⟩ := hg_M_bd M₀
- refine Exchangeability.Probability.integrable_of_bounded ?_ ⟨C, fun ω => hC (ω j)⟩
- exact (hg_M_meas M₀).comp (measurable_pi_apply j)
+ exact Integrable.of_bound ((hg_M_meas M₀).comp (measurable_pi_apply j)).aestronglyMeasurable
+ C (ae_of_all _ fun ω => hC (ω j))
exact (h_int_gj.sub h_int_gMj).abs
_ = (1 / (↑n + 1)) * ∑ j ∈ Finset.range (n + 1), ∫ ω, |g (ω 0) - g_M M₀ (ω 0)| ∂μ := by
congr 1
@@ -407,12 +407,13 @@ lemma ce_lipschitz_convergence
have hA_int : ∀ n, Integrable (A n) μ := fun n =>
(integrable_finsetSum (Finset.range (n + 1)) fun j _ =>
- integrable_of_bounded_measurable
- (hg_meas.comp (measurable_pi_apply j)) Cg fun ω => hCg (ω j)).smul (1 / ((n + 1) : ℝ))
+ Integrable.of_bound (f := fun ω : Ω[α] => g (ω j))
+ (hg_meas.comp (measurable_pi_apply j)).aestronglyMeasurable Cg
+ (ae_of_all _ fun ω => hCg (ω j))).smul (1 / ((n + 1) : ℝ))
have hg0_int : Integrable (fun ω => g (ω 0)) μ :=
- integrable_of_bounded_measurable
- (hg_meas.comp (measurable_pi_apply 0)) Cg (fun ω => hCg (ω 0))
+ Integrable.of_bound (hg_meas.comp (measurable_pi_apply 0)).aestronglyMeasurable Cg
+ (ae_of_all _ fun ω => hCg (ω 0))
have hZ_int : ∀ n, Integrable (fun ω => f (ω 0) * A n ω) μ := fun n =>
integrable_mul_of_ae_bdd_left (hf_meas.comp (measurable_pi_apply 0))
diff --git a/Exchangeability/DeFinetti/ViaKoopman/CesaroPairFactorization.lean b/Exchangeability/DeFinetti/ViaKoopman/CesaroPairFactorization.lean
index 7aab05cd..e07eaa23 100644
--- a/Exchangeability/DeFinetti/ViaKoopman/CesaroPairFactorization.lean
+++ b/Exchangeability/DeFinetti/ViaKoopman/CesaroPairFactorization.lean
@@ -108,8 +108,8 @@ private theorem h_tower_of_lagConst_from_one
(1 / ((n + 1) : ℝ)) * (Finset.range (n + 1)).sum (fun j => g (ω j))
-- By L1_cesaro_convergence: A_n → Y in L¹
have hg_int : Integrable (fun ω => g (ω 0)) μ :=
- integrable_of_bounded_measurable
- (hg_meas.comp (measurable_pi_apply 0)) Cg (fun ω => hCg (ω 0))
+ Integrable.of_bound (hg_meas.comp (measurable_pi_apply 0)).aestronglyMeasurable Cg
+ (ae_of_all _ fun ω => hCg (ω 0))
have h_A_to_Y := L1_cesaro_convergence hσ g hg_meas hg_int
-- A'_{n+1}(ω) = A_n(shift ω)
have h_eq : ∀ n ω, A' (n + 1) ω = A n (shift ω) := by
@@ -161,7 +161,8 @@ private theorem h_tower_of_lagConst_from_one
- μ[(fun ω' => f (ω' 0) * Y ω') | mSI] ω| ∂μ) atTop (𝓝 0) := by
-- Use ce_lipschitz_convergence with A' shifted by 1
have h_int : Integrable (fun ω => g (ω 0)) μ :=
- integrable_of_bounded_measurable (hg_meas.comp (measurable_pi_apply 0)) Cg (fun ω => hCg (ω 0))
+ Integrable.of_bound (hg_meas.comp (measurable_pi_apply 0)).aestronglyMeasurable Cg
+ (ae_of_all _ fun ω => hCg (ω 0))
-- A'_{n+1} has the form (1/(n+1)) * Σ_{j=0}^n g(shift ω)_j = A_n(shift ω)
-- Need to relate to ce_lipschitz_convergence format
-- ce_lipschitz_convergence needs: A_n defined as (1/(n+1)) * Σ g(ω_j)
@@ -178,8 +179,8 @@ private theorem h_tower_of_lagConst_from_one
simp only [A', if_neg (Nat.ne_of_gt hm)]
have h_sum : Integrable (fun ω => (Finset.range m).sum (fun j => g (ω (j + 1)))) μ :=
integrable_finsetSum (Finset.range m) (fun j _ =>
- integrable_of_bounded_measurable
- (hg_meas.comp (measurable_pi_apply (j + 1))) Cg (fun ω => hCg (ω (j + 1))))
+ Integrable.of_bound (hg_meas.comp (measurable_pi_apply (j + 1))).aestronglyMeasurable
+ Cg (ae_of_all _ fun ω => hCg (ω (j + 1))))
exact h_sum.smul (1 / (m : ℝ))
have hfA_int : Integrable (fun ω => f (ω 0) * A' (n + 1) ω) μ :=
integrable_mul_of_ae_bdd_left (hf_meas.comp (measurable_pi_apply 0))
diff --git a/Exchangeability/DeFinetti/ViaL2/CesaroConvergence/Cauchy.lean b/Exchangeability/DeFinetti/ViaL2/CesaroConvergence/Cauchy.lean
index eb4077fa..f07e2eff 100644
--- a/Exchangeability/DeFinetti/ViaL2/CesaroConvergence/Cauchy.lean
+++ b/Exchangeability/DeFinetti/ViaL2/CesaroConvergence/Cauchy.lean
@@ -3,9 +3,9 @@ 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.Fintype.Fin
import Exchangeability.DeFinetti.ViaL2.BlockAvgDef
import Exchangeability.Probability.CenteredVariables
-import Exchangeability.Util.FinsetHelpers
/-!
# Cesàro Cauchy Property: `blockAvg_cauchy_in_L2`
@@ -127,7 +127,7 @@ private lemma cesaro_cauchy_rho_lt
rw [Finset.sum_const]
_ = n • (n : ℝ)⁻¹ := by
congr 1
- exact Finset.filter_val_lt_card (le_max_left n n')
+ simpa using Fin.card_filter_val_lt.trans (min_eq_right (le_max_left n n'))
_ = 1 := by
rw [nsmul_eq_mul]
field_simp [Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hn_pos)]
@@ -156,7 +156,7 @@ private lemma cesaro_cauchy_rho_lt
rw [Finset.sum_const]
_ = n' • (n' : ℝ)⁻¹ := by
congr 1
- exact Finset.filter_val_lt_card (le_max_right n n')
+ simpa using Fin.card_filter_val_lt.trans (min_eq_right (le_max_right n n'))
_ = 1 := by
rw [nsmul_eq_mul]
field_simp [Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hn'_pos)]
@@ -184,8 +184,8 @@ private lemma cesaro_cauchy_rho_lt
simp only [sub_zero, ξ]
-- Z k.val is bounded, hence in L²
-- Same proof as for Z 0: |Z k.val| ≤ |f| + |m| ≤ 1 + 1 = 2
- apply memLp_two_of_bounded (hZ_meas k.val)
- intro ω
+ refine MemLp.of_bound (hZ_meas k.val).aestronglyMeasurable 2 (ae_of_all _ fun ω => ?_)
+ rw [Real.norm_eq_abs]
-- Unfold ξ and Z to show |f(X k.val ω) - m| ≤ 2
have h1 : |f (X k.val ω)| ≤ 1 := hf_bdd (X k.val ω)
have h2 : |∫ ω', f (X 0 ω') ∂μ| ≤ 1 := by
diff --git a/Exchangeability/Probability/CenteredVariables.lean b/Exchangeability/Probability/CenteredVariables.lean
index 4e080ebd..5603a35e 100644
--- a/Exchangeability/Probability/CenteredVariables.lean
+++ b/Exchangeability/Probability/CenteredVariables.lean
@@ -278,13 +278,11 @@ lemma correlation_coefficient_bounded
(hZ_var_uniform : ∀ i, ∫ ω, (Z i ω)^2 ∂μ = ∫ ω, (Z 0 ω)^2 ∂μ) :
-1 ≤ ρ ∧ ρ ≤ 1 := by
-- Z 0 and Z 1 are in L²(μ) since they are bounded by M
- have hZ0_L2 : MemLp (Z 0) 2 μ := by
- apply memLp_two_of_bounded (hZ_meas 0)
- exact hZ_bdd 0
+ have hZ0_L2 : MemLp (Z 0) 2 μ :=
+ MemLp.of_bound (hZ_meas 0).aestronglyMeasurable M (ae_of_all _ (hZ_bdd 0))
- have hZ1_L2 : MemLp (Z 1) 2 μ := by
- apply memLp_two_of_bounded (hZ_meas 1)
- exact hZ_bdd 1
+ have hZ1_L2 : MemLp (Z 1) 2 μ :=
+ MemLp.of_bound (hZ_meas 1).aestronglyMeasurable M (ae_of_all _ (hZ_bdd 1))
-- Apply Cauchy-Schwarz: |∫ Z₀·Z₁| ≤ sqrt(∫ Z₀²)·sqrt(∫ Z₁²)
have h_CS := Exchangeability.Probability.IntegrationHelpers.abs_integral_mul_le_L2 hZ0_L2 hZ1_L2
diff --git a/Exchangeability/Probability/CondExp.lean b/Exchangeability/Probability/CondExp.lean
index a4fd6549..73408188 100644
--- a/Exchangeability/Probability/CondExp.lean
+++ b/Exchangeability/Probability/CondExp.lean
@@ -394,16 +394,6 @@ section OperatorTheoretic
variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
-/-- Bounded measurable functions are integrable on finite measures.
-
-Wraps `Integrable.of_bound` so callers can pass `⟨C, hC⟩` directly instead of
-destructuring the bound first. -/
-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)⟩
-
/-- **Conditional expectation is L¹-nonexpansive** (load-bearing lemma).
For integrable functions f, g, the conditional expectation is contractive in L¹:
@@ -427,44 +417,6 @@ lemma condExp_L1_lipschitz [IsFiniteMeasure μ]
_ ≤ ∫ ω, |(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. -/
-lemma 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
- -- Use mathlib's condExp_stronglyMeasurable_mul_of_bound with explicit instance management
- -- following the pattern from condExpWith above.
-
- -- g is m-measurable, so it's m-strongly measurable
- have hg_strong : StronglyMeasurable[m] g := hg_meas.stronglyMeasurable
-
- -- g is bounded
- obtain ⟨C, hC⟩ := hg_bd
- have hg_bound : ∀ᵐ ω ∂μ, ‖g ω‖ ≤ C := ae_of_all μ fun ω => (Real.norm_eq_abs _).le.trans (hC ω)
-
- -- Provide typeclass instances explicitly (IsFiniteMeasure is automatic via mathlib)
- haveI : SigmaFinite (μ.trim hm) := inferInstance
-
- -- Now condExp_stronglyMeasurable_mul_of_bound can resolve instances
- have h := condExp_stronglyMeasurable_mul_of_bound hm hg_strong hf C hg_bound
-
- -- Commute to get μ[f * g|m] = μ[f|m] * g
- calc μ[f * g|m]
- =ᵐ[μ] μ[g * f|m] := by
- apply condExp_congr_ae
- filter_upwards with ω
- simp only [Pi.mul_apply]
- ring
- _ =ᵐ[μ] fun ω => g ω * μ[f|m] ω := h
- _ =ᵐ[μ] fun ω => μ[f|m] ω * g ω := by
- filter_upwards with ω
- ring
-
end OperatorTheoretic
end Exchangeability.Probability
diff --git a/Exchangeability/Probability/LpNormHelpers.lean b/Exchangeability/Probability/LpNormHelpers.lean
index 293b3201..df03a880 100644
--- a/Exchangeability/Probability/LpNormHelpers.lean
+++ b/Exchangeability/Probability/LpNormHelpers.lean
@@ -47,69 +47,18 @@ 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.
-
-**Proof strategy**: Use the definition of eLpNorm for p = 2, which involves
-lintegral of ‖f‖^2, and convert via toReal. -/
+the gap between ENNReal-valued Lp norms and Real-valued integrals. -/
lemma eLpNorm_two_sq_eq_integral_sq
- [IsFiniteMeasure μ] {f : Ω → ℝ}
+ {f : Ω → ℝ}
(hf : MemLp f 2 μ) :
(eLpNorm f 2 μ).toReal ^ 2 = ∫ ω, (f ω) ^ 2 ∂μ := by
- -- Strategy:
- -- 1. Use eLpNorm definition: eLpNorm f 2 μ = (∫⁻ ‖f‖²)^(1/2)
- -- 2. Square both sides: (eLpNorm f 2 μ)² = ∫⁻ ‖f‖²
- -- 3. Convert lintegral to integral: ∫⁻ ‖f‖² = ↑(∫ |f|²) = ↑(∫ f²)
-
- -- For real functions, ‖f‖² = |f|² = f²
- have h_norm_eq : ∀ ω, ‖f ω‖ ^ 2 = (f ω) ^ 2 :=
- fun _ => by rw [Real.norm_eq_abs, sq_abs]
-
- -- Use the fundamental relationship for p = 2
- -- eLpNorm f p μ ^ p = ∫⁻ ‖f‖^p when p ≠ 0, ∞
- rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by norm_num : (2 : ℝ≥0∞) ≠ 0)
- (by norm_num : (2 : ℝ≥0∞) ≠ ∞)]
-
- -- Simplify: ENNReal.toReal 2 = 2, so we have ((∫⁻ ‖f‖² )^(1/2)).toReal²
- simp only [ENNReal.toReal_ofNat]
-
- -- Main strategy: Show (∫⁻ ‖f‖²).toReal = ∫ f²
- -- Then use (a^(1/2))² = a to simplify the LHS
-
- -- Step 1: Rewrite LHS using ENNReal.toReal_rpow (backwards)
- -- We have ((∫⁻ ...)^(1/2)).toReal ^ 2 and want (∫⁻ ...).toReal
- conv_lhs => rw [← ENNReal.toReal_rpow]
-
- -- Step 2: Simplify (x^(1/2))^2 = x
- rw [← Real.rpow_natCast _ 2, ← Real.rpow_mul ENNReal.toReal_nonneg]
+ have h0 : 0 ≤ ∫ ω, ‖f ω‖ ^ (2 : ℝ≥0∞).toReal ∂μ :=
+ integral_nonneg fun ω => Real.rpow_nonneg (norm_nonneg _) _
+ rw [hf.eLpNorm_eq_integral_rpow_norm (by norm_num) (by norm_num),
+ ENNReal.toReal_ofReal (Real.rpow_nonneg h0 _),
+ ← Real.rpow_natCast _ 2, ← Real.rpow_mul h0]
norm_num
- -- Step 3: Convert lintegral to integral for nonnegative functions
- -- Key: ‖f ω‖ₑ = ↑‖f ω‖₊ where ‖·‖₊ is the nnnorm
- -- First rewrite the lintegral in terms of ofReal
- have h_enorm_conv : ∫⁻ (x : Ω), ‖f x‖ₑ ^ 2 ∂μ = ∫⁻ (x : Ω), ENNReal.ofReal (‖f x‖ ^ 2) ∂μ := by
- congr 1
- ext ω
- -- Show ‖f ω‖ₑ ^ 2 = ENNReal.ofReal (‖f ω‖ ^ 2)
- 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]
- -- Now use the fundamental relationship: (∫⁻ ofReal g).toReal = ∫ g for nonnegative g
- rw [← integral_eq_lintegral_of_nonneg_ae]
- · congr 1
- ext ω
- exact h_norm_eq ω
- · -- Nonnegativity: ‖f ω‖ ^ 2 ≥ 0
- apply ae_of_all
- intro ω
- exact sq_nonneg _
- · -- AE measurability
- apply AEStronglyMeasurable.pow
- exact 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.
@@ -145,30 +94,6 @@ lemma eLpNorm_lt_of_integral_sq_lt
/-! ### Membership in Lp Spaces -/
-/-- **Block average of bounded function is in L².**
-
-If `|f| ≤ M` everywhere on a probability space, then `f ∈ L²`. Used repeatedly in
-Cesàro convergence proofs. -/
-lemma memLp_two_of_bounded
- [IsProbabilityMeasure μ] {f : Ω → ℝ} {M : ℝ}
- (hf_meas : Measurable f)
- (hf_bdd : ∀ ω, |f ω| ≤ M) :
- MemLp f 2 μ := by
- refine MemLp.of_bound hf_meas.aestronglyMeasurable M ?_
- 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²). -/
diff --git a/Exchangeability/Probability/SigmaAlgebraHelpers.lean b/Exchangeability/Probability/SigmaAlgebraHelpers.lean
index eb13d522..3dcdb259 100644
--- a/Exchangeability/Probability/SigmaAlgebraHelpers.lean
+++ b/Exchangeability/Probability/SigmaAlgebraHelpers.lean
@@ -117,7 +117,11 @@ If `f n` are all Measurable[m] where `m ≤ m₀`, and `f n → g` a.e. (wrt a 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. -/
+we extract an a.e.-convergent subsequence and apply this.
+
+Note: mathlib's `aestronglyMeasurable_of_tendsto_ae` covers only the `m = m₀` case (its
+`AEStronglyMeasurable` is taken at the measure's own σ-algebra); this sub-σ-algebra version
+has no mathlib equivalent as of v4.30.0. -/
lemma aestronglyMeasurable_sub_of_tendsto_ae
{α : Type*} {m₀ : MeasurableSpace α} {μ : @MeasureTheory.Measure α m₀}
{m : MeasurableSpace α} (_hm : m ≤ m₀)
diff --git a/Exchangeability/Util/FinsetHelpers.lean b/Exchangeability/Util/FinsetHelpers.lean
deleted file mode 100644
index 003a68aa..00000000
--- a/Exchangeability/Util/FinsetHelpers.lean
+++ /dev/null
@@ -1,49 +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.Data.Finset.Card
-import Mathlib.Data.Fintype.Card
-
-/-!
-# Finset Helper Lemmas
-
-General-purpose lemmas about Finsets and Fin types.
-
-## Main Results
-
-* `Finset.filter_val_lt_card`: Cardinality of filtered Fin elements by value bound
--/
-
-namespace Finset
-
-/-- **Cardinality of filtered Fin elements.**
-
-For `m ≥ n`, the number of elements `i : Fin m` with `i.val < n` is exactly `n`.
-
-This is because `Fin m = {0, 1, ..., m-1}` contains all of `{0, 1, ..., n-1}` when `m ≥ n`,
-and these are precisely the elements satisfying `i.val < n`.
-
-The proof uses an explicit bijection between `Fin n` and the filtered set. -/
-lemma filter_val_lt_card {m n : ℕ} (h : m ≥ n) :
- (Finset.filter (fun i : Fin m => i.val < n) Finset.univ).card = n := by
- -- Establish bijection with Fin n via the natural inclusion
- let f : Fin n → Fin m := Fin.castLE h
-
- have hf_inj : Function.Injective f := Fin.castLE_injective h
-
- have h_image : Finset.filter (fun i : Fin m => i.val < n) Finset.univ =
- Finset.image f Finset.univ := by
- ext i
- simp only [mem_filter, mem_univ, true_and, mem_image]
- constructor
- · intro hi_lt
- exact ⟨⟨i.val, hi_lt⟩, Fin.ext rfl⟩
- · rintro ⟨j, rfl⟩
- exact j.isLt
-
- rw [h_image, card_image_of_injective _ hf_inj]
- simp only [card_univ, Fintype.card_fin]
-
-end Finset
diff --git a/Exchangeability/Util/StrictMono.lean b/Exchangeability/Util/StrictMono.lean
index d37a357f..f1a2a0d8 100644
--- a/Exchangeability/Util/StrictMono.lean
+++ b/Exchangeability/Util/StrictMono.lean
@@ -4,6 +4,7 @@ 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.Sort
import Mathlib.Data.Finset.Sort
/-!
@@ -73,78 +74,16 @@ lemma strictMono_Fin_ge_id {k : Fin m → ℕ} (hk : StrictMono k) (i : Fin m) :
/-- Any injective function `k : Fin m → ℕ` can be composed with a permutation
to become strictly monotone.
-**Construction:** Let `s := image k univ` (the image of k as a finset of ℕ).
-Since k is injective, `s.card = m`. The `orderIsoOfFin` gives the sorted
-enumeration of s. We define σ to map i to the position of k(i) in the sorted order.
-
-**Key property:** `(fun i => k (σ i))` is strictly increasing (sorted order).
+The permutation is `Tuple.sort k`; monotone-after-sorting plus injectivity gives
+strict monotonicity.
This is a key lemma for reducing proofs about injective index selections to
proofs about strictly monotone (consecutive-like) selections via contractability.
-/
lemma injective_implies_strictMono_perm
(k : Fin m → ℕ) (hk : Function.Injective k) :
- ∃ (σ : Equiv.Perm (Fin m)), StrictMono (fun i => k (σ i)) := by
- classical
- -- Define the image of k as a finset
- let s : Finset ℕ := Finset.image k Finset.univ
- -- By injectivity, s has cardinality m
- have hs : s.card = m := by
- simp only [s, Finset.card_image_of_injective Finset.univ hk, Finset.card_univ, Fintype.card_fin]
- -- Get the sorted enumeration of s
- let sorted : Fin m ≃o ↑s := Finset.orderIsoOfFin s hs
- -- For each i : Fin m, k(i) is in s, so we can find its sorted position
- have hk_mem : ∀ i : Fin m, k i ∈ s := by
- intro i
- simp only [s, Finset.mem_image, Finset.mem_univ, true_and]
- exact ⟨i, rfl⟩
- -- Define σ: for each position j in sorted order, find which i : Fin m maps to it
- -- sorted j gives the j-th smallest element of s
- -- We want σ such that k (σ j) = sorted j
- -- Define σ⁻¹ first: σ⁻¹(i) = sorted position of k(i)
- let σ_inv : Fin m → Fin m := fun i =>
- sorted.symm ⟨k i, hk_mem i⟩
- -- σ_inv is injective because sorted.symm and k are both injective
- have hσ_inv_inj : Function.Injective σ_inv := by
- intro i j hij
- simp only [σ_inv] at hij
- have h := sorted.symm.injective hij
- simp only [Subtype.mk.injEq] at h
- exact hk h
- -- Since σ_inv : Fin m → Fin m is injective, it's a bijection
- have hσ_inv_bij : Function.Bijective σ_inv := by
- rw [Fintype.bijective_iff_injective_and_card]
- exact ⟨hσ_inv_inj, rfl⟩
- -- Convert to an Equiv.Perm
- let σ : Equiv.Perm (Fin m) := Equiv.ofBijective σ_inv hσ_inv_bij
- -- Now σ.symm is the permutation we want
- use σ.symm
- -- Show k ∘ σ.symm is strictly monotone
- intro i j hij
- -- σ.symm(i) is the unique index such that σ_inv(σ.symm(i)) = i
- -- i.e., sorted position of k(σ.symm(i)) is i
- -- So k(σ.symm(i)) = sorted(i) (the i-th smallest element)
- have h_eq_i : k (σ.symm i) = ↑(sorted i) := by
- have h1 : σ_inv (σ.symm i) = i := by
- simp only [σ, Equiv.ofBijective_apply_symm_apply]
- simp only [σ_inv] at h1
- have h2 : sorted.symm ⟨k (σ.symm i), hk_mem (σ.symm i)⟩ = i := h1
- have h3 := sorted.apply_symm_apply ⟨k (σ.symm i), hk_mem (σ.symm i)⟩
- rw [h2] at h3
- exact Subtype.ext_iff.mp h3.symm
- have h_eq_j : k (σ.symm j) = ↑(sorted j) := by
- have h1 : σ_inv (σ.symm j) = j := by
- simp only [σ, Equiv.ofBijective_apply_symm_apply]
- simp only [σ_inv] at h1
- have h2 : sorted.symm ⟨k (σ.symm j), hk_mem (σ.symm j)⟩ = j := h1
- have h3 := sorted.apply_symm_apply ⟨k (σ.symm j), hk_mem (σ.symm j)⟩
- rw [h2] at h3
- exact Subtype.ext_iff.mp h3.symm
- -- Goal: (fun i => k (σ.symm i)) i < (fun i => k (σ.symm i)) j
- -- This simplifies to: k (σ.symm i) < k (σ.symm j)
- simp only
- rw [h_eq_i, h_eq_j]
- -- sorted is an OrderIso, so it's strictly monotone
- exact sorted.strictMono hij
+ ∃ (σ : Equiv.Perm (Fin m)), StrictMono (fun i => k (σ i)) :=
+ ⟨Tuple.sort k, (Tuple.monotone_sort k).strictMono_of_injective
+ (hk.comp (Tuple.sort k).injective)⟩
end Exchangeability.Util.StrictMono
diff --git a/STATUS.md b/STATUS.md
index f6f93b46..155a8468 100644
--- a/STATUS.md
+++ b/STATUS.md
@@ -1,6 +1,6 @@
# Project Status: de Finetti Theorem Formalization
-**Last Updated:** 2026-06-09
+**Last Updated:** 2026-06-10
## Executive Summary
@@ -11,9 +11,9 @@ LOC counts below cover the `Exchangeability/` library tree (excluding the top-le
|---------------|------:|-------|--------|
| **ViaMartingale** | 2,804 | Pass | **COMPLETE** |
| **ViaL2** | 7,443 | Pass | **COMPLETE** |
-| **ViaKoopman** | 5,305 | Pass | **COMPLETE** |
-| *Shared infrastructure* | 11,111 | — | — |
-| **Total** | **26,663** | Pass | **COMPLETE** |
+| **ViaKoopman** | 5,314 | Pass | **COMPLETE** |
+| *Shared infrastructure* | 10,881 | — | — |
+| **Total** | **26,442** | Pass | **COMPLETE** |
**All three proofs complete.**
diff --git a/blueprint/web/import_graph_colored.html b/blueprint/web/import_graph_colored.html
index f5ce0a05..b6dde420 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 6112f93b..8562429f 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 6ab2e3cb..a4a1def2 100644
--- a/blueprint/web/import_graph_colored.svg
+++ b/blueprint/web/import_graph_colored.svg
@@ -4,1746 +4,1732 @@
-