Specific results about ContinuousMapZero
-valued integration #
In this file, we collect a few results regarding integrability, on a measure space (X, μ)
,
of a C(Y, E)₀
-valued function, where Y
is a compact topological space with a distinguished 0
,
and E
is a normed group.
The structure of this file is largely similar to that of
Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
, which contains a more detailed
module docstring.
A natural criterion for HasFiniteIntegral
of a C(Y, E)₀
-valued function is the existence
of some positive function with finite integral such that ∀ᵐ x ∂μ, ∀ y : Y, ‖f x y‖ ≤ bound x
.
Note that there is no dominated convergence here (hence no first-countability assumption
on Y
). We are just using the properties of Banach-space-valued integration.
A variant of ContinuousMapZero.hasFiniteIntegral_of_bound
spelled in terms of
ContinuousMapZero.mkD
.
A variant of ContinuousMapZero.hasFiniteIntegral_mkD_of_bound
for a family of
functions which are continuous on a compact set.