Integral over an interval #

In this file we define ∫ x in a..b, f x ∂μ to be ∫ x in Ioc a b, f x ∂μ if a ≤ b and -∫ x in Ioc b a, f x ∂μ if b ≤ a. We prove a few simple properties and several versions of the fundamental theorem of calculus.

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 interval_integral 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;
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 integral_has_fderiv_within_at_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 FTC_filter 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_has_deriv_within_at_of_tendsto_ae_(left|right) and integral_has_fderiv_at_of_tendsto_ae). Similarly, integral_has_deriv_within_at_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_is_o_of_tendsto_ae, states the following. Let (la, la') be an FTC_filter pair of filters around a (i.e., FTC_filter a la la') and let (lb, lb') be an FTC_filter pair of filters around b. If f has finite limits ca and cb almost surely at la' and lb', 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.

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:

interval_integral.integral_eq_sub_of_has_deriv_right_of_le - most general version, for functions with a right derivative
interval_integral.integral_eq_sub_of_has_deriv_at' - version for functions with a derivative on an open set
interval_integral.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:

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

Many applications of these theorems can be found in the file analysis.special_functions.integrals.

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 continuous_on.interval_integrable or continuous_on.integrable_on_Icc or continuous_on.integrable_on_interval.

Implementation notes #

Avoiding `if`, `min`, and `max` #

In order to avoid ifs in the definition, we define interval_integrable f μ a b as integrable_on f (Ioc a b) μ ∧ integrable_on f (Ioc b a) μ. For any a, b one of these intervals is empty and the other coincides with set.interval_oc a b = set.Ioc (min a b) (max a b).

Similarly, we define ∫ x in a..b, f x ∂μ to be ∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ. Again, for any a, b one of these integrals is zero, and the other gives the expected result.

This way some properties can be translated from integrals over sets without dealing with the cases a ≤ b and b ≤ a separately.

Choice of the interval #

We use integral over set.interval_oc a b = set.Ioc (min a b) (max a b) instead of one of the other three possible intervals with the same endpoints for two reasons:

this way ∫ x in a..b, f x ∂μ + ∫ x in b..c, f x ∂μ = ∫ x in a..c, f x ∂μ holds whenever f is integrable on each interval; in particular, it works even if the measure μ has an atom at b; this rules out set.Ioo and set.Icc intervals;
with this definition for a probability measure μ, the integral ∫ x in a..b, 1 ∂μ equals the difference $F_μ(b)-F_μ(a)$, where $F_μ(a)=μ(-∞, a]$ is the cumulative distribution function of μ.

`FTC_filter` class #

As explained above, many theorems in this file rely on the typeclass FTC_filter (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 FTC_filter instances where the fact that it is one-sided or two-sided depends on the point, namely (x, 𝓝[Icc a b] x, 𝓝[Icc a b] x) (resp. (x, 𝓝[[a, b]] x, 𝓝[[a, b]] x), where [a, b] = set.interval a b), with x ∈ Icc a b (resp. x ∈ [a, b]). This results in a two-sided derivatives for x ∈ 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.is_measurably_generated and filter.tendsto_Ixx_class).

Tags #

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

Integral over an interval #

Main statements #

FTC-1 for Lebesgue measure #

One-sided derivatives #

FTC for a locally finite measure #

FTC-2 and corollaries #

Implementation notes #

Avoiding if, min, and max #

Choice of the interval #

FTC_filter class #

Combining one-sided and two-sided derivatives #

Tags #

Integrability at an interval #

Interval integral: definition and basic properties #

Integral is an additive function of the interval #

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

Fundamental theorem of calculus-1 for Lebesgue measure #

Auxiliary is_o statements #

Strict differentiability #

Fréchet differentiability #

One-sided derivatives #

Avoiding `if`, `min`, and `max` #

`FTC_filter` class #

Auxiliary `is_o` statements #