binomial_one_eq_bernoulli — Mathlib

English

The binomial distribution with n = 1 is the Bernoulli distribution, i.e., binomial(p,h,1) equals Bernoulli(p,h) mapped by cond.

Русский

Биномиальное распределение при n = 1 совпадает с распределением Бернулли: binomial(p,h,1) = Bernoulli(p,h) отображено через cond.

LaTeX

$$$\\text{binomial}(p,h,1) = (\\text{bernoulli}(p,h)).map(\\text{cond} \\cdot 1 0)$$$

Lean4

/-- The binomial distribution on one coin is the Bernoulli distribution. -/
theorem binomial_one_eq_bernoulli (p : ℝ≥0) (h : p ≤ 1) : binomial p h 1 = (bernoulli p h).map (cond · 1 0) := by ext i;
  fin_cases i <;> simp [tsum_bool, binomial_apply]

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