Median of medians

DefinitionGroup medians for median-of-medians selection#✓fully proved

Given a list \(xs\) over a linear order, split \(xs\) into consecutive blocks of five elements, the last of which may be shorter. Sort each block \(g\) by insertion sort and return, in block order, the entry at position \(\lfloor (|g| - 1)/2 \rfloor\) (counting from \(0\)) of each sorted block, that is, its lower median. The cost is the total number of comparisons made by these insertion sorts.

def medianOfMediansGroups {α : Type u} [LinearOrder α] (xs : List α) :
    TimeM Nat (List α) :=
  let rec loop : List (List α) → TimeM Nat (List α)
    | [] => pure []
    | group :: groups => do
        let sorted ← insertionSort group
        let tail ← loop groups
        match sorted[(group.length - 1) / 2]? with
        | none => pure tail
        | some x => pure (x :: tail)
  loop (xs.toChunks 5)

Uses 1 · Used by 10

Statement usesInsertion sort with comparison cost

Used byMedian-of-medians selection · Correctness of median-of-medians selection · Out-of-range ranks cost no comparisons · Median-of-medians selection is quickselect on short lists · Median-of-medians selection succeeds on valid ranks · Group medians are lower medians of their blocks · Number of group medians · Group medians come from the input · Comparison cost of the group medians · Median of medians makes linearly many comparisons

TheoremComparison cost of the group medians#✓fully proved

For every list \(xs\) of length \(n\) over a linear order, computing the group medians of \(xs\) takes at most \(2n\) comparisons.

theorem medianOfMediansGroups_time {α : Type u} [LinearOrder α] (xs : List α) :
    (medianOfMediansGroups xs).time ≤ 2 * xs.length

Uses 4 · Used by 1

Statement usesGroup medians for median-of-medians selection

Proof usesInsertion sort with comparison cost · Comparison bound for insertion sort · Chunks of a list have length at most the chunk size

Used byMedian of medians makes linearly many comparisons

TheoremGroup medians come from the input#✓fully proved

For every list \(xs\) over a linear order, every entry of the list of group medians of \(xs\) is an element of \(xs\).

theorem medianOfMediansGroups_mem {α : Type u} [LinearOrder α] {xs : List α} {x : α}
    (hx : x ∈ (medianOfMediansGroups xs).ret) : x ∈ xs

Uses 3 · Used by 3

Statement usesGroup medians for median-of-medians selection

Proof usesInsertion sort with comparison cost · Insertion sort permutes its input

Used byCorrectness of median-of-medians selection · Median-of-medians selection succeeds on valid ranks · Median of medians makes linearly many comparisons

TheoremGroup medians are lower medians of their blocks#✓fully proved

Let \(xs\) be a list over a linear order, and let \(g_1, \dots, g_m\) be its consecutive blocks of five elements, the last of which may be shorter. Then the list of group medians of \(xs\) has the same length \(m\), say \(x_1, \dots, x_m\), and for each \(i\), writing \(k_i = \lfloor (|g_i| - 1)/2 \rfloor\) and counting elements of \(g_i\) with multiplicity: \(x_i\) belongs to \(g_i\), at most \(k_i\) elements of \(g_i\) are less than \(x_i\), and more than \(k_i\) elements of \(g_i\) are less than or equal to \(x_i\).

theorem medianOfMediansGroups_correct {α : Type u} [LinearOrder α] (xs : List α) :
    List.Forall₂ (fun group x => x ∈ group ∧
      group.countP (fun y => decide (y < x)) ≤ (group.length - 1) / 2 ∧
      (group.length - 1) / 2 < group.countP (fun y => decide (y ≤ x)))
      (xs.toChunks 5) (medianOfMediansGroups xs).ret

Uses 7 · Used by 2

Statement usesGroup medians for median-of-medians selection

Proof usesInsertion sort with comparison cost · Insertion sort permutes its input · Quickselect · Correctness of quickselect · Quickselect agrees with sorting · Cost-annotated insertion sort returns the standard insertion sort

