From e805e2e8153f9b0a0fec1752b8af1e6793bc32ef Mon Sep 17 00:00:00 2001 From: Jeremy Tan Jie Rui Date: Wed, 25 Sep 2024 18:02:02 +0800 Subject: [PATCH] Update mathlib, deduplicate some lemmas (#133) Co-authored-by: Floris van Doorn --- .../Classical/SpectralProjectionBound.lean | 2 +- Carleson/Discrete/ForestComplement.lean | 6 ++--- Carleson/ForestOperator.lean | 4 +-- Carleson/GridStructure.lean | 11 +++----- Carleson/MinLayerTiles.lean | 4 +-- Carleson/TileStructure.lean | 27 ++++--------------- Carleson/ToMathlib/Misc.lean | 14 ---------- Carleson/WeakType.lean | 6 ++--- lake-manifest.json | 16 ++++++++--- 9 files changed, 32 insertions(+), 58 deletions(-) diff --git a/Carleson/Classical/SpectralProjectionBound.lean b/Carleson/Classical/SpectralProjectionBound.lean index b3c040c7..16436db8 100644 --- a/Carleson/Classical/SpectralProjectionBound.lean +++ b/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) : diff --git a/Carleson/Discrete/ForestComplement.lean b/Carleson/Discrete/ForestComplement.lean index ef049efc..7c9fbe97 100644 --- a/Carleson/Discrete/ForestComplement.lean +++ b/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 diff --git a/Carleson/ForestOperator.lean b/Carleson/ForestOperator.lean index c0600fcf..d7f17c6b 100644 --- a/Carleson/ForestOperator.lean +++ b/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 diff --git a/Carleson/GridStructure.lean b/Carleson/GridStructure.lean index 3f1691b5..0f8b4b55 100644 --- a/Carleson/GridStructure.lean +++ b/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 diff --git a/Carleson/MinLayerTiles.lean b/Carleson/MinLayerTiles.lean index 66274094..52cf95a7 100644 --- a/Carleson/MinLayerTiles.lean +++ b/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 diff --git a/Carleson/TileStructure.lean b/Carleson/TileStructure.lean index 6ce99f64..0949298c 100644 --- a/Carleson/TileStructure.lean +++ b/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 diff --git a/Carleson/ToMathlib/Misc.lean b/Carleson/ToMathlib/Misc.lean index e53bcf7b..ccabcdf5 100644 --- a/Carleson/ToMathlib/Misc.lean +++ b/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⟩)⟩ diff --git a/Carleson/WeakType.lean b/Carleson/WeakType.lean index b23bc21a..573d4769 100644 --- a/Carleson/WeakType.lean +++ b/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 diff --git a/lake-manifest.json b/lake-manifest.json index 67075453..cfb7ebe8 100644 --- a/lake-manifest.json +++ b/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",