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.

theorem ContinuousMapZero.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] [Zero Y] (f : X → ContinuousMapZero 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 ContinuousMapZero.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] [Zero Y] (f : X → Y → E) (g : ContinuousMapZero Y E) (f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)) (f_ae_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0) (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 ContinuousMapZero.hasFiniteIntegral_of_bound spelled in terms of ContinuousMapZero.mkD.

theorem ContinuousMapZero.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] [Zero ↑s] (f : X → Y → E) (g : ContinuousMapZero (↑s) E) (f_ae_contOn : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s) (f_ae_zero : ∀ᵐ (x : X) ∂μ, f x ↑0 = 0) (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 ContinuousMapZero.hasFiniteIntegral_mkD_of_bound for a family of functions which are continuous on a compact set.

theorem ContinuousMapZero.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] [Zero Y] [TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(Y, E)] (f : X → Y → E) (g : ContinuousMapZero Y E) (f_cont : Continuous (Function.uncurry f)) (f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0) : MeasureTheory.AEStronglyMeasurable (fun (x : X) => mkD (f x) g) μ

theorem ContinuousMapZero.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] [Zero Y] {s : Set X} [TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(Y, E)] (hs : MeasurableSet s) (f : X → Y → E) (g : ContinuousMapZero Y E) (f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ)) (f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0) : MeasureTheory.AEStronglyMeasurable (fun (x : X) => mkD (f x) g) (μ.restrict s)

theorem ContinuousMapZero.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] [Zero ↑t] [TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(↑t, E)] (f : X → Y → E) (g : ContinuousMapZero (↑t) E) (f_cont : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ t)) (f_zero : ∀ᵐ (x : X) ∂μ, f x ↑0 = 0) : MeasureTheory.AEStronglyMeasurable (fun (x : X) => mkD (t.restrict (f x)) g) μ

theorem ContinuousMapZero.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] [Zero ↑t] [TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(↑t, E)] (hs : MeasurableSet s) (f : X → Y → E) (g : ContinuousMapZero (↑t) E) (f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)) (f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x ↑0 = 0) : MeasureTheory.AEStronglyMeasurable (fun (x : X) => mkD (t.restrict (f x)) g) (μ.restrict s)