Links between an integral and its "improper" version #
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 aae_cover μ l
, wherel
is a countably generated filter, and iff
is a measurableennreal
-valued function, then∫⁻ x in φ n, f x ∂μ
tends to∫⁻ x, f x ∂μ
asn
tends tol
measure_theory.ae_cover.integrable_of_integral_norm_tendsto
: ifφ
is aae_cover μ l
, wherel
is a countably generated filter, iff
is measurable and integrable on eachφ n
, and if∫ x in φ n, ‖f x‖ ∂μ
tends to someI : ℝ
as n tends tol
, thenf
is integrablemeasure_theory.ae_cover.integral_tendsto_of_countably_generated
: ifφ
is aae_cover μ l
, wherel
is a countably generated filter, and iff
is measurable and integrable (globally), then∫ x in φ n, f x ∂μ
tends to∫ x, f x ∂μ
asn
tends to+∞
.
We then specialize these lemmas to various use cases involving intervals, which are frequent in analysis.
- ae_eventually_mem : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in l, x ∈ φ i
- measurable : ∀ (i : ι), measurable_set (φ i)
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
.
Slight reformulation of
measure_theory.ae_cover.integral_tendsto_of_countably_generated
.
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 (-∞, ∞)
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)
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, ∞)
Change-of-variables formula for Ioi
integrals of vector-valued functions, proved by taking
limits from the result for finite intervals.
Change-of-variables formula for Ioi
integrals of scalar-valued functions