mathlib3 documentation

measure_theory.integral.fund_thm_calculus

Fundamental Theorem of Calculus #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 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:

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:

We then derive additional integration techniques from FTC-2:

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.

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:

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

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.

source
@[class]
structure interval_integral.FTC_filter (a : out_param ℝ) (outer : filter ℝ) (inner : out_param (filter ℝ)) :
Prop

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
source
@[protected, instance]
def interval_integral.FTC_filter.pure (a : ℝ) :
interval_integral.FTC_filter a (has_pure.pure a) ⊥
source
@[protected, instance]
def interval_integral.FTC_filter.nhds_within_singleton (a : ℝ) :
interval_integral.FTC_filter a (nhds_within a {a}) ⊥
source
theorem interval_integral.FTC_filter.finite_at_inner {a : ℝ} (l : filter ℝ) {l' : out_param (filter ℝ)} [h : interval_integral.FTC_filter a l l'] {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] :
μ.finite_at_filter l'
source
@[protected, instance]
def interval_integral.FTC_filter.nhds (a : ℝ) :
interval_integral.FTC_filter a (nhds a) (nhds a)
source
@[protected, instance]
def interval_integral.FTC_filter.nhds_univ (a : ℝ) :
interval_integral.FTC_filter a (nhds_within a set.univ) (nhds a)
source
@[protected, instance]
def interval_integral.FTC_filter.nhds_left (a : ℝ) :
interval_integral.FTC_filter a (nhds_within a (set.Iic a)) (nhds_within a (set.Iic a))
source
@[protected, instance]
def interval_integral.FTC_filter.nhds_right (a : ℝ) :
interval_integral.FTC_filter a (nhds_within a (set.Ici a)) (nhds_within a (set.Ioi a))
source
@[protected, instance]
def interval_integral.FTC_filter.nhds_Icc {x a b : ℝ} [h : fact (x ∈ set.Icc a b)] :
interval_integral.FTC_filter x (nhds_within x (set.Icc a b)) (nhds_within x (set.Icc a b))
source
@[protected, instance]
def interval_integral.FTC_filter.nhds_uIcc {x a b : ℝ} [h : fact (x ∈ set.uIcc a b)] :
interval_integral.FTC_filter x (nhds_within x (set.uIcc a b)) (nhds_within x (set.uIcc a b))
source
theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae' {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {l l' : filter ℝ} {lt : filter ι} {μ : measure_theory.measure ℝ} {u v : ι → ℝ} [l'.is_measurably_generated] [filter.tendsto_Ixx_class set.Ioc l l'] (hfm : strongly_measurable_at_filter f l' μ) (hf : filter.tendsto f (l' ⊓ μ.ae) (nhds c)) (hl : μ.finite_at_filter l') (hu : filter.tendsto u lt l) (hv : filter.tendsto v lt l) :
(λ (t : ι), ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] λ (t : ι), ∫ (x : ℝ) in u t..v t, 1 ∂μ

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.

source
theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae_of_le' {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {l l' : filter ℝ} {lt : filter ι} {μ : measure_theory.measure ℝ} {u v : ι → ℝ} [l'.is_measurably_generated] [filter.tendsto_Ixx_class set.Ioc l l'] (hfm : strongly_measurable_at_filter f l' μ) (hf : filter.tendsto f (l' ⊓ μ.ae) (nhds c)) (hl : μ.finite_at_filter l') (hu : filter.tendsto u lt l) (hv : filter.tendsto v lt l) (huv : u ≤ᶠ[lt] v) :
(λ (t : ι), ∫ (x : ℝ) in u t..v t, f x ∂μ - (⇑μ (set.Ioc (u t) (v t))).to_real • c) =o[lt] λ (t : ι), (⇑μ (set.Ioc (u t) (v t))).to_real

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.

source
theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge' {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {l l' : filter ℝ} {lt : filter ι} {μ : measure_theory.measure ℝ} {u v : ι → ℝ} [l'.is_measurably_generated] [filter.tendsto_Ixx_class set.Ioc l l'] (hfm : strongly_measurable_at_filter f l' μ) (hf : filter.tendsto f (l' ⊓ μ.ae) (nhds c)) (hl : μ.finite_at_filter l') (hu : filter.tendsto u lt l) (hv : filter.tendsto v lt l) (huv : v ≤ᶠ[lt] u) :
(λ (t : ι), ∫ (x : ℝ) in u t..v t, f x ∂μ + (⇑μ (set.Ioc (v t) (u t))).to_real • c) =o[lt] λ (t : ι), (⇑μ (set.Ioc (v t) (u t))).to_real

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.

source
theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a : ℝ} {c : E} {l l' : filter ℝ} {lt : filter ι} {μ : measure_theory.measure ℝ} {u v : ι → ℝ} [measure_theory.is_locally_finite_measure μ] [interval_integral.FTC_filter a l l'] (hfm : strongly_measurable_at_filter f l' μ) (hf : filter.tendsto f (l' ⊓ μ.ae) (nhds c)) (hu : filter.tendsto u lt l) (hv : filter.tendsto v lt l) :
(λ (t : ι), ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] λ (t : ι), ∫ (x : ℝ) in u t..v t, 1 ∂μ

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.

source
theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae_of_le {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a : ℝ} {c : E} {l l' : filter ℝ} {lt : filter ι} {μ : measure_theory.measure ℝ} {u v : ι → ℝ} [measure_theory.is_locally_finite_measure μ] [interval_integral.FTC_filter a l l'] (hfm : strongly_measurable_at_filter f l' μ) (hf : filter.tendsto f (l' ⊓ μ.ae) (nhds c)) (hu : filter.tendsto u lt l) (hv : filter.tendsto v lt l) (huv : u ≤ᶠ[lt] v) :
(λ (t : ι), ∫ (x : ℝ) in u t..v t, f x ∂μ - (⇑μ (set.Ioc (u t) (v t))).to_real • c) =o[lt] λ (t : ι), (⇑μ (set.Ioc (u t) (v t))).to_real

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.

