Update mathlib, deduplicate some lemmas (#133)

Co-authored-by: Floris van Doorn <[email protected]>

Carleson/Classical/SpectralProjectionBound.lean

@@ -7,7 +7,7 @@
 import Carleson.Classical.Basic
 
 open MeasureTheory AddCircle
-
+open scoped InnerProductSpace
 
 --TODO: move somewhere else?
 lemma L2norm_sq_eq {T : ℝ} [hT : Fact (0 < T)] (f : Lp ℂ 2 <| @haarAddCircle T hT) :

Carleson/Discrete/ForestComplement.lean

@@ -427,7 +427,7 @@ lemma iUnion_L0' : ⋃ (l ≤ n), 𝔏₀' (X := X) k n l = 𝔏₀ k n := by
   have mba : b ∈ (aux𝔐 k n).toFinset := by
     simp_rw [mem_toFinset, aux𝔐, mem_setOf, qb, and_true]; rw [TilesAt, mem_preimage] at mp' ⊢
     exact 𝓘p'b ▸ mp'
-  obtain ⟨m, lm, maxm⟩ := exists_maximal_upper_bound mba
+  obtain ⟨m, lm, maxm⟩ := (aux𝔐 k n).toFinset.exists_le_maximal mba
   replace maxm : m ∈ 𝔐 k n := by simpa only [mem_toFinset] using maxm
   -- We will now show a contradiction. As a member of `𝔏₀ k n` the _first_ element `s₀` of the
   -- `LTSeries s` satisfies `𝔅 k n s₀ = ∅`. But we will show that `m ∈ 𝔅 k n s₀`,
@@ -521,7 +521,7 @@ lemma antichain_L2 : IsAntichain (· ≤ ·) (𝔏₂ (X := X) k n j) := by
           _ ≤ _ := by norm_num
       _ ≤ _ := by
         refine smul_C2_1_2 _ (by norm_num) ?_ (wiggle_order_11_10 l.le (C5_3_3_le (X := X)))
-        apply not_lt_of_𝓘_eq_𝓘.mt; rwa [not_not]
+        exact (𝓘_strictMono l).ne
   have cp : p ∈ ℭ₁ k n j := (𝔏₂_subset_ℭ₂.trans ℭ₂_subset_ℭ₁) mp
   let C : Finset (LTSeries (ℭ₁' k n j)) := { s | s.head = ⟨p, cp⟩ }
   have Cn : C.Nonempty := by
@@ -533,7 +533,7 @@ lemma antichain_L2 : IsAntichain (· ≤ ·) (𝔏₂ (X := X) k n j) := by
   · have px : z.head ≤ z.last := z.monotone (Fin.zero_le _)
     rw [mz] at px
     apply absurd mp'; rw [𝔏₂, mem_setOf, not_and_or, not_not]; right; use z.last.1, mu
-    have : 𝓘 p' < 𝓘 p := lt_of_le_of_ne l.le.1 (not_lt_of_𝓘_eq_𝓘.mt (by rwa [not_not]))
+    have : 𝓘 p' < 𝓘 p := 𝓘_strictMono l
     exact ⟨(this.trans_le px.1).ne, (p200.trans px).trans (smul_mono_left (by norm_num))⟩
   · simp_rw [𝔘₁, mem_setOf, not_and, z.last.2, true_implies, not_forall, exists_prop] at mu
     obtain ⟨q, mq, lq, ndjq⟩ := mu; rw [not_disjoint_iff] at ndjq; obtain ⟨ϑ, mϑ₁, mϑ₂⟩ := ndjq

Carleson/ForestOperator.lean

@@ -113,7 +113,7 @@ lemma biUnion_𝓙 : ⋃ J ∈ 𝓙 𝔖, J = ⋃ I : Grid X, (I : Set X) := by
   obtain ⟨J, sJ, mJ⟩ :=
     Grid.exists_containing_subcube _ ⟨le_rfl, (range_subset_iff.mp range_s_subset I).1⟩ mI
   have : J ∈ (𝓙₀ 𝔖).toFinset := by rw [mem_toFinset]; left; exact sJ
-  obtain ⟨M, lM, maxM⟩ := exists_maximal_upper_bound this
+  obtain ⟨M, lM, maxM⟩ := (𝓙₀ 𝔖).toFinset.exists_le_maximal this
   simp_rw [mem_toFinset] at maxM
   use M, maxM, (Grid.le_def.mp lM).1 mJ
 
@@ -130,7 +130,7 @@ lemma biUnion_𝓛 : ⋃ J ∈ 𝓛 𝔖, J = ⋃ I : Grid X, (I : Set X) := by
   obtain ⟨J, sJ, mJ⟩ :=
     Grid.exists_containing_subcube _ ⟨le_rfl, (range_subset_iff.mp range_s_subset I).1⟩ mI
   have : J ∈ (𝓛₀ 𝔖).toFinset := by rw [mem_toFinset]; left; exact sJ
-  obtain ⟨M, lM, maxM⟩ := exists_maximal_upper_bound this
+  obtain ⟨M, lM, maxM⟩ := (𝓛₀ 𝔖).toFinset.exists_le_maximal this
   simp_rw [mem_toFinset] at maxM
   use M, maxM, (Grid.le_def.mp lM).1 mJ
 

Carleson/GridStructure.lean

@@ -268,14 +268,9 @@ lemma succ_def (h : ¬IsMax i) : i.succ = j ↔ i ≤ j ∧ s j = s i + 1 := by
 open Classical in
 def maxCubes (s : Finset (Grid X)) : Finset (Grid X) := s.filter fun i ↦ ∀ j ∈ s, i ≤ j → i = j
 
-lemma exists_maximal_supercube {s : Finset (Grid X)} (hi : i ∈ s) :
-    ∃ j ∈ maxCubes s, i ≤ j := by
-  classical let C : Finset (Grid X) := s.filter (i ≤ ·)
-  have Cn : C.Nonempty := ⟨i, by simp only [C, Finset.mem_filter, hi, le_rfl, true_and]⟩
-  obtain ⟨j, hj, maxj⟩ := C.exists_maximal Cn
-  simp_rw [C, maxCubes, Finset.mem_filter] at hj maxj ⊢
-  refine ⟨j, ?_, hj.2⟩
-  exact ⟨hj.1, fun k hk lk ↦ eq_of_le_of_not_lt lk (maxj k ⟨hk, hj.2.trans lk⟩)⟩
+lemma exists_maximal_supercube {s : Finset (Grid X)} (hi : i ∈ s) : ∃ j ∈ maxCubes s, i ≤ j := by
+  obtain ⟨j, lj, maxj⟩ := s.exists_le_maximal hi; rw [maximal_iff] at maxj
+  simp_rw [maxCubes, Finset.mem_filter]; exact ⟨j, maxj, lj⟩
 
 lemma maxCubes_pairwiseDisjoint {s : Finset (Grid X)} :
     (maxCubes s).toSet.PairwiseDisjoint fun i ↦ (i : Set X) := fun i mi j mj hn ↦ by

Carleson/MinLayerTiles.lean

@@ -17,7 +17,7 @@ lemma exists_scale_add_le_of_mem_minLayer (hp : p ∈ A.minLayer n) :
     obtain ⟨p', mp', lp'⟩ := exists_le_in_minLayer_of_le hp (show n ≤ n + 1 by omega)
     obtain ⟨q, mq, lq, _⟩ := ih mp'; use q, mq, lq.trans lp'; suffices 𝔰 p' < 𝔰 p by omega
     have l : 𝓘 p' < 𝓘 p := by
-      refine lt_of_le_of_ne lp'.1 (not_lt_of_𝓘_eq_𝓘.mt ?_); rw [not_not]
+      apply 𝓘_strictMono
       exact lt_of_le_of_ne lp' <| (disjoint_minLayer_of_ne (by omega)).ne_of_mem mp' hp
     rw [Grid.lt_def] at l; exact l.2
 
@@ -29,7 +29,7 @@ lemma exists_le_add_scale_of_mem_maxLayer (hp : p ∈ A.maxLayer n) :
     obtain ⟨p', mp', lp'⟩ := exists_le_in_maxLayer_of_le hp (show n ≤ n + 1 by omega)
     obtain ⟨q, mq, lq, _⟩ := ih mp'; use q, mq, lp'.trans lq; suffices 𝔰 p < 𝔰 p' by omega
     have l : 𝓘 p < 𝓘 p' := by
-      refine lt_of_le_of_ne lp'.1 (not_lt_of_𝓘_eq_𝓘.mt ?_); rw [not_not]
+      apply 𝓘_strictMono
       exact lt_of_le_of_ne lp' <| (disjoint_maxLayer_of_ne (by omega)).ne_of_mem hp mp'
     rw [Grid.lt_def] at l; exact l.2
 

Carleson/TileStructure.lean

@@ -199,26 +199,9 @@ lemma dist_𝒬_lt_one_of_le {p q : 𝔓 X} (h : p ≤ q) : dist_(p) (𝒬 q) (
 lemma dist_𝒬_lt_one_of_le' {p q : 𝔓 X} (h : p ≤ q) : dist_(p) (𝒬 p) (𝒬 q) < 1 :=
   mem_ball'.mp (dist_𝒬_lt_one_of_le h)
 
-lemma 𝓘_strictMono : StrictMono (𝓘 (X := X)) := by
-  intros p p' h
+lemma 𝓘_strictMono : StrictMono (𝓘 (X := X)) := fun p p' h ↦ by
   refine h.le.1.lt_of_ne <| fun h' ↦ ?_
-  exact Set.disjoint_left.mp (disjoint_Ω h.ne h') (h.le.2 𝒬_mem_Ω) 𝒬_mem_Ω
-
-lemma eq_of_𝓘_eq_𝓘_of_le (h1 : 𝓘 p = 𝓘 p') (h2 : p ≤ p') : p = p' := by
-  by_contra h3
-  exact Set.disjoint_left.mp (disjoint_Ω h3 h1) (h2.2 𝒬_mem_Ω) 𝒬_mem_Ω
-
-lemma not_lt_of_𝓘_eq_𝓘 (h1 : 𝓘 p = 𝓘 p') : ¬ p < p' :=
-  fun h2 ↦ h2.ne <| eq_of_𝓘_eq_𝓘_of_le h1 h2.le
-
--- TODO: Clean up this lemma and the two above, it seems strict monotonicty is the basic idea
-lemma 𝓘_strict_mono : StrictMono (𝓘 (X := X)) := by
-  intro p p' h
-  apply lt_of_le_of_ne
-  · exact (𝔓.le_def'.mp (le_of_lt h)).left
-  · intro h'
-    have := not_lt_of_𝓘_eq_𝓘 h'
-    contradiction
+  exact disjoint_left.mp (disjoint_Ω h.ne h') (h.le.2 𝒬_mem_Ω) 𝒬_mem_Ω
 
 /-- Lemma 5.3.1 -/
 lemma smul_mono {m m' n n' : ℝ} (hp : smul n p ≤ smul m p') (hm : m' ≤ m) (hn : n ≤ n') :
@@ -228,7 +211,7 @@ lemma smul_mono {m m' n n' : ℝ} (hp : smul n p ≤ smul m p') (hm : m' ≤ m)
 /-- Lemma 5.3.2 (generalizing `1` to `k > 0`) -/
 lemma smul_C2_1_2 (m : ℝ) {n k : ℝ} (hk : 0 < k) (hp : 𝓘 p ≠ 𝓘 p') (hl : smul n p ≤ smul k p') :
     smul (n + C2_1_2 a * m) p ≤ smul m p' := by
-  replace hp : 𝓘 p < 𝓘 p' := lt_of_le_of_ne hl.1 hp
+  replace hp : 𝓘 p < 𝓘 p' := hl.1.lt_of_ne hp
   have : ball_(p') (𝒬 p') m ⊆ ball_(p) (𝒬 p) (n + C2_1_2 a * m) := fun x hx ↦ by
     rw [@mem_ball] at hx ⊢
     calc
@@ -249,7 +232,7 @@ lemma dist_LTSeries {n : ℕ} {u : Set (𝔓 X)} {s : LTSeries u} (hs : s.length
     let s' : LTSeries u := s.eraseLast
     specialize ih (show s'.length = n by simp [s', hs])
     have link : dist_(s'.last.1) f g ≤ C2_1_2 a * dist_(s.last.1) f g :=
-      Grid.dist_strictMono <| 𝓘_strict_mono <| s.eraseLast_last_rel_last (by omega)
+      Grid.dist_strictMono <| 𝓘_strictMono <| s.eraseLast_last_rel_last (by omega)
     apply ih.trans; rw [pow_succ, mul_assoc]; gcongr; unfold C2_1_2; positivity
 
 end
@@ -269,7 +252,7 @@ lemma wiggle_order_11_10 {n : ℝ} (hp : p ≤ p') (hn : C5_3_3 a ≤ n) : smul
   rcases eq_or_ne (𝓘 p) (𝓘 p') with h | h
   · rcases eq_or_ne p p' with rfl | h2
     · rfl
-    · exact absurd (eq_of_𝓘_eq_𝓘_of_le h hp) h2
+    · exact absurd h (𝓘_strictMono (lt_of_le_of_ne hp h2)).ne
   · calc
       _ ≤ smul (1 + C2_1_2 a * n) p := by
         apply smul_mono_left

Carleson/ToMathlib/Misc.lean

@@ -45,9 +45,6 @@ section Int
 theorem Int.floor_le_iff (c : ℝ) (z : ℤ) : ⌊c⌋ ≤ z ↔ c < z + 1 := by
   rw_mod_cast [← Int.floor_le_sub_one_iff, add_sub_cancel_right]
 
-theorem Int.le_ceil_iff (c : ℝ) (z : ℤ) : z ≤ ⌈c⌉ ↔ z - 1 < c := by
-  rw_mod_cast [← Int.add_one_le_ceil_iff, sub_add_cancel]
-
 theorem Int.Icc_of_eq_sub_1 {a b : ℤ} (h : a = b - 1) : Finset.Icc a b = {a, b} := by
   refine le_antisymm (fun t ht ↦ ?_) (fun t ht ↦ ?_)
   · rw [h, Finset.mem_Icc] at ht
@@ -347,14 +344,3 @@ lemma Real.self_lt_two_rpow (x : ℝ) : x < 2 ^ x := by
       _ < (⌊x⌋₊.succ : ℝ) := Nat.lt_succ_floor x
       _ ≤ 2 ^ (⌊x⌋₊ : ℝ) := by exact_mod_cast Nat.lt_pow_self one_lt_two _
       _ ≤ _ := rpow_le_rpow_of_exponent_le one_le_two (Nat.floor_le h)
-
-/-- For every element in a finset over a type equipped with a partial order,
-there is a maximal upper bound for that element. -/
-lemma exists_maximal_upper_bound {α : Type*} [PartialOrder α] {s : Finset α} {a : α} (ha : a ∈ s) :
-    ∃ m ≥ a, Maximal (· ∈ s) m := by
-  classical let C : Finset α := s.filter (a ≤ ·)
-  have Cn : C.Nonempty := ⟨a, by simp only [C, Finset.mem_filter, ha, le_rfl, true_and]⟩
-  obtain ⟨m, hm, maxm⟩ := C.exists_maximal Cn
-  simp_rw [C, Finset.mem_filter] at hm maxm
-  use m, hm.2; rw [maximal_iff]
-  exact ⟨hm.1, fun b mb lb ↦ eq_of_le_of_not_lt lb (maxm b ⟨mb, hm.2.trans lb⟩)⟩

Carleson/WeakType.lean

@@ -76,10 +76,10 @@ lemma distribution_measurable {g : α' → ℝ≥0∞} (hg : Measurable g) :
     Measurable (fun y : α' ↦ distribution f (g y) μ) := by
   fun_prop
 
-@[measurability, deprecated]
+/-@[measurability, deprecated]
 lemma distribution_measurable_from_real :
     Measurable (fun t : ℝ ↦ distribution f (.ofReal t) μ) :=
-  distribution_measurable measurable_ofReal
+  distribution_measurable measurable_ofReal-/
 
 lemma ENNNorm_add_le (y z : E) : ofNNReal ‖y + z‖₊ ≤ ↑‖y‖₊ + ↑‖z‖₊ :=
   (toReal_le_toReal coe_ne_top coe_ne_top).mp (nnnorm_add_le ..)
@@ -150,7 +150,7 @@ lemma tendsto_measure_iUnion_distribution (t₀ : ℝ≥0∞) :
     Filter.Tendsto (⇑μ ∘ (fun n : ℕ ↦ {x | t₀ + (↑n)⁻¹ < ‖f x‖₊}))
       Filter.atTop (nhds (μ ({x | t₀ < ‖f x‖₊}))) := by
   rw [← approx_above_superset]
-  apply tendsto_measure_iUnion
+  apply tendsto_measure_iUnion_atTop
   intro a b h x h₁
   calc
     _ ≤ t₀ + (↑a)⁻¹ := by gcongr

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8feac540abb781cb1349688c816dc02fae66b49c",
+   "rev": "35d1cd731ad832c9f1d860c4d8ec1c7c3ab96823",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c",
+   "rev": "a895713f7701e295a015b1087f3113fd3d615272",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -61,11 +61,21 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8c811c94af285516e8c76a63165c87027f18ccd0",
+   "rev": "c7d6577ad9a4110f04f2ba10501f5508a2e9e6f2",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",