The Poisson-binomial distribution

The Poisson-binomial distribution is the law of a finite sum of independent Bernoulli variables whose success probabilities need not agree. This file defines the law by its subset weights and proves the mass formula, normalization, probability-generating function, independent-sum characterization, and the recursion obtained by adjoining one Bernoulli trial.

These results provide the count law used for order statistics of independent, non-identically distributed real random variables.

Main results

• poissonBinomialMeasure is the native law on ℕ;
• poissonBinomialMeasure_singleton gives its singleton masses as a sum over subsets;
• integral_poissonBinomialMeasure writes integration as a finite sum over success sets;
• poissonBinomialMeasure_singleton_ne_zero_iff identifies the exact interval of possible counts;
• pgf_poissonBinomialMeasure gives its probability-generating function;
• iIndepFun.hasLaw_sum_poissonBinomialMeasure identifies independent Bernoulli sums;
• map_sum_pi_bernoulliMeasure gives the corresponding product-measure pushforward;
• map_sum_natCast_pi_bernoulliMeasure gives its real-cast form;
• poissonBinomialMeasure_eq_conv_bernoulliMeasure gives the adjoining-one-trial recursion;
• poissonBinomialMeasure_const recovers the binomial distribution.

References

• Y. H. Wang, “On the number of successes in independent trials”, Statistica Sinica 3 (1993), 295–312.

noncomputable def TauCeti.Probability.poissonBinomialWeight {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) (s : Finset ι) : NNReal

The probability of the success set s for independent Bernoulli trials with success probabilities p.

theorem TauCeti.Probability.poissonBinomialWeight_def {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ι → ↑unitInterval) (s : Finset ι) : poissonBinomialWeight p s = (∏ i ∈ s, unitInterval.toNNReal (p i)) * ∏ i ∈ sᶜ, unitInterval.toNNReal (unitInterval.symm (p i))

The product formula for the probability of a given success set.

@[simp]

theorem TauCeti.Probability.poissonBinomialWeight_ne_zero_iff {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) (s : Finset ι) : poissonBinomialWeight p s ≠ 0 ↔ (∀ i ∈ s, p i ≠ 0) ∧ ∀ i ∉ s, p i ≠ 1

A success set has nonzero weight exactly when it contains every certain success and contains no trial whose success probability is zero.

noncomputable def TauCeti.Probability.poissonBinomialMeasure {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) : MeasureTheory.Measure ℕ

The Poisson-binomial law with success probabilities p is the weighted sum of point masses at the cardinalities of all possible success sets.

@[simp]

theorem TauCeti.Probability.sum_poissonBinomialWeight {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) : ∑ s : Finset ι, poissonBinomialWeight p s = 1

The Poisson-binomial weights sum to one.

theorem TauCeti.Probability.poissonBinomialMeasure_apply {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) (S : Set ℕ) : (poissonBinomialMeasure p) S = ∑ s : Finset ι with s.card ∈ S, ↑(poissonBinomialWeight p s)

The value of a Poisson-binomial law on a measurable set is the sum of the weights of the success sets whose cardinalities belong to it.

instance TauCeti.Probability.isProbabilityMeasure_poissonBinomialMeasure {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) : MeasureTheory.IsProbabilityMeasure (poissonBinomialMeasure p)

The Poisson-binomial law is a probability measure.

theorem TauCeti.Probability.integrable_poissonBinomialMeasure {ι : Type u_1} [Fintype ι] {E : Type u_3} [SeminormedAddGroup E] (f : ℕ → E) (p : ι → ↑unitInterval) : MeasureTheory.Integrable f (poissonBinomialMeasure p)

Every function is integrable against a Poisson-binomial law because the law has finite support.

theorem TauCeti.Probability.integral_poissonBinomialMeasure {ι : Type u_1} [Fintype ι] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : ℕ → E) (p : ι → ↑unitInterval) : ∫ (k : ℕ), f k ∂poissonBinomialMeasure p = ∑ s : Finset ι, ↑(poissonBinomialWeight p s) • f s.card

Integration against a Poisson-binomial law is a finite weighted sum over success sets.

@[simp]

theorem TauCeti.Probability.poissonBinomialMeasure_singleton {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) (k : ℕ) : (poissonBinomialMeasure p) {k} = ∑ s ∈ Finset.powersetCard k Finset.univ, ↑(poissonBinomialWeight p s)

The mass at k is the sum of the success-set weights over subsets of cardinality k.

@[simp]

theorem TauCeti.Probability.poissonBinomialMeasure_real_singleton {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) (k : ℕ) : (poissonBinomialMeasure p).real {k} = ∑ s ∈ Finset.powersetCard k Finset.univ, ↑(poissonBinomialWeight p s)

The real singleton mass of a Poisson-binomial law.

