chore: safe-subset golfing batch from #16 (fun_prop + named lemmas) (−62 lines)

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.

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]

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

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

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,16 +69,16 @@ 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 _
           exact hf_bdd (X (m + k) ω)
       _ = 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) ω))|

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

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]

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

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 α × (ℕ → α)

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