English
Let f be a Stieltjes function. If f has left limit 0 and right limit 1 (i.e., Tendsto f atBot (nhds 0) and Tendsto f atTop (nhds 1)), then f.measure is a probability measure.
Русский
Пусть f — функция Стильтьеса. Если слева предел равен 0, справа — 1 (то есть Tendsto f atBot (nhds 0) и Tendsto f atTop (nhds 1)), то мера f.measure является вероятностной мерой.
LaTeX
$$$\\\\forall f \\\\in \\\\text{StieltjesFunction},\\\\\\\\ \\\\left( \\\\text{Tendsto } f \\\\ atBot \\\\ (\\\\nhds 0) \\\\land \\\\text{Tendsto } f \\\\ atTop \\\\ (\\\\nhds 1) \\\\right) \\\\Rightarrow \\\\text{IsProbabilityMeasure } f.\\\\mathrm{measure}$$$
Lean4
theorem isProbabilityMeasure (hf_bot : Tendsto f atBot (𝓝 0)) (hf_top : Tendsto f atTop (𝓝 1)) :
IsProbabilityMeasure f.measure :=
⟨by simp [f.measure_univ hf_bot hf_top]⟩
