R_truncation

lemma R_truncation (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')    (mF : MeasurableSet F) (mG : MeasurableSet G) (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1)    {n : ℕ} {R : ℝ} (hR : R = 2 ^ n)    (BST_T_Q : ∀ θ : Θ X, HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·)      2 2 volume volume (C_Ts a)) :    ∫⁻ x in G, ⨆ R₁ ∈ Ioo R⁻¹ R, ⨆ R₂ ∈ Ioo R₁ R, ‖T_R K Q R₁ R₂ R f x‖ₑ ≤    C1_0_2 a q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by  wlog sG : G ⊆ ball o R generalizing G  · calc      _ = _ := by        rw [← inter_comm, ← setLIntegral_indicator measurableSet_ball]        refine lintegral_congr fun x ↦ ?_        symm; rw [indicator_apply_eq_self]; intro nx        simp_rw [T_R, indicator_of_notMem nx, enorm_zero, iSup_zero]      _ ≤ _ := @this (G ∩ ball o R) (mG.inter measurableSet_ball) inter_subset_right      _ ≤ _ := by gcongr; exact inter_subset_left  wlog sF : F ⊆ ball o (2 * R) generalizing F f  · have nf' : (‖(ball o (2 * R)).indicator f ·‖) ≤ (F ∩ ball o (2 * R)).indicator 1 := fun x ↦ by      rw [inter_comm, ← indicator_indicator]      by_cases hx : x ∈ ball o (2 * R)      · simp_rw [indicator_of_mem hx]; exact nf x      · simp_rw [indicator_of_notMem hx]; simp    calc      _ = _ := by        refine setLIntegral_congr_fun mG fun x mx ↦ ?_        unfold T_R carlesonOperatorIntegrand; congr! 7 with R₁ mR₁ R₂ mR₂ x'        simp_rw [indicator_of_mem (sG mx)]        refine setIntegral_congr_fun Annulus.measurableSet_oo fun y my ↦ ?_        congr 2; symm; rw [indicator_apply_eq_self]; apply absurd        specialize sG mx; rw [Annulus.oo, mem_setOf_eq] at my; rw [mem_ball] at sG ⊢        calc          _ ≤ dist x y + dist x o := dist_triangle_left ..          _ < R₂ + R := add_lt_add my.2 sG          _ < _ := by rw [two_mul]; exact add_lt_add_left mR₂.2 _      _ ≤ _ :=        this (mF.inter measurableSet_ball) (mf.indicator measurableSet_ball) nf' inter_subset_right      _ ≤ _ := by gcongr; exact inter_subset_left  exact R_truncation' hq hqq' mF mG mf nf hR sF sG BST_T_Q