chore: safe-subset mathlib cleanup batch (bdd_mul, iterate, pi prob, indicator) (−31 lines)

Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean

@@ -95,14 +95,6 @@ lemma eventuallyEq_comp_measurePreserving {f g : Ω[α] → ℝ}
     (f ∘ shift) =ᵐ[μ] (g ∘ shift) :=
   hT.quasiMeasurePreserving.ae_eq_comp hfg
 
-/-- Iterate of a measure-preserving map is measure-preserving. -/
-@[nolint unusedArguments]
-lemma MeasurePreserving.iterate' (hT : MeasurePreserving shift μ μ) (k : ℕ) :
-    MeasurePreserving (shift^[k]) μ μ := by
-  induction k with
-  | zero => exact MeasurePreserving.id μ
-  | succ k ih => simp only [Function.iterate_succ']; exact hT.comp ih
-
 /-- General evaluation formula for shift iteration. -/
 @[nolint unusedArguments]
 lemma iterate_shift_eval' (k n : ℕ) (ω : Ω[α]) :
@@ -688,7 +680,7 @@ theorem optionB_L1_convergence_bounded
         (fun ω => g (ω k)) := by
       intro k
       -- fL2 = G a.e., and shift^[k] is measure-preserving
-      have hk_pres := MeasurePreserving.iterate' hσ k
+      have hk_pres := hσ.iterate k
       -- Pull hfL2_eq back along shift^[k] using measure-preserving property
       have hpull : (fun ω => (fL2 : Ω[α] → ℝ) (shift^[k] ω)) =ᵐ[μ]
           (fun ω => G (shift^[k] ω)) := by

Exchangeability/DeFinetti/ViaKoopman/InfraGeneralized.lean

@@ -556,7 +556,7 @@ lemma integrable_mul_of_ae_bdd_left
   have hZ_norm : ∀ᵐ ω ∂μ, ‖Z ω‖ ≤ C := by
     filter_upwards [hC] with ω hω
     rwa [Real.norm_eq_abs]
-  exact Integrable.bdd_mul' hY hZ.aestronglyMeasurable hZ_norm
+  exact Integrable.bdd_mul hY hZ.aestronglyMeasurable hZ_norm
 
 /-- Conditional expectation is L¹-Lipschitz: moving the integrand changes the CE by at most
 the L¹ distance. This is a standard property following from Jensen's inequality. -/

Exchangeability/DeFinetti/ViaMartingale.lean

@@ -278,12 +278,12 @@ lemma integral_mul_condexp_adjoint_Linfty
   classical
   -- Both products are integrable
   have h_int1 : Integrable (fun ω => g ω * μ[ξ | m] ω) μ :=
-    Integrable.bdd_mul' (MeasureTheory.integrable_condExp (m := m) (f := ξ))
+    Integrable.bdd_mul (MeasureTheory.integrable_condExp (m := m) (f := ξ))
       hg.aestronglyMeasurable hgC
   have hμgC : ∀ᵐ ω ∂μ, |μ[g | m] ω| ≤ C :=
     @ae_bound_condexp_of_ae_bound Ω m0 μ m hm _ _ _ hgC
   have h_int2 : Integrable (fun ω => μ[g | m] ω * ξ ω) μ :=
-    Integrable.bdd_mul' hξ
+    Integrable.bdd_mul hξ
       (MeasureTheory.integrable_condExp (m := m) (f := g)).aestronglyMeasurable hμgC
 
   -- Now copy the "adjointness by CE" argument, which is safe since both products are L¹.

Exchangeability/Probability/CondIndep/Indicator.lean

@@ -57,26 +57,6 @@ survives conditioning on W.
    transfers to the conditional expectations.
 -/
 
--- Product of two unit indicator functions equals the indicator of the intersection.
-private lemma mul_indicator_one_eq_indicator_inter {Ω : Type*} (S T : Set Ω) :
-    (S.indicator (fun _ => (1 : ℝ))) * (T.indicator (fun _ => (1 : ℝ)))
-      = (S ∩ T).indicator (fun _ => (1 : ℝ)) := by
-  classical
-  ext ω
-  simp only [Pi.mul_apply]
-  by_cases hS : ω ∈ S <;> by_cases hT : ω ∈ T
-  · rw [Set.indicator_of_mem hS, Set.indicator_of_mem hT]
-    have : ω ∈ S ∩ T := ⟨hS, hT⟩
-    rw [Set.indicator_of_mem this]; norm_num
-  · rw [Set.indicator_of_mem hS, Set.indicator_of_notMem hT]
-    have : ω ∉ S ∩ T := fun h => hT h.2
-    rw [Set.indicator_of_notMem this]; norm_num
-  · rw [Set.indicator_of_notMem hS, Set.indicator_of_mem hT]
-    have : ω ∉ S ∩ T := fun h => hS h.1
-    rw [Set.indicator_of_notMem this]; norm_num
-  · rw [Set.indicator_of_notMem hS, Set.indicator_of_notMem hT]
-    have : ω ∉ S ∩ T := fun h => hS h.1
-    rw [Set.indicator_of_notMem this]; norm_num
 
 -- Product of indicators composed with functions equals indicator of product set composed with pair.
 private lemma mul_indicator_comp_pair_eq_indicator_prod {Ω α β : Type*}
@@ -159,7 +139,7 @@ theorem condIndep_of_indep_pair (μ : Measure Ω) [IsProbabilityMeasure μ]
   have hfg_meas : Measurable (f * g) := hf_meas.mul hg_meas
   have hfg_int : Integrable (f * g) μ := by
     rw [show f * g = (Y ⁻¹' A ∩ Z ⁻¹' B).indicator (fun _ => (1 : ℝ))
-          from mul_indicator_one_eq_indicator_inter (Y ⁻¹' A) (Z ⁻¹' B)]
+          from (Set.inter_indicator_one (s := Y ⁻¹' A) (t := Z ⁻¹' B)).symm]
     exact (integrable_const (1 : ℝ)).indicator ((hY hA).inter (hZ hB))
   have hfg_ce : μ[f * g | MeasurableSpace.comap W (by infer_instance)] =ᵐ[μ] (fun _ => μ[f * g]) :=
     condExp_const_of_indepFun μ hfg_meas hW hfg_indep hfg_int

