MeasureTheory.lintegral_trunc_mul₂

lemma lintegral_trunc_mul₂ {g : ℝ → ℝ≥0∞} {j : Bool} {x : α} {p : ℝ} {tc : ToneCouple} :    ∫⁻ s : ℝ in res (xor j tc.mon) (tc.inv ‖f x‖ₑ), (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) * ‖f x‖ₑ ^ p := by  apply setLIntegral_congr_fun measurableSet_res  unfold res trnc trunc truncCompl  have mon_pf := tc.inv_pf  split_ifs at mon_pf with mon  -- intro s hs  · rw [mon]    rcases j <;> intro s    · simp only [Bool.bne_true, Bool.not_false, ↓reduceIte]      split_ifs with h <;> intro hs      · have := (mon_pf (.ofReal s) ‖f x‖ₑ).1.mpr (by rw [h]; exact coe_lt_top)        order      · simp      · have := (mon_pf (.ofReal s) ‖f x‖ₑ).1.mpr <| (ofReal_lt_iff_lt_toReal hs.1.le h).mpr hs.2        order      · rfl    · simp only [bne_self_eq_false, Bool.false_eq_true, ↓reduceIte]      split_ifs with h <;> intro hs      · rfl      · simp at hs      · rfl      · have := (mon_pf (ENNReal.ofReal s) ‖f x‖ₑ).2.mpr ((lt_ofReal_iff_toReal_lt h).mpr hs)        order  · rw [Bool.not_eq_true] at mon    rw [mon]    rcases j <;> intro s    · simp only [bne_self_eq_false, Bool.false_eq_true, ↓reduceIte]      split_ifs with h <;> intro hs      · simp at hs      · simp at hs      · have := (mon_pf (.ofReal s) ‖f x‖ₑ).1.mpr <| (lt_ofReal_iff_toReal_lt h).mpr hs        order      · rfl    · simp only [Bool.bne_false, ↓reduceIte]      split_ifs with h <;> intro hs      · rfl      · have := (mon_pf (.ofReal s) ‖f x‖ₑ).2.mpr (by rw [h]; exact coe_lt_top)        order      · rfl      · have := (mon_pf (.ofReal s) ‖f x‖ₑ).2.mpr <| (ofReal_lt_iff_lt_toReal hs.1.le h).mpr hs.2        order