linearized_truncation

lemma linearized_truncation    [IsCancellative X (defaultτ a)] (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')    (bF : IsBounded F) (bG : IsBounded G) (mF : MeasurableSet F) (mG : MeasurableSet G)    (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1) (mσ₁ : Measurable σ₁) (mσ₂ : Measurable σ₂)    (rσ₁ : (range σ₁).Finite) (rσ₂ : (range σ₂).Finite) (lσ : σ₁ ≤ σ₂)    (BST_T_Q : ∀ θ : Θ X, HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·)      2 2 volume volume (C_Ts a)) :    ∫⁻ x in G, ‖T_lin Q σ₁ σ₂ f x‖ₑ ≤    C3_0_4 a q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by  let CP : CP304 q q' F f σ₁ σ₂ := ⟨Q, BST_T_Q, hq, hqq', bF, mF, mf, nf, mσ₁, mσ₂, rσ₁, rσ₂, lσ⟩  calc    _ = ∫⁻ x in ⋃ n, G \ (slice CP bG mG (n + 1)).G, ‖T_lin CP.Q σ₁ σ₂ f x‖ₑ := by      apply setLIntegral_congr; rw [← sdiff_iInter]; refine (sdiff_null_ae_eq_self ?_).symm      rw [Antitone.measure_iInter]; rotate_left      · exact fun _ _ _ ↦ antitone_slice_G (by lia)      · exact fun n ↦ (slice CP bG mG (n + 1)).mG.nullMeasurableSet      · use 0; rw [← lt_top_iff_ne_top]        exact (measure_mono slice_G_subset).trans_lt bG.measure_lt_top      rw [show (0 : ℝ≥0∞) = ⊥ by rfl, iInf_eq_bot]      exact fun _ ↦ exists_volume_slice_lt_eps    _ = ∫⁻ x, ⨆ n, (G \ (slice CP bG mG (n + 1)).G).indicator (‖T_lin CP.Q σ₁ σ₂ f ·‖ₑ) x := by      rw [← lintegral_indicator (MeasurableSet.iUnion fun n ↦ mG.diff (slice CP bG mG (n + 1)).mG)]      congr! with x      rw [← iSup_apply, iSup_indicator rfl monotone_const]; swap      · exact fun _ _ _ ↦ sdiff_le_sdiff_left (antitone_slice_G (by lia))      rw [iSup_const]    _ = ⨆ n, ∫⁻ x, (G \ (slice CP bG mG (n + 1)).G).indicator (‖T_lin CP.Q σ₁ σ₂ f ·‖ₑ) x := by      refine lintegral_iSup (fun n ↦ ?_) (fun i j hl ↦ ?_)      · exact (measurable_T_lin mf mσ₁ mσ₂ rσ₁ rσ₂).enorm.indicator          (mG.diff (slice CP bG mG (n + 1)).mG)      · gcongr        exact antitone_slice_G (by lia)    _ ≤ C2_0_1 a q * (2 ^ 2 / (q - 1) : ℝ≥0) * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by      refine iSup_le fun n ↦ slice_integral_bound_sum.trans ?_      gcongr; exact sum_le_four_div_q_sub_one hq hqq'    _ = _ := by rw [← ENNReal.coe_mul, eq_C3_0_4]