Theorems · Theorem · probability

ProbabilityTheory.map_ncard_setBernoulli_real_singleton

∀ {ι : Type u_1} [Countable ι] {u : Set ι},
  u.Finite →
    ∀ (p : ↑unitInterval) (k : ℕ),
      (MeasureTheory.Measure.map Set.ncard (ProbabilityTheory.setBernoulli u p)).real {k} =
        ↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)

Defined in

Mathlib.Probability.Distributions.SetBernoulli

Cited by

2 results in Mathlib

Foundations

Depth 289 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Countable