TileStructure.Forest.first_tree_pointwise

lemma first_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L)    (hf : BoundedCompactSupport f) :    ‖∑ i ∈ 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 * maximalFunction volume 𝓑 c𝓑 r𝓑 1 (approxOnCube (𝓙 (t u)) (‖f ·‖)) x' := by  let _ : MulPosReflectLE ℝ := inferInstance -- perf: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/performance.20example.20with.20type-class.20inference  let _ : PosMulReflectLE ℝ := inferInstance -- perf: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/performance.20example.20with.20type-class.20inference  set g := approxOnCube (𝓙 (t u)) (‖f ·‖)  let q (y) := -𝒬 u y + Q x y + 𝒬 u x - Q x x  rcases (t.σ u x).eq_empty_or_nonempty with hσ | hσ; · simp [hσ]  have : ∀ s ∈ t.σ u x, ‖∫ y, (cexp (I * (q y)) - 1) * Ks s x y * f y‖ₑ ≤      ∫⁻ y, ‖(exp (I * q y) - 1) * Ks s x y * f y‖ₑ := fun s hs ↦    (enorm_integral_le_lintegral_enorm _).trans (by simp)  conv_lhs =>    enter [1, 2, s, 2, y]    rw [← Complex.ofReal_neg, ← Complex.ofReal_add, ← Complex.ofReal_add, ← Complex.ofReal_sub]  refine (enorm_sum_le _ _).trans <| ((t.σ u x).sum_le_sum this).trans ?_  suffices ∀ s ∈ t.σ u x, ∫⁻ y, ‖(exp (I * q y) - 1) * Ks s x y * f y‖ₑ ≤      (5 * 2 ^ ((𝕔 + 4) * a ^ 3) * maximalFunction volume 𝓑 c𝓑 r𝓑 1 g x')      * 2 ^ (s - t.σMax u x hσ) by    apply ((t.σ u x).sum_le_sum this).trans    rw [← Finset.mul_sum]    apply le_trans <| mul_le_mul_right (L7_1_4_sum hσ) _    rw [mul_comm _ 2, ← mul_assoc, ← mul_assoc, C7_1_4]    gcongr; norm_num  intro s hs  have eq1 : ∫⁻ y, ‖(exp (I * q y) - 1) * Ks s x y * f y‖ₑ =      ∫⁻ y in ball x (D ^ s / 2), ‖(exp (I * q y) - 1) * Ks s x y * f y‖ₑ := by    rw [← lintegral_indicator measurableSet_ball]; congr! 2 with y    symm; rw [indicator_apply_eq_self]; intro my    suffices Ks s x y = 0 by simp [this]    contrapose! my; apply dist_mem_Ioo_of_Ks_ne_zero at my    rw [mem_Ioo] at my; rw [mem_ball']; exact my.2  have eq2 : ∫⁻ y in ball x (D ^ s / 2), ‖(exp (I * q y) - 1) * Ks s x y * f y‖ₑ ≤      5 * 2 ^ (s - σMax t u x ⟨s, hs⟩) * (2 ^ ((𝕔 + 3) * a ^ 3) / volume (ball x (D ^ s))) *      ∫⁻ y in ball x (D ^ s / 2), ‖f y‖ₑ := by    convert! (lintegral_mono (L7_1_4_integrand_bound f hu hs)).trans ?_    · norm_cast    · rw [lintegral_const_mul'' _ hf.aestronglyMeasurable.enorm.restrict]  apply le_of_eq_of_le eq1 ∘ eq2.trans  rw [← mul_rotate _ (5 * 2 ^ ((𝕔 + 4) * a ^ 3)), ← mul_assoc, mul_comm _ 5]  simp_rw [mul_assoc]; gcongr _ * (_ * ?_)  rw [show (𝕔 + 4) * a ^ 3 = (𝕔 + 3) * a ^ 3 + a ^ 3 by ring, pow_add, mul_assoc,    ENNReal.mul_comm_div]  gcongr  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) := by    apply ball_subset_ball'    calc      _ ≤ (16 : ℝ) * D ^ s + 4 * D ^ 𝔰 pₛ :=        add_le_add_right (mem_ball'.mp (Grid_subset_ball xpₛ.1)).le _      _ = 16 * D ^ s + 4 * D ^ s := by nth_rw 3 [← hpₛ]      _ ≤ _ := by linarith only [defaultD_pow_pos a s]  calc  _ ≤ 2 ^ (5 * a) * ((∫⁻ y in ball x (D ^ s / 2), ‖f y‖ₑ) / volume (ball (𝔠 pₛ) (16 * D ^ s))) := by    rw [mul_comm, ENNReal.div_mul _ (.inr (by positivity)) (.inr (by finiteness))]; gcongr    refine ENNReal.div_le_of_le_mul' ((measure_mono ball_subset).trans ?_)    convert! measure_ball_two_le_same_iterate (μ := volume) x (D ^ s) 5 using 2    simp [mul_comm 5 a, pow_mul]  _ ≤ _ := by    gcongr ?_ * ?_    · apply pow_right_mono₀ one_le_two      rw [pow_succ a 2, mul_le_mul_iff_left₀ (a_pos X)]      nlinarith [four_le_a X]    · refine le_trans ?_ (L7_1_4_laverage_le_MB hL hx hx' g pₛu xpₛ)      rw [hpₛ]; gcongr ?_ / _      rw [← hpₛ]; exact L7_1_4_integral_le_integral hu hf pₛu xpₛ