# 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 MeasureTheory.AECover. 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φ : MeasureTheory.AECover μ 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 MeasureTheory.AECover of subsets of s, as it often makes proofs more complicated than necessary. See for example the proof of MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_tendsto where we use (fun x ↦ oi x) as a MeasureTheory.AECover w.r.t. μ.restrict (Iic b), instead of using (fun x ↦ Ioc x b).

## Main statements #

• MeasureTheory.AECover.lintegral_tendsto_of_countably_generated : if φ is a MeasureTheory.AECover μ 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

• MeasureTheory.AECover.integrable_of_integral_norm_tendsto : if φ is a MeasureTheory.AECover μ 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

• MeasureTheory.AECover.integral_tendsto_of_countably_generated : if φ is a MeasureTheory.AECover μ 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,

• MeasureTheory.integral_Ioi_of_hasDerivAt_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 +∞.
• MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg gives the same result assuming that g' is nonnegative instead of integrable. Its automatic integrability in this context is proved in MeasureTheory.integrableOn_Ioi_deriv_of_nonneg.
• MeasureTheory.integral_comp_smul_deriv_Ioi is a version of the change of variables formula on semi-infinite intervals.
• MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi shows that a function whose derivative is integrable on (a, +∞) has a limit at +∞.
• MeasureTheory.tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi shows that an integrable function whose derivative is integrable on (a, +∞) tends to 0 at +∞.

Versions of these results are also given on the intervals (-∞, a] and (-∞, +∞), as well as the corresponding versions of integration by parts.

structure MeasureTheory.AECover {α : Type u_1} {ι : Type u_2} [] (μ : ) (l : ) (φ : ιSet α) :

A sequence φ of subsets of α is a MeasureTheory.AECover 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 MeasureTheory.AECover.lintegral_tendsto_of_countably_generated, MeasureTheory.AECover.integrable_of_integral_norm_tendsto and MeasureTheory.AECover.integral_tendsto_of_countably_generated.