Used byNumber of group medians · Median of medians makes linearly many comparisons

TheoremNumber of group medians#✓fully proved

For every list \(xs\) of length \(n\) over a linear order, the list of group medians of \(xs\) has exactly \(\lfloor (n + 4)/5 \rfloor = \lceil n/5 \rceil\) entries.

theorem medianOfMediansGroups_length {α : Type u} [LinearOrder α] (xs : List α) :
    (medianOfMediansGroups xs).ret.length = (xs.length + 4) / 5

Uses 2 · Used by 2

Statement usesGroup medians for median-of-medians selection

Proof usesGroup medians are lower medians of their blocks

Used byMedian-of-medians selection succeeds on valid ranks · Median of medians makes linearly many comparisons

DefinitionMedian-of-medians selection#✓fully proved

Given a list \(L\) over a linear order and a zero-based rank \(k\), median-of-medians selection returns either an element of \(L\) or nothing, charging one unit of cost per order comparison. If \(k \ge |L|\), where \(|L|\) is the length of \(L\), it returns nothing at no cost. Otherwise it runs the following recursive procedure on \((L, k)\) with a budget of \(|L|\) nested calls, returning nothing if the budget runs out. A list of length at most \(140\) is handled by deterministic quickselect at the current rank. A longer list is cut into consecutive groups of five entries, the last possibly shorter; each group is sorted by insertion sort and its lower median is kept, giving a list \(M\) of \(m\) medians. The procedure recursively selects the entry of \(M\) at rank \(\lfloor m/2 \rfloor\) as the pivot \(x\) (returning nothing if that call does), and splits the list by a three-way partition into the entries below \(x\), equal to \(x\) and above \(x\), with \(b\) entries below and \(e\) equal. If the current rank \(r\) satisfies \(r < b\) it recurses on the lower part with rank \(r\); if \(b \le r < b + e\) it returns \(x\); otherwise it recurses on the upper part with rank \(r - b - e\).

Cslib.Algorithms.Lean.TimeM.medianOfMedians · 19 lines

def medianOfMedians {α : Type u} [LinearOrder α] (xs : List α) (k : Nat) :
    TimeM Nat (Option α) :=
  let rec loop : Nat → List α → Nat → TimeM Nat (Option α)
    | 0, _, _ => pure none
    | fuel + 1, ys, rank =>
        if ys.length ≤ 140 then quickselect ys rank else do
          let medians ← medianOfMediansGroups ys
          let pivot ← loop fuel medians (medians.length / 2)
          match pivot with
          | none => pure none
          | some x => do
              let parts ← partition3 x ys
              if rank < parts.below.length then
                loop fuel parts.below rank
              else if rank < parts.below.length + parts.equal.length then
                pure (some x)
              else
                loop fuel parts.above (rank - (parts.below.length + parts.equal.length))
  if k < xs.length then loop xs.length xs k else pure none

Uses 4 · Used by 14

Statement usesThree-way partition record · Group medians for median-of-medians selection · Stable three-way partition · Quickselect

Used byCorrectness of median-of-medians selection on short lists · Comparison bound for median-of-medians selection on short lists · Correctness of median-of-medians selection · Median-of-medians selection agrees with sorting · Median-of-medians selection fails exactly on out-of-range ranks · Out-of-range ranks cost no comparisons · Median-of-medians selection is quickselect on short lists · Median-of-medians selection succeeds on valid ranks · Median of medians finds the lower median · Set rank of a median-of-medians result · Median of medians selects every one-based rank · One-based rank of a median-of-medians result · Median of medians makes linearly many comparisons · Median of medians finds the upper median

TheoremMedian-of-medians selection is quickselect on short lists#✓fully proved

For every list \(L\) of length at most \(140\) over a linearly ordered type and every natural number \(k\), median-of-medians selection of rank \(k\) in \(L\) coincides with timed quickselect of rank \(k\) in \(L\): both return the same result and are charged the same number of comparisons.

