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)
:
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)