• ae_eventually_mem : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in l, x φ i
• measurableSet : ∀ (i : ι), MeasurableSet (φ i)
Instances For
theorem MeasureTheory.AECover.ae_eventually_mem {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {φ : ιSet α} (self : ) :
∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in l, x φ i
theorem MeasureTheory.AECover.measurableSet {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {φ : ιSet α} (self : ) (i : ι) :

## Operations on AECovers #

Porting note: this is a new section.

theorem MeasureTheory.AECover.inter {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {φ : ιSet α} {ψ : ιSet α} (hφ : ) (hψ : ) :
MeasureTheory.AECover μ l fun (i : ι) => φ i ψ i

Elementwise intersection of two AECovers is an AECover.

theorem MeasureTheory.AECover.superset {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {φ : ιSet α} {ψ : ιSet α} (hφ : ) (hsub : ∀ (i : ι), φ i ψ i) (hmeas : ∀ (i : ι), MeasurableSet (ψ i)) :
theorem MeasureTheory.AECover.mono_ac {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {ν : } {φ : ιSet α} (hφ : ) (hle : ν.AbsolutelyContinuous μ) :
theorem MeasureTheory.AECover.mono {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {ν : } {φ : ιSet α} (hφ : ) (hle : ν μ) :
theorem MeasureTheory.aecover_ball {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {x : α} {r : ι} (hr : Filter.Tendsto r l Filter.atTop) :
MeasureTheory.AECover μ l fun (i : ι) => Metric.ball x (r i)
theorem MeasureTheory.aecover_closedBall {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {x : α} {r : ι} (hr : Filter.Tendsto r l Filter.atTop) :
MeasureTheory.AECover μ l fun (i : ι) => Metric.closedBall x (r i)
theorem MeasureTheory.aecover_Ici {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} (ha : Filter.Tendsto a l Filter.atBot) :
MeasureTheory.AECover μ l fun (i : ι) => Set.Ici (a i)
theorem MeasureTheory.aecover_Iic {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {b : ια} (hb : Filter.Tendsto b l Filter.atTop) :
MeasureTheory.AECover μ l fun (i : ι) => Set.Iic (b i)
theorem MeasureTheory.aecover_Icc {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} (ha : Filter.Tendsto a l Filter.atBot) (hb : Filter.Tendsto b l Filter.atTop) :
MeasureTheory.AECover μ l fun (i : ι) => Set.Icc (a i) (b i)
theorem MeasureTheory.aecover_Ioi {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} (ha : Filter.Tendsto a l Filter.atBot) [] :
MeasureTheory.AECover μ l fun (i : ι) => Set.Ioi (a i)
theorem MeasureTheory.aecover_Iio {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {b : ια} (hb : Filter.Tendsto b l Filter.atTop) [] :
MeasureTheory.AECover μ l fun (i : ι) => Set.Iio (b i)
theorem MeasureTheory.aecover_Ioo {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} (ha : Filter.Tendsto a l Filter.atBot) (hb : Filter.Tendsto b l Filter.atTop) [] [] :
MeasureTheory.AECover μ l fun (i : ι) => Set.Ioo (a i) (b i)
theorem MeasureTheory.aecover_Ioc {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} (ha : Filter.Tendsto a l Filter.atBot) (hb : Filter.Tendsto b l Filter.atTop) [] :
MeasureTheory.AECover μ l fun (i : ι) => Set.Ioc (a i) (b i)
theorem MeasureTheory.aecover_Ico {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} (ha : Filter.Tendsto a l Filter.atBot) (hb : Filter.Tendsto b l Filter.atTop) [] :
MeasureTheory.AECover μ l fun (i : ι) => Set.Ico (a i) (b i)
theorem MeasureTheory.aecover_Ioi_of_Ioi {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {A : α} (ha : Filter.Tendsto a l (nhds A)) :
MeasureTheory.AECover (μ.restrict ()) l fun (i : ι) => Set.Ioi (a i)
theorem MeasureTheory.aecover_Iio_of_Iio {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {b : ια} {B : α} (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict ()) l fun (i : ι) => Set.Iio (b i)
theorem MeasureTheory.aecover_Ioi_of_Ici {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {A : α} (ha : Filter.Tendsto a l (nhds A)) :
MeasureTheory.AECover (μ.restrict ()) l fun (i : ι) => Set.Ici (a i)
theorem MeasureTheory.aecover_Iio_of_Iic {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {b : ια} {B : α} (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict ()) l fun (i : ι) => Set.Iic (b i)
theorem MeasureTheory.aecover_Ioo_of_Ioo {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun (i : ι) => Set.Ioo (a i) (b i)
theorem MeasureTheory.aecover_Ioo_of_Icc {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun (i : ι) => Set.Icc (a i) (b i)
theorem MeasureTheory.aecover_Ioo_of_Ico {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun (i : ι) => Set.Ico (a i) (b i)
theorem MeasureTheory.aecover_Ioo_of_Ioc {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun (i : ι) => Set.Ioc (a i) (b i)
theorem MeasureTheory.aecover_Ioc_of_Icc {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Ioc A B)) l fun (i : ι) => Set.Icc (a i) (b i)
theorem MeasureTheory.aecover_Ioc_of_Ico {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Ioc A B)) l fun (i : ι) => Set.Ico (a i) (b i)
theorem MeasureTheory.aecover_Ioc_of_Ioc {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Ioc A B)) l fun (i : ι) => Set.Ioc (a i) (b i)
theorem MeasureTheory.aecover_Ioc_of_Ioo {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Ioc A B)) l fun (i : ι) => Set.Ioo (a i) (b i)
theorem MeasureTheory.aecover_Ico_of_Icc {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Ico A B)) l fun (i : ι) => Set.Icc (a i) (b i)
theorem MeasureTheory.aecover_Ico_of_Ico {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Ico A B)) l fun (i : ι) => Set.Ico (a i) (b i)
theorem MeasureTheory.aecover_Ico_of_Ioc {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Ico A B)) l fun (i : ι) => Set.Ioc (a i) (b i)
theorem MeasureTheory.aecover_Ico_of_Ioo {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Ico A B)) l fun (i : ι) => Set.Ioo (a i) (b i)
theorem MeasureTheory.aecover_Icc_of_Icc {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Icc A B)) l fun (i : ι) => Set.Icc (a i) (b i)
theorem MeasureTheory.aecover_Icc_of_Ico {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Icc A B)) l fun (i : ι) => Set.Ico (a i) (b i)
theorem MeasureTheory.aecover_Icc_of_Ioc {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Icc A B)) l fun (i : ι) => Set.Ioc (a i) (b i)
theorem MeasureTheory.aecover_Icc_of_Ioo {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [] {a : ια} {b : ια} {A : α} {B : α} (ha : Filter.Tendsto a l (nhds A)) (hb : Filter.Tendsto b l (nhds B)) :
MeasureTheory.AECover (μ.restrict (Set.Icc A B)) l fun (i : ι) => Set.Ioo (a i) (b i)
theorem MeasureTheory.AECover.restrict {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {φ : ιSet α} (hφ : ) {s : Set α} :
MeasureTheory.AECover (μ.restrict s) l φ
theorem MeasureTheory.aecover_restrict_of_ae_imp {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {s : Set α} {φ : ιSet α} (hs : ) (ae_eventually_mem : ∀ᵐ (x : α) ∂μ, x s∀ᶠ (n : ι) in l, x φ n) (measurable : ∀ (n : ι), MeasurableSet (φ n)) :
MeasureTheory.AECover (μ.restrict s) l φ
theorem MeasureTheory.AECover.inter_restrict {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {φ : ιSet α} (hφ : ) {s : Set α} (hs : ) :
MeasureTheory.AECover (μ.restrict s) l fun (i : ι) => φ i s
theorem MeasureTheory.AECover.ae_tendsto_indicator {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {β : Type u_3} [Zero β] [] (f : αβ) {φ : ιSet α} (hφ : ) :
∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (i : ι) => (φ i).indicator f x) l (nhds (f x))
theorem MeasureTheory.AECover.aemeasurable {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {β : Type u_3} [] [l.IsCountablyGenerated] [l.NeBot] {f : αβ} {φ : ιSet α} (hφ : ) (hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))) :
theorem MeasureTheory.AECover.aestronglyMeasurable {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } {β : Type u_3} [] [l.IsCountablyGenerated] [l.NeBot] {f : αβ} {φ : ιSet α} (hφ : ) (hfm : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ.restrict (φ i))) :
theorem MeasureTheory.AECover.comp_tendsto {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [] {μ : } {l : } {l' : Filter ι'} {φ : ιSet α} (hφ : ) {u : ι'ι} (hu : Filter.Tendsto u l' l) :
theorem MeasureTheory.AECover.biUnion_Iic_aecover {α : Type u_1} {ι : Type u_2} [] [] {μ : } [] {φ : ιSet α} (hφ : MeasureTheory.AECover μ Filter.atTop φ) :
MeasureTheory.AECover μ Filter.atTop fun (n : ι) => k, φ k
theorem MeasureTheory.AECover.biInter_Ici_aecover {α : Type u_1} {ι : Type u_2} [] [] {μ : } [] {φ : ιSet α} (hφ : MeasureTheory.AECover μ Filter.atTop φ) :
MeasureTheory.AECover μ Filter.atTop fun (n : ι) => k, φ k
theorem MeasureTheory.AECover.lintegral_tendsto_of_nat {α : Type u_1} [] {μ : } {φ : Set α} (hφ : MeasureTheory.AECover μ Filter.atTop φ) {f : αENNReal} (hfm : ) :
Filter.Tendsto (fun (x : ) => ∫⁻ (x : α) in φ x, f xμ) Filter.atTop (nhds (∫⁻ (x : α), f xμ))
theorem MeasureTheory.AECover.lintegral_tendsto_of_countably_generated {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : αENNReal} (hfm : ) :
Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α) in φ i, f xμ) l (nhds (∫⁻ (x : α), f xμ))
theorem MeasureTheory.AECover.lintegral_eq_of_tendsto {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : αENNReal} (I : ENNReal) (hfm : ) (htendsto : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α) in φ i, f xμ) l (nhds I)) :
∫⁻ (x : α), f xμ = I
theorem MeasureTheory.AECover.iSup_lintegral_eq_of_countably_generated {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [] [l.NeBot] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : αENNReal} (hfm : ) :
⨆ (i : ι), ∫⁻ (x : α) in φ i, f xμ = ∫⁻ (x : α), f xμ
theorem MeasureTheory.AECover.integrable_of_lintegral_nnnorm_bounded {α : Type u_1} {ι : Type u_2} {E : Type u_3} [] {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : αE} (I : ) (hfm : ) (hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, f x‖₊μ ) :
theorem MeasureTheory.AECover.integrable_of_lintegral_nnnorm_tendsto {α : Type u_1} {ι : Type u_2} {E : Type u_3} [] {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : αE} (I : ) (hfm : ) (htendsto : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α) in φ i, f x‖₊μ) l ()) :
theorem MeasureTheory.AECover.integrable_of_lintegral_nnnorm_bounded' {α : Type u_1} {ι : Type u_2} {E : Type u_3} [] {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : αE} (I : NNReal) (hfm : ) (hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, f x‖₊μ I) :
theorem MeasureTheory.AECover.integrable_of_lintegral_nnnorm_tendsto' {α : Type u_1} {ι : Type u_2} {E : Type u_3} [] {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : αE} (I : NNReal) (hfm : ) (htendsto : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α) in φ i, f x‖₊μ) l (nhds I)) :
theorem MeasureTheory.AECover.integrable_of_integral_norm_bounded {α : Type u_1} {ι : Type u_2} {E : Type u_3} [] {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : αE} (I : ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ) (hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, f xμ I) :
theorem MeasureTheory.AECover.integrable_of_integral_norm_tendsto {α : Type u_1} {ι : Type u_2} {E : Type u_3} [] {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : αE} (I : ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ) (htendsto : Filter.Tendsto (fun (i : ι) => ∫ (x : α) in φ i, f xμ) l (nhds I)) :
theorem MeasureTheory.AECover.integrable_of_integral_bounded_of_nonneg_ae {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : α} (I : ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ) (hnng : ∀ᵐ (x : α) ∂μ, 0 f x) (hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, f xμ I) :
theorem MeasureTheory.AECover.integrable_of_integral_tendsto_of_nonneg_ae {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : α} (I : ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ) (hnng : ∀ᵐ (x : α) ∂μ, 0 f x) (htendsto : Filter.Tendsto (fun (i : ι) => ∫ (x : α) in φ i, f xμ) l (nhds I)) :
theorem MeasureTheory.AECover.integral_tendsto_of_countably_generated {α : Type u_1} {ι : Type u_2} {E : Type u_3} [] {μ : } {l : } [] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : αE} (hfi : ) :
Filter.Tendsto (fun (i : ι) => ∫ (x : α) in φ i, f xμ) l (nhds (∫ (x : α), f xμ))
theorem MeasureTheory.AECover.integral_eq_of_tendsto {α : Type u_1} {ι : Type u_2} {E : Type u_3} [] {μ : } {l : } [] [l.NeBot] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : αE} (I : E) (hfi : ) (h : Filter.Tendsto (fun (n : ι) => ∫ (x : α) in φ n, f xμ) l (nhds I)) :
∫ (x : α), f xμ = I

Slight reformulation of MeasureTheory.AECover.integral_tendsto_of_countably_generated.

theorem MeasureTheory.AECover.integral_eq_of_tendsto_of_nonneg_ae {α : Type u_1} {ι : Type u_2} [] {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {φ : ιSet α} (hφ : ) {f : α} (I : ) (hnng : 0 ≤ᵐ[μ] f) (hfi : ∀ (n : ι), MeasureTheory.IntegrableOn f (φ n) μ) (htendsto : Filter.Tendsto (fun (n : ι) => ∫ (x : α) in φ n, f xμ) l (nhds I)) :
∫ (x : α), f xμ = I
theorem MeasureTheory.integrable_of_intervalIntegral_norm_bounded {ι : Type u_1} {E : Type u_2} {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {a : ι} {b : ι} {f : E} (I : ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) μ) (ha : Filter.Tendsto a l Filter.atBot) (hb : Filter.Tendsto b l Filter.atTop) (h : ∀ᶠ (i : ι) in l, ∫ (x : ) in a i..b i, f xμ I) :
theorem MeasureTheory.integrable_of_intervalIntegral_norm_tendsto {ι : Type u_1} {E : Type u_2} {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {a : ι} {b : ι} {f : E} (I : ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) μ) (ha : Filter.Tendsto a l Filter.atBot) (hb : Filter.Tendsto b l Filter.atTop) (h : Filter.Tendsto (fun (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 MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_bounded {ι : Type u_1} {E : Type u_2} {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {a : ι} {f : E} (I : ) (b : ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) μ) (ha : Filter.Tendsto a l Filter.atBot) (h : ∀ᶠ (i : ι) in l, ∫ (x : ) in a i..b, f xμ I) :
theorem MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_tendsto {ι : Type u_1} {E : Type u_2} {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {a : ι} {f : E} (I : ) (b : ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) μ) (ha : Filter.Tendsto a l Filter.atBot) (h : Filter.Tendsto (fun (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 MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_bounded {ι : Type u_1} {E : Type u_2} {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {b : ι} {f : E} (I : ) (a : ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) μ) (hb : Filter.Tendsto b l Filter.atTop) (h : ∀ᶠ (i : ι) in l, ∫ (x : ) in a..b i, f xμ I) :
theorem MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_tendsto {ι : Type u_1} {E : Type u_2} {μ : } {l : } [l.NeBot] [l.IsCountablyGenerated] {b : ι} {f : E} (I : ) (a : ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) μ) (hb : Filter.Tendsto b l Filter.atTop) (h : Filter.Tendsto (fun (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 MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded {ι : Type u_1} {E : Type u_2} {l : } [l.NeBot] [l.IsCountablyGenerated] {a : ι} {b : ι} {f : E} {I : } {a₀ : } {b₀ : } (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) MeasureTheory.volume) (ha : Filter.Tendsto a l (nhds a₀)) (hb : Filter.Tendsto b l (nhds b₀)) (h : ∀ᶠ (i : ι) in l, ∫ (x : ) in Set.Ioc (a i) (b i), f x I) :
MeasureTheory.IntegrableOn f (Set.Ioc a₀ b₀) MeasureTheory.volume
theorem MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_left {ι : Type u_1} {E : Type u_2} {l : } [l.NeBot] [l.IsCountablyGenerated] {a : ι} {f : E} {I : } {a₀ : } {b : } (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) MeasureTheory.volume) (ha : Filter.Tendsto a l (nhds a₀)) (h : ∀ᶠ (i : ι) in l, ∫ (x : ) in Set.Ioc (a i) b, f x I) :
MeasureTheory.IntegrableOn f (Set.Ioc a₀ b) MeasureTheory.volume
theorem MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_right {ι : Type u_1} {E : Type u_2} {l : } [l.NeBot] [l.IsCountablyGenerated] {b : ι} {f : E} {I : } {a : } {b₀ : } (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) MeasureTheory.volume) (hb : Filter.Tendsto b l (nhds b₀)) (h : ∀ᶠ (i : ι) in l, ∫ (x : ) in Set.Ioc a (b i), f x I) :
MeasureTheory.IntegrableOn f (Set.Ioc a b₀) MeasureTheory.volume
@[deprecated MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded]
theorem MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded {ι : Type u_1} {E : Type u_2} {l : } [l.NeBot] [l.IsCountablyGenerated] {a : ι} {b : ι} {f : E} {I : } {a₀ : } {b₀ : } (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) MeasureTheory.volume) (ha : Filter.Tendsto a l (nhds a₀)) (hb : Filter.Tendsto b l (nhds b₀)) (h : ∀ᶠ (i : ι) in l, ∫ (x : ) in Set.Ioc (a i) (b i), f x I) :
MeasureTheory.IntegrableOn f (Set.Ioc a₀ b₀) MeasureTheory.volume

Alias of MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded.

@[deprecated MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_left]
theorem MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded_left {ι : Type u_1} {E : Type u_2} {l : } [l.NeBot] [l.IsCountablyGenerated] {a : ι} {f : E} {I : } {a₀ : } {b : } (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) MeasureTheory.volume) (ha : Filter.Tendsto a l (nhds a₀)) (h : ∀ᶠ (i : ι) in l, ∫ (x : ) in Set.Ioc (a i) b, f x I) :
MeasureTheory.IntegrableOn f (Set.Ioc a₀ b) MeasureTheory.volume

Alias of MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_left.

@[deprecated MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_right]
theorem MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded_right {ι : Type u_1} {E : Type u_2} {l : } [l.NeBot] [l.IsCountablyGenerated] {b : ι} {f : E} {I : } {a : } {b₀ : } (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) MeasureTheory.volume) (hb : Filter.Tendsto b l (nhds b₀)) (h : ∀ᶠ (i : ι) in l, ∫ (x : ) in Set.Ioc a (b i), f x I) :
MeasureTheory.IntegrableOn f (Set.Ioc a b₀) MeasureTheory.volume

Alias of MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_right.

theorem MeasureTheory.intervalIntegral_tendsto_integral {ι : Type u_1} {E : Type u_2} {μ : } {l : } [l.IsCountablyGenerated] [] {a : ι} {b : ι} {f : E} (hfi : ) (ha : Filter.Tendsto a l Filter.atBot) (hb : Filter.Tendsto b l Filter.atTop) :
Filter.Tendsto (fun (i : ι) => ∫ (x : ) in a i..b i, f xμ) l (nhds (∫ (x : ), f xμ))
theorem MeasureTheory.intervalIntegral_tendsto_integral_Iic {ι : Type u_1} {E : Type u_2} {μ : } {l : } [l.IsCountablyGenerated] [] {a : ι} {f : E} (b : ) (hfi : ) (ha : Filter.Tendsto a l Filter.atBot) :
Filter.Tendsto (fun (i : ι) => ∫ (x : ) in a i..b, f xμ) l (nhds (∫ (x : ) in , f xμ))
theorem MeasureTheory.intervalIntegral_tendsto_integral_Ioi {ι : Type u_1} {E : Type u_2} {μ : } {l : } [l.IsCountablyGenerated] [] {b : ι} {f : E} (a : ) (hfi : ) (hb : Filter.Tendsto b l Filter.atTop) :
Filter.Tendsto (fun (i : ι) => ∫ (x : ) in a..b i, f xμ) l (nhds (∫ (x : ) in , f xμ))
theorem MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi {E : Type u_1} {f : E} {f' : E} {a : } [] [] (hderiv : x, HasDerivAt f (f' x) x) (f'int : MeasureTheory.IntegrableOn f' () MeasureTheory.volume) :
Filter.Tendsto f Filter.atTop (nhds (limUnder Filter.atTop f))

If the derivative of a function defined on the real line is integrable close to +∞, then the function has a limit at +∞.

theorem MeasureTheory.tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi {E : Type u_1} {f : E} {f' : E} {a : } [] (hderiv : x, HasDerivAt f (f' x) x) (f'int : MeasureTheory.IntegrableOn f' () MeasureTheory.volume) (fint : MeasureTheory.IntegrableOn f () MeasureTheory.volume) :
Filter.Tendsto f Filter.atTop (nhds 0)

If a function and its derivative are integrable on (a, +∞), then the function tends to zero at +∞.

theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto {E : Type u_1} {f : E} {f' : E} {a : } {m : E} [] [] (hcont : ) (hderiv : x, HasDerivAt f (f' x) x) (f'int : MeasureTheory.IntegrableOn f' () MeasureTheory.volume) (hf : Filter.Tendsto f Filter.atTop (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 at a⁺.

Note that such a function always has a limit at infinity, see tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi.

theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto' {E : Type u_1} {f : E} {f' : E} {a : } {m : E} [] [] (hderiv : x, HasDerivAt f (f' x) x) (f'int : MeasureTheory.IntegrableOn f' () MeasureTheory.volume) (hf : Filter.Tendsto f Filter.atTop (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, +∞).

Note that such a function always has a limit at infinity, see tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi.

theorem HasCompactSupport.integral_Ioi_deriv_eq {E : Type u_1} {f : E} [] [] (hf : ) (h2f : ) (b : ) :
∫ (x : ) in , deriv f x = -f b

A special case of integral_Ioi_of_hasDerivAt_of_tendsto where we assume that f is C^1 with compact support.

theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonneg {g : } {g' : } {a : } {l : } (hcont : ) (hderiv : x, HasDerivAt g (g' x) x) (g'pos : x, 0 g' x) (hg : Filter.Tendsto g Filter.atTop (nhds l)) :
MeasureTheory.IntegrableOn g' () MeasureTheory.volume

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 at a⁺.

theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonneg' {g : } {g' : } {a : } {l : } (hderiv : x, HasDerivAt g (g' x) x) (g'pos : x, 0 g' x) (hg : Filter.Tendsto g Filter.atTop (nhds l)) :
MeasureTheory.IntegrableOn g' () MeasureTheory.volume

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 MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg {g : } {g' : } {a : } {l : } (hcont : ) (hderiv : x, HasDerivAt g (g' x) x) (g'pos : x, 0 g' x) (hg : Filter.Tendsto g Filter.atTop (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 at a⁺.

theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg' {g : } {g' : } {a : } {l : } (hderiv : x, HasDerivAt g (g' x) x) (g'pos : x, 0 g' x) (hg : Filter.Tendsto g Filter.atTop (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 MeasureTheory.integrableOn_Ioi_deriv_of_nonpos {g : } {g' : } {a : } {l : } (hcont : ) (hderiv : x, HasDerivAt g (g' x) x) (g'neg : x, g' x 0) (hg : Filter.Tendsto g Filter.atTop (nhds l)) :
MeasureTheory.IntegrableOn g' () MeasureTheory.volume

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 at a⁺.

theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonpos' {g : } {g' : } {a : } {l : } (hderiv : x, HasDerivAt g (g' x) x) (g'neg : x, g' x 0) (hg : Filter.Tendsto g Filter.atTop (nhds l)) :
MeasureTheory.IntegrableOn g' () MeasureTheory.volume

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 MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos {g : } {g' : } {a : } {l : } (hcont : ) (hderiv : x, HasDerivAt g (g' x) x) (g'neg : x, g' x 0) (hg : Filter.Tendsto g Filter.atTop (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 at a⁺.

theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos' {g : } {g' : } {a : } {l : } (hderiv : x, HasDerivAt g (g' x) x) (g'neg : x, g' x 0) (hg : Filter.Tendsto g Filter.atTop (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 MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic {E : Type u_1} {f : E} {f' : E} {a : } [] [] (hderiv : x, HasDerivAt f (f' x) x) (f'int : MeasureTheory.IntegrableOn f' () MeasureTheory.volume) :
Filter.Tendsto f Filter.atBot (nhds (limUnder Filter.atBot f))

If the derivative of a function defined on the real line is integrable close to -∞, then the function has a limit at -∞.

theorem MeasureTheory.tendsto_zero_of_hasDerivAt_of_integrableOn_Iic {E : Type u_1} {f : E} {f' : E} {a : } [] (hderiv : x, HasDerivAt f (f' x) x) (f'int : MeasureTheory.IntegrableOn f' () MeasureTheory.volume) (fint : MeasureTheory.IntegrableOn f () MeasureTheory.volume) :
Filter.Tendsto f Filter.atBot (nhds 0)

If a function and its derivative are integrable on (-∞, a], then the function tends to zero at -∞.

theorem MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto {E : Type u_1} {f : E} {f' : E} {a : } {m : E} [] [] (hcont : ) (hderiv : x, HasDerivAt f (f' x) x) (f'int : MeasureTheory.IntegrableOn f' () MeasureTheory.volume) (hf : Filter.Tendsto f Filter.atBot (nhds m)) :
∫ (x : ) in , f' x = f a - m

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

Note that such a function always has a limit at minus infinity, see tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic.

theorem MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto' {E : Type u_1} {f : E} {f' : E} {a : } {m : E} [] [] (hderiv : x, HasDerivAt f (f' x) x) (f'int : MeasureTheory.IntegrableOn f' () MeasureTheory.volume) (hf : Filter.Tendsto f Filter.atBot (nhds m)) :
∫ (x : ) in , f' x = f a - m

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

Note that such a function always has a limit at minus infinity, see tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic.

theorem HasCompactSupport.integral_Iic_deriv_eq {E : Type u_1} {f : E} [] [] (hf : ) (h2f : ) (b : ) :
∫ (x : ) in , deriv f x = f b

A special case of integral_Iic_of_hasDerivAt_of_tendsto where we assume that f is C^1 with compact support.

theorem MeasureTheory.integral_of_hasDerivAt_of_tendsto {E : Type u_1} {f : E} {f' : E} {m : E} {n : E} [] [] (hderiv : ∀ (x : ), HasDerivAt f (f' x) x) (hf' : MeasureTheory.Integrable f' MeasureTheory.volume) (hbot : Filter.Tendsto f Filter.atBot (nhds m)) (htop : Filter.Tendsto f Filter.atTop (nhds n)) :
∫ (x : ), f' x = n - m

Fundamental theorem of calculus-2, on the whole real line When a function has a limit m at -∞ and n at +∞, and its derivative is integrable, then the integral of the derivative is n - m.

Note that such a function always has a limit at -∞ and +∞, see tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic and tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi.

theorem MeasureTheory.integral_eq_zero_of_hasDerivAt_of_integrable {E : Type u_1} {f : E} {f' : E} [] (hderiv : ∀ (x : ), HasDerivAt f (f' x) x) (hf' : MeasureTheory.Integrable f' MeasureTheory.volume) (hf : MeasureTheory.Integrable f MeasureTheory.volume) :
∫ (x : ), f' x = 0

If a function and its derivative are integrable on the real line, then the integral of the derivative is zero.

theorem MeasureTheory.integral_comp_smul_deriv_Ioi {E : Type u_1} [] {f : } {f' : } {g : E} {a : } (hf : ContinuousOn f ()) (hft : Filter.Tendsto f Filter.atTop Filter.atTop) (hff' : x, HasDerivWithinAt f (f' x) () x) (hg_cont : ContinuousOn g (f '' )) (hg1 : MeasureTheory.IntegrableOn g (f '' ) MeasureTheory.volume) (hg2 : MeasureTheory.IntegrableOn (fun (x : ) => f' x (g f) x) () MeasureTheory.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 MeasureTheory.integral_comp_mul_deriv_Ioi {f : } {f' : } {g : } {a : } (hf : ContinuousOn f ()) (hft : Filter.Tendsto f Filter.atTop Filter.atTop) (hff' : x, HasDerivWithinAt f (f' x) () x) (hg_cont : ContinuousOn g (f '' )) (hg1 : MeasureTheory.IntegrableOn g (f '' ) MeasureTheory.volume) (hg2 : MeasureTheory.IntegrableOn (fun (x : ) => (g f) x * f' x) () MeasureTheory.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 MeasureTheory.integral_comp_rpow_Ioi {E : Type u_1} [] (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 MeasureTheory.integral_comp_rpow_Ioi_of_pos {E : Type u_1} [] {g : E} {p : } (hp : 0 < p) :
∫ (x : ) in , (p * x ^ (p - 1)) g (x ^ p) = ∫ (y : ) in , g y
theorem MeasureTheory.integral_comp_mul_left_Ioi {E : Type u_1} [] (g : E) (a : ) {b : } (hb : 0 < b) :
∫ (x : ) in , g (b * x) = b⁻¹ ∫ (x : ) in Set.Ioi (b * a), g x
theorem MeasureTheory.integral_comp_mul_right_Ioi {E : Type u_1} [] (g : E) (a : ) {b : } (hb : 0 < b) :
∫ (x : ) in , g (x * b) = b⁻¹ ∫ (x : ) in Set.Ioi (a * b), g x
theorem MeasureTheory.integrableOn_Ioi_comp_rpow_iff {E : Type u_1} [] (f : E) {p : } (hp : p 0) :
MeasureTheory.IntegrableOn (fun (x : ) => (|p| * x ^ (p - 1)) f (x ^ p)) () MeasureTheory.volume MeasureTheory.IntegrableOn f () MeasureTheory.volume

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

theorem MeasureTheory.integrableOn_Ioi_comp_rpow_iff' {E : Type u_1} [] (f : E) {p : } (hp : p 0) :
MeasureTheory.IntegrableOn (fun (x : ) => x ^ (p - 1) f (x ^ p)) () MeasureTheory.volume MeasureTheory.IntegrableOn f () MeasureTheory.volume

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

theorem MeasureTheory.integrableOn_Ioi_comp_mul_left_iff {E : Type u_1} (f : E) (c : ) {a : } (ha : 0 < a) :
MeasureTheory.IntegrableOn (fun (x : ) => f (a * x)) () MeasureTheory.volume MeasureTheory.IntegrableOn f (Set.Ioi (a * c)) MeasureTheory.volume
theorem MeasureTheory.integrableOn_Ioi_comp_mul_right_iff {E : Type u_1} (f : E) (c : ) {a : } (ha : 0 < a) :
MeasureTheory.IntegrableOn (fun (x : ) => f (x * a)) () MeasureTheory.volume MeasureTheory.IntegrableOn f (Set.Ioi (c * a)) MeasureTheory.volume

## Integration by parts #

theorem MeasureTheory.integral_bilinear_hasDerivAt_eq_sub {E : Type u_1} {F : Type u_2} {G : Type u_3} [] [] [] {L : E →L[] F →L[] G} {u : E} {v : F} {u' : E} {v' : F} {m : G} {n : G} [] (hu : ∀ (x : ), HasDerivAt u (u' x) x) (hv : ∀ (x : ), HasDerivAt v (v' x) x) (huv : MeasureTheory.Integrable (fun (x : ) => (L (u x)) (v' x) + (L (u' x)) (v x)) MeasureTheory.volume) (h_bot : Filter.Tendsto (fun (x : ) => (L (u x)) (v x)) Filter.atBot (nhds m)) (h_top : Filter.Tendsto (fun (x : ) => (L (u x)) (v x)) Filter.atTop (nhds n)) :
∫ (x : ), (L (u x)) (v' x) + (L (u' x)) (v x) = n - m
theorem MeasureTheory.integral_bilinear_hasDerivAt_right_eq_sub {E : Type u_1} {F : Type u_2} {G : Type u_3} [] [] [] {L : E →L[] F →L[] G} {u : E} {v : F} {u' : E} {v' : F} {m : G} {n : G} [] (hu : ∀ (x : ), HasDerivAt u (u' x) x) (hv : ∀ (x : ), HasDerivAt v (v' x) x) (huv' : MeasureTheory.Integrable (fun (x : ) => (L (u x)) (v' x)) MeasureTheory.volume) (hu'v : MeasureTheory.Integrable (fun (x : ) => (L (u' x)) (v x)) MeasureTheory.volume) (h_bot : Filter.Tendsto (fun (x : ) => (L (u x)) (v x)) Filter.atBot (nhds m)) (h_top : Filter.Tendsto (fun (x : ) => (L (u x)) (v x)) Filter.atTop (nhds n)) :
∫ (x : ), (L (u x)) (v' x) = n - m - ∫ (x : ), (L (u' x)) (v x)

Integration by parts on (-∞, ∞). With respect to a general bilinear form. For the specific case of multiplication, see integral_mul_deriv_eq_deriv_mul.

theorem MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable {E : Type u_1} {F : Type u_2} {G : Type u_3} [] [] [] {L : E →L[] F →L[] G} {u : E} {v : F} {u' : E} {v' : F} (hu : ∀ (x : ), HasDerivAt u (u' x) x) (hv : ∀ (x : ), HasDerivAt v (v' x) x) (huv' : MeasureTheory.Integrable (fun (x : ) => (L (u x)) (v' x)) MeasureTheory.volume) (hu'v : MeasureTheory.Integrable (fun (x : ) => (L (u' x)) (v x)) MeasureTheory.volume) (huv : MeasureTheory.Integrable (fun (x : ) => (L (u x)) (v x)) MeasureTheory.volume) :
∫ (x : ), (L (u x)) (v' x) = -∫ (x : ), (L (u' x)) (v x)

