Counts of independent events

The number of independent coordinates belonging to prescribed measurable sets has a Poisson-binomial law. Both the coordinate laws and the sets may vary. In particular, counting real coordinates below a threshold supplies the distribution function of an order statistic without requiring identical distributions or excluding atoms.

The construction uses Mathlib's hasLaw_indicator_one_bernoulliMeasure and the independent Bernoulli-sum characterization iIndepFun.hasLaw_sum_poissonBinomialMeasure.

References

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

theorem ProbabilityTheory.iIndepFun.hasLaw_card_filter_mem {ι : Type u_1} {Ω : Type u_2} {α : ι → Type u_3} [Fintype ι] [MeasurableSpace Ω] [(i : ι) → MeasurableSpace (α i)] {P : MeasureTheory.Measure Ω} {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {X : (i : ι) → Ω → α i} (hindep : iIndepFun X P) (hX : ∀ (i : ι), HasLaw (X i) (μ i) P) {s : (i : ι) → Set (α i)} [(i : ι) → DecidablePred fun (x : α i) => x ∈ s i] (hs : ∀ (i : ι), MeasurableSet (s i)) : HasLaw (fun (ω : Ω) => {i : ι | X i ω ∈ s i}.card) (TauCeti.Probability.poissonBinomialMeasure fun (i : ι) => ⟨(μ i).real (s i), ⋯⟩) P

The number of independent coordinates belonging to their prescribed measurable sets has the Poisson-binomial law with success probabilities given by the coordinate event masses. The coordinate spaces, laws, and sets may all vary with the index.

theorem TauCeti.Probability.hasLaw_card_filter_mem_pi {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {s : (i : ι) → Set (α i)} [(i : ι) → DecidablePred fun (x : α i) => x ∈ s i] (hs : ∀ (i : ι), MeasurableSet (s i)) : ProbabilityTheory.HasLaw (fun (x : (i : ι) → α i) => {i : ι | x i ∈ s i}.card) (poissonBinomialMeasure fun (i : ι) => ⟨(μ i).real (s i), ⋯⟩) (MeasureTheory.Measure.pi μ)

Under a product of probability laws, counting coordinates in prescribed measurable sets gives the Poisson-binomial law of their event masses. Empty products give the count zero.