From f5c0dfa4ae7aaf2f6fe5069dfd812957c96a941c Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Wed, 10 Jun 2026 14:47:15 +0000 Subject: [PATCH 1/4] chore(bump): Lean v4.30.0 + mathlib v4.30.0 Bumps the toolchain and mathlib pin from v4.30.0-rc2 to the stable v4.30.0 tags. No source changes in this commit; any build fixups follow separately. - lean-toolchain: leanprover/lean4:v4.30.0-rc2 -> v4.30.0 - lakefile.toml: mathlib rev v4.30.0-rc2 -> v4.30.0 - lake-manifest.json: regenerated via lake update mathlib (mathlib c5ea0035; aesop/Qq/Cli -> v4.30.0; proofwidgets v0.0.98 -> v0.0.99; batteries -> main pin per mathlib manifest; plausible/importGraph bumped; checkdecls/LeanSearchClient unchanged) --- lake-manifest.json | 28 ++++++++++++++-------------- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 16 insertions(+), 16 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index eb185bd1..48bc3206 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,17 +15,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6", + "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "v4.30.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8", + "rev": "a456461b368b71d2accd95234832cd9c174b5437", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cdab3938ccabbdb044be6896e251b5814bec932e", + "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,50 +55,50 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2db6054a44326f8c0230ee0570e2ddb894816511", + "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.98", + "inputRev": "v0.0.99", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5", + "rev": "558915ae105bfd8074e22d597613d1961822adc2", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809", + "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", + "rev": "32dc18cde3684679f3c003de608743b57498c56f", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", + "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "exchangeability", diff --git a/lakefile.toml b/lakefile.toml index b6722a3c..13650b49 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -5,7 +5,7 @@ defaultTargets = ["Exchangeability"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" -rev = "v4.30.0-rc2" +rev = "v4.30.0" [[require]] name = "checkdecls" diff --git a/lean-toolchain b/lean-toolchain index 6c7e31ff..af9e5d33 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0-rc2 +leanprover/lean4:v4.30.0 From 2d813068cea525aecbaa67b6ab06ea8000782a2c Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Wed, 10 Jun 2026 14:55:54 +0000 Subject: [PATCH 2/4] fix(bump): adapt CesaroConvergence/L2 to v4.30.0 stable API - zero_le (ENNReal) no longer takes its argument explicitly (2 sites) - tendsto_setIntegral_of_L1' now takes AEStronglyMeasurable f instead of Integrable f - integral_finset_sum -> integral_finsetSum (deprecation in this file) --- Exchangeability/DeFinetti/ViaL2/CesaroConvergence/L2.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Exchangeability/DeFinetti/ViaL2/CesaroConvergence/L2.lean b/Exchangeability/DeFinetti/ViaL2/CesaroConvergence/L2.lean index 04c1fa49..369253d0 100644 --- a/Exchangeability/DeFinetti/ViaL2/CesaroConvergence/L2.lean +++ b/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] From 621d4389f44f9d583247dfdb0a0dfc21460e055e Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Wed, 10 Jun 2026 15:01:51 +0000 Subject: [PATCH 3/4] chore: clear all v4.30.0 stable deprecation warnings (45 -> 0) - finset_sum/finset_prod camelCase renames: integral_finsetSum, integrable_finsetSum, condExp_finsetSum, tendsto_finsetSum, tendsto_finsetProd; Measurable.ennreal_tsum -> Measurable.tsum - @[measurability, fun_prop] on Measurable lemmas -> @[fun_prop] (the measurability attribute is deprecated for function-property statements); the 3 MeasurableSet lemmas keep @[measurability] since fun_prop does not accept set-measurability statements --- Exchangeability/Bridge/CesaroToCondExp.lean | 2 +- Exchangeability/Core.lean | 6 +++--- Exchangeability/DeFinetti/L2Helpers.lean | 6 +++--- Exchangeability/DeFinetti/MartingaleHelpers.lean | 2 +- Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean | 4 ++-- .../DeFinetti/ViaKoopman/BlockInjection.lean | 2 +- .../DeFinetti/ViaKoopman/CesaroHelpers.lean | 4 ++-- .../DeFinetti/ViaKoopman/CesaroL1Bounded.lean | 10 +++++----- Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean | 4 ++-- .../DeFinetti/ViaKoopman/CesaroPairFactorization.lean | 2 +- .../ViaKoopman/ContractableFactorization.lean | 10 +++++----- .../DeFinetti/ViaKoopman/CylinderFunctions.lean | 2 +- .../DeFinetti/ViaKoopman/DirectingKernel.lean | 4 ++-- Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean | 2 +- Exchangeability/DeFinetti/ViaL2/AlphaIic.lean | 4 ++-- Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean | 2 +- Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean | 2 +- Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean | 2 +- .../DeFinetti/ViaMartingale/DirectingMeasure.lean | 2 +- .../DeFinetti/ViaMartingale/Factorization.lean | 2 +- .../DeFinetti/ViaMartingale/KallenbergChain.lean | 2 +- .../DeFinetti/ViaMartingale/ShiftOperations.lean | 6 +++--- .../Ergodic/ShiftInvariantRepresentatives.lean | 2 +- Exchangeability/Ergodic/ShiftInvariantSigma.lean | 2 +- Exchangeability/PathSpace/CylinderHelpers.lean | 4 ++-- Exchangeability/PathSpace/Shift.lean | 4 ++-- Exchangeability/Probability/MeasureKernels.lean | 2 +- 27 files changed, 48 insertions(+), 48 deletions(-) diff --git a/Exchangeability/Bridge/CesaroToCondExp.lean b/Exchangeability/Bridge/CesaroToCondExp.lean index f291460e..e6c0c3ea 100644 --- a/Exchangeability/Bridge/CesaroToCondExp.lean +++ b/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) := diff --git a/Exchangeability/Core.lean b/Exchangeability/Core.lean index 82e924ad..5070be1d 100644 --- a/Exchangeability/Core.lean +++ b/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 diff --git a/Exchangeability/DeFinetti/L2Helpers.lean b/Exchangeability/DeFinetti/L2Helpers.lean index 384e39bc..4e0025df 100644 --- a/Exchangeability/DeFinetti/L2Helpers.lean +++ b/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] diff --git a/Exchangeability/DeFinetti/MartingaleHelpers.lean b/Exchangeability/DeFinetti/MartingaleHelpers.lean index 4c9ba040..295bf166 100644 --- a/Exchangeability/DeFinetti/MartingaleHelpers.lean +++ b/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 diff --git a/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean b/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean index 865b70c8..5a33077e 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/BlockAverage.lean +++ b/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(ωᵢ) diff --git a/Exchangeability/DeFinetti/ViaKoopman/BlockInjection.lean b/Exchangeability/DeFinetti/ViaKoopman/BlockInjection.lean index 0e37355f..913a36e5 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/BlockInjection.lean +++ b/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 diff --git a/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean b/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean index d1a83232..e9dfcf4a 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean +++ b/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 μ] diff --git a/Exchangeability/DeFinetti/ViaKoopman/CesaroL1Bounded.lean b/Exchangeability/DeFinetti/ViaKoopman/CesaroL1Bounded.lean index e41bf31d..ed24719d 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/CesaroL1Bounded.lean +++ b/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) : ℝ)) diff --git a/Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean b/Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean index 8ef92ea8..52c296fb 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean +++ b/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 : ℝ)) • diff --git a/Exchangeability/DeFinetti/ViaKoopman/CesaroPairFactorization.lean b/Exchangeability/DeFinetti/ViaKoopman/CesaroPairFactorization.lean index 3b48b823..7aab05cd 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/CesaroPairFactorization.lean +++ b/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 : ℝ)) diff --git a/Exchangeability/DeFinetti/ViaKoopman/ContractableFactorization.lean b/Exchangeability/DeFinetti/ViaKoopman/ContractableFactorization.lean index d18b11d4..4c5184ec 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/ContractableFactorization.lean +++ b/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), diff --git a/Exchangeability/DeFinetti/ViaKoopman/CylinderFunctions.lean b/Exchangeability/DeFinetti/ViaKoopman/CylinderFunctions.lean index 50cc4ec2..566d3803 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/CylinderFunctions.lean +++ b/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 diff --git a/Exchangeability/DeFinetti/ViaKoopman/DirectingKernel.lean b/Exchangeability/DeFinetti/ViaKoopman/DirectingKernel.lean index 5f53951e..376e8ef5 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/DirectingKernel.lean +++ b/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) : diff --git a/Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean b/Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean index be3eb35b..0aced824 100644 --- a/Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean +++ b/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 diff --git a/Exchangeability/DeFinetti/ViaL2/AlphaIic.lean b/Exchangeability/DeFinetti/ViaL2/AlphaIic.lean index 67974437..dd87f10f 100644 --- a/Exchangeability/DeFinetti/ViaL2/AlphaIic.lean +++ b/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) diff --git a/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean b/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean index 5afaa5d9..e8891ee9 100644 --- a/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean +++ b/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) diff --git a/Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean b/Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean index 663f1fe7..6d8a1d54 100644 --- a/Exchangeability/DeFinetti/ViaL2/BlockAvgDef.lean +++ b/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 : ℕ → Ω → α) diff --git a/Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean b/Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean index f5e15bfb..a8721a67 100644 --- a/Exchangeability/DeFinetti/ViaL2/MoreL2Helpers.lean +++ b/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 ∈ ℝ} diff --git a/Exchangeability/DeFinetti/ViaMartingale/DirectingMeasure.lean b/Exchangeability/DeFinetti/ViaMartingale/DirectingMeasure.lean index bb83a91d..308c7c82 100644 --- a/Exchangeability/DeFinetti/ViaMartingale/DirectingMeasure.lean +++ b/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 μ] diff --git a/Exchangeability/DeFinetti/ViaMartingale/Factorization.lean b/Exchangeability/DeFinetti/ViaMartingale/Factorization.lean index 72d961ee..55283795 100644 --- a/Exchangeability/DeFinetti/ViaMartingale/Factorization.lean +++ b/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 diff --git a/Exchangeability/DeFinetti/ViaMartingale/KallenbergChain.lean b/Exchangeability/DeFinetti/ViaMartingale/KallenbergChain.lean index 9f363589..d716a886 100644 --- a/Exchangeability/DeFinetti/ViaMartingale/KallenbergChain.lean +++ b/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 : ℕ)) ?_ diff --git a/Exchangeability/DeFinetti/ViaMartingale/ShiftOperations.lean b/Exchangeability/DeFinetti/ViaMartingale/ShiftOperations.lean index 7fdcd7af..cf2fb2bf 100644 --- a/Exchangeability/DeFinetti/ViaMartingale/ShiftOperations.lean +++ b/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))) diff --git a/Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean b/Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean index 29d23d82..3f0eca79 100644 --- a/Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean +++ b/Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean @@ -98,7 +98,7 @@ def gRep (g0 : Ω[α] → ℝ) : Ω[α] → ℝ := fun ω => (gLimsupE g0 ω).toReal -@[measurability, fun_prop] +@[fun_prop] lemma gRep_measurable {g0 : Ω[α] → ℝ} (hg0 : Measurable g0) : Measurable (gRep g0) := by have hstep : ∀ n : ℕ, Measurable fun ω => (g0 (shift^[n] ω) : EReal) := by fun_prop diff --git a/Exchangeability/Ergodic/ShiftInvariantSigma.lean b/Exchangeability/Ergodic/ShiftInvariantSigma.lean index 9551284f..b34358ec 100644 --- a/Exchangeability/Ergodic/ShiftInvariantSigma.lean +++ b/Exchangeability/Ergodic/ShiftInvariantSigma.lean @@ -150,7 +150,7 @@ lemma shiftInvariantSigma_measurable_shift_eq exact lt_irrefl _ this -- Helper: Measurability of iterated shifts follows from measurability of `shift`. -@[measurability, fun_prop] +@[fun_prop] lemma shift_iterate_measurable (n : ℕ) : Measurable (shift^[n] : Ω[α] → Ω[α]) := by simpa using measurable_shift.iterate n diff --git a/Exchangeability/PathSpace/CylinderHelpers.lean b/Exchangeability/PathSpace/CylinderHelpers.lean index 2e1361ef..07f7a3e7 100644 --- a/Exchangeability/PathSpace/CylinderHelpers.lean +++ b/Exchangeability/PathSpace/CylinderHelpers.lean @@ -97,8 +97,8 @@ lemma firstRCylinder_measurable_ambient /-- The firstRMap is measurable when all coordinates are measurable. File-private — the only caller is `firstRSigma_le_ambient` directly below; if a future external file needs this, lift the privacy and re-register the -`@[measurability, fun_prop]` attributes. -/ -@[measurability, fun_prop] +`@[fun_prop]` attributes. -/ +@[fun_prop] private lemma measurable_firstRMap (X : ℕ → Ω → α) (r : ℕ) (hX : ∀ i, Measurable (X i)) : Measurable (firstRMap X r) := by diff --git a/Exchangeability/PathSpace/Shift.lean b/Exchangeability/PathSpace/Shift.lean index 2aa7ffe8..58b92138 100644 --- a/Exchangeability/PathSpace/Shift.lean +++ b/Exchangeability/PathSpace/Shift.lean @@ -65,12 +65,12 @@ lemma shift_apply (ξ : ℕ → α) (n : ℕ) : shift ξ n = ξ (n + 1) := rfl Since `(shift ξ) i = ξ (i + 1)`, this is the projection onto coordinate `(i + 1)`, which is measurable by definition of the product σ-algebra. -/ -@[measurability, fun_prop] +@[fun_prop] lemma shift_measurable [MeasurableSpace α] : Measurable (@shift α) := by unfold shift; fun_prop /- Alternative name for `shift_measurable` (used in ergodic theory contexts). -/ -@[measurability, fun_prop] +@[fun_prop] lemma measurable_shift [MeasurableSpace α] : Measurable (@shift α) := shift_measurable /-- A set in the path space is **shift-invariant** if it equals its preimage under the shift. diff --git a/Exchangeability/Probability/MeasureKernels.lean b/Exchangeability/Probability/MeasureKernels.lean index bb1cfff7..ed9da613 100644 --- a/Exchangeability/Probability/MeasureKernels.lean +++ b/Exchangeability/Probability/MeasureKernels.lean @@ -148,7 +148,7 @@ This is a key lemma for proving the ConditionallyIID property in de Finetti's th yield measurable kernels, which is essential for disintegration theory and conditional independence. -/ -@[measurability, fun_prop] +@[fun_prop] lemma measurable_measure_pi {Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpace α] {m : ℕ} (ν : Ω → Measure α) (hν_prob : ∀ ω, IsProbabilityMeasure (ν ω)) From 79be697c1020e110f9b9b4457ee52cfb4c904292 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Wed, 10 Jun 2026 15:10:27 +0000 Subject: [PATCH 4/4] docs(chronology): note stable v4.30.0 bump in Phase 11 --- DEVELOPMENT_CHRONOLOGY.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DEVELOPMENT_CHRONOLOGY.md b/DEVELOPMENT_CHRONOLOGY.md index 68f70ada..3005680e 100644 --- a/DEVELOPMENT_CHRONOLOGY.md +++ b/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