Indicator component mem Lp

theorem indicator_component_memLp    {Ω : Set E} {σ g : E → ℝ}    (hσ_aemeas : AEMeasurable σ (volume.restrict Ω))    (hg_memLp : MemLp g 2 (volume.restrict Ω)) :    MemLp (fun x => if 0 < σ x then g x else 0) 2 (volume.restrict Ω) := by  let h : ℝ × ℝ → ℝ := fun yz => if 0 < yz.1 then yz.2 else 0  have hh_meas : Measurable h := by    refine measurable_snd.piecewise ?_ measurable_const    exact measurableSet_lt measurable_const measurable_fst  have hpair_aemeas :      AEMeasurable (fun x => (σ x, g x)) (volume.restrict Ω) :=    hσ_aemeas.prodMk hg_memLp.aemeasurable  have htrunc_aestrong :      AEStronglyMeasurable (fun x => if 0 < σ x then g x else 0) (volume.restrict Ω) := by    refine (hh_meas.comp_aemeasurable hpair_aemeas).aestronglyMeasurable.congr ?_    filter_upwards [] with x    by_cases hx : 0 < σ x    · simp [h, hx]    · simp [h, hx]  refine hg_memLp.norm.mono' htrunc_aestrong ?_  filter_upwards [] with x  by_cases hx : 0 < σ x  · simp [hx]  · simp [hx]