Substituting u = x² in an interval integral

On an interval of nonnegative reals the map x ↦ x² is monotone with derivative 2 x ≥ 0, so Mathlib's change of variables intervalIntegral.integral_comp_mul_deriv_of_deriv_nonneg applies to any integrand g, with no continuity or integrability hypothesis on g: ∫ x in a..b, g (x²) * (2 x) = ∫ u in a²..b², g u.

Main declarations

• TauCeti.intervalIntegral.integral_comp_sq_mul

theorem TauCeti.intervalIntegral.integral_comp_sq_mul {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (g : ℝ → ℝ) : ∫ (x : ℝ) in a..b, g (x ^ 2) * (2 * x) = ∫ (u : ℝ) in a ^ 2..b ^ 2, g u

Substituting u = x². For 0 ≤ a and 0 ≤ b, ∫ x in a..b, g (x²) * (2 x) = ∫ u in a²..b², g u for every g : ℝ → ℝ.