exponentialPDF_of_neg

Mathlib.Probability.Distributions.Exponential

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

English

For all r, x, if x < 0 then exponentialPDF(r, x) = 0.

Русский

Для любых r и x, если x < 0, то экспоненциальная плотность равна 0.

LaTeX

$$$ x < 0 \Rightarrow \ exponentialPDF(r, x) = 0 $$$

Lean4

theorem exponentialPDF_of_neg {r x : ℝ} (hx : x < 0) : exponentialPDF r x = 0 :=
  gammaPDF_of_neg hx

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

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

Разделы

Аффилиация

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