Laws of order statistics

The generic finite-tuple order-statistic API is in TauCeti.Data.Fin.Tuple.OrderStatistic. This file uses its counting characterization and measurability to reduce order-statistic laws to binomial tails. If the entries are independent with common law μ, the number of entries at most t is binomial with success probability F(t) = cdf μ t, so the k-th order statistic has cumulative distribution function

∑ j ∈ Finset.Icc (k + 1) n, n.choose j * F(t) ^ j * (1 - F(t)) ^ (n - j),

for every law μ, atoms included. By the binomial tail identity this sum is the regularized incomplete beta value I_{F(t)}(k + 1, n - k). For unit uniform entries F(t) = t on [0, 1], so the k-th order statistic of n independent unit uniforms has the beta law with parameters k + 1 and n - k.

The laws are stated for the product measure Measure.pi fun _ => μ, the law of a tuple of independent μ-distributed entries, with random-variable forms for an independent family X : Fin n → Ω → ℝ.

Main results

• TauCeti.Probability.cdf_map_orderStatistic_pi — the cumulative distribution function of an order statistic of independent entries with a common law, as a binomial tail sum, and TauCeti.Probability.cdf_map_orderStatistic_pi_eq_regularizedIncompleteBeta the same as an incomplete beta value, with the random-variable form TauCeti.Probability.measureReal_setOf_orderStatistic_le_iid;
• TauCeti.Probability.map_orderStatistic_pi_uniformMeasure — the k-th order statistic of n independent unit uniforms has the law betaMeasure (k + 1) (n - k), with the random-variable form TauCeti.Probability.hasLaw_orderStatistic_iid_uniformMeasure;
• TauCeti.Probability.map_orderStatistic_pi_eq_map_betaMeasure_quantile — the k-th order statistic of an iid sample from any real probability law μ is obtained by applying μ.quantile to a beta variable, with random-variable form TauCeti.Probability.hasLaw_orderStatistic_iid_map_betaMeasure_quantile.

References

• H. A. David and H. N. Nagaraja, Order Statistics, 3rd ed., Wiley, 2003, §2.1, for the distribution of a single order statistic and its incomplete beta form.

theorem TauCeti.Probability.cdf_map_orderStatistic_pi_eq_regularizedIncompleteBeta {n : ℕ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (k : Fin n) (t : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (orderStatistic k) (MeasureTheory.Measure.pi fun (x : Fin n) => μ))) t = regularizedIncompleteBeta (↑↑k + 1) (↑n - ↑↑k) (↑(ProbabilityTheory.cdf μ) t)

The law of an order statistic as an incomplete beta value. If the n coordinates are independent with common law μ, the k-th order statistic has cumulative distribution function I_{F(t)}(k + 1, n - k), where F = cdf μ.

theorem TauCeti.Probability.cdf_map_orderStatistic_pi {n : ℕ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (k : Fin n) (t : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (orderStatistic k) (MeasureTheory.Measure.pi fun (x : Fin n) => μ))) t = ∑ j ∈ Finset.Icc (↑k + 1) n, ↑(n.choose j) * ↑(ProbabilityTheory.cdf μ) t ^ j * (1 - ↑(ProbabilityTheory.cdf μ) t) ^ (n - j)

The law of an order statistic. If the n coordinates are independent with common law μ, the k-th order statistic (counted from 0) is at most t with probability ∑ j ∈ Finset.Icc (k + 1) n, n.choose j * F(t) ^ j * (1 - F(t)) ^ (n - j), where F = cdf μ: the probability that more than k coordinates are at most t. Atoms are allowed.

theorem TauCeti.Probability.measureReal_setOf_orderStatistic_le_iid {n : ℕ} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure ℝ} {X : Fin n → Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : Fin n), ProbabilityTheory.HasLaw (X i) μ P) (k : Fin n) (t : ℝ) : P.real {ω : Ω | (orderStatistic k fun (i : Fin n) => X i ω) ≤ t} = ∑ j ∈ Finset.Icc (↑k + 1) n, ↑(n.choose j) * ↑(ProbabilityTheory.cdf μ) t ^ j * (1 - ↑(ProbabilityTheory.cdf μ) t) ^ (n - j)

The random-variable form of TauCeti.Probability.cdf_map_orderStatistic_pi: the k-th order statistic of an independent family of n real random variables with common law μ is at most t with probability ∑ j ∈ Finset.Icc (k + 1) n, n.choose j * F(t) ^ j * (1 - F(t)) ^ (n - j), where F = cdf μ.

theorem TauCeti.Probability.map_orderStatistic_pi_uniformMeasure {n : ℕ} (k : Fin n) : MeasureTheory.Measure.map (orderStatistic k) (MeasureTheory.Measure.pi fun (x : Fin n) => uniformMeasure 0 1) = ProbabilityTheory.betaMeasure (↑↑k + 1) (↑n - ↑↑k)

Order statistics of uniform samples are beta distributed. The k-th order statistic (counted from 0) of n independent uniform variables on the unit interval has the beta law with parameters k + 1 and n - k.

theorem TauCeti.Probability.hasLaw_orderStatistic_iid_uniformMeasure {n : ℕ} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Fin n → Ω → ℝ} (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : Fin n), ProbabilityTheory.HasLaw (X i) (uniformMeasure 0 1) P) (k : Fin n) : ProbabilityTheory.HasLaw (fun (ω : Ω) => orderStatistic k fun (i : Fin n) => X i ω) (ProbabilityTheory.betaMeasure (↑↑k + 1) (↑n - ↑↑k)) P

The random-variable form of TauCeti.Probability.map_orderStatistic_pi_uniformMeasure: the k-th order statistic of an independent family of n uniform variables on the unit interval has the beta law with parameters k + 1 and n - k.

Quantile construction

theorem TauCeti.Probability.map_orderStatistic_pi_eq_map_betaMeasure_quantile {n : ℕ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (k : Fin n) : MeasureTheory.Measure.map (orderStatistic k) (MeasureTheory.Measure.pi fun (x : Fin n) => μ) = MeasureTheory.Measure.map μ.quantile (ProbabilityTheory.betaMeasure (↑↑k + 1) (↑n - ↑↑k))

Quantile construction of an order statistic. The k-th order statistic of an iid sample from a real probability law μ has the law obtained by applying μ.quantile to a beta variable with parameters k + 1 and n - k. This allows atoms and discontinuous quantiles.

theorem TauCeti.Probability.hasLaw_orderStatistic_iid_map_betaMeasure_quantile {n : ℕ} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure ℝ} {X : Fin n → Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : Fin n), ProbabilityTheory.HasLaw (X i) μ P) (k : Fin n) : ProbabilityTheory.HasLaw (fun (ω : Ω) => orderStatistic k fun (i : Fin n) => X i ω) (MeasureTheory.Measure.map μ.quantile (ProbabilityTheory.betaMeasure (↑↑k + 1) (↑n - ↑↑k))) P

The random-variable form of TauCeti.Probability.map_orderStatistic_pi_eq_map_betaMeasure_quantile: the k-th order statistic of an iid sample from μ has the beta-quantile pushforward law.