mathlib3documentation

measure_theory.integral.integral_eq_improper

Links between an integral and its "improper" version #

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

In its current state, mathlib only knows how to talk about definite ("proper") integrals, in the sense that it treats integrals over `[x, +∞)` the same as it treats integrals over `[y, z]`. For example, the integral over `[1, +∞)` is not defined to be the limit of the integral over `[1, x]` as `x` tends to `+∞`, which is known as an improper integral.

Indeed, the "proper" definition is stronger than the "improper" one. The usual counterexample is `x ↦ sin(x)/x`, which has an improper integral over `[1, +∞)` but no definite integral.

Although definite integrals have better properties, they are hardly usable when it comes to computing integrals on unbounded sets, which is much easier using limits. Thus, in this file, we prove various ways of studying the proper integral by studying the improper one.

Definitions #

The main definition of this file is `measure_theory.ae_cover`. It is a rather technical definition whose sole purpose is generalizing and factoring proofs. Given an index type `ι`, a countably generated filter `l` over `ι`, and an `ι`-indexed family `φ` of subsets of a measurable space `α` equipped with a measure `μ`, one should think of a hypothesis `hφ : ae_cover μ l φ` as a sufficient condition for being able to interpret `∫ x, f x ∂μ` (if it exists) as the limit of `∫ x in φ i, f x ∂μ` as `i` tends to `l`.

When using this definition with a measure restricted to a set `s`, which happens fairly often, one should not try too hard to use a `ae_cover` of subsets of `s`, as it often makes proofs more complicated than necessary. See for example the proof of `measure_theory.integrable_on_Iic_of_interval_integral_norm_tendsto` where we use `(λ x, Ioi x)` as an `ae_cover` w.r.t. `μ.restrict (Iic b)`, instead of using `(λ x, Ioc x b)`.

Main statements #

• `measure_theory.ae_cover.lintegral_tendsto_of_countably_generated` : if `φ` is a `ae_cover μ l`, where `l` is a countably generated filter, and if `f` is a measurable `ennreal`-valued function, then `∫⁻ x in φ n, f x ∂μ` tends to `∫⁻ x, f x ∂μ` as `n` tends to `l`
• `measure_theory.ae_cover.integrable_of_integral_norm_tendsto` : if `φ` is a `ae_cover μ l`, where `l` is a countably generated filter, if `f` is measurable and integrable on each `φ n`, and if `∫ x in φ n, ‖f x‖ ∂μ` tends to some `I : ℝ` as n tends to `l`, then `f` is integrable
• `measure_theory.ae_cover.integral_tendsto_of_countably_generated` : if `φ` is a `ae_cover μ l`, where `l` is a countably generated filter, and if `f` is measurable and integrable (globally), then `∫ x in φ n, f x ∂μ` tends to `∫ x, f x ∂μ` as `n` tends to `+∞`.

We then specialize these lemmas to various use cases involving intervals, which are frequent in analysis. In particular,

• `measure_theory.integral_Ioi_of_has_deriv_at_of_tendsto` is a version of FTC-2 on the interval `(a, +∞)`, giving the formula `∫ x in (a, +∞), g' x = l - g a` if `g'` is integrable and `g` tends to `l` at `+∞`.
• `measure_theory.integral_Ioi_of_has_deriv_at_of_nonneg` gives the same result assuming that `g'` is nonnegative instead of integrable. Its automatic integrability in this context is proved in `measure_theory.integrable_on_Ioi_deriv_of_nonneg`.
• `measure_theory.integral_comp_smul_deriv_Ioi` is a version of the change of variables formula on semi-infinite intervals.
structure measure_theory.ae_cover {α : Type u_1} {ι : Type u_2} (μ : measure_theory.measure α) (l : filter ι) (φ : ι set α) :
Prop

A sequence `φ` of subsets of `α` is a `ae_cover` w.r.t. a measure `μ` and a filter `l` if almost every point (w.r.t. `μ`) of `α` eventually belongs to `φ n` (w.r.t. `l`), and if each `φ n` is measurable. This definition is a technical way to avoid duplicating a lot of proofs. It should be thought of as a sufficient condition for being able to interpret `∫ x, f x ∂μ` (if it exists) as the limit of `∫ x in φ n, f x ∂μ` as `n` tends to `l`.

