From ddaf31334b43a702ce7a4df00a779eac6835de73 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 7 Jun 2024 12:50:55 +0200 Subject: [PATCH] bump Lean and Mathlib --- Carleson.lean | 3 ++ Carleson/Theorem1_1/Approximation.lean | 1 - .../Theorem1_1/Carleson_on_the_real_line.lean | 4 +-- Carleson/ToMathlib/MeasureReal.lean | 31 +++++++++---------- lake-manifest.json | 18 +++++------ lean-toolchain | 2 +- 6 files changed, 29 insertions(+), 30 deletions(-) diff --git a/Carleson.lean b/Carleson.lean index 355f6888..41631ab1 100644 --- a/Carleson.lean +++ b/Carleson.lean @@ -1,3 +1,4 @@ +import Carleson.Carleson import Carleson.CoverByBalls import Carleson.Defs import Carleson.HomogeneousType @@ -6,10 +7,12 @@ import Carleson.Proposition2 import Carleson.Proposition3 import Carleson.Theorem1_1.Approximation import Carleson.Theorem1_1.Basic +import Carleson.Theorem1_1.CarlesonOperatorReal import Carleson.Theorem1_1.Carleson_on_the_real_line import Carleson.Theorem1_1.ClassicalCarleson import Carleson.Theorem1_1.Control_Approximation_Effect import Carleson.Theorem1_1.Dirichlet_kernel +import Carleson.Theorem1_1.Hilbert_kernel import Carleson.ToMathlib.Finiteness import Carleson.ToMathlib.Finiteness.Attr import Carleson.ToMathlib.MeasureReal diff --git a/Carleson/Theorem1_1/Approximation.lean b/Carleson/Theorem1_1/Approximation.lean index fb7ad227..8e4a8646 100644 --- a/Carleson/Theorem1_1/Approximation.lean +++ b/Carleson/Theorem1_1/Approximation.lean @@ -5,7 +5,6 @@ import Carleson.HomogeneousType import Carleson.Theorem1_1.Basic import Mathlib.Analysis.Fourier.AddCircle -import Mathlib.Algebra.BigOperators.Basic import Mathlib.Analysis.Convolution import Mathlib.Analysis.Calculus.BumpFunction.Convolution import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension diff --git a/Carleson/Theorem1_1/Carleson_on_the_real_line.lean b/Carleson/Theorem1_1/Carleson_on_the_real_line.lean index b28773fd..9e59214d 100644 --- a/Carleson/Theorem1_1/Carleson_on_the_real_line.lean +++ b/Carleson/Theorem1_1/Carleson_on_the_real_line.lean @@ -9,7 +9,6 @@ import Carleson.Theorem1_1.CarlesonOperatorReal --import Mathlib.Tactic import Mathlib.Analysis.Fourier.AddCircle -import Mathlib.Algebra.BigOperators.Basic import Mathlib.MeasureTheory.Integral.IntervalIntegral import Mathlib.Analysis.SpecialFunctions.Integrals @@ -227,10 +226,9 @@ lemma bciSup_of_emptyset {α : Type} [ConditionallyCompleteLattice α] {ι : Ty ⨆ i ∈ (∅ : Set ι), f i = sSup ∅ := by rw [iSup] convert csSup_singleton _ - have : ∀ i : ι, IsEmpty (i ∈ ∅) := by + have : ∀ i : ι, IsEmpty (i ∈ (∅ : Set ι)) := by intro i simp - apply Set.not_mem_empty have : (fun (i : ι) ↦ ⨆ (_ : i ∈ (∅ : Set ι)), f i) = fun i ↦ sSup ∅ := by ext i --rw [csSup_empty] diff --git a/Carleson/ToMathlib/MeasureReal.lean b/Carleson/ToMathlib/MeasureReal.lean index e2f6d2ce..2f959a1b 100644 --- a/Carleson/ToMathlib/MeasureReal.lean +++ b/Carleson/ToMathlib/MeasureReal.lean @@ -64,7 +64,6 @@ namespace MeasureTheory variable {α : Type*} {β : Type*} {_ : MeasurableSpace α} [MeasurableSpace β] (μ : Measure α) /-- The real-valued version of a measure. Maps infinite measure sets to zero. Use as `μ.real s`. -/ -@[pp_dot] protected def Measure.real (s : Set α) : ℝ := (μ s).toReal @@ -85,7 +84,7 @@ theorem measure_diff_eq_top (hs : μ s = ∞) (ht : μ t ≠ ∞) : μ (s \ t) = exact ENNReal.add_lt_top.2 ⟨hs.lt_top, ht.lt_top⟩ theorem measure_symmDiff_eq_top (hs : μ s ≠ ∞) (ht : μ t = ∞) : μ (s ∆ t) = ∞ := - measure_mono_top (subset_union_right _ _) (measure_diff_eq_top ht hs) + measure_mono_top subset_union_right (measure_diff_eq_top ht hs) end move_to_MeasureSpace.lean @@ -140,7 +139,7 @@ theorem measureReal_le_measureReal_union_left (h : μ t ≠ ∞ := by finiteness μ.real s ≤ μ.real (s ∪ t) := by rcases eq_top_or_lt_top (μ s) with hs|hs · simp [Measure.real, hs] - · exact measureReal_mono (subset_union_left _ _) (measure_union_lt_top hs h.lt_top).ne + · exact measureReal_mono subset_union_left (measure_union_lt_top hs h.lt_top).ne theorem measureReal_le_measureReal_union_right (h : μ s ≠ ∞ := by finiteness) : μ.real t ≤ μ.real (s ∪ t) := by @@ -151,8 +150,8 @@ theorem measureReal_union_le (s₁ s₂ : Set α) : μ.real (s₁ ∪ s₂) ≤ rcases eq_top_or_lt_top (μ (s₁ ∪ s₂)) with h|h · simp only [Measure.real, h, ENNReal.top_toReal] exact add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg - · have A : μ s₁ ≠ ∞ := measure_ne_top_of_subset (subset_union_left _ _) h.ne - have B : μ s₂ ≠ ∞ := measure_ne_top_of_subset (subset_union_right _ _) h.ne + · have A : μ s₁ ≠ ∞ := measure_ne_top_of_subset subset_union_left h.ne + have B : μ s₂ ≠ ∞ := measure_ne_top_of_subset subset_union_right h.ne simp only [Measure.real, ← ENNReal.toReal_add A B] exact ENNReal.toReal_mono (by simp [A, B]) (measure_union_le _ _) @@ -187,8 +186,8 @@ theorem measureReal_union_null_iff μ.real (s₁ ∪ s₂) = 0 ↔ μ.real s₁ = 0 ∧ μ.real s₂ = 0 := by have : μ (s₁ ∪ s₂) ≠ ∞ := measure_union_ne_top h₁ h₂ refine ⟨fun h => ⟨?_, ?_⟩, fun h => measureReal_union_null h.1 h.2⟩ - · exact measureReal_mono_null (subset_union_left _ _) h this - · exact measureReal_mono_null (subset_union_right _ _) h this + · exact measureReal_mono_null subset_union_left h this + · exact measureReal_mono_null subset_union_right h this /-- If two sets are equal modulo a set of measure zero, then `μ.real s = μ.real t`. -/ theorem measureReal_congr (H : s =ᵐ[μ] t) : μ.real s = μ.real t := by @@ -199,8 +198,8 @@ theorem measureReal_inter_add_diff₀ (s : Set α) (ht : NullMeasurableSet t μ) μ.real (s ∩ t) + μ.real (s \ t) = μ.real s := by simp only [measureReal_def] rw [← ENNReal.toReal_add, measure_inter_add_diff₀ s ht] - · exact measure_ne_top_of_subset (inter_subset_left _ _) h - · exact measure_ne_top_of_subset (diff_subset _ _) h + · exact measure_ne_top_of_subset inter_subset_left h + · exact measure_ne_top_of_subset diff_subset h theorem measureReal_union_add_inter₀ (s : Set α) (ht : NullMeasurableSet t μ) (h₁ : μ s ≠ ∞ := by finiteness) (h₂ : μ t ≠ ∞ := by finiteness) : @@ -247,8 +246,8 @@ theorem measureReal_inter_add_diff (s : Set α) (ht : MeasurableSet t) μ.real (s ∩ t) + μ.real (s \ t) = μ.real s := by simp only [Measure.real] rw [← ENNReal.toReal_add, measure_inter_add_diff _ ht] - · exact measure_ne_top_of_subset (inter_subset_left _ _) h - · exact measure_ne_top_of_subset (diff_subset _ _) h + · exact measure_ne_top_of_subset inter_subset_left h + · exact measure_ne_top_of_subset diff_subset h theorem measureReal_diff_add_inter (s : Set α) (ht : MeasurableSet t) (h : μ s ≠ ∞ := by finiteness) : @@ -270,8 +269,8 @@ lemma measureReal_symmDiff_eq (hs : MeasurableSet s) (ht : MeasurableSet t) μ.real (s ∆ t) = μ.real (s \ t) + μ.real (t \ s) := by simp only [Measure.real] rw [← ENNReal.toReal_add, measure_symmDiff_eq hs ht] - · exact measure_ne_top_of_subset (diff_subset _ _) h₁ - · exact measure_ne_top_of_subset (diff_subset _ _) h₂ + · exact measure_ne_top_of_subset diff_subset h₁ + · exact measure_ne_top_of_subset diff_subset h₂ lemma measureReal_symmDiff_le (s t u : Set α) (h₁ : μ s ≠ ∞ := by finiteness) (h₂ : μ t ≠ ∞ := by finiteness) : @@ -318,19 +317,19 @@ theorem measureReal_diff_null' (h : μ.real (s₁ ∩ s₂) = 0) (h' : μ s₁ simp only [measureReal_def] rw [measure_diff_null'] apply (measureReal_eq_zero_iff _).1 h - exact measure_ne_top_of_subset (inter_subset_left _ _) h' + exact measure_ne_top_of_subset inter_subset_left h' theorem measureReal_diff_null (h : μ.real s₂ = 0) (h' : μ s₂ ≠ ∞ := by finiteness) : μ.real (s₁ \ s₂) = μ.real s₁ := by rcases eq_top_or_lt_top (μ s₁) with H|H · simp [measureReal_def, H, measure_diff_eq_top H h'] - · exact measureReal_diff_null' (measureReal_mono_null (inter_subset_right _ _) h h') H.ne + · exact measureReal_diff_null' (measureReal_mono_null inter_subset_right h h') H.ne theorem measureReal_add_diff (hs : MeasurableSet s) (t : Set α) (h₁ : μ s ≠ ∞ := by finiteness) (h₂ : μ t ≠ ∞ := by finiteness) : μ.real s + μ.real (t \ s) = μ.real (s ∪ t) := by rw [← measureReal_union' (@disjoint_sdiff_right _ s t) hs h₁ - (measure_ne_top_of_subset (diff_subset _ _) h₂), union_diff_self] + (measure_ne_top_of_subset diff_subset h₂), union_diff_self] theorem measureReal_diff' (s : Set α) (hm : MeasurableSet t) (h₁ : μ s ≠ ∞ := by finiteness) (h₂ : μ t ≠ ∞ := by finiteness) : diff --git a/lake-manifest.json b/lake-manifest.json index 1f7db2a0..5c575cff 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,31 +1,31 @@ -{"version": 7, +{"version": "1.0.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "914ad4f90518b7a2373ad6742a9518903f207927", + "rev": "af2dda22771c59db026c48ac0aabc73b72b7a4de", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6", + "rev": "44f57616b0d9b8f9e5606f2c58d01df54840eba7", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "f617e0673845925e612b62141ff54c4b7980dc63", + "rev": "f744aab6fc4e06553464e6ae66730a3b14b8e615", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb", + "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "7493b5f81b4c031b87877c5c124bea1ddc4e567d", + "rev": "dd36c71ca810923613cae217af028ee54aaff1e3", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/lean-toolchain b/lean-toolchain index d8a6d7ef..0ba3faf8 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc1 +leanprover/lean4:v4.9.0-rc1