Documentation

Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

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 : XContinuousMapZero Y E) (bound : X) (bound_int : MeasureTheory.HasFiniteIntegral bound μ) (bound_ge : ∀ᵐ (x : X) μ, ∀ (y : Y), (f x) y bound x) :

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 : XYE) (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 : XYE) (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) μ, ys, 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_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 : XYE) (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 : XYE) (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)