See for example `measure_theory.ae_cover.lintegral_tendsto_of_countably_generated`, `measure_theory.ae_cover.integrable_of_integral_norm_tendsto` and `measure_theory.ae_cover.integral_tendsto_of_countably_generated`.

theorem measure_theory.ae_cover_Icc {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [preorder α] {a b : ι α} (ha : filter.at_bot) (hb : filter.at_top) :
(λ (i : ι), set.Icc (a i) (b i))
theorem measure_theory.ae_cover_Ici {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [preorder α] {a : ι α} (ha : filter.at_bot) :
(λ (i : ι), set.Ici (a i))
theorem measure_theory.ae_cover_Iic {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [preorder α] {b : ι α} (hb : filter.at_top) :
(λ (i : ι), set.Iic (b i))
theorem measure_theory.ae_cover_Ioo {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} (ha : filter.at_bot) (hb : filter.at_top) [no_min_order α] [no_max_order α] :
(λ (i : ι), set.Ioo (a i) (b i))
theorem measure_theory.ae_cover_Ioc {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} (ha : filter.at_bot) (hb : filter.at_top) [no_min_order α] :
(λ (i : ι), set.Ioc (a i) (b i))
theorem measure_theory.ae_cover_Ico {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} (ha : filter.at_bot) (hb : filter.at_top) [no_max_order α] :
(λ (i : ι), set.Ico (a i) (b i))
theorem measure_theory.ae_cover_Ioi {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a : ι α} (ha : filter.at_bot) [no_min_order α] :
(λ (i : ι), set.Ioi (a i))
theorem measure_theory.ae_cover_Iio {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {b : ι α} (hb : filter.at_top) [no_max_order α] :
(λ (i : ι), set.Iio (b i))
theorem measure_theory.ae_cover_Ioo_of_Icc {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Ioo A B)) l (λ (i : ι), set.Icc (a i) (b i))
theorem measure_theory.ae_cover_Ioo_of_Ico {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Ioo A B)) l (λ (i : ι), set.Ico (a i) (b i))
theorem measure_theory.ae_cover_Ioo_of_Ioc {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Ioo A B)) l (λ (i : ι), set.Ioc (a i) (b i))
theorem measure_theory.ae_cover_Ioo_of_Ioo {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Ioo A B)) l (λ (i : ι), set.Ioo (a i) (b i))
theorem measure_theory.ae_cover_Ioc_of_Icc {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Ioc A B)) l (λ (i : ι), set.Icc (a i) (b i))
theorem measure_theory.ae_cover_Ioc_of_Ico {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Ioc A B)) l (λ (i : ι), set.Ico (a i) (b i))
theorem measure_theory.ae_cover_Ioc_of_Ioc {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Ioc A B)) l (λ (i : ι), set.Ioc (a i) (b i))
theorem measure_theory.ae_cover_Ioc_of_Ioo {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Ioc A B)) l (λ (i : ι), set.Ioo (a i) (b i))
theorem measure_theory.ae_cover_Ico_of_Icc {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Ico A B)) l (λ (i : ι), set.Icc (a i) (b i))
theorem measure_theory.ae_cover_Ico_of_Ico {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Ico A B)) l (λ (i : ι), set.Ico (a i) (b i))
theorem measure_theory.ae_cover_Ico_of_Ioc {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Ico A B)) l (λ (i : ι), set.Ioc (a i) (b i))
theorem measure_theory.ae_cover_Ico_of_Ioo {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Ico A B)) l (λ (i : ι), set.Ioo (a i) (b i))
theorem measure_theory.ae_cover_Icc_of_Icc {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Icc A B)) l (λ (i : ι), set.Icc (a i) (b i))
theorem measure_theory.ae_cover_Icc_of_Ico {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Icc A B)) l (λ (i : ι), set.Ico (a i) (b i))
theorem measure_theory.ae_cover_Icc_of_Ioc {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Icc A B)) l (λ (i : ι), set.Ioc (a i) (b i))
theorem measure_theory.ae_cover_Icc_of_Ioo {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [linear_order α] {a b : ι α} {A B : α} (ha : (nhds A)) (hb : (nhds B)) :
measure_theory.ae_cover (μ.restrict (set.Icc A B)) l (λ (i : ι), set.Ioo (a i) (b i))
theorem measure_theory.ae_cover.restrict {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} {φ : ι set α} (hφ : φ) {s : set α} :
l φ
theorem measure_theory.ae_cover_restrict_of_ae_imp {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} {s : set α} {φ : ι set α} (hs : measurable_set s) (ae_eventually_mem : ∀ᵐ (x : α) μ, x s (∀ᶠ (n : ι) in l, x φ n)) (measurable : (n : ι), measurable_set (φ n)) :
l φ
theorem measure_theory.ae_cover.inter_restrict {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} {φ : ι set α} (hφ : φ) {s : set α} (hs : measurable_set s) :
l (λ (i : ι), φ i s)
theorem measure_theory.ae_cover.ae_tendsto_indicator {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} {β : Type u_3} [has_zero β] (f : α β) {φ : ι set α} (hφ : φ) :
∀ᵐ (x : α) μ, filter.tendsto (λ (i : ι), (φ i).indicator f x) l (nhds (f x))
theorem measure_theory.ae_cover.ae_measurable {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} {β : Type u_3} [l.ne_bot] {f : α β} {φ : ι set α} (hφ : φ) (hfm : (i : ι), (μ.restrict (φ i))) :
theorem measure_theory.ae_cover.ae_strongly_measurable {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} {β : Type u_3} [l.ne_bot] {f : α β} {φ : ι set α} (hφ : φ) (hfm : (i : ι), (μ.restrict (φ i))) :
theorem measure_theory.ae_cover.comp_tendsto {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} {μ : measure_theory.measure α} {l : filter ι} {l' : filter ι'} {φ : ι set α} (hφ : φ) {u : ι' ι} (hu : l' l) :
u)
theorem measure_theory.ae_cover.bUnion_Iic_ae_cover {α : Type u_1} {ι : Type u_2} [countable ι] {μ : measure_theory.measure α} [preorder ι] {φ : ι set α} (hφ : φ) :
(λ (n : ι), (k : ι) (h : k set.Iic n), φ k)
theorem measure_theory.ae_cover.bInter_Ici_ae_cover {α : Type u_1} {ι : Type u_2} [countable ι] {μ : measure_theory.measure α} [nonempty ι] {φ : ι set α} (hφ : φ) :
(λ (n : ι), (k : ι) (h : k set.Ici n), φ k)
theorem measure_theory.ae_cover.lintegral_tendsto_of_nat {α : Type u_1} {μ : measure_theory.measure α} {φ : set α} (hφ : φ) {f : α ennreal} (hfm : μ) :
filter.tendsto (λ (i : ), ∫⁻ (x : α) in φ i, f x μ) filter.at_top (nhds (∫⁻ (x : α), f x μ))
theorem measure_theory.ae_cover.lintegral_tendsto_of_countably_generated {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} {φ : ι set α} (hφ : φ) {f : α ennreal} (hfm : μ) :
filter.tendsto (λ (i : ι), ∫⁻ (x : α) in φ i, f x μ) l (nhds (∫⁻ (x : α), f x μ))
theorem measure_theory.ae_cover.lintegral_eq_of_tendsto {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [l.ne_bot] {φ : ι set α} (hφ : φ) {f : α ennreal} (I : ennreal) (hfm : μ) (htendsto : filter.tendsto (λ (i : ι), ∫⁻ (x : α) in φ i, f x μ) l (nhds I)) :
∫⁻ (x : α), f x μ = I
theorem measure_theory.ae_cover.supr_lintegral_eq_of_countably_generated {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [nonempty ι] [l.ne_bot] {φ : ι set α} (hφ : φ) {f : α ennreal} (hfm : μ) :
( (i : ι), ∫⁻ (x : α) in φ i, f x μ) = ∫⁻ (x : α), f x μ
theorem measure_theory.ae_cover.integrable_of_lintegral_nnnorm_bounded {α : Type u_1} {ι : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} {l : filter ι} [l.ne_bot] {φ : ι set α} (hφ : φ) {f : α E} (I : ) (hfm : μ) (hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, f x‖₊ μ ) :
theorem measure_theory.ae_cover.integrable_of_lintegral_nnnorm_tendsto {α : Type u_1} {ι : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} {l : filter ι} [l.ne_bot] {φ : ι set α} (hφ : φ) {f : α E} (I : ) (hfm : μ) (htendsto : filter.tendsto (λ (i : ι), ∫⁻ (x : α) in φ i, f x‖₊ μ) l (nhds (ennreal.of_real I))) :
theorem measure_theory.ae_cover.integrable_of_lintegral_nnnorm_bounded' {α : Type u_1} {ι : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} {l : filter ι} [l.ne_bot] {φ : ι set α} (hφ : φ) {f : α E} (I : nnreal) (hfm : μ) (hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, f x‖₊ μ I) :
theorem measure_theory.ae_cover.integrable_of_lintegral_nnnorm_tendsto' {α : Type u_1} {ι : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} {l : filter ι} [l.ne_bot] {φ : ι set α} (hφ : φ) {f : α E} (I : nnreal) (hfm : μ) (htendsto : filter.tendsto (λ (i : ι), ∫⁻ (x : α) in φ i, f x‖₊ μ) l (nhds I)) :
theorem measure_theory.ae_cover.integrable_of_integral_norm_bounded {α : Type u_1} {ι : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} {l : filter ι} [l.ne_bot] {φ : ι set α} (hφ : φ) {f : α E} (I : ) (hfi : (i : ι), (φ i) μ) (hbounded : ∀ᶠ (i : ι) in l, (x : α) in φ i, f x μ I) :
theorem measure_theory.ae_cover.integrable_of_integral_norm_tendsto {α : Type u_1} {ι : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} {l : filter ι} [l.ne_bot] {φ : ι set α} (hφ : φ) {f : α E} (I : ) (hfi : (i : ι), (φ i) μ) (htendsto : filter.tendsto (λ (i : ι), (x : α) in φ i, f x μ) l (nhds I)) :
theorem measure_theory.ae_cover.integrable_of_integral_bounded_of_nonneg_ae {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [l.ne_bot] {φ : ι set α} (hφ : φ) {f : α } (I : ) (hfi : (i : ι), (φ i) μ) (hnng : ∀ᵐ (x : α) μ, 0 f x) (hbounded : ∀ᶠ (i : ι) in l, (x : α) in φ i, f x μ I) :
theorem measure_theory.ae_cover.integrable_of_integral_tendsto_of_nonneg_ae {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [l.ne_bot] {φ : ι set α} (hφ : φ) {f : α } (I : ) (hfi : (i : ι), (φ i) μ) (hnng : ∀ᵐ (x : α) μ, 0 f x) (htendsto : filter.tendsto (λ (i : ι), (x : α) in φ i, f x μ) l (nhds I)) :
theorem measure_theory.ae_cover.integral_tendsto_of_countably_generated {α : Type u_1} {ι : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} {l : filter ι} [ E] {φ : ι set α} (hφ : φ) {f : α E} (hfi : μ) :
filter.tendsto (λ (i : ι), (x : α) in φ i, f x μ) l (nhds ( (x : α), f x μ))
theorem measure_theory.ae_cover.integral_eq_of_tendsto {α : Type u_1} {ι : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} {l : filter ι} [ E] [l.ne_bot] {φ : ι set α} (hφ : φ) {f : α E} (I : E) (hfi : μ) (h : filter.tendsto (λ (n : ι), (x : α) in φ n, f x μ) l (nhds I)) :
(x : α), f x μ = I

Slight reformulation of `measure_theory.ae_cover.integral_tendsto_of_countably_generated`.

theorem measure_theory.ae_cover.integral_eq_of_tendsto_of_nonneg_ae {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {l : filter ι} [l.ne_bot] {φ : ι set α} (hφ : φ) {f : α } (I : ) (hnng : 0 ≤ᵐ[μ] f) (hfi : (n : ι), (φ n) μ) (htendsto : filter.tendsto (λ (n : ι), (x : α) in φ n, f x μ) l (nhds I)) :
(x : α), f x μ = I
theorem measure_theory.integrable_of_interval_integral_norm_bounded {ι : Type u_1} {E : Type u_2} {l : filter ι} [l.ne_bot] {a b : ι } {f : E} (I : ) (hfi : (i : ι), (set.Ioc (a i) (b i)) μ) (ha : filter.at_bot) (hb : filter.at_top) (h : ∀ᶠ (i : ι) in l, (x : ) in a i..b i, f x μ I) :
theorem measure_theory.integrable_of_interval_integral_norm_tendsto {ι : Type u_1} {E : Type u_2} {l : filter ι} [l.ne_bot] {a b : ι } {f : E} (I : ) (hfi : (i : ι), (set.Ioc (a i) (b i)) μ) (ha : filter.at_bot) (hb : filter.at_top) (h : filter.tendsto (λ (i : ι), (x : ) in a i..b i, f x μ) l (nhds I)) :

If `f` is integrable on intervals `Ioc (a i) (b i)`, where `a i` tends to -∞ and `b i` tends to ∞, and `∫ x in a i .. b i, ‖f x‖ ∂μ` converges to `I : ℝ` along a filter `l`, then `f` is integrable on the interval (-∞, ∞)

theorem measure_theory.integrable_on_Iic_of_interval_integral_norm_bounded {ι : Type u_1} {E : Type u_2} {l : filter ι} [l.ne_bot] {a : ι } {f : E} (I b : ) (hfi : (i : ι), (set.Ioc (a i) b) μ) (ha : filter.at_bot) (h : ∀ᶠ (i : ι) in l, (x : ) in a i..b, f x μ I) :
theorem measure_theory.integrable_on_Iic_of_interval_integral_norm_tendsto {ι : Type u_1} {E : Type u_2} {l : filter ι} [l.ne_bot] {a : ι } {f : E} (I b : ) (hfi : (i : ι), (set.Ioc (a i) b) μ) (ha : filter.at_bot) (h : filter.tendsto (λ (i : ι), (x : ) in a i..b, f x μ) l (nhds I)) :

If `f` is integrable on intervals `Ioc (a i) b`, where `a i` tends to -∞, and `∫ x in a i .. b, ‖f x‖ ∂μ` converges to `I : ℝ` along a filter `l`, then `f` is integrable on the interval (-∞, b)

theorem measure_theory.integrable_on_Ioi_of_interval_integral_norm_bounded {ι : Type u_1} {E : Type u_2} {l : filter ι} [l.ne_bot] {b : ι } {f : E} (I a : ) (hfi : (i : ι), (set.Ioc a (b i)) μ) (hb : filter.at_top) (h : ∀ᶠ (i : ι) in l, (x : ) in a..b i, f x μ I) :
theorem measure_theory.integrable_on_Ioi_of_interval_integral_norm_tendsto {ι : Type u_1} {E : Type u_2} {l : filter ι} [l.ne_bot] {b : ι } {f : E} (I a : ) (hfi : (i : ι), (set.Ioc a (b i)) μ) (hb : filter.at_top) (h : filter.tendsto (λ (i : ι), (x : ) in a..b i, f x μ) l (nhds I)) :

If `f` is integrable on intervals `Ioc a (b i)`, where `b i` tends to ∞, and `∫ x in a .. b i, ‖f x‖ ∂μ` converges to `I : ℝ` along a filter `l`, then `f` is integrable on the interval (a, ∞)

theorem measure_theory.integrable_on_Ioc_of_interval_integral_norm_bounded {ι : Type u_1} {E : Type u_2} {l : filter ι} [l.ne_bot] {a b : ι } {f : E} {I a₀ b₀ : } (hfi : (i : ι), ) (ha : (nhds a₀)) (hb : (nhds b₀)) (h : ∀ᶠ (i : ι) in l, (x : ) in set.Ioc (a i) (b i), f x I) :
theorem measure_theory.integrable_on_Ioc_of_interval_integral_norm_bounded_left {ι : Type u_1} {E : Type u_2} {l : filter ι} [l.ne_bot] {a : ι } {f : E} {I a₀ b : } (hfi : (i : ι), ) (ha : (nhds a₀)) (h : ∀ᶠ (i : ι) in l, (x : ) in set.Ioc (a i) b, f x I) :
theorem measure_theory.integrable_on_Ioc_of_interval_integral_norm_bounded_right {ι : Type u_1} {E : Type u_2} {l : filter ι} [l.ne_bot] {b : ι } {f : E} {I a b₀ : } (hfi : (i : ι), ) (hb : (nhds b₀)) (h : ∀ᶠ (i : ι) in l, (x : ) in (b i), f x I) :
theorem measure_theory.interval_integral_tendsto_integral {ι : Type u_1} {E : Type u_2} {l : filter ι} [ E] {a b : ι } {f : E} (hfi : μ) (ha : filter.at_bot) (hb : filter.at_top) :
filter.tendsto (λ (i : ι), (x : ) in a i..b i, f x μ) l (nhds ( (x : ), f x μ))
theorem measure_theory.interval_integral_tendsto_integral_Iic {ι : Type u_1} {E : Type u_2} {l : filter ι} [ E] {a : ι } {f : E} (b : ) (hfi : μ) (ha : filter.at_bot) :
filter.tendsto (λ (i : ι), (x : ) in a i..b, f x μ) l (nhds ( (x : ) in , f x μ))
theorem measure_theory.interval_integral_tendsto_integral_Ioi {ι : Type u_1} {E : Type u_2} {l : filter ι} [ E] {b : ι } {f : E} (a : ) (hfi : μ) (hb : filter.at_top) :
filter.tendsto (λ (i : ι), (x : ) in a..b i, f x μ) l (nhds ( (x : ) in , f x μ))
theorem measure_theory.integral_Ioi_of_has_deriv_at_of_tendsto {E : Type u_1} {f f' : E} {a : } {m : E} [ E] (hcont : (set.Ici a)) (hderiv : (x : ), x (f' x) x) (hf : (nhds m)) :
(x : ) in , f' x = m - f a

Fundamental theorem of calculus-2, on semi-infinite intervals `(a, +∞)`. When a function has a limit at infinity `m`, and its derivative is integrable, then the integral of the derivative on `(a, +∞)` is `m - f a`. Version assuming differentiability on `(a, +∞)` and continuity on `[a, +∞)`.

theorem measure_theory.integral_Ioi_of_has_deriv_at_of_tendsto' {E : Type u_1} {f f' : E} {a : } {m : E} [ E] (hderiv : (x : ), x (f' x) x) (hf : (nhds m)) :
(x : ) in , f' x = m - f a

Fundamental theorem of calculus-2, on semi-infinite intervals `(a, +∞)`. When a function has a limit at infinity `m`, and its derivative is integrable, then the integral of the derivative on `(a, +∞)` is `m - f a`. Version assuming differentiability on `[a, +∞)`.

theorem measure_theory.integrable_on_Ioi_deriv_of_nonneg {g g' : } {a l : } (hcont : (set.Ici a)) (hderiv : (x : ), x (g' x) x) (g'pos : (x : ), x 0 g' x) (hg : (nhds l)) :

When a function has a limit at infinity, and its derivative is nonnegative, then the derivative is automatically integrable on `(a, +∞)`. Version assuming differentiability on `(a, +∞)` and continuity on `[a, +∞)`.

theorem measure_theory.integrable_on_Ioi_deriv_of_nonneg' {g g' : } {a l : } (hderiv : (x : ), x (g' x) x) (g'pos : (x : ), x 0 g' x) (hg : (nhds l)) :

When a function has a limit at infinity, and its derivative is nonnegative, then the derivative is automatically integrable on `(a, +∞)`. Version assuming differentiability on `[a, +∞)`.

theorem measure_theory.integral_Ioi_of_has_deriv_at_of_nonneg {g g' : } {a l : } (hcont : (set.Ici a)) (hderiv : (x : ), x (g' x) x) (g'pos : (x : ), x 0 g' x) (hg : (nhds l)) :
(x : ) in , g' x = l - g a

When a function has a limit at infinity `l`, and its derivative is nonnegative, then the integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see `integrable_on_Ioi_deriv_of_nonneg`). Version assuming differentiability on `(a, +∞)` and continuity on `[a, +∞)`.

theorem measure_theory.integral_Ioi_of_has_deriv_at_of_nonneg' {g g' : } {a l : } (hderiv : (x : ), x (g' x) x) (g'pos : (x : ), x 0 g' x) (hg : (nhds l)) :
(x : ) in , g' x = l - g a

When a function has a limit at infinity `l`, and its derivative is nonnegative, then the integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see `integrable_on_Ioi_deriv_of_nonneg'`). Version assuming differentiability on `[a, +∞)`.

theorem measure_theory.integrable_on_Ioi_deriv_of_nonpos {g g' : } {a l : } (hcont : (set.Ici a)) (hderiv : (x : ), x (g' x) x) (g'neg : (x : ), x g' x 0) (hg : (nhds l)) :

When a function has a limit at infinity, and its derivative is nonpositive, then the derivative is automatically integrable on `(a, +∞)`. Version assuming differentiability on `(a, +∞)` and continuity on `[a, +∞)`.

theorem measure_theory.integrable_on_Ioi_deriv_of_nonpos' {g g' : } {a l : } (hderiv : (x : ), x (g' x) x) (g'neg : (x : ), x g' x 0) (hg : (nhds l)) :

When a function has a limit at infinity, and its derivative is nonpositive, then the derivative is automatically integrable on `(a, +∞)`. Version assuming differentiability on `[a, +∞)`.

theorem measure_theory.integral_Ioi_of_has_deriv_at_of_nonpos {g g' : } {a l : } (hcont : (set.Ici a)) (hderiv : (x : ), x (g' x) x) (g'neg : (x : ), x g' x 0) (hg : (nhds l)) :
(x : ) in , g' x = l - g a

When a function has a limit at infinity `l`, and its derivative is nonpositive, then the integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see `integrable_on_Ioi_deriv_of_nonneg`). Version assuming differentiability on `(a, +∞)` and continuity on `[a, +∞)`.

theorem measure_theory.integral_Ioi_of_has_deriv_at_of_nonpos' {g g' : } {a l : } (hderiv : (x : ), x (g' x) x) (g'neg : (x : ), x g' x 0) (hg : (nhds l)) :
(x : ) in , g' x = l - g a

When a function has a limit at infinity `l`, and its derivative is nonpositive, then the integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see `integrable_on_Ioi_deriv_of_nonneg'`). Version assuming differentiability on `[a, +∞)`.

theorem measure_theory.integral_comp_smul_deriv_Ioi {E : Type u_1} [ E] {f f' : } {g : E} {a : } (hf : (set.Ici a)) (hft : filter.at_top) (hff' : (x : ), x (f' x) (set.Ioi x) x) (hg_cont : (f '' set.Ioi a)) (hg2 : measure_theory.integrable_on (λ (x : ), f' x (g f) x) (set.Ici a) measure_theory.measure_space.volume) :
(x : ) in , f' x (g f) x = (u : ) in set.Ioi (f a), g u

Change-of-variables formula for `Ioi` integrals of vector-valued functions, proved by taking limits from the result for finite intervals.

theorem measure_theory.integral_comp_mul_deriv_Ioi {f f' g : } {a : } (hf : (set.Ici a)) (hft : filter.at_top) (hff' : (x : ), x (f' x) (set.Ioi x) x) (hg_cont : (f '' set.Ioi a)) (hg2 : measure_theory.integrable_on (λ (x : ), (g f) x * f' x) (set.Ici a) measure_theory.measure_space.volume) :
(x : ) in , (g f) x * f' x = (u : ) in set.Ioi (f a), g u

Change-of-variables formula for `Ioi` integrals of scalar-valued functions

theorem measure_theory.integral_comp_rpow_Ioi {E : Type u_1} [ E] (g : E) {p : } (hp : p 0) :
(x : ) in , (|p| * x ^ (p - 1)) g (x ^ p) = (y : ) in , g y

Substitution `y = x ^ p` in integrals over `Ioi 0`

theorem measure_theory.integral_comp_rpow_Ioi_of_pos {E : Type u_1} [ E] {g : E} {p : } (hp : 0 < p) :
(x : ) in , (p * x ^ (p - 1)) g (x ^ p) = (y : ) in , g y
theorem measure_theory.integral_comp_mul_left_Ioi {E : Type u_1} [ E] (g : E) (a : ) {b : } (hb : 0 < b) :
(x : ) in , g (b * x) = |b⁻¹| (x : ) in set.Ioi (b * a), g x
theorem measure_theory.integral_comp_mul_right_Ioi {E : Type u_1} [ E] (g : E) (a : ) {b : } (hb : 0 < b) :
(x : ) in , g (x * b) = |b⁻¹| (x : ) in set.Ioi (a * b), g x
theorem measure_theory.integrable_on_Ioi_comp_rpow_iff {E : Type u_1} [ E] (f : E) {p : } (hp : p 0) :

The substitution `y = x ^ p` in integrals over `Ioi 0` preserves integrability.

theorem measure_theory.integrable_on_Ioi_comp_rpow_iff' {E : Type u_1} [ E] (f : E) {p : } (hp : p 0) :

The substitution `y = x ^ p` in integrals over `Ioi 0` preserves integrability (version without `|p|` factor)