mathlib documentation

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:

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.

FTC-2 and corollaries #

We use FTC-1 to prove several versions of FTC-2 for the Lebesgue measure, using a similar naming scheme as for the versions of FTC-1. They include:

We then derive additional integration techniques from FTC-2:

Many applications of these theorems can be found in the file analysis.special_functions.integrals.

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:

FTC_filter class #

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

This typeclass has 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

Almost everywhere on an interval #

theorem ae_interval_oc_iff {α : Type u_1} [linear_order α] [measurable_space α] {μ : measure_theory.measure α} {a b : α} {P : α → Prop} :
(∀ᵐ (x : α) ∂μ, x set.interval_oc a bP x) (∀ᵐ (x : α) ∂μ, x set.Ioc a bP x) ∀ᵐ (x : α) ∂μ, x set.Ioc b aP x
theorem ae_measurable_interval_oc_iff {α : Type u_1} [linear_order α] [measurable_space α] {a b : α} {μ : measure_theory.measure α} {β : Type u_2} [measurable_space β] {f : α → β} :
theorem ae_interval_oc_iff' {α : Type u_1} [linear_order α] [measurable_space α] {μ : measure_theory.measure α} {a b : α} {P : α → Prop} [topological_space α] [opens_measurable_space α] [order_closed_topology α] :
(∀ᵐ (x : α) ∂μ, x set.interval_oc a bP x) (∀ᵐ (x : α) ∂μ.restrict (set.Ioc a b), P x) ∀ᵐ (x : α) ∂μ.restrict (set.Ioc b a), P x

Integrability at an interval #