Integration by parts on (-∞, ∞). With respect to a general bilinear form, assuming moreover that the total function is integrable.

theorem MeasureTheory.integral_deriv_mul_eq_sub {A : Type u_1} [] [] {a' : A} {b' : A} {u : A} {v : A} {u' : A} {v' : A} [] (hu : ∀ (x : ), HasDerivAt u (u' x) x) (hv : ∀ (x : ), HasDerivAt v (v' x) x) (huv : MeasureTheory.Integrable (u' * v + u * v') MeasureTheory.volume) (h_bot : Filter.Tendsto (u * v) Filter.atBot (nhds a')) (h_top : Filter.Tendsto (u * v) Filter.atTop (nhds b')) :
∫ (x : ), u' x * v x + u x * v' x = b' - a'

For finite intervals, see: intervalIntegral.integral_deriv_mul_eq_sub.

theorem MeasureTheory.integral_mul_deriv_eq_deriv_mul {A : Type u_1} [] [] {a' : A} {b' : A} {u : A} {v : A} {u' : A} {v' : A} [] (hu : ∀ (x : ), HasDerivAt u (u' x) x) (hv : ∀ (x : ), HasDerivAt v (v' x) x) (huv' : MeasureTheory.Integrable (u * v') MeasureTheory.volume) (hu'v : MeasureTheory.Integrable (u' * v) MeasureTheory.volume) (h_bot : Filter.Tendsto (u * v) Filter.atBot (nhds a')) (h_top : Filter.Tendsto (u * v) Filter.atTop (nhds b')) :
∫ (x : ), u x * v' x = b' - a' - ∫ (x : ), u' x * v x

