Finite quantiles with ties

For any proportion between zero and one, a nonempty finite collection of ordered scores has a pivot whose weak lower and upper level sets contain the corresponding proportions. Equal scores belong to both level sets; no injectivity or tie-breaking assumption is required.

Main results

• Finset.exists_quantile: select a pivot retaining the requested proportions on both sides.
• Finset.exists_median: select a median pivot with at least half of the elements on each side.
• Fintype.exists_forall_card_filter_le_card_filter: some value of a function on a finite type is taken at least as often as any other.

References

• [Threshold Circuits as Decision Trees and Finite-State Programs, Lemma 2.1] [26]

theorem Finset.exists_quantile {α : Type u_1} {β : Type u_2} [LinearOrder β] (s : Finset α) (hs : s.Nonempty) (score : α → β) {a : ℝ} (ha : 0 ≤ a) (ha₁ : a ≤ 1) : ∃ p ∈ s, a * ↑s.card ≤ ↑{x ∈ s | score x ≤ score p}.card ∧ (1 - a) * ↑s.card ≤ ↑{x ∈ s | score p ≤ score x}.card

A finite score collection has a quantile with large weak level sets on both sides. The pivot itself is retained on both sides, so the statement includes tied scores.

theorem Finset.exists_median {α : Type u_1} {β : Type u_2} [LinearOrder β] (s : Finset α) (hs : s.Nonempty) (score : α → β) : ∃ p ∈ s, s.card ≤ 2 * {x ∈ s | score x ≤ score p}.card ∧ s.card ≤ 2 * {x ∈ s | score p ≤ score x}.card

Every nonempty finite set s equipped with a linearly ordered score score : α → β has a median element p ∈ s with at least half of s weakly below score p and at least half weakly above score p.

theorem Fintype.exists_forall_card_filter_le_card_filter {ι : Type u_3} {α : Type u_4} [Fintype ι] [Nonempty α] [DecidableEq α] (f : ι → α) : ∃ (a : α), ∀ (b : α), {i : ι | f i = b}.card ≤ {i : ι | f i = a}.card

Plurality: some value of a function on a finite type is taken at least as often as any other.