From ed49b75e19cc8666641917503e85dd022d72188b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 20 Mar 2026 12:38:49 +0100 Subject: [PATCH] Bump mathlib to v4.28.0 --- PFR/MoreRuzsaDist.lean | 7 ++++--- PFR/MultiTauFunctional.lean | 11 +++-------- lake-manifest.json | 28 ++++++++++++++-------------- lakefile.toml | 1 + lean-toolchain | 2 +- 5 files changed, 23 insertions(+), 26 deletions(-) diff --git a/PFR/MoreRuzsaDist.lean b/PFR/MoreRuzsaDist.lean index e315ff49..73eda6e8 100644 --- a/PFR/MoreRuzsaDist.lean +++ b/PFR/MoreRuzsaDist.lean @@ -893,8 +893,7 @@ variable {G : Type uG} [hG : MeasurableSpace G] [AddCommGroup G] /-- Let `X_[m] = (X₁, ..., Xₘ)` be a non-empty finite tuple of `G`-valued random variables `X_i`. Then we define `D[X_[m]] = H[∑ i, X_i'] - 1/m*∑ i, H[X_i']`, where the `X_i'` are independent copies of the `X_i`. -/ -noncomputable -def multiDist {m : ℕ} {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i)) +@[expose] noncomputable def multiDist {m : ℕ} {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → G) : ℝ := H[fun x ↦ ∑ i, x i; .pi (fun i ↦ (hΩ i).volume.map (X i))] - (m:ℝ)⁻¹ * ∑ i, H[X i] @@ -2104,7 +2103,9 @@ lemma iter_multiDist_chainRule' {m : ℕ} (hm : m > 0) I[∑ i : Fin m, X i : fun ω i ↦ π d.succ (X i ω)| ⟨π d.succ ∘ ∑ i : Fin m, X i, fun ω i ↦ π d.castSucc (X i ω)⟩]) := by rw [← Fin.sum_univ_castSucc'] - congr! <;> rw [Fin.coeSucc_eq_succ] + congr! + any_goals rw [Fin.coeSucc_eq_succ] + simp_all _ ≥ _ := by rw [Finset.sum_add_distrib] gcongr diff --git a/PFR/MultiTauFunctional.lean b/PFR/MultiTauFunctional.lean index b48de987..fae4b1b3 100644 --- a/PFR/MultiTauFunctional.lean +++ b/PFR/MultiTauFunctional.lean @@ -279,10 +279,7 @@ lemma sub_condMultiDistance_le {G Ω₀ : Type u} [MeasurableFinGroup G] [Measur _ = ∏ i, ∑ ωi, Measure.real ℙ (Y i ⁻¹' {ωi}) := by convert Finset.sum_prod_piFinset Finset.univ _ with ω _ i _ rfl - _ = ∏ i, 1 := by - apply Finset.prod_congr rfl - intro i _ - exact probmes i + _ = ∏ i, 1 := by congr with i; exact probmes i _ = 1 := by simp only [Finset.prod_const_one] calc @@ -310,11 +307,9 @@ lemma sub_condMultiDistance_le {G Ω₀ : Type u} [MeasurableFinGroup G] [Measur exact sub_multiDistance_le hΩprob hmeasX h_min hΩ'prob_cond hmeasX' _ = p.η * ∑ i, ∑ ω, μ ω * d[X i ; (hΩ i).volume # X' i; ℙ[|Y i ⁻¹' {ω i}] ] := by rw [Finset.sum_comm, Finset.mul_sum] - apply Finset.sum_congr rfl - intro ω _ + congr with ω rw [Finset.mul_sum, Finset.mul_sum, Finset.mul_sum] - apply Finset.sum_congr rfl - intro i _ + congr with i ring _ = _ := by congr with i diff --git a/lake-manifest.json b/lake-manifest.json index 9bdae9b9..ed834ce3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,27 +15,27 @@ "type": "git", "subDir": null, "scope": "", - "rev": "13fd6dd3a47445b6dd10826f0ffc1116f4e13144", + "rev": "eba2c2b0e8309e19de76037c188dc14899729bce", "name": "APAP", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "v4.28.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "507f18fc9044549fc730d8d0270521e3b090360a", + "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "v4.28.0", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7311586e1a56af887b1081d05e80c11b6c41d212", + "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b5908dbac486279f1133cb937648c63c30b455af", + "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,17 +65,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294", + "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.86", + "inputRev": "v0.0.87", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0", + "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "23324752757bf28124a518ec284044c8db79fee5", + "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0100f1a3222df01286db33fcb6a1f98564f5439d", + "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,10 +105,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "28e0856d4424863a85b18f38868c5420c55f9bae", + "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0-rc1", + "inputRev": "v4.28.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "PFR", diff --git a/lakefile.toml b/lakefile.toml index 6d4e3c61..85f38c23 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -16,6 +16,7 @@ warn.sorry = false [[require]] name = "APAP" git = "https://github.com/YaelDillies/apap.git" +rev = "v4.28.0" [[require]] name = "checkdecls" diff --git a/lean-toolchain b/lean-toolchain index 3e9b4e15..ea6ca7ff 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.28.0-rc1 \ No newline at end of file +leanprover/lean4:v4.28.0 \ No newline at end of file