Order statistics of finite tuples

The k-th order statistic of a tuple x : Fin n → α in a linear order is the entry in position k once the entries of x are sorted increasingly, keeping repeated values with their multiplicity. Positions are counted from 0, so position 0 holds the minimum and position Fin.last _ the maximum. The sort is Tuple.sort, and the order statistics of x are the entries of the sorted tuple x ∘ Tuple.sort x.

The order statistics are characterized by counting: orderStatistic k x ≤ t exactly when more than k entries of x are at most t. They commute with monotone maps and are measurable whenever the binary minimum and maximum operations are measurable.

Main definitions

• TauCeti.orderStatistic — the k-th order statistic of a finite tuple.

Main results

• TauCeti.orderStatistic_comp_of_monotoneOn, TauCeti.orderStatistic_comp_of_monotone — order statistics commute with maps that are monotone on the entries of the tuple;
• TauCeti.orderStatistic_le_iff, TauCeti.orderStatistic_lt_iff — the counting characterizations;
• TauCeti.orderStatistic_zero, TauCeti.orderStatistic_last — the extreme order statistics are the minimum and the maximum;
• TauCeti.measurable_orderStatistic — measurability.

def TauCeti.orderStatistic {α : Type u_1} [LinearOrder α] {n : ℕ} (k : Fin n) (x : Fin n → α) : α

The k-th order statistic of a tuple x : Fin n → α: the entry in position k once the entries of x are sorted increasingly, repeated values kept with their multiplicity. Positions are counted from 0, so orderStatistic 0 x is the least entry of x and orderStatistic (Fin.last _) x the greatest.

theorem TauCeti.orderStatistic_def {α : Type u_1} [LinearOrder α] {n : ℕ} (k : Fin n) (x : Fin n → α) : orderStatistic k x = x ((Tuple.sort x) k)

theorem TauCeti.orderStatistic_comp_of_monotoneOn {α : Type u_1} [LinearOrder α] {n : ℕ} {x : Fin n → α} {β : Type u_2} [LinearOrder β] {s : Set α} (f : α → β) (hf : MonotoneOn f s) (hx : ∀ (i : Fin n), x i ∈ s) (k : Fin n) : orderStatistic k (f ∘ x) = f (orderStatistic k x)

Applying a map that is monotone on every entry of a tuple commutes with taking an order statistic. No behavior is required away from those entries.

theorem TauCeti.orderStatistic_comp_of_monotone {α : Type u_1} [LinearOrder α] {n : ℕ} {β : Type u_2} [LinearOrder β] (f : α → β) (hf : Monotone f) (k : Fin n) (x : Fin n → α) : orderStatistic k (f ∘ x) = f (orderStatistic k x)

Applying a monotone map to every entry commutes with taking an order statistic.

@[simp]

theorem TauCeti.orderStatistic_comp_perm {α : Type u_1} [LinearOrder α] {n : ℕ} (k : Fin n) (x : Fin n → α) (σ : Equiv.Perm (Fin n)) : orderStatistic k (x ∘ ⇑σ) = orderStatistic k x

The order statistics of a tuple do not depend on the order in which its entries are listed.

@[simp]

theorem TauCeti.orderStatistic_le_iff {α : Type u_1} [LinearOrder α] {n : ℕ} (k : Fin n) (x : Fin n → α) (t : α) : orderStatistic k x ≤ t ↔ ↑k < {i : Fin n | x i ≤ t}.card

The counting characterization of order statistics. The k-th order statistic of x is at most t exactly when more than k entries of x are at most t.

@[simp]

theorem TauCeti.orderStatistic_lt_iff {α : Type u_1} [LinearOrder α] {n : ℕ} (k : Fin n) (x : Fin n → α) (t : α) : orderStatistic k x < t ↔ ↑k < {i : Fin n | x i < t}.card

The strict form of TauCeti.orderStatistic_le_iff: the k-th order statistic of x is below t exactly when more than k entries of x are below t.

@[simp]

theorem TauCeti.orderStatistic_zero {α : Type u_1} [LinearOrder α] {n : ℕ} (x : Fin (n + 1) → α) : orderStatistic 0 x = Finset.univ.inf' ⋯ x

The least order statistic is the minimum of the entries.

@[simp]

theorem TauCeti.orderStatistic_last {α : Type u_1} [LinearOrder α] {n : ℕ} (x : Fin (n + 1) → α) : orderStatistic (Fin.last n) x = Finset.univ.sup' ⋯ x

The greatest order statistic is the maximum of the entries.

theorem TauCeti.preimage_orderStatistic_Iic {α : Type u_1} [LinearOrder α] {n : ℕ} (k : Fin n) (t : α) : orderStatistic k ⁻¹' Set.Iic t = {x : Fin n → α | ↑k < {i : Fin n | x i ≤ t}.card}

The sublevel sets of an order statistic, by the counting characterization TauCeti.orderStatistic_le_iff.

theorem TauCeti.measurable_orderStatistic {α : Type u_1} [LinearOrder α] {n : ℕ} [MeasurableSpace α] [MeasurableInf₂ α] [MeasurableSup₂ α] (k : Fin n) : Measurable (orderStatistic k)

Each order statistic is a measurable function of the tuple.