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