From 3298f748e9eb26a242da5ee38cb50dc55e604935 Mon Sep 17 00:00:00 2001 From: James Sundstrom Date: Wed, 8 Jan 2025 11:52:30 -0500 Subject: [PATCH] Lemma 7.1.4 (#201) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit I added two theorems in the ToMathlib file. We might also consider generalizing `sum_pow_two_le` (in PointwiseEstimate.lean) and adding it to Mathlib; Mathlib has some results about geometric sums indexed by naturals, but none that I could find about geometric sums indexed by integers. There were a few (as far as I could tell) mistakes in the blueprint, which I fixed: - There were a couple uninteresting typos. - There was some confusion about the constant `C7_1_4 a`: in the statement of the theorem, it's 10 * 2 ^ (105a^3), but at the end of the proof, it's 2 ^ (105a^3). I changed it to 10 * 2 ^ (104a^3). - I don't think that the step originally described in the blueprint as "[u]sing the doubling property (1.0.8), the definition of d_p and Lemma 2.1.2" works as written. The doubling property requires x_1 to be in B_2, which I don't think can be proven in this situation. I used the monotonicity property (1.0.9) to make the balls big enough that this condition holds; this requires more applications of (1.0.8) to compensate, but the extra factors from (1.0.8) eventually get absorbed into the constant, with the same result as originally in the blueprint. - The proof claims that (7.1.1) says that π’₯ is a partition of X, but (7.1.1) actually says that π’₯ is a partition of the union of the dyadic cubes; I don't see any assumption that the dyadic cubes cover all of X. I changed the reference accordingly. (I noticed that the same claim about π’₯ being a partition of X is made in the proof of Lemma 7.2.3, but I didn't edit that part.) - Toward the end, the blueprint says "we have s(L) <= s(p) for all p," but I think that conclusion is only valid assuming L and p are not disjoint. That doesn't cause any problems for the proof, because we have nondisjointness in the relevant case; I edited the blueprint to avoid the stronger claim. --------- Co-authored-by: Floris van Doorn --- Carleson/Classical/CarlesonOnTheRealLine.lean | 34 +- Carleson/Defs.lean | 24 +- Carleson/DoublingMeasure.lean | 8 + Carleson/Forest.lean | 13 +- .../ForestOperator/PointwiseEstimate.lean | 384 +++++++++++++++++- Carleson/GridStructure.lean | 6 + Carleson/Psi.lean | 16 +- Carleson/ToMathlib/Misc.lean | 47 +++ blueprint/src/chapter/main.tex | 21 +- 9 files changed, 492 insertions(+), 61 deletions(-) diff --git a/Carleson/Classical/CarlesonOnTheRealLine.lean b/Carleson/Classical/CarlesonOnTheRealLine.lean index 050393f0..b6604c8c 100644 --- a/Carleson/Classical/CarlesonOnTheRealLine.lean +++ b/Carleson/Classical/CarlesonOnTheRealLine.lean @@ -164,29 +164,24 @@ lemma coeΘ_R (n : Θ ℝ) (x : ℝ) : n x = n * x := rfl lemma coeΘ_R_C (n : Θ ℝ) (x : ℝ) : (n x : β„‚) = n * x := by norm_cast lemma oscillation_control {x : ℝ} {r : ℝ} {f g : Θ ℝ} : - localOscillation (ball x r) (coeΘ f) (coeΘ g) ≀ dist_{x, r} f g := by + localOscillation (ball x r) (coeΘ f) (coeΘ g) ≀ ENNReal.ofReal (dist_{x, r} f g) := by by_cases r_pos : r ≀ 0 Β· rw [ball_eq_empty.mpr r_pos] - unfold localOscillation - simp [dist_nonneg] + simp [localOscillation, norm_nonneg] push_neg at r_pos - rw [dist_integer_linear_eq] - calc ⨆ z ∈ ball x r Γ—Λ’ ball x r, |↑f * z.1 - ↑g * z.1 - ↑f * z.2 + ↑g * z.2| - _ = ⨆ z ∈ ball x r Γ—Λ’ ball x r, β€–(f - g) * (z.1 - x) - (f - g) * (z.2 - x)β€– := by + simp_rw [dist_integer_linear_eq] + calc ⨆ z ∈ ball x r Γ—Λ’ ball x r, ENNReal.ofReal ‖↑f * z.1 - ↑g * z.1 - ↑f * z.2 + ↑g * z.2β€– + _ = ⨆ z ∈ ball x r Γ—Λ’ ball x r, ENNReal.ofReal |(f - g) * (z.1 - x) - (f - g) * (z.2 - x)| := by congr with z congr with h rw [Real.norm_eq_abs] ring_nf - _ ≀ 2 * r * |↑f - ↑g| := by - apply Real.iSup_le - --TODO: investigate strange (delaborator) behavior - why is there still a sup? - on_goal 1 => intro z - on_goal 1 => apply Real.iSup_le - Β· intro hz - simp only [Set.mem_prod, mem_ball] at hz - rw [Real.dist_eq, Real.dist_eq] at hz - rw [Real.norm_eq_abs] - calc |(f - g) * (z.1 - x) - (f - g) * (z.2 - x)| + _ ≀ ENNReal.ofReal (2 * r * |↑f - ↑g|) := by + refine iSupβ‚‚_le (fun z hz ↦ ?_) + apply ENNReal.ofReal_le_of_le_toReal + rw [ENNReal.toReal_ofReal (by positivity)] + simp_rw [Set.mem_prod, mem_ball, Real.dist_eq] at hz + calc |(f - g) * (z.1 - x) - (f - g) * (z.2 - x)| _ ≀ |(f - g) * (z.1 - x)| + |(f - g) * (z.2 - x)| := abs_sub .. _ = |↑f - ↑g| * |z.1 - x| + |↑f - ↑g| * |z.2 - x| := by congr <;> apply abs_mul _ ≀ |↑f - ↑g| * r + |↑f - ↑g| * r := by @@ -194,12 +189,7 @@ lemma oscillation_control {x : ℝ} {r : ℝ} {f g : Θ ℝ} : Β· linarith [hz.1] Β· linarith [hz.2] _ = 2 * r * |↑f - ↑g| := by ring - all_goals - repeat - apply mul_nonneg - linarith - apply abs_nonneg - _ ≀ 2 * max r 0 * |↑f - ↑g| := by + _ ≀ ENNReal.ofReal (2 * max r 0 * |↑f - ↑g|) := by gcongr apply le_max_left diff --git a/Carleson/Defs.lean b/Carleson/Defs.lean index f45f9701..f624a72c 100644 --- a/Carleson/Defs.lean +++ b/Carleson/Defs.lean @@ -22,8 +22,8 @@ variable {π•œ X : Type*} {A : β„•} [_root_.RCLike π•œ] [PseudoMetricSpace X] section localOscillation /-- The local oscillation of two functions w.r.t. a set `E`. This is `d_E` in the blueprint. -/ -def localOscillation (E : Set X) (f g : C(X, π•œ)) : ℝ := - ⨆ z ∈ E Γ—Λ’ E, β€–f z.1 - g z.1 - f z.2 + g z.2β€– +def localOscillation (E : Set X) (f g : C(X, π•œ)) : ℝβ‰₯0∞ := + ⨆ z ∈ E Γ—Λ’ E, ENNReal.ofReal β€–f z.1 - g z.1 - f z.2 + g z.2β€– -- example (E : Set X) (hE : IsBounded E) (f : C(X, ℝ)) : -- BddAbove (range fun z : E ↦ f z) := by @@ -39,7 +39,7 @@ variable {E : Set X} {f g : C(X, π•œ)} /-- A ball w.r.t. the distance `localOscillation` -/ def localOscillationBall (E : Set X) (f : C(X, π•œ)) (r : ℝ) : Set C(X, π•œ) := - { g : C(X, π•œ) | localOscillation E f g < r } + { g : C(X, π•œ) | localOscillation E f g < ENNReal.ofReal r } end localOscillation @@ -95,7 +95,7 @@ class CompatibleFunctions (π•œ : outParam Type*) (X : Type u) (A : outParam β„• eq_zero : βˆƒ o : X, βˆ€ f : Θ, f o = 0 /-- The distance is bounded below by the local oscillation. (1.0.7) -/ localOscillation_le_cdist {x : X} {r : ℝ} {f g : Θ} : - localOscillation (ball x r) (coeΘ f) (coeΘ g) ≀ dist_{x, r} f g + localOscillation (ball x r) (coeΘ f) (coeΘ g) ≀ ENNReal.ofReal (dist_{x, r} f g) /-- The distance is monotone in the ball. (1.0.9) -/ 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 @@ -117,6 +117,22 @@ instance nonempty_Space [CompatibleFunctions π•œ X A] : Nonempty X := by instance inhabited_Space [CompatibleFunctions π•œ X A] : Inhabited X := ⟨nonempty_Space.some⟩ +lemma le_localOscillation [CompatibleFunctions π•œ X A] (x : X) (r : ℝ) (f g : Θ X) {y z : X} + (hy : y ∈ ball x r) (hz : z ∈ ball x r) : β€–coeΘ f y - coeΘ g y - coeΘ f z + coeΘ g zβ€– ≀ + ENNReal.toReal (localOscillation (ball x r) (coeΘ f) (coeΘ g)) := by + rw [(ENNReal.toReal_ofReal (norm_nonneg _)).symm] + let f (z) := ⨆ (_ : z ∈ ball x r Γ—Λ’ ball x r), ENNReal.ofReal β€–f z.1 - g z.1 - f z.2 + g z.2β€– + apply ENNReal.toReal_mono + Β· exact lt_of_le_of_lt CompatibleFunctions.localOscillation_le_cdist ENNReal.ofReal_lt_top |>.ne + Β· exact le_of_eq_of_le (Eq.symm (iSup_pos ⟨hy, hz⟩)) (le_iSup f ⟨y, z⟩) + +lemma oscillation_le_cdist [CompatibleFunctions π•œ X A] (x : X) (r : ℝ) (f g : Θ X) {y z : X} + (hy : y ∈ ball x r) (hz : z ∈ ball x r) : + β€–coeΘ f y - coeΘ g y - coeΘ f z + coeΘ g zβ€– ≀ dist_{x, r} f g := by + apply le_trans <| le_localOscillation x r f g hy hz + rw [← ENNReal.toReal_ofReal dist_nonneg] + exact ENNReal.toReal_mono ENNReal.ofReal_ne_top CompatibleFunctions.localOscillation_le_cdist + export CompatibleFunctions (localOscillation_le_cdist cdist_mono cdist_le le_cdist) lemma dist_congr [FunctionDistances π•œ X] {x₁ xβ‚‚ : X} {r₁ rβ‚‚ : ℝ} {f g : Θ X} diff --git a/Carleson/DoublingMeasure.lean b/Carleson/DoublingMeasure.lean index b24c4d2d..ac0f3a37 100644 --- a/Carleson/DoublingMeasure.lean +++ b/Carleson/DoublingMeasure.lean @@ -47,6 +47,14 @@ lemma measure_real_ball_two_le_same (x : X) (r : ℝ) : Β· exact ENNReal.mul_ne_top coe_ne_top measure_ball_lt_top.ne Β· exact measure_ball_two_le_same x r +lemma measure_real_ball_two_le_same_iterate (x : X) (r : ℝ) (n : β„•) : + ΞΌ.real (ball x ((2 ^ n) * r)) ≀ A ^ n * ΞΌ.real (ball x r) := by + induction n with + | zero => simp + | succ m ih => + simp_rw [add_comm m 1, pow_add, pow_one, mul_assoc] + exact le_trans (measure_real_ball_two_le_same x _) (by gcongr) + lemma measure_real_ball_pos [ΞΌ.IsOpenPosMeasure] (x : X) {r : ℝ} (hr : 0 < r) : 0 < ΞΌ.real (ball x r) := toReal_pos ((measure_ball_pos ΞΌ x hr).ne.symm) (measure_ball_lt_top.ne) diff --git a/Carleson/Forest.lean b/Carleson/Forest.lean index 673df3cc..d3ccb39d 100644 --- a/Carleson/Forest.lean +++ b/Carleson/Forest.lean @@ -65,15 +65,18 @@ lemma lt_dist (hu : u ∈ t) (hu' : u' ∈ t) (huu' : u β‰  u') {p} (hp : p ∈ lemma ball_subset (hu : u ∈ t) (hp : p ∈ t u) : ball (𝔠 p) (8 * D ^ 𝔰 p) βŠ† π“˜ u := t.ball_subset' hu hp +-- Used in the proof of Lemma 7.1.4 +variable {t} in +lemma ball_subset_of_mem_π“˜ (hu : u ∈ t) {p : 𝔓 X} (hp : p ∈ t u) {x : X} (hx : x ∈ π“˜ p) : + ball x (4 * D ^ (𝔰 p)) βŠ† π“˜ u := by + refine (ball_subset_ball' ?_).trans (t.ball_subset hu hp) + linarith [show dist x (𝔠 p) < 4 * D ^ (𝔰 p) from Grid_subset_ball hx] + lemma if_descendant_then_subset (hu : u ∈ t) (hp : p ∈ t u) : (π“˜ p : Set X) βŠ† π“˜ u := by calc ↑(π“˜ p) _ βŠ† ball (𝔠 p) (4 * ↑D ^ 𝔰 p) := by exact GridStructure.Grid_subset_ball (i := π“˜ p) - _ βŠ† ball (𝔠 p) (8 * ↑D ^ 𝔰 p) := by - gcongr - norm_num - _ βŠ† ↑(π“˜ u) := by - exact ball_subset t hu hp + _ βŠ† ↑(π“˜ u) := ball_subset_of_mem_π“˜ hu hp Grid.c_mem_Grid end Forest diff --git a/Carleson/ForestOperator/PointwiseEstimate.lean b/Carleson/ForestOperator/PointwiseEstimate.lean index 49a3354b..120c35a2 100644 --- a/Carleson/ForestOperator/PointwiseEstimate.lean +++ b/Carleson/ForestOperator/PointwiseEstimate.lean @@ -1,6 +1,7 @@ import Carleson.Forest import Carleson.HardyLittlewood import Carleson.ToMathlib.BoundedCompactSupport +import Carleson.ToMathlib.Misc import Carleson.Psi open ShortVariables TileStructure @@ -24,10 +25,26 @@ variable (t) in We may assume `u ∈ t` whenever proving things about this definition. -/ def Οƒ (u : 𝔓 X) (x : X) : Finset β„€ := .image 𝔰 { p | p ∈ t u ∧ x ∈ E p } -/- Maybe we should try to avoid using \overline{Οƒ} and \underline{Οƒ} in Lean: -I don't think the set is always non-empty(?) -/ --- def ΟƒMax (u : 𝔓 X) (x : X) : β„€ := --- Finset.image 𝔰 { p | p ∈ t u ∧ x ∈ E p } |>.max' sorry +variable (t) in +private lemma exists_p_of_mem_Οƒ (u : 𝔓 X) (x : X) {s : β„€} (hs : s ∈ t.Οƒ u x) : + βˆƒ p ∈ t.𝔗 u, x ∈ E p ∧ 𝔰 p = s := by + have ⟨p, hp⟩ := Finset.mem_image.mp hs + simp only [mem_𝔗, Finset.mem_filter] at hp + use p, hp.1.2.1, hp.1.2.2, hp.2 + +/- \overline{Οƒ} from the blueprint. -/ +variable (t) in +def ΟƒMax (u : 𝔓 X) (x : X) (hΟƒ : (t.Οƒ u x).Nonempty) : β„€ := + t.Οƒ u x |>.max' hΟƒ + +/- \underline{Οƒ} from the blueprint. -/ +variable (t) in +def ΟƒMin (u : 𝔓 X) (x : X) (hΟƒ : (t.Οƒ u x).Nonempty) : β„€ := + t.Οƒ u x |>.min' hΟƒ + +variable (t) in +private lemma ΟƒMax_mem_Οƒ (u : 𝔓 X) (x : X) (hΟƒ : (t.Οƒ u x).Nonempty) : ΟƒMax t u x hΟƒ ∈ t.Οƒ u x := + (t.Οƒ u x).max'_mem hΟƒ /-- The definition of `𝓙₀(𝔖), defined above Lemma 7.1.2 -/ def 𝓙₀ (𝔖 : Set (𝔓 X)) : Set (Grid X) := @@ -49,6 +66,18 @@ def 𝓛 (𝔖 : Set (𝔓 X)) : Set (Grid X) := lemma 𝓛_subset_𝓛₀ {𝔖 : Set (𝔓 X)} : 𝓛 𝔖 βŠ† 𝓛₀ 𝔖 := sep_subset .. +private lemma s_le_s_of_mem_𝓛 {𝔖 : Set (𝔓 X)} {L : Grid X} (hL : L ∈ 𝓛 𝔖) + {p : 𝔓 X} (hp : p ∈ 𝔖) (hpL : Β¬ Disjoint (π“˜ p : Set X) (L : Set X)) : s L ≀ s (π“˜ p) := by + simp only [𝓛, Maximal, 𝓛₀, Grid.le_def, not_and, not_le, mem_setOf_eq, and_imp] at hL + rcases hL.1 with h | h + Β· exact h β–Έ (range_s_subset βŸ¨π“˜ p, rfl⟩).1 + Β· by_contra! + exact lt_asymm this <| h.2 p hp <| (GridStructure.fundamental_dyadic' this.le).resolve_right hpL + +private lemma subset_of_mem_𝓛 {𝔖 : Set (𝔓 X)} {L : Grid X} (hL : L ∈ 𝓛 𝔖) {p : 𝔓 X} + (hp : p ∈ 𝔖) (hpL : Β¬ Disjoint (π“˜ p : Set X) (L : Set X)) : (L : Set X) βŠ† (π“˜ p : Set X) := + GridStructure.fundamental_dyadic' (s_le_s_of_mem_𝓛 hL hp hpL) |>.resolve_right fun h ↦ hpL h.symm + /-- The projection operator `P_𝓒 f(x)`, given above Lemma 7.1.3. In lemmas the `c` will be pairwise disjoint on `C`. -/ def approxOnCube (C : Set (Grid X)) (f : X β†’ E') (x : X) : E' := @@ -58,6 +87,37 @@ lemma stronglyMeasurable_approxOnCube (C : Set (Grid X)) (f : X β†’ E') : StronglyMeasurable (approxOnCube (X := X) (K := K) C f) := Finset.stronglyMeasurable_sum _ (fun _ _ ↦ stronglyMeasurable_const.indicator coeGrid_measurable) +lemma integrable_approxOnCube (C : Set (Grid X)) {f : X β†’ E'} : Integrable (approxOnCube C f) := by + refine integrable_finset_sum _ (fun i hi ↦ ?_) + constructor + Β· exact (aestronglyMeasurable_indicator_iff coeGrid_measurable).mpr aestronglyMeasurable_const + Β· simp_rw [hasFiniteIntegral_iff_nnnorm, nnnorm_indicator_eq_indicator_nnnorm, + ENNReal.coe_indicator] + apply lt_of_le_of_lt <| lintegral_indicator_const_le (i : Set X) _ + exact ENNReal.mul_lt_top ENNReal.coe_lt_top volume_coeGrid_lt_top + +lemma approxOnCube_nonneg (C : Set (Grid X)) {f : X β†’ ℝ} (hf : βˆ€ (y : X), f y β‰₯ 0) (x : X) : + approxOnCube C f x β‰₯ 0 := + Finset.sum_nonneg' (fun _ ↦ Set.indicator_nonneg (fun _ _ ↦ integral_nonneg hf) _) + +lemma approxOnCube_apply {C : Set (Grid X)} (hC : C.PairwiseDisjoint (fun I ↦ (I : Set X))) + (f : X β†’ E') {x : X} {J : Grid X} (hJ : J ∈ C) (xJ : x ∈ J) : + (approxOnCube C f) x = ⨍ y in J, f y := by + rw [approxOnCube, ← Finset.sum_filter_not_add_sum_filter _ (J = Β·)] + have eq0 : βˆ‘ i ∈ Finset.filter (Β¬ J = Β·) (Finset.univ.filter (Β· ∈ C)), + (i : Set X).indicator (fun _ ↦ ⨍ y in i, f y) x = 0 := by + suffices βˆ€ i ∈ (Finset.univ.filter (Β· ∈ C)).filter (Β¬ J = Β·), + (i : Set X).indicator (fun _ ↦ ⨍ y in i, f y) x = 0 by simp [Finset.sum_congr rfl this] + intro i hi + simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi + simp [Set.disjoint_left.mp ((hC.eq_or_disjoint hJ hi.1).resolve_left hi.2) xJ] + have eq_ave : βˆ‘ i ∈ (Finset.univ.filter (Β· ∈ C)).filter (J = Β·), + (i : Set X).indicator (fun _ ↦ ⨍ y in i, f y) x = ⨍ y in J, f y := by + suffices (Finset.univ.filter (Β· ∈ C)).filter (J = Β·) = {J} by simp [this, xJ, ← Grid.mem_def] + exact subset_antisymm (fun _ h ↦ Finset.mem_singleton.mpr (Finset.mem_filter.mp h).2.symm) + (fun _ h ↦ by simp [Finset.mem_singleton.mp h, hJ]) + rw [eq0, eq_ave, zero_add] + /-- The definition `I_i(x)`, given above Lemma 7.1.3. The cube of scale `s` that contains `x`. There is at most 1 such cube, if it exists. -/ def cubeOf (i : β„€) (x : X) : Grid X := @@ -146,16 +206,318 @@ lemma pairwiseDisjoint_𝓛 : (𝓛 𝔖).PairwiseDisjoint (fun I ↦ (I : Set X exact (le_or_ge_or_disjoint.resolve_left (this mI mJ hn)).resolve_left (this mJ mI hn.symm) /-- The constant used in `first_tree_pointwise`. -Has value `10 * 2 ^ (105 * a ^ 3)` in the blueprint. -/ +Has value `10 * 2 ^ (104 * a ^ 3)` in the blueprint. -/ -- Todo: define this recursively in terms of previous constants -irreducible_def C7_1_4 (a : β„•) : ℝβ‰₯0 := 10 * 2 ^ (105 * (a : ℝ) ^ 3) +irreducible_def C7_1_4 (a : β„•) : ℝβ‰₯0 := 10 * 2 ^ (104 * (a : ℝ) ^ 3) + +-- Used in the proof of `exp_sub_one_le`, which is used to prove Lemma 7.1.4 +private lemma exp_Lipschitz : LipschitzWith 1 (fun (t : ℝ) ↦ exp (.I * t)) := by + have mul_I : Differentiable ℝ fun (t : ℝ) ↦ I * t := Complex.ofRealCLM.differentiable.const_mul I + refine lipschitzWith_of_nnnorm_deriv_le mul_I.cexp (fun x ↦ ?_) + have : (fun (t : ℝ) ↦ cexp (I * t)) = cexp ∘ (fun (t : ℝ) ↦ I * t) := rfl + rw [this, deriv_comp x differentiableAt_exp (mul_I x), Complex.deriv_exp, deriv_const_mul_field'] + simp_rw [show deriv ofReal x = 1 from ofRealCLM.hasDerivAt.deriv, mul_one] + rw [nnnorm_mul, nnnorm_I, mul_one, ← norm_toNNReal, mul_comm, Complex.norm_exp_ofReal_mul_I] + exact Real.toNNReal_one.le + +-- Used in the proof of Lemma 7.1.4 +private lemma exp_sub_one_le (t : ℝ) : β€–exp (.I * t) - 1β€– ≀ β€–tβ€– := by simpa using exp_Lipschitz t 0 + +-- Used in the proofs of Lemmas 7.1.4 and 7.1.5 +private lemma dist_lt_5 (hu : u ∈ t) (mp : p ∈ t.𝔗 u) (Qxp : Q x ∈ Ξ© p) : + dist_(p) (𝒬 u) (Q x) < 5 := calc + _ ≀ dist_(p) (𝒬 u) (𝒬 p) + dist_(p) (Q x) (𝒬 p) := dist_triangle_right .. + _ < 4 + 1 := + add_lt_add ((t.smul_four_le hu mp).2 (by convert mem_ball_self zero_lt_one)) (subset_cball Qxp) + _ = 5 := by norm_num + +-- The bound in the third display in the proof of Lemma 7.1.4 +private lemma L7_1_4_bound (hu : u ∈ t) {s : β„€} (hs : s ∈ t.Οƒ u x) {y : X} (hKxy : Ks s x y β‰  0) : + β€–exp (.I * (-𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1β€– ≀ + 5 * 2 ^ (4 * a) * 2 ^ (s - ΟƒMax t u x ⟨s, hs⟩) := + have ⟨pβ‚›, pu, xpβ‚›, hpβ‚›βŸ© := t.exists_p_of_mem_Οƒ u x hs + have ⟨p', p'u, xp', hp'⟩ := t.exists_p_of_mem_Οƒ u x (t.ΟƒMax_mem_Οƒ u x ⟨s, hs⟩) + have hr : (D : ℝ) ^ s / 2 > 0 := by rw [defaultD]; positivity + have s_le : GridStructure.s (π“˜ pβ‚›) ≀ GridStructure.s (π“˜ p') := by convert (Οƒ t u x).le_max' s hs + have exp_bound : + β€–exp (.I * (- 𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1β€– ≀ ‖𝒬 u y - Q x y - 𝒬 u x + Q x xβ€– := by + convert exp_sub_one_le (- 𝒬 u y + Q x y + 𝒬 u x - Q x x) using 1 + Β· simp + Β· rw [← norm_neg]; ring_nf + have : dist_(pβ‚›) (𝒬 u) (Q x) ≀ 2 ^ (s - ΟƒMax t u x ⟨s, hs⟩) * dist_(p') (𝒬 u) (Q x) := by + have pβ‚›_le_p' : π“˜ pβ‚› ≀ π“˜ p' := le_of_mem_of_mem s_le xpβ‚›.1 xp'.1 + have sub_ge_0 : t.ΟƒMax u x ⟨s, hs⟩ - s β‰₯ 0 := by unfold ΟƒMax; linarith [(Οƒ t u x).le_max' s hs] + have : GridStructure.s (π“˜ pβ‚›) + (ΟƒMax t u x ⟨s, hs⟩ - s) = GridStructure.s (π“˜ p') := by + simp_rw [← hp', ← hpβ‚›, 𝔰, _root_.s]; ring + apply le_trans <| Grid.dist_strictMono_iterate' sub_ge_0 pβ‚›_le_p' this + gcongr + calc C2_1_2 a ^ (t.ΟƒMax u x ⟨s, hs⟩ - s) + _ ≀ C2_1_2 a ^ (t.ΟƒMax u x ⟨s, hs⟩ - s : ℝ) := by norm_cast + _ ≀ (1 / 2 : ℝ) ^ (t.ΟƒMax u x ⟨s, hs⟩ - s : ℝ) := + Real.rpow_le_rpow (by rw [C2_1_2]; positivity) + ((C2_1_2_le_inv_512 X).trans (by norm_num)) (by norm_cast) + _ = 2 ^ (s - ΟƒMax t u x ⟨s, hs⟩) := by simp [← Int.cast_sub] + calc β€–exp (.I * (-𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1β€– + _ ≀ dist_{x, D ^ s / 2} (𝒬 u) (Q x) := + exp_bound.trans <| oscillation_le_cdist x _ (𝒬 u) (Q x) + (mem_ball_comm.mp (mem_Ioo.mp (dist_mem_Ioo_of_Ks_ne_zero hKxy)).2) (mem_ball_self hr) + _ ≀ _ := cdist_mono <| ball_subset_ball (show (D : ℝ) ^ s / 2 ≀ 4 * D ^ s by linarith) + _ ≀ defaultA a * dist_{𝔠 pβ‚›, 2 * D ^ s} (𝒬 u) (Q x) := by + have two_mul_two : 2 * (2 * (D : ℝ) ^ s) = 4 * D ^ s := by ring + have x_in_ball : dist (𝔠 pβ‚›) x < 2 * (2 * D ^ s) := by + rw [two_mul_two, ← hpβ‚›] + exact mem_ball'.mp <| Grid_subset_ball xpβ‚›.1 + refine le_of_eq_of_le ?_ (cdist_le x_in_ball) + rw [two_mul_two] + _ ≀ defaultA a * (defaultA a ^ 3 * dist_(pβ‚›) (𝒬 u) (Q x)) := by + gcongr + convert cdist_le_iterate (div_pos (defaultD_pow_pos a s) four_pos) _ _ _ using 2 + Β· rw [show 2 ^ 3 * ((D : ℝ) ^ s / 4) = 2 * D ^ s by ring] + Β· rw [hpβ‚›] + _ = (defaultA a) ^ 4 * dist_(pβ‚›) (𝒬 u) (Q x) := by ring + _ ≀ (2 ^ a) ^ 4 * (2 ^ (s - t.ΟƒMax u x _) * dist_(p') (𝒬 u) (Q x)) := by norm_cast; gcongr + _ ≀ (2 ^ a) ^ 4 * (2 ^ (s - t.ΟƒMax u x _) * 5) := by gcongr; exact (dist_lt_5 hu p'u xp'.2.1).le + _ = 5 * 2 ^ (4 * a) * 2 ^ (s - ΟƒMax t u x ⟨s, hs⟩) := by ring + +-- The bound used implicitly in the fourth displayed inequality in the proof of Lemma 7.1.4 +variable (f) in +private lemma L7_1_4_integrand_bound (hu : u ∈ t) {s : β„€} (hs : s ∈ t.Οƒ u x) (y : X) : + β€–(exp (.I * (- 𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1) * Ks s x y * f yβ€– ≀ + 5 * 2^(s - ΟƒMax t u x ⟨s, hs⟩) * (2^(103 * a ^ 3) / volume.real (ball x (D ^ s))) * β€–f yβ€– := by + by_cases hKxy : Ks s x y = 0 + Β· rw [hKxy, mul_zero, zero_mul, norm_zero]; positivity + Β· rw [norm_mul, norm_mul] + refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg (f y)) + apply mul_le_mul (L7_1_4_bound hu hs hKxy) norm_Ks_le (norm_nonneg _) (by positivity) |>.trans + rw [mul_assoc 5, mul_comm (2 ^ (4 * a)), ← mul_assoc, mul_assoc, mul_div, C2_1_3] + gcongr + norm_cast + rw_mod_cast [← pow_add] + refine Nat.pow_le_pow_of_le_right two_pos <| Nat.add_le_of_le_sub ?_ ?_ + Β· exact Nat.mul_le_mul_right _ (by norm_num) + Β· rw [← Nat.sub_mul, (show a ^ 3 = a ^ 2 * a from rfl)]; nlinarith [four_le_a X] + +-- The geometric sum used to prove `L7_1_4_sum` +private lemma sum_pow_two_le (a b : β„€) : βˆ‘ s ∈ Finset.Icc a b, (2 : ℝβ‰₯0) ^ s ≀ 2 ^ (b + 1) := by + by_cases h : b < a + Β· simp [Finset.Icc_eq_empty_of_lt h] + obtain ⟨k, rfl⟩ : βˆƒ (k : β„•), b = a + k := ⟨(b - a).toNat, by simp [not_lt.mp h]⟩ + suffices βˆ‘ s ∈ Finset.Icc a (a + k), (2 : ℝβ‰₯0) ^ s = 2 ^ a * βˆ‘ n ∈ Finset.range (k + 1), 2 ^ n by + rw [this, add_assoc, zpow_add' (Or.inl two_pos.ne.symm), mul_le_mul_left (zpow_pos two_pos a), + geom_sum_of_one_lt one_lt_two (k + 1), NNReal.sub_def (r := 2)] + norm_num + exact le_self_add + rw [Finset.mul_sum] + apply Finset.sum_bij (fun n hn ↦ (n - a).toNat) + Β· intro n hn + rw [Finset.mem_Icc] at hn + rw [Finset.mem_range, Int.toNat_lt (Int.sub_nonneg.mpr hn.1), Nat.cast_add, Nat.cast_one] + linarith + Β· intro n hn m hm hnm + rw [Finset.mem_Icc] at hn hm + simpa [Int.sub_nonneg.mpr hn.1, Int.sub_nonneg.mpr hm.1] using congrArg Int.ofNat hnm + Β· exact fun n hn ↦ by use a + n, by simp [Nat.le_of_lt_succ (Finset.mem_range.mp hn)], by simp + Β· intro n hn + rw [← zpow_natCast, Int.ofNat_toNat, ← zpow_add' (Or.inl two_pos.ne.symm), + sup_eq_left.mpr <| Int.sub_nonneg_of_le (Finset.mem_Icc.mp hn).1, add_sub_cancel] + +-- The sum used in the proof of Lemma 7.1.4 +private lemma L7_1_4_sum (hΟƒ : (t.Οƒ u x).Nonempty) : + βˆ‘ s ∈ t.Οƒ u x, (2 : ℝβ‰₯0) ^ (s - t.ΟƒMax u x hΟƒ) ≀ 2 := by + have {s : β„€} : (2 : ℝβ‰₯0) ^ (s - t.ΟƒMax u x hΟƒ) = 2 ^ s * 2 ^ (- t.ΟƒMax u x hΟƒ) := by + rw [← zpow_add' (Or.inl two_pos.ne.symm), Int.sub_eq_add_neg] + simp_rw [this, ← Finset.sum_mul] + suffices βˆ‘ s ∈ t.Οƒ u x, (2 : ℝβ‰₯0) ^ s ≀ 2 ^ (t.ΟƒMax u x hΟƒ + 1) from calc + _ ≀ (2 : ℝβ‰₯0) ^ (t.ΟƒMax u x hΟƒ + 1) * 2 ^ (-t.ΟƒMax u x hΟƒ) := by gcongr + _ = 2 := by rw [zpow_add' (Or.inl two_pos.ne.symm)]; field_simp + refine le_trans (Finset.sum_le_sum_of_subset ?_) (sum_pow_two_le (t.ΟƒMin u x hΟƒ) (t.ΟƒMax u x hΟƒ)) + exact fun s hs ↦ Finset.mem_Icc.mpr <| ⟨(t.Οƒ u x).min'_le s hs, (t.Οƒ u x).le_max' s hs⟩ + +-- Inequality used twice in the proof of Lemma 7.1.4 +private lemma L7_1_4_dist_le {p : 𝔓 X} (xp : x ∈ E p) {J : Grid X} + (hJ : ((J : Set X) ∩ ball x (D ^ 𝔰 p / 2)).Nonempty) : + dist (c J) (𝔠 p) ≀ 4 * D ^ (s J) + 4.5 * D ^ (𝔰 p) := by + have ⟨z, hz⟩ := hJ + calc dist (c J) (𝔠 p) + _ ≀ dist (c J) z + dist z x + dist x (𝔠 p) := dist_triangle4 (c J) z x (𝔠 p) + _ ≀ 4 * D ^ (s J) + 0.5 * D ^ (𝔰 p) + 4 * D ^ (𝔰 p) := by + apply add_le_add_three + Β· exact (mem_ball'.mp <| Grid_subset_ball hz.1).le + Β· convert (mem_ball.mp hz.2).le using 1 + exact (eq_div_iff two_pos.ne.symm).mpr (by linarith) + Β· exact (mem_ball.mp <| Grid_subset_ball xp.1).le + _ ≀ 4 * D ^ (s J) + 4.5 * D ^ (𝔰 p) := by linarith [defaultD_pow_pos a (𝔰 p)] + +-- Inequality needed for the proof of `L7_1_4_integral_le_integral` +private lemma L7_1_4_s_le_s {p : 𝔓 X} (pu : p ∈ t.𝔗 u) (xp : x ∈ E p) + {J : Grid X} (hJ : J ∈ 𝓙 (t.𝔗 u) ∧ ((J : Set X) ∩ ball x (D ^ 𝔰 p / 2)).Nonempty) : + s J ≀ 𝔰 p := by + have ⟨z, hz⟩ := hJ.2 + by_cases h : s J ≀ 𝔰 p ∨ s J = -S + Β· exact h.elim id (Β· β–Έ (range_s_subset βŸ¨π“˜ p, rfl⟩).1) + push_neg at h + apply False.elim ∘ hJ.1.1.resolve_left h.2 p pu ∘ le_trans Grid_subset_ball ∘ ball_subset_ball' + have : (D : ℝ) ^ 𝔰 p ≀ D ^ s J := (zpow_le_zpow_iff_rightβ‚€ (one_lt_D (X := X))).mpr h.1.le + calc 4 * (D : ℝ) ^ GridStructure.s (π“˜ p) + dist (GridStructure.c (π“˜ p)) (c J) + _ ≀ 4 * (D : ℝ) ^ (s J) + (4 * D ^ (s J) + 4.5 * D ^ (s J)) := by + gcongr 4 * ?_ + ?_ + Β· exact this + Β· exact dist_comm (c (π“˜ p)) (c J) β–Έ L7_1_4_dist_le xp hJ.2 |>.trans (by gcongr) + _ ≀ 100 * D ^ (s J + 1) := by + rw [zpow_add' (Or.inl (defaultD_pos a).ne.symm), zpow_one] + nlinarith [one_le_D (a := a), defaultD_pow_pos a (s J)] + +-- The integral bound needed for the proof of Lemma 7.1.4 +private lemma L7_1_4_integral_le_integral (hu : u ∈ t) (hf : BoundedCompactSupport f) {p : 𝔓 X} + (pu : p ∈ t.𝔗 u) (xp : x ∈ E p) : ∫ y in ball x ((D : ℝ) ^ (𝔰 p) / 2), β€–f yβ€– ≀ + ∫ y in ball (𝔠 p) (16 * (D : ℝ) ^ (𝔰 p)), β€–approxOnCube (𝓙 (t u)) (β€–f Β·β€–) yβ€– := by + let Js := Set.toFinset { J ∈ 𝓙 (t u) | ((J : Set X) ∩ ball x (D ^ (𝔰 p) / 2)).Nonempty } + have mem_Js {J : Grid X} : J ∈ Js ↔ J ∈ 𝓙 (t.𝔗 u) ∧ (↑J ∩ ball x (D ^ 𝔰 p / 2)).Nonempty := by + simp [Js] + have Js_disj : (Js : Set (Grid X)).Pairwise (Disjoint on fun J ↦ (J : Set X)) := + fun i₁ hi₁ iβ‚‚ hiβ‚‚ h ↦ pairwiseDisjoint_𝓙 (mem_Js.mp hi₁).1 (mem_Js.mp hiβ‚‚).1 h + calc ∫ y in ball x (D ^ (𝔰 p) / 2), β€–f yβ€– + _ ≀ ∫ y in (⋃ J ∈ Js, (J : Set X)), β€–f yβ€– := by + apply setIntegral_mono_set hf.integrable.norm.integrableOn (Eventually.of_forall (by simp)) + suffices h : ball x (D ^ (𝔰 p) / 2) βŠ† ⋃ J ∈ 𝓙 (t.𝔗 u), (J : Set X) by + refine ((subset_inter_iff.mpr ⟨h, subset_refl _⟩).trans (fun y hy ↦ ?_)).eventuallyLE + have ⟨J, hJ, yJ⟩ := Set.mem_iUnionβ‚‚.mp hy.1 + exact ⟨J, ⟨⟨J, by simp [mem_Js.mpr ⟨hJ, ⟨y, mem_inter yJ hy.2⟩⟩]⟩, yJ⟩⟩ + calc ball x (D ^ 𝔰 p / 2) + _ βŠ† ball x (4 * D ^ 𝔰 p) := ball_subset_ball <| by linarith [defaultD_pow_pos a (𝔰 p)] + _ βŠ† (π“˜ u : Set X) := ball_subset_of_mem_π“˜ hu pu xp.1 + _ βŠ† ⋃ (I : Grid X), (I : Set X) := le_iSup _ _ + _ = ⋃ J ∈ 𝓙 (t.𝔗 u), (J : Set X) := biUnion_𝓙.symm + _ = βˆ‘ J in Js, ∫ y in J, β€–f yβ€– := by + have Js_disj : (Js : Set (Grid X)).Pairwise (Disjoint on fun J ↦ (J : Set X)) := + fun i₁ hi₁ iβ‚‚ hiβ‚‚ h ↦ pairwiseDisjoint_𝓙 (mem_Js.mp hi₁).1 (mem_Js.mp hiβ‚‚).1 h + apply integral_finset_biUnion Js (fun _ _ ↦ coeGrid_measurable) Js_disj + exact fun i hi ↦ hf.norm.integrable.integrableOn + _ = βˆ‘ J in Js, ∫ y in J, (approxOnCube (𝓙 (t u)) (β€–f Β·β€–)) y := by + refine Finset.sum_congr rfl (fun J hJ ↦ ?_) + have eq : EqOn (approxOnCube (𝓙 (t u)) (β€–f Β·β€–)) (fun _ ↦ ⨍ y in J, β€–f yβ€–) J := + fun y hy ↦ approxOnCube_apply pairwiseDisjoint_𝓙 (β€–f Β·β€–) (mem_Js.mp hJ).1 hy + rw [setIntegral_congr_fun coeGrid_measurable eq, setIntegral_const, average] + simp [← mul_assoc, CommGroupWithZero.mul_inv_cancel (volume (J : Set X)).toReal <| + ENNReal.toReal_ne_zero.mpr ⟨(volume_coeGrid_pos _).ne.symm, volume_coeGrid_lt_top.ne⟩] + _ = ∫ y in (⋃ J ∈ Js, (J : Set X)), (approxOnCube (𝓙 (t u)) (β€–f Β·β€–)) y := by + refine integral_finset_biUnion Js (fun _ _ ↦ coeGrid_measurable) ?_ ?_ |>.symm + Β· exact fun i₁ hi₁ iβ‚‚ hiβ‚‚ h ↦ pairwiseDisjoint_𝓙 (mem_Js.mp hi₁).1 (mem_Js.mp hiβ‚‚).1 h + Β· exact fun i hi ↦ And.intro (stronglyMeasurable_approxOnCube _ _).aestronglyMeasurable + (integrable_approxOnCube (𝓙 (t u))).restrict.hasFiniteIntegral + _ = ∫ y in (⋃ J ∈ Js, (J : Set X)), β€–(approxOnCube (𝓙 (t u)) (β€–f Β·β€–)) yβ€– := + setIntegral_congr_fun (Js.measurableSet_biUnion fun _ _ ↦ coeGrid_measurable) <| fun y _ ↦ + (Real.norm_of_nonneg <| approxOnCube_nonneg (𝓙 (t u)) (fun _ ↦ norm_nonneg _) y).symm + _ ≀ ∫ y in ball (𝔠 p) (16 * (D : ℝ) ^ (𝔰 p)), β€–approxOnCube (𝓙 (t u)) (β€–f Β·β€–) yβ€– := by + apply setIntegral_mono_set (integrable_approxOnCube _).norm.integrableOn <| + Eventually.of_forall (fun _ ↦ norm_nonneg _) + refine (iUnionβ‚‚_subset_iff.mpr (fun J hJ ↦ ?_)).eventuallyLE + replace hJ := mem_Js.mp hJ + have ⟨z, hz⟩ := hJ.2 + refine Grid_subset_ball.trans (ball_subset_ball' ?_) + change _ * _ ^ (s J) + dist (c J) _ ≀ _ + have := (zpow_le_zpow_iff_rightβ‚€ (one_lt_D (X := X))).mpr <| L7_1_4_s_le_s pu xp hJ + linarith [L7_1_4_dist_le xp hJ.2, defaultD_pow_pos a (𝔰 p)] + +-- An average over `ball (𝔠 p) (16 * D ^ 𝔰 p)` is bounded by `MB`; needed for Lemma 7.1.4 +private lemma L7_1_4_laverage_le_MB (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L) (g : X β†’ ℝ) + {p : 𝔓 X} (pu : p ∈ t.𝔗 u) (xp : x ∈ E p) : + (∫⁻ y in ball (𝔠 p) (16 * D ^ 𝔰 p), β€–g yβ€–β‚Š) / volume (ball (𝔠 p) (16 * D ^ 𝔰 p)) ≀ + MB volume 𝓑 c𝓑 r𝓑 g x' := by + have mem_𝓑 : ⟨4, π“˜ p⟩ ∈ 𝓑 := by simp [𝓑] + convert le_biSup (hi := mem_𝓑) <| fun i ↦ ((ball (c𝓑 i) (r𝓑 i)).indicator (x := x') <| + fun _ ↦ ⨍⁻ y in ball (c𝓑 i) (r𝓑 i), β€–g yβ€–β‚Š βˆ‚volume) + Β· have x'_in_ball : x' ∈ ball (c𝓑 (4, π“˜ p)) (r𝓑 (4, π“˜ p)) := by + simp only [c𝓑, r𝓑, _root_.s] + have : x' ∈ π“˜ p := subset_of_mem_𝓛 hL pu (not_disjoint_iff.mpr ⟨x, xp.1, hx⟩) hx' + refine Metric.ball_subset_ball ?_ <| Grid_subset_ball this + linarith [defaultD_pow_pos a (GridStructure.s (π“˜ p))] + have hc𝓑 : 𝔠 p = c𝓑 (4, π“˜ p) := by simp [c𝓑, 𝔠] + have hr𝓑 : 16 * D ^ 𝔰 p = r𝓑 (4, π“˜ p) := by rw [r𝓑, 𝔰]; norm_num + simp [-defaultD, laverage, x'_in_ball, ENNReal.div_eq_inv_mul, hc𝓑, hr𝓑] + Β· simp [MB, maximalFunction] /-- Lemma 7.1.4 -/ lemma first_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L) (hf : BoundedCompactSupport f) : β€–βˆ‘ i in t.Οƒ u x, ∫ y, (exp (.I * (- 𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1) * Ks i x y * f y β€–β‚Š ≀ C7_1_4 a * MB volume 𝓑 c𝓑 r𝓑 (approxOnCube (𝓙 (t u)) (β€–f Β·β€–)) x' := by - sorry + set g := approxOnCube (𝓙 (t u)) (β€–f Β·β€–) + let q (y : X) := -𝒬 u y + Q x y + 𝒬 u x - Q x x + by_cases hΟƒ : (t.Οƒ u x).Nonempty; swap + Β· simp [Finset.not_nonempty_iff_eq_empty.mp hΟƒ] + by_cases hMB : MB volume 𝓑 c𝓑 r𝓑 g x' = ∞ -- `MB` is finite, but we don't need to prove that. + Β· exact hMB β–Έ le_of_le_of_eq (OrderTop.le_top _) (by simp [C7_1_4]) + rw [← ENNReal.coe_toNNReal hMB] + norm_cast + have : βˆ€ s ∈ t.Οƒ u x, β€–βˆ« (y : X), (cexp (I * (q y)) - 1) * Ks s x y * f yβ€–β‚Š ≀ + (∫ (y : X), β€–(cexp (I * (q y)) - 1) * Ks s x y * f yβ€–).toNNReal := + fun s hs ↦ by apply le_trans (norm_integral_le_integral_norm _) (by simp) + refine (nnnorm_sum_le _ _).trans <| ((t.Οƒ u x).sum_le_sum this).trans ?_ + suffices βˆ€ s ∈ t.Οƒ u x, (∫ (y : X), β€–(cexp (I * (q y)) - 1) * Ks s x y * f yβ€–).toNNReal ≀ + (5 * 2 ^ (104 * a ^ 3) * (MB volume 𝓑 c𝓑 r𝓑 g x').toNNReal) * 2 ^ (s - t.ΟƒMax u x hΟƒ) by + apply le_trans ((t.Οƒ u x).sum_le_sum this) + rw [← Finset.mul_sum] + apply le_trans <| mul_le_mul_left' (L7_1_4_sum hΟƒ) _ + rw [mul_comm _ 2, ← mul_assoc, ← mul_assoc, C7_1_4] + gcongr + Β· norm_num + Β· exact_mod_cast pow_le_pow_rightβ‚€ one_lt_two.le (le_refl _) + intro s hs + have eq1 : ∫ (y : X), β€–(cexp (I * (q y)) - 1) * Ks s x y * f yβ€– = + ∫ y in ball x (D ^ s / 2), β€–(cexp (I * (q y)) - 1) * Ks s x y * f yβ€– := by + rw [← integral_indicator measurableSet_ball] + refine integral_congr_ae (EventuallyEq.of_eq (Set.indicator_eq_self.mpr fun y hy ↦ ?_)).symm + exact mem_ball_comm.mp (mem_Ioo.mp (dist_mem_Ioo_of_Ks_ne_zero fun h ↦ by simp [h] at hy)).2 + have eq2 : (∫ y in ball x (D ^ s / 2), β€–(cexp (I * (q y)) - 1) * Ks s x y * f yβ€–).toNNReal ≀ + 5 * 2 ^ (s - ΟƒMax t u x ⟨s, hs⟩) * (2 ^ (103 * a ^ 3) / volume.real (ball x (D ^ s))) * + (∫ y in ball x (D ^ s / 2), β€–f yβ€–).toNNReal := by + rw [Real.coe_toNNReal _ <| setIntegral_nonneg measurableSet_ball (fun _ _ ↦ norm_nonneg _)] + convert le_trans (integral_mono_of_nonneg (Eventually.of_forall ?_) + (hf.integrable.norm.const_mul _).restrict + (Eventually.of_forall <| L7_1_4_integrand_bound f hu hs)) ?_ + Β· norm_cast + Β· simp only [Pi.zero_apply, norm_nonneg, implies_true] + Β· exact isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure + Β· rw [integral_mul_left]; gcongr; simp + apply le_of_eq_of_le (congrArg Real.toNNReal eq1) ∘ eq2.trans + simp only [Real.coe_toNNReal', NNReal.val_eq_coe, NNReal.coe_mul, NNReal.coe_ofNat, + NNReal.coe_pow, NNReal.coe_zpow] + simp_rw [sup_of_le_left <| setIntegral_nonneg measurableSet_ball (fun _ _ ↦ norm_nonneg _)] + have : 5 * 2 ^ (s - t.ΟƒMax u x hΟƒ) * (2 ^ (103 * a ^ 3) / volume.real (ball x (D ^ s))) * + (∫ y in ball x (D ^ s / 2), β€–f yβ€–) = 5 * (2 ^ (103 * a ^ 3) * + ((∫ y in ball x (D ^ s / 2), β€–f yβ€–) / volume.real (ball x (D ^ s)))) * + 2 ^ (s - t.ΟƒMax u x hΟƒ) := by ring + rw [this, mul_le_mul_right (zpow_pos two_pos _), mul_assoc, mul_le_mul_left (by norm_num)] + rw [Nat.succ_mul 103, pow_add, mul_assoc, mul_le_mul_left (pow_pos two_pos _)] + have ⟨pβ‚›, pβ‚›u, xpβ‚›, hpβ‚›βŸ© := t.exists_p_of_mem_Οƒ u x hs + have ball_subset : ball (𝔠 pβ‚›) (16 * D ^ s) βŠ† ball x ((2 ^ 5) * D ^ s) := + ball_subset_ball' <| calc 16 * (D : ℝ) ^ s + dist (𝔠 pβ‚›) x + _ ≀ 16 * D ^ s + 4 * D ^ _ := add_le_add_left (mem_ball'.mp (Grid_subset_ball xpβ‚›.1)).le _ + _ = 16 * D ^ s + 4 * D ^ s := by nth_rewrite 3 [← hpβ‚›]; rfl + _ ≀ (2 ^ 5) * D ^ s := by linarith [defaultD_pow_pos a s] + calc (∫ y in ball x (D ^ s / 2), β€–f yβ€–) / volume.real (ball x (D ^ s)) + _ ≀ 2 ^ (5 * a) * ((∫ y in ball x (D^s / 2), β€–f yβ€–) / volume.real (ball (𝔠 pβ‚›) (16 * D^s))) := by + rw [mul_comm (2 ^ (5 * a)), div_mul] + apply div_le_divβ‚€ (setIntegral_nonneg measurableSet_ball (fun _ _ ↦ norm_nonneg _)) (le_refl _) + Β· exact div_pos (hb := pow_pos two_pos (5 * a)) <| + measure_ball_pos_real (𝔠 pβ‚›) (16 * D ^ s) (mul_pos (by norm_num) <| defaultD_pow_pos a s) + Β· apply (div_le_iffβ‚€' (pow_pos two_pos (5 * a))).mpr + apply le_trans <| ENNReal.toReal_mono (measure_ball_ne_top x _) <| + OuterMeasureClass.measure_mono volume ball_subset + apply le_of_le_of_eq <| measure_real_ball_two_le_same_iterate x (D ^ s) 5 + simp [mul_comm 5 a, pow_mul] + _ ≀ 2 ^ (a ^ 3) * (MB volume 𝓑 c𝓑 r𝓑 g x').toNNReal := by + gcongr ?_ * ?_ + Β· apply pow_right_monoβ‚€ one_lt_two.le + rw [pow_succ a 2, mul_le_mul_right (a_pos X)] + nlinarith [four_le_a X] + Β· refine le_trans ?_ <| ENNReal.toReal_mono hMB <| L7_1_4_laverage_le_MB hL hx hx' g pβ‚›u xpβ‚› + rw [hpβ‚›, ENNReal.toReal_div] + refine div_le_div_of_nonneg_right ?_ measureReal_nonneg + rw [← integral_norm_eq_lintegral_nnnorm] + Β· exact hpβ‚› β–Έ L7_1_4_integral_le_integral hu hf pβ‚›u xpβ‚› + Β· exact (stronglyMeasurable_approxOnCube (𝓙 (t u)) (β€–f Β·β€–)).aestronglyMeasurable.restrict /-- Lemma 7.1.5 -/ lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L) : @@ -177,13 +539,7 @@ lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L 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' - have d5 : dist_(p') (𝒬 u) (Q x) < 5 := - 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)) - (subset_cball Qxp') - _ = _ := by norm_num + have d5 : dist_(p') (𝒬 u) (Q x) < 5 := dist_lt_5 hu mp' Qxp' have d5' : dist_{x, D ^ sβ‚‚} (𝒬 u) (Q x) < 5 * defaultA a ^ 5 := by have i1 : dist x (𝔠 p) < 4 * D ^ 𝔰 p' := (mem_ball.mp (Grid_subset_ball xp)).trans_le <| diff --git a/Carleson/GridStructure.lean b/Carleson/GridStructure.lean index 6f447f28..730cfc41 100644 --- a/Carleson/GridStructure.lean +++ b/Carleson/GridStructure.lean @@ -399,4 +399,10 @@ lemma dist_strictMono_iterate {I J : Grid X} {d : β„•} (hij : I ≀ J) (hs : s I Β· exact dist_strictMono KJ _ = _ := by ring +-- Version of `dist_strictMono_iterate` with `d` in `β„€` +lemma dist_strictMono_iterate' {I J : Grid X} {d : β„€} (hd : d β‰₯ 0) (hij : I ≀ J) + (hs : s I + d = s J) {f g : Θ X} : dist_{I} f g ≀ C2_1_2 a ^ d * dist_{J} f g := by + rw [← Int.toNat_of_nonneg hd] at hs ⊒ + exact dist_strictMono_iterate hij hs + end Grid diff --git a/Carleson/Psi.lean b/Carleson/Psi.lean index 08750395..b469065f 100644 --- a/Carleson/Psi.lean +++ b/Carleson/Psi.lean @@ -331,13 +331,17 @@ lemma sum_Ks {t : Finset β„€} (hs : nonzeroS D (dist x y) βŠ† t) (hD : 1 < (D : -- (hD : 1 < D) (h : x β‰  y) : βˆ‘ i in t, Ks i x y = K x y := by -- sorry -lemma dist_mem_Icc_of_Ks_ne_zero {s : β„€} {x y : X} (h : Ks s x y β‰  0) : - dist x y ∈ Icc ((D ^ (s - 1) : ℝ) / 4) (D ^ s / 2) := by +lemma dist_mem_Ioo_of_Ks_ne_zero {s : β„€} {x y : X} (h : Ks s x y β‰  0) : + dist x y ∈ Ioo ((D ^ (s - 1) : ℝ) / 4) (D ^ s / 2) := by simp only [Ks, Nat.cast_pow, Nat.cast_ofNat, zpow_neg, ne_eq, mul_eq_zero, ofReal_eq_zero] at h - have dist_mem_Icc := Ioo_subset_Icc_self (support_ψ (D1 X) β–Έ mem_support.2 (not_or.1 h).2) - rwa [mem_Icc, ← div_eq_inv_mul, le_div_iffβ‚€ (D_pow0' (D1 X) s), - div_le_iffβ‚€ (D_pow0' (D1 X) s), mul_inv, mul_assoc, inv_mul_eq_div (4 : ℝ), ← zpow_neg_one, - ← zpow_addβ‚€ (D0' X).ne.symm, neg_add_eq_sub, ← div_eq_inv_mul] at dist_mem_Icc + have dist_mem_Ioo := support_ψ (D1 X) β–Έ mem_support.2 (not_or.1 h).2 + rwa [mem_Ioo, ← div_eq_inv_mul, lt_div_iffβ‚€ (D_pow0' (D1 X) s), + div_lt_iffβ‚€ (D_pow0' (D1 X) s), mul_inv, mul_assoc, inv_mul_eq_div (4 : ℝ), ← zpow_neg_one, + ← zpow_addβ‚€ (D0' X).ne.symm, neg_add_eq_sub, ← div_eq_inv_mul] at dist_mem_Ioo + +lemma dist_mem_Icc_of_Ks_ne_zero {s : β„€} {x y : X} (h : Ks s x y β‰  0) : + dist x y ∈ Icc ((D ^ (s - 1) : ℝ) / 4) (D ^ s / 2) := + Ioo_subset_Icc_self (dist_mem_Ioo_of_Ks_ne_zero h) /-- The constant appearing in part 2 of Lemma 2.1.3. -/ def C2_1_3 (a : ℝβ‰₯0) : ℝβ‰₯0 := 2 ^ (102 * (a : ℝ) ^ 3) diff --git a/Carleson/ToMathlib/Misc.lean b/Carleson/ToMathlib/Misc.lean index f2806cdd..4f82be42 100644 --- a/Carleson/ToMathlib/Misc.lean +++ b/Carleson/ToMathlib/Misc.lean @@ -388,4 +388,51 @@ theorem indicator_const {c : ℝ} {s: Set X} end Integrable +-- Currently unused +open Classical in +theorem setIntegral_biUnion_le_sum_setIntegral {X : Type*} {ΞΉ : Type*} [MeasurableSpace X] + {f : X β†’ ℝ} (s : Finset ΞΉ) {S : ΞΉ β†’ Set X} {ΞΌ : Measure X} + (f_ae_nonneg : βˆ€α΅ (x : X) βˆ‚ΞΌ.restrict (⋃ i ∈ s, S i), 0 ≀ f x) + (int_f : IntegrableOn f (⋃ i ∈ s, S i) ΞΌ) : + ∫ x in (⋃ i ∈ s, S i), f x βˆ‚ΞΌ ≀ βˆ‘ i ∈ s, ∫ x in S i, f x βˆ‚ΞΌ := by + have res_res : βˆ€ i ∈ s, (ΞΌ.restrict (⋃ i ∈ s, S i)).restrict (S i) = ΞΌ.restrict (S i) := + fun i hi ↦ by rw [Measure.restrict_restrict_of_subset]; exact (subset_biUnion_of_mem hi) + -- Show that it suffices to prove the result in the case where the integrand is measurable + let g := AEMeasurable.mk f int_f.aemeasurable + have g_ae_nonneg : βˆ€α΅ (x : X) βˆ‚ΞΌ.restrict (⋃ i ∈ s, S i), 0 ≀ g x := by + apply f_ae_nonneg.congr ∘ int_f.aemeasurable.ae_eq_mk.mp + exact Filter.Eventually.of_forall (fun _ h ↦ by rw [h]) + have int_g : βˆ€ i ∈ s, Integrable g (ΞΌ.restrict (S i)) := by + intro i hi + have := (int_f.congr int_f.aemeasurable.ae_eq_mk).restrict (s := S i) + rwa [res_res i hi] at this + have : βˆ‘ i ∈ s, ∫ (x : X) in S i, f x βˆ‚ΞΌ = βˆ‘ i ∈ s, ∫ (x : X) in S i, g x βˆ‚ΞΌ := by + refine Finset.sum_congr rfl (fun i hi ↦ integral_congr_ae ?_) + convert int_f.aemeasurable.ae_eq_mk.restrict (s := S i) using 2 + rw [Measure.restrict_restrict_of_subset] + exact (subset_biUnion_of_mem hi) + rw [this, integral_congr_ae int_f.aemeasurable.ae_eq_mk] + -- Now prove the result for the measurable integrand `g` + have meas : MeasurableSet {x | 0 ≀ g x} := + have : {x | 0 ≀ g x} = g ⁻¹' (Ici 0) := by simp [preimage, mem_Ici] + this β–Έ (AEMeasurable.measurable_mk int_f.aemeasurable) measurableSet_Ici + rw [← integral_finset_sum_measure int_g] + set ΞΌβ‚€ : ΞΉ β†’ Measure X := fun i ↦ ite (i ∈ s) (ΞΌ.restrict (S i)) 0 + refine integral_mono_measure ?_ ?_ (integrable_finset_sum_measure.mpr int_g) + Β· refine Measure.le_iff.mpr (fun T hT ↦ ?_) + simp_rw [ΞΌ.restrict_apply hT, Measure.coe_finset_sum, s.sum_apply, inter_iUnion] + apply le_trans <| measure_biUnion_finset_le s (T ∩ S Β·) + exact s.sum_le_sum (fun _ _ ↦ ge_of_eq (ΞΌ.restrict_apply hT)) + Β· have : βˆ‘ i ∈ s, ΞΌ.restrict (S i) = Measure.sum ΞΌβ‚€ := by + ext T hT + simp only [Measure.sum_apply (hs := hT), Measure.coe_finset_sum, s.sum_apply, ΞΌβ‚€] + rw [tsum_eq_sum (s := s) (fun b hb ↦ by simp [hb])] + exact Finset.sum_congr rfl (fun i hi ↦ by simp [hi, res_res]) + rw [Filter.EventuallyLE, this, Measure.ae_sum_iff' (by exact meas)] + intro i + by_cases hi : i ∈ s + Β· simp only [Pi.zero_apply, hi, reduceIte, ΞΌβ‚€, ← res_res i hi, ae_restrict_iff meas] + exact g_ae_nonneg.mono (fun _ h _ ↦ h) + Β· simp [hi, ΞΌβ‚€] + end MeasureTheory diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index bd3de728..92abbe28 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -4367,11 +4367,12 @@ \section{The pointwise tree estimate} \uses{convex-scales} For all $\fu \in \fU$, all $L \in \mathcal{L}(\fT(\fu))$, all $x, x' \in L$ and all bounded $f$ with bounded support, we have $$ - \eqref{eq-term-A} \le 10 \cdot 2^{105a^3} M_{\mathcal{B}, 1}P_{\mathcal{J}(\fT(\fu))}|f|(x')\,. + \eqref{eq-term-A} \le 10 \cdot 2^{104a^3} M_{\mathcal{B}, 1}P_{\mathcal{J}(\fT(\fu))}|f|(x')\,. $$ \end{lemma} \begin{proof} + \leanok Let $s \in \sigma(\fu,x)$. If $x, y \in X$ are such that $K_s(x,y)\neq 0$, then, by \eqref{supp-Ks}, we have $\rho(x,y)\leq 1/2 D^s$. By $1$-Lipschitz continuity of the function $t \mapsto \exp(it) = e(t)$ and the property \eqref{osccontrol} of the metrics $d_B$, it follows that \begin{multline*} @@ -4379,19 +4380,19 @@ \section{The pointwise tree estimate} \leq d_{B(x, 1/2 D^{s})}(\fcc(\fu), \tQ(x))\,. \end{multline*} Let $\fp_s \in \fT(\fu)$ be a tile with $\ps(\fp_s) = s$ and $x \in E(\fp_s)$, and let $\fp'$ be a tile with $\ps(\fp') = \overline{\sigma}(\fu, x)$ and $x \in E(\fp')$. - Using the doubling property \eqref{firstdb}, the definition of $d_{\fp}$ and \Cref{monotone-cube-metrics}, we can bound the previous display by + Using the monotonicity property \eqref{monotonedb}, the doubling property \eqref{firstdb} repeatedly, the definition of $d_{\fp}$ and \Cref{monotone-cube-metrics}, we can bound the previous display by $$ - 2^a d_{\fp_s}(\fcc(\fu), \tQ(x)) \le 2^{a} 2^{s - \overline{\sigma}(\fu, x)} d_{\fp'}(\fcc(\fu), \tQ(x))\,. + d_{B(x, 4 D^{s})}(\fcc(\fu), \tQ(x)) \leq 2^{4a} d_{\fp_s}(\fcc(\fu), \tQ(x)) \le 2^{4a} 2^{s - \overline{\sigma}(\fu, x)} d_{\fp'}(\fcc(\fu), \tQ(x))\,. $$ Since $\fcc(\fu) \in B_{\fp'}(\fcc(\fp'), 4)$ by \eqref{forest1} and $\tQ(x) \in \Omega(\fp') \subset B_{\fp'}(\fcc(\fp'), 1)$ by \eqref{eq-freq-comp-ball}, this is estimated by $$ - \le 5 \cdot 2^{a} 2^{s - \overline{\sigma}(\fu, x)} \,. + \le 5 \cdot 2^{4a} 2^{s - \overline{\sigma}(\fu, x)} \,. $$ Using \eqref{eq-Ks-size}, it follows that $$ \eqref{eq-term-A} \le 5\cdot 2^{103a^3} \sum_{s\in\sigma(x)}2^{s - \overline{\sigma}(\fu, x)} \frac{1}{\mu(B(x,D^s))}\int_{B(x,0.5D^{s})}|f(y)|\,\mathrm{d}\mu(y)\,. $$ - By \eqref{eq-J-partition}, the collection $\mathcal{J}$ is a partition of $X$, so this is estimated by + By \eqref{eq-J-partition}, the collection $\mathcal{J}$ is a partition of $\bigcup_{I \in \mathcal{D}} I$, so this is estimated by $$ 5\cdot 2^{103a^3} \sum_{s\in\sigma(x)}2^{s - \overline{\sigma}(\fu, x)} \frac{1}{\mu(B(x,D^s))}\sum_{\substack{J \in \mathcal{J}(\fT(\fu))\\J \cap B(x, 0.5D^s) \ne \emptyset} }\int_{J}|f(y)|\,\mathrm{d}\mu(y)\,. $$ @@ -4403,20 +4404,20 @@ \section{The pointwise tree estimate} $$ 5\cdot 2^{103a^3} \sum_{s\in\sigma(x)}2^{s - \overline{\sigma}(\fu, x)} \frac{1}{\mu(B(x,D^s))}\int_{B(\pc(\fp_s),16 D^s)}P_{\mathcal{J}(\fT(\fu))}|f(y)|\,\mathrm{d}\mu(y)\,. $$ - We have $B(\pc(\fp_s), 16D^s)) \subset B(x, 32D^s)$, by \eqref{eq-vol-sp-cube} and the triangle inequality, since $x \in \scI(\fp)$. Combining this with the doubling property \eqref{doublingx}, we obtain + We have $B(\pc(\fp_s), 16D^s)) \subset B(x, 32D^s)$, by \eqref{eq-vol-sp-cube} and the triangle inequality, since $x \in \scI(\fp_s)$. Combining this with the doubling property \eqref{doublingx}, we obtain $$ \mu(B(\pc(\fp_s), 16D^s)) \le 2^{5a} \mu(B(x, D^s))\,. $$ Since $a \ge 4$, it follows that \eqref{eq-term-A} is bounded by $$ - 2^{104a^3} \sum_{s\in\sigma(x)}2^{s - \overline{\sigma}(\fu, x)} \frac{1}{\mu(B(\pc(\fp_s),16D^s))}\int_{B(\pc(\fp_s),16D^s)}P_{\mathcal{J}(\fT(\fu))}|f(y)|\,\mathrm{d}\mu(y)\,. + 5\cdot 2^{103a^3} \sum_{s\in\sigma(x)}2^{s - \overline{\sigma}(\fu, x)} \frac{1}{\mu(B(\pc(\fp_s),16D^s))}\int_{B(\pc(\fp_s),16D^s)}P_{\mathcal{J}(\fT(\fu))}|f(y)|\,\mathrm{d}\mu(y)\,. $$ - Since $L \in \mathcal{L}(\fT(\fu))$, we have $s(L) \le \ps(\fp)$ for all $\fp \in \fT(\fu)$. Since $x\in L \cap \scI(\fp_s)$, it follows by \eqref{dyadicproperty} that $L \subset \scI(\fp_s)$, in particular $x' \in \scI(\fp_s) \subset B(\pc(\fp_s), 16D^s)$. Thus + Since $L \in \mathcal{L}(\fT(\fu))$ and $x\in L \cap \scI(\fp_s)$, we have $s(L) \le \ps(\fp_s)$. It follows by \eqref{dyadicproperty} that $L \subset \scI(\fp_s)$, in particular $x' \in \scI(\fp_s) \subset B(\pc(\fp_s), 16D^s)$. Thus $$ - \le 2^{104a^3} \sum_{s\in\sigma(x)}2^{s - \overline{\sigma}(\fu, x)} M_{\mathcal{B}, 1}P_{\mathcal{J}(\fT(\fu))}|f|(x') + \le 5\cdot 2^{104a^3} \sum_{s\in\sigma(x)}2^{s - \overline{\sigma}(\fu, x)} M_{\mathcal{B}, 1}P_{\mathcal{J}(\fT(\fu))}|f|(x') $$ $$ - \le 2^{105a^3} M_{\mathcal{B}, 1}P_{\mathcal{J}(\fT(\fu))}|f|(x')\,. + \le 10\cdot 2^{104a^3} M_{\mathcal{B}, 1}P_{\mathcal{J}(\fT(\fu))}|f|(x')\,. $$ This completes the estimate for term \eqref{eq-term-A}. \end{proof}