From 68076f253825a7a2d927ae825ecbbca81acf6036 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 25 Mar 2024 15:41:53 +0100 Subject: [PATCH] bump mathlib --- .gitignore | 1 + Carleson/Carleson.lean | 24 +++--- Carleson/CoverByBalls.lean | 4 +- Carleson/Defs.lean | 4 + Carleson/HomogeneousType.lean | 6 +- Carleson/Proposition1.lean | 4 +- Carleson/Proposition2.lean | 2 +- Carleson/Proposition3.lean | 2 +- Carleson/ToMathlib/Finiteness.lean | 15 ++-- Carleson/ToMathlib/MeasureReal.lean | 3 +- Carleson/ToMathlib/Misc.lean | 2 +- lake-manifest.json | 118 ++++++++++++++++------------ lakefile.lean | 8 +- lean-toolchain | 2 +- 14 files changed, 108 insertions(+), 87 deletions(-) diff --git a/.gitignore b/.gitignore index 190872c8..97ce1d0f 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,6 @@ /build /lake-packages +/.lake /.cache .DS_Store /lakefile.olean diff --git a/Carleson/Carleson.lean b/Carleson/Carleson.lean index 4f88804b..befc1207 100644 --- a/Carleson/Carleson.lean +++ b/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] diff --git a/Carleson/CoverByBalls.lean b/Carleson/CoverByBalls.lean index 23326f02..ca8763a2 100644 --- a/Carleson/CoverByBalls.lean +++ b/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 diff --git a/Carleson/Defs.lean b/Carleson/Defs.lean index 3919b58a..3e7ab791 100644 --- a/Carleson/Defs.lean +++ b/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 diff --git a/Carleson/HomogeneousType.lean b/Carleson/HomogeneousType.lean index 93d28cf2..54d3eac7 100644 --- a/Carleson/HomogeneousType.lean +++ b/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 diff --git a/Carleson/Proposition1.lean b/Carleson/Proposition1.lean index 4fc1c054..dd89192b 100644 --- a/Carleson/Proposition1.lean +++ b/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) diff --git a/Carleson/Proposition2.lean b/Carleson/Proposition2.lean index 9ed33d29..10ca7e69 100644 --- a/Carleson/Proposition2.lean +++ b/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 diff --git a/Carleson/Proposition3.lean b/Carleson/Proposition3.lean index fdf38869..08f7af58 100644 --- a/Carleson/Proposition3.lean +++ b/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 diff --git a/Carleson/ToMathlib/Finiteness.lean b/Carleson/ToMathlib/Finiteness.lean index 89bbb6c2..22a6832a 100644 --- a/Carleson/ToMathlib/Finiteness.lean +++ b/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,11 +33,11 @@ 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 @@ -45,11 +45,11 @@ attribute [aesop (rule_sets [Finiteness]) safe apply] 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 -/ diff --git a/Carleson/ToMathlib/MeasureReal.lean b/Carleson/ToMathlib/MeasureReal.lean index 07629040..e2f6d2ce 100644 --- a/Carleson/ToMathlib/MeasureReal.lean +++ b/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*} diff --git a/Carleson/ToMathlib/Misc.lean b/Carleson/ToMathlib/Misc.lean index 7cb79e32..8f2b53e0 100644 --- a/Carleson/ToMathlib/Misc.lean +++ b/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 diff --git a/lake-manifest.json b/lake-manifest.json index 7aba0633..deb65afc 100644 --- a/lake-manifest.json +++ b/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"} diff --git a/lakefile.lean b/lakefile.lean index 34d4bf2c..e0997bbf 100644 --- a/lakefile.lean +++ b/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 diff --git a/lean-toolchain b/lean-toolchain index a61d2828..e35881ce 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0-rc3 +leanprover/lean4:v4.7.0-rc2