Exchangeability/Probability/MeasureKernels.lean

@@ -196,13 +196,10 @@ lemma measurable_measure_pi {Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpac
       measurable_prod_ennreal (fun i ω => ν ω (B i)) hfac
     simpa [κ, rect]
 
-  -- Each product measure is a probability measure
-  have hκ_prob : ∀ ω, IsProbabilityMeasure (κ ω) := by
-    intro ω
-    classical
+  -- Each product measure is a probability measure (via `Measure.pi.instIsProbabilityMeasure`)
+  have hκ_prob : ∀ ω, IsProbabilityMeasure (κ ω) := fun ω => by
     haveI : ∀ _ : Fin m, IsProbabilityMeasure (ν ω) := fun _ => hν_prob ω
-    simp only [κ]
-    infer_instance
+    simp only [κ]; infer_instance
 
   -- Apply π-λ theorem to extend measurability from rectangles to all measurable sets
   exact Measurable.measure_of_isPiSystem_of_isProbabilityMeasure

Exchangeability/Probability/TripleLawDropInfo/DropInfo.lean

@@ -150,13 +150,13 @@ lemma condExp_indicator_eq_of_law_eq_of_comap_le
     rw [Real.norm_eq_abs, abs_le]; constructor <;> linarith
 
   have hμ₁sq_int : Integrable (fun ω => μ₁ ω * μ₁ ω) μ :=
-    Integrable.bdd_mul' hμ₁_int hμ₁_int.aestronglyMeasurable hμ₁_bound
+    Integrable.bdd_mul hμ₁_int hμ₁_int.aestronglyMeasurable hμ₁_bound
 
   have hμ₂sq_int : Integrable (fun ω => μ₂ ω * μ₂ ω) μ :=
-    Integrable.bdd_mul' hμ₂_int hμ₂_int.aestronglyMeasurable hμ₂_bound
+    Integrable.bdd_mul hμ₂_int hμ₂_int.aestronglyMeasurable hμ₂_bound
 
   have hμ₂μ₁_int : Integrable (fun ω => μ₂ ω * μ₁ ω) μ :=
-    Integrable.bdd_mul' hμ₁_int hμ₂_int.aestronglyMeasurable hμ₂_bound
+    Integrable.bdd_mul hμ₁_int hμ₂_int.aestronglyMeasurable hμ₂_bound
 
   -- Step 4a: Cross term E[μ₂μ₁] = E[μ₁²] using pull-out + tower
   have h_cross : ∫ ω, μ₂ ω * μ₁ ω ∂μ = ∫ ω, μ₁ ω * μ₁ ω ∂μ := by
@@ -204,7 +204,7 @@ lemma condExp_indicator_eq_of_law_eq_of_comap_le
       have h_sq_eq_mul : ∀ ω, (μ₂ ω - μ₁ ω)^2 = (μ₂ - μ₁) ω * (μ₂ - μ₁) ω := fun ω => by
         simp only [Pi.sub_apply]; ring
       simp_rw [h_sq_eq_mul]
-      exact Integrable.bdd_mul' h_diff_int h_diff_int.aestronglyMeasurable h_diff_bound
+      exact Integrable.bdd_mul h_diff_int h_diff_int.aestronglyMeasurable h_diff_bound
     exact (integral_eq_zero_iff_of_nonneg_ae h_nonneg h_sq_int).mp h_L2_zero
 
   -- (μ₂ - μ₁)² = 0 implies μ₂ = μ₁