bump mathlib

.gitignore

@@ -1,5 +1,6 @@
 /build
 /lake-packages
+/.lake
 /.cache
 .DS_Store
 /lakefile.olean

Carleson/Carleson.lean

@@ -54,7 +54,7 @@ variable
 
 -- move
 theorem Int.floor_le_iff (a : ℝ) (z : ℤ) : ⌊a⌋ ≤ z ↔ a < z + 1 := by
-  rw_mod_cast [← Int.floor_le_sub_one_iff, add_sub_cancel]
+  rw_mod_cast [← Int.floor_le_sub_one_iff, add_sub_cancel_right]
 
 theorem Int.le_ceil_iff (a : ℝ) (z : ℤ) : z ≤ ⌈a⌉ ↔ z - 1 < a := by
   rw_mod_cast [← Int.add_one_le_ceil_iff, sub_add_cancel]
@@ -88,8 +88,8 @@ lemma sum_Ks {s : Finset ℤ} (hs : nonzeroS D (dist x y) ⊆ s) (hD : 1 < D) (h
   have h2 : 0 < dist x y := dist_pos.mpr h
   simp_rw [Ks, ← Finset.mul_sum]
   norm_cast
-  suffices : ∑ i in s, ψ (D ^ i * dist x y) = 1
-  · simp [this]
+  suffices ∑ i in s, ψ (D ^ i * dist x y) = 1 by
+    simp [this]
   rw [← Finset.sum_subset hs, h3ψ _ h2]
   intros
   rwa [psi_eq_zero_iff h2ψ h2 hD]
@@ -108,8 +108,8 @@ lemma equation3_1 {f : X → ℂ} (hf : LocallyIntegrable f)
     ‖∑ s in Finset.Icc σ σ', ∫ y, Ks K D ψ s x y * f y * exp (I * (Q y - Q x))‖
     CarlesonOperator K 𝓠 f x ≤ rhs := by
   intro rhs
-  have h_rhs : 0 ≤ rhs
-  · sorry
+  have h_rhs : 0 ≤ rhs := by
+    sorry
   rw [CarlesonOperator]
   refine Real.iSup_le (fun Q ↦ ?_) h_rhs
   refine Real.iSup_le (fun hQ ↦ ?_) h_rhs
@@ -123,8 +123,8 @@ lemma equation3_1 {f : X → ℂ} (hf : LocallyIntegrable f)
   rw [← sub_le_iff_le_add]
   simp_rw [mul_sub, Complex.exp_sub, mul_div, integral_div, ← Finset.sum_div,
     norm_div]
-  have h1 : ‖cexp (I * Q x)‖ = 1
-  · lift Q x to ℝ using h𝓠 Q hQ x with qx
+  have h1 : ‖cexp (I * Q x)‖ = 1 := by
+    lift Q x to ℝ using h𝓠 Q hQ x with qx
     simp only [mul_comm I qx, norm_exp_ofReal_mul_I]
   rw [h1, div_one]
   /- use h3ψ here to rewrite the RHS -/
@@ -133,8 +133,8 @@ lemma equation3_1 {f : X → ℂ} (hf : LocallyIntegrable f)
   simp_rw [← Finset.sum_mul]
   have h3 :
     ∫ (y : X) in {y | dist x y ∈ Set.Ioo r R}, K x y * f y * cexp (I * Q y) =
-      ∫ (y : X) in {y | dist x y ∈ Set.Ioo r R}, (∑ x_1 in Finset.Icc σ σ', Ks K D ψ x_1 x y) * f y * cexp (I * Q y)
-  · sorry
+      ∫ (y : X) in {y | dist x y ∈ Set.Ioo r R}, (∑ x_1 in Finset.Icc σ σ', Ks K D ψ x_1 x y) * f y * cexp (I * Q y) := by
+    sorry
   -- after we rewrite, we should have only 4 terms of our finset left, all others are 0. These can be estimated using |K x y| ≤ 1 / volume (ball x (dist x y)).
   rw [h3, ← neg_sub, ← integral_univ, ← integral_diff]
   all_goals sorry
@@ -173,7 +173,7 @@ segment. -/
 /- finish proof of equation (2.2) -/
 
 theorem equation2_2
-    (hA : 1 < A) (hτ : τ ∈ Ioo 0 1) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjugateExponent q')
+    (hA : 1 < A) (hτ : τ ∈ Ioo 0 1) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q')
     (hF : MeasurableSet F) (hG : MeasurableSet G)
     (h2F : volume F ∈ Ioo 0 ∞) (h2G : volume G ∈ Ioo 0 ∞)
     (hT : NormBoundedBy (ANCZOperatorLp 2 K) 1) :
@@ -187,7 +187,7 @@ theorem equation2_2
 
 /- Theorem 1.1, written using constant C1_1 -/
 theorem theorem1_1C
-    (hA : 1 < A) (hτ : τ ∈ Ioo 0 1) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjugateExponent q')
+    (hA : 1 < A) (hτ : τ ∈ Ioo 0 1) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q')
     (hF : MeasurableSet F) (hG : MeasurableSet G)
     -- (h2F : volume F ∈ Ioo 0 ∞) (h2G : volume G ∈ Ioo 0 ∞)
     (hT : NormBoundedBy (ANCZOperatorLp 2 K) 1) :
@@ -204,7 +204,7 @@ end
 set_option linter.unusedVariables false in
 /- Theorem 1.1. -/
 theorem theorem1_1 {A : ℝ} (hA : 1 < A) {τ q q' : ℝ}
-    (hτ : τ ∈ Ioo 0 1) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjugateExponent q') : ∃ (C : ℝ), C > 0 ∧
+    (hτ : τ ∈ Ioo 0 1) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q') : ∃ (C : ℝ), C > 0 ∧
     ∀ {X : Type*} [MetricSpace X] [IsSpaceOfHomogeneousType X A]  [Inhabited X]
     (𝓠 : Set C(X, ℂ)) [IsCompatible 𝓠] [IsCancellative τ 𝓠]
     (K : X → X → ℂ) [IsCZKernel τ K]

Carleson/CoverByBalls.lean

@@ -93,7 +93,7 @@ lemma BallCoversSelf (x : X) (r : ℝ) : CoveredByBalls (ball x r) 1 r := by {
   let a : Finset X := singleton x
   have h : a.card ≤ 1 := by rfl
   have h2 : ball x r ⊆ ⋃ x ∈ a, ball x r := by
-    simp
+    simp [a]
     rfl
   exact ⟨a, h, h2⟩
 }
@@ -103,12 +103,10 @@ lemma BallsCoverBalls.pow_mul {a : ℝ} {k : ℕ} (h : ∀ r, BallsCoverBalls X
   induction k
   case zero =>
     simp
-    rw[BallsCoverBalls]
     intro x
     exact BallCoversSelf x r
   case succ m h2 =>
     specialize h (r * a^m)
-    simp at h
     rw[<- mul_assoc, mul_comm, <- mul_assoc] at h
     norm_cast
     ring_nf

Carleson/Defs.lean

@@ -30,6 +30,10 @@ set_option linter.unusedVariables false in
 /-- A type synonym of `C(X, ℂ)` that uses the local oscillation w.r.t. `E` as the metric. -/
 def withLocalOscillation (E : Set X) [Fact (IsBounded E)] : Type _ := C(X, ℂ)
 
+instance withLocalOscillation.funLike (E : Set X) [Fact (IsBounded E)] :
+    FunLike (withLocalOscillation E) X ℂ :=
+  ContinuousMap.funLike
+
 instance withLocalOscillation.toContinuousMapClass (E : Set X) [Fact (IsBounded E)] :
     ContinuousMapClass (withLocalOscillation E) X ℂ :=
   ContinuousMap.toContinuousMapClass

Carleson/HomogeneousType.lean

@@ -44,13 +44,13 @@ lemma volume_ball_four_le_same (x : X) (r : ℝ) :
 
 lemma measure_ball_ne_top (x : X) (r : ℝ) : volume (ball x r) ≠ ∞ := measure_ball_lt_top.ne
 
-attribute [aesop (rule_sets [Finiteness]) safe apply] measure_ball_ne_top
+attribute [aesop (rule_sets := [Finiteness]) safe apply] measure_ball_ne_top
 
 def As (A : ℝ) (s : ℝ) : ℝ :=
   A ^ ⌈ Real.log s / Real.log 2⌉₊
 
 /- Proof sketch: First do for powers of 2 by induction, then use monotonicity. -/
-lemma volume_ball_le_same (x : X) {r s r': ℝ} (hsp : s > 0)  (hs : r' ≤ s * r) :
+lemma volume_ball_le_same (x : X) {r s r': ℝ} (hsp : s > 0) (hs : r' ≤ s * r) :
     volume.real (ball x r') ≤ As A s * volume.real (ball x r) := by
   /-First show statement for s a power of two-/
   have hn (n : ℕ) : volume.real (ball x (2^n * r)) ≤ A^n * volume.real (ball x r) := by
@@ -143,7 +143,7 @@ lemma tendsto_average_zero {E} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X
 
 /- # Instances of spaces of homogeneous type -/
 
-instance (n : ℕ) : Fact ((1 : ℝ) ≤ 2 ^ n) := ⟨by norm_cast; exact Nat.one_le_two_pow n⟩
+instance (n : ℕ) : Fact ((1 : ℝ) ≤ 2 ^ n) := ⟨by norm_cast; exact Nat.one_le_two_pow⟩
 
 /- ℝ^n is a space of homogenous type. -/
 instance {ι : Type*} [Fintype ι] : IsSpaceOfHomogeneousType (ι → ℝ) (2 ^ Fintype.card ι) := sorry

Carleson/Proposition1.lean

@@ -1,7 +1,7 @@
 import Carleson.Proposition2
 import Carleson.Proposition3
 
-open MeasureTheory Measure NNReal Metric Complex Set Function
+open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators
 open scoped ENNReal
 noncomputable section
 local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
@@ -33,7 +33,7 @@ variable {ψ : ℝ → ℝ}
 
 -- todo: add some conditions that σ and other functions have finite range?
 theorem prop2_1
-    (hA : 1 < A) (hτ : τ ∈ Ioo 0 1) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjugateExponent q')
+    (hA : 1 < A) (hτ : τ ∈ Ioo 0 1) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q')
     (hC₀ : 0 < C₀) (hC : C2_1 A τ q C₀ < C) (hD : D2_1 A τ q C₀ < D)
     (hκ : κ ∈ Ioo 0 (κ2_1 A τ q C₀))
     (hF : MeasurableSet F) (hG : MeasurableSet G)

Carleson/Proposition2.lean

@@ -1,6 +1,6 @@
 import Carleson.Defs
 
-open MeasureTheory Measure NNReal Metric Complex Set Function
+open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators
 open scoped ENNReal
 noncomputable section
 local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220

Carleson/Proposition3.lean

@@ -1,6 +1,6 @@
 import Carleson.Defs
 
-open MeasureTheory Measure NNReal Metric Complex Set TileStructure Function
+open MeasureTheory Measure NNReal Metric Complex Set TileStructure Function BigOperators
 open scoped ENNReal
 noncomputable section
 local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220

Carleson/ToMathlib/Finiteness.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
 import Carleson.ToMathlib.Finiteness.Attr
-import Mathlib.MeasureTheory.Measure.MeasureSpace
+import Mathlib.MeasureTheory.Constructions.Prod.Basic
 
 /-! # Finiteness tactic
 
@@ -33,23 +33,23 @@ theorem ENNReal.add_ne_top' {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞)
 
 /-! ## Tactic implementation -/
 
-attribute [aesop (rule_sets [Finiteness]) unsafe 20%] ne_top_of_lt
+attribute [aesop (rule_sets := [Finiteness]) unsafe 20%] ne_top_of_lt
 -- would have been better to implement this as a "safe" "forward" rule, why doesn't this work?
 -- attribute [aesop (rule_sets [Finiteness]) safe forward] ne_top_of_lt
 
-attribute [aesop (rule_sets [Finiteness]) safe apply]
+attribute [aesop (rule_sets := [Finiteness]) safe apply]
   Ne.lt_top
   ENNReal.ofReal_ne_top ENNReal.coe_ne_top ENNReal.nat_ne_top
   ENNReal.zero_ne_top ENNReal.one_ne_top ENNReal.ofNat_ne_top
   ENNReal.mul_ne_top ENNReal.add_ne_top' ENNReal.sub_ne_top ENNReal.inv_ne_top'
   MeasureTheory.measure_ne_top
 
 open Aesop.BuiltinRules in
-attribute [aesop (rule_sets [Finiteness]) safe -50] assumption intros
+attribute [aesop (rule_sets := [Finiteness]) safe -50] assumption intros
 
 open Lean Elab Tactic in
 /-- A version of the positivity tactic for use by `aesop`. -/
-@[aesop safe tactic (rule_sets [Finiteness])]
+@[aesop safe tactic (rule_sets := [Finiteness])]
 def PositivityForAesop : TacticM Unit :=
   liftMetaTactic fun g => do Mathlib.Meta.Positivity.positivity g; pure []
 
@@ -58,9 +58,8 @@ nonnegative reals (`ℝ≥0∞`). -/
 macro (name := finiteness) "finiteness" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
   aesop $c*
-    (options := { introsTransparency? := some .reducible, terminal := true })
-    (simp_options := { enabled := false })
-    (rule_sets [$(Lean.mkIdent `Finiteness):ident, -default, -builtin]))
+    (config := { introsTransparency? := some .reducible, terminal := true, enableSimp := false })
+    (rule_sets := [$(Lean.mkIdent `Finiteness):ident, -default, -builtin]))
 
 /-! ## Tests -/
 

Carleson/ToMathlib/MeasureReal.lean

@@ -1,4 +1,3 @@
-import Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Carleson.ToMathlib.Finiteness
 
 /-!
@@ -22,7 +21,7 @@ more painful with reals than nonnegative extended reals. I don't expect we will
 project, but we should probably add them back in the long run if they turn out to be useful.
 -/
 
-open MeasureTheory Measure Set
+open MeasureTheory Measure Set symmDiff
 open scoped ENNReal NNReal BigOperators
 
 variable {ι : Type*}

Carleson/ToMathlib/Misc.lean

@@ -1,5 +1,5 @@
 import Mathlib.Analysis.Convex.PartitionOfUnity
-import Mathlib.Analysis.Calculus.ContDiff
+import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.Topology.MetricSpace.Holder
 

lake-manifest.json

@@ -1,52 +1,68 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/leanprover-community/mathlib4.git",
-    "subDir?": null,
-    "rev": "53ae52b4b02665479ad5297e05878c07e129e969",
-    "opts": {},
-    "name": "mathlib",
-    "inputRev?": null,
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "dd2549f76ff763c897fe997061e2625a7d628eaf",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/quote4",
-    "subDir?": null,
-    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
-    "opts": {},
-    "name": "Qq",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/aesop",
-    "subDir?": null,
-    "rev": "b601328752091a1cfcaebdd6b6b7c30dc5ffd946",
-    "opts": {},
-    "name": "aesop",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover/lean4-cli",
-    "subDir?": null,
-    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
-    "opts": {},
-    "name": "Cli",
-    "inputRev?": "nightly",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/ProofWidgets4",
-    "subDir?": null,
-    "rev": "27715d1daf32b9657dc38cd52172d77b19bde4ba",
-    "opts": {},
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.18",
-    "inherited": true}}],
- "name": "carleson"}
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "e5306c3b0edefe722370b7387ee9bcd4631d6c17",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "rev": "8be30c25e3caa06937feeb62f7ca898370f80ee9",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.30",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "496f2278b1142e4c6dc5f73dd0a5d10700be4895",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "carleson",
+ "lakeDir": ".lake"}

lakefile.lean

@@ -21,10 +21,13 @@ def weakLeanArgs : Array String :=
     #[]
 
 package «carleson» where
-  moreServerArgs := moreServerArgs
+  leanOptions := #[
+    ⟨`relaxedAutoImplicit, false⟩, -- prevents typos to be interpreted as new free variables
+    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
+    ⟨`autoImplicit, false⟩]
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
+  "https://github.com/leanprover-community/mathlib4.git" @ "master"
 
 -- This is run only if we're in `dev` mode. This is so not everyone has to build doc-gen
 meta if get_config? env = some "dev" then
@@ -34,3 +37,4 @@ require «doc-gen4» from git
 @[default_target]
 lean_lib «Carleson» where
   moreLeanArgs := moreLeanArgs
+  weakLeanArgs := weakLeanArgs

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc3
+leanprover/lean4:v4.7.0-rc2