mathlib3 documentation

measure_theory.integral.interval_integral

Integral over an interval #

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

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.

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 set.uIoc a b = set.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 set.uIoc a b = set.Ioc (min a b) (max a b) instead of one of the other three possible intervals with the same endpoints for two reasons:

Tags #

integral

Integrability on an interval #

def interval_integrable {E : Type u_3} [normed_add_comm_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

A function is interval integrable with respect to a given measure μ on a..b if and only if it is integrable on uIoc a b with respect to μ. This is an equivalent definition of interval_integrable.

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

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

theorem interval_integrable_const_iff {E : Type u_3} [normed_add_comm_group E] {a b : } {μ : measure_theory.measure } {c : E} :
interval_integrable (λ (_x : ), c) μ a b c = 0 μ (set.uIoc a b) <
@[symm]
theorem interval_integrable.symm {E : Type u_3} [normed_add_comm_group E] {f : E} {a b : } {μ : measure_theory.measure } (h : interval_integrable f μ a b) :
@[refl]
@[trans]
theorem interval_integrable.trans {E : Type u_3} [normed_add_comm_group E] {f : E} {μ : measure_theory.measure } {a b c : } (hab : interval_integrable f μ a b) (hbc : interval_integrable f μ b c) :
theorem interval_integrable.trans_iterate_Ico {E : Type u_3} [normed_add_comm_group E] {f : E} {μ : measure_theory.measure } {a : } {m n : } (hmn : m n) (hint : (k : ), k set.Ico m n interval_integrable f μ (a k) (a (k + 1))) :
interval_integrable f μ (a m) (a n)
theorem interval_integrable.trans_iterate {E : Type u_3} [normed_add_comm_group E] {f : E} {μ : measure_theory.measure } {a : } {n : } (hint : (k : ), k < n interval_integrable f μ (a k) (a (k + 1))) :
interval_integrable f μ (a 0) (a n)
theorem interval_integrable.neg {E : Type u_3} [normed_add_comm_group E] {f : E} {a b : } {μ : measure_theory.measure } (h : interval_integrable f μ a b) :
theorem interval_integrable.norm {E : Type u_3} [normed_add_comm_group E] {f : E} {a b : } {μ : measure_theory.measure } (h : interval_integrable f μ a b) :
interval_integrable (λ (x : ), f x) μ a b
theorem interval_integrable.abs {a b : } {μ : measure_theory.measure } {f : } (h : interval_integrable f μ a b) :
interval_integrable (λ (x : ), |f x|) μ a b
theorem interval_integrable.mono {E : Type u_3} [normed_add_comm_group E] {f : E} {a b c d : } {μ ν : measure_theory.measure } (hf : interval_integrable f ν a b) (h1 : set.uIcc c d set.uIcc a b) (h2 : μ ν) :
theorem interval_integrable.mono_measure {E : Type u_3} [normed_add_comm_group E] {f : E} {a b : } {μ ν : measure_theory.measure } (hf : interval_integrable f ν a b) (h : μ ν) :
theorem interval_integrable.mono_set {E : Type u_3} [normed_add_comm_group E] {f : E} {a b c d : } {μ : measure_theory.measure } (hf : interval_integrable f μ a b) (h : set.uIcc c d set.uIcc a b) :
theorem interval_integrable.mono_set_ae {E : Type u_3} [normed_add_comm_group E] {f : E} {a b c d : } {μ : measure_theory.measure } (hf : interval_integrable f μ a b) (h : set.uIoc c d ≤ᵐ[μ] set.uIoc a b) :
theorem interval_integrable.mono_set' {E : Type u_3} [normed_add_comm_group E] {f : E} {a b c d : } {μ : measure_theory.measure } (hf : interval_integrable f μ a b) (hsub : set.uIoc c d set.uIoc a b) :
theorem interval_integrable.mono_fun {E : Type u_3} {F : Type u_4} [normed_add_comm_group E] {f : E} {a b : } {μ : measure_theory.measure } [normed_add_comm_group F] {g : F} (hf : interval_integrable f μ a b) (hgm : measure_theory.ae_strongly_measurable g (μ.restrict (set.uIoc a b))) (hle : (λ (x : ), g x) ≤ᵐ[μ.restrict (set.uIoc a b)] λ (x : ), f x) :
theorem interval_integrable.mono_fun' {E : Type u_3} [normed_add_comm_group E] {f : E} {a b : } {μ : measure_theory.measure } {g : } (hg : interval_integrable g μ a b) (hfm : measure_theory.ae_strongly_measurable f (μ.restrict (set.uIoc a b))) (hle : (λ (x : ), f x) ≤ᵐ[μ.restrict (set.uIoc a b)] g) :
theorem interval_integrable.smul {𝕜 : Type u_2} {E : Type u_3} [normed_add_comm_group E] [normed_field 𝕜] [normed_space 𝕜 E] {f : E} {a b : } {μ : measure_theory.measure } (h : interval_integrable f μ a b) (r : 𝕜) :
@[simp]
theorem interval_integrable.add {E : Type u_3} [normed_add_comm_group E] {f g : E} {a b : } {μ : measure_theory.measure } (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 {E : Type u_3} [normed_add_comm_group E] {f g : E} {a b : } {μ : measure_theory.measure } (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) :
interval_integrable (λ (x : ), f x - g x) μ a b
theorem interval_integrable.sum {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] {a b : } {μ : measure_theory.measure } (s : finset ι) {f : ι E} (h : (i : ι), i s interval_integrable (f i) μ a b) :
interval_integrable (s.sum (λ (i : ι), f i)) μ a b
theorem interval_integrable.mul_continuous_on {A : Type u_5} [normed_ring A] {a b : } {μ : measure_theory.measure } {f g : A} (hf : interval_integrable f μ a b) (hg : continuous_on g (set.uIcc a b)) :
interval_integrable (λ (x : ), f x * g x) μ a b
theorem interval_integrable.continuous_on_mul {A : Type u_5} [normed_ring A] {a b : } {μ : measure_theory.measure } {f g : A} (hf : interval_integrable f μ a b) (hg : continuous_on g (set.uIcc a b)) :
interval_integrable (λ (x : ), g x * f x) μ a b
@[simp]
theorem interval_integrable.const_mul {A : Type u_5} [normed_ring A] {a b : } {μ : measure_theory.measure } {f : A} (hf : interval_integrable f μ a b) (c : A) :
interval_integrable (λ (x : ), c * f x) μ a b
@[simp]
theorem interval_integrable.mul_const {A : Type u_5} [normed_ring A] {a b : } {μ : measure_theory.measure } {f : A} (hf : interval_integrable f μ a b) (c : A) :
interval_integrable (λ (x : ), f x * c) μ a b
@[simp]
theorem interval_integrable.div_const {a b : } {μ : measure_theory.measure } {𝕜 : Type u_1} {f : 𝕜} [normed_field 𝕜] (h : interval_integrable f μ a b) (c : 𝕜) :
interval_integrable (λ (x : ), f x / c) μ 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} {E : Type u_3} [normed_add_comm_group E] {f : E} {μ : measure_theory.measure } {l l' : filter } (hfm : strongly_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) (nhds 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} {E : Type u_3} [normed_add_comm_group E] {f : E} {μ : measure_theory.measure } {l l' : filter } (hfm : strongly_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' (nhds 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.

noncomputable def interval_integral {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_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
theorem interval_integral.integral_of_le {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_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_symm {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_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 {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_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 {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {μ : measure_theory.measure } (f : E) (a b : ) :
(x : ) in a..b, f x μ { (x : ) in set.uIoc a b, f x μ, - (x : ) in set.uIoc a b, f x μ}
theorem interval_integral.norm_integral_le_of_norm_le {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } {f : E} {μ : measure_theory.measure } {g : } (h : ∀ᵐ (t : ) μ.restrict (set.uIoc a b), f t g t) (hbound : interval_integrable g μ a b) :
(t : ) in a..b, f t μ | (t : ) in a..b, g t μ|
theorem interval_integral.norm_integral_le_of_norm_le_const {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b C : } {f : E} (h : (x : ), x set.uIoc a b f x C) :
(x : ) in a..b, f x C * |b - a|
@[simp]
theorem interval_integral.integral_add {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_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 μ
theorem interval_integral.integral_finset_sum {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } {μ : measure_theory.measure } {ι : Type u_1} {s : finset ι} {f : ι E} (h : (i : ι), i s interval_integrable (f i) μ a b) :
(x : ) in a..b, s.sum (λ (i : ι), f i x) μ = s.sum (λ (i : ι), (x : ) in a..b, f i x μ)
@[simp]
theorem interval_integral.integral_neg {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_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 {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_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 {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } {μ : measure_theory.measure } {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [smul_comm_class 𝕜 E] (r : 𝕜) (f : E) :
(x : ) in a..b, r f x μ = r (x : ) in a..b, f x μ
@[simp]
theorem interval_integral.integral_smul_const {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } {μ : measure_theory.measure } {𝕜 : Type u_1} [is_R_or_C 𝕜] [normed_space 𝕜 E] (f : 𝕜) (c : E) :
(x : ) in a..b, f x c μ = ( (x : ) in a..b, f x μ) c
@[simp]
theorem interval_integral.integral_const_mul {a b : } {μ : measure_theory.measure } {𝕜 : Type u_1} [is_R_or_C 𝕜] (r : 𝕜) (f : 𝕜) :
(x : ) in a..b, r * f x μ = r * (x : ) in a..b, f x μ
@[simp]
theorem interval_integral.integral_mul_const {a b : } {μ : measure_theory.measure } {𝕜 : Type u_1} [is_R_or_C 𝕜] (r : 𝕜) (f : 𝕜) :
(x : ) in a..b, f x * r μ = (x : ) in a..b, f x μ * r
@[simp]
theorem interval_integral.integral_div {a b : } {μ : measure_theory.measure } {𝕜 : Type u_1} [is_R_or_C 𝕜] (r : 𝕜) (f : 𝕜) :
(x : ) in a..b, f x / r μ = (x : ) in a..b, f x μ / r
theorem interval_integral.integral_const' {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } (c : E) :
(x : ) in a..b, c = (b - a) c
theorem interval_integral.integral_smul_measure {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_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_of_real {a b : } {μ : measure_theory.measure } {f : } :
(x : ) in a..b, (f x) μ = (x : ) in a..b, f x μ
theorem continuous_linear_map.interval_integral_apply {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [normed_add_comm_group E] [complete_space E] [normed_space E] {μ : measure_theory.measure } [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group F] [normed_space 𝕜 F] {a b : } {φ : (F →L[𝕜] E)} (hφ : interval_integrable φ μ a b) (v : F) :
( (x : ) in a..b, φ x μ) v = (x : ) in a..b, (φ x) v μ
theorem continuous_linear_map.interval_integral_comp_comm {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } {μ : measure_theory.measure } {f : E} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_add_comm_group F] [normed_space 𝕜 F] [normed_space F] [complete_space F] (L : E →L[𝕜] F) (hf : interval_integrable f μ a b) :
(x : ) in a..b, L (f x) μ = L ( (x : ) in a..b, f x μ)
@[simp]
theorem interval_integral.integral_comp_mul_right {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_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_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } (f : E) :
(x : ) in a..b, f (-x) = (x : ) in -b..-a, f x

Integral is an additive function of the interval #

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

theorem interval_integral.integral_congr {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {f g : E} {μ : measure_theory.measure } {a b : } (h : set.eq_on f g (set.uIcc 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 {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {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 {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {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_Ico {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {f : E} {μ : measure_theory.measure } {a : } {m n : } (hmn : m n) (hint : (k : ), k set.Ico m n interval_integrable f μ (a k) (a (k + 1))) :
(finset.Ico m n).sum (λ (k : ), (x : ) in a k..a (k + 1), f x μ) = (x : ) in a m..a n, f x μ
theorem interval_integral.sum_integral_adjacent_intervals {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {f : E} {μ : measure_theory.measure } {a : } {n : } (hint : (k : ), k < n interval_integrable f μ (a k) (a (k + 1))) :
(finset.range n).sum (λ (k : ), (x : ) in a k..a (k + 1), f x μ) = (x : ) in a 0..a n, f x μ
theorem interval_integral.integral_interval_sub_left {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {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 {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {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 {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {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' {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {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' {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } {f g : E} {μ : measure_theory.measure } (h : ∀ᵐ (x : ) μ, x set.Ioc a b f x = g x) (h' : ∀ᵐ (x : ) μ, x set.Ioc b a f x = g x) :
(x : ) in a..b, f x μ = (x : ) in a..b, g x μ
theorem interval_integral.integral_congr_ae {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } {f g : E} {μ : measure_theory.measure } (h : ∀ᵐ (x : ) μ, x set.uIoc a b f x = g x) :
(x : ) in a..b, f x μ = (x : ) in a..b, g x μ
theorem interval_integral.integral_zero_ae {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } {f : E} {μ : measure_theory.measure } (h : ∀ᵐ (x : ) μ, x set.uIoc a b f x = 0) :
(x : ) in a..b, f x μ = 0
theorem interval_integral.integral_indicator {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {f : E} {μ : measure_theory.measure } {a₁ a₂ a₃ : } (h : a₂ set.Icc a₁ a₃) :
(x : ) in a₁..a₃, {x : | x a₂}.indicator f x μ = (x : ) in a₁..a₂, f x μ
theorem interval_integral.tendsto_integral_filter_of_dominated_convergence {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } {f : E} {μ : measure_theory.measure } {ι : Type u_1} {l : filter ι} [l.is_countably_generated] {F : ι E} (bound : ) (hF_meas : ∀ᶠ (n : ι) in l, measure_theory.ae_strongly_measurable (F n) (μ.restrict (set.uIoc a b))) (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ) μ, x set.uIoc a b F n x bound x) (bound_integrable : interval_integrable bound μ a b) (h_lim : ∀ᵐ (x : ) μ, x set.uIoc a b filter.tendsto (λ (n : ι), F n x) l (nhds (f x))) :
filter.tendsto (λ (n : ι), (x : ) in a..b, F n x μ) l (nhds ( (x : ) in a..b, f x μ))

Lebesgue dominated convergence theorem for filters with a countable basis

theorem interval_integral.has_sum_integral_of_dominated_convergence {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } {f : E} {μ : measure_theory.measure } {ι : Type u_1} [countable ι] {F : ι E} (bound : ι ) (hF_meas : (n : ι), measure_theory.ae_strongly_measurable (F n) (μ.restrict (set.uIoc a b))) (h_bound : (n : ι), ∀ᵐ (t : ) μ, t set.uIoc a b F n t bound n t) (bound_summable : ∀ᵐ (t : ) μ, t set.uIoc a b summable (λ (n : ι), bound n t)) (bound_integrable : interval_integrable (λ (t : ), ∑' (n : ι), bound n t) μ a b) (h_lim : ∀ᵐ (t : ) μ, t set.uIoc a b has_sum (λ (n : ι), F n t) (f t)) :
has_sum (λ (n : ι), (t : ) in a..b, F n t μ) ( (t : ) in a..b, f t μ)

Lebesgue dominated convergence theorem for series.

theorem interval_integral.has_sum_interval_integral_of_summable_norm {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } [countable ι] {f : ι C(, E)} (hf_sum : summable (λ (i : ι), continuous_map.restrict {carrier := set.uIcc a b, is_compact' := _} (f i))) :
has_sum (λ (i : ι), (x : ) in a..b, (f i) x) ( (x : ) in a..b, ∑' (i : ι), (f i) x)

Interval integrals commute with countable sums, when the supremum norms are summable (a special case of the dominated convergence theorem).

theorem interval_integral.tsum_interval_integral_eq_of_summable_norm {ι : Type u_1} {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b : } [countable ι] {f : ι C(, E)} (hf_sum : summable (λ (i : ι), continuous_map.restrict {carrier := set.uIcc a b, is_compact' := _} (f i))) :
∑' (i : ι), (x : ) in a..b, (f i) x = (x : ) in a..b, ∑' (i : ι), (f i) x
theorem interval_integral.continuous_within_at_of_dominated_interval {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {μ : measure_theory.measure } {X : Type u_6} [topological_space X] [topological_space.first_countable_topology X] {F : X E} {x₀ : X} {bound : } {a b : } {s : set X} (hF_meas : ∀ᶠ (x : X) in nhds_within x₀ s, measure_theory.ae_strongly_measurable (F x) (μ.restrict (set.uIoc a b))) (h_bound : ∀ᶠ (x : X) in nhds_within x₀ s, ∀ᵐ (t : ) μ, t set.uIoc a b F x t bound t) (bound_integrable : interval_integrable bound μ a b) (h_cont : ∀ᵐ (t : ) μ, t set.uIoc 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 {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {μ : measure_theory.measure } {X : Type u_6} [topological_space X] [topological_space.first_countable_topology X] {F : X E} {x₀ : X} {bound : } {a b : } (hF_meas : ∀ᶠ (x : X) in nhds x₀, measure_theory.ae_strongly_measurable (F x) (μ.restrict (set.uIoc a b))) (h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ) μ, t set.uIoc a b F x t bound t) (bound_integrable : interval_integrable bound μ a b) (h_cont : ∀ᵐ (t : ) μ, t set.uIoc 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 {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {μ : measure_theory.measure } {X : Type u_6} [topological_space X] [topological_space.first_countable_topology X] {F : X E} {bound : } {a b : } (hF_meas : (x : X), measure_theory.ae_strongly_measurable (F x) (μ.restrict (set.uIoc a b))) (h_bound : (x : X), ∀ᵐ (t : ) μ, t set.uIoc a b F x t bound t) (bound_integrable : interval_integrable bound μ a b) (h_cont : ∀ᵐ (t : ) μ, t set.uIoc 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 {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b₀ b₁ b₂ : } {μ : measure_theory.measure } {f : E} (hb₀ : μ {b₀} = 0) (h_int : interval_integrable f μ (linear_order.min a b₁) (linear_order.max a b₂)) :
continuous_within_at (λ (b : ), (x : ) in a..b, f x μ) (set.Icc b₁ b₂) b₀
theorem interval_integral.continuous_on_primitive_interval' {E : Type u_3} [normed_add_comm_group E] [complete_space E] [normed_space E] {a b₁ b₂ : } {μ : measure_theory.measure } {f : E} [measure_theory.has_no_atoms μ] (h_int : interval_integrable f μ b₁ b₂) (ha : a set.uIcc b₁ b₂) :
continuous_on (λ (b : ), (x : ) in a..b, f x μ) (set.uIcc b₁ b₂)

Note: this assumes that f is interval_integrable, in contrast to some other lemmas here.

theorem interval_integral.integral_eq_zero_iff_of_le_of_nonneg_ae {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 {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' {f : } {a b : } {μ : measure_theory.measure } (hf : 0 ≤ᵐ[μ.restrict (set.uIoc a b)] f) (hfi : interval_integrable f μ a b) :
0 < (x : ) in a..b, f x μ a < b 0 < μ (function.support f set.Ioc a b)

If f is nonnegative and integrable on the unordered interval set.uIoc a b, then its integral over a..b is positive if and only if a < b and the measure of function.support f ∩ set.Ioc a b is positive.

theorem interval_integral.integral_pos_iff_support_of_nonneg_ae {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)

If f is nonnegative a.e.-everywhere and it is integrable on the unordered interval set.uIoc a b, then its integral over a..b is positive if and only if a < b and the measure of function.support f ∩ set.Ioc a b is positive.

theorem interval_integral.interval_integral_pos_of_pos_on {f : } {a b : } (hfi : interval_integrable f measure_theory.measure_space.volume a b) (hpos : (x : ), x set.Ioo a b 0 < f x) (hab : a < b) :
0 < (x : ) in a..b, f x

If f : ℝ → ℝ is integrable on (a, b] for real numbers a < b, and positive on the interior of the interval, then its integral over a..b is strictly positive.

theorem interval_integral.interval_integral_pos_of_pos {f : } {a b : } (hfi : interval_integrable f measure_theory.measure_space.volume a b) (hpos : (x : ), 0 < f x) (hab : a < b) :
0 < (x : ) in a..b, f x

If f : ℝ → ℝ is strictly positive everywhere, and integrable on (a, b] for real numbers a < b, then its integral over a..b is strictly positive. (See interval_integral_pos_of_pos_on for a version only assuming positivity of f on (a, b) rather than everywhere.)

theorem interval_integral.integral_lt_integral_of_ae_le_of_measure_set_of_lt_ne_zero {f g : } {a b : } {μ : measure_theory.measure } (hab : a b) (hfi : interval_integrable f μ a b) (hgi : interval_integrable g μ a b) (hle : f ≤ᵐ[μ.restrict (set.Ioc a b)] g) (hlt : (μ.restrict (set.Ioc a b)) {x : | f x < g x} 0) :
(x : ) in a..b, f x μ < (x : ) in a..b, g x μ

If f and g are two functions that are interval integrable on a..b, a ≤ b, f x ≤ g x for a.e. x ∈ set.Ioc a b, and f x < g x on a subset of set.Ioc a b of nonzero measure, then ∫ x in a..b, f x ∂μ < ∫ x in a..b, g x ∂μ.

theorem interval_integral.integral_lt_integral_of_continuous_on_of_le_of_exists_lt {f g : } {a b : } (hab : a < b) (hfc : continuous_on f (set.Icc a b)) (hgc : continuous_on g (set.Icc a b)) (hle : (x : ), x set.Ioc a b f x g x) (hlt : (c : ) (H : c set.Icc a b), f c < g c) :
(x : ) in a..b, f x < (x : ) in a..b, g x

If f and g are continuous on [a, b], a < b, f x ≤ g x on this interval, and f c < g c at some point c ∈ [a, b], then ∫ x in a..b, f x < ∫ x in a..b, g x.

theorem interval_integral.integral_nonneg_of_ae_restrict {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 {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 {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 {f : } {a b : } {μ : measure_theory.measure } (hab : a b) (hf : (u : ), u set.Icc a b 0 f u) :
0 (u : ) in a..b, f u μ
theorem interval_integral.abs_integral_le_integral_abs {f : } {a b : } {μ : measure_theory.measure } (hab : a b) :
| (x : ) in a..b, f x μ| (x : ) in a..b, |f x| μ
theorem interval_integral.integral_mono_ae_restrict {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 {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 {f g : } {a b : } {μ : measure_theory.measure } (hab : a b) (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b) (h : (x : ), x set.Icc a b f x g x) :
(u : ) in a..b, f u μ (u : ) in a..b, g u μ
theorem interval_integral.integral_mono {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_interval {f : } {a b : } {μ : measure_theory.measure } {c d : } (hca : c a) (hab : a b) (hbd : b d) (hf : 0 ≤ᵐ[μ.restrict (set.Ioc c d)] f) (hfi : interval_integrable f μ c d) :
(x : ) in a..b, f x μ (x : ) in c..d, f x μ
theorem interval_integral.abs_integral_mono_interval {f : } {a b : } {μ : measure_theory.measure } {c d : } (h : set.uIoc a b set.uIoc c d) (hf : 0 ≤ᵐ[μ.restrict (set.uIoc c d)] f) (hfi : interval_integrable f μ c d) :
| (x : ) in a..b, f x μ| | (x : ) in c..d, f x μ|