Upgrade to Lean v4.30.0 + mathlib v4.30.0 (stable)

DEVELOPMENT_CHRONOLOGY.md

@@ -156,7 +156,7 @@ Created `DirectingMeasure.lean` infrastructure for the identification chain: a s
 **226 commits (208 non-merge, `--since="2026-01-09 00:00"` on `main`) of post-completion upkeep**
 
 - `886550af` Toolchain upgrade to Lean 4.27.0-rc1, then `8ab88df2` to v4.30.0-rc2 with
-  matching mathlib
+  matching mathlib, then `f5c0dfa4` (June 2026) to the stable v4.30.0 tags
 - Cross-tree dead-code sweeps, e.g. `b642382e` (−1,713 lines) and follow-ups — several
   thousand lines of abandoned scaffolding removed
 - Linter hygiene: `3c40bcbf` cleared all 44 remaining linter warnings; suppressions pruned

Exchangeability/Bridge/CesaroToCondExp.lean

@@ -44,7 +44,7 @@ def pathify {Ω α : Type*} (X : ℕ → Ω → α) :
     Ω → PathSpace α :=
   fun ω n => X n ω
 
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_pathify {Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpace α] {X : ℕ → Ω → α}
     (hX_meas : ∀ n, Measurable (X n)) :
     Measurable (pathify X) :=

Exchangeability/Core.lean

@@ -82,7 +82,7 @@ omit [MeasurableSpace α] in
 lemma prefixProj_apply {n : ℕ} (x : ℕ → α) (i : Fin n) :
     prefixProj (α:=α) n x i = x i := rfl
 
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_prefixProj {n : ℕ} :
     Measurable (prefixProj (α:=α) n) := by
   unfold prefixProj; fun_prop
@@ -167,7 +167,7 @@ section Measurable
 
 
 
-@[measurability, fun_prop]
+@[fun_prop]
 private lemma takePrefix_measurable {m n : ℕ} (hmn : m ≤ n) :
     Measurable (takePrefix (α:=α) hmn) := by
   unfold takePrefix; fun_prop
@@ -343,7 +343,7 @@ omit [MeasurableSpace α] in
 lemma reindex_apply {π : Equiv.Perm ℕ} (x : ℕ → α) (i : ℕ) :
     reindex (α:=α) π x i = x (π i) := rfl
 
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_reindex {π : Equiv.Perm ℕ} :
     Measurable (reindex (α:=α) π) := by
   unfold reindex; fun_prop

Exchangeability/DeFinetti/L2Helpers.lean

@@ -213,11 +213,11 @@ private lemma integral_sq_weighted_sum_eq_double_sum {μ : Measure Ω}
           intro i _; apply Finset.sum_congr rfl
           intro j _; ring
     _ = ∑ i, ∑ j, ∫ ω, (c i * c j) * (η i ω * η j ω) ∂μ := by
-          rw [integral_finset_sum _ (fun i _ => ?_)]
+          rw [integral_finsetSum _ (fun i _ => ?_)]
           congr 1; ext i
-          rw [integral_finset_sum _ (fun j _ => ?_)]
+          rw [integral_finsetSum _ (fun j _ => ?_)]
           · exact (h_integrable i j).const_mul (c i * c j)
-          · exact integrable_finset_sum _ (fun j _ => (h_integrable i j).const_mul _)
+          · exact integrable_finsetSum _ (fun j _ => (h_integrable i j).const_mul _)
     _ = ∑ i, ∑ j, c i * c j * ∫ ω, η i ω * η j ω ∂μ := by
           congr 1; ext i; congr 1; ext j
           rw [integral_const_mul]

Exchangeability/DeFinetti/MartingaleHelpers.lean

@@ -43,7 +43,7 @@ variable {β : Type*} [MeasurableSpace β]
 /-- Shift a sequence by dropping the first `d` entries. -/
 def shiftSeq (d : ℕ) (f : ℕ → β) : ℕ → β := fun n => f (n + d)
 
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_shiftSeq {d : ℕ} :
     Measurable (shiftSeq (β:=β) d) := by
   unfold shiftSeq; fun_prop

Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean

