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:
_strictmeans that the theorem is about strict differentiability;fmeans that the theorem is about differentiability in both endpoints; incompatible with_right|_left;_withinmeans that the theorem is about one-sided derivatives, see below for details;_of_tendsto_aemeans that instead of continuity the theorem assumes thatfhas a finite limit almost surely asxtends toaand/orb;_rightor_leftmean 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 derivativeinterval_integral.integral_eq_sub_of_has_deriv_at'- version for functions with a derivative on an open setinterval_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 partsinterval_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.uIoc 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.uIoc 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 wheneverfis integrable on each interval; in particular, it works even if the measureμhas an atom atb; this rules outset.Iooandset.Iccintervals; - 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 nandv ntend tol, then for anys ∈ l',Ioc (u n) (v n)is eventually included ins.
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.uIcc 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
Integrability at an interval #
A function f is called interval integrable with respect to a measure μ on an unordered
interval a..b if it is integrable on both intervals (a, b] and (b, a]. One of these
intervals is always empty, so this property is equivalent to f being integrable on
(min a b, max a b].
Equations
- interval_integrable f μ a b = (measure_theory.integrable_on f (set.Ioc a b) μ ∧ measure_theory.integrable_on f (set.Ioc b a) μ)
A function is interval integrable with respect to a given measure μ on a..b if and
only if it is integrable on uIoc a b with respect to μ. This is an equivalent
definition of interval_integrable.
If a function is interval integrable with respect to a given measure μ on a..b then
it is integrable on uIoc a b with respect to μ.
If a function is integrable with respect to a given measure μ then it is interval integrable
with respect to μ on uIcc a b.
A continuous function on ℝ is interval_integrable with respect to any locally finite measure
ν on ℝ.
Let l' be a measurably generated filter; let l be a of filter such that each s ∈ l'
eventually includes Ioc u v as both u and v tend to l. Let μ be a measure finite at l'.
Suppose that f : ℝ → E has a finite limit at l' ⊓ μ.ae. Then f is interval integrable on
u..v provided that both u and v tend to l.
Typeclass instances allow Lean to find l' based on l but not vice versa, so
apply tendsto.eventually_interval_integrable_ae will generate goals filter ℝ and
tendsto_Ixx_class Ioc ?m_1 l'.
Let l' be a measurably generated filter; let l be a of filter such that each s ∈ l'
eventually includes Ioc u v as both u and v tend to l. Let μ be a measure finite at l'.
Suppose that f : ℝ → E has a finite limit at l. Then f is interval integrable on u..v
provided that both u and v tend to l.
Typeclass instances allow Lean to find l' based on l but not vice versa, so
apply tendsto.eventually_interval_integrable_ae will generate goals filter ℝ and
tendsto_Ixx_class Ioc ?m_1 l'.
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.
The interval integral ∫ x in a..b, f x ∂μ is defined
as ∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ. If a ≤ b, then it equals
∫ x in Ioc a b, f x ∂μ, otherwise it equals -∫ x in Ioc b a, f x ∂μ.
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.
If two functions are equal in the relevant interval, their interval integrals are also equal.
If μ is a finite measure then ∫ x in a..b, c ∂μ = (μ (Iic b) - μ (Iic a)) • c.
Lebesgue dominated convergence theorem for filters with a countable basis
Lebesgue dominated convergence theorem for series.
Continuity of interval integral with respect to a parameter, at a point within a set.
Given F : X → ℝ → E, assume F x is ae-measurable on [a, b] for x in a
neighborhood of x₀ within s and at x₀, and assume it is bounded by a function integrable
on [a, b] independent of x in a neighborhood of x₀ within s. If (λ x, F x t)
is continuous at x₀ within s for almost every t in [a, b]
then the same holds for (λ x, ∫ t in a..b, F x t ∂μ) s x₀.
Continuity of interval integral with respect to a parameter at a point.
Given F : X → ℝ → E, assume F x is ae-measurable on [a, b] for x in a
neighborhood of x₀, and assume it is bounded by a function integrable on
[a, b] independent of x in a neighborhood of x₀. If (λ x, F x t)
is continuous at x₀ for almost every t in [a, b]
then the same holds for (λ x, ∫ t in a..b, F x t ∂μ) s x₀.
Continuity of interval integral with respect to a parameter.
Given F : X → ℝ → E, assume each F x is ae-measurable on [a, b],
and assume it is bounded by a function integrable on [a, b] independent of x.
If (λ x, F x t) is continuous for almost every t in [a, b]
then the same holds for (λ x, ∫ t in a..b, F x t ∂μ) s x₀.
Note: this assumes that f is interval_integrable, in contrast to some other lemmas here.
If f is nonnegative and integrable on the unordered interval set.uIoc a b, then its
integral over a..b is positive if and only if a < b and the measure of
function.support f ∩ set.Ioc a b is positive.
If f is nonnegative a.e.-everywhere and it is integrable on the unordered interval
set.uIoc a b, then its integral over a..b is positive if and only if a < b and the
measure of function.support f ∩ set.Ioc a b is positive.
If f : ℝ → ℝ is integrable on (a, b] for real numbers a < b, and positive on the interior
of the interval, then its integral over a..b is strictly positive.
If f : ℝ → ℝ is strictly positive everywhere, and integrable on (a, b] for real numbers
a < b, then its integral over a..b is strictly positive. (See interval_integral_pos_of_pos_on
for a version only assuming positivity of f on (a, b) rather than everywhere.)
If f and g are two functions that are interval integrable on a..b, a ≤ b,
f x ≤ g x for a.e. x ∈ set.Ioc a b, and f x < g x on a subset of set.Ioc a b
of nonzero measure, then ∫ x in a..b, f x ∂μ < ∫ x in a..b, g x ∂μ.
If f and g are continuous on [a, b], a < b, f x ≤ g x on this interval, and
f c < g c at some point c ∈ [a, b], then ∫ x in a..b, f x < ∫ x in a..b, g x.
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, 𝓝[≥] 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_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.
- to_tendsto_Ixx_class : filter.tendsto_Ixx_class set.Ioc outer inner
- pure_le : has_pure.pure a ≤ outer
- le_nhds : inner ≤ nhds a
- meas_gen : filter.is_measurably_generated inner
An auxiliary typeclass for the Fundamental theorem of calculus, part 1. It is used to formulate
theorems that work simultaneously for left and right one-sided derivatives of ∫ x in u..v, f x.
Instances of this typeclass
- interval_integral.FTC_filter.pure
- interval_integral.FTC_filter.nhds_within_singleton
- interval_integral.FTC_filter.nhds
- interval_integral.FTC_filter.nhds_univ
- interval_integral.FTC_filter.nhds_left
- interval_integral.FTC_filter.nhds_right
- interval_integral.FTC_filter.nhds_Icc
- interval_integral.FTC_filter.nhds_uIcc
Fundamental theorem of calculus-1, local version for any measure.
Let filters l and l' be related by tendsto_Ixx_class Ioc.
If f has a finite limit c at l' ⊓ μ.ae, where μ is a measure
finite at l', then ∫ x in u..v, f x ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, 1 ∂μ) as both
u and v tend to l.
See also measure_integral_sub_linear_is_o_of_tendsto_ae for a version assuming
[FTC_filter a l l'] and [is_locally_finite_measure μ]. If l is one of 𝓝[≥] a,
𝓝[≤] a, 𝓝 a, then it's easier to apply the non-primed version.
The primed version also works, e.g., for l = l' = at_top.
We use integrals of constants instead of measures because this way it is easier to formulate
a statement that works in both cases u ≤ v and v ≤ u.
Fundamental theorem of calculus-1, local version for any measure.
Let filters l and l' be related by tendsto_Ixx_class Ioc.
If f has a finite limit c at l ⊓ μ.ae, where μ is a measure
finite at l, then ∫ x in u..v, f x ∂μ = μ (Ioc u v) • c + o(μ(Ioc u v)) as both
u and v tend to l so that u ≤ v.
See also measure_integral_sub_linear_is_o_of_tendsto_ae_of_le for a version assuming
[FTC_filter a l l'] and [is_locally_finite_measure μ]. If l is one of 𝓝[≥] a,
𝓝[≤] a, 𝓝 a, then it's easier to apply the non-primed version.
The primed version also works, e.g., for l = l' = at_top.
Fundamental theorem of calculus-1, local version for any measure.
Let filters l and l' be related by tendsto_Ixx_class Ioc.
If f has a finite limit c at l ⊓ μ.ae, where μ is a measure
finite at l, then ∫ x in u..v, f x ∂μ = -μ (Ioc v u) • c + o(μ(Ioc v u)) as both
u and v tend to l so that v ≤ u.
See also measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge for a version assuming
[FTC_filter a l l'] and [is_locally_finite_measure μ]. If l is one of 𝓝[≥] a,
𝓝[≤] a, 𝓝 a, then it's easier to apply the non-primed version.
The primed version also works, e.g., for l = l' = at_top.
Fundamental theorem of calculus-1, local version for any measure.
Let filters l and l' be related by [FTC_filter a l l']; let μ be a locally finite measure.
If f has a finite limit c at l' ⊓ μ.ae, then
∫ x in u..v, f x ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, 1 ∂μ) as both u and v tend to l.
See also measure_integral_sub_linear_is_o_of_tendsto_ae' for a version that also works, e.g., for
l = l' = at_top.
We use integrals of constants instead of measures because this way it is easier to formulate
a statement that works in both cases u ≤ v and v ≤ u.
Fundamental theorem of calculus-1, local version for any measure.
Let filters l and l' be related by [FTC_filter a l l']; let μ be a locally finite measure.
If f has a finite limit c at l' ⊓ μ.ae, then
∫ x in u..v, f x ∂μ = μ (Ioc u v) • c + o(μ(Ioc u v)) as both u and v tend to l.
See also measure_integral_sub_linear_is_o_of_tendsto_ae_of_le' for a version that also works,
e.g., for l = l' = at_top.
Fundamental theorem of calculus-1, local version for any measure.
Let filters l and l' be related by [FTC_filter a l l']; let μ be a locally finite measure.
If f has a finite limit c at l' ⊓ μ.ae, then
∫ x in u..v, f x ∂μ = -μ (Ioc v u) • c + o(μ(Ioc v u)) as both u and v tend to l.
See also measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge' for a version that also works,
e.g., for l = l' = at_top.
Fundamental theorem of calculus-1, strict derivative in both limits for a locally finite measure.
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.
Fundamental theorem of calculus-1, strict derivative in right endpoint for a locally finite measure.
Let f be a measurable function integrable on a..b. Let (lb, lb') be a pair of FTC_filters
around b. Suppose that f has a finite limit c at lb' ⊓ μ.ae.
Then ∫ x in a..v, f x ∂μ - ∫ x in a..u, f x ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, (1:ℝ) ∂μ)
as u and v tend to lb.
Fundamental theorem of calculus-1, strict derivative in left endpoint for a locally finite measure.
Let f be a measurable function integrable on a..b. Let (la, la') be a pair of FTC_filters
around a. Suppose that f has a finite limit c at la' ⊓ μ.ae.
Then ∫ x in v..b, f x ∂μ - ∫ x in u..b, f x ∂μ = -∫ x in u..v, c ∂μ + o(∫ x in u..v, (1:ℝ) ∂μ)
as u and v tend to la.
Fundamental theorem of calculus-1 for Lebesgue measure #
In this section we restate theorems from the previous section for Lebesgue measure.
In particular, we prove that ∫ x in u..v, f x is strictly differentiable in (u, v)
at (a, b) provided that f is integrable on a..b and is continuous at a and b.
Auxiliary is_o statements #
In this section we prove several lemmas that can be interpreted as strict differentiability of
(u, v) ↦ ∫ x in u..v, f x ∂μ in u and/or v at a filter. The statements use is_o because
we have no definition of has_strict_(f)deriv_at_filter in the library.