From 788e0f8402fb3e51b03ba7f1977e26a75c981643 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 18 Jun 2024 11:55:39 +0200 Subject: [PATCH] various redefinitions, partly fix real_line file --- Carleson.lean | 6 +- Carleson/Defs.lean | 86 +++++++++++-------- Carleson/DiscreteCarleson.lean | 52 +++++------ Carleson/GridStructure.lean | 44 +++++----- Carleson/MetricCarleson.lean | 10 +-- Carleson/Proposition2.lean | 4 +- Carleson/Theorem1_1/Basic.lean | 2 +- .../Theorem1_1/Carleson_on_the_real_line.lean | 55 ++++++++---- 8 files changed, 142 insertions(+), 117 deletions(-) diff --git a/Carleson.lean b/Carleson.lean index 333993c6..0818117f 100644 --- a/Carleson.lean +++ b/Carleson.lean @@ -1,10 +1,12 @@ -import Carleson.MetricCarleson import Carleson.CoverByBalls import Carleson.Defs -import Carleson.DoublingMeasure import Carleson.DiscreteCarleson +import Carleson.DoublingMeasure +import Carleson.GridStructure +import Carleson.MetricCarleson import Carleson.Proposition2 import Carleson.Proposition3 +import Carleson.Psi import Carleson.Theorem1_1.Approximation import Carleson.Theorem1_1.Basic import Carleson.Theorem1_1.CarlesonOperatorReal diff --git a/Carleson/Defs.lean b/Carleson/Defs.lean index 6e8e2027..a23e277e 100644 --- a/Carleson/Defs.lean +++ b/Carleson/Defs.lean @@ -73,48 +73,57 @@ lemma fact_isCompact_ball (x : X) (r : ℝ) : Fact (IsBounded (ball x r)) := ⟨isBounded_ball⟩ attribute [local instance] fact_isCompact_ball -/-- A class stating that continuous functions have distances associated to every ball. -/ +/-- A class stating that continuous functions have distances associated to every ball. +We use a separate type to conveniently index these functions. -/ class FunctionDistances (π•œ : outParam Type*) (X : Type u) [NormedField π•œ] [TopologicalSpace X] where - ΞΉ' : Type u - Θ : ΞΉ' β†’ C(X, π•œ) - out : βˆ€ (_x : X) (_r : ℝ), PseudoMetricSpace ΞΉ' + Θ : Type u + coeΘ : Θ β†’ C(X, π•œ) + metric : βˆ€ (_x : X) (_r : ℝ), PseudoMetricSpace Θ -export FunctionDistances (ΞΉ' Θ) +export FunctionDistances (Θ coeΘ) + +section FunctionDistances +variable [FunctionDistances π•œ X] + +instance : Coe (Θ X) C(X, π•œ) := ⟨coeΘ⟩ +instance : CoeFun (Θ X) (fun _ ↦ X β†’ π•œ) := ⟨fun f ↦ coeΘ f⟩ set_option linter.unusedVariables false in -def WithFunctionDistance (x : X) (r : ℝ) [FunctionDistances π•œ X] := ΞΉ' X +def WithFunctionDistance (x : X) (r : ℝ) := Θ X variable {x : X} {r : ℝ} -def toWithFunctionDistance [FunctionDistances π•œ X] : ΞΉ' X ≃ WithFunctionDistance x r := +def toWithFunctionDistance [FunctionDistances π•œ X] : Θ X ≃ WithFunctionDistance x r := .refl _ --- instance : FunLike (WithFunctionDistance ΞΉ' x r) X π•œ := ContinuousMap.funLike --- instance : ContinuousMapClass (WithFunctionDistance ΞΉ' x r) X π•œ := +-- instance : FunLike (WithFunctionDistance Θ x r) X π•œ := ContinuousMap.funLike +-- instance : ContinuousMapClass (WithFunctionDistance Θ x r) X π•œ := -- ContinuousMap.toContinuousMapClass instance [d : FunctionDistances π•œ X] : PseudoMetricSpace (WithFunctionDistance x r) := - d.out x r + d.metric x r + +end FunctionDistances -local notation3 "dist_{" x " ," r "}" => @dist (WithFunctionDistance x r) _ -local notation3 "ball_{" x " ," r "}" => @ball (WithFunctionDistance x r) _ in +notation3 "dist_{" x " ," r "}" => @dist (WithFunctionDistance x r) _ +notation3 "ball_{" x " ," r "}" => @ball (WithFunctionDistance x r) _ in /-- A set `Θ` of (continuous) functions is compatible. `A` will usually be `2 ^ a`. -/ class CompatibleFunctions (π•œ : outParam Type*) (X : Type u) (A : outParam ℝ) [RCLike π•œ] [PseudoMetricSpace X] extends FunctionDistances π•œ X where - eq_zero : βˆƒ o : X, βˆ€ f, Θ f o = 0 + eq_zero : βˆƒ o : X, βˆ€ f : Θ, f o = 0 /-- The distance is bounded below by the local oscillation. -/ - localOscillation_le_cdist {x : X} {r : ℝ} {f g : ΞΉ'} : - localOscillation (ball x r) (Θ f) (Θ g) ≀ dist_{x, r} f g + localOscillation_le_cdist {x : X} {r : ℝ} {f g : Θ} : + localOscillation (ball x r) (coeΘ f) (coeΘ g) ≀ dist_{x, r} f g /-- The distance is monotone in the ball. -/ - cdist_mono {x₁ xβ‚‚ : X} {r₁ rβ‚‚ : ℝ} {f g : ΞΉ'} + cdist_mono {x₁ xβ‚‚ : X} {r₁ rβ‚‚ : ℝ} {f g : Θ} (h : ball x₁ r₁ βŠ† ball xβ‚‚ rβ‚‚) : dist_{x₁, rβ‚‚} f g ≀ dist_{xβ‚‚, rβ‚‚} f g /-- The distance of a ball with large radius is bounded above. -/ - cdist_le {x₁ xβ‚‚ : X} {r : ℝ} {f g : ΞΉ'} (h : dist x₁ xβ‚‚ < 2 * r) : + cdist_le {x₁ xβ‚‚ : X} {r : ℝ} {f g : Θ} (h : dist x₁ xβ‚‚ < 2 * r) : dist_{xβ‚‚, 2 * r} f g ≀ A * dist_{x₁, r} f g /-- The distance of a ball with large radius is bounded below. -/ - le_cdist {x₁ xβ‚‚ : X} {r : ℝ} {f g : ΞΉ'} (h1 : ball x₁ r βŠ† ball xβ‚‚ (A * r)) + le_cdist {x₁ xβ‚‚ : X} {r : ℝ} {f g : Θ} (h1 : ball x₁ r βŠ† ball xβ‚‚ (A * r)) /-(h2 : A * r ≀ Metric.diam (univ : Set X))-/ : 2 * dist_{x₁, r} f g ≀ dist_{xβ‚‚, A * r} f g /-- The distance of a ball with large radius is bounded below. -/ @@ -127,11 +136,11 @@ variable (X) in /-- The point `o` in the blueprint -/ def cancelPt [CompatibleFunctions π•œ X A] : X := CompatibleFunctions.eq_zero (π•œ := π•œ) |>.choose -def cancelPt_eq_zero [CompatibleFunctions π•œ X A] {f : ΞΉ' X} : Θ f (cancelPt X) = 0 := +def cancelPt_eq_zero [CompatibleFunctions π•œ X A] {f : Θ X} : f (cancelPt X) = 0 := CompatibleFunctions.eq_zero (π•œ := π•œ) |>.choose_spec f lemma CompatibleFunctions.IsSeparable [CompatibleFunctions π•œ X A] : - IsSeparable (range (Θ (X := X))) := + IsSeparable (range (coeΘ (X := X))) := sorry set_option linter.unusedVariables false in @@ -141,10 +150,10 @@ def iLipNorm {π•œ} [NormedField π•œ] (Ο• : X β†’ π•œ) (xβ‚€ : X) (R : ℝ) : variable (X) in /-- Θ is Ο„-cancellative. `Ο„` will usually be `1 / a` -/ -class IsCancellative (Ο„ : ℝ) [CompatibleFunctions β„‚ X A] : Prop where +class IsCancellative (Ο„ : ℝ) [CompatibleFunctions ℝ X A] : Prop where norm_integral_exp_le {x : X} {r : ℝ} {Ο• : X β†’ β„‚} {K : ℝβ‰₯0} (h1 : LipschitzWith K Ο•) - (h2 : tsupport Ο• βŠ† ball x r) {f g : ΞΉ' X} : - β€–βˆ« x in ball x r, exp (I * (Θ f x - Θ g x)) * Ο• xβ€– ≀ + (h2 : tsupport Ο• βŠ† ball x r) {f g : Θ X} : + β€–βˆ« x in ball x r, exp (I * (f x - g x)) * Ο• xβ€– ≀ A * volume.real (ball x r) * iLipNorm Ο• x r * (1 + dist_{x, r} f g) ^ (- Ο„) export IsCancellative (norm_integral_exp_le) @@ -188,25 +197,26 @@ def NormBoundedBy {E F : Type*} [NormedAddCommGroup E] [NormedAddCommGroup F] (T Prop := βˆ€ x, β€–T xβ€– ≀ c * β€–xβ€– +def HasStrongType {E E' Ξ± Ξ±' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] + {_x : MeasurableSpace Ξ±} {_x' : MeasurableSpace Ξ±'} (T : (Ξ± β†’ E) β†’ (Ξ±' β†’ E')) + (ΞΌ : Measure Ξ±) (Ξ½ : Measure Ξ±') (p p' : ℝβ‰₯0∞) (c : ℝβ‰₯0) : Prop := + βˆ€ f : Ξ± β†’ E, Memβ„’p f p ΞΌ β†’ AEStronglyMeasurable (T f) Ξ½ ∧ snorm (T f) p' Ξ½ ≀ c * snorm f p ΞΌ + set_option linter.unusedVariables false in /-- The associated nontangential Calderon Zygmund operator -/ -def ANCZOperator (K : X β†’ X β†’ β„‚) (f : X β†’ β„‚) (x : X) : ℝβ‰₯0∞ := +def ANCZOperator (K : X β†’ X β†’ β„‚) (f : X β†’ β„‚) (x : X) : ℝ := ⨆ (R₁ : ℝ) (Rβ‚‚ : ℝ) (h1 : R₁ < Rβ‚‚) (x' : X) (h2 : dist x x' ≀ R₁), - β€–βˆ« y in {y | dist x' y ∈ Ioo R₁ Rβ‚‚}, K x' y * f yβ€–β‚Š - -/-- The associated nontangential Calderon Zygmund operator, viewed as a map `L^p β†’ L^p`. -Todo: is `T_*f` indeed in L^p if `f` is? Needed at least for `p = 2`. -/ -def ANCZOperatorLp (p : ℝβ‰₯0∞) [Fact (1 ≀ p)] (K : X β†’ X β†’ β„‚) (f : Lp β„‚ p (volume : Measure X)) : - Lp ℝ p (volume : Measure X) := - Memβ„’p.toLp (ANCZOperator K (f : X β†’ β„‚) Β· |>.toReal) sorry + β€–βˆ« y in {y | dist x' y ∈ Ioo R₁ Rβ‚‚}, K x' y * f yβ€–β‚Š |>.toReal --- /-- The generalized Carleson operator `T`, using real suprema -/ --- def Real.CarlesonOperator (K : X β†’ X β†’ β„‚) (Θ : Set C(X, β„‚)) (f : X β†’ β„‚) (x : X) : ℝ := --- ⨆ (Q ∈ Θ) (R₁ : ℝ) (Rβ‚‚ : ℝ) (_ : 0 < R₁) (_ : R₁ < Rβ‚‚), --- β€–βˆ« y in {y | dist x y ∈ Ioo R₁ Rβ‚‚}, K x y * f y * Complex.exp (I * Q y)β€– +-- /-- The associated nontangential Calderon Zygmund operator, viewed as a map `L^p β†’ L^p`. +-- Todo: is `T_*f` indeed in L^p if `f` is? Needed at least for `p = 2`. -/ +-- def ANCZOperatorLp (p : ℝβ‰₯0∞) [Fact (1 ≀ p)] (K : X β†’ X β†’ β„‚) +-- (f : Lp β„‚ p (volume : Measure X)) : Lp ℝ p (volume : Measure X) := +-- Memβ„’p.toLp (ANCZOperator K (f : X β†’ β„‚) Β· |>.toReal) sorry -/-- The generalized Carleson operator `T`, ℝβ‰₯0∞ version -/ +/-- The generalized Carleson operator `T`, taking values in `ℝβ‰₯0∞`. +Use `ENNReal.toReal` to get the corresponding real number. -/ --TODO: remove the last two suprema? -def CarlesonOperator (K : X β†’ X β†’ β„‚) (Θ : Set C(X, β„‚)) (f : X β†’ β„‚) (x : X) : ℝβ‰₯0∞ := - ⨆ (Q ∈ Θ) (R₁ : ℝ) (Rβ‚‚ : ℝ) (_ : 0 < R₁) (_ : R₁ < Rβ‚‚), +def CarlesonOperator [FunctionDistances ℝ X] (K : X β†’ X β†’ β„‚) (f : X β†’ β„‚) (x : X) : ℝβ‰₯0∞ := + ⨆ (Q : Θ X) (R₁ : ℝ) (Rβ‚‚ : ℝ) (_ : 0 < R₁) (_ : R₁ < Rβ‚‚), β†‘β€–βˆ« y in {y | dist x y ∈ Ioo R₁ Rβ‚‚}, K x y * f y * exp (I * Q y)β€–β‚Š diff --git a/Carleson/DiscreteCarleson.lean b/Carleson/DiscreteCarleson.lean index feae3730..8d80f119 100644 --- a/Carleson/DiscreteCarleson.lean +++ b/Carleson/DiscreteCarleson.lean @@ -1,51 +1,43 @@ import Carleson.GridStructure +import Carleson.Psi -- import Carleson.Proposition2 -- import Carleson.Proposition3 -open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators +open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology open scoped ENNReal noncomputable section -/- The constant used in proposition2_1 -/ -def C2_1 (a : ℝ) (q : ℝ) : ℝ := 2 ^ (440 * a ^ 3) / (q - 1) ^ 4 +/- The constant used in Proposition 2.0.2 -/ +def C2_2 (a : ℝ) (q : ℝ) : ℝ := 2 ^ (440 * a ^ 3) / (q - 1) ^ 4 -lemma C2_1_pos (a q : ℝ) : C2_1 a q > 0 := sorry +lemma C2_2_pos (a q : ℝ) : C2_2 a q > 0 := sorry -def D2_1 (A : ℝ) (Ο„ q : ℝ) (C : ℝ) : ℝ := sorry +def D2_2 (a : ℝ) : ℝ := 2 ^ (100 * a ^ 2) -lemma D2_1_pos (A : ℝ) (Ο„ q : ℝ) (C : ℝ) : D2_1 A Ο„ q C > 0 := sorry +lemma D2_2_pos (a : ℝ) : D2_2 a > 0 := sorry -def ΞΊ2_1 (A : ℝ) (Ο„ q : ℝ) (C : ℝ) : ℝ := sorry +def ΞΊ2_2 (A : ℝ) (Ο„ q : ℝ) (C : ℝ) : ℝ := sorry -lemma ΞΊ2_1_pos (A : ℝ) (Ο„ q : ℝ) (C : ℝ) : ΞΊ2_1 A Ο„ q C > 0 := sorry +lemma ΞΊ2_2_pos (A : ℝ) (Ο„ q : ℝ) (C : ℝ) : ΞΊ2_2 A Ο„ q C > 0 := sorry --- this should be `10 * D` or something -def Cψ2_1 (A : ℝ) (Ο„ q : ℝ) (C : ℝ) : ℝβ‰₯0 := sorry - -lemma Cψ2_1_pos (A : ℝ) (Ο„ : ℝ) (C : ℝ) : Cψ2_1 A Ο„ C > 0 := sorry - -/- -variable {X : Type*} {A : ℝ} [MetricSpace X] [DoublingMeasure X A] [Inhabited X] +variable {X : Type*} {a : ℝ} [MetricSpace X] [DoublingMeasure X (2 ^ a)] [Inhabited X] variable {Ο„ q q' D ΞΊ : ℝ} {Cβ‚€ C : ℝ} -variable {Θ : Set C(X, β„‚)} [IsCompatible Θ] [IsCancellative Ο„ Θ] [TileStructure Θ D ΞΊ Cβ‚€] -variable {F G : Set X} {Οƒ Οƒ' : X β†’ β„€} {Q' : X β†’ C(X, β„‚)} /- Q-tilde in the pdf -/ +variable [CompatibleFunctions ℝ X (2 ^ a)] [IsCancellative X Ο„] +variable {Q : X β†’ Θ X} {S : β„€} {o : X} [TileStructure Q D ΞΊ C S o] +variable {F G : Set X} {σ₁ Οƒβ‚‚ : X β†’ β„€} {Q : X β†’ Θ X} variable (K : X β†’ X β†’ β„‚) [IsCZKernel Ο„ K] -variable {ψ : ℝ β†’ ℝ} -- todo: add some conditions that Οƒ and other functions have finite range? -- todo: fix statement theorem discrete_carleson - (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β‚€)) + (hA : 4 ≀ a) (hΟ„ : Ο„ ∈ Ioo 0 1) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q') + -- (hCβ‚€ : 0 < Cβ‚€) (hC : C2_2 A Ο„ q Cβ‚€ < C) (hD : D2_2 A Ο„ q Cβ‚€ < D) + (hΞΊ : ΞΊ ∈ Ioo 0 (ΞΊ2_2 (2 ^ a) Ο„ q Cβ‚€)) (hF : MeasurableSet F) (hG : MeasurableSet G) - (h2F : volume F ∈ Ioo 0 ∞) (h2G : volume G ∈ Ioo 0 ∞) - (Q'_mem : βˆ€ x, Q' x ∈ Θ) (m_Q' : Measurable Q') - (m_Οƒ : Measurable Οƒ) (m_Οƒ' : Measurable Οƒ') - (hT : NormBoundedBy (ANCZOperatorLp 2 K) 1) - (hψ : LipschitzWith (Cψ2_1 A Ο„ q Cβ‚€) ψ) - (h2ψ : support ψ βŠ† Icc (4 * D)⁻¹ 2⁻¹) (h3ψ : βˆ€ x > 0, βˆ‘αΆ  s : β„€, ψ (D ^ s * x) = 1) + (h2F : IsBounded F) (h2G : IsBounded G) + (m_σ₁ : Measurable σ₁) (m_Οƒβ‚‚ : Measurable Οƒβ‚‚) + (hT : HasStrongType (ANCZOperator K) volume volume 2 2 1) : - βˆƒ G', volume G' ≀ volume G / 4 ∧ β€–βˆ« x in G \ G', βˆ‘' p, T K Q' Οƒ Οƒ' ψ p F 1 xβ€–β‚Š ≀ - C * (volume.real G) ^ (1 / q') * (volume.real F) ^ (1 / q) := by sorry --/ + βˆƒ G', 2 * volume G' ≀ volume G ∧ βˆ€ f : X β†’ β„‚, (βˆ€ x, β€–f xβ€– ≀ F.indicator 1 x) β†’ + β€–βˆ« x in G \ G', βˆ‘' p, T K σ₁ Οƒβ‚‚ (ψ (D2_2 a)) p F 1 xβ€–β‚Š ≀ + C2_2 a q * (volume.real G) ^ (1 / q') * (volume.real F) ^ (1 / q) := by sorry diff --git a/Carleson/GridStructure.lean b/Carleson/GridStructure.lean index ae309a10..06df58f6 100644 --- a/Carleson/GridStructure.lean +++ b/Carleson/GridStructure.lean @@ -4,7 +4,7 @@ open Set MeasureTheory Metric Function Complex open scoped ENNReal noncomputable section -variable {π•œ : Type*} {A : ℝ} [_root_.RCLike π•œ] +variable {π•œ : Type*} [_root_.RCLike π•œ] variable {X : Type*} {A : ℝ} [PseudoMetricSpace X] [DoublingMeasure X A] variable (X) in @@ -70,8 +70,8 @@ class TileStructureData.{u} [FunctionDistances π•œ X] fintype_𝔓 : Fintype 𝔓 protected π“˜ : 𝔓 β†’ ΞΉ surjective_π“˜ : Surjective π“˜ - Ξ© : 𝔓 β†’ Set (ΞΉ' X) - 𝒬 : 𝔓 β†’ ΞΉ' X + Ξ© : 𝔓 β†’ Set (Θ X) + 𝒬 : 𝔓 β†’ Θ X export TileStructureData (Ξ© 𝒬) @@ -91,10 +91,10 @@ notation3 "dist_(" D "," 𝔭 ")" => @dist (WithFunctionDistance (𝔠 𝔭) (D notation3 "ball_(" D "," 𝔭 ")" => @ball (WithFunctionDistance (𝔠 𝔭) (D ^ 𝔰 𝔭 / 4)) _ /-- A tile structure. -/ -class TileStructure [FunctionDistances β„‚ X] (Q : outParam (X β†’ C(X, β„‚))) +class TileStructure [FunctionDistances ℝ X] (Q : outParam (X β†’ Θ X)) (D ΞΊ C : outParam ℝ) (S : outParam β„€) (o : outParam X) extends TileStructureData D ΞΊ C S o where - biUnion_Ξ© {i} : range Q βŠ† Θ '' ⋃ p ∈ π“˜ ⁻¹' {i}, Ξ© p + biUnion_Ξ© {i} : range Q βŠ† ⋃ p ∈ π“˜ ⁻¹' {i}, Ξ© p disjoint_Ξ© {p p'} (h : p β‰  p') (hp : π“˜ p = π“˜ p') : Disjoint (Ξ© p) (Ξ© p') relative_fundamental_dyadic {p p'} (h : 𝓓 (π“˜ p) βŠ† 𝓓 (π“˜ p')) : Disjoint (Ξ© p) (Ξ© p') ∨ Ξ© p' βŠ† Ξ© p cdist_subset {p} : ball_(D, p) (𝒬 p) 5⁻¹ βŠ† Ξ© p @@ -102,33 +102,33 @@ class TileStructure [FunctionDistances β„‚ X] (Q : outParam (X β†’ C(X, β„‚))) export TileStructure (biUnion_Ξ© disjoint_Ξ© relative_fundamental_dyadic cdist_subset subset_cdist) -variable {Q : X β†’ C(X, β„‚)} [FunctionDistances β„‚ X] [TileStructure Q D ΞΊ C S o] +variable [FunctionDistances ℝ X] {Q : X β†’ Θ X} [TileStructure Q D ΞΊ C S o] -/- The set `E` defined in Proposition 2.1. -/ -def E (Οƒ Οƒ' : X β†’ β„€) (p : 𝔓 X) : Set X := - { x ∈ 𝓓 (π“˜ p) | Q x ∈ Θ '' Ξ© p ∧ 𝔰 p ∈ Icc (Οƒ x) (Οƒ' x) } +/- The set `E` defined in Proposition 2.0.2. -/ +def E (σ₁ Οƒβ‚‚ : X β†’ β„€) (p : 𝔓 X) : Set X := + { x ∈ 𝓓 (π“˜ p) | Q x ∈ Ξ© p ∧ 𝔰 p ∈ Icc (σ₁ x) (Οƒβ‚‚ x) } section T -variable (K : X β†’ X β†’ β„‚) (Οƒ Οƒ' : X β†’ β„€) (ψ : ℝ β†’ ℝ) (p : 𝔓 X) (F : Set X) +variable (K : X β†’ X β†’ β„‚) (σ₁ Οƒβ‚‚ : X β†’ β„€) (ψ : ℝ β†’ ℝ) (p : 𝔓 X) (F : Set X) -/- The operator `T` defined in Proposition 2.1, considered on the set `F`. +/- The operator `T` defined in Proposition 2.0.2, considered on the set `F`. It is the map `T ∘ (1_F * Β·) : f ↦ T (1_F * f)`, also denoted `T1_F` -The operator `T` in Proposition 2.1 is therefore `applied to `(F := Set.univ)`. -/ +The operator `T` in Proposition 2.0.2 is therefore `applied to `(F := Set.univ)`. -/ def T (f : X β†’ β„‚) : X β†’ β„‚ := - indicator (E Οƒ Οƒ' p) + indicator (E σ₁ Οƒβ‚‚ p) fun x ↦ ∫ y, exp (Q x x - Q x y) * K x y * ψ (D ^ (- 𝔰 p) * dist x y) * F.indicator f y -lemma Memβ„’p_T {f : X β†’ β„‚} {q : ℝβ‰₯0∞} (hf : Memβ„’p f q) : Memβ„’p (T K Οƒ Οƒ' ψ p F f) q := +lemma Memβ„’p_T {f : X β†’ β„‚} {q : ℝβ‰₯0∞} (hf : Memβ„’p f q) : Memβ„’p (T K σ₁ Οƒβ‚‚ ψ p F f) q := by sorry /- The operator `T`, defined on `L^2` maps. -/ def Tβ‚‚ (f : X β†’β‚‚[volume] β„‚) : X β†’β‚‚[volume] β„‚ := - Memβ„’p.toLp (T K Οƒ Οƒ' ψ p F f) <| Memβ„’p_T K Οƒ Οƒ' ψ p F <| Lp.memβ„’p f + Memβ„’p.toLp (T K σ₁ Οƒβ‚‚ ψ p F f) <| Memβ„’p_T K σ₁ Οƒβ‚‚ ψ p F <| Lp.memβ„’p f /- The operator `T`, defined on `L^2` maps as a continuous linear map. -/ def TL : (X β†’β‚‚[volume] β„‚) β†’L[β„‚] (X β†’β‚‚[volume] β„‚) where - toFun := Tβ‚‚ K Οƒ Οƒ' ψ p F + toFun := Tβ‚‚ K σ₁ Οƒβ‚‚ ψ p F map_add' := sorry map_smul' := sorry cont := by sorry @@ -136,10 +136,10 @@ def TL : (X β†’β‚‚[volume] β„‚) β†’L[β„‚] (X β†’β‚‚[volume] β„‚) where end T variable (X) in -def TileLike : Type _ := Set X Γ— OrderDual (Set (ΞΉ' X)) +def TileLike : Type _ := Set X Γ— OrderDual (Set (Θ X)) def TileLike.fst (x : TileLike X) : Set X := x.1 -def TileLike.snd (x : TileLike X) : Set (ΞΉ' X) := x.2 +def TileLike.snd (x : TileLike X) : Set (Θ X) := x.2 instance : PartialOrder (TileLike X) := by dsimp [TileLike]; infer_instance example (x y : TileLike X) : x ≀ y ↔ x.fst βŠ† y.fst ∧ y.snd βŠ† x.snd := by rfl @@ -150,9 +150,9 @@ lemma toTileLike_injective : Injective (fun p : 𝔓 X ↦ toTileLike p) := sorr instance : PartialOrder (𝔓 X) := PartialOrder.lift toTileLike toTileLike_injective def smul (a : ℝ) (p : 𝔓 X) : TileLike X := - sorry --(𝓓 (π“˜ p), localOscillationBall (𝓓 (π“˜ p)) (Θ (𝒬 p)) a) + (𝓓 (π“˜ p), ball_(D, p) (𝒬 p) a) -def TileLike.toTile (t : TileLike X) : Set (X Γ— ΞΉ' X) := +def TileLike.toTile (t : TileLike X) : Set (X Γ— Θ X) := t.fst Γ—Λ’ t.snd lemma isAntichain_iff_disjoint (𝔄 : Set (𝔓 X)) : @@ -163,10 +163,10 @@ lemma isAntichain_iff_disjoint (𝔄 : Set (𝔓 X)) : def convexShadow (𝔓' : Set (𝔓 X)) : Set (ΞΉ X) := { i | βˆƒ p p' : 𝔓 X, p ∈ 𝔓' ∧ p' ∈ 𝔓' ∧ (𝓓 (π“˜ p) : Set X) βŠ† 𝓓 i ∧ 𝓓 i βŠ† 𝓓 (π“˜ p') } -def EBar (G : Set X) (Q : X β†’ ΞΉ' X) (t : TileLike X) : Set X := +def EBar (G : Set X) (Q : X β†’ Θ X) (t : TileLike X) : Set X := { x ∈ t.fst ∩ G | Q x ∈ t.snd } -def density (G : Set X) (Q : X β†’ ΞΉ' X) (𝔓' : Set (𝔓 X)) : ℝ := +def density (G : Set X) (Q : X β†’ Θ X) (𝔓' : Set (𝔓 X)) : ℝ := ⨆ (p ∈ 𝔓') (l β‰₯ (2 : ℝ)), l ^ (-2 * Real.log A) * ⨆ (p' : 𝔓 X) (_h : π“˜ p' ∈ convexShadow 𝔓') (_h2 : smul l p ≀ smul l p'), volume.real (EBar G Q (smul l p')) / volume.real (EBar G Q (toTileLike p)) diff --git a/Carleson/MetricCarleson.lean b/Carleson/MetricCarleson.lean index 87660a53..330320b4 100644 --- a/Carleson/MetricCarleson.lean +++ b/Carleson/MetricCarleson.lean @@ -32,7 +32,6 @@ section -- todo: old code variable {X : Type*} {a : ℝ} [MetricSpace X] [DoublingMeasure X (2 ^ a)] [Inhabited X] variable {Ο„ q q' : ℝ} {C : ℝ} -variable {Θ : Set C(X, β„‚)} variable {F G : Set X} variable (K : X β†’ X β†’ β„‚) @@ -130,16 +129,17 @@ segment. -/ (section 2). -/ /- Theorem 1.2, written using constant C1_2 -/ -theorem metric_carleson [CompatibleFunctions β„‚ X (2 ^ a)] +theorem metric_carleson [CompatibleFunctions ℝ X (2 ^ a)] [IsCancellative X (2 ^ a)] [IsCZKernel a K] (ha : 4 ≀ a) (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) (2 ^ a ^ 3)) - (hT : βˆ€ (g : X β†’ β„‚) (hg : Memβ„’p g ∞) (h2g : volume (support g) < ∞) (h3g : Memβ„’p g 2 volume), - snorm (ANCZOperatorLp 2 K h3g.toLp) 2 volume ≀ 2 ^ a ^ (3 : β„•) * snorm g 2 volume) + (hT : βˆ€ (g : X β†’ β„‚) (hg : Memβ„’p g ∞ volume) (h2g : volume (support g) < ∞) + (h3g : Memβ„’p g 2 volume), + snorm (ANCZOperator K g) 2 volume ≀ 2 ^ a ^ (3 : β„•) * snorm g 2 volume) (f : X β†’ β„‚) (hf : βˆ€ x, β€–f xβ€– ≀ F.indicator 1 x) : - ∫⁻ x in G, CarlesonOperator K Θ f x ≀ + ∫⁻ x in G, CarlesonOperator K f x ≀ ENNReal.ofReal (C1_2 a q) * (volume G) ^ q'⁻¹ * (volume F) ^ q⁻¹ := by sorry diff --git a/Carleson/Proposition2.lean b/Carleson/Proposition2.lean index a6799252..c9d7f42b 100644 --- a/Carleson/Proposition2.lean +++ b/Carleson/Proposition2.lean @@ -3,7 +3,7 @@ import Carleson.GridStructure open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators open scoped ENNReal noncomputable section - +/- def C2_2 (A : ℝ) (Ο„ q : ℝ) (C : ℝ) : ℝ := sorry lemma C2_2_pos (A : ℝ) (Ο„ q : ℝ) (C : ℝ) : C2_2 A Ο„ q C > 0 := sorry @@ -24,7 +24,7 @@ lemma ΞΊ2_2_pos (A : ℝ) (Ο„ q : ℝ) (C : ℝ) : ΞΊ2_2 A Ο„ q C > 0 := sorry def Cψ2_2 (A : ℝ) (Ο„ q : ℝ) (C : ℝ) : ℝβ‰₯0 := sorry lemma Cψ2_2_pos (A : ℝ) (Ο„ : ℝ) (C : ℝ) : Cψ2_2 A Ο„ C > 0 := sorry -/- + variable {X : Type*} {A : ℝ} [MetricSpace X] [DoublingMeasure X A] [Inhabited X] variable {Ο„ q D ΞΊ Ξ΅ : ℝ} {Cβ‚€ C t : ℝ} variable {Θ : Set C(X, β„‚)} [IsCompatible Θ] [IsCancellative Ο„ Θ] [TileStructure Θ D ΞΊ Cβ‚€] diff --git a/Carleson/Theorem1_1/Basic.lean b/Carleson/Theorem1_1/Basic.lean index 73ef2331..dbedde19 100644 --- a/Carleson/Theorem1_1/Basic.lean +++ b/Carleson/Theorem1_1/Basic.lean @@ -211,7 +211,7 @@ lemma lower_secant_bound {Ξ· : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * Real.p /-TODO : relocate this-/ --TODO : call constructor in a better way? -def integer_linear (n : β„€) : C(ℝ, β„‚) := ⟨fun (x : ℝ) ↦ (n * x : β„‚), by continuity⟩ +def integer_linear (n : β„€) : C(ℝ, ℝ) := ⟨fun (x : ℝ) ↦ n * x, by fun_prop⟩ --local notation "ΞΈ" => integer_linear diff --git a/Carleson/Theorem1_1/Carleson_on_the_real_line.lean b/Carleson/Theorem1_1/Carleson_on_the_real_line.lean index 84280663..865460dd 100644 --- a/Carleson/Theorem1_1/Carleson_on_the_real_line.lean +++ b/Carleson/Theorem1_1/Carleson_on_the_real_line.lean @@ -12,6 +12,8 @@ import Mathlib.Analysis.SpecialFunctions.Integrals noncomputable section +open MeasureTheory Function Metric Bornology + --#lint section @@ -31,17 +33,17 @@ def DoublingMeasureR2 : DoublingMeasure ℝ 2 where sorry --exact this.volume_ball_two_le_same x r -instance DoublingMeasureR4 : DoublingMeasure ℝ (2 ^ 4) := +instance DoublingMeasureR4 : DoublingMeasure ℝ (2 ^ (4 : ℝ)) := DoublingMeasureR2.mono (by norm_num) end lemma h1 : 2 ∈ Set.Ioc 1 (2 : ℝ) := by simp lemma h2 : Real.IsConjExponent 2 2 := by rw [Real.isConjExponent_iff_eq_conjExponent] <;> norm_num -lemma localOscillation_on_emptyset {X : Type} [PseudoMetricSpace X] {f g : C(X, β„‚)} : localOscillation βˆ… f g = 0 := by +lemma localOscillation_on_emptyset {X : Type} [PseudoMetricSpace X] {f g : C(X, ℝ)} : localOscillation βˆ… f g = 0 := by simp [localOscillation] -lemma localOscillation_on_empty_ball {X : Type} [PseudoMetricSpace X] {x : X} {f g : C(X, β„‚)} {R : ℝ} (R_nonpos : R ≀ 0): +lemma localOscillation_on_empty_ball {X : Type} [PseudoMetricSpace X] {x : X} {f g : C(X, ℝ)} {R : ℝ} (R_nonpos : R ≀ 0): localOscillation (Metric.ball x R) f g = 0 := by convert localOscillation_on_emptyset exact Metric.ball_eq_empty.mpr R_nonpos @@ -98,12 +100,13 @@ section open ENNReal +section local notation "ΞΈ" => integer_linear local notation "Θ" => {(ΞΈ n) | n : β„€} -theorem localOscillation_of_same {X : Type} [PseudoMetricSpace X] {E : Set X} {f : C(X, β„‚)} : localOscillation E f f = 0 := by +theorem localOscillation_of_same {X : Type} [PseudoMetricSpace X] {E : Set X} {f : C(X, ℝ)} : localOscillation E f f = 0 := by rw [localOscillation] simp only [Set.mem_prod, sub_self, zero_sub, add_left_neg, norm_zero, Real.ciSup_const_zero] @@ -121,7 +124,7 @@ lemma localOscillation_of_integer_linear {x R : ℝ} (R_nonneg : 0 ≀ R) : βˆ€ rwa [sub_eq_zero, Int.cast_inj] /- Rewrite to a more convenient form for the following steps. -/ have norm_integer_linear_eq {n m : β„€} {z : ℝ Γ— ℝ} : β€–(ΞΈ n) z.1 - (ΞΈ m) z.1 - (ΞΈ n) z.2 + (ΞΈ m) z.2β€– = β€–(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)β€– := by - rw [←Complex.norm_real, integer_linear, integer_linear] + rw [integer_linear, integer_linear] congr 1 simp ring @@ -158,7 +161,7 @@ lemma localOscillation_of_integer_linear {x R : ℝ} (R_nonneg : 0 ≀ R) : βˆ€ by_cases c_nonneg : 0 > c . calc c _ < 0 := c_nonneg - _ ≀ @dist (withLocalOscillation β„‚ (Metric.ball x R)) PseudoMetricSpace.toDist (ΞΈ n) (ΞΈ m) := dist_nonneg + _ ≀ @dist (withLocalOscillation ℝ (Metric.ball x R)) PseudoMetricSpace.toDist (ΞΈ n) (ΞΈ m) := dist_nonneg _ = localOscillation (Metric.ball x R) (ΞΈ n) (ΞΈ m) := rfl _ = ⨆ z ∈ Metric.ball x R Γ—Λ’ Metric.ball x R, β€–(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)β€– := by rw [localOscillation] @@ -197,7 +200,7 @@ lemma localOscillation_of_integer_linear {x R : ℝ} (R_nonneg : 0 ≀ R) : βˆ€ apply le_abs_self _ ≀ ⨆ z ∈ Metric.ball x R Γ—Λ’ Metric.ball x R, β€–(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)β€– := by apply ConditionallyCompleteLattice.le_biSup - . convert bddAbove_localOscillation (Metric.ball x R) (ΞΈ n) (ΞΈ m) + . convert bddAbove_localOscillation (Metric.ball x R) (ΞΈ n) (ΞΈ m) using 2 apply norm_integer_linear_eq.symm . use y simp @@ -224,9 +227,24 @@ lemma bciSup_of_emptyset {Ξ± : Type} [ConditionallyCompleteLattice Ξ±] {ΞΉ : Ty rw [this] apply Set.range_const +end --lemma frequency_ball_doubling {x R : ℝ} (Rpos : 0 < R) : -instance h4 : CompatibleFunctions β„‚ ℝ (2 ^ 4) := sorry /-where +instance : FunctionDistances ℝ ℝ where + Θ := β„€ + coeΘ := integer_linear + metric := fun x R ↦ sorry + +lemma coeΘ_R (n : Θ ℝ) : coeΘ n = integer_linear n := rfl + +instance h4 : CompatibleFunctions ℝ ℝ (2 ^ (4 : ℝ)) where + eq_zero := sorry + localOscillation_le_cdist := sorry + cdist_mono := sorry + cdist_le := sorry + le_cdist := sorry + ballsCoverBalls := sorry +/- /- Lemma frequency_ball_doubling from the paper. -/ localOscillation_two_mul_le := by intro x₁ xβ‚‚ R f g hf hg _ @@ -403,7 +421,7 @@ instance h4 : CompatibleFunctions β„‚ ℝ (2 ^ 4) := sorry /-where --TODO : What is Lemma 10.34 (frequency ball growth) needed for? --TODO : possibly issues with a different "doubling constant" than in the paper (4 instead of 2) -instance h5 : IsCancellative ℝ (2 ^ 4) where +instance h5 : IsCancellative ℝ (2 ^ (4 : ℝ)) where /- Lemma 10.36 (real van der Corput) from the paper. -/ norm_integral_exp_le := by sorry @@ -452,7 +470,9 @@ instance h6 : IsCZKernel 4 K where measurable := Hilbert_kernel_measurable /- Lemma ?-/ -lemma h3 : NormBoundedBy (ANCZOperatorLp 2 K) 1 := sorry +lemma h3 (g : ℝ β†’ β„‚) (hg : Memβ„’p g ∞ volume) (h2g : volume (support g) < ∞) + (h3g : Memβ„’p g 2 volume) : + snorm (ANCZOperator K g) 2 volume ≀ 2 ^ (4 : ℝ) ^ 3 * snorm g 2 volume := sorry @@ -466,7 +486,7 @@ local notation "T'" => CarlesonOperatorReal' K /-Not sure whether this is actually true. Probably we only have "le" (which should suffice). -/ --TODO : change name to reflect that this only holds for a specific instance of CarlesonOperaterReal? -lemma CarlesonOperatorReal'_le_CarlesonOperator : T' ≀ CarlesonOperator K Θ := by +lemma CarlesonOperatorReal'_le_CarlesonOperator : T' ≀ CarlesonOperator K := by intro f x rw [CarlesonOperator, CarlesonOperatorReal'] apply iSup_le @@ -477,15 +497,18 @@ lemma CarlesonOperatorReal'_le_CarlesonOperator : T' ≀ CarlesonOperator K Θ : intro rpos apply iSup_le intro rle1 - apply le_iSupβ‚‚_of_le (ΞΈ n) (by simp) + apply le_iSup_of_le n apply le_iSupβ‚‚_of_le r 1 apply le_iSupβ‚‚_of_le rpos rle1 apply le_of_eq - rw [integer_linear, ContinuousMap.coe_mk] + rw [coeΘ_R, integer_linear, ContinuousMap.coe_mk] congr ext y + push_cast ring_nf + + /- Lemma 10.4 (ENNReal version) -/ lemma rcarleson' {F G : Set ℝ} (hF : MeasurableSet F) (hG : MeasurableSet G) @@ -496,11 +519,9 @@ lemma rcarleson' {F G : Set ℝ} ENNReal.ofReal (C1_2 4 2) * (MeasureTheory.volume G) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ := by --rw [CarlesonOperatorReal_eq_CarlesonOperator] calc ∫⁻ x in G, T' f x - _ ≀ ∫⁻ x in G, CarlesonOperator K Θ f x := by + _ ≀ ∫⁻ x in G, CarlesonOperator K f x := by apply MeasureTheory.lintegral_mono apply CarlesonOperatorReal'_le_CarlesonOperator - _ ≀ ENNReal.ofReal (C1_2 4 2) * (MeasureTheory.volume G) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ := by - --WARNING : metric_carleson does not yet require all necessary implicit parameters since no proof using them has been provided yet. - convert metric_carleson (a := 4) K (by norm_num) h1 h2 sorry /- hF-/ sorry sorry f hf <;> sorry + _ ≀ ENNReal.ofReal (C1_2 4 2) * (MeasureTheory.volume G) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ := metric_carleson (a := 4) K (by norm_num) h1 h2 hF hG h3 f hf end section