Specific results about ContinuousMap
-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 and E
is a normed group.
These are all elementary from a mathematical point of view, but they require a bit of care in order
to be conveniently usable. In particular, to accomodate the need of families f : X → Y → E
which
such that f x
is only continuous for almost every x
, we give a variety of results about the
integrability of fun x ↦ ContinuousMap.mkD (f x) g
whose assumption only mention f
(so that
user don't have to convert between f
and fun x ↦ ContinuousMap.mkD (f x) g
by hand).
Main results #
hasFiniteIntegral_of_bound
: givenf : X → C(Y, E)
, the natural way to showHasFiniteIntegral f
is to give abound : X → ℝ
, which itself has finite integral, and such that∀ᵐ x ∂μ, ∀ y : Y, ‖f x y‖ ≤ bound x
.hasFiniteIntegral_mkD_of_bound
is themkD
analog of the above: givenf : X → Y → E
such thatf x
is continuous for almost everyx
, as well as a bound as above, we proveHasFiniteIntegral (fun x ↦ mkD (f x) g)
. Note that, conveniently,mkD
only appears in the result.aeStronglyMeasurable_mkD_of_uncurry
: if nowX
is a topological space with the borel σ-algebra, andf : X → Y → E
is continuous onX × Y
, thenfun x ↦ mkD (f x) g
isAEStronglyMeasurable
. Note that this is far from optimal: this function is in fact continuous, and one could avoidmkD
entirely sincef x
is always continuous in that case. Nevertheless, this turns out to be most convenient, as we explain below.
Implementation Note #
We claim that using "constructors with default values" such as ContinuousMap.mkD
is the right way
to approach integration valued in a functional space ℱ
. More precisely:
- if you happen to start from a bundled
f : X → ℱ
function, you should be able to use the general theory without any issues. - if instead you start with a family of bare functions
f : X → Y → E
, to integrate it inℱ
, you should always consider the familyfun x ↦ ℱ.mkD (f x) 0
, even if yourf
always lands inℱ
. This allows for a unified setting with the case wheref x
belongs toℱ
for almost everyx
, and also avoids entering dependent-types hell.
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 ContinuousMap.hasFiniteIntegral_of_bound
spelled in terms of
ContinuousMap.mkD
.
A variant of ContinuousMap.hasFiniteIntegral_mkD_of_bound
for a family of
functions which are continuous on a compact set.