Order statistics of independent, non-identically distributed variables

For independent real coordinates with distribution functions Fᵢ, the number of coordinates at most t has Poisson-binomial success probabilities Fᵢ(t). The order statistic at position k, counted from zero, is at most t exactly when this count exceeds k. Thus its cdf is a Poisson-binomial tail, equivalently a finite sum over success sets of cardinality greater than k. These formulas retain repeated values and atoms, and allow probabilities zero and one.

References

• H. A. David and H. N. Nagaraja, Order Statistics, 3rd ed., Wiley, 2003, Chapter 5 (order statistics from independent non-identically distributed variables).

theorem TauCeti.Probability.cdf_map_orderStatistic_pi_eq_poissonBinomial {n : ℕ} (μ : Fin n → MeasureTheory.Measure ℝ) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (k : Fin n) (t : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (orderStatistic k) (MeasureTheory.Measure.pi μ))) t = (poissonBinomialMeasure fun (i : Fin n) => ⟨↑(ProbabilityTheory.cdf (μ i)) t, ⋯⟩).real (Set.Ioi ↑k)

The cdf of an order statistic of independent real coordinates is the tail of the Poisson-binomial count with success probabilities equal to their cdfs at the threshold. No continuity or identical-distribution hypothesis is needed.

theorem TauCeti.Probability.cdf_map_orderStatistic_pi_eq_sum {n : ℕ} (μ : Fin n → MeasureTheory.Measure ℝ) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (k : Fin n) (t : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (orderStatistic k) (MeasureTheory.Measure.pi μ))) t = ∑ s : Finset (Fin n) with ↑k < s.card, ↑(poissonBinomialWeight (fun (i : Fin n) => ⟨↑(ProbabilityTheory.cdf (μ i)) t, ⋯⟩) s)

The cdf of an order statistic is the sum of the probabilities of success sets with more than k coordinates at most the threshold. The success-set weights use the individual cdfs.

theorem TauCeti.Probability.measureReal_setOf_orderStatistic_le_indep {n : ℕ} (μ : Fin n → MeasureTheory.Measure ℝ) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Fin n → Ω → ℝ} (hindep : ProbabilityTheory.iIndepFun X P) (hX : ∀ (i : Fin n), ProbabilityTheory.HasLaw (X i) (μ i) P) (k : Fin n) (t : ℝ) : P.real {ω : Ω | (orderStatistic k fun (i : Fin n) => X i ω) ≤ t} = (poissonBinomialMeasure fun (i : Fin n) => ⟨↑(ProbabilityTheory.cdf (μ i)) t, ⋯⟩).real (Set.Ioi ↑k)

For an independent family with possibly different laws, the probability that the order statistic at position k is at most t is the corresponding Poisson-binomial tail. Positions are counted from zero, and ties are included.