← Mathematical handbook

theorem Verification.lintegral_add_Ioi (f : ℝ → ENNReal) (x : ℝ) : ∫⁻ (y : ℝ) in Set.Ioi 0, f (x + y) = ∫⁻ (t : ℝ) in Set.Ioi x, f t

theorem Verification.lintegral_quadrant_sum (f : ℝ → ENNReal) (hf : Measurable f) : ∫⁻ (x : ℝ) (y : ℝ) in Set.Ioi 0, f (x + y) = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal t * f t

theorem Verification.integral_quadrant_sum (f : ℝ → ℝ) (hf : Measurable f) (hn : ∀ (t : ℝ), 0 ≤ f t) (hi : MeasureTheory.IntegrableOn (fun (t : ℝ) => t * f t) (Set.Ioi 0) MeasureTheory.volume) : ∫ (x : ℝ) (y : ℝ) in Set.Ioi 0, f (x + y) = ∫ (t : ℝ) in Set.Ioi 0, t * f t