bump Lean and Mathlib

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

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

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]

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) :

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",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc1
+leanprover/lean4:v4.9.0-rc1