theorem medianOfMedians_eq_quickselect_of_length_le {α : Type u} [LinearOrder α]
    (xs : List α) (k : Nat) (hlen : xs.length ≤ 140) :
    medianOfMedians xs k = quickselect xs k

Uses 5 · Used by 3

Statement usesMedian-of-medians selection · Quickselect

Proof usesThree-way partition record · Group medians for median-of-medians selection · Stable three-way partition

Used byCorrectness of median-of-medians selection on short lists · Comparison bound for median-of-medians selection on short lists · Median of medians makes linearly many comparisons

TheoremOut-of-range ranks cost no comparisons#✓fully proved

For every list \(L\) over a linearly ordered type and every natural number \(k\) at least the length of \(L\), median-of-medians selection of rank \(k\) in \(L\) returns nothing and is charged zero comparisons.

theorem medianOfMedians_eq_pure_none_of_length_le_rank {α : Type u} [LinearOrder α]
    (xs : List α) (k : Nat) (hk : xs.length ≤ k) :
    medianOfMedians xs k = pure none

Uses 5 · Used by 1

Statement usesMedian-of-medians selection

Proof usesThree-way partition record · Group medians for median-of-medians selection · Stable three-way partition · Quickselect

Used byMedian-of-medians selection fails exactly on out-of-range ranks

TheoremComparison bound for median-of-medians selection on short lists#✓fully proved

For every list \(L\) of length \(n \le 140\) over a linearly ordered type and every natural number \(k\), median-of-medians selection of rank \(k\) in \(L\) is charged at most \(80n\) comparisons.

theorem medianOfMedians_base_time {α : Type u} [LinearOrder α]
    (xs : List α) (k : Nat) (hlen : xs.length ≤ 140) :
    (medianOfMedians xs k).time ≤ 80 * xs.length

Uses 4 · Used by 1

Statement usesMedian-of-medians selection

Proof usesMedian-of-medians selection is quickselect on short lists · Quickselect · Worst-case comparison bound for quickselect

Used byMedian of medians makes linearly many comparisons

TheoremCorrectness of median-of-medians selection on short lists#✓fully proved

Let \(L\) be a list of length at most \(140\) over a linearly ordered type and let \(k\) be a natural number. If median-of-medians selection of rank \(k\) in \(L\) returns an element \(x\), then \(x\) occurs in \(L\), the number of entries of \(L\) less than \(x\), counted with multiplicity, is at most \(k\), and \(k\) is less than the number of entries of \(L\) that are at most \(x\).

theorem medianOfMedians_base_correct {α : Type u} [LinearOrder α]
    {xs : List α} {k : Nat} {x : α} (hlen : xs.length ≤ 140)
    (hresult : (medianOfMedians xs k).ret = some x) :
    x ∈ xs ∧ xs.countP (fun y => decide (y < x)) ≤ k ∧
      k < xs.countP (fun y => decide (y ≤ x))

Uses 4

Statement usesMedian-of-medians selection

Proof usesMedian-of-medians selection is quickselect on short lists · Quickselect · Correctness of quickselect

TheoremCorrectness of median-of-medians selection#✓fully proved

Let \(L\) be a list over a linearly ordered type and let \(k\) be a natural number. If median-of-medians selection of rank \(k\) in \(L\) returns an element \(x\), then \(x\) occurs in \(L\), the number of entries of \(L\) less than \(x\), counted with multiplicity, is at most \(k\), and \(k\) is less than the number of entries of \(L\) that are at most \(x\).

theorem medianOfMedians_correct {α : Type u} [LinearOrder α]
    {xs : List α} {k : Nat} {x : α} (hresult : (medianOfMedians xs k).ret = some x) :
    x ∈ xs ∧ xs.countP (fun y => decide (y < x)) ≤ k ∧
      k < xs.countP (fun y => decide (y ≤ x))

Uses 12 · Used by 5

Statement usesMedian-of-medians selection

