bernoulli — Mathlib

English

Define a Bernoulli distribution on Bool with parameter p: it assigns probability p to true and 1-p to false, provided p ≤ 1.

Русский

Определим распределение Бернулли на булевом множестве с параметром p: вероятность true равна p, а вероятность false равна 1-p (при p ≤ 1).

LaTeX

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

Lean4

/-- A `PMF` which assigns probability `p` to `true` and `1 - p` to `false`. -/
def bernoulli (p : ℝ≥0) (h : p ≤ 1) : PMF Bool :=
  ofFintype (fun b => cond b p (1 - p)) (by simp [h])

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