Theorems · Theorem · probability

ProbabilityTheory.map_cast_binomial_singleton

∀ {R : Type u_1} [inst : MeasurableSpace R] [inst_1 : AddMonoidWithOne R] [MeasurableSingletonClass R] [CharZero R]
  (n k : ℕ) (p : ↑unitInterval),
  (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p)) {↑k} =
    ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k))

Defined in

Mathlib.Probability.Distributions.Binomial

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceAddMonoidWithOneMeasurableSingletonClassCharZero