mathlib

5c016137 - feat(analysis/special_functions/integrals): some simple integration lemmas (#6216)

feat(analysis/special_functions/integrals): some simple integration lemmas (#6216) Integration of some simple functions, including `sin`, `cos`, `pow`, and `inv`. @ADedecker and I are working on the integrals of some more intricate functions, which we hope to add in a subsequent (series of) PR(s). With this PR, simple integrals are now computable by `norm_num`. Here are some examples: ``` import analysis.special_functions.integrals open real interval_integral open_locale real example : ∫ x in 0..π, sin x = 2 := by norm_num example : ∫ x in 0..π/4, cos x = sqrt 2 / 2 := by simp example : ∫ x:ℝ in 2..4, x^(3:ℕ) = 60 := by norm_num example : ∫ x in 0..2, -exp x = 1 - exp 2 := by simp example : ∫ x:ℝ in (-1)..4, x = 15/2 := by norm_num example : ∫ x:ℝ in 8..11, (1:ℝ) = 3 := by norm_num example : ∫ x:ℝ in 2..3, x⁻¹ = log (3/2) := by norm_num example : ∫ x:ℝ in 0..1, 1 / (1 + x^2) = π/4 := by simp ``` `integral_deriv_eq_sub'` courtesy of @gebner.