Poisson binomial distribution

DefinitionBernoulli random variable#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\Omega\), let \(X : \Omega \to \mathbb{N}\) and let \(p\) be a real number. Then \(X\) is a Bernoulli random variable with parameter \(p\) under \(\mu\) when \(0 \le p \le 1\), \(X\) is \(\mu\)-almost everywhere measurable, and the pushforward of \(\mu\) along \(X\) is the Bernoulli distribution \(p\,\delta_1 + (1 - p)\,\delta_0\) on \(\mathbb{N}\), which gives mass \(p\) to \(1\), mass \(1 - p\) to \(0\) and no mass elsewhere.

def IsBernoulliRV {Ω : Type*} [MeasurableSpace Ω]
    (X : Ω → ℕ) (μ : Measure Ω) (p : ℝ) : Prop :=
  ∃ hp : p ∈ Set.Icc (0 : ℝ) 1, HasLaw X (bernoulliMeasure 1 0 ⟨p, hp⟩) μ
Used by 8
Used byDistribution of a sum of independent Bernoulli variables · Binomial distribution of a sum of i.i.d. Bernoulli variables · Law of a Bernoulli random variable · Bernoulli parameters are at most one · Tail of a sum of independent Bernoulli variables is Poisson-binomial · Probability that a Bernoulli variable equals one · Probability that a Bernoulli variable equals zero · Bernoulli parameters are nonnegative

LemmaBernoulli parameters are nonnegative#✓fully proved

If \(X\) is a Bernoulli random variable with parameter \(p\) under a measure \(\mu\), then \(0 \le p\).

lemma IsBernoulliRV.nonneg (hX : IsBernoulliRV X μ p) : 0 ≤ p
Uses 1 · Used by 4
Statement usesBernoulli random variable
Used byDistribution of a sum of independent Bernoulli variables · Law of a Bernoulli random variable · Probability that a Bernoulli variable equals one · Probability that a Bernoulli variable equals zero

LemmaBernoulli parameters are at most one#✓fully proved

If \(X\) is a Bernoulli random variable with parameter \(p\) under a measure \(\mu\), then \(p \le 1\).

lemma IsBernoulliRV.le_one (hX : IsBernoulliRV X μ p) : p ≤ 1
Uses 1 · Used by 4
Statement usesBernoulli random variable
Used byDistribution of a sum of independent Bernoulli variables · Law of a Bernoulli random variable · Probability that a Bernoulli variable equals one · Probability that a Bernoulli variable equals zero

LemmaLaw of a Bernoulli random variable#✓fully proved

If \(X : \Omega \to \mathbb{N}\) is a Bernoulli random variable with parameter \(p\) under a measure \(\mu\), then \(X\) is \(\mu\)-almost everywhere measurable and its law under \(\mu\), the pushforward of \(\mu\) along \(X\), is the Bernoulli distribution \(p\,\delta_1 + (1 - p)\,\delta_0\) on \(\mathbb{N}\).

lemma IsBernoulliRV.hasLaw (hX : IsBernoulliRV X μ p) :
    HasLaw X (bernoulliMeasure 1 0 ⟨p, hX.nonneg, hX.le_one⟩) μ
Uses 3 · Used by 2
Statement usesBernoulli random variable · Bernoulli parameters are at most one · Bernoulli parameters are nonnegative
Used byProbability that a Bernoulli variable equals one · Probability that a Bernoulli variable equals zero

LemmaProbability that a Bernoulli variable equals zero#✓fully proved

If \(X : \Omega \to \mathbb{N}\) is a Bernoulli random variable with parameter \(p\) under a measure \(\mu\), then \(\mu(\{\omega : X(\omega) = 0\}) = 1 - p\), as an extended nonnegative real.

