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 (λ x, Ioi 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 aMeasureTheory.AECover μ l, wherelis a countably generated filter, and iffis a measurableENNReal-valued function, then∫⁻ x in φ n, f x ∂μtends to∫⁻ x, f x ∂μasntends tol -
MeasureTheory.AECover.integrable_of_integral_norm_tendsto: ifφis aMeasureTheory.AECover μ l, wherelis a countably generated filter, iffis measurable and integrable on eachφ n, and if∫ x in φ n, ‖f x‖ ∂μtends to someI : ℝas n tends tol, thenfis integrable -
MeasureTheory.AECover.integral_tendsto_of_countably_generated: ifφis aMeasureTheory.AECover μ l, wherelis a countably generated filter, and iffis measurable and integrable (globally), then∫ x in φ n, f x ∂μtends to∫ x, f x ∂μasntends 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_tendstois a version of FTC-2 on the interval(a, +∞), giving the formula∫ x in (a, +∞), g' x = l - g aifg'is integrable andgtends tolat+∞.MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneggives the same result assuming thatg'is nonnegative instead of integrable. Its automatic integrability in this context is proved inMeasureTheory.integrableOn_Ioi_deriv_of_nonneg.MeasureTheory.integral_comp_smul_deriv_Ioiis a version of the change of variables formula on semi-infinite intervals.
structure
MeasureTheory.AECover
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
(l : Filter ι)
(φ : ι → 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.inter
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
{φ : ι → Set α}
{ψ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
(hψ : MeasureTheory.AECover μ l ψ)
:
MeasureTheory.AECover μ l fun (i : ι) => φ i ∩ ψ i
theorem
MeasureTheory.AECover.superset
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
{φ : ι → Set α}
{ψ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
(hsub : ∀ (i : ι), φ i ⊆ ψ i)
(hmeas : ∀ (i : ι), MeasurableSet (ψ i))
:
MeasureTheory.AECover μ l ψ
theorem
MeasureTheory.AECover.mono_ac
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
{ν : MeasureTheory.Measure α}
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
(hle : MeasureTheory.Measure.AbsolutelyContinuous ν μ)
:
MeasureTheory.AECover ν l φ
theorem
MeasureTheory.AECover.mono
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
{ν : MeasureTheory.Measure α}
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
(hle : ν ≤ μ)
:
MeasureTheory.AECover ν l φ
theorem
MeasureTheory.aecover_Ici
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[Preorder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[Preorder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[Preorder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
(ha : Filter.Tendsto a l Filter.atBot)
[NoMinOrder α]
:
MeasureTheory.AECover μ l fun (i : ι) => Set.Ioi (a i)
theorem
MeasureTheory.aecover_Iio
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{b : ι → α}
(hb : Filter.Tendsto b l Filter.atTop)
[NoMaxOrder α]
:
MeasureTheory.AECover μ l fun (i : ι) => Set.Iio (b i)
theorem
MeasureTheory.aecover_Ioo
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
(ha : Filter.Tendsto a l Filter.atBot)
(hb : Filter.Tendsto b l Filter.atTop)
[NoMinOrder α]
[NoMaxOrder α]
:
MeasureTheory.AECover μ l fun (i : ι) => Set.Ioo (a i) (b i)
theorem
MeasureTheory.aecover_Ioc
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
(ha : Filter.Tendsto a l Filter.atBot)
(hb : Filter.Tendsto b l Filter.atTop)
[NoMinOrder α]
:
MeasureTheory.AECover μ l fun (i : ι) => Set.Ioc (a i) (b i)
theorem
MeasureTheory.aecover_Ico
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
(ha : Filter.Tendsto a l Filter.atBot)
(hb : Filter.Tendsto b l Filter.atTop)
[NoMaxOrder α]
:
MeasureTheory.AECover μ l fun (i : ι) => Set.Ico (a i) (b i)
theorem
MeasureTheory.aecover_Ioi_of_Ioi
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{A : α}
(ha : Filter.Tendsto a l (nhds A))
:
MeasureTheory.AECover (MeasureTheory.Measure.restrict μ (Set.Ioi A)) l fun (i : ι) => Set.Ioi (a i)
theorem
MeasureTheory.aecover_Iio_of_Iio
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{b : ι → α}
{B : α}
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.restrict μ (Set.Iio B)) l fun (i : ι) => Set.Iio (b i)
theorem
MeasureTheory.aecover_Ioi_of_Ici
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{A : α}
(ha : Filter.Tendsto a l (nhds A))
:
MeasureTheory.AECover (MeasureTheory.Measure.restrict μ (Set.Ioi A)) l fun (i : ι) => Set.Ici (a i)
theorem
MeasureTheory.aecover_Iio_of_Iic
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{b : ι → α}
{B : α}
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.restrict μ (Set.Iio B)) l fun (i : ι) => Set.Iic (b i)
theorem
MeasureTheory.aecover_Ioo_of_Ioo
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
[MeasureTheory.NoAtoms μ]
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
[MeasureTheory.NoAtoms μ]
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
[MeasureTheory.NoAtoms μ]
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
[MeasureTheory.NoAtoms μ]
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
[MeasureTheory.NoAtoms μ]
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
[MeasureTheory.NoAtoms μ]
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
[MeasureTheory.NoAtoms μ]
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
[MeasureTheory.NoAtoms μ]
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
[MeasureTheory.NoAtoms μ]
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
[MeasureTheory.NoAtoms μ]
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
[MeasureTheory.NoAtoms μ]
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[LinearOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
[OpensMeasurableSpace α]
{a : ι → α}
{b : ι → α}
{A : α}
{B : α}
[MeasureTheory.NoAtoms μ]
(ha : Filter.Tendsto a l (nhds A))
(hb : Filter.Tendsto b l (nhds B))
:
MeasureTheory.AECover (MeasureTheory.Measure.restrict μ (Set.Icc A B)) l fun (i : ι) => Set.Ioo (a i) (b i)
theorem
MeasureTheory.AECover.restrict
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{s : Set α}
:
theorem
MeasureTheory.aecover_restrict_of_ae_imp
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
{s : Set α}
{φ : ι → Set α}
(hs : MeasurableSet s)
(ae_eventually_mem : ∀ᵐ (x : α) ∂μ, x ∈ s → ∀ᶠ (n : ι) in l, x ∈ φ n)
(measurable : ∀ (n : ι), MeasurableSet (φ n))
:
theorem
MeasureTheory.AECover.inter_restrict
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{s : Set α}
(hs : MeasurableSet s)
:
MeasureTheory.AECover (MeasureTheory.Measure.restrict μ s) l fun (i : ι) => φ i ∩ s
theorem
MeasureTheory.AECover.ae_tendsto_indicator
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
{β : Type u_3}
[Zero β]
[TopologicalSpace β]
(f : α → β)
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
:
∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (i : ι) => Set.indicator (φ i) f x) l (nhds (f x))
theorem
MeasureTheory.AECover.aemeasurable
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
{β : Type u_3}
[MeasurableSpace β]
[Filter.IsCountablyGenerated l]
[Filter.NeBot l]
{f : α → β}
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
(hfm : ∀ (i : ι), AEMeasurable f)
:
theorem
MeasureTheory.AECover.aestronglyMeasurable
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
{β : Type u_3}
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[Filter.IsCountablyGenerated l]
[Filter.NeBot l]
{f : α → β}
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
(hfm : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ (φ i)))
:
theorem
MeasureTheory.AECover.comp_tendsto
{α : Type u_1}
{ι : Type u_2}
{ι' : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
{l' : Filter ι'}
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{u : ι' → ι}
(hu : Filter.Tendsto u l' l)
:
MeasureTheory.AECover μ l' (φ ∘ u)
theorem
MeasureTheory.AECover.biUnion_Iic_aecover
{α : Type u_1}
{ι : Type u_2}
[Countable ι]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[Preorder ι]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ Filter.atTop φ)
:
MeasureTheory.AECover μ Filter.atTop fun (n : ι) => ⋃ k ∈ Set.Iic n, φ k
theorem
MeasureTheory.AECover.biInter_Ici_aecover
{α : Type u_1}
{ι : Type u_2}
[Countable ι]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[Preorder ι]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ Filter.atTop φ)
:
MeasureTheory.AECover μ Filter.atTop fun (n : ι) => ⋂ k ∈ Set.Ici n, φ k
theorem
MeasureTheory.AECover.lintegral_tendsto_of_nat
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{φ : ℕ → Set α}
(hφ : MeasureTheory.AECover μ Filter.atTop φ)
{f : α → ENNReal}
(hfm : AEMeasurable f)
:
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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{f : α → ENNReal}
(hfm : AEMeasurable f)
:
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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{f : α → ENNReal}
(I : ENNReal)
(hfm : AEMeasurable f)
(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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[Nonempty ι]
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{f : α → ENNReal}
(hfm : AEMeasurable f)
:
⨆ (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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[NormedAddCommGroup E]
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{f : α → E}
(I : ℝ)
(hfm : MeasureTheory.AEStronglyMeasurable f μ)
(hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I)
:
theorem
MeasureTheory.AECover.integrable_of_lintegral_nnnorm_tendsto
{α : Type u_1}
{ι : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[NormedAddCommGroup E]
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{f : α → E}
(I : ℝ)
(hfm : MeasureTheory.AEStronglyMeasurable f μ)
(htendsto : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (nhds (ENNReal.ofReal I)))
:
theorem
MeasureTheory.AECover.integrable_of_lintegral_nnnorm_bounded'
{α : Type u_1}
{ι : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[NormedAddCommGroup E]
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{f : α → E}
(I : NNReal)
(hfm : MeasureTheory.AEStronglyMeasurable f μ)
(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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[NormedAddCommGroup E]
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{f : α → E}
(I : NNReal)
(hfm : MeasureTheory.AEStronglyMeasurable f μ)
(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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[NormedAddCommGroup E]
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[NormedAddCommGroup E]
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{f : α → E}
(hfi : MeasureTheory.Integrable f)
:
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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{f : α → E}
(I : E)
(hfi : MeasureTheory.Integrable f)
(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}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
{φ : ι → Set α}
(hφ : MeasureTheory.AECover μ l φ)
{f : α → ℝ}
(I : ℝ)
(hnng : 0 ≤ᶠ[MeasureTheory.Measure.ae μ] 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}
{μ : MeasureTheory.Measure ℝ}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
[NormedAddCommGroup E]
{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}
{μ : MeasureTheory.Measure ℝ}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
[NormedAddCommGroup E]
{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}
{μ : MeasureTheory.Measure ℝ}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
[NormedAddCommGroup E]
{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}
{μ : MeasureTheory.Measure ℝ}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
[NormedAddCommGroup E]
{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}
{μ : MeasureTheory.Measure ℝ}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
[NormedAddCommGroup E]
{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}
{μ : MeasureTheory.Measure ℝ}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
[NormedAddCommGroup E]
{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_interval_integral_norm_bounded
{ι : Type u_1}
{E : Type u_2}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
[NormedAddCommGroup E]
{a : ι → ℝ}
{b : ι → ℝ}
{f : ℝ → E}
{I : ℝ}
{a₀ : ℝ}
{b₀ : ℝ}
(hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)))
(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₀)
theorem
MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded_left
{ι : Type u_1}
{E : Type u_2}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
[NormedAddCommGroup E]
{a : ι → ℝ}
{f : ℝ → E}
{I : ℝ}
{a₀ : ℝ}
{b : ℝ}
(hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b))
(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)
theorem
MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded_right
{ι : Type u_1}
{E : Type u_2}
{l : Filter ι}
[Filter.NeBot l]
[Filter.IsCountablyGenerated l]
[NormedAddCommGroup E]
{b : ι → ℝ}
{f : ℝ → E}
{I : ℝ}
{a : ℝ}
{b₀ : ℝ}
(hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)))
(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₀)
theorem
MeasureTheory.intervalIntegral_tendsto_integral
{ι : Type u_1}
{E : Type u_2}
{μ : MeasureTheory.Measure ℝ}
{l : Filter ι}
[Filter.IsCountablyGenerated l]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a : ι → ℝ}
{b : ι → ℝ}
{f : ℝ → E}
(hfi : MeasureTheory.Integrable f)
(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}
{μ : MeasureTheory.Measure ℝ}
{l : Filter ι}
[Filter.IsCountablyGenerated l]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{a : ι → ℝ}
{f : ℝ → E}
(b : ℝ)
(hfi : MeasureTheory.IntegrableOn f (Set.Iic b))
(ha : Filter.Tendsto a l Filter.atBot)
:
Filter.Tendsto (fun (i : ι) => ∫ (x : ℝ) in a i..b, f x ∂μ) l (nhds (∫ (x : ℝ) in Set.Iic b, f x ∂μ))
theorem
MeasureTheory.intervalIntegral_tendsto_integral_Ioi
{ι : Type u_1}
{E : Type u_2}
{μ : MeasureTheory.Measure ℝ}
{l : Filter ι}
[Filter.IsCountablyGenerated l]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{b : ι → ℝ}
{f : ℝ → E}
(a : ℝ)
(hfi : MeasureTheory.IntegrableOn f (Set.Ioi a))
(hb : Filter.Tendsto b l Filter.atTop)
:
Filter.Tendsto (fun (i : ι) => ∫ (x : ℝ) in a..b i, f x ∂μ) l (nhds (∫ (x : ℝ) in Set.Ioi a, f x ∂μ))
theorem
MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto
{E : Type u_1}
{f : ℝ → E}
{f' : ℝ → E}
{a : ℝ}
{m : E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hcont : ContinuousWithinAt f (Set.Ici a) a)
(hderiv : ∀ x ∈ Set.Ioi a, HasDerivAt f (f' x) x)
(f'int : MeasureTheory.IntegrableOn f' (Set.Ioi a))
(hf : Filter.Tendsto f Filter.atTop (nhds m))
:
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⁺.
theorem
MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto'
{E : Type u_1}
{f : ℝ → E}
{f' : ℝ → E}
{a : ℝ}
{m : E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hderiv : ∀ x ∈ Set.Ici a, HasDerivAt f (f' x) x)
(f'int : MeasureTheory.IntegrableOn f' (Set.Ioi a))
(hf : Filter.Tendsto f Filter.atTop (nhds m))
:
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
HasCompactSupport.integral_Ioi_deriv_eq
{E : Type u_1}
{f : ℝ → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hf : ContDiff ℝ 1 f)
(h2f : HasCompactSupport 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 : ContinuousWithinAt g (Set.Ici a) a)
(hderiv : ∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x)
(g'pos : ∀ x ∈ Set.Ioi a, 0 ≤ g' x)
(hg : Filter.Tendsto g Filter.atTop (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 at a⁺.
theorem
MeasureTheory.integrableOn_Ioi_deriv_of_nonneg'
{g : ℝ → ℝ}
{g' : ℝ → ℝ}
{a : ℝ}
{l : ℝ}
(hderiv : ∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x)
(g'pos : ∀ x ∈ Set.Ioi a, 0 ≤ g' x)
(hg : Filter.Tendsto g Filter.atTop (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
MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg
{g : ℝ → ℝ}
{g' : ℝ → ℝ}
{a : ℝ}
{l : ℝ}
(hcont : ContinuousWithinAt g (Set.Ici a) a)
(hderiv : ∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x)
(g'pos : ∀ x ∈ Set.Ioi a, 0 ≤ g' x)
(hg : Filter.Tendsto g Filter.atTop (nhds l))
:
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 ∈ Set.Ici a, HasDerivAt g (g' x) x)
(g'pos : ∀ x ∈ Set.Ioi a, 0 ≤ g' x)
(hg : Filter.Tendsto g Filter.atTop (nhds l))
:
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 : ContinuousWithinAt g (Set.Ici a) a)
(hderiv : ∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x)
(g'neg : ∀ x ∈ Set.Ioi a, g' x ≤ 0)
(hg : Filter.Tendsto g Filter.atTop (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 at a⁺.
theorem
MeasureTheory.integrableOn_Ioi_deriv_of_nonpos'
{g : ℝ → ℝ}
{g' : ℝ → ℝ}
{a : ℝ}
{l : ℝ}
(hderiv : ∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x)
(g'neg : ∀ x ∈ Set.Ioi a, g' x ≤ 0)
(hg : Filter.Tendsto g Filter.atTop (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
MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos
{g : ℝ → ℝ}
{g' : ℝ → ℝ}
{a : ℝ}
{l : ℝ}
(hcont : ContinuousWithinAt g (Set.Ici a) a)
(hderiv : ∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x)
(g'neg : ∀ x ∈ Set.Ioi a, g' x ≤ 0)
(hg : Filter.Tendsto g Filter.atTop (nhds l))
:
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 ∈ Set.Ici a, HasDerivAt g (g' x) x)
(g'neg : ∀ x ∈ Set.Ioi a, g' x ≤ 0)
(hg : Filter.Tendsto g Filter.atTop (nhds l))
:
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.integral_Iic_of_hasDerivAt_of_tendsto
{E : Type u_1}
{f : ℝ → E}
{f' : ℝ → E}
{a : ℝ}
{m : E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hcont : ContinuousWithinAt f (Set.Iic a) a)
(hderiv : ∀ x ∈ Set.Iio a, HasDerivAt f (f' x) x)
(f'int : MeasureTheory.IntegrableOn f' (Set.Iic a))
(hf : Filter.Tendsto f Filter.atBot (nhds 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⁻.
theorem
MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto'
{E : Type u_1}
{f : ℝ → E}
{f' : ℝ → E}
{a : ℝ}
{m : E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hderiv : ∀ x ∈ Set.Iic a, HasDerivAt f (f' x) x)
(f'int : MeasureTheory.IntegrableOn f' (Set.Iic a))
(hf : Filter.Tendsto f Filter.atBot (nhds 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].
theorem
HasCompactSupport.integral_Iic_deriv_eq
{E : Type u_1}
{f : ℝ → E}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(hf : ContDiff ℝ 1 f)
(h2f : HasCompactSupport 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_comp_smul_deriv_Ioi
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ → ℝ}
{f' : ℝ → ℝ}
{g : ℝ → E}
{a : ℝ}
(hf : ContinuousOn f (Set.Ici a))
(hft : Filter.Tendsto f Filter.atTop Filter.atTop)
(hff' : ∀ x ∈ Set.Ioi a, HasDerivWithinAt f (f' x) (Set.Ioi x) x)
(hg_cont : ContinuousOn g (f '' Set.Ioi a))
(hg1 : MeasureTheory.IntegrableOn g (f '' Set.Ici a))
(hg2 : MeasureTheory.IntegrableOn (fun (x : ℝ) => f' x • (g ∘ f) x) (Set.Ici a))
:
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 (Set.Ici a))
(hft : Filter.Tendsto f Filter.atTop Filter.atTop)
(hff' : ∀ x ∈ Set.Ioi a, HasDerivWithinAt f (f' x) (Set.Ioi x) x)
(hg_cont : ContinuousOn g (f '' Set.Ioi a))
(hg1 : MeasureTheory.IntegrableOn g (f '' Set.Ici a))
(hg2 : MeasureTheory.IntegrableOn (fun (x : ℝ) => (g ∘ f) x * f' x) (Set.Ici a))
:
Change-of-variables formula for Ioi integrals of scalar-valued functions
theorem
MeasureTheory.integrableOn_Ioi_comp_rpow_iff
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(f : ℝ → E)
{p : ℝ}
(hp : p ≠ 0)
:
The substitution y = x ^ p in integrals over Ioi 0 preserves integrability.
theorem
MeasureTheory.integrableOn_Ioi_comp_rpow_iff'
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(f : ℝ → E)
{p : ℝ}
(hp : p ≠ 0)
:
MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ (p - 1) • f (x ^ p)) (Set.Ioi 0) ↔ MeasureTheory.IntegrableOn f (Set.Ioi 0)
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}
[NormedAddCommGroup E]
(f : ℝ → E)
(c : ℝ)
{a : ℝ}
(ha : 0 < a)
:
MeasureTheory.IntegrableOn (fun (x : ℝ) => f (a * x)) (Set.Ioi c) ↔ MeasureTheory.IntegrableOn f (Set.Ioi (a * c))
theorem
MeasureTheory.integrableOn_Ioi_comp_mul_right_iff
{E : Type u_1}
[NormedAddCommGroup E]
(f : ℝ → E)
(c : ℝ)
{a : ℝ}
(ha : 0 < a)
:
MeasureTheory.IntegrableOn (fun (x : ℝ) => f (x * a)) (Set.Ioi c) ↔ MeasureTheory.IntegrableOn f (Set.Ioi (c * a))