def interval_integrable {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [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 interval_integrable_iff {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a b : α} {μ : measure_theory.measure α} :

A function is interval integrable with respect to a given measure μ on interval a b if and only if it is integrable on Ioc (min a b) (max a b) with respect to μ. This is an equivalent defintion of interval_integrable.

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

If a function is interval integrable with respect to a given measure μ on interval a b then it is integrable on Ioc (min a b) (max a b) with respect to μ.

theorem measure_theory.integrable.interval_integrable {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a b : α} {μ : measure_theory.measure α} (hf : measure_theory.integrable f μ) :

If a function is integrable with respect to a given measure μ then it is interval integrable with respect to μ on interval a b.

theorem interval_integrable.symm {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a b : α} {μ : measure_theory.measure α} (h : interval_integrable f μ a b) :
theorem interval_integrable.refl {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a : α} {μ : measure_theory.measure α} :
theorem interval_integrable.trans {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a b c : α} {μ : measure_theory.measure α} (hab : interval_integrable f μ a b) (hbc : interval_integrable f μ b c) :
theorem interval_integrable.trans_iterate {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {μ : measure_theory.measure α} {a : → α} {n : } (hint : ∀ (k : ), k < ninterval_integrable f μ (a k) (a (k + 1))) :
interval_integrable f μ (a 0) (a n)
theorem interval_integrable.neg {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a b : α} {μ : measure_theory.measure α} [borel_space E] (h : interval_integrable f μ a b) :
theorem interval_integrable.norm {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a b : α} {μ : measure_theory.measure α} [opens_measurable_space E] (h : interval_integrable f μ a b) :
interval_integrable (λ (x : α), f x) μ a b
theorem interval_integrable.abs {α : Type u_1} [linear_order α] [measurable_space α] {a b : α} {μ : measure_theory.measure α} {f : α → } (h : interval_integrable f μ a b) :
interval_integrable (λ (x : α), abs (f x)) μ a b
theorem interval_integrable.mono {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a b c d : α} {μ ν : measure_theory.measure α} (hf : interval_integrable f ν a b) (h1 : set.interval c d set.interval a b) (h2 : μ ν) :
theorem interval_integrable.mono_set {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a b c d : α} {μ : measure_theory.measure α} (hf : interval_integrable f μ a b) (h : set.interval c d set.interval a b) :
theorem interval_integrable.mono_measure {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a b : α} {μ ν : measure_theory.measure α} (hf : interval_integrable f ν a b) (h : μ ν) :
theorem interval_integrable.mono_set_ae {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a b c d : α} {μ : measure_theory.measure α} (hf : interval_integrable f μ a b) (h : set.Ioc (min c d) (max c d) ≤ᵐ[μ] set.Ioc (min a b) (max a b)) :
theorem interval_integrable.ae_measurable {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a b : α} {μ : measure_theory.measure α} (h : interval_integrable f μ a b) :
theorem interval_integrable.ae_measurable' {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {a b : α} {μ : measure_theory.measure α} (h : interval_integrable f μ a b) :
theorem interval_integrable.smul {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [borel_space E] [normed_field 𝕜] [normed_space 𝕜 E] [measurable_space 𝕜] [opens_measurable_space 𝕜] {f : α → E} {a b : α} {μ : measure_theory.measure α} (h : interval_integrable f μ a b) (r : 𝕜) :
@[simp]
theorem interval_integrable.add {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [borel_space E] {f g : α → E} {a b : α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] (hf : interval_integrable f μ a b) (hg : interval_integrable g μ 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 α] [measurable_space α] [measurable_space E] [normed_group E] [borel_space E] {f g : α → E} {a b : α} {μ : measure_theory.measure α} [topological_space.second_countable_topology E] (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) :
interval_integrable (λ (x : α), f x - g x) μ 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 α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {μ : measure_theory.measure α} {l l' : filter α} (hfm : measurable_at_filter f l' μ) [filter.tendsto_Ixx_class set.Ioc l l'] [l'.is_measurably_generated] (hμ : μ.finite_at_filter l') {c : E} (hf : filter.tendsto f (l' μ.ae) (𝓝 c)) {u v : β → α} {lt : filter β} (hu : filter.tendsto u lt l) (hv : filter.tendsto v lt l) :
∀ᶠ (t : β) in lt, interval_integrable f μ (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 α] [measurable_space α] [measurable_space E] [normed_group E] {f : α → E} {μ : measure_theory.measure α} {l l' : filter α} (hfm : measurable_at_filter f l' μ) [filter.tendsto_Ixx_class set.Ioc l l'] [l'.is_measurably_generated] (hμ : μ.finite_at_filter l') {c : E} (hf : filter.tendsto f l' (𝓝 c)) {u v : β → α} {lt : filter β} (hu : filter.tendsto u lt l) (hv : filter.tendsto v lt l) :
∀ᶠ (t : β) in lt, interval_integrable f μ (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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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_of_le {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} (h : a b) :
(x : α) in a..b, f x μ = (x : α) in set.Ioc a b, f x μ
@[simp]
theorem interval_integral.integral_same {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} (h : b a) :
(x : α) in a..b, f x μ = - (x : α) in set.Ioc b a, f x μ
theorem interval_integral.integral_cases {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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_undef {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} (h : ¬interval_integrable f μ a b) :
(x : α) in a..b, f x μ = 0
theorem interval_integral.integral_non_ae_measurable {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} (hf : ¬ae_measurable f (μ.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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {a b : α} {f : α → E} {μ : measure_theory.measure α} (h : a b) (hf : ¬ae_measurable f (μ.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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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_of_norm_le_const_ae {E : Type u_4} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {a b : α} {f g : α → E} {μ : measure_theory.measure α} (hf : interval_integrable f μ a b) (hg : interval_integrable g μ 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {a b : α} {f g : α → E} {μ : measure_theory.measure α} (hf : interval_integrable f μ a b) (hg : interval_integrable g μ 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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_add_left {E : Type u_4} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {a b : } (f : → E) (d : ) :
∫ (x : ) in a..b, f (d + x) = ∫ (x : ) in d + a..d + b, f x
@[simp]
theorem interval_integral.integral_comp_mul_add {E : Type u_4} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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_Icc_eq_integral_Ioc {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {μ : measure_theory.measure α} {f : α → E} {a b : α} (ha : μ {a} = 0) :
(t : α) in set.Icc a b, f t μ = (t : α) in set.Ioc a b, f t μ
theorem interval_integral.integral_congr {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {f g : α → E} {μ : measure_theory.measure α} {a b : α} (h : set.eq_on f g (set.interval a 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {a b c : α} {f : α → E} {μ : measure_theory.measure α} (hab : interval_integrable f μ a b) (hbc : interval_integrable f μ 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {a b c : α} {f : α → E} {μ : measure_theory.measure α} (hab : interval_integrable f μ a b) (hbc : interval_integrable f μ b c) :
(x : α) in a..b, f x μ + (x : α) in b..c, f x μ = (x : α) in a..c, f x μ
theorem interval_integral.sum_integral_adjacent_intervals {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {f : α → E} {μ : measure_theory.measure α} {a : → α} {n : } (hint : ∀ (k : ), k < ninterval_integrable f μ (a k) (a (k + 1))) :
∑ (k : ) in finset.range n, (x : α) in a k..a (k + 1), f x μ = (x : α) in a 0..a n, f x μ
theorem interval_integral.integral_interval_sub_left {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {a b c : α} {f : α → E} {μ : measure_theory.measure α} (hab : interval_integrable f μ a b) (hac : interval_integrable f μ 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {a b c d : α} {f : α → E} {μ : measure_theory.measure α} (hab : interval_integrable f μ a b) (hcd : interval_integrable f μ c d) (hac : interval_integrable f μ 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {a b c d : α} {f : α → E} {μ : measure_theory.measure α} (hab : interval_integrable f μ a b) (hcd : interval_integrable f μ c d) (hac : interval_integrable f μ 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {a b c d : α} {f : α → E} {μ : measure_theory.measure α} (hab : interval_integrable f μ a b) (hcd : interval_integrable f μ c d) (hac : interval_integrable f μ 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 μ

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

theorem interval_integral.integral_congr_ae' {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {a b : α} {μ : measure_theory.measure α} {f g : α → E} (h : ∀ᵐ (x : α) ∂μ, x set.Ioc a bf x = g x) (h' : ∀ᵐ (x : α) ∂μ, x set.Ioc b af x = g x) :
(x : α) in a..b, f x μ = (x : α) in a..b, g x μ
theorem interval_integral.integral_congr_ae {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {a b : α} {μ : measure_theory.measure α} {f g : α → E} (h : ∀ᵐ (x : α) ∂μ, x set.interval_oc a bf x = g x) :
(x : α) in a..b, f x μ = (x : α) in a..b, g x μ
theorem interval_integral.integral_zero_ae {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {a b : α} {μ : measure_theory.measure α} {f : α → E} (h : ∀ᵐ (x : α) ∂μ, x set.interval_oc a bf x = 0) :
(x : α) in a..b, f x μ = 0
theorem interval_integral.integral_indicator {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_closed_topology α] [opens_measurable_space α] {μ : measure_theory.measure α} {a₁ a₂ a₃ : α} (h : a₂ set.Icc a₁ a₃) {f : α → E} :
(x : α) in a₁..a₃, {x : α | x a₂}.indicator f x μ = (x : α) in a₁..a₂, f x μ
theorem interval_integral.continuous_within_at_of_dominated_interval {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {X : Type u_6} [topological_space X] [topological_space.first_countable_topology X] {μ : measure_theory.measure α} {F : X → α → E} {x₀ : X} {bound : α → } {a b : α} {s : set X} (hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, ae_measurable (F x) (μ.restrict (set.interval_oc a b))) (hF_meas₀ : ae_measurable (F x₀) (μ.restrict (set.interval_oc a b))) (h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (t : α) ∂μ.restrict (set.interval_oc a b), F x t bound t) (bound_integrable : interval_integrable bound μ a b) (h_cont : ∀ᵐ (t : α) ∂μ.restrict (set.interval_oc a b), continuous_within_at (λ (x : X), F x t) s x₀) :
continuous_within_at (λ (x : X), (t : α) in a..b, F x t μ) s x₀

Continuity of interval integral with respect to a parameter, at a point within a set. Given F : X → α → E, assume F x is ae-measurable on [a, b] for x in a neighborhood of x₀ within s and at x₀, and assume it is bounded by a function integrable on [a, b] independent of x in a neighborhood of x₀ within s. If (λ x, F x t) is continuous at x₀ within s for almost every t in [a, b] then the same holds for (λ x, ∫ t in a..b, F x t ∂μ) s x₀.

theorem interval_integral.continuous_at_of_dominated_interval {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {X : Type u_6} [topological_space X] [topological_space.first_countable_topology X] {μ : measure_theory.measure α} {F : X → α → E} {x₀ : X} {bound : α → } {a b : α} (hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, ae_measurable (F x) (μ.restrict (set.interval_oc a b))) (h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : α) ∂μ.restrict (set.interval_oc a b), F x t bound t) (bound_integrable : interval_integrable bound μ a b) (h_cont : ∀ᵐ (t : α) ∂μ.restrict (set.interval_oc a b), continuous_at (λ (x : X), F x t) x₀) :
continuous_at (λ (x : X), (t : α) in a..b, F x t μ) x₀

Continuity of interval integral with respect to a parameter at a point. Given F : X → α → E, assume F x is ae-measurable on [a, b] for x in a neighborhood of x₀, and assume it is bounded by a function integrable on [a, b] independent of x in a neighborhood of x₀. If (λ x, F x t) is continuous at x₀ for almost every t in [a, b] then the same holds for (λ x, ∫ t in a..b, F x t ∂μ) s x₀.

theorem interval_integral.continuous_of_dominated_interval {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {X : Type u_6} [topological_space X] [topological_space.first_countable_topology X] {μ : measure_theory.measure α} {F : X → α → E} {bound : α → } {a b : α} (hF_meas : ∀ (x : X), ae_measurable (F x) (μ.restrict (set.interval_oc a b))) (h_bound : ∀ (x : X), ∀ᵐ (t : α) ∂μ.restrict (set.interval_oc a b), F x t bound t) (bound_integrable : interval_integrable bound μ a b) (h_cont : ∀ᵐ (t : α) ∂μ.restrict (set.interval_oc a b), continuous (λ (x : X), F x t)) :
continuous (λ (x : X), (t : α) in a..b, F x t μ)

Continuity of interval integral with respect to a parameter. Given F : X → α → E, assume each F x is ae-measurable on [a, b], and assume it is bounded by a function integrable on [a, b] independent of x. If (λ x, F x t) is continuous for almost every t in [a, b] then the same holds for (λ x, ∫ t in a..b, F x t ∂μ) s x₀.

theorem interval_integral.continuous_within_at_primitive {α : Type u_1} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] [topological_space α] [order_topology α] [opens_measurable_space α] [topological_space.first_countable_topology α] {μ : measure_theory.measure α} {f : α → E} {a b₀ b₁ b₂ : α} (hb₀ : μ {b₀} = 0) (h_int : interval_integrable f μ (min a b₁) (max a b₂)) :
continuous_within_at (λ (b : α), (x : α) in a..b, f x μ) (set.Icc b₁ b₂) b₀
theorem interval_integral.integral_eq_zero_iff_of_le_of_nonneg_ae {α : Type u_1} [linear_order α] [measurable_space α] {f : α → } {a b : α} {μ : measure_theory.measure α} (hab : a b) (hf : 0 ≤ᵐ[μ.restrict (set.Ioc a b)] f) (hfi : interval_integrable f μ a b) :
(x : α) in a..b, f x μ = 0 f =ᵐ[μ.restrict (set.Ioc a b)] 0
theorem interval_integral.integral_eq_zero_iff_of_nonneg_ae {α : Type u_1} [linear_order α] [measurable_space α] {f : α → } {a b : α} {μ : measure_theory.measure α} (hf : 0 ≤ᵐ[μ.restrict (set.Ioc a b set.Ioc b a)] f) (hfi : interval_integrable f μ a b) :
(x : α) in a..b, f x μ = 0 f =ᵐ[μ.restrict (set.Ioc a b set.Ioc b a)] 0
theorem interval_integral.integral_pos_iff_support_of_nonneg_ae' {α : Type u_1} [linear_order α] [measurable_space α] {f : α → } {a b : α} {μ : measure_theory.measure α} (hf : 0 ≤ᵐ[μ.restrict (set.Ioc a b set.Ioc b a)] f) (hfi : interval_integrable f μ a b) :
0 < (x : α) in a..b, f x μ a < b 0 < μ (function.support f set.Ioc a b)
theorem interval_integral.integral_pos_iff_support_of_nonneg_ae {α : Type u_1} [linear_order α] [measurable_space α] {f : α → } {a b : α} {μ : measure_theory.measure α} (hf : 0 ≤ᵐ[μ] f) (hfi : interval_integrable f μ a b) :
0 < (x : α) in a..b, f x μ a < b 0 < μ (function.support f set.Ioc a b)
theorem interval_integral.integral_nonneg_of_ae_restrict {α : Type u_1} [linear_order α] [measurable_space α] {f : α → } {a b : α} {μ : measure_theory.measure α} (hab : a b) (hf : 0 ≤ᵐ[μ.restrict (set.Icc a b)] f) :
0 (u : α) in a..b, f u μ
theorem interval_integral.integral_nonneg_of_ae {α : Type u_1} [linear_order α] [measurable_space α] {f : α → } {a b : α} {μ : measure_theory.measure α} (hab : a b) (hf : 0 ≤ᵐ[μ] f) :
0 (u : α) in a..b, f u μ
theorem interval_integral.integral_nonneg_of_forall {α : Type u_1} [linear_order α] [measurable_space α] {f : α → } {a b : α} {μ : measure_theory.measure α} (hab : a b) (hf : ∀ (u : α), 0 f u) :
0 (u : α) in a..b, f u μ
theorem interval_integral.integral_nonneg {α : Type u_1} [linear_order α] [measurable_space α] {f : α → } {a b : α} {μ : measure_theory.measure α} (hab : a b) [topological_space α] [opens_measurable_space α] [order_closed_topology α] (hf : ∀ (u : α), u set.Icc a b0 f u) :
0 (u : α) in a..b, f u μ
theorem interval_integral.norm_integral_le_integral_norm {α : Type u_1} [linear_order α] [measurable_space α] {f : α → } {a b : α} {μ : measure_theory.measure α} (hab : a b) :
(x : α) in a..b, f x μ (x : α) in a..b, f x μ
theorem interval_integral.abs_integral_le_integral_abs {α : Type u_1} [linear_order α] [measurable_space α] {f : α → } {a b : α} {μ : measure_theory.measure α} (hab : a b) :
abs ( (x : α) in a..b, f x μ) (x : α) in a..b, abs (f x) μ
theorem interval_integral.integral_mono_ae_restrict {α : Type u_1} [linear_order α] [measurable_space α] {f g : α → } {a b : α} {μ : measure_theory.measure α} (hab : a b) (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) (h : f ≤ᵐ[μ.restrict (set.Icc a b)] g) :
(u : α) in a..b, f u μ (u : α) in a..b, g u μ
theorem interval_integral.integral_mono_ae {α : Type u_1} [linear_order α] [measurable_space α] {f g : α → } {a b : α} {μ : measure_theory.measure α} (hab : a b) (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) (h : f ≤ᵐ[μ] g) :
(u : α) in a..b, f u μ (u : α) in a..b, g u μ
theorem interval_integral.integral_mono_on {α : Type u_1} [linear_order α] [measurable_space α] {f g : α → } {a b : α} {μ : measure_theory.measure α} (hab : a b) (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) [topological_space α] [opens_measurable_space α] [order_closed_topology α] (h : ∀ (x : α), x set.Icc a bf x g x) :
(u : α) in a..b, f u μ (u : α) in a..b, g u μ
theorem interval_integral.integral_mono {α : Type u_1} [linear_order α] [measurable_space α] {f g : α → } {a b : α} {μ : measure_theory.measure α} (hab : a b) (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) (h : f g) :
(u : α) in a..b, f u μ (u : α) in a..b, g 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_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 β] [measurable_space β] [topological_space β] (a : out_param β) (outer : filter β) (inner : out_param (filter β)) :
Prop

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

Instances
theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae' {α : Type u_1} {β : Type u_2} {E : Type u_4} [linear_order α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : α → E} {c : E} {l l' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [l'.is_measurably_generated] [filter.tendsto_Ixx_class set.Ioc l l'] (hfm : measurable_at_filter f l' μ) (hf : filter.tendsto f (l' μ.ae) (𝓝 c)) (hl : μ.finite_at_filter l') (hu : filter.tendsto u lt l) (hv : filter.tendsto v 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : α → E} {c : E} {l l' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [l'.is_measurably_generated] [filter.tendsto_Ixx_class set.Ioc l l'] (hfm : measurable_at_filter f l' μ) (hf : filter.tendsto f (l' μ.ae) (𝓝 c)) (hl : μ.finite_at_filter l') (hu : filter.tendsto u lt l) (hv : filter.tendsto v 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : α → E} {c : E} {l l' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [l'.is_measurably_generated] [filter.tendsto_Ixx_class set.Ioc l l'] (hfm : measurable_at_filter f l' μ) (hf : filter.tendsto f (l' μ.ae) (𝓝 c)) (hl : μ.finite_at_filter l') (hu : filter.tendsto u lt l) (hv : filter.tendsto v 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : α → E} {a : α} {c : E} {l l' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [topological_space α] [measure_theory.locally_finite_measure μ] [interval_integral.FTC_filter a l l'] (hfm : measurable_at_filter f l' μ) (hf : filter.tendsto f (l' μ.ae) (𝓝 c)) (hu : filter.tendsto u lt l) (hv : filter.tendsto v 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : α → E} {a : α} {c : E} {l l' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [topological_space α] [measure_theory.locally_finite_measure μ] [interval_integral.FTC_filter a l l'] (hfm : measurable_at_filter f l' μ) (hf : filter.tendsto f (l' μ.ae) (𝓝 c)) (hu : filter.tendsto u lt l) (hv : filter.tendsto v 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : α → E} {a : α} {c : E} {l l' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [topological_space α] [measure_theory.locally_finite_measure μ] [interval_integral.FTC_filter a l l'] (hfm : measurable_at_filter f l' μ) (hf : filter.tendsto f (l' μ.ae) (𝓝 c)) (hu : filter.tendsto u lt l) (hv : filter.tendsto v 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space 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 : β → α} [topological_space α] [order_topology α] [borel_space α] [interval_integral.FTC_filter a la la'] [interval_integral.FTC_filter b lb lb'] [measure_theory.locally_finite_measure μ] (hab : interval_integrable f μ a b) (hmeas_a : measurable_at_filter f la' μ) (hmeas_b : measurable_at_filter f lb' μ) (ha_lim : filter.tendsto f (la' μ.ae) (𝓝 ca)) (hb_lim : filter.tendsto f (lb' μ.ae) (𝓝 cb)) (hua : filter.tendsto ua lt la) (hva : filter.tendsto va lt la) (hub : filter.tendsto ub lt lb) (hvb : filter.tendsto vb lt lb) :
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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : α → E} {a b : α} {c : E} {lb lb' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [topological_space α] [order_topology α] [borel_space α] [interval_integral.FTC_filter b lb lb'] [measure_theory.locally_finite_measure μ] (hab : interval_integrable f μ a b) (hmeas : measurable_at_filter f lb' μ) (hf : filter.tendsto f (lb' μ.ae) (𝓝 c)) (hu : filter.tendsto u lt lb) (hv : filter.tendsto v 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 α] [measurable_space α] [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : α → E} {a b : α} {c : E} {la la' : filter α} {lt : filter β} {μ : measure_theory.measure α} {u v : β → α} [topological_space α] [order_topology α] [borel_space α] [interval_integral.FTC_filter a la la'] [measure_theory.locally_finite_measure μ] (hab : interval_integrable f μ a b) (hmeas : measurable_at_filter f la' μ) (hf : filter.tendsto f (la' μ.ae) (𝓝 c)) (hu : filter.tendsto u lt la) (hv : filter.tendsto v 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : → E} {c : E} {l l' : filter } {lt : filter β} {a : } [interval_integral.FTC_filter a l l'] (hfm : measurable_at_filter f l' measure_theory.measure_space.volume) (hf : filter.tendsto f (l' measure_theory.measure_space.volume.ae) (𝓝 c)) {u v : β → } (hu : filter.tendsto u lt l) (hv : filter.tendsto v 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : → E} {ca cb : E} {la la' lb lb' : filter } {lt : filter β} {a b : } {ua ub va vb : β → } [interval_integral.FTC_filter a la la'] [interval_integral.FTC_filter b lb lb'] (hab : interval_integrable f measure_theory.measure_space.volume a b) (hmeas_a : measurable_at_filter f la' measure_theory.measure_space.volume) (hmeas_b : measurable_at_filter f lb' measure_theory.measure_space.volume) (ha_lim : filter.tendsto f (la' measure_theory.measure_space.volume.ae) (𝓝 ca)) (hb_lim : filter.tendsto f (lb' measure_theory.measure_space.volume.ae) (𝓝 cb)) (hua : filter.tendsto ua lt la) (hva : filter.tendsto va lt la) (hub : filter.tendsto ub lt lb) (hvb : filter.tendsto vb lt lb) :
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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : → E} {c : E} {lb lb' : filter } {lt : filter β} {a b : } {u v : β → } [interval_integral.FTC_filter b lb lb'] (hab : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : measurable_at_filter f lb' measure_theory.measure_space.volume) (hf : filter.tendsto f (lb' measure_theory.measure_space.volume.ae) (𝓝 c)) (hu : filter.tendsto u lt lb) (hv : filter.tendsto v 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : → E} {c : E} {la la' : filter } {lt : filter β} {a b : } {u v : β → } [interval_integral.FTC_filter a la la'] (hab : interval_integrable f measure_theory.measure_space.volume a b) (hmeas : measurable_at_filter f la' measure_theory.measure_space.volume) (hf : filter.tendsto f (la' measure_theory.measure_space.volume.ae) (𝓝 c)) (hu : filter.tendsto u lt la) (hv : filter.tendsto v 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,

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

Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f is continuous at a and b, then (u, v) ↦ ∫ x in u..v, f x has derivative (u, v) ↦ v • cb - u • ca at (a, b) in the sense of strict differentiability.

First Fundamental Theorem of Calculus: if f : ℝ → E is integrable on a..b and f x has a finite limit c almost surely at b, then u ↦ ∫ x in a..u, f x has derivative c at b in the sense of strict differentiability.

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

Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f x has a finite limit c almost surely at a, then u ↦ ∫ x in u..b, f x has derivative -c at a in the sense of strict differentiability.

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

Fréchet differentiability #

In this subsection we restate results from the previous subsection in terms of has_fderiv_at, has_deriv_at, fderiv, and deriv.

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

Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f is continuous at a and b, then (u, v) ↦ ∫ x in u..v, f x has derivative (u, v) ↦ v • cb - u • ca at (a, b).

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

Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f is continuous at a and b, then fderiv derivative of (u, v) ↦ ∫ x in u..v, f x at (a, b) equals (u, v) ↦ v • cb - u • ca.

Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f x has a finite limit c almost surely at b, then u ↦ ∫ x in a..u, f x has derivative c at b.

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

Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f has a finite limit c almost surely at b, then the derivative of u ↦ ∫ x in a..u, f x at b equals c.

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

Fundamental theorem of calculus-1: if f : ℝ → E is integrable on a..b and f x has a finite limit c almost surely at a, then u ↦ ∫ x in u..b, f x has derivative -c at a.

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

Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f has a finite limit c almost surely at a, then the derivative of u ↦ ∫ x in u..b, f x at a equals -c.

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

One-sided derivatives #

Let f be a measurable function integrable on a..b. The function (u, v) ↦ ∫ x in u..v, f x has derivative (u, v) ↦ v • cb - u • ca within s × t at (a, b), where s ∈ {Iic a, {a}, Ici a, univ} and t ∈ {Iic b, {b}, Ici b, univ} provided that f tends to ca and cb almost surely at the filters la and lb from the following table.

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

Let f be a measurable function integrable on a..b. The function (u, v) ↦ ∫ x in u..v, f x has derivative (u, v) ↦ v • f b - u • f a within s × t at (a, b), where s ∈ {Iic a, {a}, Ici a, univ} and t ∈ {Iic b, {b}, Ici b, univ} provided that f tends to f a and f b at the filters la and lb from the following table. In most cases this assumption is definitionally equal continuous_at f _ or continuous_within_at f _ _.

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

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

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

s la t lb
Iic a 𝓝[Iic a] a Iic b 𝓝[Iic b] b
Ici a 𝓝[Ioi a] a Ici b 𝓝[Ioi b] b
univ 𝓝 a univ 𝓝 b

Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x has a finite limit c almost surely as x tends to b from the right or from the left, then u ↦ ∫ x in a..u, f x has right (resp., left) derivative c at b.

Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x is continuous from the left or from the right at b, then u ↦ ∫ x in a..u, f x has left (resp., right) derivative f b at b.

Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x has a finite limit c almost surely as x tends to b from the right or from the left, then the right (resp., left) derivative of u ↦ ∫ x in a..u, f x at b equals c.

Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x is continuous on the right or on the left at b, then the right (resp., left) derivative of u ↦ ∫ x in a..u, f x at b equals f b.

Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x has a finite limit c almost surely as x tends to a from the right or from the left, then u ↦ ∫ x in u..b, f x has right (resp., left) derivative -c at a.

Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x is continuous from the left or from the right at a, then u ↦ ∫ x in u..b, f x has left (resp., right) derivative -f a at a.

Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x has a finite limit c almost surely as x tends to a from the right or from the left, then the right (resp., left) derivative of u ↦ ∫ x in u..b, f x at a equals -c.

Fundamental theorem of calculus: if f : ℝ → E is integrable on a..b and f x is continuous on the right or on the left at a, then the right (resp., left) derivative of u ↦ ∫ x in u..b, f x at a equals -f a.

Fundamental theorem of calculus, part 2 #

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

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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : → E} {a : } {s : set } (hintg : ∀ (x : ), x sinterval_integrable f measure_theory.measure_space.volume a 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : → E} {a b : } {f' : → E} (hab : a b) (hcont : continuous_on f (set.Icc a b)) (hderiv : ∀ (x : ), x set.Ico a bhas_deriv_within_at f (f' x) (set.Ici x) x) (hcont' : continuous_on f' (set.Icc a b)) :
∫ (y : ) in a..b, f' y = f b - f a

Second Fundamental Theorem of Calculus: 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} [measurable_space E] [normed_group E] [topological_space.second_countable_topology E] [complete_space E] [normed_space E] [borel_space E] {f : → E} {a b : } {f' : → E} (hcont : continuous_on f (set.interval a b)) (hderiv : ∀ (x : ), x set.Ico (min a b) (max a b)has_deriv_within_at f (f' x) (set.Ici x) x) (hcont' : continuous_on f' (set.interval 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] then ∫ y in a..b, f' y equals f b - f a.