Lemma 7.5.11 (#238)

[[blueprint]](https://florisvandoorn.com/carleson/blueprint/treesection.html#lower-oscillation-bound)

The proof is ready, can be merged.

### TODOs

- [x] add `\leanok`
- [x] refactor

Author: lakesare

Carleson/Calculations.lean

@@ -171,6 +171,84 @@ lemma calculation_9 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G]
   apply (Real.rpow_le_rpow_left_iff (x := 2) (by linarith)).mp
   linarith
 
+lemma calculation_11 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (s : ℤ) :
+    100 * (D : ℝ) ^ (s + 2) + 4 * D ^ (s + 1) < 128 * D^(s + 2) := by
+  rw [show (128 : ℝ) = 100 + 28 by norm_num]
+  rw [right_distrib]
+  gcongr
+  · linarith
+  · exact one_lt_D (X := X)
+  · linarith
+
+lemma calculation_12 (s : ℝ) :
+    128 * (D : ℝ)^(s + 2) = 2^(200 * a ^ 2 + 4) * (8 * D ^ s) := by
+  simp only [defaultD]
+  have leftSide := calc 128 * ((2 : ℝ) ^ (100 * a ^ 2)) ^ (s + 2)
+    _ = 128 * 2^(100 * a^2 * (s + 2)) := by
+      congrm 128 * ?_
+      have fact := Real.rpow_mul (x := 2) (y := 100 * a ^ 2) (z := s + 2) (by positivity)
+      rw_mod_cast [fact]
+    _ = 128 * 2^((100 * a^2 * s) + (100 * a^2 * 2)) := by
+      congrm 128 * (2 ^ ?_)
+      ring
+    _ = (2 ^ 7) * 2^((100 * a^2 * s) + (100 * a^2 * 2)) := by
+      norm_num
+    _ = 2 ^ (7 + ((100 * a^2 * s) + (100 * a^2 * 2))) := by
+      have fact := Real.rpow_add (x := 2) (y := 7) (z := 100 * a^2 * s + 100 * a^2 * 2) (by positivity)
+      rw_mod_cast [fact]
+  have rightSide := calc 2 ^ (200 * a ^ 2 + 4) * (8 * ((2 : ℝ) ^ (100 * a ^ 2)) ^ s)
+    _ = 2 ^ (200*a^2 + 4) * ((2^3)*((2 ^ (100 * a ^ 2)) ^ s)) := by
+      norm_num
+    _ = 2 ^ (200*a^2 + 4) * (  2^3   *   2 ^ (100 * a ^ 2 * s)  ) := by
+      rw [Real.rpow_mul (x:=2) (by positivity)]
+      norm_cast
+    _ = 2 ^ (200*a^2 + 4) * 2 ^ (3    +   100 * a ^ 2 * s) := by
+      have fact := Real.rpow_add (x:=2) (y:= 3) (z:= 100 * a ^ 2 * s) (by positivity)
+      rw_mod_cast [fact]
+    _ = 2^(     200*a^2 + 4           +      (3    +   100 * a ^ 2 * s)  ) := by
+      have fact := Real.rpow_add (x:=2) (y:= 200*a^2 + 4) (z:= 3    +   100 * a ^ 2 * s) (by positivity)
+      nth_rw 2 [Real.rpow_add]
+      norm_cast
+      positivity
+    _ = 2^(7 + ((100 * a^2 * s) + (100 * a^2 * 2))) := by
+      congrm 2 ^ ?_
+      linarith
+  rw_mod_cast [leftSide]
+  rw_mod_cast [rightSide]
+
+lemma calculation_13 : (2 : ℝ) ^ (200 * (a^3) + 4*a) = (defaultA a) ^ (200*a^2 + 4) := by
+  simp only [defaultA, Nat.cast_pow, Nat.cast_ofNat]
+  have fact := Real.rpow_mul (x := 2) (y := a) (z := 200 * a ^ 2 + 4) (by positivity)
+  rw_mod_cast [← fact]
+  ring
+
+lemma calculation_14 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (n: ℕ) : 
+    (2 : ℝ) ^ ((Z : ℝ) * n / 2 - 201 * a ^ 3) ≤ 2 ^ ((Z : ℝ) * n / 2 - (200 * a ^ 3 + 4 * a)) := by
+  gcongr
+  · linarith
+  rw [show 201 * (a : ℝ) ^ 3 = 200 * (a : ℝ) ^ 3 + a ^ 3 by ring]
+  gcongr 200 * (a : ℝ) ^ 3 + ?_
+  rw [show (a : ℝ) ^ 3 = a ^ 2 * a by ring]
+  gcongr
+  suffices 4 ^ 2 ≤ (a : ℝ) ^ 2 by linarith
+  apply pow_le_pow_left₀ (ha := by linarith)
+  exact_mod_cast four_le_a X
+
+lemma calculation_15 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G]
+    (dist: ℝ) (zon : ℝ)
+    (h : 2 ^ zon ≤ 2 ^ (200 * a ^ 3 + 4 * a) * dist) :
+    2 ^ (zon - (200 * a^3 + 4*a)) ≤ dist := by
+  rw [Real.rpow_sub (hx := by linarith)]
+  rw [show dist = 2 ^ (200 * a ^ 3 + 4 * a) * dist / 2 ^ (200 * a ^ 3 + 4 * a) by simp]
+  have := (div_le_div_iff_of_pos_right (c := 2 ^ (200 * a ^ 3 + 4 * a)) (hc := by have aIsBig := four_le_a X; positivity)).mpr h
+  exact_mod_cast this
+
+lemma calculation_16 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (s: ℤ) :
+    4 * (D : ℝ) ^ s < 100 * D ^ (s + 1) := by
+  gcongr
+  · linarith
+  · exact one_lt_D (X := X)
+  · linarith
 
 lemma calculation_7_7_4 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {n : ℕ}:
   (1:ℝ) ≤ 2 ^ (Z * (n + 1)) - 4 := by
