Documentation

Mathlib.MeasureTheory.Integral.FundThmCalculus

Fundamental Theorem of Calculus #

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 intervalIntegral 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 intervalIntegral.integral_hasFDerivWithinAt_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 intervalIntegral.FTCFilter 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_hasDerivWithinAt_of_tendsto_ae_(left|right) and integral_hasFDerivAt_of_tendsto_ae). Similarly, integral_hasDerivWithinAt_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_isLittleO_of_tendsto_ae, states the following. Let (la, la') be an intervalIntegral.FTCFilter pair of filters around a (i.e., intervalIntegral.FTCFilter a la la') and let (lb, lb') be an intervalIntegral.FTCFilter pair of filters around b. If f has finite limits ca and cb almost surely at la' and lb', respectively, then $$ \int_{va}^{vb} f ∂μ - \int_{ua}^{ub} f ∂μ = \int_{ub}^{vb} cb ∂μ - \int_{ua}^{va} ca ∂μ + o(‖∫_{ua}^{va} 1 ∂μ‖ + ‖∫_{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 Mathlib/Analysis/SpecialFunctions/Integrals.lean.

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 ContinuousOn.intervalIntegrable or ContinuousOn.integrableOn_Icc or ContinuousOn.integrableOn_uIcc.

intervalIntegral.FTCFilter class #

As explained above, many theorems in this file rely on the typeclass intervalIntegral.FTCFilter (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 intervalIntegral.FTCFilter instances where the fact that it is one-sided or two-sided depends on the point, namely (x, 𝓝[Set.Icc a b] x, 𝓝[Set.Icc a b] x) (resp. (x, 𝓝[Set.uIcc a b] x, 𝓝[Set.uIcc a b] x), with x ∈ Icc a b (resp. x ∈ uIcc a b). This results in a two-sided derivatives for x ∈ Set.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.IsMeasurablyGenerated and Filter.TendstoIxxClass).

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 intervalIntegral.FTCFilter 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_isLittleO_of_tendsto_ae can be seen as a generalization of lemma integral_hasStrictFDerivAt 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_isLittleO_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 intervalIntegral.FTCFilters around a; let (lb, lb') be a pair of intervalIntegral.FTCFilters 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.

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
    theorem intervalIntegral.FTCFilter.pure_le {a : outParam } {outer : Filter } {inner : outParam (Filter )} [self : intervalIntegral.FTCFilter a outer inner] :
    pure a outer
    theorem intervalIntegral.FTCFilter.le_nhds {a : outParam } (outer : Filter ) {inner : outParam (Filter )} [self : intervalIntegral.FTCFilter a outer inner] :
    inner nhds a
    Equations
    • =
    Equations
    • =
    theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae' {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : E} {l : Filter } {l' : Filter } {lt : Filter ι} {μ : MeasureTheory.Measure } {u : ι} {v : ι} [l'.IsMeasurablyGenerated] [Filter.TendstoIxxClass Set.Ioc l l'] (hfm : StronglyMeasurableAtFilter f l' μ) (hf : Filter.Tendsto f (l' MeasureTheory.ae μ) (nhds c)) (hl : μ.FiniteAtFilter l') (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) :
    (fun (t : ι) => ∫ (x : ) in u t..v t, f xμ - ∫ (x : ) in u t..v t, cμ) =o[lt] fun (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 TendstoIxxClass 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_isLittleO_of_tendsto_ae for a version assuming [intervalIntegral.FTCFilter a l l'] and [MeasureTheory.IsLocallyFiniteMeasure μ]. 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' = atTop.

    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.

    theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le' {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : E} {l : Filter } {l' : Filter } {lt : Filter ι} {μ : MeasureTheory.Measure } {u : ι} {v : ι} [CompleteSpace E] [l'.IsMeasurablyGenerated] [Filter.TendstoIxxClass Set.Ioc l l'] (hfm : StronglyMeasurableAtFilter f l' μ) (hf : Filter.Tendsto f (l' MeasureTheory.ae μ) (nhds c)) (hl : μ.FiniteAtFilter l') (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) (huv : u ≤ᶠ[lt] v) :
    (fun (t : ι) => ∫ (x : ) in u t..v t, f xμ - (μ (Set.Ioc (u t) (v t))).toReal c) =o[lt] fun (t : ι) => (μ (Set.Ioc (u t) (v t))).toReal

    Fundamental theorem of calculus-1, local version for any measure. Let filters l and l' be related by TendstoIxxClass 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_isLittleO_of_tendsto_ae_of_le for a version assuming [intervalIntegral.FTCFilter a l l'] and [MeasureTheory.IsLocallyFiniteMeasure μ]. 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' = Filter.atTop.

    theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge' {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : E} {l : Filter } {l' : Filter } {lt : Filter ι} {μ : MeasureTheory.Measure } {u : ι} {v : ι} [CompleteSpace E] [l'.IsMeasurablyGenerated] [Filter.TendstoIxxClass Set.Ioc l l'] (hfm : StronglyMeasurableAtFilter f l' μ) (hf : Filter.Tendsto f (l' MeasureTheory.ae μ) (nhds c)) (hl : μ.FiniteAtFilter l') (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) (huv : v ≤ᶠ[lt] u) :
    (fun (t : ι) => ∫ (x : ) in u t..v t, f xμ + (μ (Set.Ioc (v t) (u t))).toReal c) =o[lt] fun (t : ι) => (μ (Set.Ioc (v t) (u t))).toReal

    Fundamental theorem of calculus-1, local version for any measure. Let filters l and l' be related by TendstoIxxClass 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 [intervalIntegral.FTCFilter a l l'] and [MeasureTheory.IsLocallyFiniteMeasure μ]. 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' = Filter.atTop.

    theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {c : E} {l : Filter } {l' : Filter } {lt : Filter ι} {μ : MeasureTheory.Measure } {u : ι} {v : ι} [MeasureTheory.IsLocallyFiniteMeasure μ] [intervalIntegral.FTCFilter a l l'] (hfm : StronglyMeasurableAtFilter f l' μ) (hf : Filter.Tendsto f (l' MeasureTheory.ae μ) (nhds c)) (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) :
    (fun (t : ι) => ∫ (x : ) in u t..v t, f xμ - ∫ (x : ) in u t..v t, cμ) =o[lt] fun (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 [intervalIntegral.FTCFilter 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_isLittleO_of_tendsto_ae' for a version that also works, e.g., for l = l' = Filter.atTop.

    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.

    theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {c : E} {l : Filter } {l' : Filter } {lt : Filter ι} {μ : MeasureTheory.Measure } {u : ι} {v : ι} [MeasureTheory.IsLocallyFiniteMeasure μ] [CompleteSpace E] [intervalIntegral.FTCFilter a l l'] (hfm : StronglyMeasurableAtFilter f l' μ) (hf : Filter.Tendsto f (l' MeasureTheory.ae μ) (nhds c)) (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) (huv : u ≤ᶠ[lt] v) :
    (fun (t : ι) => ∫ (x : ) in u t..v t, f xμ - (μ (Set.Ioc (u t) (v t))).toReal c) =o[lt] fun (t : ι) => (μ (Set.Ioc (u t) (v t))).toReal

    Fundamental theorem of calculus-1, local version for any measure.

    Let filters l and l' be related by [intervalIntegral.FTCFilter 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_isLittleO_of_tendsto_ae_of_le' for a version that also works, e.g., for l = l' = Filter.atTop.

    theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {c : E} {l : Filter } {l' : Filter } {lt : Filter ι} {μ : MeasureTheory.Measure } {u : ι} {v : ι} [MeasureTheory.IsLocallyFiniteMeasure μ] [CompleteSpace E] [intervalIntegral.FTCFilter a l l'] (hfm : StronglyMeasurableAtFilter f l' μ) (hf : Filter.Tendsto f (l' MeasureTheory.ae μ) (nhds c)) (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) (huv : v ≤ᶠ[lt] u) :
    (fun (t : ι) => ∫ (x : ) in u t..v t, f xμ + (μ (Set.Ioc (v t) (u t))).toReal c) =o[lt] fun (t : ι) => (μ (Set.Ioc (v t) (u t))).toReal

    Fundamental theorem of calculus-1, local version for any measure.

    Let filters l and l' be related by [intervalIntegral.FTCFilter 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 ∂μ = -μ (Set.Ioc v u) • c + o(μ(Set.Ioc v u)) as both u and v tend to l.

    See also measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge' for a version that also works, e.g., for l = l' = Filter.atTop.

    theorem intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {ca : E} {cb : E} {la : Filter } {la' : Filter } {lb : Filter } {lb' : Filter } {lt : Filter ι} {μ : MeasureTheory.Measure } {ua : ι} {va : ι} {ub : ι} {vb : ι} [intervalIntegral.FTCFilter a la la'] [intervalIntegral.FTCFilter b lb lb'] [MeasureTheory.IsLocallyFiniteMeasure μ] (hab : IntervalIntegrable f μ a b) (hmeas_a : StronglyMeasurableAtFilter f la' μ) (hmeas_b : StronglyMeasurableAtFilter f lb' μ) (ha_lim : Filter.Tendsto f (la' MeasureTheory.ae μ) (nhds ca)) (hb_lim : Filter.Tendsto f (lb' MeasureTheory.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) :
    (fun (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] fun (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 intervalIntegral.FTCFilters around a; let (lb, lb') be a pair of intervalIntegral.FTCFilters 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.

    theorem intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {c : E} {lb : Filter } {lb' : Filter } {lt : Filter ι} {μ : MeasureTheory.Measure } {u : ι} {v : ι} [intervalIntegral.FTCFilter b lb lb'] [MeasureTheory.IsLocallyFiniteMeasure μ] (hab : IntervalIntegrable f μ a b) (hmeas : StronglyMeasurableAtFilter f lb' μ) (hf : Filter.Tendsto f (lb' MeasureTheory.ae μ) (nhds c)) (hu : Filter.Tendsto u lt lb) (hv : Filter.Tendsto v lt lb) :
    (fun (t : ι) => ∫ (x : ) in a..v t, f xμ - ∫ (x : ) in a..u t, f xμ - ∫ (x : ) in u t..v t, cμ) =o[lt] fun (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 intervalIntegral.FTCFilters 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.

    theorem intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {c : E} {la : Filter } {la' : Filter } {lt : Filter ι} {μ : MeasureTheory.Measure } {u : ι} {v : ι} [intervalIntegral.FTCFilter a la la'] [MeasureTheory.IsLocallyFiniteMeasure μ] (hab : IntervalIntegrable f μ a b) (hmeas : StronglyMeasurableAtFilter f la' μ) (hf : Filter.Tendsto f (la' MeasureTheory.ae μ) (nhds c)) (hu : Filter.Tendsto u lt la) (hv : Filter.Tendsto v lt la) :
    (fun (t : ι) => ∫ (x : ) in v t..b, f xμ - ∫ (x : ) in u t..b, f xμ + ∫ (x : ) in u t..v t, cμ) =o[lt] fun (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 intervalIntegral.FTCFilters 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 Asymptotics.IsLittleO 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 Asymptotics.isLittleO because we have no definition of HasStrict(F)DerivAtFilter in the library.

    theorem intervalIntegral.integral_sub_linear_isLittleO_of_tendsto_ae {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {l : Filter } {l' : Filter } {lt : Filter ι} {a : } [intervalIntegral.FTCFilter a l l'] (hfm : StronglyMeasurableAtFilter f l' MeasureTheory.volume) (hf : Filter.Tendsto f (l' MeasureTheory.ae MeasureTheory.volume) (nhds c)) {u : ι} {v : ι} (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) :
    (fun (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 intervalIntegral.FTCFilter pair around a, then ∫ x in u..v, f x ∂μ = (v - u) • c + o (v - u) as both u and v tend to l.

    theorem intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {ca : E} {cb : E} {la : Filter } {la' : Filter } {lb : Filter } {lb' : Filter } {lt : Filter ι} {a : } {b : } {ua : ι} {ub : ι} {va : ι} {vb : ι} [intervalIntegral.FTCFilter a la la'] [intervalIntegral.FTCFilter b lb lb'] (hab : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f la' MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f lb' MeasureTheory.volume) (ha_lim : Filter.Tendsto f (la' MeasureTheory.ae MeasureTheory.volume) (nhds ca)) (hb_lim : Filter.Tendsto f (lb' MeasureTheory.ae MeasureTheory.volume) (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) :
    (fun (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] fun (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 intervalIntegral.FTCFilter pair around a, and (lb, lb') is an intervalIntegral.FTCFilter 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 HasStrictFDerivAtFilter if we had this definition.

    theorem intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {lb : Filter } {lb' : Filter } {lt : Filter ι} {a : } {b : } {u : ι} {v : ι} [intervalIntegral.FTCFilter b lb lb'] (hab : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f lb' MeasureTheory.volume) (hf : Filter.Tendsto f (lb' MeasureTheory.ae MeasureTheory.volume) (nhds c)) (hu : Filter.Tendsto u lt lb) (hv : Filter.Tendsto v lt lb) :
    (fun (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 intervalIntegral.FTCFilter 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 HasStrictDerivAtFilter if we had this definition.

    theorem intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {la : Filter } {la' : Filter } {lt : Filter ι} {a : } {b : } {u : ι} {v : ι} [intervalIntegral.FTCFilter a la la'] (hab : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f la' MeasureTheory.volume) (hf : Filter.Tendsto f (la' MeasureTheory.ae MeasureTheory.volume) (nhds c)) (hu : Filter.Tendsto u lt la) (hv : Filter.Tendsto v lt la) :
    (fun (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 intervalIntegral.FTCFilter 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 HasStrictDerivAtFilter if we had this definition.

    Strict differentiability #

    In this section we prove that for a measurable function f integrable on a..b,

    theorem intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {ca : E} {cb : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (ha : Filter.Tendsto f (nhds a MeasureTheory.ae MeasureTheory.volume) (nhds ca)) (hb : Filter.Tendsto f (nhds b MeasureTheory.ae MeasureTheory.volume) (nhds cb)) :
    HasStrictFDerivAt (fun (p : × ) => ∫ (x : ) in p.1 ..p.2, f x) ((ContinuousLinearMap.snd ).smulRight cb - (ContinuousLinearMap.fst ).smulRight ca) (a, b)

    Fundamental theorem of calculus-1, strict differentiability in both endpoints.

    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.

    theorem intervalIntegral.integral_hasStrictFDerivAt {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (ha : ContinuousAt f a) (hb : ContinuousAt f b) :
    HasStrictFDerivAt (fun (p : × ) => ∫ (x : ) in p.1 ..p.2, f x) ((ContinuousLinearMap.snd ).smulRight (f b) - (ContinuousLinearMap.fst ).smulRight (f a)) (a, b)

    Fundamental theorem of calculus-1, strict differentiability in both endpoints.

    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.

    theorem intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (hb : Filter.Tendsto f (nhds b MeasureTheory.ae MeasureTheory.volume) (nhds c)) :
    HasStrictDerivAt (fun (u : ) => ∫ (x : ) in a..u, f x) c b

    Fundamental theorem of calculus-1, strict differentiability in the right endpoint.

    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.

    theorem intervalIntegral.integral_hasStrictDerivAt_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (hb : ContinuousAt f b) :
    HasStrictDerivAt (fun (u : ) => ∫ (x : ) in a..u, f x) (f b) b

    Fundamental theorem of calculus-1, strict differentiability in the right endpoint.

    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.

    theorem intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (ha : Filter.Tendsto f (nhds a MeasureTheory.ae MeasureTheory.volume) (nhds c)) :
    HasStrictDerivAt (fun (u : ) => ∫ (x : ) in u..b, f x) (-c) a

    Fundamental theorem of calculus-1, strict differentiability in the left endpoint.

    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.

    theorem intervalIntegral.integral_hasStrictDerivAt_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (ha : ContinuousAt f a) :
    HasStrictDerivAt (fun (u : ) => ∫ (x : ) in u..b, f x) (-f a) a

    Fundamental theorem of calculus-1, strict differentiability in the left endpoint.

    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.

    theorem Continuous.integral_hasStrictDerivAt {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} (hf : Continuous f) (a : ) (b : ) :
    HasStrictDerivAt (fun (u : ) => ∫ (x : ) in a..u, f x) (f b) b

    Fundamental theorem of calculus-1, strict differentiability in the right endpoint.

    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.

    theorem Continuous.deriv_integral {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : E) (hf : Continuous f) (a : ) (b : ) :
    deriv (fun (u : ) => ∫ (x : ) in a..u, f x) b = f b

    Fundamental theorem of calculus-1, derivative in the right endpoint.

    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 HasFDerivAt, HasDerivAt, fderiv, and deriv.

    theorem intervalIntegral.integral_hasFDerivAt_of_tendsto_ae {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {ca : E} {cb : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (ha : Filter.Tendsto f (nhds a MeasureTheory.ae MeasureTheory.volume) (nhds ca)) (hb : Filter.Tendsto f (nhds b MeasureTheory.ae MeasureTheory.volume) (nhds cb)) :
    HasFDerivAt (fun (p : × ) => ∫ (x : ) in p.1 ..p.2, f x) ((ContinuousLinearMap.snd ).smulRight cb - (ContinuousLinearMap.fst ).smulRight 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).

    theorem intervalIntegral.integral_hasFDerivAt {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (ha : ContinuousAt f a) (hb : ContinuousAt f b) :
    HasFDerivAt (fun (p : × ) => ∫ (x : ) in p.1 ..p.2, f x) ((ContinuousLinearMap.snd ).smulRight (f b) - (ContinuousLinearMap.fst ).smulRight (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).

    theorem intervalIntegral.fderiv_integral_of_tendsto_ae {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {ca : E} {cb : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (ha : Filter.Tendsto f (nhds a MeasureTheory.ae MeasureTheory.volume) (nhds ca)) (hb : Filter.Tendsto f (nhds b MeasureTheory.ae MeasureTheory.volume) (nhds cb)) :
    fderiv (fun (p : × ) => ∫ (x : ) in p.1 ..p.2, f x) (a, b) = (ContinuousLinearMap.snd ).smulRight cb - (ContinuousLinearMap.fst ).smulRight 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.

    theorem intervalIntegral.fderiv_integral {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (ha : ContinuousAt f a) (hb : ContinuousAt f b) :
    fderiv (fun (p : × ) => ∫ (x : ) in p.1 ..p.2, f x) (a, b) = (ContinuousLinearMap.snd ).smulRight (f b) - (ContinuousLinearMap.fst ).smulRight (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.

    theorem intervalIntegral.integral_hasDerivAt_of_tendsto_ae_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (hb : Filter.Tendsto f (nhds b MeasureTheory.ae MeasureTheory.volume) (nhds c)) :
    HasDerivAt (fun (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.

    theorem intervalIntegral.integral_hasDerivAt_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (hb : ContinuousAt f b) :
    HasDerivAt (fun (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.

    theorem intervalIntegral.deriv_integral_of_tendsto_ae_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (hb : Filter.Tendsto f (nhds b MeasureTheory.ae MeasureTheory.volume) (nhds c)) :
    deriv (fun (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.

    theorem intervalIntegral.deriv_integral_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (hb : ContinuousAt f b) :
    deriv (fun (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.

    theorem intervalIntegral.integral_hasDerivAt_of_tendsto_ae_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (ha : Filter.Tendsto f (nhds a MeasureTheory.ae MeasureTheory.volume) (nhds c)) :
    HasDerivAt (fun (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.

    theorem intervalIntegral.integral_hasDerivAt_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (ha : ContinuousAt f a) :
    HasDerivAt (fun (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.

    theorem intervalIntegral.deriv_integral_of_tendsto_ae_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (hb : Filter.Tendsto f (nhds a MeasureTheory.ae MeasureTheory.volume) (nhds c)) :
    deriv (fun (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.

    theorem intervalIntegral.deriv_integral_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (hb : ContinuousAt f a) :
    deriv (fun (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 #

    theorem intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {ca : E} {cb : E} {la : Filter } {lb : Filter } {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) {s : Set } {t : Set } [intervalIntegral.FTCFilter a (nhdsWithin a s) la] [intervalIntegral.FTCFilter b (nhdsWithin b t) lb] (hmeas_a : StronglyMeasurableAtFilter f la MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f lb MeasureTheory.volume) (ha : Filter.Tendsto f (la MeasureTheory.ae MeasureTheory.volume) (nhds ca)) (hb : Filter.Tendsto f (lb MeasureTheory.ae MeasureTheory.volume) (nhds cb)) :
    HasFDerivWithinAt (fun (p : × ) => ∫ (x : ) in p.1 ..p.2, f x) ((ContinuousLinearMap.snd ).smulRight cb - (ContinuousLinearMap.fst ).smulRight 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
    theorem intervalIntegral.integral_hasFDerivWithinAt {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {la : Filter } {lb : Filter } {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f la MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f lb MeasureTheory.volume) {s : Set } {t : Set } [intervalIntegral.FTCFilter a (nhdsWithin a s) la] [intervalIntegral.FTCFilter b (nhdsWithin b t) lb] (ha : Filter.Tendsto f la (nhds (f a))) (hb : Filter.Tendsto f lb (nhds (f b))) :
    HasFDerivWithinAt (fun (p : × ) => ∫ (x : ) in p.1 ..p.2, f x) ((ContinuousLinearMap.snd ).smulRight (f b) - (ContinuousLinearMap.fst ).smulRight (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 ContinuousAt f _ or ContinuousWithinAt f _ _.

    s la t lb
    Iic a 𝓝[≤] a Iic b 𝓝[≤] b
    Ici a 𝓝[>] a Ici b 𝓝[>] b
    {a} {b}
    univ 𝓝 a univ 𝓝 b

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem intervalIntegral.fderivWithin_integral_of_tendsto_ae {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {ca : E} {cb : E} {la : Filter } {lb : Filter } {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f la MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f lb MeasureTheory.volume) {s : Set } {t : Set } [intervalIntegral.FTCFilter a (nhdsWithin a s) la] [intervalIntegral.FTCFilter b (nhdsWithin b t) lb] (ha : Filter.Tendsto f (la MeasureTheory.ae MeasureTheory.volume) (nhds ca)) (hb : Filter.Tendsto f (lb MeasureTheory.ae MeasureTheory.volume) (nhds cb)) (hs : autoParam (UniqueDiffWithinAt s a) _auto✝) (ht : autoParam (UniqueDiffWithinAt t b) _auto✝) :
      fderivWithin (fun (p : × ) => ∫ (x : ) in p.1 ..p.2, f x) (s ×ˢ t) (a, b) = (ContinuousLinearMap.snd ).smulRight cb - (ContinuousLinearMap.fst ).smulRight 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 fderivWithin ℝ (fun 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
      theorem intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) {s : Set } {t : Set } [intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)] (hmeas : StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume) (hb : Filter.Tendsto f (nhdsWithin b t MeasureTheory.ae MeasureTheory.volume) (nhds c)) :
      HasDerivWithinAt (fun (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.

      theorem intervalIntegral.integral_hasDerivWithinAt_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) {s : Set } {t : Set } [intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)] (hmeas : StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume) (hb : ContinuousWithinAt f t b) :
      HasDerivWithinAt (fun (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.

      theorem intervalIntegral.derivWithin_integral_of_tendsto_ae_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) {s : Set } {t : Set } [intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)] (hmeas : StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume) (hb : Filter.Tendsto f (nhdsWithin b t MeasureTheory.ae MeasureTheory.volume) (nhds c)) (hs : autoParam (UniqueDiffWithinAt s b) _auto✝) :
      derivWithin (fun (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.

      theorem intervalIntegral.derivWithin_integral_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) {s : Set } {t : Set } [intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)] (hmeas : StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume) (hb : ContinuousWithinAt f t b) (hs : autoParam (UniqueDiffWithinAt s b) _auto✝) :
      derivWithin (fun (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.

      theorem intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) {s : Set } {t : Set } [intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)] (hmeas : StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume) (ha : Filter.Tendsto f (nhdsWithin a t MeasureTheory.ae MeasureTheory.volume) (nhds c)) :
      HasDerivWithinAt (fun (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.

      theorem intervalIntegral.integral_hasDerivWithinAt_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) {s : Set } {t : Set } [intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)] (hmeas : StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume) (ha : ContinuousWithinAt f t a) :
      HasDerivWithinAt (fun (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.

      theorem intervalIntegral.derivWithin_integral_of_tendsto_ae_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) {s : Set } {t : Set } [intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)] (hmeas : StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume) (ha : Filter.Tendsto f (nhdsWithin a t MeasureTheory.ae MeasureTheory.volume) (nhds c)) (hs : autoParam (UniqueDiffWithinAt s a) _auto✝) :
      derivWithin (fun (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.

      theorem intervalIntegral.derivWithin_integral_left {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {b : } (hf : IntervalIntegrable f MeasureTheory.volume a b) {s : Set } {t : Set } [intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)] (hmeas : StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume) (ha : ContinuousWithinAt f t a) (hs : autoParam (UniqueDiffWithinAt s a) _auto✝) :
      derivWithin (fun (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.

      theorem intervalIntegral.differentiableOn_integral_of_continuous {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {a : } {s : Set } (hintg : xs, IntervalIntegrable f MeasureTheory.volume a x) (hcont : Continuous f) :
      DifferentiableOn (fun (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)][rudin2006real]. 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.

      theorem intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Ico {g' : } {g : } {φ : } {a : } {b : } (hab : a b) (hcont : ContinuousOn g (Set.Icc a b)) (hderiv : xSet.Ico a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) (φint : MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume) (hφg : xSet.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_hasDeriv_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).

      theorem intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le {g' : } {g : } {φ : } {a : } {b : } (hab : a b) (hcont : ContinuousOn g (Set.Icc a b)) (hderiv : xSet.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) (φint : MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume) (hφg : xSet.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_hasDeriv_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).

      theorem intervalIntegral.integral_le_sub_of_hasDeriv_right_of_le {g' : } {g : } {φ : } {a : } {b : } (hab : a b) (hcont : ContinuousOn g (Set.Icc a b)) (hderiv : xSet.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) (φint : MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume) (hφg : xSet.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_hasDeriv_right_of_le.

      theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le_real {g' : } {g : } {a : } {b : } (hab : a b) (hcont : ContinuousOn g (Set.Icc a b)) (hderiv : xSet.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) (g'int : MeasureTheory.IntegrableOn g' (Set.Icc a b) MeasureTheory.volume) :
      ∫ (y : ) in a..b, g' y = g b - g a

      Auxiliary lemma in the proof of integral_eq_sub_of_hasDeriv_right_of_le: real version

      theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } [CompleteSpace E] {f : E} {f' : E} (hab : a b) (hcont : ContinuousOn f (Set.Icc a b)) (hderiv : xSet.Ioo a b, HasDerivWithinAt f (f' x) (Set.Ioi x) x) (f'int : IntervalIntegrable f' MeasureTheory.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.

      theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } [CompleteSpace E] {f : E} {f' : E} (hcont : ContinuousOn f (Set.uIcc a b)) (hderiv : xSet.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hint : IntervalIntegrable f' MeasureTheory.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.

      theorem intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } [CompleteSpace E] {f : E} {f' : E} (hab : a b) (hcont : ContinuousOn f (Set.Icc a b)) (hderiv : xSet.Ioo a b, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f' MeasureTheory.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.

      theorem intervalIntegral.integral_eq_sub_of_hasDerivAt {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } [CompleteSpace E] {f : E} {f' : E} (hderiv : xSet.uIcc a b, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f' MeasureTheory.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.

      theorem intervalIntegral.integral_eq_sub_of_hasDerivAt_of_tendsto {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } [CompleteSpace E] {f : E} {f' : E} (hab : a < b) {fa : E} {fb : E} (hderiv : xSet.Ioo a b, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f' MeasureTheory.volume a b) (ha : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds fa)) (hb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds fb)) :
      ∫ (y : ) in a..b, f' y = fb - fa
      theorem intervalIntegral.integral_deriv_eq_sub {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } [CompleteSpace E] {f : E} (hderiv : xSet.uIcc a b, DifferentiableAt f x) (hint : IntervalIntegrable (deriv f) MeasureTheory.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.

      theorem intervalIntegral.integral_deriv_eq_sub' {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } [CompleteSpace E] {f' : E} (f : E) (hderiv : deriv f = f') (hdiff : xSet.uIcc a b, DifferentiableAt f x) (hcont : ContinuousOn f' (Set.uIcc a b)) :
      ∫ (y : ) in a..b, f' y = f b - f a
      theorem intervalIntegral.integral_unitInterval_deriv_eq_sub {𝕜 : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] [RCLike 𝕜] [NormedSpace 𝕜 E] [IsScalarTower 𝕜 E] {f : 𝕜E} {f' : 𝕜E} {z₀ : 𝕜} {z₁ : 𝕜} (hcont : ContinuousOn (fun (t : ) => f' (z₀ + t z₁)) (Set.Icc 0 1)) (hderiv : tSet.Icc 0 1, HasDerivAt f (f' (z₀ + t z₁)) (z₀ + t z₁)) :
      z₁ ∫ (t : ) in 0 ..1, f' (z₀ + t z₁) = f (z₀ + z₁) - f z₀

      A variant of intervalIntegral.integral_deriv_eq_sub, the Fundamental theorem of calculus, involving integrating over the unit interval.

      Automatic integrability for nonnegative derivatives #

      theorem intervalIntegral.integrableOn_deriv_right_of_nonneg {g' : } {g : } {a : } {b : } (hcont : ContinuousOn g (Set.Icc a b)) (hderiv : xSet.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) (g'pos : xSet.Ioo a b, 0 g' x) :
      MeasureTheory.IntegrableOn g' (Set.Ioc a b) MeasureTheory.volume

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

      theorem intervalIntegral.integrableOn_deriv_of_nonneg {g' : } {g : } {a : } {b : } (hcont : ContinuousOn g (Set.Icc a b)) (hderiv : xSet.Ioo a b, HasDerivAt g (g' x) x) (g'pos : xSet.Ioo a b, 0 g' x) :
      MeasureTheory.IntegrableOn g' (Set.Ioc a b) MeasureTheory.volume

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

      theorem intervalIntegral.intervalIntegrable_deriv_of_nonneg {g' : } {g : } {a : } {b : } (hcont : ContinuousOn g (Set.uIcc a b)) (hderiv : xSet.Ioo (min a b) (max a b), HasDerivAt g (g' x) x) (hpos : xSet.Ioo (min a b) (max a b), 0 g' x) :
      IntervalIntegrable g' MeasureTheory.volume a b

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

      Integration by parts #

      theorem intervalIntegral.integral_deriv_mul_eq_sub_of_hasDeriv_right {A : Type u_5} {a : } {b : } [NormedRing A] [NormedAlgebra A] [CompleteSpace A] {u : A} {v : A} {u' : A} {v' : A} (hu : ContinuousOn u (Set.uIcc a b)) (hv : ContinuousOn v (Set.uIcc a b)) (huu' : xSet.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) (hvv' : xSet.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
      ∫ (x : ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

      The integral of the derivative of a product of two maps. For improper integrals, see MeasureTheory.integral_deriv_mul_eq_sub, MeasureTheory.integral_Ioi_deriv_mul_eq_sub, and MeasureTheory.integral_Iic_deriv_mul_eq_sub.

      theorem intervalIntegral.integral_deriv_mul_eq_sub_of_hasDerivAt {A : Type u_5} {a : } {b : } [NormedRing A] [NormedAlgebra A] [CompleteSpace A] {u : A} {v : A} {u' : A} {v' : A} (hu : ContinuousOn u (Set.uIcc a b)) (hv : ContinuousOn v (Set.uIcc a b)) (huu' : xSet.Ioo (min a b) (max a b), HasDerivAt u (u' x) x) (hvv' : xSet.Ioo (min a b) (max a b), HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
      ∫ (x : ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

      The integral of the derivative of a product of two maps. Special case of integral_deriv_mul_eq_sub_of_hasDeriv_right where the functions have a two-sided derivative in the interior of the interval.

      theorem intervalIntegral.integral_deriv_mul_eq_sub_of_hasDerivWithinAt {A : Type u_5} {a : } {b : } [NormedRing A] [NormedAlgebra A] [CompleteSpace A] {u : A} {v : A} {u' : A} {v' : A} (hu : xSet.uIcc a b, HasDerivWithinAt u (u' x) (Set.uIcc a b) x) (hv : xSet.uIcc a b, HasDerivWithinAt v (v' x) (Set.uIcc a b) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
      ∫ (x : ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

      The integral of the derivative of a product of two maps. Special case of integral_deriv_mul_eq_sub_of_hasDeriv_right where the functions have a one-sided derivative at the endpoints.

      theorem intervalIntegral.integral_deriv_mul_eq_sub {A : Type u_5} {a : } {b : } [NormedRing A] [NormedAlgebra A] [CompleteSpace A] {u : A} {v : A} {u' : A} {v' : A} (hu : xSet.uIcc a b, HasDerivAt u (u' x) x) (hv : xSet.uIcc a b, HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
      ∫ (x : ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

      Special case of integral_deriv_mul_eq_sub_of_hasDeriv_right where the functions have a derivative at the endpoints.

      theorem intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right {A : Type u_5} {a : } {b : } [NormedRing A] [NormedAlgebra A] [CompleteSpace A] {u : A} {v : A} {u' : A} {v' : A} (hu : ContinuousOn u (Set.uIcc a b)) (hv : ContinuousOn v (Set.uIcc a b)) (huu' : xSet.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) (hvv' : xSet.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.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 parts. For improper integrals, see MeasureTheory.integral_mul_deriv_eq_deriv_mul, MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul, and MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul.

      theorem intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivAt {A : Type u_5} {a : } {b : } [NormedRing A] [NormedAlgebra A] [CompleteSpace A] {u : A} {v : A} {u' : A} {v' : A} (hu : ContinuousOn u (Set.uIcc a b)) (hv : ContinuousOn v (Set.uIcc a b)) (huu' : xSet.Ioo (min a b) (max a b), HasDerivAt u (u' x) x) (hvv' : xSet.Ioo (min a b) (max a b), HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.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 parts. Special case of integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right where the functions have a two-sided derivative in the interior of the interval.

      theorem intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivWithinAt {A : Type u_5} {a : } {b : } [NormedRing A] [NormedAlgebra A] [CompleteSpace A] {u : A} {v : A} {u' : A} {v' : A} (hu : xSet.uIcc a b, HasDerivWithinAt u (u' x) (Set.uIcc a b) x) (hv : xSet.uIcc a b, HasDerivWithinAt v (v' x) (Set.uIcc a b) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.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 parts. Special case of intervalIntegrable.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right where the functions have a one-sided derivative at the endpoints.

      theorem intervalIntegral.integral_mul_deriv_eq_deriv_mul {A : Type u_5} {a : } {b : } [NormedRing A] [NormedAlgebra A] [CompleteSpace A] {u : A} {v : A} {u' : A} {v' : A} (hu : xSet.uIcc a b, HasDerivAt u (u' x) x) (hv : xSet.uIcc a b, HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.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 parts. Special case of intervalIntegrable.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right where the functions have a derivative also at the endpoints. For improper integrals, see MeasureTheory.integral_mul_deriv_eq_deriv_mul, MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul, and MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul.

      Integration by substitution / Change of variables #

      theorem intervalIntegral.integral_comp_smul_deriv''' {a : } {b : } {G : Type u_6} [NormedAddCommGroup G] [NormedSpace G] {f : } {f' : } {g : G} (hf : ContinuousOn f (Set.uIcc a b)) (hff' : xSet.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hg_cont : ContinuousOn g (f '' Set.Ioo (min a b) (max a b))) (hg1 : MeasureTheory.IntegrableOn g (f '' Set.uIcc a b) MeasureTheory.volume) (hg2 : MeasureTheory.IntegrableOn (fun (x : ) => f' x (g f) x) (Set.uIcc a b) MeasureTheory.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.

      theorem intervalIntegral.integral_comp_smul_deriv'' {a : } {b : } {G : Type u_6} [NormedAddCommGroup G] [NormedSpace G] {f : } {f' : } {g : G} (hf : ContinuousOn f (Set.uIcc a b)) (hff' : xSet.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hf' : ContinuousOn f' (Set.uIcc a b)) (hg : ContinuousOn 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.

      theorem intervalIntegral.integral_comp_smul_deriv' {a : } {b : } {G : Type u_6} [NormedAddCommGroup G] [NormedSpace G] {f : } {f' : } {g : G} (h : xSet.uIcc a b, HasDerivAt f (f' x) x) (h' : ContinuousOn f' (Set.uIcc a b)) (hg : ContinuousOn 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 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 intervalIntegral.integral_comp_smul_deriv we only require that g is continuous on f '' [a, b].

      theorem intervalIntegral.integral_comp_smul_deriv {a : } {b : } {G : Type u_6} [NormedAddCommGroup G] [NormedSpace G] {f : } {f' : } {g : G} (h : xSet.uIcc a b, HasDerivAt f (f' x) x) (h' : ContinuousOn 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 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.

      theorem intervalIntegral.integral_deriv_comp_smul_deriv' {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } [CompleteSpace E] {f : } {f' : } {g : E} {g' : E} (hf : ContinuousOn f (Set.uIcc a b)) (hff' : xSet.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hf' : ContinuousOn f' (Set.uIcc a b)) (hg : ContinuousOn g (Set.uIcc (f a) (f b))) (hgg' : xSet.Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Set.Ioi x) x) (hg' : ContinuousOn g' (f '' Set.uIcc a b)) :
      ∫ (x : ) in a..b, f' x (g' f) x = (g f) b - (g f) a
      theorem intervalIntegral.integral_deriv_comp_smul_deriv {E : Type u_3} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } [CompleteSpace E] {f : } {f' : } {g : E} {g' : E} (hf : xSet.uIcc a b, HasDerivAt f (f' x) x) (hg : xSet.uIcc a b, HasDerivAt g (g' (f x)) (f x)) (hf' : ContinuousOn f' (Set.uIcc a b)) (hg' : Continuous g') :
      ∫ (x : ) in a..b, f' x (g' f) x = (g f) b - (g f) a
      theorem intervalIntegral.integral_comp_mul_deriv''' {a : } {b : } {f : } {f' : } {g : } (hf : ContinuousOn f (Set.uIcc a b)) (hff' : xSet.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hg_cont : ContinuousOn g (f '' Set.Ioo (min a b) (max a b))) (hg1 : MeasureTheory.IntegrableOn g (f '' Set.uIcc a b) MeasureTheory.volume) (hg2 : MeasureTheory.IntegrableOn (fun (x : ) => (g f) x * f' x) (Set.uIcc a b) MeasureTheory.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.

      theorem intervalIntegral.integral_comp_mul_deriv'' {a : } {b : } {f : } {f' : } {g : } (hf : ContinuousOn f (Set.uIcc a b)) (hff' : xSet.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hf' : ContinuousOn f' (Set.uIcc a b)) (hg : ContinuousOn 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.

      theorem intervalIntegral.integral_comp_mul_deriv' {a : } {b : } {f : } {f' : } {g : } (h : xSet.uIcc a b, HasDerivAt f (f' x) x) (h' : ContinuousOn f' (Set.uIcc a b)) (hg : ContinuousOn 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 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 intervalIntegral.integral_comp_mul_deriv we only require that g is continuous on f '' [a, b].

      theorem intervalIntegral.integral_comp_mul_deriv {a : } {b : } {f : } {f' : } {g : } (h : xSet.uIcc a b, HasDerivAt f (f' x) x) (h' : ContinuousOn 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 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.

      theorem intervalIntegral.integral_deriv_comp_mul_deriv' {a : } {b : } {f : } {f' : } {g : } {g' : } (hf : ContinuousOn f (Set.uIcc a b)) (hff' : xSet.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hf' : ContinuousOn f' (Set.uIcc a b)) (hg : ContinuousOn g (Set.uIcc (f a) (f b))) (hgg' : xSet.Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Set.Ioi x) x) (hg' : ContinuousOn g' (f '' Set.uIcc a b)) :
      ∫ (x : ) in a..b, (g' f) x * f' x = (g f) b - (g f) a
      theorem intervalIntegral.integral_deriv_comp_mul_deriv {a : } {b : } {f : } {f' : } {g : } {g' : } (hf : xSet.uIcc a b, HasDerivAt f (f' x) x) (hg : xSet.uIcc a b, HasDerivAt g (g' (f x)) (f x)) (hf' : ContinuousOn f' (Set.uIcc a b)) (hg' : Continuous g') :
      ∫ (x : ) in a..b, (g' f) x * f' x = (g f) b - (g f) a