isProbabilityMeasure_expMeasure

Mathlib.Probability.Distributions.Exponential

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

← MathLib Explorer

English

If r > 0, then expMeasure(r) is a probability measure.

Русский

Если r > 0, то expMeasure(r) является вероятностной мерой.

LaTeX

$$$ (r > 0) \Rightarrow \mathrm{IsProbabilityMeasure}(\expMeasure(r)) $$$

Lean4

theorem isProbabilityMeasure_expMeasure {r : ℝ} (hr : 0 < r) : IsProbabilityMeasure (expMeasure r) :=
  isProbabilityMeasure_gammaMeasure zero_lt_one hr

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

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

Разделы

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

Аффилиация

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