Commit 2021-03-19 12:51 ce107da5

feat(analysis/special_functions/integrals): integrating linear combinations of functions (#6597) Together with #6357, this PR makes it possible to compute integrals of the form ∫ x in a..b, c * f x + d * g x by simp (where c and d are constants and f and g are functions that are interval_integrable on interval a b. Notably, this allows us to compute the integrals of polynomials by norm_num. Here's an example, followed by an example of a more random linear combination of interval_integrable functions:

import analysis.special_functions.integrals
open interval_integral real
open_locale real
example : ∫ x:ℝ in 0..2, 6*x^5 + 3*x^4 + x^3 - 2*x^2 + x - 7 = 1048 / 15 := by norm_num
example : ∫ x:ℝ in 0..1, exp x + 9 * x^8 + x^3 - x/2 + (1 + x^2)⁻¹ = exp 1 + π/4 := by norm_num