Bucket sort

DefinitionBucket sort#✓fully proved

Let \(R\) be a linearly ordered field with a floor function and let \(x_1, \dots, x_n\) be an array of elements of \(R\) that all lie in \([0, 1)\). If \(n = 0\), bucket sort returns the empty array at zero cost. Otherwise it creates \(n\) empty buckets indexed by \(0, \dots, n - 1\), visits the entries in order and prepends each entry \(x\) to bucket \(\lfloor n x \rfloor\), sorts each bucket with insertion sort, and concatenates the sorted buckets in increasing order of index. The cost is \(n\) for creating the buckets, plus one per entry placed, plus one per bucket sorted together with the comparisons insertion sort makes on it, plus one per bucket and one per entry during concatenation.

public def bucketSort {R : Type} [Field R] [LinearOrder R]
    [IsStrictOrderedRing R] [FloorRing R] (xs : Array R)
    (hx : ∀ x ∈ xs.toList, x ∈ Ico (0 : R) 1) : TimeM Nat (Array R) :=
  if hn : 0 < xs.size then do
    let initial : _root_.Vector (List R) xs.size := _root_.Vector.replicate xs.size []
    ✓[xs.size]
    let buckets ← placeBuckets xs hx hn initial
    let sorted ← buckets.mapM (m := TimeM Nat) (fun bucket => do
      ✓
      TimeM.insertionSort bucket)
    flattenBuckets sorted
  else pure #[]

Uses 1 · Used by 13

Statement usesInsertion sort with comparison cost

Used byBucket sort on the empty array · Bucket sort permutes its input · Bucket sort sorts · Exact cost of bucket sort · Bucket sort runs in expected linear time · Lower bound on the expected time of bucket sort · Expected time of bucket sort on one input · Upper bound on the expected time of bucket sort · Bucket sort on the empty input has expected time zero · The running time of bucket sort is integrable · Bound on the cost of bucket sort via squared bucket sizes · Linear lower bound on the cost of bucket sort · The running time of bucket sort is measurable

TheoremExact cost of bucket sort#✓fully proved

Let \(R\) be a linearly ordered field with a floor function and let \(x_1, \dots, x_n\) be an array of elements of \(R\) that all lie in \([0, 1)\). For \(0 \le i < n\) let \(B_i\) be the list of the entries \(x_j\) with \(\lfloor n x_j \rfloor = i\), in decreasing order of \(j\), and let \(T(B_i)\) be the number of comparisons insertion sort makes on \(B_i\). Then the cost of bucket sort on this array equals \(5n + \sum_{i=0}^{n-1} T(B_i)\).

public theorem bucketSort_time {R : Type} [Field R] [LinearOrder R]
    [IsStrictOrderedRing R] [FloorRing R] (xs : Array R)
    (hx : ∀ x ∈ xs.toList, x ∈ Ico (0 : R) 1) :
    (bucketSort xs hx).time = 5 * xs.size +
      ∑ i : Fin xs.size, (insertionSort
        ((xs.toList.filter
          (fun x => decide (Nat.floor ((xs.size : R) * x) = i.val))).reverse)).time

Uses 5 · Used by 7

Statement usesBucket sort · Insertion sort with comparison cost

Proof usesCharged comparison · Agreement with CSLib's monadic insertion sort · Insertion sort permutes its input

Used byLower bound on the expected time of bucket sort · Expected time of bucket sort on one input · Upper bound on the expected time of bucket sort · The running time of bucket sort is integrable · Bound on the cost of bucket sort via squared bucket sizes · Linear lower bound on the cost of bucket sort · The running time of bucket sort is measurable

TheoremLinear lower bound on the cost of bucket sort#✓fully proved

Let \(R\) be a linearly ordered field with a floor function. For every array of \(n\) elements of \(R\) that all lie in \([0, 1)\), the cost of bucket sort on this array is at least \(5n\).

public theorem bucketSort_time_lower {R : Type} [Field R] [LinearOrder R]
    [IsStrictOrderedRing R] [FloorRing R] (xs : Array R)
    (hx : ∀ x ∈ xs.toList, x ∈ Ico (0 : R) 1) :
    5 * xs.size ≤ (bucketSort xs hx).time

Uses 3

Statement usesBucket sort

Proof usesExact cost of bucket sort · Insertion sort with comparison cost

TheoremBound on the cost of bucket sort via squared bucket sizes#✓fully proved

Let \(R\) be a linearly ordered field with a floor function and let \(x_1, \dots, x_n\) be an array of elements of \(R\) that all lie in \([0, 1)\). For \(0 \le i < n\) let \(c_i\) be the number of indices \(j\) with \(\lfloor n x_j \rfloor = i\). Then the cost of bucket sort on this array is at most \(5n + \sum_{i=0}^{n-1} c_i^2\).

