The binomial distribution on Fin (n + 1) #
The binomial distribution Bin(n, p) cast into Fin (n + 1) gives each point k the mass
n.choose k * p ^ k * (1 - p) ^ (n - k): the cast is injective on the support Set.Iic n, so
the Bin(R, n, p) formulas, stated in mathlib for CharZero R, hold for the finite carrier.
Main results #
ProbabilityTheory.map_cast_binomial_fin_singleton,ProbabilityTheory.map_cast_binomial_fin_real_singleton: the mass at a point ofBin(Fin (n + 1), n, p).
[UPSTREAM] candidates for Mathlib.Probability.Distributions.Binomial.
theorem
ProbabilityTheory.map_cast_binomial_fin_singleton
(n : ℕ)
(p : ↑unitInterval)
(k : Fin (n + 1))
:
(MeasureTheory.Measure.map Nat.cast (binomial n p)) {k} = ENNReal.ofReal (↑(n.choose ↑k) * ↑p ^ ↑k * (1 - ↑p) ^ (n - ↑k))
theorem
ProbabilityTheory.map_cast_binomial_fin_real_singleton
(n : ℕ)
(p : ↑unitInterval)
(k : Fin (n + 1))
:
(MeasureTheory.Measure.map Nat.cast (binomial n p)).real {k} = ↑(n.choose ↑k) * ↑p ^ ↑k * (1 - ↑p) ^ (n - ↑k)