Strongly measurable and finitely strongly measurable functions #
A function f
is said to be strongly measurable if f
is the sequential limit of simple functions.
It is said to be finitely strongly measurable with respect to a measure μ
if the supports
of those simple functions have finite measure. We also provide almost everywhere versions of
these notions.
Almost everywhere strongly measurable functions form the largest class of functions that can be integrated using the Bochner integral.
If the target space has a second countable topology, strongly measurable and measurable are equivalent.
If the measure is sigma-finite, strongly measurable and finitely strongly measurable are equivalent.
The main property of finitely strongly measurable functions is
FinStronglyMeasurable.exists_set_sigmaFinite
: there exists a measurable set t
such that the
function is supported on t
and μ.restrict t
is sigma-finite. As a consequence, we can prove some
results for those functions as if the measure was sigma-finite.
Main definitions #
StronglyMeasurable f
:f : α → β
is the limit of a sequencefs : ℕ → SimpleFunc α β
.FinStronglyMeasurable f μ
:f : α → β
is the limit of a sequencefs : ℕ → SimpleFunc α β
such that for alln ∈ ℕ
, the measure of the support offs n
is finite.AEStronglyMeasurable f μ
:f
is almost everywhere equal to aStronglyMeasurable
function.AEFinStronglyMeasurable f μ
:f
is almost everywhere equal to aFinStronglyMeasurable
function.AEFinStronglyMeasurable.sigmaFiniteSet
: a measurable sett
such thatf =ᵐ[μ.restrict tᶜ] 0
andμ.restrict t
is sigma-finite.
Main statements #
AEFinStronglyMeasurable.exists_set_sigmaFinite
: there exists a measurable sett
such thatf =ᵐ[μ.restrict tᶜ] 0
andμ.restrict t
is sigma-finite.
We provide a solid API for strongly measurable functions, and for almost everywhere strongly measurable functions, as a basis for the Bochner integral.
References #
- Hytönen, Tuomas, Jan Van Neerven, Mark Veraar, and Lutz Weis. Analysis in Banach spaces. Springer, 2016.
A function is StronglyMeasurable
if it is the limit of simple functions.
Equations
- MeasureTheory.StronglyMeasurable f = ∃ (fs : ℕ → MeasureTheory.SimpleFunc α β), ∀ (x : α), Filter.Tendsto (fun (n : ℕ) => (fs n) x) Filter.atTop (nhds (f x))
Instances For
The notation for StronglyMeasurable giving the measurable space instance explicitly.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A function is FinStronglyMeasurable
with respect to a measure if it is the limit of simple
functions with support with finite measure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A function is AEStronglyMeasurable
with respect to a measure μ
if it is almost everywhere
equal to the limit of a sequence of simple functions.
Equations
- MeasureTheory.AEStronglyMeasurable f μ = ∃ (g : α → β), MeasureTheory.StronglyMeasurable g ∧ f =ᵐ[μ] g
Instances For
A function is AEFinStronglyMeasurable
with respect to a measure if it is almost everywhere
equal to the limit of a sequence of simple functions with support with finite measure.
Equations
- MeasureTheory.AEFinStronglyMeasurable f μ = ∃ (g : α → β), MeasureTheory.FinStronglyMeasurable g μ ∧ f =ᵐ[μ] g
Instances For
Strongly measurable functions #
A version of stronglyMeasurable_const
that assumes f x = f y
for all x, y
.
This version works for functions between empty types.
A sequence of simple functions such that
∀ x, Tendsto (fun n => hf.approx n x) atTop (𝓝 (f x))
.
That property is given by stronglyMeasurable.tendsto_approx
.
Equations
- hf.approx = Exists.choose hf
Instances For
Similar to stronglyMeasurable.approx
, but enforces that the norm of every function in the
sequence is less than c
everywhere. If ‖f x‖ ≤ c
this sequence of simple functions verifies
Tendsto (fun n => hf.approxBounded n x) atTop (𝓝 (f x))
.
Equations
Instances For
If the measure is sigma-finite, all strongly measurable functions are
FinStronglyMeasurable
.
A strongly measurable function is measurable.
A strongly measurable function is almost everywhere measurable.
In a normed vector space, the addition of a measurable function and a strongly measurable function is measurable. Note that this is not true without further second-countability assumptions for the addition of two measurable functions.
In a normed vector space, the subtraction of a measurable function and a strongly measurable function is measurable. Note that this is not true without further second-countability assumptions for the subtraction of two measurable functions.
In a normed vector space, the addition of a strongly measurable function and a measurable function is measurable. Note that this is not true without further second-countability assumptions for the addition of two measurable functions.
Big operators: ∏
and ∑
#
The range of a strongly measurable function is separable.
In a space with second countable topology, measurable implies strongly measurable.
In a space with second countable topology, strongly measurable and measurable are equivalent.
A function is strongly measurable if and only if it is measurable and has separable range.
A continuous function is strongly measurable when either the source space or the target space is second-countable.
A continuous function whose support is contained in a compact set is strongly measurable.
A continuous function with compact support is strongly measurable.
A continuous function with compact support on a product space is strongly measurable for the product sigma-algebra. The subtlety is that we do not assume that the spaces are separable, so the product of the Borel sigma algebras might not contain all open sets, but still it contains enough of them to approximate compactly supported continuous functions.
If g
is a topological embedding, then f
is strongly measurable iff g ∘ f
is.
A sequential limit of strongly measurable functions is strongly measurable.
this is slightly different from StronglyMeasurable.piecewise
. It can be used to show
StronglyMeasurable (ite (x=0) 0 1)
by
exact StronglyMeasurable.ite (measurableSet_singleton 0) stronglyMeasurable_const stronglyMeasurable_const
, but replacing StronglyMeasurable.ite
by
StronglyMeasurable.piecewise
in that example proof does not work.
If the restriction to a set s
of a σ-algebra m
is included in the restriction to s
of
another σ-algebra m₂
(hypothesis hs
), the set s
is m
measurable and a function f
supported
on s
is m
-strongly-measurable, then f
is also m₂
-strongly-measurable.
If a function f
is strongly measurable w.r.t. a sub-σ-algebra m
and the measure is σ-finite
on m
, then there exists spanning measurable sets with finite measure on which f
has bounded
norm. In particular, f
is integrable on each of those sets.
Finitely strongly measurable functions #
A sequence of simple functions such that ∀ x, Tendsto (fun n ↦ hf.approx n x) atTop (𝓝 (f x))
and ∀ n, μ (support (hf.approx n)) < ∞
. These properties are given by
FinStronglyMeasurable.tendsto_approx
and FinStronglyMeasurable.fin_support_approx
.
Equations
- hf.approx = Exists.choose hf
Instances For
A finitely strongly measurable function is strongly measurable.
A finitely strongly measurable function is measurable.
Almost everywhere strongly measurable functions #
A StronglyMeasurable
function such that f =ᵐ[μ] hf.mk f
. See lemmas
stronglyMeasurable_mk
and ae_eq_mk
.
Equations
Instances For
The composition of a continuous function and an ae strongly measurable function is ae strongly measurable.
A continuous function from α
to β
is ae strongly measurable when one of the two spaces is
second countable.
The composition of a continuous function of two variables and two ae strongly measurable functions is ae strongly measurable.
In a space with second countable topology, measurable implies ae strongly measurable.
Big operators: ∏
and ∑
#
In a space with second countable topology, measurable implies strongly measurable.
In a space with second countable topology, strongly measurable and measurable are equivalent.
A function is almost everywhere strongly measurable if and only if it is almost everywhere measurable, and up to a zero measure set its range is contained in a separable set.
An almost everywhere sequential limit of almost everywhere strongly measurable functions is almost everywhere strongly measurable.
If a sequence of almost everywhere strongly measurable functions converges almost everywhere, one can select a strongly measurable function as the almost everywhere limit.
Almost everywhere finitely strongly measurable functions #
A fin_strongly_measurable
function such that f =ᵐ[μ] hf.mk f
. See lemmas
fin_strongly_measurable_mk
and ae_eq_mk
.
Equations
Instances For
A measurable set t
such that f =ᵐ[μ.restrict tᶜ] 0
and sigma_finite (μ.restrict t)
.
Equations
- hf.sigmaFiniteSet = ⋯.choose
Instances For
Equations
- ⋯ = ⋯
In a space with second countable topology and a sigma-finite measure, FinStronglyMeasurable
and Measurable
are equivalent.
In a space with second countable topology and a sigma-finite measure, a measurable function
is FinStronglyMeasurable
.
In a space with second countable topology and a sigma-finite measure,
AEFinStronglyMeasurable
and AEMeasurable
are equivalent.
In a space with second countable topology and a sigma-finite measure,
an AEMeasurable
function is AEFinStronglyMeasurable
.