TileStructure.Forest.nontangential_operator_bound

lemma nontangential_operator_bound (hf : BoundedCompactSupport f) (θ : Θ X) :    eLpNorm (nontangentialMaximalFunction θ f) 2 volume ≤ C7_2_2 a * eLpNorm f 2 volume := by  have aemeas_MB : AEMeasurable (maximalFunction volume 𝓑 c𝓑 r𝓑 1 f ·) :=    measurable_maximalFunction.aemeasurable  have ⟨hT₁, hT₂⟩ := BST_T_Q θ f hf.boundedFiniteSupport  dsimp only at hT₁ hT₂  calc    _ ≤ eLpNorm (fun x ↦ 2 * linearizedNontangentialOperator Q θ K f x +        2 ^ (7 * a + (𝕔 + 1) * a ^ 3 + 1) * maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x) 2 volume := by      simp only [eLpNorm, OfNat.ofNat_ne_zero, reduceIte, ENNReal.ofNat_ne_top, eLpNorm']      gcongr; simp_rw [enorm_eq_self]; exact nontangential_pointwise_bound hf θ _    _ ≤ eLpNorm (fun x ↦ 2 * linearizedNontangentialOperator Q θ K f x) 2 volume +        eLpNorm (2 ^ (7 * a + (𝕔 + 1) * a ^ 3 + 1) *          maximalFunction volume 𝓑 c𝓑 r𝓑 1 f ·) 2 volume := by      simpa [eLpNorm, eLpNorm'] using        ENNReal.lintegral_Lp_add_le (hT₁.aemeasurable.const_mul _)          (aemeas_MB.const_mul _) one_le_two    _ = eLpNorm (fun x ↦ 2 * linearizedNontangentialOperator Q θ K f x) 2 volume +        2 ^ (7 * a + (𝕔 + 1) * a ^ 3 + 1) * eLpNorm (maximalFunction volume 𝓑 c𝓑 r𝓑 1 f) 2 volume := by      congr      simp only [eLpNorm, eLpNorm', OfNat.ofNat_ne_zero, reduceIte, ENNReal.ofNat_ne_top]      exact ENNReal.lintegral_Lp_smul aemeas_MB two_pos ((2 : ℝ≥0) ^ (7 * a + (𝕔 + 1) * a ^ 3 + 1))    _ ≤ 2 * eLpNorm (linearizedNontangentialOperator Q θ K f) 2 volume +        2 ^ (7 * a + (𝕔 + 1) * a ^ 3 + 1) * eLpNorm (maximalFunction volume 𝓑 c𝓑 r𝓑 1 f) 2 volume := by      gcongr      refine eLpNorm_le_mul_eLpNorm_of_ae_le_mul'' 2 hT₁ (.of_forall fun x ↦ ?_)      rw [enorm_eq_self, enorm_eq_self]    _ ≤ (2 * C_Ts a + 2 ^ (7 * a + (𝕔 + 1) * a ^ 3 + 1) * CMB (defaultA a) 2)        * eLpNorm f 2 volume := by      simp only [add_mul, one_mul, Nat.cast_pow, Nat.cast_ofNat, mul_assoc]      gcongr      simpa using eLpNorm_MB_le hf    _ ≤ _ := by      simp_rw [show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl, ← ENNReal.coe_pow, ← ENNReal.coe_mul,        ← ENNReal.coe_add]      gcongr; exact le_C7_2_2 (four_le_a X)