Set integral #
In this file we prove some properties of ∫ x in s, f x ∂μ
. Recall that this notation
is defined as ∫ x, f x ∂(μ.restrict s)
. In integral_indicator
we prove that for a measurable
function f
and a measurable set s
this definition coincides with another natural definition:
∫ x, indicator s f x ∂μ = ∫ x in s, f x ∂μ
, where indicator s f x
is equal to f x
for x ∈ s
and is zero otherwise.
Since ∫ x in s, f x ∂μ
is a notation, one can rewrite or apply any theorem about ∫ x, f x ∂μ
directly. In this file we prove some theorems about dependence of ∫ x in s, f x ∂μ
on s
, e.g.
setIntegral_union
, setIntegral_empty
, setIntegral_univ
.
We use the property IntegrableOn f s μ := Integrable f (μ.restrict s)
, defined in
MeasureTheory.IntegrableOn
. We also defined in that same file a predicate
IntegrableAtFilter (f : X → E) (l : Filter X) (μ : Measure X)
saying that f
is integrable at
some set s ∈ l
.
Finally, we prove a version of the
Fundamental theorem of calculus
for set integral, see Filter.Tendsto.integral_sub_linear_isLittleO_ae
and its corollaries.
Namely, consider a measurably generated filter l
, a measure μ
finite at this filter, and
a function f
that has a finite limit c
at l ⊓ ae μ
. Then ∫ x in s, f x ∂μ = μ s • c + o(μ s)
as s
tends to l.smallSets
, i.e. for any ε>0
there exists t ∈ l
such that
‖∫ x in s, f x ∂μ - μ s • c‖ ≤ ε * μ s
whenever s ⊆ t
. We also formulate a version of this
theorem for a locally finite measure μ
and a function f
continuous at a point a
.
Notation #
We provide the following notations for expressing the integral of a function on a set :
∫ x in s, f x ∂μ
isMeasureTheory.integral (μ.restrict s) f
∫ x in s, f x
is∫ x in s, f x ∂volume
Note that the set notations are defined in the file Mathlib/MeasureTheory/Integral/Bochner.lean
,
but we reference them here because all theorems about set integrals are in this file.
Alias of MeasureTheory.setIntegral_congr_ae₀
.
Alias of MeasureTheory.setIntegral_congr_ae
.
Alias of MeasureTheory.setIntegral_congr_fun₀
.
Alias of MeasureTheory.setIntegral_congr_fun₀
.
Alias of MeasureTheory.setIntegral_congr_fun
.
Alias of MeasureTheory.setIntegral_congr_fun
.
Alias of MeasureTheory.setIntegral_congr_set
.
Alias of MeasureTheory.setIntegral_congr_set
.
Alias of MeasureTheory.setIntegral_union
.
Alias of MeasureTheory.setIntegral_empty
.
Alias of MeasureTheory.setIntegral_univ
.
For a function f
and a measurable set s
, the integral of indicator s f
over the whole space is equal to ∫ x in s, f x ∂μ
defined as ∫ x, f x ∂(μ.restrict s)
.
Alias of MeasureTheory.setIntegral_indicator
.
Alias of MeasureTheory.ofReal_setIntegral_one_of_measure_ne_top
.
Alias of MeasureTheory.ofReal_setIntegral_one
.
Alias of MeasureTheory.setIntegral_eq_zero_of_forall_eq_zero
.
Alias of MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux
.
If a function vanishes almost everywhere on t \ s
with s ⊆ t
, then its integrals on s
and t
coincide if t
is null-measurable.
Alias of MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero
.
If a function vanishes almost everywhere on t \ s
with s ⊆ t
, then its integrals on s
and t
coincide if t
is null-measurable.
If a function vanishes on t \ s
with s ⊆ t
, then its integrals on s
and t
coincide if t
is measurable.
Alias of MeasureTheory.setIntegral_eq_of_subset_of_forall_diff_eq_zero
.
If a function vanishes on t \ s
with s ⊆ t
, then its integrals on s
and t
coincide if t
is measurable.
If a function vanishes almost everywhere on sᶜ
, then its integral on s
coincides with its integral on the whole space.
Alias of MeasureTheory.setIntegral_eq_integral_of_ae_compl_eq_zero
.
If a function vanishes almost everywhere on sᶜ
, then its integral on s
coincides with its integral on the whole space.
If a function vanishes on sᶜ
, then its integral on s
coincides with its integral on the
whole space.
Alias of MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero
.
If a function vanishes on sᶜ
, then its integral on s
coincides with its integral on the
whole space.
Alias of MeasureTheory.setIntegral_neg_eq_setIntegral_nonpos
.
Alias of MeasureTheory.setIntegral_const
.
Alias of MeasureTheory.setIntegral_map
.
Alias of MeasurableEmbedding.setIntegral_map
.
Alias of IsClosedEmbedding.setIntegral_map
.
Alias of IsClosedEmbedding.setIntegral_map
.
Alias of IsClosedEmbedding.setIntegral_map
.
Alias of IsClosedEmbedding.setIntegral_map
.
Alias of MeasureTheory.MeasurePreserving.setIntegral_preimage_emb
.
Alias of MeasureTheory.MeasurePreserving.setIntegral_image_emb
.
Alias of MeasureTheory.setIntegral_map_equiv
.
Alias of MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae
.
Alias of MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae'
.
Alias of MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae''
.
Alias of MeasureTheory.norm_setIntegral_le_of_norm_le_const
.
Alias of MeasureTheory.norm_setIntegral_le_of_norm_le_const'
.
Alias of MeasureTheory.setIntegral_eq_zero_iff_of_nonneg_ae
.
Alias of MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae
.
Alias of MeasureTheory.setIntegral_gt_gt
.
Alias of MeasureTheory.setIntegral_trim
.
Lemmas about adding and removing interval boundaries #
The primed lemmas take explicit arguments about the endpoint having zero measure, while the
unprimed ones use [NoAtoms μ]
.
Alias of MeasureTheory.setIntegral_mono_ae
.
Alias of MeasureTheory.setIntegral_mono_on
.
Alias of MeasureTheory.setIntegral_mono_on_ae
.
Alias of MeasureTheory.setIntegral_mono
.
Alias of MeasureTheory.setIntegral_mono_set
.
Alias of MeasureTheory.setIntegral_le_integral
.
Alias of MeasureTheory.setIntegral_ge_of_const_le
.
Alias of MeasureTheory.setIntegral_nonneg_of_ae
.
Alias of MeasureTheory.setIntegral_nonneg
.
Alias of MeasureTheory.setIntegral_nonneg_ae
.
Alias of MeasureTheory.setIntegral_le_nonneg
.
Alias of MeasureTheory.setIntegral_nonpos_of_ae
.
Alias of MeasureTheory.setIntegral_nonpos_ae
.
Alias of MeasureTheory.setIntegral_nonpos
.
Alias of MeasureTheory.setIntegral_nonpos_le
.
If s
is a countable family of compact sets, f
is a continuous function, and the sequence
‖f.restrict (s i)‖ * μ (s i)
is summable, then f
is integrable on the union of the s i
.
If s
is a countable family of compact sets covering X
, f
is a continuous function, and
the sequence ‖f.restrict (s i)‖ * μ (s i)
is summable, then f
is integrable.
Continuity of the set integral #
We prove that for any set s
, the function
fun f : X →₁[μ] E => ∫ x in s, f x ∂μ
is continuous.
For f : Lp E p μ
, we can define an element of Lp E p (μ.restrict s)
by
(Lp.memℒp f).restrict s).toLp f
. This map is additive.
For f : Lp E p μ
, we can define an element of Lp E p (μ.restrict s)
by
(Lp.memℒp f).restrict s).toLp f
. This map commutes with scalar multiplication.
For f : Lp E p μ
, we can define an element of Lp E p (μ.restrict s)
by
(Lp.memℒp f).restrict s).toLp f
. This map is non-expansive.
Continuous linear map sending a function of Lp F p μ
to the same function in
Lp F p (μ.restrict s)
.
Equations
- MeasureTheory.LpToLpRestrictCLM X F 𝕜 μ p s = { toFun := fun (f : ↥(MeasureTheory.Lp F p μ)) => MeasureTheory.Memℒp.toLp ↑↑f ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯
Instances For
Alias of MeasureTheory.continuous_setIntegral
.
Fundamental theorem of calculus for set integrals
Fundamental theorem of calculus for set integrals:
if μ
is a measure that is finite at a filter l
and
f
is a measurable function that has a finite limit b
at l ⊓ ae μ
, then
∫ x in s i, f x ∂μ = μ (s i) • b + o(μ (s i))
at a filter li
provided that
s i
tends to l.smallSets
along li
.
Since μ (s i)
is an ℝ≥0∞
number, we use (μ (s i)).toReal
in the actual statement.
Often there is a good formula for (μ (s i)).toReal
, so the formalization can take an optional
argument m
with this formula and a proof of (fun i => (μ (s i)).toReal) =ᶠ[li] m
. Without these
arguments, m i = (μ (s i)).toReal
is used in the output.
Fundamental theorem of calculus for set integrals, nhdsWithin
version: if μ
is a locally
finite measure and f
is an almost everywhere measurable function that is continuous at a point a
within a measurable set t
, then ∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i))
at a filter li
provided that s i
tends to (𝓝[t] a).smallSets
along li
. Since μ (s i)
is an ℝ≥0∞
number, we use (μ (s i)).toReal
in the actual statement.
Often there is a good formula for (μ (s i)).toReal
, so the formalization can take an optional
argument m
with this formula and a proof of (fun i => (μ (s i)).toReal) =ᶠ[li] m
. Without these
arguments, m i = (μ (s i)).toReal
is used in the output.
Fundamental theorem of calculus for set integrals, nhds
version: if μ
is a locally finite
measure and f
is an almost everywhere measurable function that is continuous at a point a
, then
∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i))
at li
provided that s
tends to
(𝓝 a).smallSets
along li
. Since μ (s i)
is an ℝ≥0∞
number, we use (μ (s i)).toReal
in
the actual statement.
Often there is a good formula for (μ (s i)).toReal
, so the formalization can take an optional
argument m
with this formula and a proof of (fun i => (μ (s i)).toReal) =ᶠ[li] m
. Without these
arguments, m i = (μ (s i)).toReal
is used in the output.
Fundamental theorem of calculus for set integrals, nhdsWithin
version: if μ
is a locally
finite measure, f
is continuous on a measurable set t
, and a ∈ t
, then ∫ x in (s i), f x ∂μ = μ (s i) • f a + o(μ (s i))
at li
provided that s i
tends to (𝓝[t] a).smallSets
along li
.
Since μ (s i)
is an ℝ≥0∞
number, we use (μ (s i)).toReal
in the actual statement.
Often there is a good formula for (μ (s i)).toReal
, so the formalization can take an optional
argument m
with this formula and a proof of (fun i => (μ (s i)).toReal) =ᶠ[li] m
. Without these
arguments, m i = (μ (s i)).toReal
is used in the output.
Continuous linear maps composed with integration #
The goal of this section is to prove that integration commutes with continuous linear maps.
This holds for simple functions. The general result follows from the continuity of all involved
operations on the space L¹
. Note that composition by a continuous linear map on L¹
is not just
the composition, as we are dealing with classes of functions, but it has already been defined
as ContinuousLinearMap.compLp
. We take advantage of this construction here.
Alias of ContinuousLinearMap.setIntegral_compLp
.
Alias of setIntegral_re_add_im
.
The parametric integral over a continuous function on a compact set is continuous, under mild assumptions on the topologies involved.
Consider a parameterized integral x ↦ ∫ y, L (g y) (f x y)
where L
is bilinear,
g
is locally integrable and f
is continuous and uniformly compactly supported. Then the
integral depends continuously on x
.
Consider a parameterized integral x ↦ ∫ y, f x y
where f
is continuous and uniformly
compactly supported. Then the integral depends continuously on x
.