measure_univ_of_tendsto_atBot_atBot

English

Let f be a Stieltjes function. If f tends to the bottom value along the left end (i.e., Tendsto f atBot atBot), then the total mass of the associated measure is infinite: f.measure(univ) = ∞.

Русский

Пусть f — функция Стильтьеса. Если в левой части она стремится к нижнему пределу (Tendsto f atBot atBot), то общая масса связанной меры бесконечна: f.measure(univ) = ∞.

LaTeX

$$$\\\\forall f \\\\\\,\\\\ (\\\\text{Tendsto } f \\\\ atBot \\\\ (\\\\nhds \\\\ univ)) \\\\Rightarrow f.\\\\mathrm{measure} \\\\ univ = \\\\infty$$$

Lean4

theorem measure_univ_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) : f.measure univ = ∞ :=
  by
  rw [← top_le_iff, ← f.measure_Iio_of_tendsto_atBot_atBot hf 0]
  exact measure_mono (subset_univ _)

Похожие утверждения