instIsProbabilityMeasure_stieltjesFunction

English

For every a, the Stieltjes measure associated to a is a probability measure on the real line; equivalently its total mass is 1.

Русский

Для каждого a мера Стильтьджеса, связанная с a, является вероятностной мерой на ℝ; следовательно её суммарная масса равна 1.

LaTeX

$$$\text{IsProbabilityMeasure}\big((hf.stieltjesFunction a).\text{measure}\big)$$$

Lean4

instance instIsProbabilityMeasure_stieltjesFunction (a : α) : IsProbabilityMeasure (hf.stieltjesFunction a).measure :=
  ⟨measure_stieltjesFunction_univ hf a⟩

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