bernoulli_expectation

Mathlib.Probability.ProbabilityMassFunction.Integrals

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

English

The expected value of Bernoulli(p,h) is p.

Русский

Ожидание распределения Бернулли(p,h) равно p.

LaTeX

$$$ \int_{\mathsf{Bool}} \mathbf{1}_{\{\text{true}\}} \, d((\mathrm{bernoulli}(p,h)).toMeasure) = p. $$$

Lean4

theorem bernoulli_expectation {p : ℝ≥0} (h : p ≤ 1) : ∫ b, cond b 1 0 ∂((bernoulli p h).toMeasure) = p.toReal := by
  simp [integral_eq_sum]

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

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

Разделы

Аффилиация

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