Proof usesThree-way partition record · Group medians for median-of-medians selection · Group medians come from the input · Stable three-way partition · Correctness of the stable three-way partition · Counting through the below block · Counting through the above block · Entries at most the pivot · Entries below the pivot · Quickselect · Correctness of quickselect

Used byMedian-of-medians selection agrees with sorting · Median of medians finds the lower median · Set rank of a median-of-medians result · Median of medians selects every one-based rank · Median of medians finds the upper median

TheoremMedian-of-medians selection succeeds on valid ranks#✓fully proved

For every list \(L\) over a linearly ordered type and every natural number \(k\) less than the length of \(L\), median-of-medians selection of rank \(k\) in \(L\) returns some element.

theorem medianOfMedians_exists {α : Type u} [LinearOrder α]
    (xs : List α) (k : Nat) (hk : k < xs.length) :
    ∃ x, (medianOfMedians xs k).ret = some x

Uses 16 · Used by 4

Statement usesMedian-of-medians selection

Proof usesThree-way partition record · Group medians for median-of-medians selection · Number of group medians · Group medians come from the input · Stable three-way partition · Correctness of the stable three-way partition · Counting through the below block · Counting through the above block · Entries at most the pivot · Entries below the pivot · The equal list of a three-way partition is a filter · Sizes of the three parts of a three-way partition · Quickselect · Correctness of quickselect · Quickselect fails exactly out of range

Used byMedian-of-medians selection fails exactly on out-of-range ranks · Median of medians finds the lower median · Median of medians selects every one-based rank · Median of medians finds the upper median

TheoremMedian-of-medians selection fails exactly on out-of-range ranks#✓fully proved

For every list \(L\) over a linearly ordered type and every natural number \(k\), median-of-medians selection of rank \(k\) in \(L\) returns nothing if and only if \(k\) is at least the length of \(L\).

theorem medianOfMedians_eq_none_iff {α : Type u} [LinearOrder α] (xs : List α) (k : Nat) :
    (medianOfMedians xs k).ret = none ↔ xs.length ≤ k

Uses 3 · Used by 1

Statement usesMedian-of-medians selection

Proof usesOut-of-range ranks cost no comparisons · Median-of-medians selection succeeds on valid ranks

Used byMedian-of-medians selection agrees with sorting

TheoremMedian-of-medians selection agrees with sorting#✓fully proved

For every list \(L\) over a linearly ordered type and every natural number \(k\), median-of-medians selection of rank \(k\) in \(L\) returns the entry at zero-based position \(k\) of the insertion sort of \(L\) by \(\le\) when \(k\) is less than the length of \(L\), and returns nothing otherwise.

theorem medianOfMedians_eq_getElem?_insertionSort {α : Type u} [LinearOrder α]
    (xs : List α) (k : Nat) :
    (medianOfMedians xs k).ret = (xs.insertionSort (· ≤ ·))[k]?

Uses 6

Statement usesMedian-of-medians selection

Proof usesCorrectness of median-of-medians selection · Median-of-medians selection fails exactly on out-of-range ranks · Quickselect · Quickselect agrees with sorting · Rank inequalities determine the quickselect value

TheoremSet rank of a median-of-medians result#✓fully proved

Let \(L\) be a list without repeated entries over a linear order and let \(k \in \mathbb{N}\). If median-of-medians selection on \(L\) at zero-based rank \(k\) returns an element \(x\), then the set \(\{y \in L : y \le x\}\) has exactly \(k + 1\) elements.

theorem medianOfMedians_set_rank {α : Type u} [LinearOrder α]
    {xs : List α} {k : Nat} {x : α} (hnodup : xs.Nodup)
    (hresult : (medianOfMedians xs k).ret = some x) :
    (xs.toFinset.filter (fun y => y ≤ x)).card = k + 1

Uses 7 · Used by 1

Statement usesMedian-of-medians selection

Proof usesThree-way partition record · Correctness of median-of-medians selection · Stable three-way partition · Entries at most the pivot · Entries below the pivot · The equal list of a three-way partition is a filter

Used byOne-based rank of a median-of-medians result

