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:
_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 | 𝓝[Iic a] a | Iic b | 𝓝[Iic b] b |
| Ici a | 𝓝[Ioi a] a | Ici b | 𝓝[Ioi 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.
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 wheneverfis integrable on each interval; in particular, it works even if the measureμhas an atom atb; this rules outIooandIccintervals; - 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 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
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) μ)
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.
If μ is a finite measure then ∫ x in a..b, c ∂μ = (μ (Iic b) - μ (Iic a)) • c.
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 integral
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.
- 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.
There are four instances: (a, pure a, ⊥), (a, 𝓝[Ici a], 𝓝[Ioi a]),
(a, 𝓝[Iic a], 𝓝[Iic a]), and (a, 𝓝 a, 𝓝 a).
Equations
- _ = _
Equations
- _ = _
Equations
- _ = _
Equations
- _ = _
Equations
- _ = _
Equations
- _ = _
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 [locally_finite_measure μ]. If l is one of 𝓝[Ici a] a,
𝓝[Iic 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 [locally_finite_measure μ]. If l is one of 𝓝[Ici a] a,
𝓝[Iic 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 [locally_finite_measure μ]. If l is one of 𝓝[Ici a] a,
𝓝[Iic 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.
Fundamental theorem of calculus-1, local version. If f has a finite limit c almost surely at
l', where (l, l') is an FTC_filter pair around a, then
∫ x in u..v, f x ∂μ = (v - u) • c + o (v - u) as both u and v tend to l.
Fundamental theorem of calculus-1, strict differentiability at filter in both endpoints.
If f is a measurable function integrable on a..b, (la, la') is an FTC_filter pair around
a, and (lb, lb') is an FTC_filter pair around b, and 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 = (vb - ub) • cb - (va - ua) • ca +
o(∥va - ua∥ + ∥vb - ub∥) as ua and va tend to la while ub and vb tend to lb.
This lemma could've been formulated using has_strict_fderiv_at_filter if we had this
definition.
Fundamental theorem of calculus-1, strict differentiability at filter in both endpoints.
If f is a measurable function integrable on a..b, (lb, lb') is an FTC_filter pair
around b, and f has a finite limit c almost surely at lb', then
(∫ x in a..v, f x) - ∫ x in a..u, f x = (v - u) • c + o(∥v - u∥) as u and v tend to lb.
This lemma could've been formulated using has_strict_deriv_at_filter if we had this definition.
Fundamental theorem of calculus-1, strict differentiability at filter in both endpoints.
If f is a measurable function integrable on a..b, (la, la') is an FTC_filter pair
around a, and f has a finite limit c almost surely at la', then
(∫ x in v..b, f x) - ∫ x in u..b, f x = -(v - u) • c + o(∥v - u∥) as u and v tend to la.
This lemma could've been formulated using has_strict_deriv_at_filter if we had this definition.
Strict differentiability
In this section we prove that for a measurable function f integrable on a..b,
integral_has_strict_fderiv_at_of_tendsto_ae: the function(u, v) ↦ ∫ x in u..v, f xhas derivative(u, v) ↦ v • cb - u • caat(a, b)in the sense of strict differentiability provided thatftends tocaandcbalmost surely asxtendsto toaandb, respectively;integral_has_strict_fderiv_at: the function(u, v) ↦ ∫ x in u..v, f xhas derivative(u, v) ↦ v • f b - u • f aat(a, b)in the sense of strict differentiability provided thatfis continuous ataandb;integral_has_strict_deriv_at_of_tendsto_ae_right: the functionu ↦ ∫ x in a..u, f xhas derivativecatbin the sense of strict differentiability provided thatftends tocalmost surely asxtends tob;integral_has_strict_deriv_at_right: the functionu ↦ ∫ x in a..u, f xhas derivativef batbin the sense of strict differentiability provided thatfis continuous atb;integral_has_strict_deriv_at_of_tendsto_ae_left: the functionu ↦ ∫ x in u..b, f xhas derivative-catain the sense of strict differentiability provided thatftends tocalmost surely asxtends toa;integral_has_strict_deriv_at_left: the functionu ↦ ∫ x in u..b, f xhas derivative-f aatain the sense of strict differentiability provided thatfis continuous ata.
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f x has finite
limits ca and cb almost surely as x tends to a and b, respectively, then
(u, v) ↦ ∫ x in u..v, f x has derivative (u, v) ↦ v • cb - u • ca at (a, b)
in the sense of strict differentiability.
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f is continuous
at a and b, then (u, v) ↦ ∫ x in u..v, f x has derivative (u, v) ↦ v • cb - u • ca
at (a, b) in the sense of strict differentiability.
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f x has a finite
limit c almost surely at b, then u ↦ ∫ x in a..u, f x has derivative c at b in the sense
of strict differentiability.
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f is continuous
at b, then u ↦ ∫ x in a..u, f x has derivative f b at b in the sense of strict
differentiability.
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f x has a finite
limit c almost surely at a, then u ↦ ∫ x in u..b, f x has derivative -c at a in the sense
of strict differentiability.
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f is continuous
at a, then u ↦ ∫ x in u..b, f x has derivative -f a at a in the sense of strict
differentiability.
Fréchet differentiability
In this subsection we restate results from the previous subsection in terms of has_fderiv_at,
has_deriv_at, fderiv, and deriv.
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f x has finite
limits ca and cb almost surely as x tends to a and b, respectively, then
(u, v) ↦ ∫ x in u..v, f x has derivative (u, v) ↦ v • cb - u • ca at (a, b).
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f is continuous
at a and b, then (u, v) ↦ ∫ x in u..v, f x has derivative (u, v) ↦ v • cb - u • ca
at (a, b).
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f x has finite
limits ca and cb almost surely as x tends to a and b, respectively, then fderiv
derivative of (u, v) ↦ ∫ x in u..v, f x at (a, b) equals (u, v) ↦ v • cb - u • ca.
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f is continuous
at a and b, then fderiv derivative of (u, v) ↦ ∫ x in u..v, f x at (a, b) equals (u, v) ↦
v • cb - u • ca.
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f x has a finite
limit c almost surely at b, then u ↦ ∫ x in a..u, f x has derivative c at b.
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f is continuous
at b, then u ↦ ∫ x in a..u, f x has derivative f b at b.
Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f has a finite
limit c almost surely at b, then the derivative of u ↦ ∫ x in a..u, f x at b equals c.
Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f is continuous
at b, then the derivative of u ↦ ∫ x in a..u, f x at b equals f b.
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f x has a finite
limit c almost surely at a, then u ↦ ∫ x in u..b, f x has derivative -c at a.
Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f is continuous
at a, then u ↦ ∫ x in u..b, f x has derivative -f a at a.
Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f has a finite
limit c almost surely at a, then the derivative of u ↦ ∫ x in u..b, f x at a equals -c.
Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f is continuous
at a, then the derivative of u ↦ ∫ x in u..b, f x at a equals -f a.
One-sided derivatives
Let f be a measurable function integrable on a..b. The function (u, v) ↦ ∫ x in u..v, f x
has derivative (u, v) ↦ v • cb - u • ca within s × t at (a, b), where
s ∈ {Iic a, {a}, Ici a, univ} and t ∈ {Iic b, {b}, Ici b, univ} provided that f tends to ca
and cb almost surely at the filters la and lb from the following table.
| s | la | t | lb |
| ------- | ---- | --- | ---- |
| Iic a | 𝓝[Iic a] a | Iic b | 𝓝[Iic b] b |
| Ici a | 𝓝[Ioi a] a | Ici b | 𝓝[Ioi b] b |
| {a} | ⊥ | {b} | ⊥ |
| univ | 𝓝 a | univ | 𝓝 b |
Let f be a measurable function integrable on a..b. The function (u, v) ↦ ∫ x in u..v, f x
has derivative (u, v) ↦ v • f b - u • f a within s × t at (a, b), where
s ∈ {Iic a, {a}, Ici a, univ} and t ∈ {Iic b, {b}, Ici b, univ} provided that f tends to
f a and f b at the filters la and lb from the following table. In most cases this assumption
is definitionally equal continuous_at f _ or continuous_within_at f _ _.
| s | la | t | lb |
| ------- | ---- | --- | ---- |
| Iic a | 𝓝[Iic a] a | Iic b | 𝓝[Iic b] b |
| Ici a | 𝓝[Ioi a] a | Ici b | 𝓝[Ioi b] b |
| {a} | ⊥ | {b} | ⊥ |
| univ | 𝓝 a | univ | 𝓝 b |
An auxiliary tactic closing goals unique_diff_within_at ℝ s a where
s ∈ {Iic a, Ici a, univ}.
Let f be a measurable function integrable on a..b. Choose s ∈ {Iic a, Ici a, univ}
and t ∈ {Iic b, Ici b, univ}. Suppose that f tends to ca and cb almost surely at the filters
la and lb from the table below. Then fderiv_within ℝ (λ p, ∫ x in p.1..p.2, f x) (s.prod t)
is equal to (u, v) ↦ u • cb - v • ca.
| s | la | t | lb |
| ------- | ---- | --- | ---- |
| Iic a | 𝓝[Iic a] a | Iic b | 𝓝[Iic b] b |
| Ici a | 𝓝[Ioi a] a | Ici b | 𝓝[Ioi b] b |
| univ | 𝓝 a | univ | 𝓝 b |
Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x has a finite
limit c almost surely as x tends to b from the right or from the left,
then u ↦ ∫ x in a..u, f x has right (resp., left) derivative c at b.
Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x is continuous
from the left or from the right at b, then u ↦ ∫ x in a..u, f x has left (resp., right)
derivative f b at b.
Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x has a finite
limit c almost surely as x tends to b from the right or from the left, then the right
(resp., left) derivative of u ↦ ∫ x in a..u, f x at b equals c.
Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x is continuous
on the right or on the left at b, then the right (resp., left) derivative of
u ↦ ∫ x in a..u, f x at b equals f b.
Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x has a finite
limit c almost surely as x tends to a from the right or from the left,
then u ↦ ∫ x in u..b, f x has right (resp., left) derivative -c at a.
Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x is continuous
from the left or from the right at a, then u ↦ ∫ x in u..b, f x has left (resp., right)
derivative -f a at a.
Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x has a finite
limit c almost surely as x tends to a from the right or from the left, then the right
(resp., left) derivative of u ↦ ∫ x in u..b, f x at a equals -c.
Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x is continuous
on the right or on the left at a, then the right (resp., left) derivative of
u ↦ ∫ x in u..b, f x at a equals -f a.