Fundamental Theorem of Calculus #

We prove various versions of the fundamental theorem of calculus for interval integrals in ℝ.

Recall that its first version states that the function (u, v) ↦ ∫ x in u..v, f x has derivative (δu, δv) ↦ δv • f b - δu • f a at (a, b) provided that f is continuous at a and b, and its second version states that, if f has an integrable derivative on [a, b], then ∫ x in a..b, f' x = f b - f a.

Main statements #

FTC-1 for Lebesgue measure #

We prove several versions of FTC-1, all in the intervalIntegral namespace. Many of them follow the naming scheme integral_has(Strict?)(F?)Deriv(Within?)At(_of_tendsto_ae?)(_right|_left?). They formulate FTC in terms of Has(Strict?)(F?)Deriv(Within?)At. Let us explain the meaning of each part of the name:

Strict means that the theorem is about strict differentiability, see HasStrictDerivAt and HasStrictFDerivAt;
F means that the theorem is about differentiability in both endpoints; incompatible with _right|_left;
Within means that the theorem is about one-sided derivatives, see below for details;
_of_tendsto_ae means that instead of continuity the theorem assumes that f has a finite limit almost surely as x tends to a and/or b;
_right or _left mean that the theorem is about differentiability in the right (resp., left) endpoint.

We also reformulate these theorems in terms of (f?)deriv(Within?). These theorems are named (f?)deriv(Within?)_integral(_of_tendsto_ae?)(_right|_left?) with the same meaning of parts of the name.

One-sided derivatives #

Theorem intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae states that (u, v) ↦ ∫ x in u..v, f x has a derivative (δu, δv) ↦ δv • cb - δu • ca within the set s × t at (a, b) provided that f tends to ca (resp., cb) almost surely at la (resp., lb), where possible values of s, t, and corresponding filters la, lb are given in the following table.

`s`	`la`	`t`	`lb`
`Iic a`	`𝓝[≤] a`	`Iic b`	`𝓝[≤] b`
`Ici a`	`𝓝[>] a`	`Ici b`	`𝓝[>] b`
`{a}`	`⊥`	`{b}`	`⊥`
`univ`	`𝓝 a`	`univ`	`𝓝 b`

We use a typeclass intervalIntegral.FTCFilter to make Lean automatically find la/lb based on s/t. This way we can formulate one theorem instead of 16 (or 8 if we leave only non-trivial ones not covered by integral_hasDerivWithinAt_of_tendsto_ae_(left|right) and integral_hasFDerivAt_of_tendsto_ae). Similarly, integral_hasDerivWithinAt_of_tendsto_ae_right works for both one-sided derivatives using the same typeclass to find an appropriate filter.

FTC for a locally finite measure #

