Integration of specific interval integrals #
This file contains proofs of the integrals of various simple functions, including
λ x, 1 / (1 + x^2).
There are also facts about more complicated integrals:
sin x ^ n: We prove a recursive formula for
sin x ^ (n + 2)in terms of
sin x ^ n, along with explicit product formulas for even and odd
cos x ^ 2 - sin x ^ 2
With these lemmas, many simple integrals can be computed by
test/integration.lean for specific examples.
This file is still being developed.