English
Let f be a Stieltjes function. If f has finite left and right limits l,u (i.e., Tendsto f atBot (nhds l) and Tendsto f atTop (nhds u)) then the associated measure f.measure is finite.
Русский
Пусть f — функция Стильтьеса. Если слева и справа существуют конечные пределы l и u (то есть Tendsto f atBot (nhds l) и Tendsto f atTop (nhds u)), то связанная мера f.measure конечна.
LaTeX
$$$\\\\forall f \\\\in \\\\text{StieltjesFunction},\\\\\\\\ \\\\exists l,u \in \\\\mathbb{R}, \\\\left( \\\\text{Tendsto } f \\\\ atBot \\\\ (\\\\nhds l) \\\\\\land \\\\text{Tendsto } f \\\\ atTop \\\\ (\\\\nhds u) \\\\right) \\\\Rightarrow \\\\text{IsFiniteMeasure } f.\\\\mathrm{measure}$$$
Lean4
theorem isFiniteMeasure {l u : ℝ} (hfl : Tendsto f atBot (𝓝 l)) (hfu : Tendsto f atTop (𝓝 u)) :
IsFiniteMeasure f.measure :=
⟨by simp [f.measure_univ hfl hfu]⟩
