betaPDF_eq_zero_of_one_le

Mathlib.Probability.Distributions.Beta

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

English

Let α, β ∈ ℝ and x ∈ ℝ with x ≥ 1. Then betaPDF α β x = 0.

Русский

Пусть α, β ∈ ℝ и x ∈ ℝ удовлетворяет x ≥ 1. Тогда betaPDF α β x = 0.

LaTeX

$$$\forall \alpha,\beta, x \in \mathbb{R},\ 1 \le x \Rightarrow \betaPDF(\alpha,\beta,x)=0$$$

Lean4

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

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

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

Разделы

Аффилиация

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