measure_stieltjesFunction_univ — Mathlib

English

Let f be a measurable function valued in rationals, and for each a the Stieltjes measure associated to f at a is a probability measure on the real line. In particular, the total mass of the measure is 1: the measure of the whole space is 1.

Русский

Пусть f — измеримая функция, принимающая значения в рациональных числах; для каждого a, мера Стильтьджеса, связанная с f в точке a, является вероятностной мерой на множествах действительных чисел. В частности, сумма масс по всей области равна 1: μ_a(ℝ) = 1.

LaTeX

$$$\big( hf.stieltjesFunction(a)\big).\text{measure}(\mathbb{R}) = 1$$$

Lean4

theorem measure_stieltjesFunction_univ (a : α) : (hf.stieltjesFunction a).measure univ = 1 :=
  by
  rw [← ENNReal.ofReal_one, ← sub_zero (1 : ℝ)]
  exact StieltjesFunction.measure_univ _ (tendsto_stieltjesFunction_atBot hf a) (tendsto_stieltjesFunction_atTop hf a)

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