Elementary interval integrals

Interval integrals of elementary functions in closed form, continuing Mathlib's Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean.

Main declarations

• TauCeti.integral_one_div_sqrt_one_sub_sq: ∫ x in a..b, 1 / √(1 - x²) = arcsin b - arcsin a for a, b ∈ (-1, 1).

theorem TauCeti.integral_one_div_sqrt_one_sub_sq {a b : ℝ} (ha : a ∈ Set.Ioo (-1) 1) (hb : b ∈ Set.Ioo (-1) 1) : ∫ (x : ℝ) in a..b, 1 / √(1 - x ^ 2) = Real.arcsin b - Real.arcsin a

The integral of 1 / √(1 - x²) is arcsin, between any two points of (-1, 1).