Commit 2021-03-02 02:22 5c016137

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.