Documentation

Mathlib.Probability.Distributions.Binomial

Binomial random variables #

This file defines the binomial distribution and binomial random variables, and computes their expectation and variance.

Main definitions #

Notation #

Bin(n, p) is the binomial distribution with parameters n and p in ℕ. Bin(R, n, p) is the binomial distribution with parameters n and p in R.

source
🔸 coverage
noncomputable def ProbabilityTheory.binomial (n : ℕ) (p : ↑unitInterval) :
MeasureTheory.Measure ℕ

The binomial probability distribution with parameter p.

Instances For
    source
    🔸 coverage
    def ProbabilityTheory.«termBin(_,_)» :
    Lean.ParserDescr

    The binomial probability distribution with parameter p.

    Instances For
      source
      🔸 coverage
      def ProbabilityTheory.«termBin(_,_,_)» :
      Lean.ParserDescr

      The binomial probability distribution with parameter p valued in the semiring R.

      Instances For
        source
        📐 coverage
        instance ProbabilityTheory.isProbabilityMeasure_binomial {n : ℕ} {p : ↑unitInterval} :
        MeasureTheory.IsProbabilityMeasure (binomial n p)
        source
        📐 coverage
        theorem ProbabilityTheory.ae_le_of_hasLaw_binomial {Ω : Type u_2} {m : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {n : ℕ} {p : ↑unitInterval} {X : Ω → ℕ} (hX : HasLaw X (binomial n p) P) :
        ∀ᵐ (ω : Ω) ∂P, X ω ≤ n

        Binomial random variables #