Integration by parts on (-∞, ∞). For finite intervals, see: intervalIntegral.integral_mul_deriv_eq_deriv_mul.

theorem MeasureTheory.integral_mul_deriv_eq_deriv_mul_of_integrable {A : Type u_1} [] [] {u : A} {v : A} {u' : A} {v' : A} (hu : ∀ (x : ), HasDerivAt u (u' x) x) (hv : ∀ (x : ), HasDerivAt v (v' x) x) (huv' : MeasureTheory.Integrable (u * v') MeasureTheory.volume) (hu'v : MeasureTheory.Integrable (u' * v) MeasureTheory.volume) (huv : MeasureTheory.Integrable (u * v) MeasureTheory.volume) :
∫ (x : ), u x * v' x = -∫ (x : ), u' x * v x

Integration by parts on (-∞, ∞). Version assuming that the total function is integrable

theorem MeasureTheory.integral_Ioi_deriv_mul_eq_sub {A : Type u_1} [] [] {a : } {a' : A} {b' : A} {u : A} {v : A} {u' : A} {v' : A} [] (hu : x, HasDerivAt u (u' x) x) (hv : x, HasDerivAt v (v' x) x) (huv : MeasureTheory.IntegrableOn (u' * v + u * v') () MeasureTheory.volume) (h_zero : Filter.Tendsto (u * v) (nhdsWithin a ()) (nhds a')) (h_infty : Filter.Tendsto (u * v) Filter.atTop (nhds b')) :
∫ (x : ) in , u' x * v x + u x * v' x = b' - a'

