Simplify via mathlib v4.30.0: replace upstreamed/missed helpers

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

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
 

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))

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))

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

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

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