diff --git a/Carleson/Defs.lean b/Carleson/Defs.lean index 51d76db..e9d835f 100644 --- a/Carleson/Defs.lean +++ b/Carleson/Defs.lean @@ -171,14 +171,15 @@ def CZOperator (K : X → X → ℂ) (r : ℝ) (f : X → ℂ) (x : X) : ℂ := ∫ y in {y | dist x y ∈ Ici r}, K x y * f y /-- `R_Q(θ, x)` defined in (1.0.20). -/ -def upperRadius [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (x : X) : ℝ := - sSup { r : ℝ | dist_{x, r} θ (Q x) < 1 } +def upperRadius [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (x : X) : ℝ≥0∞ := + sSup { r : ℝ≥0∞ | dist_{x, r.toReal} θ (Q x) < 1 } /-- The linearized maximally truncated nontangential Calderon Zygmund operator `T_Q^θ` -/ def linearizedNontangentialOperator [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (K : X → X → ℂ) (f : X → ℂ) (x : X) : ℝ≥0∞ := ⨆ (R₁ : ℝ) (x' : X) (_ : dist x x' ≤ R₁), - ‖∫ y in {y | dist x' y ∈ Ioo R₁ (upperRadius Q θ x')}, K x' y * f y‖₊ + ‖∫ y in {y | ENNReal.ofReal (dist x' y) ∈ Ioo (ENNReal.ofReal R₁) (upperRadius Q θ x')}, + K x' y * f y‖₊ /-- The maximally truncated nontangential Calderon Zygmund operator `T_*` -/ def nontangentialOperator (K : X → X → ℂ) (f : X → ℂ) (x : X) : ℝ≥0∞ := @@ -486,6 +487,10 @@ lemma DκZ_le_two_rpow_100 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F nth_rw 1 [← mul_one (a ^ 2), ← mul_assoc] gcongr; exact Nat.one_le_two_pow +lemma four_le_Z [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] : 4 ≤ Z := by + rw [defaultZ, show 4 = 2 ^ 2 by rfl] + exact Nat.pow_le_pow_right zero_lt_two (by linarith [four_le_a X]) + variable (a) in /-- `D` as an element of `ℝ≥0`. -/ def nnD : ℝ≥0 := ⟨D, by simp [D_nonneg]⟩ diff --git a/Carleson/ForestOperator.lean b/Carleson/ForestOperator.lean index 2426907..7fffa50 100644 --- a/Carleson/ForestOperator.lean +++ b/Carleson/ForestOperator.lean @@ -111,7 +111,7 @@ lemma biUnion_𝓙 : ⋃ J ∈ 𝓙 𝔖, J = ⋃ I : Grid X, (I : Set X) := by refine subset_antisymm (iUnion₂_subset_iUnion ..) fun x mx ↦ ?_ simp_rw [mem_iUnion] at mx ⊢; obtain ⟨I, mI⟩ := mx obtain ⟨J, sJ, mJ⟩ := - Grid.exists_containing_subcube _ ⟨le_rfl, (range_subset_iff.mp range_s_subset I).1⟩ mI + Grid.exists_containing_subcube _ ⟨le_rfl, scale_mem_Icc.1⟩ mI have : J ∈ (𝓙₀ 𝔖).toFinset := by rw [mem_toFinset]; left; exact sJ obtain ⟨M, lM, maxM⟩ := (𝓙₀ 𝔖).toFinset.exists_le_maximal this simp_rw [mem_toFinset] at maxM @@ -128,7 +128,7 @@ lemma biUnion_𝓛 : ⋃ J ∈ 𝓛 𝔖, J = ⋃ I : Grid X, (I : Set X) := by refine subset_antisymm (iUnion₂_subset_iUnion ..) fun x mx ↦ ?_ simp_rw [mem_iUnion] at mx ⊢; obtain ⟨I, mI⟩ := mx obtain ⟨J, sJ, mJ⟩ := - Grid.exists_containing_subcube _ ⟨le_rfl, (range_subset_iff.mp range_s_subset I).1⟩ mI + Grid.exists_containing_subcube _ ⟨le_rfl, scale_mem_Icc.1⟩ mI have : J ∈ (𝓛₀ 𝔖).toFinset := by rw [mem_toFinset]; left; exact sJ obtain ⟨M, lM, maxM⟩ := (𝓛₀ 𝔖).toFinset.exists_le_maximal this simp_rw [mem_toFinset] at maxM @@ -152,23 +152,22 @@ lemma first_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) sorry /-- Lemma 7.1.5 -/ -lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L) - (hf : IsBounded (range f)) (h2f : HasCompactSupport f) (h3f : AEStronglyMeasurable f) : +lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L) : ‖∑ i in t.σ u x, ∫ y, Ks i x y * approxOnCube (𝓙 (t u)) f y‖₊ ≤ nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 (t u)) f) x' := by rcases (t.σ u x).eq_empty_or_nonempty with hne | hne; · simp [hne] let s₁ := Finset.min' (t.σ u x) hne have ms₁ : s₁ ∈ t.σ u x := Finset.min'_mem .. simp_rw [σ, Finset.mem_image, Finset.mem_filter, Finset.mem_univ, true_and] at ms₁ - obtain ⟨p, ⟨mp, xp, Qxp, sxp⟩, sp⟩ := ms₁ + obtain ⟨p, ⟨mp, xp, _, _⟩, sp⟩ := ms₁ have Lle : L ≤ 𝓘 p := by rcases 𝓛_subset_𝓛₀ hL with hL | hL - · exact le_of_mem_of_mem (hL.symm ▸ (range_subset_iff.mp range_s_subset (𝓘 p)).1) hx xp + · exact le_of_mem_of_mem (hL.symm ▸ scale_mem_Icc.1) hx xp · exact (le_or_ge_of_mem_of_mem xp hx).resolve_left (hL.2 p mp) let s₂ := Finset.max' (t.σ u x) hne have ms₂ : s₂ ∈ t.σ u x := Finset.max'_mem .. simp_rw [σ, Finset.mem_image, Finset.mem_filter, Finset.mem_univ, true_and] at ms₂ - obtain ⟨p', ⟨mp', xp', Qxp', sxp'⟩, sp'⟩ := ms₂ + obtain ⟨p', ⟨mp', xp', Qxp', _⟩, sp'⟩ := ms₂ have s_ineq : 𝔰 p ≤ 𝔰 p' := by rw [sp, sp']; exact (t.σ u x).min'_le s₂ (Finset.max'_mem ..) have pinc : 𝓘 p ≤ 𝓘 p' := le_of_mem_of_mem s_ineq xp xp' @@ -176,7 +175,7 @@ lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L calc _ ≤ dist_(p') (𝒬 u) (𝒬 p') + dist_(p') (Q x) (𝒬 p') := dist_triangle_right .. _ < 4 + 1 := - add_lt_add_of_lt_of_lt ((t.smul_four_le' hu mp').2 (by convert mem_ball_self zero_lt_one)) + add_lt_add_of_lt_of_lt ((t.smul_four_le hu mp').2 (by convert mem_ball_self zero_lt_one)) (subset_cball Qxp') _ = _ := by norm_num have d5' : dist_{x, D ^ s₂} (𝒬 u) (Q x) < 5 * defaultA a ^ 5 := by @@ -224,9 +223,17 @@ lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L · linarith [four_le_a X] _ < _ := by norm_num have x'p : x' ∈ 𝓘 p := (Grid.le_def.mp Lle).1 hx' - simp_rw [nontangentialMaximalFunction] - -- ... - sorry + refine le_iSup₂_of_le (𝓘 p) x'p <| le_iSup₂_of_le x xp <| + le_iSup₂_of_le (𝔰 p') ⟨s_ineq, scale_mem_Icc.2⟩ <| le_iSup_of_le ?_ ?_ + · have : ((D : ℝ≥0∞) ^ (𝔰 p' - 1)).toReal = D ^ (s₂ - 1) := by + rw [sp', ← ENNReal.toReal_zpow]; simp + apply le_sSup; rwa [mem_setOf, dist_congr rfl this] + · convert le_rfl; change (Icc (𝔰 p) _).toFinset = _; rw [sp, sp'] + apply subset_antisymm + · rw [← Finset.toFinset_coe (t.σ u x), toFinset_subset_toFinset] + exact (convex_scales hu).out (Finset.min'_mem ..) (Finset.max'_mem ..) + · intro z mz; rw [toFinset_Icc, Finset.mem_Icc] + exact ⟨Finset.min'_le _ _ mz, Finset.le_max' _ _ mz⟩ /-- The constant used in `third_tree_pointwise`. Has value `2 ^ (151 * a ^ 3)` in the blueprint. -/ @@ -413,11 +420,11 @@ lemma density_tree_bound2 -- some assumptions on f are superfluous /-! ## Section 7.4 except Lemmas 4-6 -/ -/-- The definition of `Tₚ*g(x), defined above Lemma 7.4.1 -/ +/-- The definition of `Tₚ*g(x)`, defined above Lemma 7.4.1 -/ def adjointCarleson (p : 𝔓 X) (f : X → ℂ) (x : X) : ℂ := ∫ y in E p, conj (Ks (𝔰 p) y x) * exp (.I * (Q y y - Q y x)) * f y -/-- The definition of `T_ℭ*g(x), defined at the bottom of Section 7.4 -/ +/-- The definition of `T_ℭ*g(x)`, defined at the bottom of Section 7.4 -/ def adjointCarlesonSum (ℭ : Set (𝔓 X)) (f : X → ℂ) (x : X) : ℂ := ∑ p ∈ {p | p ∈ ℭ}, adjointCarleson p f x @@ -441,9 +448,9 @@ lemma _root_.MeasureTheory.AEStronglyMeasurable.adjointCarleson (hf : AEStrongly refine aestronglyMeasurable_Ks.prod_swap · refine Complex.continuous_exp.comp_aestronglyMeasurable ?_ refine .const_mul (.sub ?_ ?_) _ - . refine Measurable.aestronglyMeasurable ?_ + · refine Measurable.aestronglyMeasurable ?_ fun_prop - . refine continuous_ofReal.comp_aestronglyMeasurable ?_ + · refine continuous_ofReal.comp_aestronglyMeasurable ?_ exact aestronglyMeasurable_Q₂ (X := X) |>.prod_swap · exact hf.snd @@ -529,16 +536,60 @@ lemma adjoint_tree_control (hu : u ∈ t) (hf : IsBounded (range f)) (h2f : HasC simp_rw [C7_4_3, ENNReal.coe_add, ENNReal.one_rpow, mul_one, ENNReal.coe_one] with_reducible rfl -/-- Part 2 of Lemma 7.4.7. -/ -lemma 𝔗_subset_𝔖₀ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) - (h2u : 𝓘 u₁ ≤ 𝓘 u₂) : t u₁ ⊆ 𝔖₀ t u₁ u₂ := by - sorry - /-- Part 1 of Lemma 7.4.7. -/ lemma overlap_implies_distance (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₁ ∪ t u₂) - (hpu₁ : ¬ Disjoint (𝓘 p : Set X) (𝓘 u₁)) : p ∈ 𝔖₀ t u₁ u₂ := by - sorry + (hpu₁ : ¬Disjoint (𝓘 p : Set X) (𝓘 u₁)) : p ∈ 𝔖₀ t u₁ u₂ := by + simp_rw [𝔖₀, mem_setOf, hp, true_and] + wlog plu₁ : 𝓘 p ≤ 𝓘 u₁ generalizing p + · have u₁lp : 𝓘 u₁ ≤ 𝓘 p := (le_or_ge_or_disjoint.resolve_left plu₁).resolve_right hpu₁ + obtain ⟨p', mp'⟩ := t.nonempty hu₁ + have p'lu₁ : 𝓘 p' ≤ 𝓘 u₁ := (t.smul_four_le hu₁ mp').1 + obtain ⟨c, mc⟩ := (𝓘 p').nonempty + specialize this (mem_union_left _ mp') (not_disjoint_iff.mpr ⟨c, mc, p'lu₁.1 mc⟩) p'lu₁ + exact this.trans (Grid.dist_mono (p'lu₁.trans u₁lp)) + have four_Z := four_le_Z (X := X) + have four_le_Zn : 4 ≤ Z * (n + 1) := by rw [← mul_one 4]; exact mul_le_mul' four_Z (by omega) + have four_le_two_pow_Zn : 4 ≤ 2 ^ (Z * (n + 1) - 1) := by + change 2 ^ 2 ≤ _; exact Nat.pow_le_pow_right zero_lt_two (by omega) + have ha : (2 : ℝ) ^ (Z * (n + 1)) - 4 ≥ 2 ^ (Z * n / 2 : ℝ) := + calc + _ ≥ (2 : ℝ) ^ (Z * (n + 1)) - 2 ^ (Z * (n + 1) - 1) := by gcongr; norm_cast + _ = 2 ^ (Z * (n + 1) - 1) := by + rw [sub_eq_iff_eq_add, ← two_mul, ← pow_succ', Nat.sub_add_cancel (by omega)] + _ ≥ 2 ^ (Z * n) := by apply pow_le_pow_right one_le_two; rw [mul_add_one]; omega + _ ≥ _ := by + rw [← Real.rpow_natCast] + apply Real.rpow_le_rpow_of_exponent_le one_le_two; rw [Nat.cast_mul] + exact half_le_self (by positivity) + rcases hp with (c : p ∈ t.𝔗 u₁) | (c : p ∈ t.𝔗 u₂) + · calc + _ ≥ dist_(p) (𝒬 p) (𝒬 u₂) - dist_(p) (𝒬 p) (𝒬 u₁) := by + change _ ≤ _; rw [sub_le_iff_le_add, add_comm]; exact dist_triangle .. + _ ≥ 2 ^ (Z * (n + 1)) - 4 := by + gcongr + · exact (t.lt_dist' hu₂ hu₁ hu.symm c (plu₁.trans h2u)).le + · have : 𝒬 u₁ ∈ ball_(p) (𝒬 p) 4 := + (t.smul_four_le hu₁ c).2 (by convert mem_ball_self zero_lt_one) + rw [@mem_ball'] at this; exact this.le + _ ≥ _ := ha + · calc + _ ≥ dist_(p) (𝒬 p) (𝒬 u₁) - dist_(p) (𝒬 p) (𝒬 u₂) := by + change _ ≤ _; rw [sub_le_iff_le_add, add_comm]; exact dist_triangle_right .. + _ ≥ 2 ^ (Z * (n + 1)) - 4 := by + gcongr + · exact (t.lt_dist' hu₁ hu₂ hu c plu₁).le + · have : 𝒬 u₂ ∈ ball_(p) (𝒬 p) 4 := + (t.smul_four_le hu₂ c).2 (by convert mem_ball_self zero_lt_one) + rw [@mem_ball'] at this; exact this.le + _ ≥ _ := ha + +/-- Part 2 of Lemma 7.4.7. -/ +lemma 𝔗_subset_𝔖₀ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂) : + t u₁ ⊆ 𝔖₀ t u₁ u₂ := fun p mp ↦ by + apply overlap_implies_distance hu₁ hu₂ hu h2u (mem_union_left _ mp) + obtain ⟨c, mc⟩ := (𝓘 p).nonempty + exact not_disjoint_iff.mpr ⟨c, mc, (t.smul_four_le hu₁ mp).1.1 mc⟩ /-! ## Section 7.5 -/ diff --git a/Carleson/GridStructure.lean b/Carleson/GridStructure.lean index 0f8b4b5..8e5d59f 100644 --- a/Carleson/GridStructure.lean +++ b/Carleson/GridStructure.lean @@ -91,6 +91,8 @@ lemma eq_or_disjoint (hs : s i = s j) : i = j ∨ Disjoint (i : Set X) (j : Set Or.elim (le_or_disjoint hs.le) (fun ij ↦ Or.elim (le_or_disjoint hs.ge) (fun ji ↦ Or.inl (le_antisymm ij ji)) (fun h ↦ Or.inr h.symm)) (fun h ↦ Or.inr h) +lemma scale_mem_Icc : s i ∈ Icc (-S : ℤ) S := mem_Icc.mp (range_s_subset ⟨i, rfl⟩) + lemma volume_coeGrid_lt_top : volume (i : Set X) < ⊤ := measure_lt_top_of_subset Grid_subset_ball (measure_ball_ne_top _ _) @@ -104,7 +106,7 @@ namespace Grid protected lemma inj : Injective (fun i : Grid X ↦ ((i : Set X), s i)) := GridStructure.inj lemma le_topCube : i ≤ topCube := - ⟨subset_topCube, (range_s_subset ⟨i, rfl⟩).2.trans_eq s_topCube.symm⟩ + ⟨subset_topCube, scale_mem_Icc.2.trans_eq s_topCube.symm⟩ lemma isTop_topCube : IsTop (topCube : Grid X) := fun _ ↦ le_topCube @@ -216,7 +218,7 @@ lemma exists_supercube (l : ℤ) (h : l ∈ Icc (s i) S) : ∃ j, s j = l ∧ i obtain ⟨lb, ub⟩ := h rcases ub.eq_or_lt with ub | ub; · exact ⟨topCube, by simpa [ub] using s_topCube, le_topCube⟩ obtain ⟨x, hx⟩ := i.nonempty - have bound_i : -S ≤ s i ∧ s i ≤ S := mem_Icc.mp (range_s_subset ⟨i, rfl⟩) + have bound_i : -S ≤ s i ∧ s i ≤ S := scale_mem_Icc have ts := Grid_subset_biUnion (X := X) (i := topCube) l (by rw [s_topCube, mem_Ico]; omega) have := mem_of_mem_of_subset hx ((le_topCube (i := i)).1.trans ts) simp_rw [mem_preimage, mem_singleton_iff, mem_iUnion, exists_prop] at this @@ -225,7 +227,7 @@ lemma exists_supercube (l : ℤ) (h : l ∈ Icc (s i) S) : ∃ j, s j = l ∧ i lemma exists_sandwiched (h : i ≤ j) (l : ℤ) (hl : l ∈ Icc (s i) (s j)) : ∃ k, s k = l ∧ i ≤ k ∧ k ≤ j := by - have bound_q : -S ≤ s j ∧ s j ≤ S := mem_Icc.mp (range_s_subset ⟨j, rfl⟩) + have bound_q : -S ≤ s j ∧ s j ≤ S := scale_mem_Icc rw [mem_Icc] at hl obtain ⟨K, sK, lbK⟩ := exists_supercube l (by change s i ≤ _ ∧ _; omega) use K, sK, lbK @@ -242,7 +244,7 @@ lemma scale_succ (h : ¬IsMax i) : s i.succ = s i + 1 := by lemma opSize_succ_lt (h : ¬IsMax i) : i.succ.opSize < i.opSize := by simp only [opSize, Int.lt_toNat] - have : s i.succ ≤ S := (mem_Icc.mp (range_s_subset ⟨i.succ, rfl⟩)).2 + have : s i.succ ≤ S := (mem_Icc.mp scale_mem_Icc).2 replace : 0 ≤ S - s i.succ := by omega rw [Int.toNat_of_nonneg this, scale_succ h] omega diff --git a/Carleson/TileExistence.lean b/Carleson/TileExistence.lean index e1fae1a..38cb99f 100644 --- a/Carleson/TileExistence.lean +++ b/Carleson/TileExistence.lean @@ -2138,7 +2138,7 @@ lemma Ω_RFD {p q : 𝔓 X} (h𝓘 : 𝓘 p ≤ 𝓘 q) : Disjoint (Ω p) (Ω q) have nmaxJ : ¬IsMax J := by by_contra maxJ; rw [Grid.isMax_iff] at maxJ rw [maxJ, show s topCube = S from s_topCube (X := X)] at sJ - have : 𝔰 q ≤ S := (range_s_subset ⟨q.1, rfl⟩).2 + have : 𝔰 q ≤ S := scale_mem_Icc.2 omega have succJ : J.succ = q.1 := (Grid.succ_def nmaxJ).mpr ⟨ubJ, by change 𝔰 q = _; omega⟩ have key : Ω q ⊆ Ω ⟨J, a⟩ := by diff --git a/Carleson/ToMathlib/Misc.lean b/Carleson/ToMathlib/Misc.lean index 703d86b..46b4729 100644 --- a/Carleson/ToMathlib/Misc.lean +++ b/Carleson/ToMathlib/Misc.lean @@ -137,6 +137,9 @@ lemma tsum_geometric_ite_eq_tsum_geometric {k c : ℕ} : · rw [mem_support, ne_eq, ite_eq_right_iff, Classical.not_imp] at mn use n - k, Nat.sub_add_cancel mn.1 +lemma ENNReal.toReal_zpow (x : ℝ≥0∞) (z : ℤ) : x.toReal ^ z = (x ^ z).toReal := by + rw [← rpow_intCast, ← toReal_rpow, Real.rpow_intCast] + end ENNReal section Indicator diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index 1150d7e..d5c23e6 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -4394,6 +4394,7 @@ \section{The pointwise tree estimate} \end{lemma} \begin{proof} + \leanok Let $s_1 = \underline{\sigma}(\fu, x)$. By definition, there exists a tile $\fp \in \fT(\fu)$ with $\ps(\fp) = s_1$ and $x \in E(\fp)$. Then $x \in \scI(\fp) \cap L$. By \eqref{dyadicproperty} and the definition of $\mathcal{L}(\fT(\fu))$, it follows that $L \subset \scI(\fp)$, in particular $x' \in \scI(\fp)$, so $x \in I_{s_1}(x')$. Next, let $s_2 = \overline{\sigma}(\fu, x)$ and let $\fp' \in \fT(\fu)$ with $\ps(\fp') = s_2$ and $x \in E(\fp')$. Since $\fp' \in \fT(\fu)$, we have $4\fp' \lesssim \fu$. Since $\tQ(x) \in \fc(\fp')$, it follows that $$ @@ -5106,11 +5107,12 @@ \section{Almost orthogonality of separated trees} \end{lemma} \begin{proof} + \leanok Suppose first that $\fp \in \fT(\fu_1)$. Then $\scI(\fp) \subset \scI(\fu_1) \subset \scI(\fu_2)$, by \eqref{forest1}. Thus we have by the separation condition \eqref{forest5}, \eqref{eq-freq-comp-ball}, \eqref{forest1} and the triangle inequality \begin{align*} d_{\fp}(\fcc(\fu_1), \fcc(\fu_2)) &\ge d_{\fp}(\fcc(\fp), \fcc(\fu_2)) - d_{\fp}(\fcc(\fp), \fcc(\fu_1))\\ &\ge 2^{Z(n+1)} - 4\\ - &\ge 2^{Zn}\,, + &\ge 2^{Zn/2}\,, \end{align*} using that $Z= 2^{12a}\ge 4$. Hence $\fp \in \mathfrak{S}$.