source
theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a : ℝ} {c : E} {l l' : filter ℝ} {lt : filter ι} {μ : measure_theory.measure ℝ} {u v : ι → ℝ} [measure_theory.is_locally_finite_measure μ] [interval_integral.FTC_filter a l l'] (hfm : strongly_measurable_at_filter f l' μ) (hf : filter.tendsto f (l' ⊓ μ.ae) (nhds c)) (hu : filter.tendsto u lt l) (hv : filter.tendsto v lt l) (huv : v ≤ᶠ[lt] u) :
(λ (t : ι), ∫ (x : ℝ) in u t..v t, f x ∂μ + (⇑μ (set.Ioc (v t) (u t))).to_real • c) =o[lt] λ (t : ι), (⇑μ (set.Ioc (v t) (u t))).to_real

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.

source
theorem interval_integral.measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {ca cb : E} {la la' lb lb' : filter ℝ} {lt : filter ι} {μ : measure_theory.measure ℝ} {ua va ub vb : ι → ℝ} [interval_integral.FTC_filter a la la'] [interval_integral.FTC_filter b lb lb'] [measure_theory.is_locally_finite_measure μ] (hab : interval_integrable f μ a b) (hmeas_a : strongly_measurable_at_filter f la' μ) (hmeas_b : strongly_measurable_at_filter f lb' μ) (ha_lim : filter.tendsto f (la' ⊓ μ.ae) (nhds ca)) (hb_lim : filter.tendsto f (lb' ⊓ μ.ae) (nhds cb)) (hua : filter.tendsto ua lt la) (hva : filter.tendsto va lt la) (hub : filter.tendsto ub lt lb) (hvb : filter.tendsto vb lt lb) :
(λ (t : ι), ∫ (x : ℝ) in va t..vb t, f x ∂μ - ∫ (x : ℝ) in ua t..ub t, f x ∂μ - (∫ (x : ℝ) in ub t..vb t, cb ∂μ - ∫ (x : ℝ) in ua t..va t, ca ∂μ)) =o[lt] λ (t : ι), ‖∫ (x : ℝ) in ua t..va t, 1 ∂μ‖ + ‖∫ (x : ℝ) in ub t..vb t, 1 ∂μ‖

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.

source
theorem interval_integral.measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {c : E} {lb lb' : filter ℝ} {lt : filter ι} {μ : measure_theory.measure ℝ} {u v : ι → ℝ} [interval_integral.FTC_filter b lb lb'] [measure_theory.is_locally_finite_measure μ] (hab : interval_integrable f μ a b) (hmeas : strongly_measurable_at_filter f lb' μ) (hf : filter.tendsto f (lb' ⊓ μ.ae) (nhds c)) (hu : filter.tendsto u lt lb) (hv : filter.tendsto v lt lb) :
(λ (t : ι), ∫ (x : ℝ) in a..v t, f x ∂μ - ∫ (x : ℝ) in a..u t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] λ (t : ι), ∫ (x : ℝ) in u t..v t, 1 ∂μ

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.

source
theorem interval_integral.measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_left {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {c : E} {la la' : filter ℝ} {lt : filter ι} {μ : measure_theory.measure ℝ} {u v : ι → ℝ} [interval_integral.FTC_filter a la la'] [measure_theory.is_locally_finite_measure μ] (hab : interval_integrable f μ a b) (hmeas : strongly_measurable_at_filter f la' μ) (hf : filter.tendsto f (la' ⊓ μ.ae) (nhds c)) (hu : filter.tendsto u lt la) (hv : filter.tendsto v lt la) :
(λ (t : ι), ∫ (x : ℝ) in v t..b, f x ∂μ - ∫ (x : ℝ) in u t..b, f x ∂μ + ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] λ (t : ι), ∫ (x : ℝ) in u t..v t, 1 ∂μ

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.

source
theorem interval_integral.integral_sub_linear_is_o_of_tendsto_ae {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {l l' : filter ℝ} {lt : filter ι} {a : ℝ} [interval_integral.FTC_filter a l l'] (hfm : strongly_measurable_at_filter f l' measure_theory.measure_space.volume) (hf : filter.tendsto f (l' ⊓ measure_theory.measure_space.volume.ae) (nhds c)) {u v : ι → ℝ} (hu : filter.tendsto u lt l) (hv : filter.tendsto v lt l) :
(λ (t : ι), (∫ (x : ℝ) in u t..v t, f x) - (v t - u t) • c) =o[lt] (v - u)

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.

source
theorem interval_integral.integral_sub_integral_sub_linear_is_o_of_tendsto_ae {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {ca cb : E} {la la' lb lb' : filter ℝ} {lt : filter ι} {a b : ℝ} {ua ub va vb : ι → ℝ} [interval_integral.FTC_filter a la la'] [interval_integral.FTC_filter b lb lb'] (hab : interval_integrable f measure_theory.measure_space.volume a b) (hmeas_a : strongly_measurable_at_filter f la' measure_theory.measure_space.volume) (hmeas_b : strongly_measurable_at_filter f lb' measure_theory.measure_space.volume) (ha_lim : filter.tendsto f (la' ⊓ measure_theory.measure_space.volume.ae) (nhds ca)) (hb_lim : filter.tendsto f (lb' ⊓ measure_theory.measure_space.volume.ae) (nhds cb)) (hua : filter.tendsto ua lt la) (hva : filter.tendsto va lt la) (hub : filter.tendsto ub lt lb) (hvb : filter.tendsto vb lt lb) :
(λ (t : ι), ((∫ (x : ℝ) in va t..vb t, f x) - ∫ (x : ℝ) in ua t..ub t, f x) - ((vb t - ub t) • cb - (va t - ua t) • ca)) =o[lt] λ (t : ι), ‖va t - ua t‖ + ‖vb t - ub t‖

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.

source
theorem interval_integral.integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {lb lb' : filter ℝ} {lt : filter ι} {a b : ℝ} {u v : ι → ℝ} [interval_integral.FTC_filter b lb lb'] (hab : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f lb' measure_theory.measure_space.volume) (hf : filter.tendsto f (lb' ⊓ measure_theory.measure_space.volume.ae) (nhds c)) (hu : filter.tendsto u lt lb) (hv : filter.tendsto v lt lb) :
(λ (t : ι), ((∫ (x : ℝ) in a..v t, f x) - ∫ (x : ℝ) in a..u t, f x) - (v t - u t) • c) =o[lt] (v - u)

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.

