Measurability of measure-valued maps #
This file supplies general-purpose measurability results for maps into the Giry measurable space of measures.
Main results #
TauCeti.MeasureTheory.measurable_sum_smul_dirac— a countable mixture of Dirac measures at fixed atoms is measurable when each weight is measurable.TauCeti.MeasureTheory.measurable_probabilityMeasure_map— pushing forward along a fixed measurable map is measurable onProbabilityMeasure.TauCeti.MeasureTheory.measurable_map_of_measurable_uncurry— pushing a fixed s-finite measure forward along a jointly measurable family of maps is measurable in the parameter.
theorem
TauCeti.MeasureTheory.measurable_sum_smul_dirac
{β : Type u_1}
{ι : Type u_2}
{α : Type u_3}
[MeasurableSpace β]
[MeasurableSpace α]
[Countable ι]
{f : β → ι → ENNReal}
{g : ι → α}
(hf : ∀ (i : ι), Measurable fun (b : β) => f b i)
:
Measurable fun (b : β) => MeasureTheory.Measure.sum fun (i : ι) => f b i • MeasureTheory.Measure.dirac (g i)
A countable mixture of Dirac measures at fixed atoms g i is measurable in the weights.
Evaluating on a measurable set turns the measure into the sum
∑' i, f b i * 1_{g i ∈ s}, and a tsum of measurable functions is measurable. The atoms are
indexed by a countable type of their own, so the ambient space α may be uncountable.
theorem
TauCeti.MeasureTheory.measurable_probabilityMeasure_map
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
(hf : Measurable f)
:
Measurable fun (P : MeasureTheory.ProbabilityMeasure α) => P.map f
Pushing a probability measure forward along a fixed measurable map is measurable for the Giry
structure that ProbabilityMeasure inherits as a subtype of Measure.
theorem
TauCeti.MeasureTheory.measurable_map_of_measurable_uncurry
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{f : α → β → γ}
(hf : Measurable (Function.uncurry f))
:
Measurable fun (a : α) => MeasureTheory.Measure.map (f a) ν
Pushing a fixed s-finite measure forward along a jointly measurable family of maps f a is
measurable in the parameter a.