For finite intervals, see: intervalIntegral.integral_deriv_mul_eq_sub.

theorem MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul {A : Type u_1} [] [] {a : } {a' : A} {b' : A} {u : A} {v : A} {u' : A} {v' : A} [] (hu : x, HasDerivAt u (u' x) x) (hv : x, HasDerivAt v (v' x) x) (huv' : MeasureTheory.IntegrableOn (u * v') () MeasureTheory.volume) (hu'v : MeasureTheory.IntegrableOn (u' * v) () MeasureTheory.volume) (h_zero : Filter.Tendsto (u * v) (nhdsWithin a ()) (nhds a')) (h_infty : Filter.Tendsto (u * v) Filter.atTop (nhds b')) :
∫ (x : ) in , u x * v' x = b' - a' - ∫ (x : ) in , u' x * v x

Integration by parts on (a, ∞). For finite intervals, see: intervalIntegral.integral_mul_deriv_eq_deriv_mul.

theorem MeasureTheory.integral_Iic_deriv_mul_eq_sub {A : Type u_1} [] [] {a : } {a' : A} {b' : A} {u : A} {v : A} {u' : A} {v' : A} [] (hu : x, HasDerivAt u (u' x) x) (hv : x, HasDerivAt v (v' x) x) (huv : MeasureTheory.IntegrableOn (u' * v + u * v') () MeasureTheory.volume) (h_zero : Filter.Tendsto (u * v) (nhdsWithin a ()) (nhds a')) (h_infty : Filter.Tendsto (u * v) Filter.atBot (nhds b')) :
∫ (x : ) in , u' x * v x + u x * v' x = a' - b'

For finite intervals, see: intervalIntegral.integral_deriv_mul_eq_sub.

theorem MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul {A : Type u_1} [] [] {a : } {a' : A} {b' : A} {u : A} {v : A} {u' : A} {v' : A} [] (hu : x, HasDerivAt u (u' x) x) (hv : x, HasDerivAt v (v' x) x) (huv' : MeasureTheory.IntegrableOn (u * v') () MeasureTheory.volume) (hu'v : MeasureTheory.IntegrableOn (u' * v) () MeasureTheory.volume) (h_zero : Filter.Tendsto (u * v) (nhdsWithin a ()) (nhds a')) (h_infty : Filter.Tendsto (u * v) Filter.atBot (nhds b')) :
∫ (x : ) in , u x * v' x = a' - b' - ∫ (x : ) in , u' x * v x

Integration by parts on (∞, a]. For finite intervals, see: intervalIntegral.integral_mul_deriv_eq_deriv_mul.