MeasureTheory.estimate_eLpNorm_trunc

lemma estimate_eLpNorm_trunc {p q : ℝ≥0∞}    (hq : q ≠ ⊤) (hpq : p ∈ Ioc 0 q) {f : α → ε} (hf : AEStronglyMeasurable f μ) :    eLpNorm (trunc f t) q μ ^ q.toReal ≤    (t ^ (q.toReal - p.toReal)) * eLpNorm f p μ ^ p.toReal := by  have hq' : 0 < q := hpq.1.trans_le hpq.2  have p_ne_top : p ≠ ∞ := (hpq.2.trans_lt (lt_top_iff_ne_top.mpr hq)).ne  by_cases ht : t = ⊤  · by_cases hf' : eLpNorm f p μ ^ p.toReal = 0    · have : (fun x ↦ ‖f x‖ₑ) =ᵐ[μ] 0 := by        rw [← eLpNorm_enorm] at hf'        rwa [← eLpNorm_eq_zero_iff (by fun_prop) hpq.1.ne',          ← ENNReal.rpow_eq_zero_iff_of_pos (toReal_pos hpq.1.ne' p_ne_top)]      refine le_of_eq_of_le ?_ zero_le      rw [rpow_eq_zero_iff_of_pos]      · rw [← MeasureTheory.eLpNorm_enorm, eLpNorm_eq_zero_iff (by fun_prop) hq'.ne']        filter_upwards [this] with x h₀        exact nonpos_iff_eq_zero.mp (le_of_le_of_eq trunc_le_func h₀)      · rw [toReal_pos_iff]        exact ⟨hq', hq.lt_top⟩    · -- The right hand side is `∞`, hence the statement is always true.      simp only [ht, trunc_top, ge_iff_le]      by_cases p_eq_q : p = q      · simp [p_eq_q]      rw [top_rpow_of_pos, top_mul hf']      · apply le_top      rw [sub_pos, toReal_lt_toReal p_ne_top hq]      exact lt_of_le_of_ne hpq.2 p_eq_q  unfold eLpNorm eLpNorm'  have : p ≠ 0 := hpq.1.ne'  split_ifs with h  · exfalso    exact hq'.ne' h  · calc    _ = ∫⁻ (x : α) in {x | 0 < ‖f x‖ₑ ∧ ‖f x‖ₑ ≤ t}, ‖trunc f t x‖ₑ ^ q.toReal ∂μ := by      rw [one_div, ENNReal.rpow_inv_rpow]      · apply Eq.symm        apply setLIntegral_eq_of_support_subset        unfold Function.support        intro x        dsimp only [Pi.sub_apply, mem_setOf_eq]        unfold trunc        split_ifs with is_fx_le_a        · intro fx_rpow_ne_zero          refine ⟨?_, is_fx_le_a⟩          contrapose! fx_rpow_ne_zero          simpa [nonpos_iff_eq_zero.mp fx_rpow_ne_zero] using toReal_pos hq'.ne' hq        · contrapose; intro _; simpa using toReal_pos hq'.ne' hq      · exact (toReal_pos (hpq.1.trans_le hpq.2).ne' hq).ne'    _ ≤ ∫⁻ (x : α) in {x | 0 < ‖f x‖ₑ ∧ ‖f x‖ₑ ≤ t}, ‖f x‖ₑ ^ q.toReal ∂ μ := by      gcongr with x      exact trnc_le_func (j := ⊤)    _ ≤ (t ^ (q.toReal - p.toReal)) *        ∫⁻ (x : α) in {x | 0 < ‖f x‖ₑ ∧ ‖f x‖ₑ ≤ t}, ‖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_le_enorm hx.1 (ne_top_of_le_ne_top ht hx.2) hx.2 <| toReal_mono hq hpq.2      · simp_all    _ ≤ _ := by      gcongr      rw [one_div, ENNReal.rpow_inv_rpow]      · exact setLIntegral_le_lintegral _ _      · exact (toReal_pos hpq.1.ne' p_ne_top).ne'