instIsProbabilityMeasure_stieltjesOfMeasurableRat

English

For each a, the measure associated to the Stieltjes function is a probability measure.

Русский

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

LaTeX

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

Lean4

instance instIsProbabilityMeasure_stieltjesOfMeasurableRat (hf : Measurable f) (a : α) :
    IsProbabilityMeasure (stieltjesOfMeasurableRat f hf a).measure :=
  IsMeasurableRatCDF.instIsProbabilityMeasure_stieltjesFunction _ _

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