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 many versions of the first part of the fundamental theorem of calculus. Recall that it 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.

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.

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.

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 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 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 Ioo and 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 exactly four “real” instances: (a, pure a, ⊥), (a, 𝓝[Ici a] a, 𝓝[Ioi a] a), (a, 𝓝[Iic a] a, 𝓝[Iic 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). 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.

Tags #

integral, fundamental theorem of calculus

Integrability at an interval #

Interval integral: definition and basic properties #

In this section we define ∫ x in a..b, f x ∂μ as ∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ and prove some basic properties.

Integral is an additive function of the interval #

In this section we prove that ∫ x in a..b, f x ∂μ + ∫ x in b..c, f x ∂μ = ∫ x in a..c, f x ∂μ as well as a few other identities trivially equivalent to this one. We also prove that ∫ x in a..b, f x ∂μ = ∫ x, f x ∂μ provided that support f ⊆ Ioc a b.

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 FTC_filter a l l'. This typeclass has exactly four “real” instances: (a, pure a, ⊥), (a, 𝓝[Ici a] a, 𝓝[Ioi a] a), (a, 𝓝[Iic a] a, 𝓝[Iic 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_is_o_of_tendsto_ae can be seen as a generalization of lemma integral_has_strict_fderiv_at 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_is_o_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 FTC_filters around a; let (lb, lb') be a pair of FTC_filters 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.