isProbabilityMeasure_gammaMeasure

Mathlib.Probability.Distributions.Gamma

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

← MathLib Explorer

English

For a > 0 and r > 0, gammaMeasure(a, r) is a probability measure.

Русский

Для a > 0 и r > 0 гамма-мера gammaMeasure(a, r) является вероятностной мерой.

LaTeX

$$$\text{IsProbabilityMeasure}(\gammaMeasure(a,r))$$$

Lean4

theorem isProbabilityMeasure_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : IsProbabilityMeasure (gammaMeasure a r)
    where measure_univ := by simp [gammaMeasure, lintegral_gammaPDF_eq_one ha hr]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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