source
theorem interval_integral.integral_sub_integral_sub_linear_is_o_of_tendsto_ae_left {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {la la' : filter ℝ} {lt : filter ι} {a b : ℝ} {u v : ι → ℝ} [interval_integral.FTC_filter a la la'] (hab : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f la' measure_theory.measure_space.volume) (hf : filter.tendsto f (la' ⊓ measure_theory.measure_space.volume.ae) (nhds c)) (hu : filter.tendsto u lt la) (hv : filter.tendsto v lt la) :
(λ (t : ι), ((∫ (x : ℝ) in v t..b, f x) - ∫ (x : ℝ) in u t..b, f x) + (v t - u t) • c) =o[lt] (v - u)

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,

source
theorem interval_integral.integral_has_strict_fderiv_at_of_tendsto_ae {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {ca cb : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas_a : strongly_measurable_at_filter f (nhds a) measure_theory.measure_space.volume) (hmeas_b : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (ha : filter.tendsto f (nhds a ⊓ measure_theory.measure_space.volume.ae) (nhds ca)) (hb : filter.tendsto f (nhds b ⊓ measure_theory.measure_space.volume.ae) (nhds cb)) :
has_strict_fderiv_at (λ (p : ℝ × ℝ), ∫ (x : ℝ) in p.fst..p.snd, f x) ((continuous_linear_map.snd ℝ ℝ ℝ).smul_right cb - (continuous_linear_map.fst ℝ ℝ ℝ).smul_right ca) (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 (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.

source
theorem interval_integral.integral_has_strict_fderiv_at {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas_a : strongly_measurable_at_filter f (nhds a) measure_theory.measure_space.volume) (hmeas_b : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (ha : continuous_at f a) (hb : continuous_at f b) :
has_strict_fderiv_at (λ (p : ℝ × ℝ), ∫ (x : ℝ) in p.fst..p.snd, f x) ((continuous_linear_map.snd ℝ ℝ ℝ).smul_right (f b) - (continuous_linear_map.fst ℝ ℝ ℝ).smul_right (f a)) (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) in the sense of strict differentiability.

source
theorem interval_integral.integral_has_strict_deriv_at_of_tendsto_ae_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (hb : filter.tendsto f (nhds b ⊓ measure_theory.measure_space.volume.ae) (nhds c)) :
has_strict_deriv_at (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) c b

First Fundamental Theorem of Calculus: 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.

source
theorem interval_integral.integral_has_strict_deriv_at_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (hb : continuous_at f b) :
has_strict_deriv_at (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) (f b) 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 in the sense of strict differentiability.

source
theorem interval_integral.integral_has_strict_deriv_at_of_tendsto_ae_left {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds a) measure_theory.measure_space.volume) (ha : filter.tendsto f (nhds a ⊓ measure_theory.measure_space.volume.ae) (nhds c)) :
has_strict_deriv_at (λ (u : ℝ), ∫ (x : ℝ) in u..b, f x) (-c) a

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.

source
theorem interval_integral.integral_has_strict_deriv_at_left {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds a) measure_theory.measure_space.volume) (ha : continuous_at f a) :
has_strict_deriv_at (λ (u : ℝ), ∫ (x : ℝ) in u..b, f x) (-f a) 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 in the sense of strict differentiability.

source
theorem continuous.integral_has_strict_deriv_at {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} (hf : continuous f) (a b : ℝ) :
has_strict_deriv_at (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) (f b) b

Fundamental theorem of calculus-1: if f : ℝ → E is continuous, then u ↦ ∫ x in a..u, f x has derivative f b at b in the sense of strict differentiability.

source
theorem continuous.deriv_integral {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] (f : ℝ → E) (hf : continuous f) (a b : ℝ) :
deriv (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) b = f b

Fundamental theorem of calculus-1: if f : ℝ → E is continuous, then the derivative of u ↦ ∫ x in a..u, f x at b is f b.

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.

source
theorem interval_integral.integral_has_fderiv_at_of_tendsto_ae {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {ca cb : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas_a : strongly_measurable_at_filter f (nhds a) measure_theory.measure_space.volume) (hmeas_b : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (ha : filter.tendsto f (nhds a ⊓ measure_theory.measure_space.volume.ae) (nhds ca)) (hb : filter.tendsto f (nhds b ⊓ measure_theory.measure_space.volume.ae) (nhds cb)) :
has_fderiv_at (λ (p : ℝ × ℝ), ∫ (x : ℝ) in p.fst..p.snd, f x) ((continuous_linear_map.snd ℝ ℝ ℝ).smul_right cb - (continuous_linear_map.fst ℝ ℝ ℝ).smul_right ca) (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 (u, v) ↦ ∫ x in u..v, f x has derivative (u, v) ↦ v • cb - u • ca at (a, b).

source
theorem interval_integral.integral_has_fderiv_at {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas_a : strongly_measurable_at_filter f (nhds a) measure_theory.measure_space.volume) (hmeas_b : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (ha : continuous_at f a) (hb : continuous_at f b) :
has_fderiv_at (λ (p : ℝ × ℝ), ∫ (x : ℝ) in p.fst..p.snd, f x) ((continuous_linear_map.snd ℝ ℝ ℝ).smul_right (f b) - (continuous_linear_map.fst ℝ ℝ ℝ).smul_right (f a)) (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).

source
theorem interval_integral.fderiv_integral_of_tendsto_ae {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {ca cb : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas_a : strongly_measurable_at_filter f (nhds a) measure_theory.measure_space.volume) (hmeas_b : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (ha : filter.tendsto f (nhds a ⊓ measure_theory.measure_space.volume.ae) (nhds ca)) (hb : filter.tendsto f (nhds b ⊓ measure_theory.measure_space.volume.ae) (nhds cb)) :
fderiv ℝ (λ (p : ℝ × ℝ), ∫ (x : ℝ) in p.fst..p.snd, f x) (a, b) = (continuous_linear_map.snd ℝ ℝ ℝ).smul_right cb - (continuous_linear_map.fst ℝ ℝ ℝ).smul_right ca

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.

source
theorem interval_integral.fderiv_integral {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas_a : strongly_measurable_at_filter f (nhds a) measure_theory.measure_space.volume) (hmeas_b : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (ha : continuous_at f a) (hb : continuous_at f b) :
fderiv ℝ (λ (p : ℝ × ℝ), ∫ (x : ℝ) in p.fst..p.snd, f x) (a, b) = (continuous_linear_map.snd ℝ ℝ ℝ).smul_right (f b) - (continuous_linear_map.fst ℝ ℝ ℝ).smul_right (f a)

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.

source
theorem interval_integral.integral_has_deriv_at_of_tendsto_ae_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (hb : filter.tendsto f (nhds b ⊓ measure_theory.measure_space.volume.ae) (nhds c)) :
has_deriv_at (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) c 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 b, then u ↦ ∫ x in a..u, f x has derivative c at b.

source
theorem interval_integral.integral_has_deriv_at_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (hb : continuous_at f b) :
has_deriv_at (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) (f b) 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.

source
theorem interval_integral.deriv_integral_of_tendsto_ae_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (hb : filter.tendsto f (nhds b ⊓ measure_theory.measure_space.volume.ae) (nhds c)) :
deriv (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) b = c

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.

source
theorem interval_integral.deriv_integral_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds b) measure_theory.measure_space.volume) (hb : continuous_at f b) :
deriv (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) b = f b

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.

source
theorem interval_integral.integral_has_deriv_at_of_tendsto_ae_left {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds a) measure_theory.measure_space.volume) (ha : filter.tendsto f (nhds a ⊓ measure_theory.measure_space.volume.ae) (nhds c)) :
has_deriv_at (λ (u : ℝ), ∫ (x : ℝ) in u..b, f x) (-c) a

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.

source
theorem interval_integral.integral_has_deriv_at_left {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds a) measure_theory.measure_space.volume) (ha : continuous_at f a) :
has_deriv_at (λ (u : ℝ), ∫ (x : ℝ) in u..b, f x) (-f a) 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.

source
theorem interval_integral.deriv_integral_of_tendsto_ae_left {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds a) measure_theory.measure_space.volume) (hb : filter.tendsto f (nhds a ⊓ measure_theory.measure_space.volume.ae) (nhds c)) :
deriv (λ (u : ℝ), ∫ (x : ℝ) in u..b, f x) a = -c

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.

source
theorem interval_integral.deriv_integral_left {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : strongly_measurable_at_filter f (nhds a) measure_theory.measure_space.volume) (hb : continuous_at f a) :
deriv (λ (u : ℝ), ∫ (x : ℝ) in u..b, f x) a = -f a

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 #

source
theorem interval_integral.integral_has_fderiv_within_at_of_tendsto_ae {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {ca cb : E} {la lb : filter ℝ} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) {s t : set ℝ} [interval_integral.FTC_filter a (nhds_within a s) la] [interval_integral.FTC_filter b (nhds_within b t) lb] (hmeas_a : strongly_measurable_at_filter f la measure_theory.measure_space.volume) (hmeas_b : strongly_measurable_at_filter f lb measure_theory.measure_space.volume) (ha : filter.tendsto f (la ⊓ measure_theory.measure_space.volume.ae) (nhds ca)) (hb : filter.tendsto f (lb ⊓ measure_theory.measure_space.volume.ae) (nhds cb)) :
has_fderiv_within_at (λ (p : ℝ × ℝ), ∫ (x : ℝ) in p.fst..p.snd, f x) ((continuous_linear_map.snd ℝ ℝ ℝ).smul_right cb - (continuous_linear_map.fst ℝ ℝ ℝ).smul_right ca) (s ×ˢ t) (a, 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 • 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 𝓝[≤] a Iic b 𝓝[≤] b
Ici a 𝓝[>] a Ici b 𝓝[>] b
{a} ⊥ {b} ⊥
univ 𝓝 a univ 𝓝 b
source
theorem interval_integral.integral_has_fderiv_within_at {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {la lb : filter ℝ} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas_a : strongly_measurable_at_filter f la measure_theory.measure_space.volume) (hmeas_b : strongly_measurable_at_filter f lb measure_theory.measure_space.volume) {s t : set ℝ} [interval_integral.FTC_filter a (nhds_within a s) la] [interval_integral.FTC_filter b (nhds_within b t) lb] (ha : filter.tendsto f la (nhds (f a))) (hb : filter.tendsto f lb (nhds (f b))) :
has_fderiv_within_at (λ (p : ℝ × ℝ), ∫ (x : ℝ) in p.fst..p.snd, f x) ((continuous_linear_map.snd ℝ ℝ ℝ).smul_right (f b) - (continuous_linear_map.fst ℝ ℝ ℝ).smul_right (f a)) (s ×ˢ t) (a, 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 𝓝[≤] a Iic b 𝓝[≤] b
Ici a 𝓝[>] a Ici b 𝓝[>] b
{a} ⊥ {b} ⊥
univ 𝓝 a univ 𝓝 b
source
meta def interval_integral.unique_diff_within_at_Ici_Iic_univ  :
tactic unit

An auxiliary tactic closing goals unique_diff_within_at ℝ s a where s ∈ {Iic a, Ici a, univ}.

source
theorem interval_integral.fderiv_within_integral_of_tendsto_ae {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {ca cb : E} {la lb : filter ℝ} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) (hmeas_a : strongly_measurable_at_filter f la measure_theory.measure_space.volume) (hmeas_b : strongly_measurable_at_filter f lb measure_theory.measure_space.volume) {s t : set ℝ} [interval_integral.FTC_filter a (nhds_within a s) la] [interval_integral.FTC_filter b (nhds_within b t) lb] (ha : filter.tendsto f (la ⊓ measure_theory.measure_space.volume.ae) (nhds ca)) (hb : filter.tendsto f (lb ⊓ measure_theory.measure_space.volume.ae) (nhds cb)) (hs : unique_diff_within_at ℝ s a . "unique_diff_within_at_Ici_Iic_univ") (ht : unique_diff_within_at ℝ t b . "unique_diff_within_at_Ici_Iic_univ") :
fderiv_within ℝ (λ (p : ℝ × ℝ), ∫ (x : ℝ) in p.fst..p.snd, f x) (s ×ˢ t) (a, b) = (continuous_linear_map.snd ℝ ℝ ℝ).smul_right cb - (continuous_linear_map.fst ℝ ℝ ℝ).smul_right ca

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 ×ˢ t) is equal to (u, v) ↦ u • cb - v • ca.

s la t lb
Iic a 𝓝[≤] a Iic b 𝓝[≤] b
Ici a 𝓝[>] a Ici b 𝓝[>] b
{a} ⊥ {b} ⊥
univ 𝓝 a univ 𝓝 b
source
theorem interval_integral.integral_has_deriv_within_at_of_tendsto_ae_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) {s t : set ℝ} [interval_integral.FTC_filter b (nhds_within b s) (nhds_within b t)] (hmeas : strongly_measurable_at_filter f (nhds_within b t) measure_theory.measure_space.volume) (hb : filter.tendsto f (nhds_within b t ⊓ measure_theory.measure_space.volume.ae) (nhds c)) :
has_deriv_within_at (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) c s 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.

source
theorem interval_integral.integral_has_deriv_within_at_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) {s t : set ℝ} [interval_integral.FTC_filter b (nhds_within b s) (nhds_within b t)] (hmeas : strongly_measurable_at_filter f (nhds_within b t) measure_theory.measure_space.volume) (hb : continuous_within_at f t b) :
has_deriv_within_at (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) (f b) s 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.

source
theorem interval_integral.deriv_within_integral_of_tendsto_ae_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) {s t : set ℝ} [interval_integral.FTC_filter b (nhds_within b s) (nhds_within b t)] (hmeas : strongly_measurable_at_filter f (nhds_within b t) measure_theory.measure_space.volume) (hb : filter.tendsto f (nhds_within b t ⊓ measure_theory.measure_space.volume.ae) (nhds c)) (hs : unique_diff_within_at ℝ s b . "unique_diff_within_at_Ici_Iic_univ") :
deriv_within (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) s b = c

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.

source
theorem interval_integral.deriv_within_integral_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) {s t : set ℝ} [interval_integral.FTC_filter b (nhds_within b s) (nhds_within b t)] (hmeas : strongly_measurable_at_filter f (nhds_within b t) measure_theory.measure_space.volume) (hb : continuous_within_at f t b) (hs : unique_diff_within_at ℝ s b . "unique_diff_within_at_Ici_Iic_univ") :
deriv_within (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) s b = f b

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.

source
theorem interval_integral.integral_has_deriv_within_at_of_tendsto_ae_left {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) {s t : set ℝ} [interval_integral.FTC_filter a (nhds_within a s) (nhds_within a t)] (hmeas : strongly_measurable_at_filter f (nhds_within a t) measure_theory.measure_space.volume) (ha : filter.tendsto f (nhds_within a t ⊓ measure_theory.measure_space.volume.ae) (nhds c)) :
has_deriv_within_at (λ (u : ℝ), ∫ (x : ℝ) in u..b, f x) (-c) s 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 u ↦ ∫ x in u..b, f x has right (resp., left) derivative -c at a.

source
theorem interval_integral.integral_has_deriv_within_at_left {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) {s t : set ℝ} [interval_integral.FTC_filter a (nhds_within a s) (nhds_within a t)] (hmeas : strongly_measurable_at_filter f (nhds_within a t) measure_theory.measure_space.volume) (ha : continuous_within_at f t a) :
has_deriv_within_at (λ (u : ℝ), ∫ (x : ℝ) in u..b, f x) (-f a) s 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.

source
theorem interval_integral.deriv_within_integral_of_tendsto_ae_left {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) {s t : set ℝ} [interval_integral.FTC_filter a (nhds_within a s) (nhds_within a t)] (hmeas : strongly_measurable_at_filter f (nhds_within a t) measure_theory.measure_space.volume) (ha : filter.tendsto f (nhds_within a t ⊓ measure_theory.measure_space.volume.ae) (nhds c)) (hs : unique_diff_within_at ℝ s a . "unique_diff_within_at_Ici_Iic_univ") :
deriv_within (λ (u : ℝ), ∫ (x : ℝ) in u..b, f x) s a = -c

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.

source
theorem interval_integral.deriv_within_integral_left {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hf : interval_integrable f measure_theory.measure_space.volume a b) {s t : set ℝ} [interval_integral.FTC_filter a (nhds_within a s) (nhds_within a t)] (hmeas : strongly_measurable_at_filter f (nhds_within a t) measure_theory.measure_space.volume) (ha : continuous_within_at f t a) (hs : unique_diff_within_at ℝ s a . "unique_diff_within_at_Ici_Iic_univ") :
deriv_within (λ (u : ℝ), ∫ (x : ℝ) in u..b, f x) s a = -f a

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.

source
theorem interval_integral.differentiable_on_integral_of_continuous {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a : ℝ} {s : set ℝ} (hintg : ∀ (x : ℝ), x ∈ s → interval_integrable f measure_theory.measure_space.volume a x) (hcont : continuous f) :
differentiable_on ℝ (λ (u : ℝ), ∫ (x : ℝ) in a..u, f x) s

The integral of a continuous function is differentiable on a real set s.

Fundamental theorem of calculus, part 2 #

This section contains theorems pertaining to FTC-2 for interval integrals, i.e., the assertion that ∫ x in a..b, f' x = f b - f a under suitable assumptions.

The most classical version of this theorem assumes that f' is continuous. However, this is unnecessarily strong: the result holds if f' is just integrable. We prove the strong version, following Rudin, Real and Complex Analysis (Theorem 7.21). The proof is first given for real-valued functions, and then deduced for functions with a general target space. For a real-valued function g, it suffices to show that g b - g a ≤ (∫ x in a..b, g' x) + ε for all positive ε. To prove this, choose a lower-semicontinuous function G' with g' < G' and with integral close to that of g' (its existence is guaranteed by the Vitali-Carathéodory theorem). It satisfies g t - g a ≤ ∫ x in a..t, G' x for all t ∈ [a, b]: this inequality holds at a, and if it holds at t then it holds for u close to t on its right, as the left hand side increases by g u - g t ∼ (u -t) g' t, while the right hand side increases by ∫ x in t..u, G' x which is roughly at least ∫ x in t..u, G' t = (u - t) G' t, by lower semicontinuity. As g' t < G' t, this gives the conclusion. One can therefore push progressively this inequality to the right until the point b, where it gives the desired conclusion.

source
theorem interval_integral.sub_le_integral_of_has_deriv_right_of_le_Ico {a b : ℝ} {g' g φ : ℝ → ℝ} (hab : a ≤ b) (hcont : continuous_on g (set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ico a b → has_deriv_within_at g (g' x) (set.Ioi x) x) (φint : measure_theory.integrable_on φ (set.Icc a b) measure_theory.measure_space.volume) (hφg : ∀ (x : ℝ), x ∈ set.Ico a b → g' x ≤ φ x) :
g b - g a ≤ ∫ (y : ℝ) in a..b, φ y

Hard part of FTC-2 for integrable derivatives, real-valued functions: one has g b - g a ≤ ∫ y in a..b, g' y when g' is integrable. Auxiliary lemma in the proof of integral_eq_sub_of_has_deriv_right_of_le. We give the slightly more general version that g b - g a ≤ ∫ y in a..b, φ y when g' ≤ φ and φ is integrable (even if g' is not known to be integrable). Version assuming that g is differentiable on [a, b).

source
theorem interval_integral.sub_le_integral_of_has_deriv_right_of_le {a b : ℝ} {g' g φ : ℝ → ℝ} (hab : a ≤ b) (hcont : continuous_on g (set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_within_at g (g' x) (set.Ioi x) x) (φint : measure_theory.integrable_on φ (set.Icc a b) measure_theory.measure_space.volume) (hφg : ∀ (x : ℝ), x ∈ set.Ioo a b → g' x ≤ φ x) :
g b - g a ≤ ∫ (y : ℝ) in a..b, φ y

Hard part of FTC-2 for integrable derivatives, real-valued functions: one has g b - g a ≤ ∫ y in a..b, g' y when g' is integrable. Auxiliary lemma in the proof of integral_eq_sub_of_has_deriv_right_of_le. We give the slightly more general version that g b - g a ≤ ∫ y in a..b, φ y when g' ≤ φ and φ is integrable (even if g' is not known to be integrable). Version assuming that g is differentiable on (a, b).

source
theorem interval_integral.integral_le_sub_of_has_deriv_right_of_le {a b : ℝ} {g' g φ : ℝ → ℝ} (hab : a ≤ b) (hcont : continuous_on g (set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_within_at g (g' x) (set.Ioi x) x) (φint : measure_theory.integrable_on φ (set.Icc a b) measure_theory.measure_space.volume) (hφg : ∀ (x : ℝ), x ∈ set.Ioo a b → φ x ≤ g' x) :
∫ (y : ℝ) in a..b, φ y ≤ g b - g a

Auxiliary lemma in the proof of integral_eq_sub_of_has_deriv_right_of_le.

source
theorem interval_integral.integral_eq_sub_of_has_deriv_right_of_le_real {a b : ℝ} {g' g : ℝ → ℝ} (hab : a ≤ b) (hcont : continuous_on g (set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_within_at g (g' x) (set.Ioi x) x) (g'int : measure_theory.integrable_on g' (set.Icc a b) measure_theory.measure_space.volume) :
∫ (y : ℝ) in a..b, g' y = g b - g a

