# mathlibdocumentation

measure_theory.interval_integral

# Integral over an interval #

In this file we define `∫ x in a..b, f x ∂μ` to be `∫ x in Ioc a b, f x ∂μ` if `a ≤ b` and `-∫ x in Ioc b a, f x ∂μ` if `b ≤ a`. We prove a few simple properties and many versions of the first part of the fundamental theorem of calculus. Recall that it states that the function `(u, v) ↦ ∫ x in u..v, f x` has derivative `(δu, δv) ↦ δv • f b - δu • f a` at `(a, b)` provided that `f` is continuous at `a` and `b`.

## Main statements #

### FTC-1 for Lebesgue measure #

We prove several versions of FTC-1, all in the `interval_integral` namespace. Many of them follow the naming scheme `integral_has(_strict?)_(f?)deriv(_within?)_at(_of_tendsto_ae?)(_right|_left?)`. They formulate FTC in terms of `has(_strict?)_(f?)deriv(_within?)_at`. Let us explain the meaning of each part of the name:

• `_strict` means that the theorem is about strict differentiability;
• `f` means that the theorem is about differentiability in both endpoints; incompatible with `_right|_left`;
• `_within` means that the theorem is about one-sided derivatives, see below for details;
• `_of_tendsto_ae` means that instead of continuity the theorem assumes that `f` has a finite limit almost surely as `x` tends to `a` and/or `b`;
• `_right` or `_left` mean that the theorem is about differentiability in the right (resp., left) endpoint.

We also reformulate these theorems in terms of `(f?)deriv(_within?)`. These theorems are named `(f?)deriv(_within?)_integral(_of_tendsto_ae?)(_right|_left?)` with the same meaning of parts of the name.

### One-sided derivatives #

Theorem `integral_has_fderiv_within_at_of_tendsto_ae` states that `(u, v) ↦ ∫ x in u..v, f x` has a derivative `(δu, δv) ↦ δv • cb - δu • ca` within the set `s × t` at `(a, b)` provided that `f` tends to `ca` (resp., `cb`) almost surely at `la` (resp., `lb`), where possible values of `s`, `t`, and corresponding filters `la`, `lb` are given in the following table.

`s` `la` `t` `lb`
`Iic a` `𝓝[Iic a] a` `Iic b` `𝓝[Iic b] b`
`Ici a` `𝓝[Ioi a] a` `Ici b` `𝓝[Ioi b] b`
`{a}` `⊥` `{b}` `⊥`
`univ` `𝓝 a` `univ` `𝓝 b`

We use a typeclass `FTC_filter` to make Lean automatically find `la`/`lb` based on `s`/`t`. This way we can formulate one theorem instead of `16` (or `8` if we leave only non-trivial ones not covered by `integral_has_deriv_within_at_of_tendsto_ae_(left|right)` and `integral_has_fderiv_at_of_tendsto_ae`). Similarly, `integral_has_deriv_within_at_of_tendsto_ae_right` works for both one-sided derivatives using the same typeclass to find an appropriate filter.

### FTC for a locally finite measure #

Before proving FTC for the Lebesgue measure, we prove a few statements that can be seen as FTC for any measure. The most general of them, `measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae`, states the following. Let `(la, la')` be an `FTC_filter` pair of filters around `a` (i.e., `FTC_filter a la la'`) and let `(lb, lb')` be an `FTC_filter` pair of filters around `b`. If `f` has finite limits `ca` and `cb` almost surely at `la'` and `lb'`, respectively, then `∫ x in va..vb, f x ∂μ - ∫ x in ua..ub, f x ∂μ = ∫ x in ub..vb, cb ∂μ - ∫ x in ua..va, ca ∂μ + o(∥∫ x in ua..va, (1:ℝ) ∂μ∥ + ∥∫ x in ub..vb, (1:ℝ) ∂μ∥)` as `ua` and `va` tend to `la` while `ub` and `vb` tend to `lb`.

## Implementation notes #

### Avoiding `if`, `min`, and `max`#

In order to avoid `if`s in the definition, we define `interval_integrable f μ a b` as `integrable_on f (Ioc a b) μ ∧ integrable_on f (Ioc b a) μ`. For any `a`, `b` one of these intervals is empty and the other coincides with `Ioc (min a b) (max a b)`.

Similarly, we define `∫ x in a..b, f x ∂μ` to be `∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ`. Again, for any `a`, `b` one of these integrals is zero, and the other gives the expected result.

This way some properties can be translated from integrals over sets without dealing with the cases `a ≤ b` and `b ≤ a` separately.

### Choice of the interval #

We use integral over `Ioc (min a b) (max a b)` instead of one of the other three possible intervals with the same endpoints for two reasons:

• this way `∫ x in a..b, f x ∂μ + ∫ x in b..c, f x ∂μ = ∫ x in a..c, f x ∂μ` holds whenever `f` is integrable on each interval; in particular, it works even if the measure `μ` has an atom at `b`; this rules out `Ioo` and `Icc` intervals;
• with this definition for a probability measure `μ`, the integral `∫ x in a..b, 1 ∂μ` equals the difference \$F_μ(b)-F_μ(a)\$, where \$F_μ(a)=μ(-∞, a]\$ is the cumulative distribution function of `μ`.

### `FTC_filter` class #

As explained above, many theorems in this file rely on the typeclass `FTC_filter (a : α) (l l' : filter α)` to avoid code duplication. This typeclass combines four assumptions:

• `pure a ≤ l`;
• `l' ≤ 𝓝 a`;
• `l'` has a basis of measurable sets;
• if `u n` and `v n` tend to `l`, then for any `s ∈ l'`, `Ioc (u n) (v n)` is eventually included in `s`.

This typeclass has exactly four “real” instances: `(a, pure a, ⊥)`, `(a, 𝓝[Ici a] a, 𝓝[Ioi a] a)`, `(a, 𝓝[Iic a] a, 𝓝[Iic a] a)`, `(a, 𝓝 a, 𝓝 a)`, and two instances that are equal to the first and last “real” instances: `(a, 𝓝[{a}] a, ⊥)` and `(a, 𝓝[univ] a, 𝓝[univ] a)`. While the difference between `Ici a` and `Ioi a` doesn't matter for theorems about Lebesgue measure, it becomes important in the versions of FTC about any locally finite measure if this measure has an atom at one of the endpoints.

## Tags #

integral, fundamental theorem of calculus

### Integrability at an interval #

def interval_integrable {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] (f : α → E) (μ : measure_theory.measure α) (a b : α) :
Prop

A function `f` is called interval integrable with respect to a measure `μ` on an unordered interval `a..b` if it is integrable on both intervals `(a, b]` and `(b, a]`. One of these intervals is always empty, so this property is equivalent to `f` being integrable on `(min a b, max a b]`.

