MeasureTheory.estimate_eLpNorm_truncCompl

lemma estimate_eLpNorm_truncCompl {p q : ℝ≥0∞}    (p_ne_top : p ≠ ⊤) (hpq : q ∈ Ioc 0 p) (hf : AEStronglyMeasurable f μ) (ht : 0 < t) :    eLpNorm (truncCompl f t) q μ ^ q.toReal ≤    (t ^ (q.toReal - p.toReal)) * eLpNorm f p μ ^ p.toReal := by  have q_ne_top: q ≠ ⊤ := ne_top_of_le_ne_top p_ne_top hpq.2  have p_ne_zero : p ≠ 0 := (hpq.1.trans_le hpq.2).ne'  apply le_trans (eLpNorm_truncCompl_le hpq.1.ne' (ne_top_of_le_ne_top p_ne_top hpq.2))  calc    _ ≤ (t ^ (q.toReal - p.toReal)) * ∫⁻ x : α in {x | t < ‖f x‖ₑ},        ‖f x‖ₑ ^ p.toReal ∂μ := by      rw [← lintegral_const_mul']      · apply setLIntegral_mono_ae (AEMeasurable.restrict (by fun_prop))        filter_upwards with x hx        rw [mul_comm]        exact rpow_le_rpow_of_exponent_le_base_ge_enorm ht hx.ne_top hx.le (toReal_mono p_ne_top hpq.2)      · by_cases ht' : t = ⊤        · simp_all        · finiteness    _ ≤ (t ^ (q.toReal - p.toReal)) * ∫⁻ x : α, ‖f x‖ₑ ^ p.toReal ∂μ := by      gcongr      exact Measure.restrict_le_self    _ = _ := by      congr      rw [eLpNorm_eq_lintegral_rpow_enorm_toReal p_ne_zero p_ne_top, one_div, ENNReal.rpow_inv_rpow]      exact (toReal_pos p_ne_zero p_ne_top).ne'