MeasureTheory.memLp_truncCompl_of_memLp_top

lemma memLp_truncCompl_of_memLp_top (hf : MemLp f ⊤ μ) (h : μ {x | t < ‖f x‖ₑ} < ⊤) :    MemLp (trnc ⊥ f t) p μ := by  by_cases hp_top : p = ⊤  · rw [hp_top]    simp only [bot_eq_false, trnc_false]    exact hf.truncCompl  obtain ⟨hf_m, hf_lt_top⟩ := hf  by_cases hp0 : p = 0  · rw [hp0, memLp_zero_iff_aestronglyMeasurable]    exact aestronglyMeasurable_trnc hf_m  /- TODO: We currently need this annoying extra step because    we do not have `MeasurableSet {a | t < ‖f a‖ₑ}` in general    (since f is only aestronglymeasurable).  -/  rcases hf_m with ⟨g, ⟨wg1, wg2⟩⟩  have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top  have ae_eq_trunc : (trnc ⊥ f t) =ᶠ[ae μ] (trnc ⊥ g t) := by    simp only [bot_eq_false, trnc_false]    rw [truncCompl_eq_indicator, truncCompl_eq_indicator]    rw [Filter.eventuallyEq_iff_exists_mem] at wg2    rcases wg2 with ⟨s, hs, hfgs⟩    rw [Filter.eventuallyEq_iff_exists_mem]    use s, hs    intro x hs    rw [indicator, indicator]    split_ifs with hx hx' hx''    · exact hfgs hs    · exfalso      simp only [mem_compl_iff, mem_setOf_eq, not_le, not_lt, hfgs hs] at hx hx'      order    · exfalso      simp only [mem_compl_iff, mem_setOf_eq, not_le, not_lt, hfgs hs] at hx hx''      order    · rfl  apply MemLp.ae_eq ae_eq_trunc.symm  use aestronglyMeasurable_trnc wg1.aestronglyMeasurable  simp only [bot_eq_false, trnc_false]  rw [truncCompl_eq_indicator,      eLpNorm_indicator_eq_eLpNorm_restrict        (by rw [compl_setOf]; simp only [not_le]; exact measurableSet_lt measurable_const (by fun_prop))]  rw [eLpNorm_eq_eLpNorm' hp0 hp_top]  apply (eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hp_pos).trans_lt  apply ENNReal.mul_lt_top  · rw [← eLpNorm_exponent_top]    apply (eLpNorm_restrict_le _ _ _ _).trans_lt    rwa [eLpNorm_congr_ae wg2.symm]  apply ENNReal.rpow_lt_top_of_nonneg (by simp [hp_pos.le])  simp only [MeasurableSet.univ, Measure.restrict_apply, univ_inter]  rw [← lt_top_iff_ne_top, compl_setOf]  calc  _ = μ {a | t < ‖f a‖ₑ} := by    apply measure_congr    rw [Filter.eventuallyEq_iff_exists_mem] at wg2    rcases wg2 with ⟨s, hs, hfgs⟩    rw [Filter.eventuallyEq_iff_exists_mem]    exact ⟨s, hs, fun a ha ↦ by simp [setOf, hfgs.symm ha]⟩  _ < ∞ := h