TheoremOne-based rank of a median-of-medians result#✓fully proved

Let \(L\) be a list without repeated entries over a linear order and let \(i \ge 1\). If median-of-medians selection on \(L\) at zero-based rank \(i - 1\) returns an element \(x\), then the set \(\{y \in L : y \le x\}\) has exactly \(i\) elements.

theorem medianOfMedians_source_rank {α : Type u} [LinearOrder α]
    {xs : List α} (i : Nat) (hi : 0 < i) (hnodup : xs.Nodup) {x : α}
    (hresult : (medianOfMedians xs (i - 1)).ret = some x) :
    (xs.toFinset.filter (fun y => y ≤ x)).card = i

Uses 2 · Used by 1

Statement usesMedian-of-medians selection

Proof usesSet rank of a median-of-medians result

Used byMedian of medians selects every one-based rank

TheoremMedian of medians selects every one-based rank#✓fully proved

Let \(L\) be a list without repeated entries over a linear order, of length \(n\), and let \(1 \le i \le n\). Then median-of-medians selection on \(L\) at zero-based rank \(i - 1\) returns an element \(x\) of \(L\), and the set \(\{y \in L : y \le x\}\) has exactly \(i\) elements.

theorem medianOfMedians_source_exists {α : Type u} [LinearOrder α]
    (xs : List α) (i : Nat) (hi : 0 < i) (hlen : i ≤ xs.length) (hnodup : xs.Nodup) :
    ∃ x, (medianOfMedians xs (i - 1)).ret = some x ∧ x ∈ xs ∧
      (xs.toFinset.filter (fun y => y ≤ x)).card = i

Uses 4

Statement usesMedian-of-medians selection

Proof usesCorrectness of median-of-medians selection · Median-of-medians selection succeeds on valid ranks · One-based rank of a median-of-medians result

TheoremMedian of medians finds the lower median#✓fully proved

Let \(L\) be a nonempty list of length \(n\) over a linear order, and let \(k = \lfloor (n - 1)/2 \rfloor\). Then median-of-medians selection on \(L\) at zero-based rank \(k\) returns an element \(x\) of \(L\) such that at most \(k\) entries of \(L\) are less than \(x\) and more than \(k\) entries of \(L\) are at most \(x\), where entries are counted with repetition.

theorem medianOfMedians_lower_median {α : Type u} [LinearOrder α]
    (xs : List α) (hnonempty : 0 < xs.length) :
    ∃ x, (medianOfMedians xs ((xs.length - 1) / 2)).ret = some x ∧
      x ∈ xs ∧ xs.countP (fun y => decide (y < x)) ≤ (xs.length - 1) / 2 ∧
        (xs.length - 1) / 2 < xs.countP (fun y => decide (y ≤ x))

Uses 3

Statement usesMedian-of-medians selection

Proof usesCorrectness of median-of-medians selection · Median-of-medians selection succeeds on valid ranks

TheoremMedian of medians finds the upper median#✓fully proved

Let \(L\) be a nonempty list of length \(n\) over a linear order, and let \(k = \lfloor n/2 \rfloor\). Then median-of-medians selection on \(L\) at zero-based rank \(k\) returns an element \(x\) of \(L\) such that at most \(k\) entries of \(L\) are less than \(x\) and more than \(k\) entries of \(L\) are at most \(x\), where entries are counted with repetition.

theorem medianOfMedians_upper_median {α : Type u} [LinearOrder α]
    (xs : List α) (hnonempty : 0 < xs.length) :
    ∃ x, (medianOfMedians xs (xs.length / 2)).ret = some x ∧
      x ∈ xs ∧ xs.countP (fun y => decide (y < x)) ≤ xs.length / 2 ∧
        xs.length / 2 < xs.countP (fun y => decide (y ≤ x))

Uses 3

Statement usesMedian-of-medians selection

Proof usesCorrectness of median-of-medians selection · Median-of-medians selection succeeds on valid ranks

