Counting below, and the element counted to

A finite set of numbers is enumerated in increasing order by Finset.orderEmbOfFin. An algorithm cannot enumerate; what it can do is count. This module connects the two: the position of an element in the increasing enumeration is the number of elements below it, so an algorithm finds the k-th element by looking for the one with k elements below it.

Main definitions

• Complexity.countBelow — how many elements of a set lie below a number

Main results

• Complexity.countBelow_orderEmbOfFin — counting below the i-th element gives i
• Complexity.orderEmbOfFin_eq_of_countBelow — so the count names the element
• Complexity.idxOf_eq_countP — and in a list sorted by a key, the position of an entry is the number of entries with a smaller key

def Complexity.countBelow (S : Finset ℕ) (p : ℕ) : ℕ

How many elements of S lie below p.

Equations

• Complexity.countBelow S p = {x ∈ S | x < p}.card

theorem Complexity.countBelow_orderEmbOfFin (S : Finset ℕ) {k : ℕ} (h : S.card = k) (i : Fin k) : countBelow S ((S.orderEmbOfFin h) i) = ↑i

Counting below the i-th smallest element gives i.

theorem Complexity.orderEmbOfFin_eq_of_countBelow {S : Finset ℕ} {k : ℕ} (h : S.card = k) (i : Fin k) {p : ℕ} (hp : p ∈ S) (hcount : countBelow S p = ↑i) : (S.orderEmbOfFin h) i = p

The count names the element.

theorem Complexity.countBelow_lt_countBelow {S : Finset ℕ} {j c : ℕ} (hj : j ∈ S) (hlt : j < c) : countBelow S j < countBelow S c

Counting below is strictly monotone along the set.

theorem Complexity.countBelow_lt_card {S : Finset ℕ} {c : ℕ} (hc : c ∈ S) : countBelow S c < S.card

An element's position is below the size.

Positions in a sorted list

theorem Complexity.idxOf_eq_countP {β : Type} [BEq β] [LawfulBEq β] {key : β → ℕ} {l : List β} : List.Pairwise (fun (p q : β) => key p ≤ key q) l → (∀ p ∈ l, ∀ q ∈ l, key p = key q → p = q) → ∀ {x : β}, x ∈ l → List.idxOf x l = List.countP (fun (q : β) => decide (key q < key x)) l

In a list sorted by a key, an entry's position is the number of entries with a smaller key.