English
A measurable α → StieltjesFunction yields a measurable α → Measure ℝ when taking Stieltjes measures pointwise.
Русский
Из измеримой функции α → StieltjesFunction можно получить измеримую φ: α → Measure ℝ, взяв по точкам соответствующую Measure.
LaTeX
$$$\\forall a, f(a) \\text{ measurable} \\Rightarrow a \\mapsto (f(a)).\\mathrm{measure} \\text{ measurable}$$$
Lean4
/-- A measurable function `α → StieltjesFunction` with limits 0 at -∞ and 1 at +∞ gives a measurable
function `α → Measure ℝ` by taking `StieltjesFunction.measure` at each point. -/
theorem measurable_measure {α : Type*} {_ : MeasurableSpace α} {f : α → StieltjesFunction}
(hf : ∀ q, Measurable fun a ↦ f a q) (hf_bot : ∀ a, Tendsto (f a) atBot (𝓝 0))
(hf_top : ∀ a, Tendsto (f a) atTop (𝓝 1)) : Measurable fun a ↦ (f a).measure :=
have : ∀ a, IsProbabilityMeasure (f a).measure := fun a ↦ (f a).isProbabilityMeasure (hf_bot a) (hf_top a)
.measure_of_isPiSystem_of_isProbabilityMeasure (borel_eq_generateFrom_Iic ℝ) isPiSystem_Iic <|
by
simp_rw [forall_mem_range, StieltjesFunction.measure_Iic (f _) (hf_bot _), sub_zero]
exact fun _ ↦ (hf _).ennreal_ofReal
