TileStructure.Forest.pointwise_tree_estimate

lemma pointwise_tree_estimate (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L)    (hf : BoundedCompactSupport f) :    ‖carlesonSum (t u) (fun y ↦ exp (.I * - 𝒬 u y) * f y) x‖ₑ ≤    C7_1_3 a * (maximalFunction volume 𝓑 c𝓑 r𝓑 1 (approxOnCube (𝓙 (t u)) (‖f ·‖)) x' +    t.boundaryOperator u (approxOnCube (𝓙 (t u)) (‖f ·‖)) x') +    nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 (t u)) f) x' := by  set g := approxOnCube (𝓙 (t u)) f  -- Convert the sum over `p` into a sum over `s`.  unfold carlesonSum carlesonOn  rw [p_sum_eq_s_sum fun s x ↦ ∫ (y : X), cexp (I * (Q x y - Q x x)) * Ks s x y *        (fun y ↦ cexp (I * -𝒬 u y) * f y) y]  -- Next introduce an extra factor of `‖cexp (I * 𝒬 u x)‖ₑ`, i.e., 1. Then simplify.  have : 1 = ‖cexp (I * 𝒬 u x)‖ₑ := by simp  rw [← one_mul ‖_‖ₑ, this, ← enorm_mul, Finset.mul_sum]  have : ∑ i ∈ t.σ u x, cexp (I * 𝒬 u x) * ∫ (y : X), (cexp (I * (Q x y - Q x x)) * Ks i x y *            (cexp (I * -𝒬 u y) * f y)) =          ∑ i ∈ t.σ u x, ∫ (y : X),            (f y * ((exp (I * (- 𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1) * Ks i x y) +            (f y - g y) * Ks i x y + g y * Ks i x y) := by    simp_rw [Ks, mul_sub, mul_add, sub_eq_add_neg, exp_add]    apply Finset.sum_congr rfl    intro _ _    apply (integral_const_mul ..).symm.trans    apply integral_congr_ae    exact (funext fun y ↦ by ring).eventuallyEq  rw [this]  -- It suffices to show that the integral splits into the three terms bounded by Lemmas 7.1.4-6  suffices ∑ i ∈ t.σ u x, ∫ (y : X),             (f y * ((cexp (I * (-𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1) * Ks i x y)) +             (f y - g y) * Ks i x y + g y * Ks i x y =           ∑ i ∈ t.σ u x,             ((∫ (y : X), f y * ((cexp (I * (-𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1) * Ks i x y)) +             (∫ (y : X), (f y - g y) * Ks i x y) + (∫ (y : X), g y * Ks i x y)) by    -- Separate the LHS into three pieces    rw [this, Finset.sum_add_distrib, Finset.sum_add_distrib]    apply le_trans <| ENNReal.coe_strictMono.monotone <| (nnnorm_add_le _ _).trans      (add_le_add_left (nnnorm_add_le _ _) _)    rw [ENNReal.coe_add, ENNReal.coe_add, mul_add]    -- Apply Lemmas 7.1.4, 7.1.5, and 7.1.6    simp_rw [← mul_comm (Ks _ x _)]    refine add_le_add_three ?_ ?_ (second_tree_pointwise hu hL hx hx')    · simp_rw [mul_comm (Ks _ x _), mul_comm (f _)]      have h : C7_1_3 a ≥ C7_1_4 a := C7_1_4_le_C7_1_3 (four_le_a X)      exact (first_tree_pointwise hu hL hx hx' hf).trans <| mul_left_mono (by exact_mod_cast h)    · have h : C7_1_3 a ≥ C7_1_6 a := C7_1_6_le_C7_1_3      exact (third_tree_pointwise hu hL hx hx' hf).trans <| mul_left_mono (by exact_mod_cast h)  -- In order to split the integral, we will first need some trivial integrability results  have h1 {i : ℤ} : Integrable (fun y ↦ approxOnCube (𝓙 (t.𝔗 u)) f y * Ks i x y) := by    classical    apply (integrable_Ks_x <| one_lt_realD (K := K)).bdd_mul      (c := ∑ J with J ∈ 𝓙 (t u), ‖⨍ y in J, f y‖)    · exact (stronglyMeasurable_approxOnCube _ _).aestronglyMeasurable    · refine ae_of_all _ fun x ↦ (norm_sum_le _ _).trans <| Finset.sum_le_sum (fun J hJ ↦ ?_)      by_cases h : x ∈ (J : Set X)      · rw [Set.indicator_of_mem h]      · rw [Set.indicator_apply, if_neg h, norm_zero]        exact norm_nonneg _  have : ∀ (y : X), ‖cexp (I * (-𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1‖ ≤ 2 := by    refine fun y ↦ le_of_le_of_eq (norm_sub_le _ _) ?_    norm_cast    rw [mul_comm, norm_exp_ofReal_mul_I, one_add_one_eq_two]  have h2 {i : ℤ} : Integrable      (fun y ↦ f y * ((cexp (I * (-𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1) * Ks i x y)) :=    hf.integrable_mul <| (integrable_Ks_x <| one_lt_realD (K := K)).bdd_mul (c := 2)      (Measurable.aestronglyMeasurable (by fun_prop)) (ae_of_all _ this)  have h3 {i : ℤ} : Integrable (fun y ↦ (f y - approxOnCube (𝓙 (t.𝔗 u)) f y) * Ks i x y) := by    simp_rw [sub_mul]    exact hf.integrable_mul (integrable_Ks_x <| one_lt_realD (K := K)) |>.sub h1  exact Finset.fold_congr fun i _ ↦ (by rw [integral_add _ h1, integral_add h2 h3]; exact h2.add h3)