# 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 ifs in the definition, we define interval_integrable f μ a b as integrable_on f (Ioc a b) μ ∧ integrable_on f (Ioc b a) μ. For any a, b one of these intervals is empty and the other coincides with Ioc (min a b) (max a b).

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

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

### Choice of the interval

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

• this way ∫ x in a..b, f x ∂μ + ∫ x in b..c, f x ∂μ = ∫ x in a..c, f x ∂μ holds 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

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

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

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 (f + g) μ a b

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 (f - g) μ 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 : α} (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)

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 μ

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 μ

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

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 : ennreal) :
(x : α) in a..b, f x c μ = c.to_real (x : α) in a..b, f x μ

theorem interval_integral.integral_comp_add_right {E : Type u_4} [normed_group E] [ E] [borel_space E] (a b c : ) (f : → E)  :
∫ (x : ) in a..b, f (x + c) = ∫ (x : ) in a + c..b + c, f x

theorem interval_integral.integral_comp_mul_right {E : Type u_4} [normed_group E] [ E] [borel_space E] {c : } (hc : 0 < c) (a b : ) (f : → E)  :
∫ (x : ) in a..b, f (x * c) = c⁻¹ ∫ (x : ) in a * c..b * c, f x

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

### 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_filters around a; let (lb, lb') be a pair of FTC_filters around b. Suppose that f has finite limits ca and cb at la' ⊓ μ.ae and lb' ⊓ μ.ae, respectively. Then ∫ x in va..vb, f x ∂μ - ∫ x in ua..ub, f x ∂μ = ∫ x in ub..vb, cb ∂μ - ∫ x in ua..va, ca ∂μ + o(∥∫ x in ua..va, (1:ℝ) ∂μ∥ + ∥∫ x in ub..vb, (1:ℝ) ∂μ∥) as ua and va tend to la while ub and vb tend to lb.

This theorem is formulated with integral of constants instead of measures in the right hand sides for two reasons: first, this way we avoid min/max in the statements; second, often it is possible to write better simp lemmas for these integrals, see integral_const and integral_const_of_cdf.

In the next subsection we apply this theorem to prove various theorems about differentiability of the integral w.r.t. Lebesgue measure.

@[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
@[instance]
def interval_integral.FTC_filter.pure {β : Type u_2} [linear_order β] (a : β) :

@[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 β}  :

@[instance]
def interval_integral.FTC_filter.nhds {β : Type u_2} [linear_order β] (a : β) :
(𝓝 a)

@[instance]
def interval_integral.FTC_filter.nhds_univ {β : Type u_2} [linear_order β] (a : β) :
(𝓝 a)

@[instance]
def interval_integral.FTC_filter.nhds_left {β : Type u_2} [linear_order β] (a : β) :
(𝓝[] a)

@[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_filters around a; let (lb, lb') be a pair of FTC_filters around b. Suppose that f has finite limits ca and cb at la' ⊓ μ.ae and lb' ⊓ μ.ae, respectively. Then ∫ x in va..vb, f x ∂μ - ∫ x in ua..ub, f x ∂μ = ∫ x in ub..vb, cb ∂μ - ∫ x in ua..va, ca ∂μ + o(∥∫ x in ua..va, (1:ℝ) ∂μ∥ + ∥∫ x in ub..vb, (1:ℝ) ∂μ∥) as ua and va tend to la while ub and vb tend to lb.

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_filters around b. Suppose that f has a finite limit c at lb' ⊓ μ.ae.

Then ∫ x in a..v, f x ∂μ - ∫ x in a..u, f x ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, (1:ℝ) ∂μ) as u and v tend to lb.

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_filters around a. Suppose that f has a finite limit c at la' ⊓ μ.ae.

Then ∫ x in v..b, f x ∂μ - ∫ x in u..b, f x ∂μ = -∫ x in u..v, c ∂μ + o(∫ x in u..v, (1:ℝ) ∂μ) as u and v tend to la.

### Fundamental theorem of calculus-1 for Lebesgue measure

In this section we restate theorems from the previous section for Lebesgue measure. In particular, we prove that ∫ x in u..v, f x is strictly differentiable in (u, v) at (a, b) provided that f is integrable on a..b and is continuous at a and b.

#### Auxiliary is_o statements

In this section we prove several lemmas that can be interpreted as strict differentiability of (u, v) ↦ ∫ x in u..v, f x ∂μ in u and/or v at a filter. The statements use is_o because we have no definition of has_strict_(f)deriv_at_filter in the library.

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] and has a right derivative at f' x for all x in [a, b), and f' is continuous on [a, b] and measurable, 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] (where a ≤ b) and has a right derivative at f' x for all x in [a, b), and f' is continuous on [a, b] and measurable, 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.Ico (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] and measurable, 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] and measurable, 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.