How to Formalize Integral Substitution in Lean 4?

Stream: new members

[Zhu]

I'm trying to formalize the following integral in Lean 4:

example : ∫ (x : ℝ) in (-2)..0, Real.sqrt (4 - x ^ 2) = π := by
  sorry

I've noticed that there's a related theorem integral_sqrt_one_sub_sq in mathlib:

example : ∫ (x : ℝ) in (-1)..1, Real.sqrt (1 - x ^ 2) = π / 2 := by
  exact integral_sqrt_one_sub_sq

Manually, I can solve my integral using a substitution: u = x / 2, but I'm not sure how to formalize this substitution process in Lean4.

Could anyone guide me on how to formalize this step in Lean 4? Thank you for your help! :smiley:

[Floris van Doorn]

docs#intervalIntegral.integral_comp_mul_deriv is a (pretty) general change of variables formula.
A specialized one for multiplying by a constant is docs#intervalIntegral.smul_integral_comp_mul_left

[Zhu]

Thanks