@@ -84,7 +84,7 @@ lemma blockAvg_eq_cesaro_shifted {m n : ℕ} (hn : 0 < n) (k : Fin m) (f : α 
 
 /-! ### Measurability of Block Averages -/
 
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_blockAvg {m n : ℕ} (k : Fin m) {f : α → ℝ} (hf : Measurable f) :
     Measurable (blockAvg (α := α) m n k f) := by
   unfold blockAvg
@@ -447,7 +447,7 @@ lemma integral_prod_eq_integral_blockAvg
   rw [integral_const_mul]
 
   -- ∫ ∑_j ... = ∑_j ∫ ... (Fubini for finite sum)
-  rw [integral_finset_sum]
+  rw [integral_finsetSum]
   · -- Goal: ∫ ∏ fs(ωᵢ) = (1/n^m) * ∑_j ∫ ∏ fs(ω(i*n + j(i)))
     --
     -- By h_each_j: each ∫ ∏ fs(ω(i*n + j(i))) = ∫ ∏ fs(ωᵢ)

Exchangeability/DeFinetti/ViaKoopman/BlockInjection.lean

@@ -134,7 +134,7 @@ lemma reindexBlock_apply (m n : ℕ) (j : Fin m → Fin n) (ω : ℕ → α) (i
     reindexBlock m n j ω i = ω (blockInjection m n j i) := rfl
 
 /-- Reindexing by block injection is measurable. -/
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_reindexBlock (m n : ℕ) (j : Fin m → Fin n) :
     Measurable (reindexBlock (α := α) m n j) := by
   unfold reindexBlock; fun_prop

Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean

@@ -38,7 +38,7 @@ local notation "mSI" => shiftInvariantSigma (α := α)
 
 /-- Finite sum linearity of conditional expectation, stated with the sum applied
 pointwise (`fun ω => ∑ i ∈ s, f i ω`) as it appears in the Cesàro averages below.
-η-expands to mathlib's `condExp_finset_sum`. -/
+η-expands to mathlib's `condExp_finsetSum`. -/
 private lemma condExp_sum_finset
     {Ω : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
     {m : MeasurableSpace Ω} (_hm : m ≤ mΩ)
@@ -54,7 +54,7 @@ private lemma condExp_sum_finset
     funext ω
     simp only [Finset.sum_apply]
   rw [h_sum_eta, h_ce_sum_eta]
-  exact condExp_finset_sum hint m
+  exact condExp_finsetSum hint m
 
 lemma condexp_precomp_iterate_eq
     {μ : Measure (Ω[α])} [IsProbabilityMeasure μ]

Exchangeability/DeFinetti/ViaKoopman/CesaroL1Bounded.lean

@@ -266,7 +266,7 @@ lemma L1_cesaro_convergence
         rw [h_eq]
         have h_shiftj_pres : MeasurePreserving (shift^[j]) μ μ := hσ.iterate j
         exact h_shiftj_pres.integrable_comp_of_integrable hg_int
-      exact integrable_finset_sum (Finset.range (n + 1)) h_each_int
+      exact integrable_finsetSum (Finset.range (n + 1)) h_each_int
     exact h_int_sum.const_mul (1 / ((n + 1) : ℝ))
 
   have h_int_AM : Integrable A_M₀ μ := by
@@ -277,7 +277,7 @@ lemma L1_cesaro_convergence
         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_finset_sum (Finset.range (n + 1)) h_each_int
+      exact integrable_finsetSum (Finset.range (n + 1)) h_each_int
     exact h_int_sum.const_mul (1 / ((n + 1) : ℝ))
 
   have h_int_diff1 : Integrable (fun ω => |A n ω - A_M₀ ω|) μ := (h_int_A.sub h_int_AM).abs
@@ -314,7 +314,7 @@ lemma L1_cesaro_convergence
                 refine integral_mono_ae ?_ ?_ ?_
                 · exact (h_int_A.sub h_int_AM).abs
                 · have h_sum_int : Integrable (fun ω => ∑ j ∈ Finset.range (n + 1), |g (ω j) - g_M M₀ (ω j)|) μ := by
-                    refine integrable_finset_sum _ (fun j _ => ?_)
+                    refine integrable_finsetSum _ (fun j _ => ?_)
                     have h_int_gj : Integrable (fun ω => g (ω j)) μ := by
                       have h_eq : (fun ω => g (ω j)) = (fun ω => g ((shift^[j] ω) 0)) := by
                         simp [shift_iterate_apply_zero]
@@ -331,7 +331,7 @@ lemma L1_cesaro_convergence
                   rw [← mul_sub_left_distrib, ← Finset.sum_sub_distrib, abs_mul, abs_of_pos (by positivity : 0 < 1 / (↑n + 1 : ℝ))]
                   exact mul_le_mul_of_nonneg_left (Finset.abs_sum_le_sum_abs _ _) (by positivity)
             _ = (1 / (↑n + 1)) * ∑ j ∈ Finset.range (n + 1), ∫ ω, |g (ω j) - g_M M₀ (ω j)| ∂μ := by
-                rw [integral_const_mul, integral_finset_sum]
+                rw [integral_const_mul, integral_finsetSum]
                 intro j _
                 have h_int_gj : Integrable (fun ω => g (ω j)) μ := by
                   have h_eq : (fun ω => g (ω j)) = (fun ω => g ((shift^[j] ω) 0)) := by
@@ -406,7 +406,7 @@ lemma ce_lipschitz_convergence
   obtain ⟨Cg, hCg⟩ := hg_bd
 
   have hA_int : ∀ n, Integrable (A n) μ := fun n =>
-    (integrable_finset_sum (Finset.range (n + 1)) fun j _ =>
+    (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) : ℝ))
 

Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean

@@ -346,7 +346,7 @@ private lemma optionB_Step4b_AB_close
         have h_sum :
             Integrable (fun ω =>
               (Finset.range (n+1)).sum (fun i => g (ω i))) μ :=
-          integrable_finset_sum (Finset.range (n+1)) (fun i hi => h_i i hi)
+          integrable_finsetSum (Finset.range (n+1)) (fun i hi => h_i i hi)
         -- A n is (1/(n+1)) • (sum …)
         have h_smul :
             Integrable (fun ω =>
@@ -376,7 +376,7 @@ private lemma optionB_Step4b_AB_close
           have h_sum :
               Integrable (fun ω =>
                 (Finset.range n).sum (fun i => g (ω i))) μ :=
-            integrable_finset_sum (Finset.range n) (fun i hi => h_i i hi)
+            integrable_finsetSum (Finset.range n) (fun i hi => h_i i hi)
           have h_smul :
               Integrable (fun ω =>
                 (1 / (n : ℝ)) •

Exchangeability/DeFinetti/ViaKoopman/CesaroPairFactorization.lean

@@ -177,7 +177,7 @@ private theorem h_tower_of_lagConst_from_one
         intro m hm
         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_finset_sum (Finset.range m) (fun j _ =>
+          integrable_finsetSum (Finset.range m) (fun j _ =>
             integrable_of_bounded_measurable
               (hg_meas.comp (measurable_pi_apply (j + 1))) Cg (fun ω => hCg (ω (j + 1))))
         exact h_sum.smul (1 / (m : ℝ))

Exchangeability/DeFinetti/ViaKoopman/ContractableFactorization.lean

@@ -183,7 +183,7 @@ lemma product_blockAvg_L1_convergence
   --
   -- **Step 5**: Apply blockAvg_tendsto_condExp for each i.
   --   Each term ∫ |blockAvg_i - CE_i| → 0 by blockAvg_tendsto_condExp.
-  --   Finite sum of things → 0 is → 0 (by tendsto_finset_sum).
+  --   Finite sum of things → 0 is → 0 (by tendsto_finsetSum).
   --
   -- **Key ingredients from MoreL2Helpers.lean**:
   --   - abs_prod_sub_prod_le: |∏ f - ∏ g| ≤ ∑ |f_i - g_i| for |f|, |g| ≤ 1
@@ -213,7 +213,7 @@ lemma product_blockAvg_L1_convergence
     -- Sum of limits = limit of sums
     have h_sum_zero : (∑ _ : Fin m, (0 : ℝ)) = 0 := Finset.sum_const_zero
     rw [← h_sum_zero]
-    exact tendsto_finset_sum _ fun i _ =>
+    exact tendsto_finsetSum _ fun i _ =>
       blockAvg_tendsto_condExp hσ m i (hfs_meas i) ⟨C, fun x => hC_bd i x⟩
 
   -- Apply squeeze theorem
@@ -321,10 +321,10 @@ lemma product_blockAvg_L1_convergence
     calc ∫ ω, |∏ i, A i ω - ∏ i, B i ω| ∂μ
       _ ≤ ∫ ω, C^(m - 1) * ∑ i, |A i ω - B i ω| ∂μ :=
           integral_mono_ae (hprodA_int.sub hprodB_int).abs
-            ((integrable_finset_sum _ fun i _ => (hAB_diff_int i).abs).const_mul _) h_pointwise
+            ((integrable_finsetSum _ fun i _ => (hAB_diff_int i).abs).const_mul _) h_pointwise
       _ = C^(m - 1) * ∫ ω, ∑ i, |A i ω - B i ω| ∂μ := integral_const_mul _ _
       _ = C^(m - 1) * ∑ i, ∫ ω, |A i ω - B i ω| ∂μ := by
-          congr 1; exact integral_finset_sum _ fun i _ => (hAB_diff_int i).abs
+          congr 1; exact integral_finsetSum _ fun i _ => (hAB_diff_int i).abs
       _ = upper n := rfl
   · exact h_upper_tendsto
 
@@ -670,7 +670,7 @@ theorem condexp_product_factorization_contractable
       rw [h_rhs_eq]
 
       -- Swap finite sum and integral (integrability check below)
-      rw [integral_finset_sum Finset.univ]
+      rw [integral_finsetSum Finset.univ]
       · -- Now: ∫_s f = (1/(n+1)^m) * ∑_j ∫_s ∏_i fs_i(ω(i*(n+1) + j(i)))
         -- Use h_each_j_setIntegral and blockInjection_val_lt
         have h_each_term : ∀ j : Fin m → Fin (n + 1),

Exchangeability/DeFinetti/ViaKoopman/CylinderFunctions.lean

@@ -36,7 +36,7 @@ def productCylinder {m : ℕ} (fs : Fin m → α → ℝ) : (ℕ → α) → ℝ
   fun ω => ∏ k : Fin m, fs k (ω k.val)
 
 /-- Measurability of product cylinders. -/
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_productCylinder {m : ℕ} {fs : Fin m → α → ℝ}
     (hmeas : ∀ k, Measurable (fs k)) :
     Measurable (productCylinder fs) := by

Exchangeability/DeFinetti/ViaKoopman/DirectingKernel.lean

@@ -47,7 +47,7 @@ local notation "mSI" => shiftInvariantSigma (α := α)
 /-- Projection onto the first coordinate. -/
 def π0 : Ω[α] → α := fun ω => ω 0
 
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_pi0 : Measurable (π0 (α := α)) := measurable_pi_apply 0
 
 /-! ## Regular conditional distribution kernel -/
@@ -76,7 +76,7 @@ noncomputable def ν {μ : Measure (Ω[α])} [IsProbabilityMeasure μ]
   fun ω => (rcdKernel (μ := μ)) ω
 
 /-- ν evaluation on measurable sets is measurable in the parameter. -/
-@[measurability, fun_prop]
+@[fun_prop]
 lemma ν_eval_measurable
     {μ : Measure (Ω[α])} [IsProbabilityMeasure μ] [StandardBorelSpace α]
     {s : Set α} (hs : MeasurableSet s) :

Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean

@@ -111,7 +111,7 @@ def extendByZero (ω : Ω[α]) : Ωℤ[α] :=
   | Int.ofNat n => ω n
   | Int.negSucc _ => ω 0
 
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_shiftℤ : Measurable (shiftℤ (α := α)) := by
   unfold shiftℤ; fun_prop
 

Exchangeability/DeFinetti/ViaL2/AlphaIic.lean

@@ -81,7 +81,7 @@ noncomputable def alphaIic
       (indIic t) (indIic_measurable t) ⟨1, indIic_bdd t⟩).choose ω))
 
 /-- Measurability of the raw α_{Iic t}. -/
-@[measurability, fun_prop]
+@[fun_prop]
 lemma alphaIic_measurable
     {μ : Measure Ω} [IsProbabilityMeasure μ]
     (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X)
@@ -139,7 +139,7 @@ noncomputable def alphaIicRat
   fun ω q => alphaIic X hX_contract hX_meas hX_L2 (q : ℝ) ω
 
 /-- `alphaIicRat` is measurable, which is required for `stieltjesOfMeasurableRat`. -/
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_alphaIicRat
     {μ : Measure Ω} [IsProbabilityMeasure μ]
     (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X)

Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean

@@ -81,7 +81,7 @@ noncomputable def alphaIicCE
 The conditional expectation is strongly measurable with respect to the tail σ-algebra
 (`stronglyMeasurable_condExp`), and `Measurable.mono` lifts this to the ambient
 σ-algebra via `tailProcess_le_ambient`. -/
-@[measurability, fun_prop]
+@[fun_prop]
 lemma alphaIicCE_measurable
     {μ : Measure Ω} [IsProbabilityMeasure μ]
     (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X)

Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean

@@ -45,7 +45,7 @@ This is the building block for Kallenberg's L² convergence proof. -/
 def blockAvg (f : α → ℝ) (X : ℕ → Ω → α) (m n : ℕ) (ω : Ω) : ℝ :=
   (n : ℝ)⁻¹ * (Finset.range n).sum (fun k => f (X (m + k) ω))
 
-@[measurability, fun_prop]
+@[fun_prop]
 lemma blockAvg_measurable
     {Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpace α]
     (f : α → ℝ) (X : ℕ → Ω → α)

Exchangeability/DeFinetti/ViaL2/CesaroConvergence/L2.lean

@@ -165,7 +165,7 @@ private lemma blockAvg_shift_tendsto
 
   -- Step 5: Use squeeze theorem
   apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hUpper_tendsto
-  · exact Eventually.of_forall (fun _ => zero_le _)
+  · exact Eventually.of_forall (fun _ => zero_le)
   · rw [Filter.eventually_atTop]
     use 1
     intro m hm_pos
@@ -318,13 +318,13 @@ private lemma tendsto_setIntegral_of_L2_tendsto
   -- Step 1: L² → L¹ convergence on probability spaces (‖g‖₁ ≤ ‖g‖₂)
   have h1 : Tendsto (fun n => eLpNorm (fn n - f) 1 μ) atTop (𝓝 0) := by
     apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hL2
-    · intro n; exact zero_le _
+    · intro n; exact zero_le
     · intro n
       exact eLpNorm_le_eLpNorm_of_exponent_le one_le_two ((hfn n).sub hf).aestronglyMeasurable
   -- Step 2: Show each fn is integrable
   have hfn_int : ∀ n, Integrable (fn n) μ := fun n => (hfn n).integrable one_le_two
   -- Step 3: Apply tendsto_setIntegral_of_L1'
-  exact tendsto_setIntegral_of_L1' f (hf.integrable one_le_two)
+  exact tendsto_setIntegral_of_L1' f hf.aestronglyMeasurable
     (Filter.univ_mem' hfn_int) h1 A
 
 
@@ -513,7 +513,7 @@ lemma cesaro_to_condexp_L2
           exact MeasureTheory.integral_smul _ _
         rw [h_scalar]
         -- Sum pullout: ∫_A (∑ ...) = ∑ ∫_A ...
-        rw [MeasureTheory.integral_finset_sum _ (fun k _ => (hfXk_int k).integrableOn.integrable)]
+        rw [MeasureTheory.integral_finsetSum _ (fun k _ => (hfXk_int k).integrableOn.integrable)]
         -- Apply shift invariance: ∑ ∫_A f(X k) = ∑ ∫_A f(X 0) = n * ∫_A f(X 0)
         simp_rw [h_shift_eq]
         rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]

Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean

@@ -175,7 +175,7 @@ lemma directing_measure_measurable
           exact measure_iUnion hdisj (fun n => (hf n).1)
         simp_rw [h_union_eq]
         -- ∑' n, ν(ω)(f n) is measurable as tsum of measurable functions
-        exact Measurable.ennreal_tsum (fun n => (hf n).2)
+        exact Measurable.tsum (fun n => (hf n).2)
 
     -- Step 3: Apply π-λ theorem (induction_on_inter)
     -- The Borel σ-algebra on ℝ is generated by half-lines {Iic t | t ∈ ℝ}

Exchangeability/DeFinetti/ViaMartingale/DirectingMeasure.lean

@@ -59,7 +59,7 @@ noncomputable def directingMeasure
 /-- `directingMeasure` evaluates measurably on measurable sets.
 
 Uses: `Kernel.measurable_coe` and `Measure.map_apply`. -/
-@[measurability, fun_prop]
+@[fun_prop]
 lemma directingMeasure_measurable_eval
     {Ω : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
     {μ : Measure Ω} [IsProbabilityMeasure μ]

Exchangeability/DeFinetti/ViaMartingale/Factorization.lean

@@ -388,7 +388,7 @@ lemma tail_factorization_from_future
                   μ[Set.indicator (C i) (fun _ => (1 : ℝ)) ∘ (X 0) | tailSigma X] ω)) := by
     -- Product of tendsto gives tendsto of product (finitely many factors)
     filter_upwards [ae_all_iff.mpr h_rev] with ω hω
-    exact tendsto_finset_prod _ (fun i _ => hω i)
+    exact tendsto_finsetProd _ (fun i _ => hω i)
 
   -- Both LHS and RHS converge, and they're equal at each finite level for large m
   -- Therefore their limits are equal

Exchangeability/DeFinetti/ViaMartingale/KallenbergChain.lean

@@ -69,7 +69,7 @@ as a strictly increasing subsequence of X.
 def projectPairSeq : (ℕ → α) → α × (ℕ → α) :=
   fun f => (f 0, fun n => f (n + 1))
 
-@[measurability, fun_prop]
+@[fun_prop]
 lemma projectPairSeq_measurable : Measurable (projectPairSeq : (ℕ → α) → α × (ℕ → α)) :=
   by
     refine Measurable.prod (measurable_pi_apply (0 : ℕ)) ?_

Exchangeability/DeFinetti/ViaMartingale/ShiftOperations.lean

@@ -58,12 +58,12 @@ lemma tailRV_consRV (x : Ω → α) (t : Ω → ℕ → α) : tailRV (consRV x t
 /-! ### Measurable combinators -/
 
 /-- A process viewed as a full path is measurable. -/
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_path {X : ℕ → Ω → α} (hX : ∀ n, Measurable (X n)) : Measurable (path X) := by
   unfold path; fun_prop
 
 /-- Consing a head to a sequence is measurable if both pieces are measurable. -/
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_consRV (x : Ω → α) (t : Ω → ℕ → α) :
     Measurable x → Measurable t → Measurable (consRV x t) := by
   intro hx ht
@@ -97,7 +97,7 @@ lemma comap_le_comap_consRV (x : Ω → α) (t : Ω → ℕ → α) :
 
 variable {X : ℕ → Ω → α}
 
-@[measurability, fun_prop]
+@[fun_prop]
 lemma measurable_shiftRV (hX : ∀ n, Measurable (X n)) {m : ℕ} :
     Measurable (shiftRV X m) := by
   simpa [shiftRV, path] using (measurable_path (fun n => hX (m + n)))