From 7156e346667e42b28fa19c4b5ea79a6f2a9d8649 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Mon, 18 May 2026 02:15:30 +0000 Subject: [PATCH] chore: safe-subset mathlib cleanup batch (bdd_mul, iterate, pi prob, indicator) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Four small, independent mathlib-alignment cleanups, all proof-body-only with statements unchanged. Net -31 lines. 1) Integrable.bdd_mul' → Integrable.bdd_mul (deprecated alias). 7 sites: - DeFinetti/ViaMartingale.lean (2) - DeFinetti/ViaKoopman/InfraGeneralized.lean (1) - Probability/TripleLawDropInfo/DropInfo.lean (4) 2) Delete local MeasurePreserving.iterate' wrapper in DeFinetti/ViaKoopman/CesaroL2ToL1.lean. The single caller switches to the dot-notation form `hσ.iterate k` which resolves directly to mathlib's `MeasurePreserving.iterate`. 3) Shorten the per-ω probability-measure proof for product kernels in Probability/MeasureKernels.lean (`hκ_prob`). The block already used typeclass inference to find `Measure.pi.instIsProbabilityMeasure`; collapse the surrounding plumbing from 6 lines to 3 and name the instance in a leading comment. 4) Delete the private wrapper `mul_indicator_one_eq_indicator_inter` in Probability/CondIndep/Indicator.lean. Its single caller switches to `(Set.inter_indicator_one ..).symm` from mathlib. Out of scope: the related manual case-splits in DeFinetti/ViaMartingale/IndicatorAlgebra.lean (`indProd_mul`) don't have a clean named-lemma replacement; left as-is. --- .../DeFinetti/ViaKoopman/CesaroL2ToL1.lean | 10 +-------- .../ViaKoopman/InfraGeneralized.lean | 2 +- Exchangeability/DeFinetti/ViaMartingale.lean | 4 ++-- .../Probability/CondIndep/Indicator.lean | 22 +------------------ .../Probability/MeasureKernels.lean | 9 +++----- .../TripleLawDropInfo/DropInfo.lean | 8 +++---- 6 files changed, 12 insertions(+), 43 deletions(-) diff --git a/Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean b/Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean index 4c2b8f0a..bb3eee12 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean +++ b/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 diff --git a/Exchangeability/DeFinetti/ViaKoopman/InfraGeneralized.lean b/Exchangeability/DeFinetti/ViaKoopman/InfraGeneralized.lean index 405074c1..bb4d1bd5 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/InfraGeneralized.lean +++ b/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. -/ diff --git a/Exchangeability/DeFinetti/ViaMartingale.lean b/Exchangeability/DeFinetti/ViaMartingale.lean index fd61c021..8a8465fe 100644 --- a/Exchangeability/DeFinetti/ViaMartingale.lean +++ b/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¹. diff --git a/Exchangeability/Probability/CondIndep/Indicator.lean b/Exchangeability/Probability/CondIndep/Indicator.lean index a583e7c6..f754477f 100644 --- a/Exchangeability/Probability/CondIndep/Indicator.lean +++ b/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 diff --git a/Exchangeability/Probability/MeasureKernels.lean b/Exchangeability/Probability/MeasureKernels.lean index 86026448..e6bdc911 100644 --- a/Exchangeability/Probability/MeasureKernels.lean +++ b/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 diff --git a/Exchangeability/Probability/TripleLawDropInfo/DropInfo.lean b/Exchangeability/Probability/TripleLawDropInfo/DropInfo.lean index 1910497f..a3358deb 100644 --- a/Exchangeability/Probability/TripleLawDropInfo/DropInfo.lean +++ b/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 μ₂ = μ₁