enorm_carlesonOperatorIntegrand_le_T_S

lemma enorm_carlesonOperatorIntegrand_le_T_S {R₁ R₂ : ℝ} (hR₁ : 0 < R₁) (hR₂ : R₁ < R₂)    (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1) {x : X} :    ‖carlesonOperatorIntegrand K (Q x) R₁ R₂ f x‖ₑ ≤    ‖T_S Q (L302 a R₁) (U302 a R₂) f x‖ₑ +    4 * C2_1_3 a * globalMaximalFunction volume 1 (F.indicator (1 : X → ℝ)) x := by  have Dg1 := one_lt_realD X  let BR := Finset.Icc (L302 a R₁ - 2) (U302 a R₂ + 2) -- big range  let SR := Finset.Icc (L302 a R₁) (U302 a R₂) -- small range  calc    _ = ‖∫ y in Annulus.oo x R₁ R₂, ∑ s ∈ BR, Ks s x y * f y * exp (I * Q x y)‖ₑ := by      unfold carlesonOperatorIntegrand; congr 1      refine setIntegral_congr_fun Annulus.measurableSet_oo fun y my ↦ ?_      have dpos : 0 < dist x y := by rw [Annulus.oo, mem_setOf_eq] at my; exact hR₁.trans my.1      simp_rw [← Finset.sum_mul]; congr      refine (sum_Ks (Finset.Icc_subset_Icc ?_ ?_) Dg1 dpos).symm      · rw [L302, add_sub_assoc, show (3 : ℤ) - 2 = 1 by norm_num, add_comm 1, Int.floor_add_one]        gcongr; exact my.1.le      · rw [U302, sub_add_cancel]; gcongr; exact my.2.le    _ = ‖∑ s ∈ BR, ∫ y in Annulus.oo x R₁ R₂, Ks s x y * f y * exp (I * Q x y)‖ₑ := by      congr 1; refine integral_finsetSum _ fun s ms ↦ ?_      simp_rw [mul_rotate _ (f _)]; refine ((integrable_Ks_x Dg1).bdd_mul (c := 1) ?_ ?_).restrict      · rw [aestronglyMeasurable_iff_aemeasurable]        exact (mf.mul ((Complex.measurable_ofReal.comp (measurable_Q₁ _))          |>.const_mul I).cexp).aemeasurable      · simp_rw [norm_mul, norm_exp_I_mul_ofReal, mul_one]        exact ae_of_all _ fun y ↦ (nf y).trans (indicator_one_le_one y)    _ ≤ ‖∑ s ∈ SR, ∫ y in Annulus.oo x R₁ R₂, Ks s x y * f y * exp (I * Q x y)‖ₑ +        ‖∑ s ∈ BR \ SR, ∫ y in Annulus.oo x R₁ R₂, Ks s x y * f y * exp (I * Q x y)‖ₑ := by      have : SR ⊆ BR := Finset.Icc_subset_Icc (by lia) (by lia)      rw [← Finset.inter_eq_right] at this      rw [← Finset.sum_inter_add_sum_sdiff BR SR, this]      exact enorm_add_le _ _    _ = ‖T_S Q (L302 a R₁) (U302 a R₂) f x‖ₑ +        ‖∑ s ∈ BR \ SR, ∫ y in Annulus.oo x R₁ R₂, Ks s x y * f y * exp (I * Q x y)‖ₑ := by      unfold SR T_S; congr! 3 with s ms; rw [Finset.mem_Icc] at ms      refine setIntegral_eq_integral_of_forall_compl_eq_zero fun y ny ↦ ?_      suffices Ks s x y = 0 by simp_rw [this, zero_mul]      contrapose! ny; replace ny := dist_mem_Ioo_of_Ks_ne_zero ny      rw [Annulus.oo, mem_setOf_eq]; refine mem_of_mem_of_subset ny (Ioo_subset_Ioo ?_ ?_)      · apply R₁_le_D_zpow_div_four (X := X).trans; gcongr; exacts [Dg1.le, ms.1]      · refine le_trans ?_ (D_zpow_div_two_le_R₂ (X := X) (hR₁.trans hR₂))        gcongr; exacts [Dg1.le, ms.2]    _ ≤ ‖T_S Q (L302 a R₁) (U302 a R₂) f x‖ₑ +        ∑ s ∈ BR \ SR, ‖∫ y in Annulus.oo x R₁ R₂, Ks s x y * f y * exp (I * Q x y)‖ₑ := by      gcongr; exact enorm_sum_le _ _    _ ≤ ‖T_S Q (L302 a R₁) (U302 a R₂) f x‖ₑ + ∑ s ∈ edgeScales a R₁ R₂,        ‖∫ y in Annulus.oo x R₁ R₂, Ks s x y * f y * exp (I * Q x y)‖ₑ := by      gcongr; exact diff_subset_edgeScales    _ ≤ ‖T_S Q (L302 a R₁) (U302 a R₂) f x‖ₑ + ∑ s ∈ edgeScales a R₁ R₂,        C2_1_3 a * globalMaximalFunction volume 1 (F.indicator (1 : X → ℝ)) x := by      gcongr with s ms; rw [← Finset.mem_coe] at ms; exact enorm_setIntegral_annulus_le nf    _ ≤ _ := by      rw [Finset.sum_const, nsmul_eq_mul, ← mul_assoc]; gcongr; exact_mod_cast Finset.card_le_four