← Mathematical handbook

theorem Verification.lintegral_mul_Ioi (f : ℝ → ENNReal) {x : ℝ} (hx : 0 < x) : ∫⁻ (y : ℝ) in Set.Ioi 0, f y = ∫⁻ (s : ℝ) in Set.Ioi 0, ENNReal.ofReal x * f (x * s)

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

theorem Verification.integral_quadrant_scale (f : ℝ × ℝ → ℝ) (hf : Measurable f) (hn : ∀ (z : ℝ × ℝ), 0 ≤ f z) (hi : MeasureTheory.Integrable f ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod (MeasureTheory.volume.restrict (Set.Ioi 0)))) : ∫ (x : ℝ) (y : ℝ) in Set.Ioi 0, f (x, y) = ∫ (s : ℝ) (x : ℝ) in Set.Ioi 0, max 0 x * f (x, x * s)