bernoulli_apply

Mathlib.Probability.ProbabilityMassFunction.Constructions

URI: https://scilib.ai/kg/mathlib#PMF.bernoulli_apply

← MathLib Explorer

English

For any b ∈ Bool, bernoulli(p,h)(b) = cond b p (1-p).

Русский

Для любого b ∈ Bool верно, что bernoulli(p,h)(b) = cond(b, p, 1-p).

LaTeX

$$$ \mathrm{bernoulli}(p,h)(b) = \operatorname{cond}(b, p, 1-p) $$$

Lean4

@[simp]
theorem bernoulli_apply : bernoulli p h b = cond b p (1 - p) :=
  by
  simp only [bernoulli, ofFintype_apply]
  exact Eq.symm (Bool.apply_cond ofNNReal)

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

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

Разделы

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

Аффилиация

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