Bump mathlib

YaelDillies · Dec 29, 2024 · 96de77c · 96de77c
1 parent 218a0d9
commit 96de77c
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 17 deletions.
diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean
@@ -233,7 +233,7 @@ lemma unbalancing' (p : ℕ) (hp : p ≠ 0) (ε : ℝ) (hε₀ : 0 < ε) (hε₁
       _ ≤ 2 * (2 ^ 7 * ε⁻¹ * (2 ^ 2 * ε⁻¹) * p) := by gcongr <;> norm_num
       _ = 2 ^ 10 * ε⁻¹ ^ 2 * p := by ring
   calc
-    _ ≤ ↑‖f + 1‖_[.ofReal (24 / ε * log (3 / ε) * ↑(2 * p + 3)), ν] :=
+    1 + ε / 2 ≤ ↑‖f + 1‖_[.ofReal (24 / ε * log (3 / ε) * ↑(2 * p + 3)), ν] :=
       unbalancing'' (2 * p + 3) this ((even_two_mul _).add_odd $ by decide) hε₀ hε₁ hf hν hν₁ $
         hε.trans $ wLpNorm_mono_right
           (Nat.cast_le.2 $ le_add_of_le_left $ le_mul_of_one_le_left' one_le_two) _ _

diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean
@@ -45,6 +45,7 @@ lemma ae_le_nnLinftyNorm (hf : Memℒp f ∞ μ) : ∀ᵐ x ∂μ, ‖f x‖₊
 lemma nnLinftyNorm_eq_essSup (hf : Memℒp f ∞ μ) : nnLpNorm f ∞ μ = essSup (‖f ·‖₊) μ := by
   refine ENNReal.coe_injective ?_
   rw [coe_nnLpNorm_eq_eLpNorm hf, ENNReal.coe_essSup, eLpNorm_exponent_top, eLpNormEssSup]
+  simp_rw [enorm_eq_nnnorm]
   exact ⟨_, ae_le_nnLinftyNorm hf⟩
 
 @[simp] lemma nnLpNorm_zero (p : ℝ≥0∞) (μ : Measure α) :

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c",
+   "rev": "43d30441447b3b8da2ae24e2091751feb743640c",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "90f062feea36adad53b81925aa9dc3e09c268262",
+   "rev": "68fbd252aa5d0168c5f582c0f66b3005dba683e1",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014",
+   "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
+   "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,27 +85,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
+   "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
+   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.46",
+   "inputRev": "v0.0.48",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "de91b59101763419997026c35a41432ac8691f15",
+   "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -115,17 +115,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.14.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dfbe9387054e2972449de7bf346059d3609529fa",
+   "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc3
+leanprover/lean4:v4.15.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.14.0-rc3
		leanprover/lean4:v4.15.0-rc1