Before proving FTC for the Lebesgue measure, we prove a few statements that can be seen as FTC for any measure. The most general of them, measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae, states the following. Let (la, la') be an intervalIntegral.FTCFilter pair of filters around a (i.e., intervalIntegral.FTCFilter a la la') and let (lb, lb') be an intervalIntegral.FTCFilter pair of filters around b. If f has finite limits ca and cb almost surely at la' and lb', respectively, then $$ \int_{va}^{vb} f ∂μ - \int_{ua}^{ub} f ∂μ = \int_{ub}^{vb} cb ∂μ - \int_{ua}^{va} ca ∂μ + o(‖∫_{ua}^{va} 1 ∂μ‖ + ‖∫_{ub}^{vb} (1:ℝ) ∂μ‖) $$ as ua and va tend to la while ub and vb tend to lb.

FTC-2 and corollaries #

We use FTC-1 to prove several versions of FTC-2 for the Lebesgue measure, using a similar naming scheme as for the versions of FTC-1. They include:

intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le - most general version, for functions with a right derivative
intervalIntegral.integral_eq_sub_of_hasDerivAt - version for functions with a derivative on an open set
intervalIntegral.integral_deriv_eq_sub' - version that is easiest to use when computing the integral of a specific function

We then derive additional integration techniques from FTC-2:

intervalIntegral.integral_mul_deriv_eq_deriv_mul - integration by parts
intervalIntegral.integral_comp_mul_deriv'' - integration by substitution

Many applications of these theorems can be found in the file Mathlib/Analysis/SpecialFunctions/Integrals.lean.

Note that the assumptions of FTC-2 are formulated in the form that f' is integrable. To use it in a context with the stronger assumption that f' is continuous, one can use ContinuousOn.intervalIntegrable or ContinuousOn.integrableOn_Icc or ContinuousOn.integrableOn_uIcc.

`intervalIntegral.FTCFilter` class #

As explained above, many theorems in this file rely on the typeclass intervalIntegral.FTCFilter (a : ℝ) (l l' : Filter ℝ) to avoid code duplication. This typeclass combines four assumptions:

pure a ≤ l;
l' ≤ 𝓝 a;
l' has a basis of measurable sets;
if u n and v n tend to l, then for any s ∈ l', Ioc (u n) (v n) is eventually included in s.

This typeclass has the following “real” instances: (a, pure a, ⊥), (a, 𝓝[≥] a, 𝓝[>] a), (a, 𝓝[≤] a, 𝓝[≤] a), (a, 𝓝 a, 𝓝 a). Furthermore, we have the following instances that are equal to the previously mentioned instances: (a, 𝓝[{a}] a, ⊥) and (a, 𝓝[univ] a, 𝓝[univ] a). While the difference between Ici a and Ioi a doesn't matter for theorems about Lebesgue measure, it becomes important in the versions of FTC about any locally finite measure if this measure has an atom at one of the endpoints.

Combining one-sided and two-sided derivatives #

There are some intervalIntegral.FTCFilter instances where the fact that it is one-sided or two-sided depends on the point, namely (x, 𝓝[Set.Icc a b] x, 𝓝[Set.Icc a b] x) (resp. (x, 𝓝[Set.uIcc a b] x, 𝓝[Set.uIcc a b] x), with x ∈ Icc a b (resp. x ∈ uIcc a b). This results in a two-sided derivatives for x ∈ Set.Ioo a b and one-sided derivatives for x ∈ {a, b}. Other instances could be added when needed (in that case, one also needs to add instances for Filter.IsMeasurablyGenerated and Filter.TendstoIxxClass).

Tags #

integral, fundamental theorem of calculus, FTC-1, FTC-2, change of variables in integrals

Fundamental theorem of calculus, part 1, for any measure #

In this section we prove a few lemmas that can be seen as versions of FTC-1 for interval integrals w.r.t. any measure. Many theorems are formulated for one or two pairs of filters related by intervalIntegral.FTCFilter a l l'. This typeclass has exactly four “real” instances: (a, pure a, ⊥), (a, 𝓝[≥] a, 𝓝[>] a), (a, 𝓝[≤] a, 𝓝[≤] a), (a, 𝓝 a, 𝓝 a), and two instances that are equal to the first and last “real” instances: (a, 𝓝[{a}] a, ⊥) and (a, 𝓝[univ] a, 𝓝[univ] a). We use this approach to avoid repeating arguments in many very similar cases. Lean can automatically find both a and l' based on l.

The most general theorem measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae can be seen as a generalization of lemma integral_hasStrictFDerivAt below which states strict differentiability of ∫ x in u..v, f x in (u, v) at (a, b) for a measurable function f that is integrable on a..b and is continuous at a and b. The lemma is generalized in three directions: first, measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae deals with any locally finite measure μ; second, it works for one-sided limits/derivatives; third, it assumes only that f has finite limits almost surely at a and b.

Namely, let f be a measurable function integrable on a..b. Let (la, la') be a pair of intervalIntegral.FTCFilters around a; let (lb, lb') be a pair of intervalIntegral.FTCFilters around b. Suppose that f has finite limits ca and cb at la' ⊓ ae μ and lb' ⊓ ae μ, respectively. Then ∫ x in va..vb, f x ∂μ - ∫ x in ua..ub, f x ∂μ = ∫ x in ub..vb, cb ∂μ - ∫ x in ua..va, ca ∂μ + o(‖∫ x in ua..va, (1:ℝ) ∂μ‖ + ‖∫ x in ub..vb, (1:ℝ) ∂μ‖) as ua and va tend to la while ub and vb tend to lb.

This theorem is formulated with integral of constants instead of measures in the right hand sides for two reasons: first, this way we avoid min/max in the statements; second, often it is possible to write better simp lemmas for these integrals, see integral_const and integral_const_of_cdf.

In the next subsection we apply this theorem to prove various theorems about differentiability of the integral w.r.t. Lebesgue measure.

Fundamental Theorem of Calculus #

Main statements #

FTC-1 for Lebesgue measure #

One-sided derivatives #

FTC for a locally finite measure #

FTC-2 and corollaries #

intervalIntegral.FTCFilter class #

Combining one-sided and two-sided derivatives #

Tags #

Fundamental theorem of calculus, part 1, for any measure #

Fundamental theorem of calculus-1 for Lebesgue measure #

Auxiliary Asymptotics.IsLittleO statements #

Strict differentiability #

Fréchet differentiability #

One-sided derivatives #

Fundamental theorem of calculus, part 2 #

Automatic integrability for nonnegative derivatives #

Integration by parts #

Integration by substitution / Change of variables #

`intervalIntegral.FTCFilter` class #

Auxiliary `Asymptotics.IsLittleO` statements #