Equations
theorem measure_theory.integrable.interval_integrable {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] {f : α → E} {μ : measure_theory.measure α} (hf : μ) {a b : α} :
a b
theorem interval_integrable.symm {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] {f : α → E} {a b : α} {μ : measure_theory.measure α} (h : a b) :
b a
theorem interval_integrable.refl {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] {f : α → E} {a : α} {μ : measure_theory.measure α} :
a a
theorem interval_integrable.trans {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] {f : α → E} {a b c : α} {μ : measure_theory.measure α} (hab : a b) (hbc : b c) :
a c
theorem interval_integrable.neg {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] {f : α → E} {a b : α} {μ : measure_theory.measure α} [borel_space E] (h : a b) :
μ a b
@[protected]
theorem interval_integrable.ae_measurable {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] {f : α → E} {a b : α} {μ : measure_theory.measure α} (h : a b) :
(μ.restrict (set.Ioc a b))
@[protected]
theorem interval_integrable.ae_measurable' {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] {f : α → E} {a b : α} {μ : measure_theory.measure α} (h : a b) :
(μ.restrict (set.Ioc b a))
theorem interval_integrable.smul {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [linear_order α] [normed_group E] [borel_space E] [normed_field 𝕜] [ E] {f : α → E} {a b : α} {μ : measure_theory.measure α} (h : a b) (r : 𝕜) :
@[simp]
theorem interval_integrable.add {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [borel_space E] {f g : α → E} {a b : α} {μ : measure_theory.measure α} (hf : a b) (hg : a b) :
interval_integrable (λ (x : α), f x + g x) μ a b
@[simp]
theorem interval_integrable.sub {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [borel_space E] {f g : α → E} {a b : α} {μ : measure_theory.measure α} (hf : a b) (hg : a b) :
interval_integrable (λ (x : α), f x - g x) μ a b
theorem continuous_on.interval_integrable {E : Type u_4} [normed_group E] [borel_space E] {u : → E} {a b : } (hu : b)) :
a b
theorem continuous_on.interval_integrable_of_Icc {E : Type u_4} [normed_group E] [borel_space E] {u : → E} {a b : } (h : a b) (hu : (set.Icc a b)) :
a b
theorem continuous.interval_integrable {E : Type u_4} [normed_group E] [borel_space E] {u : → E} (hu : continuous u) (a b : ) :
a b

A continuous function on `ℝ` is `interval_integrable` with respect to any locally finite measure `ν` on ℝ.

theorem filter.tendsto.eventually_interval_integrable_ae {α : Type u_1} {β : Type u_2} {E : Type u_4} [linear_order α] [normed_group E] {f : α → E} {μ : measure_theory.measure α} {l l' : filter α} (hfm : μ) (hμ : μ.finite_at_filter l') {c : E} (hf : (l' μ.ae) (𝓝 c)) {u v : β → α} {lt : filter β} (hu : lt l) (hv : lt l) :
∀ᶠ (t : β) in lt, (u t) (v t)

Let `l'` be a measurably generated filter; let `l` be a of filter such that each `s ∈ l'` eventually includes `Ioc u v` as both `u` and `v` tend to `l`. Let `μ` be a measure finite at `l'`.

Suppose that `f : α → E` has a finite limit at `l' ⊓ μ.ae`. Then `f` is interval integrable on `u..v` provided that both `u` and `v` tend to `l`.

Typeclass instances allow Lean to find `l'` based on `l` but not vice versa, so `apply tendsto.eventually_interval_integrable_ae` will generate goals `filter α` and `tendsto_Ixx_class Ioc ?m_1 l'`.

theorem filter.tendsto.eventually_interval_integrable {α : Type u_1} {β : Type u_2} {E : Type u_4} [linear_order α] [normed_group E] {f : α → E} {μ : measure_theory.measure α} {l l' : filter α} (hfm : μ) (hμ : μ.finite_at_filter l') {c : E} (hf : l' (𝓝 c)) {u v : β → α} {lt : filter β} (hu : lt l) (hv : lt l) :
∀ᶠ (t : β) in lt, (u t) (v t)

Let `l'` be a measurably generated filter; let `l` be a of filter such that each `s ∈ l'` eventually includes `Ioc u v` as both `u` and `v` tend to `l`. Let `μ` be a measure finite at `l'`.

Suppose that `f : α → E` has a finite limit at `l`. Then `f` is interval integrable on `u..v` provided that both `u` and `v` tend to `l`.

Typeclass instances allow Lean to find `l'` based on `l` but not vice versa, so `apply tendsto.eventually_interval_integrable_ae` will generate goals `filter α` and `tendsto_Ixx_class Ioc ?m_1 l'`.

### Interval integral: definition and basic properties #

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

def interval_integral {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] (f : α → E) (a b : α) (μ : measure_theory.measure α) :
E

The interval integral `∫ x in a..b, f x ∂μ` is defined as `∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ`. If `a ≤ b`, then it equals `∫ x in Ioc a b, f x ∂μ`, otherwise it equals `-∫ x in Ioc b a, f x ∂μ`.

Equations
@[simp]
theorem interval_integral.integral_zero {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {μ : measure_theory.measure α} :
(x : α) in a..b, 0 μ = 0
theorem interval_integral.integral_of_le {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} (h : a b) :
(x : α) in a..b, f x μ = (x : α) in b, f x μ
@[simp]
theorem interval_integral.integral_same {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a : α} {f : α → E} {μ : measure_theory.measure α} :
(x : α) in a..a, f x μ = 0
theorem interval_integral.integral_symm {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {f : α → E} {μ : measure_theory.measure α} (a b : α) :
(x : α) in b..a, f x μ = - (x : α) in a..b, f x μ
theorem interval_integral.integral_of_ge {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} (h : b a) :
(x : α) in a..b, f x μ = - (x : α) in a, f x μ
theorem interval_integral.integral_cases {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} (f : α → E) (a b : α) :
(x : α) in a..b, f x μ { (x : α) in set.Ioc (min a b) (max a b), f x μ, - (x : α) in set.Ioc (min a b) (max a b), f x μ}
theorem interval_integral.integral_non_ae_measurable {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {f : α → E} {a b : α} (hf : ¬ (μ.restrict (set.Ioc (min a b) (max a b)))) :
(x : α) in a..b, f x μ = 0
theorem interval_integral.integral_non_ae_measurable_of_le {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {f : α → E} {a b : α} (h : a b) (hf : ¬ (μ.restrict (set.Ioc a b))) :
(x : α) in a..b, f x μ = 0
theorem interval_integral.norm_integral_eq_norm_integral_Ioc {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} :
(x : α) in a..b, f x μ = (x : α) in set.Ioc (min a b) (max a b), f x μ
theorem interval_integral.norm_integral_le_integral_norm_Ioc {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} :
(x : α) in a..b, f x μ (x : α) in set.Ioc (min a b) (max a b), f x μ
theorem interval_integral.norm_integral_le_abs_integral_norm {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} :
(x : α) in a..b, f x μ abs ( (x : α) in a..b, f x μ)
theorem interval_integral.norm_integral_le_of_norm_le_const_ae {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b C : } {f : → E} (h : ∀ᵐ (x : ), x set.Ioc (min a b) (max a b)f x C) :
∫ (x : ) in a..b, f x C * abs (b - a)
theorem interval_integral.norm_integral_le_of_norm_le_const {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b C : } {f : → E} (h : ∀ (x : ), x set.Ioc (min a b) (max a b)f x C) :
∫ (x : ) in a..b, f x C * abs (b - a)
@[simp]
theorem interval_integral.integral_add {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {f g : α → E} {μ : measure_theory.measure α} (hf : a b) (hg : a b) :
(x : α) in a..b, f x + g x μ = (x : α) in a..b, f x μ + (x : α) in a..b, g x μ
@[simp]
theorem interval_integral.integral_neg {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} :
(x : α) in a..b, -f x μ = - (x : α) in a..b, f x μ
@[simp]
theorem interval_integral.integral_sub {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {f g : α → E} {μ : measure_theory.measure α} (hf : a b) (hg : a b) :
(x : α) in a..b, f x - g x μ = (x : α) in a..b, f x μ - (x : α) in a..b, g x μ
@[simp]
theorem interval_integral.integral_smul {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} (r : ) :
(x : α) in a..b, r f x μ = r (x : α) in a..b, f x μ
theorem interval_integral.integral_const' {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {μ : measure_theory.measure α} (c : E) :
(x : α) in a..b, c μ = ((μ (set.Ioc a b)).to_real - (μ (set.Ioc b a)).to_real) c
@[simp]
theorem interval_integral.integral_const {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (c : E) :
∫ (x : ) in a..b, c = (b - a) c
theorem interval_integral.integral_smul_measure {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} (c : ℝ≥0∞) :
(x : α) in a..b, f x c μ = c.to_real (x : α) in a..b, f x μ
@[simp]
theorem interval_integral.integral_comp_mul_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b c : } (f : → E) (hc : c 0) :
∫ (x : ) in a..b, f (x * c) = c⁻¹ ∫ (x : ) in a * c..b * c, f x
@[simp]
theorem interval_integral.smul_integral_comp_mul_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (c : ) :
c ∫ (x : ) in a..b, f (x * c) = ∫ (x : ) in a * c..b * c, f x
@[simp]
theorem interval_integral.integral_comp_mul_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b c : } (f : → E) (hc : c 0) :
∫ (x : ) in a..b, f (c * x) = c⁻¹ ∫ (x : ) in c * a..c * b, f x
@[simp]
theorem interval_integral.smul_integral_comp_mul_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (c : ) :
c ∫ (x : ) in a..b, f (c * x) = ∫ (x : ) in c * a..c * b, f x
@[simp]
theorem interval_integral.integral_comp_div {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b c : } (f : → E) (hc : c 0) :
∫ (x : ) in a..b, f (x / c) = c ∫ (x : ) in a / c..b / c, f x
@[simp]
theorem interval_integral.inv_smul_integral_comp_div {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (c : ) :
c⁻¹ ∫ (x : ) in a..b, f (x / c) = ∫ (x : ) in a / c..b / c, f x
@[simp]
theorem interval_integral.integral_comp_add_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (d : ) :
∫ (x : ) in a..b, f (x + d) = ∫ (x : ) in a + d..b + d, f x
@[simp]
theorem interval_integral.integral_comp_mul_add {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b c : } (f : → E) (hc : c 0) (d : ) :
∫ (x : ) in a..b, f (c * x + d) = c⁻¹ ∫ (x : ) in c * a + d..c * b + d, f x
@[simp]
theorem interval_integral.smul_integral_comp_mul_add {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (c d : ) :
c ∫ (x : ) in a..b, f (c * x + d) = ∫ (x : ) in c * a + d..c * b + d, f x
@[simp]
theorem interval_integral.integral_comp_add_mul {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b c : } (f : → E) (hc : c 0) (d : ) :
∫ (x : ) in a..b, f (d + c * x) = c⁻¹ ∫ (x : ) in d + c * a..d + c * b, f x
@[simp]
theorem interval_integral.smul_integral_comp_add_mul {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (c d : ) :
c ∫ (x : ) in a..b, f (d + c * x) = ∫ (x : ) in d + c * a..d + c * b, f x
@[simp]
theorem interval_integral.integral_comp_div_add {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b c : } (f : → E) (hc : c 0) (d : ) :
∫ (x : ) in a..b, f (x / c + d) = c ∫ (x : ) in a / c + d..b / c + d, f x
@[simp]
theorem interval_integral.inv_smul_integral_comp_div_add {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (c d : ) :
c⁻¹ ∫ (x : ) in a..b, f (x / c + d) = ∫ (x : ) in a / c + d..b / c + d, f x
@[simp]
theorem interval_integral.integral_comp_add_div {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b c : } (f : → E) (hc : c 0) (d : ) :
∫ (x : ) in a..b, f (d + x / c) = c ∫ (x : ) in d + a / c..d + b / c, f x
@[simp]
theorem interval_integral.inv_smul_integral_comp_add_div {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (c d : ) :
c⁻¹ ∫ (x : ) in a..b, f (d + x / c) = ∫ (x : ) in d + a / c..d + b / c, f x
@[simp]
theorem interval_integral.integral_comp_mul_sub {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b c : } (f : → E) (hc : c 0) (d : ) :
∫ (x : ) in a..b, f (c * x - d) = c⁻¹ ∫ (x : ) in c * a - d..c * b - d, f x
@[simp]
theorem interval_integral.smul_integral_comp_mul_sub {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (c d : ) :
c ∫ (x : ) in a..b, f (c * x - d) = ∫ (x : ) in c * a - d..c * b - d, f x
@[simp]
theorem interval_integral.integral_comp_sub_mul {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b c : } (f : → E) (hc : c 0) (d : ) :
∫ (x : ) in a..b, f (d - c * x) = c⁻¹ ∫ (x : ) in d - c * b..d - c * a, f x
@[simp]
theorem interval_integral.smul_integral_comp_sub_mul {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (c d : ) :
c ∫ (x : ) in a..b, f (d - c * x) = ∫ (x : ) in d - c * b..d - c * a, f x
@[simp]
theorem interval_integral.integral_comp_div_sub {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b c : } (f : → E) (hc : c 0) (d : ) :
∫ (x : ) in a..b, f (x / c - d) = c ∫ (x : ) in a / c - d..b / c - d, f x
@[simp]
theorem interval_integral.inv_smul_integral_comp_div_sub {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (c d : ) :
c⁻¹ ∫ (x : ) in a..b, f (x / c - d) = ∫ (x : ) in a / c - d..b / c - d, f x
@[simp]
theorem interval_integral.integral_comp_sub_div {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b c : } (f : → E) (hc : c 0) (d : ) :
∫ (x : ) in a..b, f (d - x / c) = c ∫ (x : ) in d - b / c..d - a / c, f x
@[simp]
theorem interval_integral.inv_smul_integral_comp_sub_div {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (c d : ) :
c⁻¹ ∫ (x : ) in a..b, f (d - x / c) = ∫ (x : ) in d - b / c..d - a / c, f x
@[simp]
theorem interval_integral.integral_comp_sub_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (d : ) :
∫ (x : ) in a..b, f (x - d) = ∫ (x : ) in a - d..b - d, f x
@[simp]
theorem interval_integral.integral_comp_sub_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) (d : ) :
∫ (x : ) in a..b, f (d - x) = ∫ (x : ) in d - b..d - a, f x
@[simp]
theorem interval_integral.integral_comp_neg {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } (f : → E) :
∫ (x : ) in a..b, f (-x) = ∫ (x : ) in -b..-a, f x

### Integral is an additive function of the interval #

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

theorem interval_integral.integral_congr {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {f g : α → E} {μ : measure_theory.measure α} {a b : α} (h : g b)) :
(x : α) in a..b, f x μ = (x : α) in a..b, g x μ

If two functions are equal in the relevant interval, their interval integrals are also equal.

theorem interval_integral.integral_add_adjacent_intervals_cancel {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b c : α} {f : α → E} {μ : measure_theory.measure α} (hab : a b) (hbc : b c) :
(x : α) in a..b, f x μ + (x : α) in b..c, f x μ + (x : α) in c..a, f x μ = 0
theorem interval_integral.integral_add_adjacent_intervals {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b c : α} {f : α → E} {μ : measure_theory.measure α} (hab : a b) (hbc : b c) :
(x : α) in a..b, f x μ + (x : α) in b..c, f x μ = (x : α) in a..c, f x μ
theorem interval_integral.integral_interval_sub_left {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b c : α} {f : α → E} {μ : measure_theory.measure α} (hab : a b) (hac : a c) :
(x : α) in a..b, f x μ - (x : α) in a..c, f x μ = (x : α) in c..b, f x μ
theorem interval_integral.integral_interval_add_interval_comm {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b c d : α} {f : α → E} {μ : measure_theory.measure α} (hab : a b) (hcd : c d) (hac : a c) :
(x : α) in a..b, f x μ + (x : α) in c..d, f x μ = (x : α) in a..d, f x μ + (x : α) in c..b, f x μ
theorem interval_integral.integral_interval_sub_interval_comm {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b c d : α} {f : α → E} {μ : measure_theory.measure α} (hab : a b) (hcd : c d) (hac : a c) :
(x : α) in a..b, f x μ - (x : α) in c..d, f x μ = (x : α) in a..c, f x μ - (x : α) in b..d, f x μ
theorem interval_integral.integral_interval_sub_interval_comm' {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b c d : α} {f : α → E} {μ : measure_theory.measure α} (hab : a b) (hcd : c d) (hac : a c) :
(x : α) in a..b, f x μ - (x : α) in c..d, f x μ = (x : α) in d..b, f x μ - (x : α) in c..a, f x μ
theorem interval_integral.integral_Iic_sub_Iic {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} (ha : μ) (hb : μ) :
(x : α) in , f x μ - (x : α) in , f x μ = (x : α) in a..b, f x μ
theorem interval_integral.integral_const_of_cdf {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {a b : α} {μ : measure_theory.measure α} (c : E) :
(x : α) in a..b, c μ = ((μ (set.Iic b)).to_real - (μ (set.Iic a)).to_real) c

If `μ` is a finite measure then `∫ x in a..b, c ∂μ = (μ (Iic b) - μ (Iic a)) • c`.

theorem interval_integral.integral_eq_integral_of_support_subset {α : Type u_1} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {f : α → E} {a b : α} (h : b) :
(x : α) in a..b, f x μ = (x : α), f x μ
theorem interval_integral.integral_eq_zero_iff_of_le_of_nonneg_ae {f : } {a b : } (hab : a b) (hf : 0 ≤ᵐ[] f)  :
∫ (x : ) in a..b, f x = 0
theorem interval_integral.integral_eq_zero_iff_of_nonneg_ae {f : } {a b : } (hf : 0 ≤ᵐ[] f)  :
∫ (x : ) in a..b, f x = 0 f =ᵐ[] 0
theorem interval_integral.integral_pos_iff_support_of_nonneg_ae' {f : } {a b : } (hf : 0 ≤ᵐ[] f)  :
0 < ∫ (x : ) in a..b, f x a < b
theorem interval_integral.integral_pos_iff_support_of_nonneg_ae {f : } {a b : }  :
0 < ∫ (x : ) in a..b, f x a < b
theorem interval_integral.integral_mono_ae_restrict {f g : } {a b : } (hf : a b) (hg : a b) (hab : a b) (h : f ≤ᵐ[μ.restrict b)] g) :
(u : ) in a..b, f u μ (u : ) in a..b, g u μ
theorem interval_integral.integral_mono_ae {f g : } {a b : } (hf : a b) (hg : a b) (hab : a b) (h : f ≤ᵐ[μ] g) :
(u : ) in a..b, f u μ (u : ) in a..b, g u μ
theorem interval_integral.integral_mono_on {f g : } {a b : } (hf : a b) (hg : a b) (hab : a b) (h : ∀ (x : ), x bf x g x) :
(u : ) in a..b, f u μ (u : ) in a..b, g u μ
theorem interval_integral.integral_mono {f g : } {a b : } (hf : a b) (hg : a b) (hab : a b) (h : f g) :
(u : ) in a..b, f u μ (u : ) in a..b, g u μ
theorem interval_integral.integral_nonneg_of_ae_restrict {f : } {a b : } (hab : a b) (hf : 0 ≤ᵐ[μ.restrict b)] f) :
0 (u : ) in a..b, f u μ
theorem interval_integral.integral_nonneg_of_ae {f : } {a b : } (hab : a b) (hf : 0 ≤ᵐ[μ] f) :
0 (u : ) in a..b, f u μ
theorem interval_integral.integral_nonneg {f : } {a b : } (hab : a b) (hf : ∀ (u : ), u b0 f u) :
0 (u : ) in a..b, f u μ

### Fundamental theorem of calculus, part 1, for any measure #

In this section we prove a few lemmas that can be seen as versions of FTC-1 for interval integrals w.r.t. any measure. Many theorems are formulated for one or two pairs of filters related by `FTC_filter a l l'`. This typeclass has exactly four “real” instances: `(a, pure a, ⊥)`, `(a, 𝓝[Ici a] a, 𝓝[Ioi a] a)`, `(a, 𝓝[Iic a] a, 𝓝[Iic a] a)`, `(a, 𝓝 a, 𝓝 a)`, and two instances that are equal to the first and last “real” instances: `(a, 𝓝[{a}] a, ⊥)` and `(a, 𝓝[univ] a, 𝓝[univ] a)`. We use this approach to avoid repeating arguments in many very similar cases. Lean can automatically find both `a` and `l'` based on `l`.

The most general theorem `measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae` can be seen as a generalization of lemma `integral_has_strict_fderiv_at` below which states strict differentiability of `∫ x in u..v, f x` in `(u, v)` at `(a, b)` for a measurable function `f` that is integrable on `a..b` and is continuous at `a` and `b`. The lemma is generalized in three directions: first, `measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae` deals with any locally finite measure `μ`; second, it works for one-sided limits/derivatives; third, it assumes only that `f` has finite limits almost surely at `a` and `b`.

Namely, let `f` be a measurable function integrable on `a..b`. Let `(la, la')` be a pair of `FTC_filter`s around `a`; let `(lb, lb')` be a pair of `FTC_filter`s 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.

@[class]
structure interval_integral.FTC_filter {β : Type u_6} [linear_order β] (a : out_param β) (outer : filter β) (inner : out_param (filter β)) :
Prop
• to_tendsto_Ixx_class : inner
• pure_le : pure a outer
• le_nhds : inner 𝓝 a
• meas_gen :

An auxiliary typeclass for the Fundamental theorem of calculus, part 1. It is used to formulate theorems that work simultaneously for left and right one-sided derivatives of `∫ x in u..v, f x`. There are four instances: `(a, pure a, ⊥)`, `(a, 𝓝[Ici a], 𝓝[Ioi a])`, `(a, 𝓝[Iic a], 𝓝[Iic a])`, and `(a, 𝓝 a, 𝓝 a)`.

Instances
@[protected, instance]
def interval_integral.FTC_filter.pure {β : Type u_2} [linear_order β] (a : β) :
@[protected, instance]
def interval_integral.FTC_filter.nhds_within_singleton {β : Type u_2} [linear_order β] (a : β) :
(𝓝[{a}] a)
theorem interval_integral.FTC_filter.finite_at_inner {β : Type u_2} [linear_order β] {a : β} (l : filter β) {l' : out_param (filter β)} [h : l'] {μ : measure_theory.measure β}  :
@[protected, instance]
def interval_integral.FTC_filter.nhds {β : Type u_2} [linear_order β] (a : β) :
(𝓝 a)
@[protected, instance]
def interval_integral.FTC_filter.nhds_univ {β : Type u_2} [linear_order β] (a : β) :
(𝓝 a)
@[protected, instance]
def interval_integral.FTC_filter.nhds_left {β : Type u_2} [linear_order β] (a : β) :
(𝓝[] a)
@[protected, instance]
def interval_integral.FTC_filter.nhds_right {β : Type u_2} [linear_order β] (a : β) :
(𝓝[] a)
theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae' {α : Type u_1} {β : Type u_2} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {f : α → E} {c : E} {l l' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} (hfm : μ) (hf : (l' μ.ae) (𝓝 c)) (hl : μ.finite_at_filter l') (hu : lt l) (hv : lt l) :
asymptotics.is_o (λ (t : β), (x : α) in u t..v t, f x μ - (x : α) in u t..v t, c μ) (λ (t : β), (x : α) in u t..v t, 1 μ) lt

Fundamental theorem of calculus-1, local version for any measure. Let filters `l` and `l'` be related by `tendsto_Ixx_class Ioc`. If `f` has a finite limit `c` at `l' ⊓ μ.ae`, where `μ` is a measure finite at `l'`, then `∫ x in u..v, f x ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, 1 ∂μ)` as both `u` and `v` tend to `l`.

See also `measure_integral_sub_linear_is_o_of_tendsto_ae` for a version assuming `[FTC_filter a l l']` and `[locally_finite_measure μ]`. If `l` is one of `𝓝[Ici a] a`, `𝓝[Iic a] a`, `𝓝 a`, then it's easier to apply the non-primed version. The primed version also works, e.g., for `l = l' = at_top`.

We use integrals of constants instead of measures because this way it is easier to formulate a statement that works in both cases `u ≤ v` and `v ≤ u`.

theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae_of_le' {α : Type u_1} {β : Type u_2} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {f : α → E} {c : E} {l l' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} (hfm : μ) (hf : (l' μ.ae) (𝓝 c)) (hl : μ.finite_at_filter l') (hu : lt l) (hv : lt l) (huv : u ≤ᶠ[lt] v) :
asymptotics.is_o (λ (t : β), (x : α) in u t..v t, f x μ - (μ (set.Ioc (u t) (v t))).to_real c) (λ (t : β), (μ (set.Ioc (u t) (v t))).to_real) lt

Fundamental theorem of calculus-1, local version for any measure. Let filters `l` and `l'` be related by `tendsto_Ixx_class Ioc`. If `f` has a finite limit `c` at `l ⊓ μ.ae`, where `μ` is a measure finite at `l`, then `∫ x in u..v, f x ∂μ = μ (Ioc u v) • c + o(μ(Ioc u v))` as both `u` and `v` tend to `l` so that `u ≤ v`.

See also `measure_integral_sub_linear_is_o_of_tendsto_ae_of_le` for a version assuming `[FTC_filter a l l']` and `[locally_finite_measure μ]`. If `l` is one of `𝓝[Ici a] a`, `𝓝[Iic a] a`, `𝓝 a`, then it's easier to apply the non-primed version. The primed version also works, e.g., for `l = l' = at_top`.

theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge' {α : Type u_1} {β : Type u_2} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {f : α → E} {c : E} {l l' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} (hfm : μ) (hf : (l' μ.ae) (𝓝 c)) (hl : μ.finite_at_filter l') (hu : lt l) (hv : lt l) (huv : v ≤ᶠ[lt] u) :
asymptotics.is_o (λ (t : β), (x : α) in u t..v t, f x μ + (μ (set.Ioc (v t) (u t))).to_real c) (λ (t : β), (μ (set.Ioc (v t) (u t))).to_real) lt

Fundamental theorem of calculus-1, local version for any measure. Let filters `l` and `l'` be related by `tendsto_Ixx_class Ioc`. If `f` has a finite limit `c` at `l ⊓ μ.ae`, where `μ` is a measure finite at `l`, then `∫ x in u..v, f x ∂μ = -μ (Ioc v u) • c + o(μ(Ioc v u))` as both `u` and `v` tend to `l` so that `v ≤ u`.

See also `measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge` for a version assuming `[FTC_filter a l l']` and `[locally_finite_measure μ]`. If `l` is one of `𝓝[Ici a] a`, `𝓝[Iic a] a`, `𝓝 a`, then it's easier to apply the non-primed version. The primed version also works, e.g., for `l = l' = at_top`.

theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae {α : Type u_1} {β : Type u_2} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {f : α → E} {a : α} {c : E} {l l' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [ l'] (hfm : μ) (hf : (l' μ.ae) (𝓝 c)) (hu : lt l) (hv : lt l) :
asymptotics.is_o (λ (t : β), (x : α) in u t..v t, f x μ - (x : α) in u t..v t, c μ) (λ (t : β), (x : α) in u t..v t, 1 μ) lt

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`.

theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae_of_le {α : Type u_1} {β : Type u_2} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {f : α → E} {a : α} {c : E} {l l' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [ l'] (hfm : μ) (hf : (l' μ.ae) (𝓝 c)) (hu : lt l) (hv : lt l) (huv : u ≤ᶠ[lt] v) :
asymptotics.is_o (λ (t : β), (x : α) in u t..v t, f x μ - (μ (set.Ioc (u t) (v t))).to_real c) (λ (t : β), (μ (set.Ioc (u t) (v t))).to_real) lt

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`.

theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge {α : Type u_1} {β : Type u_2} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {f : α → E} {a : α} {c : E} {l l' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [ l'] (hfm : μ) (hf : (l' μ.ae) (𝓝 c)) (hu : lt l) (hv : lt l) (huv : v ≤ᶠ[lt] u) :
asymptotics.is_o (λ (t : β), (x : α) in u t..v t, f x μ + (μ (set.Ioc (v t) (u t))).to_real c) (λ (t : β), (μ (set.Ioc (v t) (u t))).to_real) lt

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`.

theorem interval_integral.measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae {α : Type u_1} {β : Type u_2} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {f : α → E} {a b : α} {ca cb : E} {la la' lb lb' : filter α} {lt : filter β} {μ : measure_theory.measure α} {ua va ub vb : β → α} [borel_space α] [ la'] [ lb'] (hab : a b) (hmeas_a : la' μ) (hmeas_b : lb' μ) (ha_lim : (la' μ.ae) (𝓝 ca)) (hb_lim : (lb' μ.ae) (𝓝 cb)) (hua : lt la) (hva : lt la) (hub : lt lb) (hvb : lt lb) :
asymptotics.is_o (λ (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 μ)) (λ (t : β), (x : α) in ua t..va t, 1 μ + (x : α) in ub t..vb t, 1 μ) lt

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_filter`s around `a`; let `(lb, lb')` be a pair of `FTC_filter`s 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 interval_integral.measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right {α : Type u_1} {β : Type u_2} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {f : α → E} {a b : α} {c : E} {lb lb' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [borel_space α] [ lb'] (hab : a b) (hmeas : lb' μ) (hf : (lb' μ.ae) (𝓝 c)) (hu : lt lb) (hv : lt lb) :
asymptotics.is_o (λ (t : β), (x : α) in a..v t, f x μ - (x : α) in a..u t, f x μ - (x : α) in u t..v t, c μ) (λ (t : β), (x : α) in u t..v t, 1 μ) lt

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_filter`s 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 interval_integral.measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_left {α : Type u_1} {β : Type u_2} {E : Type u_4} [linear_order α] [normed_group E] [ E] [borel_space E] {f : α → E} {a b : α} {c : E} {la la' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [borel_space α] [ la'] (hab : a b) (hmeas : la' μ) (hf : (la' μ.ae) (𝓝 c)) (hu : lt la) (hv : lt la) :
asymptotics.is_o (λ (t : β), (x : α) in v t..b, f x μ - (x : α) in u t..b, f x μ + (x : α) in u t..v t, c μ) (λ (t : β), (x : α) in u t..v t, 1 μ) lt

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_filter`s 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.

theorem interval_integral.integral_sub_linear_is_o_of_tendsto_ae {β : Type u_2} {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {l l' : filter } {lt : filter β} {a : } [ l'] (hf : (𝓝 c)) {u v : β → } (hu : lt l) (hv : lt l) :
asymptotics.is_o (λ (t : β), (∫ (x : ) in u t..v t, f x) - (v t - u t) c) (v - u) lt

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`.

theorem interval_integral.integral_sub_integral_sub_linear_is_o_of_tendsto_ae {β : Type u_2} {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {ca cb : E} {la la' lb lb' : filter } {lt : filter β} {a b : } {ua ub va vb : β → } [ la'] [ lb'] (hmeas_a : la' measure_theory.measure_space.volume) (hmeas_b : lb' measure_theory.measure_space.volume) (ha_lim : (𝓝 ca)) (hb_lim : (𝓝 cb)) (hua : lt la) (hva : lt la) (hub : lt lb) (hvb : lt lb) :
asymptotics.is_o (λ (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)) (λ (t : β), va t - ua t + vb t - ub t) lt

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.

theorem interval_integral.integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right {β : Type u_2} {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {lb lb' : filter } {lt : filter β} {a b : } {u v : β → } [ lb'] (hmeas : lb' measure_theory.measure_space.volume) (hf : (𝓝 c)) (hu : lt lb) (hv : lt lb) :
asymptotics.is_o (λ (t : β), ((∫ (x : ) in a..v t, f x) - ∫ (x : ) in a..u t, f x) - (v t - u t) c) (v - u) lt

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.

theorem interval_integral.integral_sub_integral_sub_linear_is_o_of_tendsto_ae_left {β : Type u_2} {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {la la' : filter } {lt : filter β} {a b : } {u v : β → } [ la'] (hmeas : la' measure_theory.measure_space.volume) (hf : (𝓝 c)) (hu : lt la) (hv : lt la) :
asymptotics.is_o (λ (t : β), ((∫ (x : ) in v t..b, f x) - ∫ (x : ) in u t..b, f x) + (v t - u t) c) (v - u) lt

Fundamental theorem of calculus-1, strict differentiability at filter in both endpoints. If `f` is a measurable function integrable on `a..b`, `(la, la')` is an `FTC_filter` pair around `a`, and `f` has a finite limit `c` almost surely at `la'`, then `(∫ x in v..b, f x) - ∫ x in u..b, f x = -(v - u) • c + o(∥v - u∥)` as `u` and `v` tend to `la`.

This lemma could've been formulated using `has_strict_deriv_at_filter` if we had this definition.

#### Strict differentiability #

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

• `integral_has_strict_fderiv_at_of_tendsto_ae`: the function `(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)` in the sense of strict differentiability provided that `f` tends to `ca` and `cb` almost surely as `x` tendsto to `a` and `b`, respectively;

• `integral_has_strict_fderiv_at`: the function `(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • f b - u • f a` at `(a, b)` in the sense of strict differentiability provided that `f` is continuous at `a` and `b`;

• `integral_has_strict_deriv_at_of_tendsto_ae_right`: the function `u ↦ ∫ x in a..u, f x` has derivative `c` at `b` in the sense of strict differentiability provided that `f` tends to `c` almost surely as `x` tends to `b`;

• `integral_has_strict_deriv_at_right`: the function `u ↦ ∫ x in a..u, f x` has derivative `f b` at `b` in the sense of strict differentiability provided that `f` is continuous at `b`;

• `integral_has_strict_deriv_at_of_tendsto_ae_left`: the function `u ↦ ∫ x in u..b, f x` has derivative `-c` at `a` in the sense of strict differentiability provided that `f` tends to `c` almost surely as `x` tends to `a`;

• `integral_has_strict_deriv_at_left`: the function `u ↦ ∫ x in u..b, f x` has derivative `-f a` at `a` in the sense of strict differentiability provided that `f` is continuous at `a`.

theorem interval_integral.integral_has_strict_fderiv_at_of_tendsto_ae {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {ca cb : E} {a b : } (hmeas_a : (𝓝 a) measure_theory.measure_space.volume) (hmeas_b : (𝓝 b) measure_theory.measure_space.volume) (ha : (𝓝 ca)) (hb : (𝓝 cb)) :
has_strict_fderiv_at (λ (p : × ), ∫ (x : ) in p.fst..p.snd, f x) - (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.

theorem interval_integral.integral_has_strict_fderiv_at {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } (hmeas_a : (𝓝 a) measure_theory.measure_space.volume) (hmeas_b : (𝓝 b) measure_theory.measure_space.volume) (ha : a) (hb : b) :
has_strict_fderiv_at (λ (p : × ), ∫ (x : ) in p.fst..p.snd, f x) (f b) - (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.

theorem interval_integral.integral_has_strict_deriv_at_of_tendsto_ae_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {a b : } (hmeas : (𝓝 b) measure_theory.measure_space.volume) (hb : (𝓝 c)) :
has_strict_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` in the sense of strict differentiability.

theorem interval_integral.integral_has_strict_deriv_at_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } (hmeas : (𝓝 b) measure_theory.measure_space.volume) (hb : 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.

theorem interval_integral.integral_has_strict_deriv_at_of_tendsto_ae_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {a b : } (hmeas : (𝓝 a) measure_theory.measure_space.volume) (ha : (𝓝 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.

theorem interval_integral.integral_has_strict_deriv_at_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } (hmeas : (𝓝 a) measure_theory.measure_space.volume) (ha : 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.

#### 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`.

theorem interval_integral.integral_has_fderiv_at_of_tendsto_ae {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {ca cb : E} {a b : } (hmeas_a : (𝓝 a) measure_theory.measure_space.volume) (hmeas_b : (𝓝 b) measure_theory.measure_space.volume) (ha : (𝓝 ca)) (hb : (𝓝 cb)) :
has_fderiv_at (λ (p : × ), ∫ (x : ) in p.fst..p.snd, f x) - (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 interval_integral.integral_has_fderiv_at {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } (hmeas_a : (𝓝 a) measure_theory.measure_space.volume) (hmeas_b : (𝓝 b) measure_theory.measure_space.volume) (ha : a) (hb : b) :
has_fderiv_at (λ (p : × ), ∫ (x : ) in p.fst..p.snd, f x) (f b) - (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 interval_integral.fderiv_integral_of_tendsto_ae {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {ca cb : E} {a b : } (hmeas_a : (𝓝 a) measure_theory.measure_space.volume) (hmeas_b : (𝓝 b) measure_theory.measure_space.volume) (ha : (𝓝 ca)) (hb : (𝓝 cb)) :
(λ (p : × ), ∫ (x : ) in p.fst..p.snd, f x) (a, b) =

Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has finite limits `ca` and `cb` almost surely as `x` tends to `a` and `b`, respectively, then `fderiv` derivative of `(u, v) ↦ ∫ x in u..v, f x` at `(a, b)` equals `(u, v) ↦ v • cb - u • ca`.

theorem interval_integral.fderiv_integral {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } (hmeas_a : (𝓝 a) measure_theory.measure_space.volume) (hmeas_b : (𝓝 b) measure_theory.measure_space.volume) (ha : a) (hb : b) :
(λ (p : × ), ∫ (x : ) in p.fst..p.snd, f x) (a, b) = (f b) - (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 interval_integral.integral_has_deriv_at_of_tendsto_ae_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {a b : } (hmeas : (𝓝 b) measure_theory.measure_space.volume) (hb : (𝓝 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`.

theorem interval_integral.integral_has_deriv_at_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } (hmeas : (𝓝 b) measure_theory.measure_space.volume) (hb : 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`.

theorem interval_integral.deriv_integral_of_tendsto_ae_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {a b : } (hmeas : (𝓝 b) measure_theory.measure_space.volume) (hb : (𝓝 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`.

theorem interval_integral.deriv_integral_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } (hmeas : (𝓝 b) measure_theory.measure_space.volume) (hb : 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`.

theorem interval_integral.integral_has_deriv_at_of_tendsto_ae_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {a b : } (hmeas : (𝓝 a) measure_theory.measure_space.volume) (ha : (𝓝 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`.

theorem interval_integral.integral_has_deriv_at_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } (hmeas : (𝓝 a) measure_theory.measure_space.volume) (ha : 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`.

theorem interval_integral.deriv_integral_of_tendsto_ae_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {a b : } (hmeas : (𝓝 a) measure_theory.measure_space.volume) (hb : (𝓝 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`.

theorem interval_integral.deriv_integral_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } (hmeas : (𝓝 a) measure_theory.measure_space.volume) (hb : 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 #

theorem interval_integral.integral_has_fderiv_within_at_of_tendsto_ae {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {ca cb : E} {la lb : filter } {a b : } {s t : set } [ la] [ lb] (hmeas_a : measure_theory.measure_space.volume) (hmeas_b : measure_theory.measure_space.volume) (ha : (𝓝 ca)) (hb : (𝓝 cb)) :
has_fderiv_within_at (λ (p : × ), ∫ (x : ) in p.fst..p.snd, f x) - (s.prod 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` `𝓝[Iic a] a` `Iic b` `𝓝[Iic b] b`
`Ici a` `𝓝[Ioi a] a` `Ici b` `𝓝[Ioi b] b`
`{a}` `⊥` `{b}` `⊥`
`univ` `𝓝 a` `univ` `𝓝 b`
theorem interval_integral.integral_has_fderiv_within_at {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {la lb : filter } {a b : } (hmeas_a : measure_theory.measure_space.volume) (hmeas_b : measure_theory.measure_space.volume) {s t : set } [ la] [ lb] (ha : la (𝓝 (f a))) (hb : lb (𝓝 (f b))) :
has_fderiv_within_at (λ (p : × ), ∫ (x : ) in p.fst..p.snd, f x) (f b) - (f a)) (s.prod 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` `𝓝[Iic a] a` `Iic b` `𝓝[Iic b] b`
`Ici a` `𝓝[Ioi a] a` `Ici b` `𝓝[Ioi b] b`
`{a}` `⊥` `{b}` `⊥`
`univ` `𝓝 a` `univ` `𝓝 b`

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

theorem interval_integral.fderiv_within_integral_of_tendsto_ae {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {ca cb : E} {la lb : filter } {a b : } (hmeas_a : measure_theory.measure_space.volume) (hmeas_b : measure_theory.measure_space.volume) {s t : set } [ la] [ lb] (ha : (𝓝 ca)) (hb : (𝓝 cb)) (hs : . "unique_diff_within_at_Ici_Iic_univ") (ht : . "unique_diff_within_at_Ici_Iic_univ") :
(λ (p : × ), ∫ (x : ) in p.fst..p.snd, f x) (s.prod t) (a, b) =

Let `f` be a measurable function integrable on `a..b`. Choose `s ∈ {Iic a, Ici a, univ}` and `t ∈ {Iic b, Ici b, univ}`. Suppose that `f` tends to `ca` and `cb` almost surely at the filters `la` and `lb` from the table below. Then `fderiv_within ℝ (λ p, ∫ x in p.1..p.2, f x) (s.prod t)` is equal to `(u, v) ↦ u • cb - v • ca`.

`s` `la` `t` `lb`
`Iic a` `𝓝[Iic a] a` `Iic b` `𝓝[Iic b] b`
`Ici a` `𝓝[Ioi a] a` `Ici b` `𝓝[Ioi b] b`
`univ` `𝓝 a` `univ` `𝓝 b`
theorem interval_integral.integral_has_deriv_within_at_of_tendsto_ae_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {a b : } {s t : set } [ (𝓝[t] b)] (hmeas : (𝓝[t] b) measure_theory.measure_space.volume) (hb : (𝓝 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`.

theorem interval_integral.integral_has_deriv_within_at_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } {s t : set } [ (𝓝[t] b)] (hmeas : (𝓝[t] b) measure_theory.measure_space.volume) (hb : 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`.

theorem interval_integral.deriv_within_integral_of_tendsto_ae_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {a b : } {s t : set } [ (𝓝[t] b)] (hmeas : (𝓝[t] b) measure_theory.measure_space.volume) (hb : (𝓝 c)) (hs : . "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`.

theorem interval_integral.deriv_within_integral_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } {s t : set } [ (𝓝[t] b)] (hmeas : (𝓝[t] b) measure_theory.measure_space.volume) (hb : b) (hs : . "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`.

theorem interval_integral.integral_has_deriv_within_at_of_tendsto_ae_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {a b : } {s t : set } [ (𝓝[t] a)] (hmeas : (𝓝[t] a) measure_theory.measure_space.volume) (ha : (𝓝 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`.

theorem interval_integral.integral_has_deriv_within_at_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } {s t : set } [ (𝓝[t] a)] (hmeas : (𝓝[t] a) measure_theory.measure_space.volume) (ha : 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`.

theorem interval_integral.deriv_within_integral_of_tendsto_ae_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {c : E} {a b : } {s t : set } [ (𝓝[t] a)] (hmeas : (𝓝[t] a) measure_theory.measure_space.volume) (ha : (𝓝 c)) (hs : . "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`.

theorem interval_integral.deriv_within_integral_left {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } {s t : set } [ (𝓝[t] a)] (hmeas : (𝓝[t] a) measure_theory.measure_space.volume) (ha : a) (hs : . "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`.

### Fundamental theorem of calculus, part 2 #

This section contains theorems pertaining to FTC-2 for interval integrals.

theorem interval_integral.differentiable_on_integral_of_continuous {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a : } {s : set } (hintg : ∀ (x : ), ) (hcont : continuous f) :
(λ (u : ), ∫ (x : ) in a..u, f x) s

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

theorem interval_integral.continuous_on_integral_of_continuous {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a : } {s : set } (hintg : ∀ (x : ), ) (hcont : continuous f) :
continuous_on (λ (u : ), ∫ (x : ) in a..u, f x) s

The integral of a continuous function is continuous on a real set `s`. This is true even without the assumption of continuity, but a proof of that fact does not yet exist in mathlib.

theorem interval_integral.integral_eq_sub_of_has_deriv_right_of_le {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } {f' : → E} (hab : a b) (hcont : (set.Icc a b)) (hderiv : ∀ (x : ), x b (f' x) (set.Ici x) x) (hcont' : (set.Icc 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 continuous on `[a, b]`, then `∫ y in a..b, f' y` equals `f b - f a`.

theorem interval_integral.integral_eq_sub_of_has_deriv_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } {f' : → E} (hcont : b)) (hderiv : ∀ (x : ), x set.Ico (min a b) (max a b) (f' x) (set.Ici x) x) (hcont' : 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 continuous on `[a, b]` then `∫ y in a..b, f' y` equals `f b - f a`.

theorem interval_integral.integral_eq_sub_of_has_deriv_at' {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } {f' : → E} (hcont : b)) (hderiv : ∀ (x : ), x set.Ioo (min a b) (max a b) (f' x) x) (hcont' : 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 derivative at `f' x` for all `x` in `(a, b)`, and `f'` is continuous on `[a, b]`, then `∫ y in a..b, f' y` equals `f b - f a`.

theorem interval_integral.integral_eq_sub_of_has_deriv_at'_of_le {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } {f' : → E} (hab : a b) (hcont : b)) (hderiv : ∀ (x : ), x b (f' x) x) (hcont' : 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 continuous on `[a, b]`, then `∫ y in a..b, f' y` equals `f b - f a`.

theorem interval_integral.integral_eq_sub_of_has_deriv_at {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } {f' : → E} (hderiv : ∀ (x : ), x b (f' x) x) (hcont' : 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 continuous on `[a, b]`, then `∫ y in a..b, f' y` equals `f b - f a`.

theorem interval_integral.integral_deriv_eq_sub {E : Type u_4} [normed_group E] [ E] [borel_space E] {f : → E} {a b : } (hderiv : ∀ (x : ), x b) (hcont' : b)) :
∫ (y : ) in a..b, 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 continuous on `[a, b]`, then `∫ y in a..b, deriv f y` equals `f b - f a`.

theorem interval_integral.integral_deriv_eq_sub' {E : Type u_4} [normed_group E] [ E] [borel_space E] {a b : } {f' : → E} (f : → E) (hderiv : = f') (hdiff : ∀ (x : ), x b) (hcont' : b)) :
∫ (y : ) in a..b, f' y = f b - f a

### Integration by parts #

theorem interval_integral.integral_deriv_mul_eq_sub {a b : } {u v u' v' : } (hu : ∀ (x : ), x b (u' x) x) (hv : ∀ (x : ), x b (v' x) x) (hcu' : b)) (hcv' : b)) :
∫ (x : ) in a..b, (u' x) * v x + (u x) * v' x = (u b) * v b - (u a) * v a
theorem interval_integral.integral_mul_deriv_eq_deriv_mul {a b : } {u v u' v' : } (hu : ∀ (x : ), x b (u' x) x) (hv : ∀ (x : ), x b (v' x) x) (hcu' : b)) (hcv' : b)) :
∫ (x : ) in a..b, (u x) * v' x = (u b) * v b - (u a) * v a - ∫ (x : ) in a..b, (v x) * u' x