diff --git a/Carleson/Carleson.lean b/Carleson/Carleson.lean index 4627a58e..63c1ad35 100644 --- a/Carleson/Carleson.lean +++ b/Carleson/Carleson.lean @@ -3,12 +3,11 @@ import Carleson.Proposition1 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 -/- The constant used in theorem1_1 -/ -def C1_1 (A : ℝ) (τ q : ℝ) : ℝ := sorry +/- The constant used in theorem1_2 -/ +def C1_2 (a q : ℝ) : ℝ := 2 ^ (270 * a ^ 3) / (q - 1) ^ 5 -lemma C1_1_pos (A : ℝ) (τ q : ℝ) : C1_1 A τ q > 0 := sorry +lemma C1_1_pos (a q : ℝ) (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) : C1_2 a q > 0 := sorry /- The constant used in equation (2.2) -/ def Ce2_2 (A : ℝ) (τ q : ℝ) : ℝ := sorry @@ -20,13 +19,13 @@ def Ce3_1 (A : ℝ) (τ q : ℝ) : ℝ := sorry lemma Ce3_1_pos (A : ℝ) (τ q : ℝ) : Ce3_1 A τ q > 0 := sorry -section +section -- todo: old code -variable {X : Type*} {A : ℝ} [MetricSpace X] [IsSpaceOfHomogeneousType X A] [Inhabited X] +variable {X : Type*} {a : ℝ} [MetricSpace X] [IsSpaceOfHomogeneousType X a] [Inhabited X] variable {τ q q' : ℝ} {C : ℝ} -variable {𝓠 : Set C(X, ℂ)} [IsCompatible 𝓠] [IsCancellative τ 𝓠] +variable {Θ : Set C(X, ℂ)} [IsCompatible Θ] [IsCancellative a Θ] variable {F G : Set X} -variable (K : X → X → ℂ) [IsCZKernel τ K] +variable (K : X → X → ℂ) [IsCZKernel a K] def D1_1 (A : ℝ) (τ q : ℝ) : ℝ := sorry @@ -38,7 +37,7 @@ def Cψ1_1 (A : ℝ) (τ q : ℝ) : ℝ≥0 := sorry lemma Cψ1_1_pos (A : ℝ) (τ : ℝ) : Cψ2_1 A τ C > 0 := sorry -/- extra variables not in theorem 1.1. -/ +/- extra variables not in theorem 1.2. -/ variable {D : ℝ} {ψ : ℝ → ℝ} {s : ℤ} {x y : X} /- the one or two numbers `s` where `ψ (D ^ s * x)` is possibly nonzero -/ @@ -47,20 +46,18 @@ variable (D) in def nonzeroS (x : ℝ) : Finset ℤ := variable - (hD : D > D1_1 A τ q) - (hψ : LipschitzWith (Cψ1_1 A τ q) ψ) + (hD : D > D1_1 a τ q) + (hψ : LipschitzWith (Cψ1_1 a τ q) ψ) (h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹) (h3ψ : ∀ x > 0, ∑ s in nonzeroS D x, ψ (D ^ s * x) = 1) -- move -theorem Int.floor_le_iff (a : ℝ) (z : ℤ) : ⌊a⌋ ≤ z ↔ a < z + 1 := by +theorem Int.floor_le_iff (c : ℝ) (z : ℤ) : ⌊c⌋ ≤ z ↔ c < z + 1 := by 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 +theorem Int.le_ceil_iff (c : ℝ) (z : ℤ) : z ≤ ⌈c⌉ ↔ z - 1 < c := by rw_mod_cast [← Int.add_one_le_ceil_iff, sub_add_cancel] -example (a b c : ℝ) (hc : 0 < c) : a < b / c ↔ a * c < b := by exact _root_.lt_div_iff hc - lemma mem_nonzeroS_iff {i : ℤ} {x : ℝ} (hx : 0 < x) (hD : 1 < D) : i ∈ nonzeroS D x ↔ (D ^ i * x) ∈ Ioo (4 * D)⁻¹ 2⁻¹ := by rw [Set.mem_Ioo, nonzeroS, Finset.mem_Icc] @@ -100,13 +97,13 @@ lemma sum_Ks' {s : Finset ℤ} - +-- old /- (No need to take the supremum over the assumption `σ < σ'`.) -/ lemma equation3_1 {f : X → ℂ} (hf : LocallyIntegrable f) - (h𝓠 : ∀ Q ∈ 𝓠, ∀ x, (Q x).im = 0) : - let rhs := Ce3_1 A τ q * maximalFunction f x + ⨆ (Q ∈ 𝓠) (σ : ℤ) (σ' : ℤ), + (hΘ : ∀ Q ∈ Θ, ∀ x, (Q x).im = 0) : + let rhs := Ce3_1 a τ q * maximalFunction f x + ⨆ (Q ∈ Θ) (σ : ℤ) (σ' : ℤ), ‖∑ 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 + CarlesonOperator K Θ f x ≤ rhs := by intro rhs have h_rhs : 0 ≤ rhs := by sorry @@ -118,13 +115,13 @@ lemma equation3_1 {f : X → ℂ} (hf : LocallyIntegrable f) refine Real.iSup_le (fun hrR ↦ ?_) h_rhs let σ : ℤ := ⌊Real.logb D (2 * r)⌋ + 1 let σ' : ℤ := ⌈Real.logb D (4 * R)⌉ - trans Ce3_1 A τ q * maximalFunction f x + + trans Ce3_1 a τ q * maximalFunction f x + ‖∑ s in Finset.Icc σ σ', ∫ y, Ks K D ψ s x y * f y * exp (I * (Q y - Q x))‖ 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 := by - lift Q x to ℝ using h𝓠 Q hQ x with qx + 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 -/ @@ -139,12 +136,10 @@ lemma equation3_1 {f : X → ℂ} (hf : LocallyIntegrable f) rw [h3, ← neg_sub, ← integral_univ, ← integral_diff] all_goals sorry - /- Proof should be straightforward from the definition of maximalFunction and conditions on `𝓠`. + /- Proof should be straightforward from the definition of maximalFunction and conditions on `Θ`. We have to approximate `Q` by an indicator function. 2^σ ≈ r, 2^σ' ≈ R There is a small difference in integration domain, and for that we use the estimate IsCZKernel.norm_le_vol_inv - - -/ variable (C F G) in @@ -153,7 +148,7 @@ def G₀' : Set X := { x : X | maximalFunction (F.indicator (1 : X → ℂ)) x > C * volume.real F / volume.real G } /- estimation of the volume of G₀' -/ -lemma volume_G₀'_pos (hC : C1_1 A τ q < C) : volume.real (G₀' C F G) ≤ volume.real G / 4 := sorry +-- lemma volume_G₀'_pos (hC : C1_2 A τ q < C) : volume.real (G₀' C F G) ≤ volume.real G / 4 := sorry /- estimate first term (what does this mean exactly?) -/ @@ -171,47 +166,30 @@ segment. -/ /- Lemma 3.3: obtain tile structure -/ /- finish proof of equation (2.2) -/ - +-- old theorem equation2_2 - (hA : 1 < A) (hτ : τ ∈ Ioo 0 1) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent 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) : + (hT : NormBoundedBy (ANCZOperatorLp 2 K) (2 ^ a ^ 3)) : ∃ G', volume G' ≤ volume G / 2 ∧ - ‖∫ x in G \ G', CarlesonOperator K 𝓠 (indicator F 1) x‖₊ ≤ - Ce2_2 A τ q * (volume.real G) ^ (1 / q') * (volume.real F) ^ (1 / q) := by + ‖∫ x in G \ G', CarlesonOperator K Θ (indicator F 1) x‖₊ ≤ + Ce2_2 a τ q * (volume.real G) ^ (1 / q') * (volume.real F) ^ (1 / q) := by sorry /- to prove theorem 1.1 from (2.2): bootstrapping argument, recursing over excised sets. (section 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.IsConjExponent q') +/- Theorem 1.2, written using constant C1_2 -/ +theorem theorem1_2C + (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) 1) : - ‖∫ x in G, CarlesonOperator K 𝓠 (indicator F 1) x‖₊ ≤ - C1_1 A τ q * (volume.real G) ^ (1 / q') * (volume.real F) ^ (1 / q) := by + (hT : NormBoundedBy (ANCZOperatorLp 2 K) 1) (f : X → ℂ) + (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) : + ‖∫ x in G, CarlesonOperator K Θ f x‖ ≤ + C1_2 a q * (volume.real G) ^ q'⁻¹ * (volume.real F) ^ q⁻¹ := by sorry -/- Specialize this to get the usual version of Carleson's theorem, -by taking `X = ℝ`, `K x y := 1 / (x - y)` and `𝓠 = {linear functions}`. --/ 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.IsConjExponent q') : ∃ (C : ℝ), C > 0 ∧ - ∀ {X : Type*} [MetricSpace X] [IsSpaceOfHomogeneousType X A] [Inhabited X] - (𝓠 : Set C(X, ℂ)) [IsCompatible 𝓠] [IsCancellative τ 𝓠] - (K : X → X → ℂ) [IsCZKernel τ K] - (hT : NormBoundedBy (ANCZOperatorLp 2 K) 1) - {F G : Set X} (hF : MeasurableSet F) (hG : MeasurableSet G), - ‖∫ x in G, CarlesonOperator K 𝓠 (indicator F 1) x‖₊ ≤ - C * (volume.real G) ^ (1 / q') * (volume.real F) ^ (1 / q) := by - use C1_1 A τ q, C1_1_pos A τ q - intros X _ _ 𝓠 _ _ _ K _ hT F G hF hG - exact theorem1_1C K hA hτ hq hqq' hF hG hT diff --git a/Carleson/Defs.lean b/Carleson/Defs.lean index 6ea187c0..9699ddb3 100644 --- a/Carleson/Defs.lean +++ b/Carleson/Defs.lean @@ -8,8 +8,6 @@ noncomputable section /-! Miscellaneous definitions. We should move them to separate files once we start proving things about them. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable {X : Type*} {A : ℝ} [PseudoMetricSpace X] [IsSpaceOfHomogeneousType X A] section localOscillation @@ -66,21 +64,21 @@ lemma fact_isCompact_ball (x : X) (r : ℝ) : Fact (IsBounded (ball x r)) := ⟨isBounded_ball⟩ attribute [local instance] fact_isCompact_ball -/-- A set `𝓠` of (continuous) functions is compatible. -/ -class IsCompatible [IsSpaceOfHomogeneousType X A] (𝓠 : Set C(X, ℂ)) : Prop where - localOscillation_two_mul_le {x₁ x₂ : X} {r : ℝ} {f g : C(X, ℂ)} (hf : f ∈ 𝓠) (hg : g ∈ 𝓠) +/-- A set `Θ` of (continuous) functions is compatible. -/ +class IsCompatible [IsSpaceOfHomogeneousType X A] (Θ : Set C(X, ℂ)) : Prop where + localOscillation_two_mul_le {x₁ x₂ : X} {r : ℝ} {f g : C(X, ℂ)} (hf : f ∈ Θ) (hg : g ∈ Θ) (h : dist x₁ x₂ < 2 * r) : localOscillation (ball x₂ (2 * r)) f g ≤ A * localOscillation (ball x₁ r) f g - localOscillation_le_of_subset {x₁ x₂ : X} {r : ℝ} {f g : C(X, ℂ)} (hf : f ∈ 𝓠) (hg : g ∈ 𝓠) + localOscillation_le_of_subset {x₁ x₂ : X} {r : ℝ} {f g : C(X, ℂ)} (hf : f ∈ Θ) (hg : g ∈ Θ) (h1 : ball x₁ r ⊆ ball x₂ (A * r)) (h2 : A * r ≤ Metric.diam (univ : Set X)) : 2 * localOscillation (ball x₁ r) f g ≤ localOscillation (ball x₂ (A * r)) f g ballsCoverBalls {x : X} {r R : ℝ} : - ∀ f : withLocalOscillation (ball x r), f ∈ 𝓠 → CoveredByBalls (ball f (2 * R) ∩ 𝓠) ⌊A⌋₊ R + ∀ f : withLocalOscillation (ball x r), f ∈ Θ → CoveredByBalls (ball f (2 * R) ∩ Θ) ⌊A⌋₊ R export IsCompatible (localOscillation_two_mul_le localOscillation_le_of_subset ballsCoverBalls) -- todo -lemma IsCompatible.IsSeparable (hA : 1 ≤ A) {𝓠 : Set C(X, ℂ)} [IsCompatible 𝓠] : IsSeparable 𝓠 := +lemma IsCompatible.IsSeparable (hA : 1 ≤ A) {Θ : Set C(X, ℂ)} [IsCompatible Θ] : IsSeparable Θ := sorry set_option linter.unusedVariables false in @@ -88,16 +86,16 @@ set_option linter.unusedVariables false in def iLipNorm (ϕ : X → ℂ) (x₀ : X) (R : ℝ) : ℝ := (⨆ x ∈ ball x₀ R, ‖ϕ x‖) + R * ⨆ (x : X) (y : X) (h : x ≠ y), ‖ϕ x - ϕ y‖ / nndist x y -/-- 𝓠 is τ-cancellative -/ -class IsCancellative (τ : ℝ) (𝓠 : Set C(X, ℂ)) : Prop where +/-- Θ is τ-cancellative -/ +class IsCancellative (τ : ℝ) (Θ : Set C(X, ℂ)) : Prop where norm_integral_exp_le {x : X} {r : ℝ} {ϕ : X → ℂ} {K : ℝ≥0} (h1 : LipschitzWith K ϕ) - (h2 : tsupport ϕ ⊆ ball x r) {f g : C(X, ℂ)} (hf : f ∈ 𝓠) (hg : g ∈ 𝓠) : + (h2 : tsupport ϕ ⊆ ball x r) {f g : C(X, ℂ)} (hf : f ∈ Θ) (hg : g ∈ Θ) : ‖∫ x in ball x r, exp (I * (f x - g x)) * ϕ x‖ ≤ A * volume.real (ball x r) * iLipNorm ϕ x r * (1 + localOscillation (ball x r) f g) ^ (- τ) export IsCancellative (norm_integral_exp_le) -/-- The "volume function". Note that we will need to assume +/-- The "volume function" `V`. Note that we will need to assume `IsFiniteMeasureOnCompacts` and `ProperSpace` to actually know that this volume is finite. -/ def Real.vol {X : Type*} [PseudoMetricSpace X] [MeasureSpace X] (x y : X) : ℝ := volume.real (ball x (dist x y)) @@ -108,10 +106,10 @@ open Function /-- `K` is a one-sided `τ`-Calderon-Zygmund kernel In the formalization `K x y` is defined everywhere, even for `x = y`. The assumptions on `K` show that `K x x = 0`. -/ -class IsCZKernel (τ : ℝ) (K : X → X → ℂ) : Prop where - norm_le_vol_inv (x y : X) : ‖K x y‖ ≤ (vol x y)⁻¹ +class IsCZKernel (a : ℝ) (K : X → X → ℂ) : Prop where + norm_le_vol_inv (x y : X) : ‖K x y‖ ≤ 2 ^ a ^ 3 / vol x y norm_sub_le {x y y' : X} (h : 2 * A * dist y y' ≤ dist x y) : - ‖K x y - K x y'‖ ≤ (dist y y' / dist x y) ^ τ * (vol x y)⁻¹ + ‖K x y - K x y'‖ ≤ (dist y y' / dist x y) ^ a⁻¹ * (2 ^ a ^ 3 / vol x y) measurable_right (y : X) : Measurable (K · y) -- either we should assume this or prove from the other conditions measurable : Measurable (uncurry K) @@ -151,8 +149,8 @@ def ANCZOperatorLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (K : X → X → ℂ) (f : set_option linter.unusedVariables false in /-- The (maximally truncated) polynomial Carleson operator `T`. -/ -def CarlesonOperator (K : X → X → ℂ) (𝓠 : Set C(X, ℂ)) (f : X → ℂ) (x : X) : ℝ := - ⨆ (Q ∈ 𝓠) (R₁ : ℝ) (R₂ : ℝ) (h1 : R₁ < R₂), +def CarlesonOperator (K : X → X → ℂ) (Θ : Set C(X, ℂ)) (f : X → ℂ) (x : X) : ℝ := + ⨆ (Q ∈ Θ) (R₁ : ℝ) (R₂ : ℝ) (h1 : R₁ < R₂), ‖∫ y in {y | dist x y ∈ Ioo R₁ R₂}, K x y * f y * exp (I * Q y)‖ variable (X) in @@ -202,25 +200,25 @@ instance homogeneousMeasurableSpace [Inhabited X] : MeasurableSpace C(X, ℂ) := @borel C(X, ℂ) t /-- A tile structure. Note: compose `𝓘` with `𝓓` to get the `𝓘` of the paper. -/ -class TileStructure.{u} [Inhabited X] (𝓠 : outParam (Set C(X, ℂ))) +class TileStructure.{u} [Inhabited X] (Θ : outParam (Set C(X, ℂ))) (D κ : outParam ℝ) (C : outParam ℝ) extends GridStructure X κ D C where protected 𝔓 : Type u protected 𝓘 : 𝔓 → ι Ω : 𝔓 → Set C(X, ℂ) measurableSet_Ω : ∀ p, MeasurableSet (Ω p) Q : 𝔓 → C(X, ℂ) - Q_mem : ∀ p, Q p ∈ 𝓠 - union_Ω {i} : ⋃ (p) (_h : 𝓓 (𝓘 p) = 𝓓 i), Ω p = 𝓠 + Q_mem : ∀ p, Q p ∈ Θ + union_Ω {i} : ⋃ (p) (_h : 𝓓 (𝓘 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 - localOscillationBall_subset {p} : localOscillationBall (𝓓 (𝓘 p)) (Q p) 5⁻¹ ∩ 𝓠 ⊆ Ω p + localOscillationBall_subset {p} : localOscillationBall (𝓓 (𝓘 p)) (Q p) 5⁻¹ ∩ Θ ⊆ Ω p subset_localOscillationBall {p} : Ω p ⊆ localOscillationBall (𝓓 (𝓘 p)) (Q p) 1 export TileStructure (Ω measurableSet_Ω Q Q_mem union_Ω disjoint_Ω relative_fundamental_dyadic localOscillationBall_subset subset_localOscillationBall) -- #print homogeneousMeasurableSpace -- #print TileStructure -variable [Inhabited X] {𝓠 : Set C(X, ℂ)} [TileStructure 𝓠 D κ C] +variable [Inhabited X] {Θ : Set C(X, ℂ)} [TileStructure Θ D κ C] variable (X) in def 𝔓 := TileStructure.𝔓 X A diff --git a/Carleson/HomogeneousType.lean b/Carleson/HomogeneousType.lean index 54d3eac7..43896875 100644 --- a/Carleson/HomogeneousType.lean +++ b/Carleson/HomogeneousType.lean @@ -7,8 +7,6 @@ import Mathlib.Analysis.SpecialFunctions.Log.Base open MeasureTheory Measure NNReal ENNReal Metric Filter Topology TopologicalSpace noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - /-! Question(F): should a space of homogeneous type extend `PseudoMetricSpace` or `MetricSpace`? -/ diff --git a/Carleson/Proposition1.lean b/Carleson/Proposition1.lean index dd89192b..afce322a 100644 --- a/Carleson/Proposition1.lean +++ b/Carleson/Proposition1.lean @@ -4,7 +4,6 @@ import Carleson.Proposition3 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 /- The constant used in proposition2_1 -/ def C2_1 (A : ℝ) (τ q : ℝ) (C : ℝ) : ℝ := sorry @@ -26,7 +25,7 @@ lemma Cψ2_1_pos (A : ℝ) (τ : ℝ) (C : ℝ) : Cψ2_1 A τ C > 0 := sorry variable {X : Type*} {A : ℝ} [MetricSpace X] [IsSpaceOfHomogeneousType X A] [Inhabited X] variable {τ q q' D κ : ℝ} {C₀ C : ℝ} -variable {𝓠 : Set C(X, ℂ)} [IsCompatible 𝓠] [IsCancellative τ 𝓠] [TileStructure 𝓠 D κ 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 (K : X → X → ℂ) [IsCZKernel τ K] variable {ψ : ℝ → ℝ} @@ -38,7 +37,7 @@ theorem prop2_1 (hκ : κ ∈ Ioo 0 (κ2_1 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') + (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₀) ψ) diff --git a/Carleson/Proposition2.lean b/Carleson/Proposition2.lean index 10ca7e69..9b09a1ab 100644 --- a/Carleson/Proposition2.lean +++ b/Carleson/Proposition2.lean @@ -3,7 +3,6 @@ import Carleson.Defs 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 def C2_2 (A : ℝ) (τ q : ℝ) (C : ℝ) : ℝ := sorry @@ -28,7 +27,7 @@ lemma Cψ2_2_pos (A : ℝ) (τ : ℝ) (C : ℝ) : Cψ2_2 A τ C > 0 := sorry variable {X : Type*} {A : ℝ} [MetricSpace X] [IsSpaceOfHomogeneousType X A] [Inhabited X] variable {τ q D κ ε : ℝ} {C₀ C t : ℝ} -variable {𝓠 : Set C(X, ℂ)} [IsCompatible 𝓠] [IsCancellative τ 𝓠] [TileStructure 𝓠 D κ 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 (K : X → X → ℂ) [IsCZKernel τ K] variable {ψ : ℝ → ℝ} @@ -41,7 +40,7 @@ theorem prop2_2 (hε : ε ∈ Ioo 0 (ε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') + (Q'_mem : ∀ x, Q' x ∈ Θ) (m_Q' : Measurable Q') (m_σ : Measurable σ) (m_σ' : Measurable σ') (hT : NormBoundedBy (ANCZOperatorLp 2 K) 1) (hψ : LipschitzWith (Cψ2_2 A τ q C₀) ψ) diff --git a/Carleson/Proposition3.lean b/Carleson/Proposition3.lean index 08f7af58..d80fe251 100644 --- a/Carleson/Proposition3.lean +++ b/Carleson/Proposition3.lean @@ -3,7 +3,6 @@ import Carleson.Defs 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 def C2_3 (A : ℝ) (τ q : ℝ) (C : ℝ) : ℝ := sorry @@ -27,7 +26,7 @@ lemma Cψ2_3_pos (A : ℝ) (τ : ℝ) (C : ℝ) : Cψ2_3 A τ C > 0 := sorry variable {X : Type*} {A : ℝ} [MetricSpace X] [IsSpaceOfHomogeneousType X A] [Inhabited X] variable {τ q D κ ε δ : ℝ} {C₀ C t : ℝ} -variable {𝓠 : Set C(X, ℂ)} [IsCompatible 𝓠] [IsCancellative τ 𝓠] [TileStructure 𝓠 D κ 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 (K : X → X → ℂ) [IsCZKernel τ K] variable {ψ : ℝ → ℝ} @@ -42,7 +41,7 @@ theorem prop2_3 (hD : (2 * A) ^ 100 < D) -- or some other appropriate bound (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') + (Q'_mem : ∀ x, Q' x ∈ Θ) (m_Q' : Measurable Q') (m_σ : Measurable σ) (m_σ' : Measurable σ') (hT : NormBoundedBy (ANCZOperatorLp 2 K) 1) (hψ : LipschitzWith (Cψ2_3 A τ q C₀) ψ)