Auxiliary lemma in the proof of integral_eq_sub_of_has_deriv_right_of_le: real version

source
theorem interval_integral.integral_eq_sub_of_has_deriv_right_of_le {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hab : a ≤ b) (hcont : continuous_on f (set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_within_at f (f' x) (set.Ioi x) x) (f'int : interval_integrable f' measure_theory.measure_space.volume a b) :
∫ (y : ℝ) in a..b, f' y = f b - f a

Fundamental theorem of calculus-2: If f : ℝ → E is continuous on [a, b] (where a ≤ b) and has a right derivative at f' x for all x in (a, b), and f' is integrable on [a, b], then ∫ y in a..b, f' y equals f b - f a.

source
theorem interval_integral.integral_eq_sub_of_has_deriv_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hcont : continuous_on f (set.uIcc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ioo (linear_order.min a b) (linear_order.max a b) → has_deriv_within_at f (f' x) (set.Ioi x) x) (hint : interval_integrable f' measure_theory.measure_space.volume a b) :
∫ (y : ℝ) in a..b, f' y = f b - f a

Fundamental theorem of calculus-2: If f : ℝ → E is continuous on [a, b] and has a right derivative at f' x for all x in [a, b), and f' is integrable on [a, b] then ∫ y in a..b, f' y equals f b - f a.

source
theorem interval_integral.integral_eq_sub_of_has_deriv_at_of_le {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hab : a ≤ b) (hcont : continuous_on f (set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at f (f' x) x) (hint : interval_integrable f' measure_theory.measure_space.volume a b) :
∫ (y : ℝ) in a..b, f' y = f b - f a

Fundamental theorem of calculus-2: If f : ℝ → E is continuous on [a, b] (where a ≤ b) and has a derivative at f' x for all x in (a, b), and f' is integrable on [a, b], then ∫ y in a..b, f' y equals f b - f a.

source
theorem interval_integral.integral_eq_sub_of_has_deriv_at {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hderiv : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at f (f' x) x) (hint : interval_integrable f' measure_theory.measure_space.volume a b) :
∫ (y : ℝ) in a..b, f' y = f b - f a

Fundamental theorem of calculus-2: If f : ℝ → E has a derivative at f' x for all x in [a, b] and f' is integrable on [a, b], then ∫ y in a..b, f' y equals f b - f a.

source
theorem interval_integral.integral_eq_sub_of_has_deriv_at_of_tendsto {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} (hab : a < b) {fa fb : E} (hderiv : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at f (f' x) x) (hint : interval_integrable f' measure_theory.measure_space.volume a b) (ha : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds fa)) (hb : filter.tendsto f (nhds_within b (set.Iio b)) (nhds fb)) :
∫ (y : ℝ) in a..b, f' y = fb - fa
source
theorem interval_integral.integral_deriv_eq_sub {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hderiv : ∀ (x : ℝ), x ∈ set.uIcc a b → differentiable_at ℝ f x) (hint : interval_integrable (deriv f) measure_theory.measure_space.volume a b) :
∫ (y : ℝ) in a..b, deriv f y = f b - f a

Fundamental theorem of calculus-2: If f : ℝ → E is differentiable at every x in [a, b] and its derivative is integrable on [a, b], then ∫ y in a..b, deriv f y equals f b - f a.

source
theorem interval_integral.integral_deriv_eq_sub' {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {a b : ℝ} {f' : ℝ → E} (f : ℝ → E) (hderiv : deriv f = f') (hdiff : ∀ (x : ℝ), x ∈ set.uIcc a b → differentiable_at ℝ f x) (hcont : continuous_on f' (set.uIcc a b)) :
∫ (y : ℝ) in a..b, f' y = f b - f a

Automatic integrability for nonnegative derivatives #

source
theorem interval_integral.integrable_on_deriv_right_of_nonneg {a b : ℝ} {g' g : ℝ → ℝ} (hcont : continuous_on g (set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_within_at g (g' x) (set.Ioi x) x) (g'pos : ∀ (x : ℝ), x ∈ set.Ioo a b → 0 ≤ g' x) :
measure_theory.integrable_on g' (set.Ioc a b) measure_theory.measure_space.volume

When the right derivative of a function is nonnegative, then it is automatically integrable.

source
theorem interval_integral.integrable_on_deriv_of_nonneg {a b : ℝ} {g' g : ℝ → ℝ} (hcont : continuous_on g (set.Icc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at g (g' x) x) (g'pos : ∀ (x : ℝ), x ∈ set.Ioo a b → 0 ≤ g' x) :
measure_theory.integrable_on g' (set.Ioc a b) measure_theory.measure_space.volume

When the derivative of a function is nonnegative, then it is automatically integrable, Ioc version.

source
theorem interval_integral.interval_integrable_deriv_of_nonneg {a b : ℝ} {g' g : ℝ → ℝ} (hcont : continuous_on g (set.uIcc a b)) (hderiv : ∀ (x : ℝ), x ∈ set.Ioo (linear_order.min a b) (linear_order.max a b) → has_deriv_at g (g' x) x) (hpos : ∀ (x : ℝ), x ∈ set.Ioo (linear_order.min a b) (linear_order.max a b) → 0 ≤ g' x) :
interval_integrable g' measure_theory.measure_space.volume a b

When the derivative of a function is nonnegative, then it is automatically integrable, interval version.

Integration by parts #

source
theorem interval_integral.integral_deriv_mul_eq_sub {A : Type u_5} {a b : ℝ} [normed_ring A] [normed_algebra ℝ A] [complete_space A] {u v u' v' : ℝ → A} (hu : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at u (u' x) x) (hv : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at v (v' x) x) (hu' : interval_integrable u' measure_theory.measure_space.volume a b) (hv' : interval_integrable v' measure_theory.measure_space.volume a b) :
∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
source
theorem interval_integral.integral_mul_deriv_eq_deriv_mul {A : Type u_5} {a b : ℝ} [normed_ring A] [normed_algebra ℝ A] [complete_space A] {u v u' v' : ℝ → A} (hu : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at u (u' x) x) (hv : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at v (v' x) x) (hu' : interval_integrable u' measure_theory.measure_space.volume a b) (hv' : interval_integrable v' measure_theory.measure_space.volume a b) :
∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x

Integration by substitution / Change of variables #

source
theorem interval_integral.integral_comp_smul_deriv''' {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {a b : ℝ} {f f' : ℝ → ℝ} {g : ℝ → E} (hf : continuous_on f (set.uIcc a b)) (hff' : ∀ (x : ℝ), x ∈ set.Ioo (linear_order.min a b) (linear_order.max a b) → has_deriv_within_at f (f' x) (set.Ioi x) x) (hg_cont : continuous_on g (f '' set.Ioo (linear_order.min a b) (linear_order.max a b))) (hg1 : measure_theory.integrable_on g (f '' set.uIcc a b) measure_theory.measure_space.volume) (hg2 : measure_theory.integrable_on (λ (x : ℝ), f' x • (g ∘ f) x) (set.uIcc a b) measure_theory.measure_space.volume) :
∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Change of variables, general form. If f is continuous on [a, b] and has right-derivative f' in (a, b), g is continuous on f '' (a, b) and integrable on f '' [a, b], and f' x • (g ∘ f) x is integrable on [a, b], then we can substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.

source
theorem interval_integral.integral_comp_smul_deriv'' {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {a b : ℝ} {f f' : ℝ → ℝ} {g : ℝ → E} (hf : continuous_on f (set.uIcc a b)) (hff' : ∀ (x : ℝ), x ∈ set.Ioo (linear_order.min a b) (linear_order.max a b) → has_deriv_within_at f (f' x) (set.Ioi x) x) (hf' : continuous_on f' (set.uIcc a b)) (hg : continuous_on g (f '' set.uIcc a b)) :
∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Change of variables for continuous integrands. If f is continuous on [a, b] and has continuous right-derivative f' in (a, b), and g is continuous on f '' [a, b] then we can substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.

source
theorem interval_integral.integral_comp_smul_deriv' {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {a b : ℝ} {f f' : ℝ → ℝ} {g : ℝ → E} (h : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at f (f' x) x) (h' : continuous_on f' (set.uIcc a b)) (hg : continuous_on g (f '' set.uIcc a b)) :
∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x

Change of variables. If f is has continuous derivative f' on [a, b], and g is continuous on f '' [a, b], then we can substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u. Compared to interval_integral.integral_comp_smul_deriv we only require that g is continuous on f '' [a, b].

source
theorem interval_integral.integral_comp_smul_deriv {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {a b : ℝ} {f f' : ℝ → ℝ} {g : ℝ → E} (h : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at f (f' x) x) (h' : continuous_on f' (set.uIcc a b)) (hg : continuous g) :
∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x

Change of variables, most common version. If f is has continuous derivative f' on [a, b], and g is continuous, then we can substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.

source
theorem interval_integral.integral_deriv_comp_smul_deriv' {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {a b : ℝ} {f f' : ℝ → ℝ} {g g' : ℝ → E} (hf : continuous_on f (set.uIcc a b)) (hff' : ∀ (x : ℝ), x ∈ set.Ioo (linear_order.min a b) (linear_order.max a b) → has_deriv_within_at f (f' x) (set.Ioi x) x) (hf' : continuous_on f' (set.uIcc a b)) (hg : continuous_on g (set.uIcc (f a) (f b))) (hgg' : ∀ (x : ℝ), x ∈ set.Ioo (linear_order.min (f a) (f b)) (linear_order.max (f a) (f b)) → has_deriv_within_at g (g' x) (set.Ioi x) x) (hg' : continuous_on g' (f '' set.uIcc a b)) :
∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
source
theorem interval_integral.integral_deriv_comp_smul_deriv {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space ℝ E] {a b : ℝ} {f f' : ℝ → ℝ} {g g' : ℝ → E} (hf : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at f (f' x) x) (hg : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at g (g' (f x)) (f x)) (hf' : continuous_on f' (set.uIcc a b)) (hg' : continuous g') :
∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
source
theorem interval_integral.integral_comp_mul_deriv''' {a b : ℝ} {f f' g : ℝ → ℝ} (hf : continuous_on f (set.uIcc a b)) (hff' : ∀ (x : ℝ), x ∈ set.Ioo (linear_order.min a b) (linear_order.max a b) → has_deriv_within_at f (f' x) (set.Ioi x) x) (hg_cont : continuous_on g (f '' set.Ioo (linear_order.min a b) (linear_order.max a b))) (hg1 : measure_theory.integrable_on g (f '' set.uIcc a b) measure_theory.measure_space.volume) (hg2 : measure_theory.integrable_on (λ (x : ℝ), (g ∘ f) x * f' x) (set.uIcc a b) measure_theory.measure_space.volume) :
∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u

Change of variables, general form for scalar functions. If f is continuous on [a, b] and has continuous right-derivative f' in (a, b), g is continuous on f '' (a, b) and integrable on f '' [a, b], and (g ∘ f) x * f' x is integrable on [a, b], then we can substitute u = f x to get ∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u.

source
theorem interval_integral.integral_comp_mul_deriv'' {a b : ℝ} {f f' g : ℝ → ℝ} (hf : continuous_on f (set.uIcc a b)) (hff' : ∀ (x : ℝ), x ∈ set.Ioo (linear_order.min a b) (linear_order.max a b) → has_deriv_within_at f (f' x) (set.Ioi x) x) (hf' : continuous_on f' (set.uIcc a b)) (hg : continuous_on g (f '' set.uIcc a b)) :
∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u

Change of variables for continuous integrands. If f is continuous on [a, b] and has continuous right-derivative f' in (a, b), and g is continuous on f '' [a, b] then we can substitute u = f x to get ∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u.

source
theorem interval_integral.integral_comp_mul_deriv' {a b : ℝ} {f f' g : ℝ → ℝ} (h : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at f (f' x) x) (h' : continuous_on f' (set.uIcc a b)) (hg : continuous_on g (f '' set.uIcc a b)) :
∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (x : ℝ) in f a..f b, g x

Change of variables. If f is has continuous derivative f' on [a, b], and g is continuous on f '' [a, b], then we can substitute u = f x to get ∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u. Compared to interval_integral.integral_comp_mul_deriv we only require that g is continuous on f '' [a, b].

source
theorem interval_integral.integral_comp_mul_deriv {a b : ℝ} {f f' g : ℝ → ℝ} (h : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at f (f' x) x) (h' : continuous_on f' (set.uIcc a b)) (hg : continuous g) :
∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (x : ℝ) in f a..f b, g x

Change of variables, most common version. If f is has continuous derivative f' on [a, b], and g is continuous, then we can substitute u = f x to get ∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u.

source
theorem interval_integral.integral_deriv_comp_mul_deriv' {a b : ℝ} {f f' g g' : ℝ → ℝ} (hf : continuous_on f (set.uIcc a b)) (hff' : ∀ (x : ℝ), x ∈ set.Ioo (linear_order.min a b) (linear_order.max a b) → has_deriv_within_at f (f' x) (set.Ioi x) x) (hf' : continuous_on f' (set.uIcc a b)) (hg : continuous_on g (set.uIcc (f a) (f b))) (hgg' : ∀ (x : ℝ), x ∈ set.Ioo (linear_order.min (f a) (f b)) (linear_order.max (f a) (f b)) → has_deriv_within_at g (g' x) (set.Ioi x) x) (hg' : continuous_on g' (f '' set.uIcc a b)) :
∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a
source
theorem interval_integral.integral_deriv_comp_mul_deriv {a b : ℝ} {f f' g g' : ℝ → ℝ} (hf : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at f (f' x) x) (hg : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at g (g' (f x)) (f x)) (hf' : continuous_on f' (set.uIcc a b)) (hg' : continuous g') :
∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a