theorem TauCeti.Probability.poissonBinomialMeasure_singleton_ne_zero_iff {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) (k : ℕ) : (poissonBinomialMeasure p) {k} ≠ 0 ↔ {i : ι | p i = 1}.card ≤ k ∧ k ≤ {i : ι | p i ≠ 0}.card

The possible counts run from the number of certain successes to the number of trials with nonzero success probability, including both endpoints and every count between them.

theorem TauCeti.Probability.poissonBinomialMeasure_singleton_eq_zero {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) {k : ℕ} (hk : Fintype.card ι < k) : (poissonBinomialMeasure p) {k} = 0

A Poisson-binomial law has no mass above the number of trials.

@[simp]

theorem TauCeti.Probability.poissonBinomialMeasure_Iic_card {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) : (poissonBinomialMeasure p) (Set.Iic (Fintype.card ι)) = 1

A Poisson-binomial count is at most the number of trials almost surely.

@[simp]

theorem TauCeti.Probability.pgf_poissonBinomialMeasure {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) (z : ℝ) : pgf id (poissonBinomialMeasure p) z = ∏ i : ι, (1 - ↑(p i) + ↑(p i) * z)

The probability-generating function of a Poisson-binomial law is the product of the Bernoulli probability-generating functions.

theorem ProbabilityTheory.iIndepFun.hasLaw_sum_poissonBinomialMeasure {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℕ} {p : ι → ↑unitInterval} (hindep : iIndepFun X P) (hX : ∀ (i : ι), HasLaw (X i) (bernoulliMeasure 1 0 (p i)) P) : HasLaw (fun (ω : Ω) => ∑ i : ι, X i ω) (TauCeti.Probability.poissonBinomialMeasure p) P

A finite sum of independent Bernoulli variables has the Poisson-binomial law with the corresponding success probabilities.

theorem TauCeti.Probability.map_sum_pi_bernoulliMeasure {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) : MeasureTheory.Measure.map (fun (x : ι → ℕ) => ∑ i : ι, x i) (MeasureTheory.Measure.pi fun (i : ι) => ProbabilityTheory.bernoulliMeasure 1 0 (p i)) = poissonBinomialMeasure p

Pushing the product of Bernoulli laws forward by coordinate sum gives the Poisson-binomial law.

theorem TauCeti.Probability.map_sum_natCast_pi_bernoulliMeasure {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) : MeasureTheory.Measure.map (fun (x : ι → ℕ) => ∑ i : ι, ↑(x i)) (MeasureTheory.Measure.pi fun (i : ι) => ProbabilityTheory.bernoulliMeasure 1 0 (p i)) = MeasureTheory.Measure.map Nat.cast (poissonBinomialMeasure p)

Pushing the product of native Bernoulli laws forward by the sum of the real-cast coordinates gives the real cast of the Poisson-binomial law.

@[simp]

theorem TauCeti.Probability.poissonBinomialMeasure_of_isEmpty {ι : Type u_1} [Fintype ι] [IsEmpty ι] (p : ι → ↑unitInterval) : poissonBinomialMeasure p = MeasureTheory.Measure.dirac 0

The Poisson-binomial law of an empty family is the point mass at zero.

@[simp]

theorem TauCeti.Probability.poissonBinomialMeasure_const {ι : Type u_1} [Fintype ι] (p : ↑unitInterval) : (poissonBinomialMeasure fun (x : ι) => p) = ProbabilityTheory.binomial (Fintype.card ι) p

Equal success probabilities recover the ordinary binomial distribution.

theorem TauCeti.Probability.poissonBinomialMeasure_eq_conv_bernoulliMeasure {ι : Type u_1} [Fintype ι] [DecidableEq ι] (j : ι) (p : ι → ↑unitInterval) : poissonBinomialMeasure p = (poissonBinomialMeasure fun (i : { i : ι // i ≠ j }) => p ↑i).conv (ProbabilityTheory.bernoulliMeasure 1 0 (p j))

Adjoining one trial convolves the previous Poisson-binomial law with its Bernoulli law.

theorem TauCeti.Probability.poissonBinomialMeasure_eq_sum {ι : Type u_1} [Fintype ι] (p : ι → ↑unitInterval) : poissonBinomialMeasure p = MeasureTheory.Measure.sum fun (s : Finset ι) => ↑(poissonBinomialWeight p s) • MeasureTheory.Measure.dirac s.card

The finite weighted sum defining a Poisson-binomial law, written as a countable measure sum.

theorem TauCeti.Probability.measurable_poissonBinomialWeight {ι : Type u_1} [Fintype ι] (s : Finset ι) : Measurable fun (p : ι → ↑unitInterval) => poissonBinomialWeight p s

The success-set weight is measurable in the vector of success probabilities.

theorem TauCeti.Probability.measurable_poissonBinomialMeasure {ι : Type u_1} [Fintype ι] : Measurable fun (p : ι → ↑unitInterval) => poissonBinomialMeasure p

The Poisson-binomial family is measurable in its finite vector of success probabilities.