@@ -188,3 +266,4 @@ lemma calculation_7_7_4 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G]
     · norm_num
     omega
   exact Nat.mul_le_mul this (Nat.le_add_left 1 n)
+

Carleson/ForestOperator/LargeSeparation.lean

@@ -49,6 +49,14 @@ lemma IF_subset_THEN_distance_between_centers (subset : (J : Set X) ⊆ J') :
   apply Grid_subset_ball
   exact (subset (Grid.c_mem_Grid))
 
+lemma IF_subset_THEN_not_disjoint {A : Grid X} {B: Grid X} (h : (A : Set X) ⊆ B) :
+    ¬ Disjoint (B : Set X) (A : Set X) := by
+  rw [disjoint_comm]
+  intro disjoint
+  have nonempty := Grid.nonempty A
+  rw [← Mathlib.Tactic.PushNeg.empty_ne_eq_nonempty] at nonempty
+  exact nonempty (Eq.symm ((Set.disjoint_of_subset_iff_left_eq_empty h).mp disjoint))
+
 lemma IF_disjoint_with_ball_THEN_distance_bigger_than_radius {J : X} {r : ℝ} {pSet : Set X} {p : X}
     (belongs : p ∈ pSet) (h : Disjoint (Metric.ball J r) pSet) :
     dist J p ≥ r := by
@@ -121,15 +129,9 @@ lemma union_𝓙₅ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u
         _ ⊆ ball (c cube) (4 * D ^ s cube) := by
           exact Grid_subset_ball (i := cube)
         _ ⊆ ball (c cube) (100 * D ^ (s cube + 1)) := by
-          unfold ball
           intro y xy
-          rw [mem_setOf_eq] at xy ⊢
-          have numbers : 4 * (D : ℝ) ^ s cube < 100 * D ^ (s cube + 1) := by
-            gcongr
-            linarith
-            exact one_lt_D (X := X)
-            linarith
-          exact gt_trans numbers xy
+          rw [ball, mem_setOf_eq] at xy ⊢
+          exact gt_trans (calculation_16 (X := X) (s := s cube)) xy
       have black : ¬↑(𝓘 p) ⊆ ball (c cube) (100 * D ^ (s cube + 1)) := by
         have in_𝔖₀ := 𝔗_subset_𝔖₀ (hu₁ := hu₁) (hu₂ := hu₂) (hu := hu) (h2u := h2u)
         rw [subset_def] at in_𝔖₀
@@ -1069,7 +1071,82 @@ irreducible_def C7_5_11 (a n : ℕ) : ℝ≥0 := 2 ^ (Z * n / 2 - 201 * (a : ℝ
 lemma lower_oscillation_bound (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
     (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) :
     C7_5_11 a n ≤ dist_{c J, 8 * D ^ s J} (𝒬 u₁) (𝒬 u₂) := by
-  sorry
+  have existsBiggerThanJ : ∃ (J' : Grid X), J ≤ J' ∧ s J' = s J + 1 := by
+    apply Grid.exists_scale_succ
+    obtain ⟨⟨Jin𝓙₀, _⟩, ⟨jIsSubset : (J : Set X) ⊆ 𝓘 u₁, smaller : s J ≤ s (𝓘 u₁)⟩⟩ := hJ
+    obtain ⟨p, belongs⟩ := t.nonempty' hu₁
+    apply lt_of_le_of_ne smaller
+    by_contra! h
+    have u₁In𝓙₀ : 𝓘 u₁ ∈ 𝓙₀ (t.𝔖₀ u₁ u₂) := by
+      apply mem_of_eq_of_mem (h := Jin𝓙₀)
+      rw [eq_comm]
+      apply (eq_or_disjoint h).resolve_right
+      have notDisjoint := IF_subset_THEN_not_disjoint jIsSubset
+      rw [disjoint_comm] at notDisjoint
+      exact notDisjoint
+    cases u₁In𝓙₀ with
+    | inl min =>
+      have sameScale : s (𝓘 p) = s (𝓘 u₁) := by
+        linarith [
+          (scale_mem_Icc (i := 𝓘 p)).left,
+          show s (𝓘 p) ≤ s (𝓘 u₁) by exact (𝓘_le_𝓘 t hu₁ belongs).2
+        ]
+      suffices s (𝓘 u₁) > s (𝓘 p) by linarith
+      by_contra! smaller
+      have pIsSubset := (𝓘_le_𝓘 t hu₁ belongs).1
+      apply HasSubset.Subset.not_ssubset ((fundamental_dyadic smaller).resolve_right (IF_subset_THEN_not_disjoint pIsSubset))
+      apply HasSubset.Subset.ssubset_of_ne pIsSubset
+      by_contra! sameSet
+      apply Forest.𝓘_ne_𝓘 (hu := hu₁) (hp := belongs)
+      exact Grid.inj (Prod.ext sameSet sameScale)
+    | inr avoidance =>
+      have pIn𝔖₀ : p ∈ t.𝔖₀ u₁ u₂ := 𝔗_subset_𝔖₀ (hu₁ := hu₁) (hu₂ := hu₂) (hu := hu) (h2u := h2u) belongs
+      apply avoidance p pIn𝔖₀
+      calc (𝓘 p : Set X)
+      _ ⊆ 𝓘 u₁ := (𝓘_le_𝓘 t hu₁ belongs).1
+      _ ⊆ ball (c (𝓘 u₁)) (4 * D ^ s (𝓘 u₁)) := by
+        exact Grid_subset_ball
+      _ ⊆ ball (c (𝓘 u₁)) (100 * D ^ (s (𝓘 u₁) + 1)) := by
+        intro x hx
+        exact gt_trans (calculation_16 (X := X) (s := s (𝓘 u₁))) hx
+  rcases existsBiggerThanJ with ⟨J', JleJ', scaleSmaller⟩
+  have notIn𝓙₀ : J' ∉ 𝓙₀ (t.𝔖₀ u₁ u₂) := by
+    apply bigger_than_𝓙_is_not_in_𝓙₀ (sle := by linarith) (le := JleJ')
+    exact mem_of_mem_inter_left hJ
+  unfold 𝓙₀ at notIn𝓙₀
+  simp only [mem_setOf_eq, not_or, not_forall, Classical.not_imp, Decidable.not_not] at notIn𝓙₀
+  push_neg at notIn𝓙₀
+  obtain ⟨_, ⟨ p, pIn, pSubset ⟩⟩ := notIn𝓙₀
+  have thus :=
+    calc 2 ^ ((Z : ℝ) * n / 2)
+    _ ≤ dist_{𝔠 p, D ^ 𝔰 p / 4} (𝒬 u₁) (𝒬 u₂) := pIn.2
+    _ ≤ dist_{c J, 128 * D^(s J + 2)} (𝒬 u₁) (𝒬 u₂) := by
+      apply cdist_mono
+      intro point pointIn
+      calc dist point (c J)
+      _ ≤ dist point (c J') + dist (c J') (c J) := dist_triangle ..
+      _ ≤ 100 * D ^ (s J' + 1) + dist (c J') (c J) := by
+        rw [ball, Set.subset_def] at pSubset
+        have := pSubset point (ball_subset_Grid pointIn)
+        rw [mem_setOf_eq] at this
+        gcongr
+      _ ≤ 100 * D ^ (s J' + 1) + 4 * D ^ (s J') := by
+        have : dist (c J) (c J') < 4 * D ^ (s J') := IF_subset_THEN_distance_between_centers (subset := JleJ'.1)
+        rw [dist_comm] at this
+        gcongr
+      _ = 100 * D ^ (s J + 2) + 4 * D ^ (s J + 1) := by
+        rw [scaleSmaller, add_assoc, show (1 : ℤ) + 1 = 2 by rfl]
+      _ < 128 * D^(s J + 2) := by
+        exact calculation_11 (s J) (X := X)
+    _ ≤ 2 ^ (200 * (a^3) + 4 * a) * dist_{c J, 8 * D ^ s J} (𝒬 u₁) (𝒬 u₂) := by
+      rw [show 128 * (D : ℝ)^(s J + 2) = 2^(200*a^2 + 4) * (8*D^(s J)) by exact_mod_cast calculation_12 (s := s J)]
+      rw [calculation_13]
+      apply cdist_le_iterate
+      have := defaultD_pos a
+      positivity
+  rw [C7_5_11]
+  push_cast
+  linarith [calculation_14 (X := X) (n := n), calculation_15 (X := X) (h := thus)]
 
 /-- The constant used in `correlation_distant_tree_parts`.
 Has value `2 ^ (541 * a ^ 3 - Z * n / (4 * a ^ 2 + 2 * a ^ 3))` in the blueprint. -/

blueprint/src/chapter/main.tex

@@ -5676,6 +5676,7 @@ \subsection{The van der Corput estimate}
     \end{lemma}
 
     \begin{proof}
+    \leanok
     Since $\emptyset \ne \fT(\fu_1) \subset \mathfrak{S}$ by \Cref{overlap-implies-distance}, there exists at least one tile $\fp \in \mathcal{S}$ with $\scI(\fp) \subsetneq \scI(\fu_1)$. Thus $\scI(\fu_1) \notin \mathcal{J}'$, so $J \subsetneq \scI(\fu_1)$. Thus there exists a cube $J' \in \mathcal{D}$ with $J \subset J'$ and $s(J') = s(J) + 1$, by \eqref{coverdyadic} and \eqref{dyadicproperty}. By definition of $\mathcal{J'}$ and the triangle inequality, there exists $\fp \in \mathfrak{S}$ such that
     $$
         \scI(\fp) \subset B(c(J'), 100 D^{s(J') + 1}) \subset B(c(J), 128 D^{s(J)+2})\,.