Module mathcomp.analysis.ftc

# Fundamental Theorem of Calculus and Consequences This file provides lemmas about derivation and integration. It contains in particular a proof of the first fundamental theorem of calculus for the Lebesgue integral and its consequences, in particular a corollary to compute the integral of continuous functions, integration by parts, by substitution, etc. Reference: - R. Affeldt, Z. Stone. A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. ITP 2024 Examples of lemmas (with `F` and `G` antiderivatives of `f` and `g`): - `continuous_FTC2`: $\int_a^b f(x)dx = F(b) - F(a)$ - `{ge0,le0}_continuous_FTC2y`: $\int_a^\infty f(x)dx = \ell - F(a)$ with $\lim_{x\to\infty}F(x)=\ell$ and $f$ non-negative or non-positive - `integration_by_parts`: $\int_a^b F(x)g(x)dx = F(b)G(b) - F(a)G(a) - \int_a^b f(x)G(x)dx$ - `integration_by_substitution_{decreasing,increasing}`: $\int_{F(b)}^{F(a)} G(x)dx = \int_a^b -G(F(x))f(x)dx$ with $F$ decreasing, $\int_{F(a)}^{F(b)} G(x)dx = \int_a^b G(F(x))f(x)dx$ with $F$ increasing - `{decreasing,increasing}_ge0_integration_by_substitutiony`: $\int_{-\infty}^{F(a)} G(x)dx = \int_a^\infty -G(F(x))f(x)dx$ with $F$ decreasing, $\lim_{x\to\infty}F(x)=-\infty$, and $G$ non-negative, $\int_{F(a)}^{\infty} G(x)dx = \int_a^\infty G(F(x))f(x)dx$ with $F$ increasing, $\lim_{x\to\infty}F(x)=\infty$, and $G$ non-negative - `increasing_ge0_integration_by_substitutionT`: $\int_{-\infty}^{\infty} G(x)dx = \int_{-\infty}^\infty -G(F(x))f(x)dx$ with $F$ increasing and $G$ non-negative Detailed documentation: ``` partial1of2 f == first partial derivative of f f has type R -> T -> R for R : realType parameterized_integral mu a x f := \int[mu]_(t \in `[a, x] f t) ```