public theorem bucketSort_time_le_sum_sq {R : Type} [Field R] [LinearOrder R]
    [IsStrictOrderedRing R] [FloorRing R] (xs : Array R)
    (hx : ∀ x ∈ xs.toList, x ∈ Ico (0 : R) 1) :
    (bucketSort xs hx).time ≤ 5 * xs.size +
      ∑ i : Fin xs.size, (xs.toList.countP
        (fun x => decide (Nat.floor ((xs.size : R) * x) = i.val))) ^ 2

Uses 4

Statement usesBucket sort

Proof usesExact cost of bucket sort · Insertion sort with comparison cost · Comparison bound for insertion sort

TheoremBucket sort on the empty array#✓fully proved

For every linearly ordered field \(R\) with a floor function, bucket sort applied to the empty array of elements of \(R\) returns the empty array at zero cost.

public theorem bucketSort_empty {R : Type} [Field R] [LinearOrder R]
    [IsStrictOrderedRing R] [FloorRing R]
    (hx : ∀ x ∈ (#[] : Array R).toList, x ∈ Ico (0 : R) 1) :
    bucketSort #[] hx = (pure #[] : TimeM Nat (Array R))

Uses 2 · Used by 6

Statement usesBucket sort

Proof usesInsertion sort with comparison cost

Used byLower bound on the expected time of bucket sort · Expected time of bucket sort on one input · Upper bound on the expected time of bucket sort · Bucket sort on the empty input has expected time zero · The running time of bucket sort is integrable · The running time of bucket sort is measurable

TheoremBucket sort permutes its input#✓fully proved

Let \(R\) be a linearly ordered field with a floor function. For every array of elements of \(R\) that all lie in \([0, 1)\), the array returned by bucket sort is a permutation of the input: every element occurs in the output exactly as many times as in the input.

public theorem bucketSort_perm {R : Type} [Field R] [LinearOrder R]
    [IsStrictOrderedRing R] [FloorRing R] (xs : Array R)
    (hx : ∀ x ∈ xs.toList, x ∈ Ico (0 : R) 1) :
    (bucketSort xs hx).ret.toList.Perm xs.toList

Uses 5

Statement usesBucket sort

Proof usesCharged comparison · Insertion sort with comparison cost · Agreement with CSLib's monadic insertion sort · Insertion sort permutes its input

TheoremBucket sort sorts#✓fully proved

Let \(R\) be a linearly ordered field with a floor function. For every array of elements of \(R\) that all lie in \([0, 1)\), the array returned by bucket sort is nondecreasing: each entry is at most every entry after it.

public theorem bucketSort_sorted {R : Type} [Field R] [LinearOrder R]
    [IsStrictOrderedRing R] [FloorRing R] (xs : Array R)
    (hx : ∀ x ∈ xs.toList, x ∈ Ico (0 : R) 1) :
    List.Pairwise (fun x y => x ≤ y) (bucketSort xs hx).ret.toList

Uses 4

Statement usesBucket sort

Proof usesInsertion sort with comparison cost · Insertion sort permutes its input · Insertion sort returns a sorted list

TheoremExpected occupancy of a bucket in bucket sort#✓fully proved

Let \(n \ge 1\) and let \(\omega_0, \dots, \omega_{n-1}\) be independent random variables, each uniformly distributed on \([0, 1)\). For \(i < n\), let \(N_i\) be the number of indices \(j < n\) with \(\lfloor n \omega_j \rfloor = i\). Then \(\mathbb{E}[N_i] = 1\).

public theorem bucketSort_occupancy_mean {n : ℕ} (hn : 0 < n) (i : Fin n) :
    (∫ ω : Fin n → ℝ, ((Array.ofFn ω).toList.countP
      (fun x => decide (Nat.floor ((n : ℝ) * x) = i.val)) : ℝ)
      ∂Measure.pi (fun _ : Fin n => cond (volume : Measure ℝ) (Ico 0 1))) = 1

TheoremVariance of a bucket's occupancy in bucket sort#✓fully proved

Let \(n \ge 1\) and let \(\omega_0, \dots, \omega_{n-1}\) be independent random variables, each uniformly distributed on \([0, 1)\). For \(i < n\), let \(N_i\) be the number of indices \(j < n\) with \(\lfloor n \omega_j \rfloor = i\). Then \(\operatorname{Var}(N_i) = 1 - 1/n\).

public theorem bucketSort_occupancy_variance {n : ℕ} (hn : 0 < n) (i : Fin n) :
    variance (fun ω : Fin n → ℝ => ((Array.ofFn ω).toList.countP
      (fun x => decide (Nat.floor ((n : ℝ) * x) = i.val)) : ℝ))
      (Measure.pi (fun _ : Fin n => cond (volume : Measure ℝ) (Ico 0 1))) =
      1 - 1 / (n : ℝ)

TheoremSecond moment of a bucket's occupancy in bucket sort#✓fully proved

Let \(n \ge 1\) and let \(\omega_0, \dots, \omega_{n-1}\) be independent random variables, each uniformly distributed on \([0, 1)\). For \(i < n\), let \(N_i\) be the number of indices \(j < n\) with \(\lfloor n \omega_j \rfloor = i\). Then \(\mathbb{E}[N_i^2] = 2 - 1/n\).

public theorem bucketSort_occupancy_secondMoment {n : ℕ} (hn : 0 < n) (i : Fin n) :
    (∫ ω : Fin n → ℝ, ((Array.ofFn ω).toList.countP
      (fun x => decide (Nat.floor ((n : ℝ) * x) = i.val)) : ℝ) ^ 2
      ∂Measure.pi (fun _ : Fin n => cond (volume : Measure ℝ) (Ico 0 1))) =
      2 - 1 / (n : ℝ)

TheoremThe running time of bucket sort is measurable#✓fully proved

For every \(n\), the function \(T : \mathbb{R}^n \to \mathbb{R}\) that maps \(\omega = (\omega_0, \dots, \omega_{n-1})\) to the number of time steps that bucket sort charges on the array \((\omega_0, \dots, \omega_{n-1})\) if every \(\omega_j\) lies in \([0, 1)\), and to \(0\) otherwise, is measurable.

public theorem bucketSort_time_measurable (n : ℕ) :
    Measurable (fun ω : Fin n → ℝ =>
      if hx : ∀ x ∈ (Array.ofFn ω).toList, x ∈ Ico 0 1 then
        ((bucketSort (Array.ofFn ω) hx).time : ℝ) else 0)

Uses 7

Statement usesBucket sort

Proof usesBucket sort on the empty array · Exact cost of bucket sort · Charged comparison · Insertion sort with comparison cost · Agreement with CSLib's monadic insertion sort · Insertion sort permutes its input

TheoremThe running time of bucket sort is integrable#✓fully proved

For every \(n\), let \(T : \mathbb{R}^n \to \mathbb{R}\) map \(\omega = (\omega_0, \dots, \omega_{n-1})\) to the number of time steps that bucket sort charges on the array \((\omega_0, \dots, \omega_{n-1})\) if every \(\omega_j\) lies in \([0, 1)\), and to \(0\) otherwise. Then \(T\) is integrable with respect to the product of \(n\) copies of the uniform distribution on \([0, 1)\).

public theorem bucketSort_time_integrable (n : ℕ) :
    Integrable (fun ω : Fin n → ℝ =>
      if hx : ∀ x ∈ (Array.ofFn ω).toList, x ∈ Ico 0 1 then
        ((bucketSort (Array.ofFn ω) hx).time : ℝ) else 0)
      (Measure.pi (fun _ : Fin n => cond (volume : Measure ℝ) (Ico 0 1)))

Uses 8

Statement usesBucket sort

Proof usesBucket sort on the empty array · Exact cost of bucket sort · Charged comparison · Insertion sort with comparison cost · Agreement with CSLib's monadic insertion sort · Insertion sort permutes its input · Comparison bound for insertion sort

TheoremLower bound on the expected time of bucket sort#✓fully proved

Let \(n \ge 1\) and let \(\omega = (\omega_0, \dots, \omega_{n-1})\) have independent coordinates, each uniformly distributed on \([0, 1)\). Let \(T(\omega)\) be the number of time steps that bucket sort charges on the array \((\omega_0, \dots, \omega_{n-1})\) if every \(\omega_j\) lies in \([0, 1)\), and \(T(\omega) = 0\) otherwise. Then \(5n \le \mathbb{E}[T]\).

public theorem bucketSort_time_expected_lower {n : ℕ} (hn : 0 < n) :
    5 * (n : ℝ) ≤ (∫ ω : Fin n → ℝ,
      (if hx : ∀ x ∈ (Array.ofFn ω).toList, x ∈ Ico 0 1 then
        ((bucketSort (Array.ofFn ω) hx).time : ℝ) else 0)
      ∂Measure.pi (fun _ : Fin n => cond (volume : Measure ℝ) (Ico 0 1)))

Uses 8 · Used by 1

Statement usesBucket sort

Proof usesBucket sort on the empty array · Exact cost of bucket sort · Charged comparison · Insertion sort with comparison cost · Agreement with CSLib's monadic insertion sort · Insertion sort permutes its input · Comparison bound for insertion sort

Used byBucket sort runs in expected linear time

TheoremUpper bound on the expected time of bucket sort#✓fully proved

Let \(n \ge 1\) and let \(\omega = (\omega_0, \dots, \omega_{n-1})\) have independent coordinates, each uniformly distributed on \([0, 1)\). Let \(T(\omega)\) be the number of time steps that bucket sort charges on the array \((\omega_0, \dots, \omega_{n-1})\) if every \(\omega_j\) lies in \([0, 1)\), and \(T(\omega) = 0\) otherwise. Then \(\mathbb{E}[T] \le 5n + (n - 1)/2\).

public theorem bucketSort_time_expected_upper {n : ℕ} (hn : 0 < n) :
    (∫ ω : Fin n → ℝ,
      (if hx : ∀ x ∈ (Array.ofFn ω).toList, x ∈ Ico 0 1 then
        ((bucketSort (Array.ofFn ω) hx).time : ℝ) else 0)
      ∂Measure.pi (fun _ : Fin n => cond (volume : Measure ℝ) (Ico 0 1))) ≤
      5 * n + ((n : ℝ) - 1) / 2

Uses 8 · Used by 1

Statement usesBucket sort

Proof usesBucket sort on the empty array · Exact cost of bucket sort · Charged comparison · Insertion sort with comparison cost · Agreement with CSLib's monadic insertion sort · Insertion sort permutes its input · Comparison bound for insertion sort

Used byBucket sort runs in expected linear time

TheoremBucket sort on the empty input has expected time zero#✓fully proved

Let \(T\) be the number of time steps that bucket sort charges on the empty array, the only input of length \(n = 0\). Its expectation under the product of zero copies of the uniform distribution on \([0, 1)\) is \(0\).

public theorem bucketSort_time_expected_zero :
    (∫ ω : Fin 0 → ℝ,
      (if hx : ∀ x ∈ (Array.ofFn ω).toList, x ∈ Ico 0 1 then
        ((bucketSort (Array.ofFn ω) hx).time : ℝ) else 0)
      ∂Measure.pi (fun _ : Fin 0 => cond (volume : Measure ℝ) (Ico 0 1))) = 0

Uses 2

Statement usesBucket sort

Proof usesBucket sort on the empty array

TheoremExpected time of bucket sort on one input#✓fully proved

Let \(\omega_0\) be uniformly distributed on \([0, 1)\), and let \(T(\omega_0)\) be the number of time steps that bucket sort charges on the one-element array \((\omega_0)\) if \(\omega_0 \in [0, 1)\), and \(T(\omega_0) = 0\) otherwise. Then \(\mathbb{E}[T] = 5\).

public theorem bucketSort_time_expected_one :
    (∫ ω : Fin 1 → ℝ,
      (if hx : ∀ x ∈ (Array.ofFn ω).toList, x ∈ Ico 0 1 then
        ((bucketSort (Array.ofFn ω) hx).time : ℝ) else 0)
      ∂Measure.pi (fun _ : Fin 1 => cond (volume : Measure ℝ) (Ico 0 1))) = 5

Uses 8

Statement usesBucket sort

Proof usesBucket sort on the empty array · Exact cost of bucket sort · Charged comparison · Insertion sort with comparison cost · Agreement with CSLib's monadic insertion sort · Insertion sort permutes its input · Comparison bound for insertion sort

TheoremBucket sort runs in expected linear time#✓fully proved

For each \(n\), let \(\omega = (\omega_0, \dots, \omega_{n-1})\) have independent coordinates, each uniformly distributed on \([0, 1)\). Let \(T_n(\omega)\) be the number of time steps that bucket sort charges on the array \((\omega_0, \dots, \omega_{n-1})\) if every \(\omega_j\) lies in \([0, 1)\), and \(T_n(\omega) = 0\) otherwise. Then \(\mathbb{E}[T_n] = \Theta(n)\) as \(n \to \infty\).

public theorem bucketSort_time_expected_isTheta :
    Asymptotics.IsTheta atTop
      (fun n : ℕ => ∫ ω : Fin n → ℝ,
        (if hx : ∀ x ∈ (Array.ofFn ω).toList, x ∈ Ico 0 1 then
          ((bucketSort (Array.ofFn ω) hx).time : ℝ) else 0)
        ∂Measure.pi (fun _ : Fin n => cond (volume : Measure ℝ) (Ico 0 1)))
      (fun n : ℕ => (n : ℝ))

Uses 3

Statement usesBucket sort

Proof usesLower bound on the expected time of bucket sort · Upper bound on the expected time of bucket sort

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.