lemma IsBernoulliRV.measure_zero (hX : IsBernoulliRV X μ p) :
    μ (X ⁻¹' {0}) = ENNReal.ofReal (1 - p)
Uses 4 · Used by 1
Statement usesBernoulli random variable
Proof usesLaw of a Bernoulli random variable · Bernoulli parameters are at most one · Bernoulli parameters are nonnegative
Used byDistribution of a sum of independent Bernoulli variables

LemmaProbability that a Bernoulli variable equals one#✓fully proved

If \(X : \Omega \to \mathbb{N}\) is a Bernoulli random variable with parameter \(p\) under a measure \(\mu\), then \(\mu(\{\omega : X(\omega) = 1\}) = p\), as an extended nonnegative real.

lemma IsBernoulliRV.measure_one (hX : IsBernoulliRV X μ p) :
    μ (X ⁻¹' {1}) = ENNReal.ofReal p
Uses 4 · Used by 1
Statement usesBernoulli random variable
Proof usesLaw of a Bernoulli random variable · Bernoulli parameters are at most one · Bernoulli parameters are nonnegative
Used byDistribution of a sum of independent Bernoulli variables

TheoremDistribution of a sum of independent Bernoulli variables#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \(m \in \mathbb{N}\), and let \(X_1, \dots, X_m : \Omega \to \mathbb{N}\) be measurable, mutually independent random variables such that each \(X_i\) is a Bernoulli random variable with real parameter \(p_i\) under \(\mu\). Then for every \(j \in \mathbb{N}\) the probability that \(X_1 + \dots + X_m = j\) equals

\[ \sum_{A \subseteq \{1, \dots, m\},\ |A| = j} \ \prod_{i \in A} p_i \prod_{i \notin A} (1 - p_i). \]

This is the Poisson binomial distribution.

theorem bernoulli_sum_pmf
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    {m : ℕ} {X : Fin m → Ω → ℕ} {p : Fin m → ℝ}
    (hBernoulli : ∀ i, IsBernoulliRV (X i) μ (p i))
    (hIndep : iIndepFun X μ)
    (hMeas : ∀ i, Measurable (X i))
    (j : ℕ) :
    (μ ((fun ω => ∑ i : Fin m, X i ω) ⁻¹' {↑j})).toReal =
      ∑ A ∈ Finset.univ.powersetCard j,
        (∏ i ∈ A, p i) * (∏ i ∈ Finset.univ \ A, (1 - p i))
Uses 5 · Used by 2
Statement usesBernoulli random variable
Proof usesBernoulli parameters are at most one · Probability that a Bernoulli variable equals one · Probability that a Bernoulli variable equals zero · Bernoulli parameters are nonnegative
Used byBinomial distribution of a sum of i.i.d. Bernoulli variables · Tail of a sum of independent Bernoulli variables is Poisson-binomial

TheoremBinomial distribution of a sum of i.i.d. Bernoulli variables#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \(m \in \mathbb{N}\), let \(p\) be a real number, and let \(X_1, \dots, X_m : \Omega \to \mathbb{N}\) be measurable, mutually independent random variables, each a Bernoulli random variable with parameter \(p\) under \(\mu\). Then for every \(j \in \mathbb{N}\) the probability that \(X_1 + \dots + X_m = j\) is \(\binom{m}{j} p^j (1 - p)^{m - j}\), where the exponent \(m - j\) is taken to be \(0\) when \(j > m\).

theorem bernoulli_sum_pmf_iid
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    {m : ℕ} {X : Fin m → Ω → ℕ} {p : ℝ}
    (hBernoulli : ∀ i, IsBernoulliRV (X i) μ p)
    (hIndep : iIndepFun X μ)
    (hMeas : ∀ i, Measurable (X i))
    (j : ℕ) :
    (μ ((fun ω => ∑ i : Fin m, X i ω) ⁻¹' {↑j})).toReal =
      (m.choose j : ℝ) * p ^ j * (1 - p) ^ (m - j)
Uses 2
Statement usesBernoulli random variable
Proof usesDistribution of a sum of independent Bernoulli variables

DefinitionPoisson-binomial mass function#✓fully proved

Poisson-binomial mass function of the number of successes among independent trials with success probabilities p : Fin m → ℝ: ∑_{A ⊆ [m], |A| = j} ∏_{i ∈ A} p i ∏_{i ∉ A} (1 - p i). A probability mass function when every p i ∈ [0, 1]; the algebraic identities below hold for all real p.

noncomputable def poissonBinomialPMF {m : ℕ} (p : Fin m → ℝ) (j : ℕ) : ℝ :=
  ∑ A ∈ (univ : Finset (Fin m)).powersetCard j, (∏ i ∈ A, p i) * ∏ i ∈ univ \ A, (1 - p i)
Used by 14
Used byBinomial tail monotonicity · Tail of a sum of independent Bernoulli variables is Poisson-binomial · First-step recurrence for the Poisson-binomial mass function · Poisson-binomial mass at zero after adding a trial · Poisson-binomial law with equal probabilities is binomial · Poisson-binomial mass vanishes above the number of trials · Nonnegativity of the Poisson-binomial mass function · Upper tail of the Poisson-binomial law · Poisson-binomial tail after adding a trial · Peeling off the lowest term of the Poisson-binomial tail · The burden-test p-value is monotone in every background rate · Poisson-binomial masses sum to one · Le Cam's inequality, finite truncations · Le Cam's inequality

DefinitionUpper tail of the Poisson-binomial law#✓fully proved

Upper tail P(S ≥ k) = ∑_{k ≤ j ≤ m} P(S = j) of the Poisson-binomial law (the mass function vanishes above m).

noncomputable def poissonBinomialTail {m : ℕ} (p : Fin m → ℝ) (k : ℕ) : ℝ :=
  ∑ j ∈ Icc k m, poissonBinomialPMF p j
Uses 1 · Used by 5
Statement usesPoisson-binomial mass function
Used byBinomial tail monotonicity · Tail of a sum of independent Bernoulli variables is Poisson-binomial · Poisson-binomial tail after adding a trial · Peeling off the lowest term of the Poisson-binomial tail · The burden-test p-value is monotone in every background rate

TheoremNonnegativity of the Poisson-binomial mass function#✓fully proved

The Poisson-binomial mass function is nonnegative for probabilities in [0, 1].

theorem poissonBinomialPMF_nonneg {m : ℕ} {p : Fin m → ℝ} (hp : ∀ i, p i ∈ Set.Icc (0 : ℝ) 1)
    (j : ℕ) :
    0 ≤ poissonBinomialPMF p j
Uses 1 · Used by 1
Statement usesPoisson-binomial mass function
Used byThe burden-test p-value is monotone in every background rate

TheoremPoisson-binomial mass vanishes above the number of trials#✓fully proved

The Poisson-binomial mass function vanishes above the number of trials.

theorem poissonBinomialPMF_eq_zero_of_lt {m : ℕ} (p : Fin m → ℝ) {j : ℕ} (hj : m < j) :
    poissonBinomialPMF p j = 0
Uses 1 · Used by 4
Statement usesPoisson-binomial mass function
Used byPoisson-binomial tail after adding a trial · Peeling off the lowest term of the Poisson-binomial tail · Poisson-binomial masses sum to one · Le Cam's inequality, finite truncations

TheoremPoisson-binomial mass at zero after adding a trial#✓fully proved

Adding a trial with probability a: no successes requires a failure of the new trial.

theorem poissonBinomialPMF_cons_zero {m : ℕ} (a : ℝ) (q : Fin m → ℝ) :
    poissonBinomialPMF (Fin.cons a q : Fin (m + 1) → ℝ) 0 = (1 - a) * poissonBinomialPMF q 0
Uses 1 · Used by 2
Statement usesPoisson-binomial mass function
Used byPoisson-binomial masses sum to one · Le Cam's inequality, finite truncations

TheoremFirst-step recurrence for the Poisson-binomial mass function#✓fully proved

Adding a trial with probability a: first-step decomposition of the mass function, P(S' = j + 1) = a P(S = j) + (1 - a) P(S = j + 1).

theorem poissonBinomialPMF_cons_succ {m : ℕ} (a : ℝ) (q : Fin m → ℝ) (j : ℕ) :
    poissonBinomialPMF (Fin.cons a q : Fin (m + 1) → ℝ) (j + 1) =
      a * poissonBinomialPMF q j + (1 - a) * poissonBinomialPMF q (j + 1)
Uses 1 · Used by 3
Statement usesPoisson-binomial mass function
Used byPoisson-binomial tail after adding a trial · Poisson-binomial masses sum to one · Le Cam's inequality, finite truncations

TheoremPoisson-binomial masses sum to one#✓fully proved

The Poisson-binomial masses sum to one (an identity for all real p; it is the expansion of ∏ ((1 - p i) + p i) = 1).

theorem sum_poissonBinomialPMF {m : ℕ} (p : Fin m → ℝ) :
    ∑ j ∈ range (m + 1), poissonBinomialPMF p j = 1
Uses 4 · Used by 2
Statement usesPoisson-binomial mass function
Proof usesFirst-step recurrence for the Poisson-binomial mass function · Poisson-binomial mass at zero after adding a trial · Poisson-binomial mass vanishes above the number of trials
Used byTail of a sum of independent Bernoulli variables is Poisson-binomial · The burden-test p-value is monotone in every background rate

TheoremPeeling off the lowest term of the Poisson-binomial tail#✓fully proved

Peeling off the lowest term of the tail: P(S ≥ k) = P(S = k) + P(S ≥ k + 1).

theorem poissonBinomialTail_eq_add {m : ℕ} (q : Fin m → ℝ) (k : ℕ) :
    poissonBinomialTail q k = poissonBinomialPMF q k + poissonBinomialTail q (k + 1)
Uses 3 · Used by 2
Statement usesPoisson-binomial mass function · Upper tail of the Poisson-binomial law
Proof usesPoisson-binomial mass vanishes above the number of trials
Used byPoisson-binomial tail after adding a trial · The burden-test p-value is monotone in every background rate

TheoremPoisson-binomial tail after adding a trial#✓fully proved

Adding a trial with probability a raises the upper tail by exactly a P(S = k): P(S' ≥ k + 1) = P(S ≥ k + 1) + a P(S = k). So the tail is affine in each trial's probability, with nonnegative slope a point mass of the remaining trials.

theorem poissonBinomialTail_cons_succ {m : ℕ} (a : ℝ) (q : Fin m → ℝ) (k : ℕ) :
    poissonBinomialTail (Fin.cons a q : Fin (m + 1) → ℝ) (k + 1) =
      poissonBinomialTail q (k + 1) + a * poissonBinomialPMF q k
Uses 5 · Used by 1
Statement usesPoisson-binomial mass function · Upper tail of the Poisson-binomial law
Proof usesFirst-step recurrence for the Poisson-binomial mass function · Poisson-binomial mass vanishes above the number of trials · Peeling off the lowest term of the Poisson-binomial tail
Used byThe burden-test p-value is monotone in every background rate

TheoremThe burden-test p-value is monotone in every background rate#✓fully proved

If p i ≤ q i for all i, with all probabilities in [0, 1], then P_p(S ≥ k) ≤ P_q(S ≥ k).

theorem poissonBinomialTail_mono {m : ℕ} {p q : Fin m → ℝ} (hp : ∀ i, p i ∈ Set.Icc (0 : ℝ) 1)
    (hq : ∀ i, q i ∈ Set.Icc (0 : ℝ) 1) (hpq : ∀ i, p i ≤ q i) (k : ℕ) :
    poissonBinomialTail p k ≤ poissonBinomialTail q k
Uses 6 · Used by 1
Statement usesUpper tail of the Poisson-binomial law
Proof usesPoisson-binomial mass function · Nonnegativity of the Poisson-binomial mass function · Poisson-binomial tail after adding a trial · Peeling off the lowest term of the Poisson-binomial tail · Poisson-binomial masses sum to one
Used byBinomial tail monotonicity

TheoremPoisson-binomial law with equal probabilities is binomial#✓fully proved

With equal probabilities the Poisson-binomial law is the binomial law.

theorem poissonBinomialPMF_const {m : ℕ} (a : ℝ) (j : ℕ) :
    poissonBinomialPMF (fun _ : Fin m => a) j = (m.choose j : ℝ) * a ^ j * (1 - a) ^ (m - j)
Uses 1 · Used by 1
Statement usesPoisson-binomial mass function
Used byBinomial tail monotonicity

TheoremBinomial tail monotonicity#✓fully proved

For 0 ≤ p ≤ q ≤ 1, ∑_{k ≤ j ≤ n} C(n, j) p^j (1 - p)^{n - j} ≤ ∑_{k ≤ j ≤ n} C(n, j) q^j (1 - q)^{n - j}.

theorem binomialTail_mono {n k : ℕ} {p q : ℝ} (hp : 0 ≤ p) (hpq : p ≤ q) (hq : q ≤ 1) :
    ∑ j ∈ Icc k n, (n.choose j : ℝ) * p ^ j * (1 - p) ^ (n - j) ≤
      ∑ j ∈ Icc k n, (n.choose j : ℝ) * q ^ j * (1 - q) ^ (n - j)
Uses 4 · Used by 1
Proof usesPoisson-binomial mass function · Poisson-binomial law with equal probabilities is binomial · Upper tail of the Poisson-binomial law · The burden-test p-value is monotone in every background rate
Used byBinomial upper tail is monotone in the success probability

TheoremBinomial upper tail is monotone in the success probability#✓fully proved

The upper tail Bin(n, p)([k, ∞)) of Mathlib's binomial law is monotone in p.

theorem binomial_real_Ici_mono (n k : ℕ) :
    Monotone fun p : unitInterval => (binomial n p).real (Set.Ici k)
Uses 1
Proof usesBinomial tail monotonicity

TheoremTail of a sum of independent Bernoulli variables is Poisson-binomial#✓fully proved

For independent Bernoulli variables X i with parameters p i, the one-sided burden p-value P(∑ X i ≥ k) is the Poisson-binomial tail.

theorem measure_le_sum_eq_poissonBinomialTail {m : ℕ}
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : Fin m → Ω → ℕ} {p : Fin m → ℝ}
    (hBernoulli : ∀ i, IsBernoulliRV (X i) μ (p i)) (hIndep : iIndepFun X μ)
    (hMeas : ∀ i, Measurable (X i)) (k : ℕ) :
    (μ {ω | k ≤ ∑ i, X i ω}).toReal = poissonBinomialTail p k
Uses 5
Statement usesBernoulli random variable · Upper tail of the Poisson-binomial law
Proof usesDistribution of a sum of independent Bernoulli variables · Poisson-binomial mass function · Poisson-binomial masses sum to one

TheoremLe Cam's inequality, finite truncations#✓fully proved

For probabilities p i ∈ [0, 1] and λ = ∑ p i, every partial sum of ∑_j |P(S = j) - e^{-λ} λ^j / j!| is at most 2 ∑ (p i)².

theorem sum_range_abs_poissonBinomialPMF_sub_poisson_le {m : ℕ} {p : Fin m → ℝ}
    (hp : ∀ i, p i ∈ Set.Icc (0 : ℝ) 1) (N : ℕ) :
    ∑ j ∈ range N, |poissonBinomialPMF p j - exp (-∑ i, p i) * (∑ i, p i) ^ j / (j ! : ℝ)| ≤
      2 * ∑ i, p i ^ 2
Uses 4 · Used by 1
Statement usesPoisson-binomial mass function
Proof usesFirst-step recurrence for the Poisson-binomial mass function · Poisson-binomial mass at zero after adding a trial · Poisson-binomial mass vanishes above the number of trials
Used byLe Cam's inequality

TheoremLe Cam's inequality#✓fully proved

Le Cam's inequality (Le Cam 1960): the series ∑_j |P(S = j) - e^{-λ} λ^j / j!| is summable and its sum is at most 2 ∑ (p i)², where λ = ∑ p i.

theorem tsum_abs_poissonBinomialPMF_sub_poisson_le {m : ℕ} {p : Fin m → ℝ}
    (hp : ∀ i, p i ∈ Set.Icc (0 : ℝ) 1) :
    Summable (fun j : ℕ =>
        |poissonBinomialPMF p j - exp (-∑ i, p i) * (∑ i, p i) ^ j / (j ! : ℝ)|) ∧
      ∑' j : ℕ, |poissonBinomialPMF p j - exp (-∑ i, p i) * (∑ i, p i) ^ j / (j ! : ℝ)| ≤
        2 * ∑ i, p i ^ 2
Uses 2
Statement usesPoisson-binomial mass function
Proof usesLe Cam's inequality, finite truncations
24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.