English
Bernoulli(p,h) equals the two-point distribution with masses p and 1-p on true and false respectively.
Русский
Распределение Бернулли(p,h) есть двухточечное распределение с массами p и 1-p на true и false соответственно.
LaTeX
$$$ \mathrm{bernoulli}(p,h) = \mathrm{PMF.ofFintype}(\lambda b. \operatorname{if } b \text{ then } p \text{ else } 1-p) $$$
Lean4
theorem integral_eq_sum [Fintype α] (p : PMF α) (f : α → E) : ∫ a, f a ∂(p.toMeasure) = ∑ a, (p a).toReal • f a :=
by
rw [integral_fintype _ .of_finite]
congr with x
rw [measureReal_def]
congr 2
exact PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)