betaPDF_eq_zero_of_nonpos

Mathlib.Probability.Distributions.Beta

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

English

If x ≤ 0, then betaPDF(α,β,x) = 0.

Русский

Если x ≤ 0, то betaPDF(α,β,x) = 0.

LaTeX

$$$x \le 0 \Rightarrow \betaPDF(\alpha,\beta,x)=0$$$

Lean4

theorem betaPDF_eq_zero_of_nonpos {α β x : ℝ} (hx : x ≤ 0) : betaPDF α β x = 0 := by simp [betaPDF_eq, hx.not_gt]

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

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

Разделы

Аффилиация

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