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 accommodate 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: given f : X → C(Y, E), the natural way to show HasFiniteIntegral f is to give a bound : X → ℝ, which itself has finite integral, and such that ∀ᵐ x ∂μ, ∀ y : Y, ‖f x y‖ ≤ bound x.
• hasFiniteIntegral_mkD_of_bound is the mkD analog of the above: given f : X → Y → E such that f x is continuous for almost every x, as well as a bound as above, we prove HasFiniteIntegral (fun x ↦ mkD (f x) g). Note that, conveniently, mkD only appears in the result.
• aeStronglyMeasurable_mkD_of_uncurry: if now X is a topological space with the Borel σ-algebra, and f : X → Y → E is continuous on X × Y, then fun x ↦ mkD (f x) g is AEStronglyMeasurable. Note that this is far from optimal: this function is in fact continuous, and one could avoid mkD entirely since f 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 family fun x ↦ ℱ.mkD (f x) 0, even if your f always lands in ℱ. This allows for a unified setting with the case where f x belongs to ℱ for almost every x, and also avoids entering dependent-types hell.

theorem ContinuousMap.hasFiniteIntegral_of_bound {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [TopologicalSpace Y] {E : Type u_3} [NormedAddCommGroup E] [CompactSpace Y] (f : X → C(Y, E)) (bound : X → ℝ) (bound_int : MeasureTheory.HasFiniteIntegral bound μ) (bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x) : MeasureTheory.HasFiniteIntegral f μ

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.

theorem ContinuousMap.hasFiniteIntegral_mkD_of_bound {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [TopologicalSpace Y] {E : Type u_3} [NormedAddCommGroup E] [CompactSpace Y] (f : X → Y → E) (g : C(Y, E)) (f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)) (bound : X → ℝ) (bound_int : MeasureTheory.HasFiniteIntegral bound μ) (bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x) : MeasureTheory.HasFiniteIntegral (fun (x : X) => mkD (f x) g) μ

A variant of ContinuousMap.hasFiniteIntegral_of_bound spelled in terms of ContinuousMap.mkD.

theorem ContinuousMap.hasFiniteIntegral_mkD_restrict_of_bound {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [TopologicalSpace Y] {E : Type u_3} [NormedAddCommGroup E] {s : Set Y} [CompactSpace ↑s] (f : X → Y → E) (g : C(↑s, E)) (f_ae_contOn : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s) (bound : X → ℝ) (bound_int : MeasureTheory.HasFiniteIntegral bound μ) (bound_ge : ∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x) : MeasureTheory.HasFiniteIntegral (fun (x : X) => mkD (s.restrict (f x)) g) μ

A variant of ContinuousMap.hasFiniteIntegral_mkD_of_bound for a family of functions which are continuous on a compact set.

theorem ContinuousMap.aeStronglyMeasurable_mkD_of_uncurry {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [TopologicalSpace Y] {E : Type u_3} [NormedAddCommGroup E] [CompactSpace Y] [TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(Y, E)] (f : X → Y → E) (g : C(Y, E)) (f_cont : Continuous (Function.uncurry f)) : MeasureTheory.AEStronglyMeasurable (fun (x : X) => mkD (f x) g) μ

theorem ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [TopologicalSpace Y] {E : Type u_3} [NormedAddCommGroup E] [CompactSpace Y] {s : Set X} [TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(Y, E)] (hs : MeasurableSet s) (f : X → Y → E) (g : C(Y, E)) (f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ)) : MeasureTheory.AEStronglyMeasurable (fun (x : X) => mkD (f x) g) (μ.restrict s)

theorem ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [TopologicalSpace Y] {E : Type u_3} [NormedAddCommGroup E] {t : Set Y} [CompactSpace ↑t] [TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(↑t, E)] (f : X → Y → E) (g : C(↑t, E)) (f_cont : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ t)) : MeasureTheory.AEStronglyMeasurable (fun (x : X) => mkD (t.restrict (f x)) g) μ

theorem ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [TopologicalSpace Y] {E : Type u_3} [NormedAddCommGroup E] {s : Set X} {t : Set Y} [CompactSpace ↑t] [TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(↑t, E)] (hs : MeasurableSet s) (f : X → Y → E) (g : C(↑t, E)) (f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)) : MeasureTheory.AEStronglyMeasurable (fun (x : X) => mkD (t.restrict (f x)) g) (μ.restrict s)