MeasureTheory.lintegral_trunc_mul₀

lemma lintegral_trunc_mul₀ {g : ℝ → ℝ≥0∞} {j : Bool} {x : α} {tc : ToneCouple} {p : ℝ} (hp : 0 < p)    :    ∫⁻ s : ℝ in Ioi 0, (g s) * ‖trnc j f (tc.ton (ENNReal.ofReal s)) x‖ₑ ^ p =    ∫⁻ s : ℝ in res' (xor j tc.mon) (tc.inv ‖f x‖ₑ), (g s) *        ‖trnc j f (tc.ton (ENNReal.ofReal s)) x‖ₑ ^ p := by  rw [lintegral_double_restrict_set (B := res' (xor j tc.mon) (tc.inv ‖f x‖ₑ))      measurableSet_Ioi measurableSet_res', inter_eq_self_of_subset_right res'subset_Ioi]  filter_upwards  rw [res'comp]  intro s  unfold res trnc trunc truncCompl  have mon_pf := tc.inv_pf  split_ifs at mon_pf with mon  · rw [mon]    rcases j    · simp only [Bool.bne_true, Bool.not_false, not_true_eq_false, decide_false,      Bool.false_eq_true, ↓reduceIte]      split_ifs with h <;> intro hs      · simp [hp]      · simp at hs      · simp [hp]      · have := (mon_pf (ENNReal.ofReal s) ‖f x‖ₑ).2.mpr ((lt_ofReal_iff_toReal_lt h).mpr hs)        order    · simp only [bne_self_eq_false, Bool.false_eq_true, not_false_eq_true, decide_true]      split_ifs with h <;> intro hs      · have := (mon_pf (.ofReal s) ‖f x‖ₑ).1.mpr (by rw [h]; exact coe_lt_top)        order      · simp [hp]      · have := (mon_pf (.ofReal s) ‖f x‖ₑ).1.mpr <| (ofReal_lt_iff_lt_toReal hs.1.le h).mpr hs.2        order      · simp [hp]  · rw [Bool.not_eq_true] at mon    rw [mon]    rcases j    · simp only [bne_self_eq_false, Bool.false_eq_true, not_false_eq_true, decide_true,      ↓reduceIte]      split_ifs with h <;> intro hs      · simp [hp]      · have := (mon_pf (.ofReal s) ‖f x‖ₑ).2.mpr (by rw [h]; exact coe_lt_top)        order      · simp [hp]      · have := (mon_pf (.ofReal s) ‖f x‖ₑ).2.mpr <| (ofReal_lt_iff_lt_toReal hs.1.le h).mpr hs.2        order    · simp only [Bool.bne_false, not_true_eq_false, decide_false, Bool.false_eq_true, ↓reduceIte]      split_ifs with h <;> intro hs      · simp at hs      · simp [hp]      · have := (mon_pf (.ofReal s) ‖f x‖ₑ).1.mpr <| (lt_ofReal_iff_toReal_lt h).mpr hs        order      · simp [hp]