chore: bump toolchain to v4.18.0-rc1 (#256)

Author: pitmonticone

Carleson/Antichain/TileCorrelation.lean

@@ -340,12 +340,12 @@ lemma uncertainty (ha : 1 ≤ a) {p₁ p₂ : 𝔓 X} (hle : 𝔰 p₁ ≤ 𝔰
             apply add_le_add_right
             norm_cast
             nth_rewrite 1 [← pow_one 2]
-            exact Nat.pow_le_pow_of_le_right zero_lt_two (by omega)
+            exact Nat.pow_le_pow_right zero_lt_two (by omega)
           _ = 2 * (2 : ℝ)^ (6 * a) := by ring
           _ ≤ 2 ^ (a * 8) := by
             nth_rewrite 1 [← pow_one 2, ← pow_add]
             norm_cast
-            exact Nat.pow_le_pow_of_le_right zero_lt_two (by omega)
+            exact Nat.pow_le_pow_right zero_lt_two (by omega)
       have h38 : 3 ≤ 8 := by omega
       have h12 : (1 : ℝ) ≤ 2 := by linarith
       rw [C_6_2_3]

Carleson/ForestOperator/LargeSeparation.lean

@@ -482,7 +482,8 @@ lemma enorm_ψ_le_edist {y : X} (my : y ∈ E p) (hx' : x' ∉ ball (𝔠 p) (5
     _ = (edist x x' / D ^ (𝔰 p) * 4) ^ (a : ℝ)⁻¹ := by
       rw [enorm_mul]; nth_rw 2 [enorm_eq_nnnorm]; rw [Real.nnnorm_ofNat, ENNReal.coe_ofNat]; congr
       rw [enorm_eq_nnnorm, nnnorm_div, nnnorm_zpow]; norm_cast
-      rw [ENNReal.coe_div (by simp; positivity), ENNReal.coe_zpow (by simp)]; norm_cast; congr
+      rw [ENNReal.coe_div (by simp only [defaultD, Nat.cast_pow, Nat.cast_ofNat, defaultA,
+        defaultκ.eq_1, ne_eq]; positivity), ENNReal.coe_zpow (by simp)]; norm_cast; congr
       rw [edist_dist, ← Real.enorm_of_nonneg dist_nonneg, enorm_eq_nnnorm]
     _ ≤ _ := by
       rw [ENNReal.mul_rpow_of_nonneg _ _ (by positivity), mul_comm]; gcongr
@@ -822,7 +823,7 @@ lemma holder_correlation_tile (hu : u ∈ t) (hp : p ∈ t u) (hf : BoundedCompa
   exact holder_correlation_tile_two hu hp hf hx hx'
 
 /-- Part of Lemma 7.5.6. -/
-lemma limited_scale_impact__first_estimate (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+lemma limited_scale_impact_first_estimate (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
     (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)
     (h : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J))) : s J ≤ 𝔰 p := by
   by_contra! contr
@@ -874,7 +875,7 @@ lemma limited_scale_impact__first_estimate (hu₁ : u₁ ∈ t) (hu₂ : u₂ 
   norm_cast
 
 /-- Part of Lemma 7.5.6. -/
-lemma limited_scale_impact__second_estimate (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)
+lemma limited_scale_impact_second_estimate (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)
     (h : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J))) :
     𝔰 p ≤ s J + 3 := by
   by_contra! three
@@ -938,8 +939,8 @@ lemma limited_scale_impact (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁
     (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)
     (h : ¬ Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J))) :
     𝔰 p ∈ Icc (s J) (s J + 3) :=
-  ⟨limited_scale_impact__first_estimate hu₁ hu₂ hu h2u hp hJ h,
-    limited_scale_impact__second_estimate hp hJ h⟩
+  ⟨limited_scale_impact_first_estimate hu₁ hu₂ hu h2u hp hJ h,
+    limited_scale_impact_second_estimate hp hJ h⟩
 
 lemma local_tree_control_sumsumsup (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
     (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf : BoundedCompactSupport f) :

Carleson/ForestOperator/PointwiseEstimate.lean

@@ -389,7 +389,7 @@ private lemma L7_1_4_integrand_bound (hu : u ∈ t) {s : ℤ} (hs : s ∈ t.σ u
     gcongr
     norm_cast
     rw_mod_cast [← pow_add]
-    refine Nat.pow_le_pow_of_le_right two_pos <| Nat.add_le_of_le_sub ?_ ?_
+    refine Nat.pow_le_pow_right two_pos <| Nat.add_le_of_le_sub ?_ ?_
     · exact Nat.mul_le_mul_right _ (by norm_num)
     · rw [← Nat.sub_mul, (show a ^ 3 = a ^ 2 * a from rfl)]; nlinarith [four_le_a X]
 

Carleson/ToMathlib/BoundedCompactSupport.lean

@@ -73,7 +73,7 @@ omit [TopologicalSpace X] in
 -- maybe in mathlib, but couldn't find it
 theorem ae_le_of_eLpNorm_top_lt_top (hf : eLpNorm f ⊤ μ < ⊤) :
     ∀ᵐ x ∂μ, ‖f x‖ ≤ ENNReal.toReal (eLpNorm f ⊤ μ) := by
-  have := coe_nnnorm_ae_le_eLpNormEssSup f μ
+  have := enorm_ae_le_eLpNormEssSup f μ
   filter_upwards [this] with x hx
   have : ENNReal.ofReal ‖f x‖₊ ≠ ⊤ := ENNReal.ofReal_ne_top
   convert (ENNReal.toReal_le_toReal this ?_).mpr ?_

Carleson/ToMathlib/Data/ENNReal.lean

@@ -1,5 +1,6 @@
 import Mathlib.Analysis.Normed.Field.Basic
-import Mathlib.Topology.Instances.NNReal.Defs
+import Mathlib.Order.CompletePartialOrder
+import Mathlib.Topology.Order.Real
 
 /-! ## `ENNReal` manipulation lemmas -/
 

Carleson/ToMathlib/HardyLittlewood.lean

@@ -270,7 +270,7 @@ theorem MB_le_eLpNormEssSup {u : X → E} {x : X} : MB μ 𝓑 c r u x ≤ eLpNo
         fun _x ↦ ⨍⁻ _y in ball (c i) (r i), eLpNormEssSup u μ ∂μ := by
         simp_rw [MB, maximalFunction, inv_one, ENNReal.rpow_one]
         gcongr
-        exact coe_nnnorm_ae_le_eLpNormEssSup u μ
+        exact MeasureTheory.enorm_ae_le_eLpNormEssSup u μ
     _ ≤ ⨆ i ∈ 𝓑, (ball (c i) (r i)).indicator (x := x) fun _x ↦ eLpNormEssSup u μ := by
       gcongr; apply setLaverage_const_le
     _ ≤ ⨆ i ∈ 𝓑, eLpNormEssSup u μ := by gcongr; apply indicator_le_self

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5269898d6a51d047931107c8d72d934d8d5d3753",
+   "rev": "b523ce86050b5a10fc246cfa4d330aaa0f6df896",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c708be04267e3e995a14ac0d08b1530579c1525a",
+   "rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0447b0a7b7f41f0a1749010db3f222e4a96f9d30",
+   "rev": "08372f1ec11df288ff76621ead7b0b575cb29355",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "799f6986de9f61b784ff7be8f6a8b101045b8ffd",
+   "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.52",
+   "inputRev": "v0.0.53",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "56a2c80b209c253e0281ac4562a92122b457dcc0",
+   "rev": "ec060e0e10c685be8af65f288e23d026c9fde245",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "95561f7a5811fae6a309e4a1bbe22a0a4a98bf03",
+   "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5",
+   "rev": "cce013731b5b355ff4528ac9717ae3e0cc5c4519",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "e7fd1a415c80985ade02a021172834ca2139b0ca",
+   "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.17.0
+leanprover/lean4:v4.18.0-rc1