From edd247ec5f565b8d589da86267391c14334262ce Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Mon, 18 May 2026 14:44:37 +0000 Subject: [PATCH] chore: safe-subset golfing batch from #16 (fun_prop + named lemmas) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mines safe-subset replacements from the PR #16 autoGolf draft and applies them to current main, skipping the suspicious subset (lia / bare assumption / Real.ext_cauchy / grind only on non-arithmetic goals). `fun_prop` adoptions (replace hand-built `Measurable.const_mul + Finset.measurable_sum + .comp` chains): - `DeFinetti/ViaKoopman/BlockAverage.lean` (1 site) - `DeFinetti/ViaL2/BlockAvgDef.lean` (1 site) - `DeFinetti/ViaL2/AlphaConvergence.lean` (2 sites) - `DeFinetti/ViaL2/CesaroConvergence.lean` (3 sites) - `DeFinetti/ViaL2/DirectingMeasureIntegral.lean` (4 sites, incl. one Integrable wrap via `fun_prop`) - `DeFinetti/ViaL2/MainConvergence.lean` (1 site) - `DeFinetti/ViaMartingale/PairLawEquality.lean` (1 site, `measurable_consRV` → fun_prop) - `Ergodic/ShiftInvariantRepresentatives.lean` (1 site, `measurable_coe_real_ereal.comp …` → fun_prop) - `Core.lean:683` — collapse `simpa using (show … from by fun_prop)` to bare `fun_prop`. Named-lemma replacements: - `DeFinetti/ViaL2/DirectingMeasureIntegral.lean` 2× hand-built `IsPiSystem` proof for `Set.range Iic` → `isPiSystem_Iic`. - `Contractability.lean:perm_range_eq` — 4-line `ext`+`use`+`simp` → `Finset.image_univ_equiv σ`. Minor `by exact` removals in `BlockAvgDef.lean`. Out of scope (per the audit, suspicious-category from #16): - `BlockAverage.lean:82` `congr 1; ring` → `lia` swap (opaque substitution on non-arithmetic context). - The proof-golfing-branch reversion of #18's `exists_perm_extending_strictMono` refactor. Net -62 lines across 10 files. Build clean (3527 jobs), axioms standard, 0 sorries. No statement or signature changes. --- Exchangeability/Contractability.lean | 7 ++-- Exchangeability/Core.lean | 3 +- .../DeFinetti/ViaKoopman/BlockAverage.lean | 7 +--- .../DeFinetti/ViaL2/AlphaConvergence.lean | 11 ++---- .../DeFinetti/ViaL2/BlockAvgDef.lean | 14 +++----- .../DeFinetti/ViaL2/CesaroConvergence.lean | 14 ++------ .../ViaL2/DirectingMeasureIntegral.lean | 34 ++++--------------- .../DeFinetti/ViaL2/MainConvergence.lean | 5 +-- .../ViaMartingale/PairLawEquality.lean | 5 +-- .../ShiftInvariantRepresentatives.lean | 6 +--- 10 files changed, 22 insertions(+), 84 deletions(-) diff --git a/Exchangeability/Contractability.lean b/Exchangeability/Contractability.lean index 65f26108..1d4c3706 100644 --- a/Exchangeability/Contractability.lean +++ b/Exchangeability/Contractability.lean @@ -363,11 +363,8 @@ lemma Contractable.shift_and_select {μ : Measure Ω} {X : ℕ → Ω → α} /-- For a permutation σ on Fin n, the range {σ(0), ..., σ(n-1)} equals {0, ..., n-1}. -/ lemma perm_range_eq {n : ℕ} (σ : Equiv.Perm (Fin n)) : - Finset.image (fun i : Fin n => σ i) Finset.univ = Finset.univ := by - ext x - simp only [Finset.mem_image, Finset.mem_univ, true_and, iff_true] - use σ.symm x - simp + Finset.image (fun i : Fin n => σ i) Finset.univ = Finset.univ := + Finset.image_univ_equiv σ /-- Helper lemma: All values of a strictly monotone function are bounded by its last value plus one. diff --git a/Exchangeability/Core.lean b/Exchangeability/Core.lean index 7a878c8c..65625eea 100644 --- a/Exchangeability/Core.lean +++ b/Exchangeability/Core.lean @@ -679,8 +679,7 @@ theorem exchangeable_iff_fullyExchangeable {μ : Measure Ω} let μX := pathLaw (α:=α) μ X have hμ_univ : μ Set.univ = 1 := measure_univ have hμX_univ : μX Set.univ = 1 := by - have hX_meas : Measurable fun ω => fun i : ℕ => X i ω := by - simpa using (show Measurable (fun ω => fun i : ℕ => X i ω) from by fun_prop) + have hX_meas : Measurable fun ω => fun i : ℕ => X i ω := by fun_prop dsimp [μX, pathLaw] rw [Measure.map_apply_of_aemeasurable (hX_meas.aemeasurable) MeasurableSet.univ] simp [hμ_univ] diff --git a/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean b/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean index 4f6709d3..e02df983 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean +++ b/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean @@ -238,12 +238,7 @@ lemma blockAvg_tendsto_condExp -- 2. Use h_pres.map_eq to get ν = μ have h_smeas : StronglyMeasurable (fun ω : Ω[α] => |A n ω - Y ω|) := by -- A n is measurable (Cesàro average = const * finite sum of measurable functions) - have hA_meas : Measurable (A n) := by - simp only [A] - apply Measurable.const_mul - apply Finset.measurable_sum - intro j _ - exact hf.comp (measurable_pi_apply j) + have hA_meas : Measurable (A n) := by fun_prop -- Y is the conditional expectation, measurable via shiftInvariantSigma_le have hY_meas : Measurable Y := stronglyMeasurable_condExp.measurable.mono (shiftInvariantSigma_le (α := α)) le_rfl diff --git a/Exchangeability/DeFinetti/ViaL2/AlphaConvergence.lean b/Exchangeability/DeFinetti/ViaL2/AlphaConvergence.lean index 8d882440..e86894f5 100644 --- a/Exchangeability/DeFinetti/ViaL2/AlphaConvergence.lean +++ b/Exchangeability/DeFinetti/ViaL2/AlphaConvergence.lean @@ -153,12 +153,7 @@ lemma alphaIic_ae_eq_alphaIicCE -- Prove integrability of A n m have hA_int : Integrable (A n m) μ := by - have hA_meas_nm : Measurable (A n m) := by - simp only [A] - apply Measurable.const_mul - apply Finset.measurable_sum - intro k _ - exact (indIic_measurable t).comp (hX_meas _) + have hA_meas_nm : Measurable (A n m) := by fun_prop refine Integrable.of_bound hA_meas_nm.aestronglyMeasurable 1 ?_ filter_upwards with ω unfold A @@ -562,9 +557,7 @@ lemma alphaIic_ae_eq_alphaIicCE -- A n m is a Cesàro average of indIic ∘ X, which are measurable -- Each indIic ∘ X_i is measurable, sum is measurable, scalar mult is measurable refine Measurable.aestronglyMeasurable ?_ - show Measurable fun ω => (1 / (m : ℝ)) * ∑ k : Fin m, indIic t (X (n + k.val + 1) ω) - refine Measurable.const_mul ?_ _ - exact Finset.measurable_sum _ (fun k _ => (indIic_measurable t).comp (hX_meas _)) + fun_prop -- Step 3: Use uniqueness of L¹ limits to conclude a.e. equality -- If both f and g are L¹ limits of the same sequence, then f =ᵐ g diff --git a/Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean b/Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean index a630b264..5dc15801 100644 --- a/Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean +++ b/Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean @@ -54,13 +54,7 @@ lemma blockAvg_measurable Measurable (fun ω => blockAvg f X m n ω) := by classical unfold blockAvg - have hsum : - Measurable (fun ω => - (Finset.range n).sum (fun k => f (X (m + k) ω))) := - Finset.measurable_sum _ (by - intro k _ - exact hf.comp (hX (m + k))) - simpa using (measurable_const.mul hsum : Measurable _) + fun_prop @[nolint unusedArguments] lemma blockAvg_abs_le_one @@ -75,8 +69,8 @@ lemma blockAvg_abs_le_one have hsum_bound : |(Finset.range n).sum (fun k => f (X (m + k) ω))| ≤ (n : ℝ) := by calc |(Finset.range n).sum (fun k => f (X (m + k) ω))| - ≤ (Finset.range n).sum (fun k => |f (X (m + k) ω)|) := by - exact Finset.abs_sum_le_sum_abs (fun k => f (X (m + k) ω)) (Finset.range n) + ≤ (Finset.range n).sum (fun k => |f (X (m + k) ω)|) := + Finset.abs_sum_le_sum_abs (fun k => f (X (m + k) ω)) (Finset.range n) _ ≤ (Finset.range n).sum (fun _ => (1 : ℝ)) := by apply Finset.sum_le_sum intro k _ @@ -84,7 +78,7 @@ lemma blockAvg_abs_le_one _ = n := by have : (Finset.range n).card = n := Finset.card_range n simp [this] - have hnonneg : 0 ≤ (n : ℝ)⁻¹ := by exact inv_nonneg.mpr (by exact_mod_cast Nat.zero_le n) + have hnonneg : 0 ≤ (n : ℝ)⁻¹ := inv_nonneg.mpr (by exact_mod_cast Nat.zero_le n) calc |(n : ℝ)⁻¹ * (Finset.range n).sum (fun k => f (X (m + k) ω))| = (n : ℝ)⁻¹ * |(Finset.range n).sum (fun k => f (X (m + k) ω))| diff --git a/Exchangeability/DeFinetti/ViaL2/CesaroConvergence.lean b/Exchangeability/DeFinetti/ViaL2/CesaroConvergence.lean index 7e7db9ce..9e1f6d59 100644 --- a/Exchangeability/DeFinetti/ViaL2/CesaroConvergence.lean +++ b/Exchangeability/DeFinetti/ViaL2/CesaroConvergence.lean @@ -1327,15 +1327,9 @@ private lemma cesaro_cauchy_rho_lt -- Use memLp_of_abs_le_const from LpNormHelpers -- Show measurability - have h_meas_n : Measurable (fun ω => blockAvg f X 0 n ω) := by - simp only [blockAvg] - exact Measurable.const_mul (Finset.measurable_sum _ fun k _ => - hf_meas.comp (hX_meas (0 + k))) _ + have h_meas_n : Measurable (fun ω => blockAvg f X 0 n ω) := by fun_prop - have h_meas_n' : Measurable (fun ω => blockAvg f X 0 n' ω) := by - simp only [blockAvg] - exact Measurable.const_mul (Finset.measurable_sum _ fun k _ => - hf_meas.comp (hX_meas (0 + k))) _ + have h_meas_n' : Measurable (fun ω => blockAvg f X 0 n' ω) := by fun_prop have h_meas_diff : Measurable (fun ω => blockAvg f X 0 n ω - blockAvg f X 0 n' ω) := h_meas_n.sub h_meas_n' @@ -2329,9 +2323,7 @@ lemma cesaro_to_condexp_L2 -- blockAvg is bounded since f is bounded apply memLp_two_of_bounded · -- Measurable: blockAvg is a finite sum of measurable functions - show Measurable (fun ω => (n : ℝ)⁻¹ * (Finset.range n).sum (fun k => f (X (0 + k) ω))) - exact Measurable.const_mul (Finset.measurable_sum _ fun k _ => - hf_meas.comp (hX_meas (0 + k))) _ + fun_prop intro ω -- |blockAvg f X 0 n ω| ≤ 1 since |f| ≤ 1 show |(n : ℝ)⁻¹ * (Finset.range n).sum (fun k => f (X (0 + k) ω))| ≤ 1 diff --git a/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean b/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean index d86b7419..22d53082 100644 --- a/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean +++ b/Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean @@ -686,12 +686,7 @@ lemma integral_indicator_borel_tailAEStronglyMeasurable let S : Set (Set ℝ) := Set.range (Set.Iic : ℝ → Set ℝ) have h_gen : (inferInstance : MeasurableSpace ℝ) = MeasurableSpace.generateFrom S := @borel_eq_generateFrom_Iic ℝ _ _ _ _ - have h_pi_S : IsPiSystem S := by - intro u hu v hv _ - obtain ⟨s, rfl⟩ := hu - obtain ⟨t, rfl⟩ := hv - use min s t - exact Set.Iic_inter_Iic.symm + have h_pi_S : IsPiSystem S := isPiSystem_Iic have h_induction : ∀ t (htm : MeasurableSet t), t ∈ G := fun t htm => MeasurableSpace.induction_on_inter h_gen h_pi_S @@ -1202,12 +1197,7 @@ lemma setIntegral_directing_measure_indicator_eq let S : Set (Set ℝ) := Set.range (Set.Iic : ℝ → Set ℝ) have h_gen : (inferInstance : MeasurableSpace ℝ) = MeasurableSpace.generateFrom S := @borel_eq_generateFrom_Iic ℝ _ _ _ _ - have h_pi_S : IsPiSystem S := by - intro u hu v hv _ - obtain ⟨r, rfl⟩ := hu - obtain ⟨t, rfl⟩ := hv - use min r t - exact Set.Iic_inter_Iic.symm + have h_pi_S : IsPiSystem S := isPiSystem_Iic have h_induction : ∀ t (htm : MeasurableSet t), t ∈ G := fun t htm => MeasurableSpace.induction_on_inter h_gen h_pi_S @@ -1818,9 +1808,7 @@ lemma directing_measure_integral_via_chain simp only [hω, sub_self, abs_zero, Pi.zero_apply] · -- Integrability: α_g - condExp is in L¹ have hα_g_int : Integrable α_g μ := hα_g_L2.integrable one_le_two - have hcond_int : Integrable (μ[g ∘ X 0 | TailSigma.tailSigma X]) μ := - integrable_condExp - exact (hα_g_int.sub hcond_int).norm + fun_prop -- Triangle inequality: g-averages → α_g in L¹ have hg_to_alpha_g : ∀ ε > 0, ∃ M_idx : ℕ, ∀ m ≥ M_idx, @@ -1836,10 +1824,7 @@ lemma directing_measure_integral_via_chain apply integral_mono_of_nonneg (ae_of_all μ (fun _ => abs_nonneg _)) · apply Integrable.add · have hg_avg_meas : Measurable (fun ω => (1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω)) := by - apply Measurable.const_mul - apply Finset.measurable_sum - intro k _ - exact hg_meas.comp (hX_meas (k.val + 1)) + fun_prop have hg_avg_bdd : ∀ ω, |(1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω)| ≤ 1 := by intro ω by_cases hm : m = 0 @@ -1870,10 +1855,7 @@ lemma directing_measure_integral_via_chain ∫ ω, |μ[g ∘ X 0 | TailSigma.tailSigma X] ω - α_g ω| ∂μ := by apply integral_add · have hg_avg_meas : Measurable (fun ω => (1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω)) := by - apply Measurable.const_mul - apply Finset.measurable_sum - intro k _ - exact hg_meas.comp (hX_meas (k.val + 1)) + fun_prop have hg_avg_bdd : ∀ ω, |(1/(m:ℝ)) * ∑ k : Fin m, g (X (k.val+1) ω)| ≤ 1 := by intro ω by_cases hm : m = 0 @@ -1941,11 +1923,7 @@ lemma directing_measure_integral_via_chain -- Both A → alpha and A → M * α_g in L¹ -- First convert L¹ convergence to eLpNorm convergence - have hA_meas : ∀ m, Measurable (A m) := fun m => by - apply Measurable.const_mul - apply Finset.measurable_sum - intro k _ - exact hf_meas.comp (hX_meas (k.val + 1)) + have hA_meas : ∀ m, Measurable (A m) := fun m => by fun_prop have hA_bdd : ∀ m ω, |A m ω| ≤ M := fun m ω => by simp only [A] diff --git a/Exchangeability/DeFinetti/ViaL2/MainConvergence.lean b/Exchangeability/DeFinetti/ViaL2/MainConvergence.lean index 54a286a3..c5ecedb8 100644 --- a/Exchangeability/DeFinetti/ViaL2/MainConvergence.lean +++ b/Exchangeability/DeFinetti/ViaL2/MainConvergence.lean @@ -80,10 +80,7 @@ theorem weighted_sums_converge_L1 have hA_meas : ∀ n m, Measurable (A n m) := by intro n m simp only [A] - apply Measurable.const_mul - apply Finset.measurable_sum - intro k _ - exact hf_meas.comp (hX_meas _) + fun_prop -- A n m is in L¹ for all n, m (bounded measurable on probability space) have hA_memLp : ∀ n m, MemLp (A n m) 1 μ := by diff --git a/Exchangeability/DeFinetti/ViaMartingale/PairLawEquality.lean b/Exchangeability/DeFinetti/ViaMartingale/PairLawEquality.lean index efe8a89e..177ab41b 100644 --- a/Exchangeability/DeFinetti/ViaMartingale/PairLawEquality.lean +++ b/Exchangeability/DeFinetti/ViaMartingale/PairLawEquality.lean @@ -353,10 +353,7 @@ lemma comap_consRV_eq_sup ext ω n cases n <;> simp [Function.comp_apply, consSeq, consRV] -- consSeq is measurable - have h_consSeq_meas : Measurable consSeq := by - simpa [consSeq] using - (measurable_consRV (x := fun q : α × (ℕ → α) => q.1) - (t := fun q : α × (ℕ → α) => q.2) measurable_fst measurable_snd) + have h_consSeq_meas : Measurable consSeq := by fun_prop -- So consRV x t ⁻¹' S = (fun ω => (x ω, t ω)) ⁻¹' (consSeq ⁻¹' S) rw [h_factor, Set.preimage_comp] -- consSeq ⁻¹' S is measurable in α × (ℕ → α) diff --git a/Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean b/Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean index 14bd47fe..6a9cf16f 100644 --- a/Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean +++ b/Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean @@ -101,11 +101,7 @@ def gRep (g0 : Ω[α] → ℝ) : Ω[α] → ℝ := @[measurability, fun_prop] lemma gRep_measurable {g0 : Ω[α] → ℝ} (hg0 : Measurable g0) : Measurable (gRep g0) := by - have hstep : ∀ n : ℕ, Measurable fun ω => (g0 (shift^[n] ω) : EReal) := by - intro n - have hreal : Measurable fun ω => g0 (shift^[n] ω) := - hg0.comp (shift_iterate_measurable (α := α) n) - exact measurable_coe_real_ereal.comp hreal + have hstep : ∀ n : ℕ, Measurable fun ω => (g0 (shift^[n] ω) : EReal) := by fun_prop have h_meas_ereal : Measurable fun ω => gLimsupE g0 ω := by simpa [gLimsupE] using (Measurable.limsup hstep) have : Measurable fun ω => (gLimsupE g0 ω).toReal := by