TheoremSize budget for the two median-of-medians recursive calls#✓fully proved

Let \(n\), \(m\) and \(p\) be natural numbers with \(n \ge 140\), \(m \le \lfloor (n + 4)/5 \rfloor\) and \(p \le \lfloor 7n/10 \rfloor + 6\). Then \(20m + 20p + n \le 20n\).

theorem medianOfMedians_child_size_budget (n m p : Nat) (hn : 140 ≤ n)
    (hm : m ≤ (n + 4) / 5) (hp : p ≤ 7 * n / 10 + 6) :
    20 * m + 20 * p + n ≤ 20 * n

Used by 1

Used byCost budget for one median-of-medians step

TheoremCost budget for one median-of-medians step#✓fully proved

Let \(n\), \(m\), \(p\), \(a\), \(c_1\) and \(c_2\) be natural numbers with \(n \ge 140\), \(m \le \lfloor (n + 4)/5 \rfloor\), \(p \le \lfloor 7n/10 \rfloor + 6\), \(c_1 \le 20am\) and \(c_2 \le 20ap\). Then \(c_1 + c_2 + an \le 20an\).

theorem medianOfMedians_combine_time (n m p a leftCost rightCost : Nat)
    (hn : 140 ≤ n) (hm : m ≤ (n + 4) / 5) (hp : p ≤ 7 * n / 10 + 6)
    (hleft : leftCost ≤ 20 * a * m) (hright : rightCost ≤ 20 * a * p) :
    leftCost + rightCost + a * n ≤ 20 * a * n

Uses 1 · Used by 2

Proof usesSize budget for the two median-of-medians recursive calls

Used byLinear solution of the median-of-medians recurrence · Median of medians makes linearly many comparisons

TheoremMedian of medians makes linearly many comparisons#✓fully proved

For every list \(L\) of length \(n\) over a linear order and every \(k \in \mathbb{N}\), median-of-medians selection on \(L\) at rank \(k\) charges at most \(80n\) comparisons, where \(n\) counts repeated entries.

Only order comparisons are charged; list construction, rank checks and recursion are free.

theorem medianOfMedians_time {α : Type u} [LinearOrder α] (xs : List α) (k : Nat) :
    (medianOfMedians xs k).time ≤ 80 * xs.length

Uses 20

Statement usesMedian-of-medians selection

Proof usesThree-way partition record · Group medians for median-of-medians selection · Group medians are lower medians of their blocks · Number of group medians · Group medians come from the input · Comparison cost of the group medians · Comparison bound for median-of-medians selection on short lists · Cost budget for one median-of-medians step · Median-of-medians selection is quickselect on short lists · Stable three-way partition · Correctness of the stable three-way partition · Counting through the below block · Counting through the above block · Entries at most the pivot · Entries below the pivot · Sizes of the three parts of a three-way partition · Cost of the stable three-way partition · Quickselect · Correctness of quickselect

TheoremLinear solution of the median-of-medians recurrence#✓fully proved

Let \(T : \mathbb{N} \to \mathbb{N}\) and \(a \in \mathbb{N}\). Suppose that \(T(n) \le 20an\) for every \(n \le 140\), and that for every \(n > 140\) there are \(m, p \in \mathbb{N}\) with \(m \le \lfloor (n + 4)/5 \rfloor\), \(p \le \lfloor 7n/10 \rfloor + 6\) and \(T(n) \le T(m) + T(p) + an\). Then \(T(n) \le 20an\) for every \(n \in \mathbb{N}\).

theorem medianOfMedians_linear_recurrence (T : Nat → Nat) (a : Nat)
    (hbase : ∀ n, n ≤ 140 → T n ≤ 20 * a * n)
    (hstep : ∀ n, 140 < n → ∃ m p,
      m ≤ (n + 4) / 5 ∧ p ≤ 7 * n / 10 + 6 ∧ T n ≤ T m + T p + a * n) :
    ∀ n, T n ≤ 20 * a * n

Uses 1

Proof usesCost budget for one median-of-medians step

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.