TileStructure.Forest.second_tree_pointwise

lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L) :    ‖∑ i ∈ 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_univ] at 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 ▸ 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_univ] at 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'  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 <| by        gcongr; exacts [one_le_realD _, s_ineq]    have i2 : dist (𝔠 p') (𝔠 p) < 4 * D ^ 𝔰 p' :=      mem_ball'.mp (ball_subset_Grid.trans (Grid.le_def.mp pinc).1 |>.trans Grid_subset_ball <|        mem_ball_self (by unfold defaultD; positivity))    calc      _ ≤ dist_{𝔠 p, 8 * D ^ 𝔰 p'} (𝒬 u) (Q x) := by        refine cdist_mono (ball_subset_ball' ?_); rw [← sp']        calc          _ ≤ (D : ℝ) ^ 𝔰 p' + 4 * D ^ 𝔰 p' := add_le_add_right i1.le _          _ = 5 * D ^ 𝔰 p' := by ring          _ ≤ _ := by gcongr; norm_num      _ ≤ defaultA a * dist_{𝔠 p', 4 * D ^ 𝔰 p'} (𝒬 u) (Q x) := by        convert cdist_le (x₂ := 𝔠 p) _ using 1        · exact dist_congr rfl (by ring)        · apply i2.trans_le; nth_rw 1 [← one_mul (4 * _)]; gcongr; exact one_le_two      _ ≤ defaultA a ^ 5 * dist_(p') (𝒬 u) (Q x) := by        rw [pow_succ', mul_assoc]; gcongr        convert! cdist_le_iterate _ (𝒬 u) (Q x) 4 using 1        · exact dist_congr rfl (by ring)        · unfold defaultD; positivity      _ < _ := by rw [mul_comm]; gcongr  have d1 : dist_{x, D ^ (s₂ - 1)} (𝒬 u) (Q x) < 1 := by    calc      _ ≤ dist_{x, D ^ s₂} (𝒬 u) (Q x) * 2 ^ (-𝕔 * a : ℤ) := by        rw [neg_mul, zpow_neg, le_mul_inv_iff₀ (by positivity), mul_comm]        convert! le_cdist_iterate _ (𝒬 u) (Q x) (𝕔 * a) using 1        · apply dist_congr rfl          rw [Nat.cast_pow, ← pow_mul, show a * (𝕔 * a) = 𝕔 * a ^ 2 by ring, ← Nat.cast_pow]          change _ = (D : ℝ) * _          rw [← zpow_one_add₀ (realD_pos _).ne', add_sub_cancel]        · unfold defaultD; positivity      _ < 5 * defaultA a ^ 5 * 2 ^ (-𝕔 * a : ℤ) := by gcongr      _ = 5 * (2 : ℝ) ^ (-(𝕔 - 5) * a : ℤ) := by        rw [Nat.cast_pow, ← pow_mul, ← zpow_natCast, show (2 : ℕ) = (2 : ℝ) by rfl, mul_assoc,          ← zpow_add₀ two_ne_zero]        congr        simp        ring      _ ≤ 5 * 2 ^ (-3 : ℤ) := by        gcongr        · exact one_le_two        · simp only [neg_sub, sub_mul, Int.reduceNeg, tsub_le_iff_right, le_neg_add_iff_add_le]          norm_cast          calc          3 + 5 * a          _ ≤ a + 5 * a := by gcongr; linarith [four_le_a X]          _ = 6 * a := by ring          _ ≤ 𝕔 * a := by gcongr; linarith [seven_le_c]      _ < _ := by norm_num  have x'p : x' ∈ 𝓘 p := (Grid.le_def.mp Lle).1 hx'  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 ?_ ?_  · apply le_upperRadius; convert! d1  · 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⟩