paretoMeasure

Mathlib.Probability.Distributions.Pareto

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.paretoMeasure

English

For t>0 and r>0, the Pareto measure is a probability measure.

Русский

Для t>0 и r>0 мера Парето является вероятностной мерой.

LaTeX

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

Lean4

/-- Measure defined by the Pareto distribution. -/
noncomputable def paretoMeasure (t r : ℝ) : Measure ℝ :=
  volume.withDensity (paretoPDF t r)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru