English
The integral of sqrt(1 − x^2) over [−1,1] equals π/2.
Русский
Интеграл sqrt(1 − x^2) по [−1,1] равен π/2.
LaTeX
$$$$\\int_{-1}^{1} \\sqrt{1-x^{2}} \\,dx = \\frac{\\pi}{2}.$$$$
Lean4
theorem integral_sqrt_one_sub_sq : ∫ x in (-1 : ℝ)..1, √(1 - x ^ 2 : ℝ) = π / 2 :=
calc
_ = ∫ x in sin (-(π / 2))..sin (π / 2), √(1 - x ^ 2 : ℝ) := by rw [sin_neg, sin_pi_div_two]
_ = ∫ x in (-(π / 2))..(π / 2), √(1 - sin x ^ 2 : ℝ) * cos x :=
(integral_comp_mul_deriv (fun x _ => hasDerivAt_sin x) continuousOn_cos (by fun_prop)).symm
_ = ∫ x in (-(π / 2))..(π / 2), cos x ^ 2 :=
by
refine integral_congr_ae (MeasureTheory.ae_of_all _ fun _ h => ?_)
rw [uIoc_of_le (neg_le_self (le_of_lt (half_pos Real.pi_pos))), Set.mem_Ioc] at h
rw [← Real.cos_eq_sqrt_one_sub_sin_sq (le_of_lt h.1) h.2, pow_two]
_ = π / 2 := by simp
