isProbabilityMeasure_paretoMeasure

English

For ht > 0 and hr > 0, paretoMeasure t r is a probability measure with total mass 1.

Русский

При ht>0 и hr>0 мера Парето имеет единичную массу на всей шкале.

LaTeX

$$$\\text{IsProbabilityMeasure}(\\mathrm{paretoMeasure}(t,r))$$$

Lean4

theorem isProbabilityMeasure_paretoMeasure (ht : 0 < t) (hr : 0 < r) : IsProbabilityMeasure (paretoMeasure t r) where
  measure_univ := by simp [paretoMeasure, lintegral_paretoPDF_eq_one ht hr]

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