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) (sF : F ⊆ ball o (2 * R)) (sG : G ⊆ ball o R)    (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  have Rpos : 0 < R := by rw [hR]; positivity  have iRpos : 0 < R⁻¹ := by rw [hR]; positivity  obtain ⟨B, hB⟩ := exists_uniform_annulus_bound (X := X) Rpos  calc    _ = ∫⁻ x in G, ⨆ R₁ ∈ Ioo R⁻¹ R, ⨆ R₂ ∈ Ioo R₁ R,        ‖carlesonOperatorIntegrand K (Q x) R₁ R₂ f x‖ₑ := by      refine setLIntegral_congr_fun mG fun x mx ↦ ?_      unfold T_R; congr! 7 with R₁ mR₁ R₂ mR₂; rw [indicator_of_mem (sG mx)]    _ ≤ ∫⁻ x in G, ⨆ R₁ ∈ Ioo R⁻¹ R, ⨆ R₂ ∈ Ioo R₁ R,        ‖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      gcongr with x R₁ mR₁ R₂ mR₂      exact enorm_carlesonOperatorIntegrand_le_T_S (iRpos.trans mR₁.1) mR₂.1 mf nf    _ ≤ ∫⁻ x in G, ⨆ R₁ ∈ Ioo R⁻¹ R, (⨆ R₂ ∈ Ioo R₁ R, ‖T_S Q (L302 a R₁) (U302 a R₂) f x‖ₑ) +        ⨆ R₂ ∈ Ioo R₁ R, 4 * C2_1_3 a *          globalMaximalFunction volume 1 (F.indicator (1 : X → ℝ)) x := by      gcongr with x R₁ mR₁; exact biSup_add_le_add_biSup    _ ≤ ∫⁻ x in G, (⨆ R₁ ∈ Ioo R⁻¹ R, ⨆ R₂ ∈ Ioo R₁ R, ‖T_S Q (L302 a R₁) (U302 a R₂) f x‖ₑ) +        ⨆ R₁ ∈ Ioo R⁻¹ R, ⨆ R₂ ∈ Ioo R₁ R, 4 * C2_1_3 a *          globalMaximalFunction volume 1 (F.indicator (1 : X → ℝ)) x := by      gcongr with x; exact biSup_add_le_add_biSup    _ ≤ ∫⁻ x in G, (⨆ s₁ ∈ Finset.Icc (-B : ℤ) B, ⨆ s₂ ∈ Finset.Icc s₁ B, ‖T_S Q s₁ s₂ f x‖ₑ) +        4 * C2_1_3 a * globalMaximalFunction volume 1 (F.indicator (1 : X → ℝ)) x := by      gcongr with x      all_goals refine iSup₂_le fun R₁ mR₁ ↦ iSup₂_le fun R₂ mR₂ ↦ ?_      · specialize hB R₁ mR₁ R₂ mR₂        rcases lt_or_ge (U302 a R₂) (L302 a R₁) with hul | hul        · rw [T_S, Finset.Icc_eq_empty (not_le.mpr hul), Finset.sum_empty, enorm_zero]          exact zero_le        · trans ⨆ s₂ ∈ Finset.Icc (L302 a R₁) B, ‖T_S Q (L302 a R₁) s₂ f x‖ₑ          · have : U302 a R₂ ∈ Finset.Icc (L302 a R₁) B :=              Finset.mem_Icc.mpr ⟨hul, (Finset.mem_Icc.mp hB.2).2⟩            exact le_biSup (α := ℝ≥0∞) _ this          · exact le_biSup (α := ℝ≥0∞) _ hB.1      · rfl    _ = (∫⁻ x in G, ⨆ s₁ ∈ Finset.Icc (-B : ℤ) B, ⨆ s₂ ∈ Finset.Icc s₁ B, ‖T_S Q s₁ s₂ f x‖ₑ) +        4 * C2_1_3 a * ∫⁻ x in G, globalMaximalFunction volume 1 (F.indicator (1 : X → ℝ)) x := by      rw [← lintegral_const_mul' _ _ (by finiteness)]; apply lintegral_add_left      simp_rw [← Finset.mem_coe]      refine Measurable.biSup _ (Finset.countable_toSet _) fun s₁ ms₁ ↦ ?_      exact Measurable.biSup _ (Finset.countable_toSet _) fun s₂ ms₂ ↦ (measurable_T_S mf).enorm    _ ≤ C3_0_4 a q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ + 4 * C2_1_3 a *        (C2_0_6 (defaultA a) 1 q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹) := by      have bF := isBounded_ball.subset sF      have bG := isBounded_ball.subset sG      gcongr      · exact S_truncation hq hqq' bF bG mF mG mf nf BST_T_Q      · exact lintegral_globalMaximalFunction_le hq hqq' bF mF mG    _ ≤ _ := by      simp_rw [← mul_assoc, ← add_mul]; gcongr; norm_cast; exact le_C1_0_2 (four_le_a X) hq