Documentation

Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap

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 #

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:

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 : XC(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 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 : XYE) (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 : XYE) (g : C(s, E)) (f_ae_contOn : ∀ᵐ (x : X) μ, ContinuousOn (f x) s) (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 ContinuousMap.hasFiniteIntegral_mkD_of_bound for a family of functions which are continuous on a compact set.