Chapter 11 — Hash Tables

CLRS, fourth edition · Lean 4 formalization

The proofs below use the models and assumptions described in the scope and implementation notes.

Imports

import Mathlib

11.1. Direct-Address Tables

This section models a direct-address table as a total function from natural keys to optional values. This is the mathematical core of the CLRS operations: search reads the key slot, insert overwrites that slot, and delete clears it.

Main results:

Theorem search_insert_same: searching the inserted key returns the new value.
Theorem search_insert_other: inserting at one key leaves other keys unchanged.
Theorem search_delete_same: deleting a key clears that key.

Status: proved for the functional direct-address model.

Deferred refinements: array bounds and RAM costs.

namespace CLRSnamespace Chapter11

Direct-address table model

A direct-address table maps each natural key to an optional value.

abbrev DirectAddressTable (V : Type u) := Nat → Option V

The empty direct-address table.

def emptyDirectAddressTable : DirectAddressTable V :=
  fun _ => none

Search a direct-address table by reading the corresponding slot.

def directSearch (T : DirectAddressTable V) (key : Nat) : Option V :=
  T key

Insert overwrites the slot at key.

def directInsert (key : Nat) (value : V)
    (T : DirectAddressTable V) : DirectAddressTable V :=
  fun j => if j = key then some value else T j

Delete clears the slot at key.

def directDelete (key : Nat)
    (T : DirectAddressTable V) : DirectAddressTable V :=
  fun j => if j = key then none else T j

Operation correctness

Searching the inserted key returns the inserted value.

theorem search_insert_same (key : Nat) (value : V)
    (T : DirectAddressTable V) :
    directSearch (directInsert key value T) key = some value := by
  simp [directSearch, directInsert]

Inserting at one key leaves every other key unchanged.

theorem search_insert_other {key other : Nat} (h : other ≠ key)
    (value : V) (T : DirectAddressTable V) :
    directSearch (directInsert key value T) other = directSearch T other := by
  simp [directSearch, directInsert, h]

Deleting a key makes search at that key return none.

theorem search_delete_same (key : Nat) (T : DirectAddressTable V) :
    directSearch (directDelete key T) key = none := by
  simp [directSearch, directDelete]

Deleting one key leaves every other key unchanged.

theorem search_delete_other {key other : Nat} (h : other ≠ key)
    (T : DirectAddressTable V) :
    directSearch (directDelete key T) other = directSearch T other := by
  simp [directSearch, directDelete, h]

Searching an empty direct-address table returns none.

theorem search_empty (key : Nat) :
    directSearch (emptyDirectAddressTable : DirectAddressTable V) key = none := by
  rfl

end Chapter11end CLRS

Imports

import Mathlib
import CLRSLean.Probability.FiniteExpectation

11.2. Chained Hash Tables

This section gives a deterministic correctness layer for chained hash tables. The table is a function from bucket indices to lists of keys. The hash function decides the bucket, insertion conses the key onto that bucket, and deletion filters the key from that same bucket.

Main results:

Theorem bucket_hashInsert_same: the inserted key appears in its hash bucket.
Theorem bucket_hashInsert_other: buckets with a different index are unchanged.
Theorem hashSearch_hashInsert_self: after insertion, searching for the inserted key succeeds.
Theorem hashSearch_hashInsert_iff: after insertion, searching for any query succeeds exactly when it is the inserted key or was already present.
Theorem hashSearch_hashDelete_self: after deletion, searching for the deleted key fails.
Theorem hashSearch_hashDelete_iff: after deletion, searching for any query succeeds exactly when it is different from the deleted key and was already present.
Theorem expectedSearchChainLength_eq_loadFactor: in the finite-uniform bucket model, expected chain length is exactly the load factor.
Theorem expectedUnsuccessfulSearchCost_finiteHashInsert: inserting one key increases expected unsuccessful-search cost by 1/m.
Theorem expectedRandomChainLength_eq_loadFactor: under SUHA (keys hashed independently and uniformly), the expected chain length at any fixed bucket is the load factor α = n/m, as a genuine expectation over the input distribution Fin n → Fin m.
Theorem expectedRandomUnsuccessfulSearchCost: the expected unsuccessful search cost is 1 + α, as a genuine expectation.
Theorem pairCollisionProb: under SUHA, two distinct keys collide with probability exactly 1/m, as a genuine expectation.
Theorem expectedRandomSuccessfulSearchCost: the expected successful-search cost is 1 + (n-1)/(2m) (CLRS Theorem 11.2), as a double expectation over the uniform query key and the SUHA input distribution.
Definition IsUniversal and Theorems universal_expected_collisions / universal_expected_search_cost: a random hash-function model, where a universal family gives expected collisions ≤ α and search cost ≤ 1 + α (CLRS Theorem 11.3).

Status: proved for deterministic correctness, finite-uniform expected cost, the SUHA true-expectation chain-length / unsuccessful- / successful-search analysis, and a universal random-hash-function collision-bound model.

Deferred refinements: RAM / probe-count operational semantics.

namespace CLRSnamespace Chapter11

Chained table model

A chained hash table maps bucket indices to lists of stored keys.

abbrev ChainedHashTable (K : Type u) := Nat → List K

Insert a key into the bucket selected by the hash function.

def hashInsert (h : K → Nat) (x : K)
    (T : ChainedHashTable K) : ChainedHashTable K :=
  fun i => if i = h x then x :: T i else T i

Delete every copy of a key from the bucket selected by the hash function. This is the deterministic functional analogue of CLRS chained-hash deletion; pointer updates inside a linked list are intentionally outside this model.

def hashDelete [DecidableEq K] (h : K → Nat) (x : K)
    (T : ChainedHashTable K) : ChainedHashTable K :=
  fun i => if i = h x then (T i).filter fun y => y != x else T i

Search for a key in the bucket selected by its hash value.

def hashSearch (h : K → Nat) (T : ChainedHashTable K) (x : K) : Prop :=
  x ∈ T (h x)

Deterministic correctness

The inserted key appears in its own hash bucket.

theorem bucket_hashInsert_same (h : K → Nat) (T : ChainedHashTable K) (x : K) :
    x ∈ hashInsert h x T (h x) := by
  simp [hashInsert]

A bucket with a different index is unchanged by insertion.

theorem bucket_hashInsert_other {h : K → Nat} {T : ChainedHashTable K}
    {x : K} {i : Nat} (hi : i ≠ h x) :
    hashInsert h x T i = T i := by
  simp [hashInsert, hi]

The deleted key no longer appears in its hash bucket.

theorem bucket_hashDelete_same [DecidableEq K]
    (h : K → Nat) (T : ChainedHashTable K) (x : K) :
    x ∉ hashDelete h x T (h x) := by
  simp [hashDelete]

A bucket with a different index is unchanged by deletion.

theorem bucket_hashDelete_other [DecidableEq K]
    {h : K → Nat} {T : ChainedHashTable K} {x : K} {i : Nat}
    (hi : i ≠ h x) :
    hashDelete h x T i = T i := by
  simp [hashDelete, hi]

After inserting a key, searching for that key succeeds.

theorem hashSearch_hashInsert_self (h : K → Nat)
    (T : ChainedHashTable K) (x : K) :
    hashSearch h (hashInsert h x T) x := by
  exact bucket_hashInsert_same h T x

Searching after insertion succeeds exactly when the query is the inserted key or the query already appeared in its own hash bucket.


theorem hashSearch_hashInsert_iff (h : K → Nat)
    (T : ChainedHashTable K) (x y : K) :
    hashSearch h (hashInsert h y T) x ↔ x = y ∨ hashSearch h T x := by
  by_cases hxy : h x = h y
  · simp [hashSearch, hashInsert, hxy]
  · have hxne : x ≠ y := by
      intro hkey
      exact hxy (by rw [hkey])
    simp [hashSearch, hashInsert, hxy, hxne]

After deleting a key, searching for that key fails.

theorem hashSearch_hashDelete_self [DecidableEq K] (h : K → Nat)
    (T : ChainedHashTable K) (x : K) :
    ¬ hashSearch h (hashDelete h x T) x := by
  exact bucket_hashDelete_same h T x

Searching after deletion succeeds exactly when the query is not the deleted key and the query was already present in its own hash bucket.


theorem hashSearch_hashDelete_iff [DecidableEq K] (h : K → Nat)
    (T : ChainedHashTable K) (x y : K) :
    hashSearch h (hashDelete h y T) x ↔ x ≠ y ∧ hashSearch h T x := by
  by_cases hxy : h x = h y
  · simp [hashSearch, hashDelete, hxy, and_comm]
  · have hxne : x ≠ y := by
      intro hkey
      exact hxy (by rw [hkey])
    simp [hashSearch, hashDelete, hxy, hxne]

Finite-uniform hashing interface

A finite chained hash table with exactly m buckets.

abbrev FiniteChainedHashTable (m : Nat) (K : Type u) := Fin m → List K

A real-valued 0/1 indicator for finite probability calculations.

def probabilityIndicator (P : Prop) [Decidable P] : ℝ :=
  if P then 1 else 0

Uniform average over the bucket set Fin m.

noncomputable def uniformAverageFin {m : Nat} (X : Fin m → ℝ) : ℝ :=
  (∑ i : Fin m, X i) / (m : ℝ)

The finite-uniform bucket average is the shared CLRS.Probability.fintypeExpect toolkit specialised to Fin m. This bridge lets the algebraic lemmas below reuse the toolkit instead of re-deriving them.

theorem uniformAverageFin_eq_fintypeExpect {m : Nat} (X : Fin m → ℝ) :
    uniformAverageFin X = CLRS.Probability.fintypeExpect X := by
  simp [uniformAverageFin, CLRS.Probability.fintypeExpect, Fintype.card_fin]

Uniform averages are additive.

theorem uniformAverageFin_add {m : Nat} (X Y : Fin m → ℝ) :
    uniformAverageFin (fun i => X i + Y i) =
      uniformAverageFin X + uniformAverageFin Y := by
  simp only [uniformAverageFin_eq_fintypeExpect]
  exact CLRS.Probability.fintypeExpect_add X Y

A uniform average of nonnegative quantities is nonnegative.


theorem uniformAverageFin_nonneg {m : Nat} {X : Fin m → ℝ}
    (hX : ∀ i, 0 ≤ X i) :
    0 ≤ uniformAverageFin X := by
  rw [uniformAverageFin_eq_fintypeExpect]
  exact CLRS.Probability.fintypeExpect_nonneg hX

A singleton bucket has probability 1/m under the uniform bucket model.


theorem uniformAverageFin_indicator_singleton {m : Nat} (j : Fin m) :
    uniformAverageFin (fun i => probabilityIndicator (i = j)) = 1 / (m : ℝ) := by
  rw [uniformAverageFin_eq_fintypeExpect,
    show (fun i : Fin m => probabilityIndicator (i = j))
        = (fun i => CLRS.Probability.indicator (i = j)) from rfl,
    CLRS.Probability.fintypeExpect_indicator_singleton, Fintype.card_fin]

Insert into a finite-bucket chained hash table.

def finiteHashInsert {m : Nat} (h : K → Fin m) (x : K)
    (T : FiniteChainedHashTable m K) : FiniteChainedHashTable m K :=
  fun i => if i = h x then x :: T i else T i

Search in a finite-bucket chained hash table.

def finiteHashSearch {m : Nat} (h : K → Fin m)
    (T : FiniteChainedHashTable m K) (x : K) : Prop :=
  x ∈ T (h x)

The finite-bucket load factor: stored keys divided by bucket count.

noncomputable def finiteHashLoadFactor {m : Nat}
    (T : FiniteChainedHashTable m K) : ℝ :=
  (∑ i : Fin m, ((T i).length : ℝ)) / (m : ℝ)

Load factor is nonnegative.

theorem finiteHashLoadFactor_nonneg {m : Nat}
    (T : FiniteChainedHashTable m K) :
    0 ≤ finiteHashLoadFactor T := by
  unfold finiteHashLoadFactor
  refine div_nonneg ?_ ?_
  · exact Finset.sum_nonneg (fun i _hi => by exact_mod_cast Nat.zero_le (T i).length)
  · exact_mod_cast Nat.zero_le m

Expected chain length for an unsuccessful search when the searched bucket is uniform over all buckets.

noncomputable def expectedSearchChainLength {m : Nat}
    (T : FiniteChainedHashTable m K) : ℝ :=
  uniformAverageFin (fun i => ((T i).length : ℝ))

Expected unsuccessful-search cost in the current abstraction: one bucket access plus the expected chain length.

noncomputable def expectedUnsuccessfulSearchCost {m : Nat}
    (T : FiniteChainedHashTable m K) : ℝ :=
  1 + expectedSearchChainLength T

Under uniform hashing over buckets, expected chain length is exactly the load factor.

theorem expectedSearchChainLength_eq_loadFactor {m : Nat}
    (T : FiniteChainedHashTable m K) :
    expectedSearchChainLength T = finiteHashLoadFactor T := by
  rfl

Expected chain length is nonnegative in the finite-uniform bucket model.


theorem expectedSearchChainLength_nonneg {m : Nat}
    (T : FiniteChainedHashTable m K) :
    0 ≤ expectedSearchChainLength T := by
  rw [expectedSearchChainLength_eq_loadFactor]
  exact finiteHashLoadFactor_nonneg T

Under uniform hashing over buckets, unsuccessful search has cost 1 + load factor in the current finite-bucket abstraction.

theorem expectedUnsuccessfulSearchCost_eq_one_plus_loadFactor {m : Nat}
    (T : FiniteChainedHashTable m K) :
    expectedUnsuccessfulSearchCost T = 1 + finiteHashLoadFactor T := by
  rfl

Expected unsuccessful-search cost is at least the initial bucket access.

theorem expectedUnsuccessfulSearchCost_ge_one {m : Nat}
    (T : FiniteChainedHashTable m K) :
    1 ≤ expectedUnsuccessfulSearchCost T := by
  unfold expectedUnsuccessfulSearchCost
  have hnonneg := expectedSearchChainLength_nonneg T
  linarith

Inserting one key into a finite chained table increases total chain length by one.


theorem totalBucketLength_finiteHashInsert {m : Nat} (h : K → Fin m)
    (T : FiniteChainedHashTable m K) (x : K) :
    (∑ i : Fin m, ((finiteHashInsert h x T i).length : ℝ)) =
      (∑ i : Fin m, ((T i).length : ℝ)) + 1 := by
  classical
  have hpoint : ∀ i : Fin m,
      ((finiteHashInsert h x T i).length : ℝ) =
        ((T i).length : ℝ) + probabilityIndicator (i = h x) := by
    intro i
    by_cases hi : i = h x
    · simp [finiteHashInsert, probabilityIndicator, hi]
    · simp [finiteHashInsert, probabilityIndicator, hi]
  have hindicator :
      (∑ i : Fin m, probabilityIndicator (i = h x)) = (1 : ℝ) := by
    rw [Finset.sum_eq_single (h x)]
    · simp [probabilityIndicator]
    · intro b _hb hbne
      simp [probabilityIndicator, hbne]
    · intro hmissing
      exact (hmissing (Finset.mem_univ (h x))).elim
  calc
    (∑ i : Fin m, ((finiteHashInsert h x T i).length : ℝ))
        = ∑ i : Fin m, (((T i).length : ℝ) + probabilityIndicator (i = h x)) := by
          exact Finset.sum_congr rfl (fun i _hi => hpoint i)
    _ = (∑ i : Fin m, ((T i).length : ℝ)) +
          ∑ i : Fin m, probabilityIndicator (i = h x) := by
          rw [Finset.sum_add_distrib]
    _ = (∑ i : Fin m, ((T i).length : ℝ)) + 1 := by
          rw [hindicator]

Inserting one key increases the expected chain length by 1/m in the finite-uniform bucket model.

theorem expectedSearchChainLength_finiteHashInsert {m : Nat} (h : K → Fin m)
    (T : FiniteChainedHashTable m K) (x : K) :
    expectedSearchChainLength (finiteHashInsert h x T) =
      expectedSearchChainLength T + 1 / (m : ℝ) := by
  simp [expectedSearchChainLength, uniformAverageFin,
    totalBucketLength_finiteHashInsert, add_div]

Inserting one key increases the finite-bucket load factor by 1/m.

theorem finiteHashLoadFactor_finiteHashInsert {m : Nat} (h : K → Fin m)
    (T : FiniteChainedHashTable m K) (x : K) :
    finiteHashLoadFactor (finiteHashInsert h x T) =
      finiteHashLoadFactor T + 1 / (m : ℝ) := by
  simp [finiteHashLoadFactor, totalBucketLength_finiteHashInsert, add_div]

Inserting one key increases expected unsuccessful-search cost by 1/m in the finite-uniform bucket model.


theorem expectedUnsuccessfulSearchCost_finiteHashInsert {m : Nat} (h : K → Fin m)
    (T : FiniteChainedHashTable m K) (x : K) :
    expectedUnsuccessfulSearchCost (finiteHashInsert h x T) =
      expectedUnsuccessfulSearchCost T + 1 / (m : ℝ) := by
  rw [expectedUnsuccessfulSearchCost, expectedSearchChainLength_finiteHashInsert,
    expectedUnsuccessfulSearchCost]
  ring

Expected search cost as a true expectation (SUHA)

The finite-uniform layer above is definitional. We now derive the CLRS chained-hash costs as genuine expectations under the simple uniform hashing assumption: n keys are hashed independently and uniformly into m buckets. The sample space is the explicit independent uniform distribution Fin n → Fin m (the bucket each key hashes to), and the load factor is α = n/m.

open CLRS.Probability

The load factor α = n/m of n keys in m buckets.

noncomputable def loadFactor (m n : Nat) : ℝ := (n : ℝ) / (m : ℝ)

Split a hash assignment a : Fin n → Fin m into the bucket of one key i and the assignment of the remaining keys. This is the product decomposition witnessing that coordinate i is independent of the rest.

noncomputable def hashSplit {m n : Nat} (i : Fin n) :
    (Fin n → Fin m) ≃ Fin m × ({x : Fin n // x ≠ i} → Fin m) where
  toFun a := (a i, fun x => a x.val)
  invFun q := fun x => if hx : x = i then q.1 else q.2 ⟨x, hx⟩
  left_inv a := by
    funext x; by_cases hx : x = i
    · subst hx; simp
    · simp [hx]
  right_inv q := by
    obtain ⟨b, rest⟩ := q
    simp only [Prod.mk.injEq]
    refine ⟨by simp, ?_⟩
    funext x; obtain ⟨xv, hxi⟩ := x; simp [hxi]

Marginalisation: the expectation of a function of a single hash coordinate equals the expectation over the single-bucket space Fin m.


theorem fintypeExpect_hashCoord {m n : Nat} (i : Fin n) (hm : 0 < m) (f : Fin m → ℝ) :
    fintypeExpect (fun a : Fin n → Fin m => f (a i)) = fintypeExpect f := by
  haveI : Nonempty (Fin m) := ⟨⟨0, hm⟩⟩
  have hcard : Fintype.card ({x : Fin n // x ≠ i} → Fin m) ≠ 0 := Fintype.card_ne_zero
  have he := fintypeExpect_equiv (hashSplit (m := m) i)
    (fun q : Fin m × ({x : Fin n // x ≠ i} → Fin m) => f q.1)
  simp only [hashSplit, Equiv.coe_fn_mk] at he
  rw [he]
  exact fintypeExpect_fst hcard f

A single key hashes to a fixed bucket q with probability 1/m.


theorem singleBucketProb {m n : Nat} (i : Fin n) (q : Fin m) (hm : 0 < m) :
    fintypeExpect (fun a : Fin n → Fin m => indicator (a i = q)) = 1 / (m : ℝ) := by
  rw [fintypeExpect_hashCoord i hm (fun c => indicator (c = q)),
    fintypeExpect_indicator_singleton, Fintype.card_fin]

The length of the chain at bucket q under a hash assignment a: the number of keys that hash to q.

noncomputable def randomChainLength {m n : Nat} (a : Fin n → Fin m) (q : Fin m) : ℝ :=
  ∑ i : Fin n, indicator (a i = q)

Expected chain length = load factor (true expectation). Under SUHA, the expected number of keys hashing to any fixed bucket q is exactly the load factor α = n/m (CLRS Theorem 11.1, unsuccessful-search chain length).


theorem expectedRandomChainLength_eq_loadFactor {m n : Nat} (q : Fin m) (hm : 0 < m) :
    fintypeExpect (fun a : Fin n → Fin m => randomChainLength a q) = loadFactor m n := by
  unfold randomChainLength loadFactor
  rw [fintypeExpect_sum]
  simp only [singleBucketProb _ q hm]
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  ring

Expected unsuccessful-search cost = 1 + α (true expectation). One bucket access plus the expected chain length, as a genuine expectation over the SUHA input distribution (CLRS Theorem 11.1).


theorem expectedRandomUnsuccessfulSearchCost {m n : Nat} (q : Fin m) (hm : 0 < m) :
    fintypeExpect (fun a : Fin n → Fin m => 1 + randomChainLength a q) =
      1 + loadFactor m n := by
  haveI : Nonempty (Fin m) := ⟨⟨0, hm⟩⟩
  have hcard : Fintype.card (Fin n → Fin m) ≠ 0 := Fintype.card_ne_zero
  have key : (fun a : Fin n → Fin m => 1 + randomChainLength a q)
      = (fun a => (fun _ : Fin n → Fin m => (1 : ℝ)) a
          + (fun a => randomChainLength a q) a) := rfl
  rw [key, fintypeExpect_add, fintypeExpect_const hcard,
    expectedRandomChainLength_eq_loadFactor q hm]

Successful search as a true expectation (SUHA)

CLRS Theorem 11.2 analyses a successful search: the query key is one of the n stored keys, chosen uniformly, and the number of probes is one (for the key itself) plus the number of keys that precede it in its chain. Because new keys are prepended, the keys ahead of k_i are exactly those inserted after it, i.e. the later-indexed keys k_j with j > i that hash to the same bucket. Averaging over both the uniformly random query key and the SUHA input distribution Fin n → Fin m gives the expected cost 1 + α/2 - α/(2n), which we prove here in the exact form 1 + (n-1)/(2m).

Scalar factors pull out of fintypeExpect: the finite-uniform expectation is linear in a constant multiplier.


theorem fintypeExpect_const_mul {Ω : Type} [Fintype Ω] [DecidableEq Ω]
    (c : ℝ) (X : Ω → ℝ) :
    fintypeExpect (fun ω => c * X ω) = c * fintypeExpect X := by
  unfold fintypeExpect
  rw [← Finset.mul_sum, mul_div_assoc]

Split a hash assignment a : Fin n → Fin m into the buckets of two distinct keys i ≠ j together with the assignment of the remaining keys. This witnesses that the pair of coordinates (i, j) is independent of the rest.

noncomputable def hashSplitPair {m n : Nat} (i j : Fin n) (hij : i ≠ j) :
    (Fin n → Fin m) ≃
      (Fin m × Fin m) × ({x : Fin n // x ≠ i ∧ x ≠ j} → Fin m) where
  toFun a := ((a i, a j), fun x => a x.val)
  invFun q := fun x =>
    if hx : x = i then q.1.1
    else if hy : x = j then q.1.2
    else q.2 ⟨x, ⟨hx, hy⟩⟩
  left_inv a := by
    funext x
    by_cases hx : x = i
    · subst hx; simp
    · by_cases hy : x = j
      · subst hy; simp [hx]
      · simp [hx, hy]
  right_inv q := by
    obtain ⟨⟨b1, b2⟩, rest⟩ := q
    simp only [Prod.mk.injEq]
    refine ⟨⟨?_, ?_⟩, ?_⟩
    · simp
    · have hji : ¬ (j = i) := fun h => hij h.symm
      simp [hji]
    · funext x; obtain ⟨xv, hxi, hxj⟩ := x
      simp [hxi, hxj]

The uniform probability that the two coordinates of a pair over Fin m agree is 1/m: the diagonal of Fin m × Fin m has m of the m² points.


theorem fintypeExpect_prod_diag {m : Nat} (hm : 0 < m) :
    fintypeExpect (fun q : Fin m × Fin m => indicator (q.1 = q.2)) = 1 / (m : ℝ) := by
  have hm' : (m : ℝ) ≠ 0 := by exact_mod_cast hm.ne'
  have hnum : (∑ q : Fin m × Fin m, indicator (q.1 = q.2)) = (m : ℝ) := by
    unfold indicator
    rw [Fintype.sum_prod_type]
    have hinner : ∀ a : Fin m, (∑ b : Fin m, (if a = b then (1 : ℝ) else 0)) = 1 := by
      intro a; simp
    rw [Finset.sum_congr rfl (fun a _ => hinner a), Finset.sum_const,
      Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, mul_one]
  unfold fintypeExpect
  rw [hnum, Fintype.card_prod, Fintype.card_fin]
  push_cast
  rw [div_mul_eq_div_div, div_self hm']

Pairwise collision probability = 1/m (true expectation). Under SUHA, two distinct keys i ≠ j hash to the same bucket with probability exactly 1/m, as a genuine expectation over the input distribution Fin n → Fin m (CLRS Corollary/analysis underlying Theorems 11.1-11.2, E[X_ij] = 1/m).


theorem pairCollisionProb {m n : Nat} (i j : Fin n) (hij : i ≠ j) (hm : 0 < m) :
    fintypeExpect (fun a : Fin n → Fin m => indicator (a i = a j)) = 1 / (m : ℝ) := by
  haveI : Nonempty (Fin m) := ⟨⟨0, hm⟩⟩
  have hcard :
      Fintype.card ({x : Fin n // x ≠ i ∧ x ≠ j} → Fin m) ≠ 0 := Fintype.card_ne_zero
  have he := fintypeExpect_equiv (hashSplitPair (m := m) i j hij)
    (fun p : (Fin m × Fin m) × ({x : Fin n // x ≠ i ∧ x ≠ j} → Fin m) =>
      indicator (p.1.1 = p.1.2))
  simp only [hashSplitPair, Equiv.coe_fn_mk] at he
  have h2 : fintypeExpect
        (fun p : (Fin m × Fin m) × ({x : Fin n // x ≠ i ∧ x ≠ j} → Fin m) =>
          indicator (p.1.1 = p.1.2)) = 1 / (m : ℝ) := by
    rw [← fintypeExpect_prod_diag hm]
    exact fintypeExpect_fst hcard (fun q : Fin m × Fin m => indicator (q.1 = q.2))
  exact he.trans h2

The number of ordered pairs i < j in Fin n, counted in ℝ, is n(n-1)/2. This is the Gauss triangle count obtained from trichotomy and the symmetry of the strict order.


theorem sum_upper_triangle (n : Nat) :
    (∑ i : Fin n, ∑ j : Fin n, (if i < j then (1 : ℝ) else 0))
      = (n : ℝ) * ((n : ℝ) - 1) / 2 := by
  have hpt : ∀ i j : Fin n,
      (if i < j then (1 : ℝ) else 0) + (if j < i then (1 : ℝ) else 0)
        + (if i = j then (1 : ℝ) else 0) = 1 := by
    intro i j
    rcases lt_trichotomy i j with h | h | h
    · have h1 : ¬ j < i := lt_asymm h
      have h2 : ¬ i = j := ne_of_lt h
      simp [h, h1, h2]
    · subst h; simp
    · have h1 : ¬ i < j := lt_asymm h
      have h2 : ¬ i = j := fun he => (ne_of_lt h) he.symm
      simp [h, h1, h2]
  have hUL : (∑ i : Fin n, ∑ j : Fin n, (if i < j then (1 : ℝ) else 0))
      = ∑ i : Fin n, ∑ j : Fin n, (if j < i then (1 : ℝ) else 0) := Finset.sum_comm
  have hD : (∑ i : Fin n, ∑ j : Fin n, (if i = j then (1 : ℝ) else 0)) = (n : ℝ) := by
    have hone : ∀ i : Fin n, (∑ j : Fin n, (if i = j then (1 : ℝ) else 0)) = 1 := by
      intro i; simp
    rw [Finset.sum_congr rfl (fun i _ => hone i), Finset.sum_const,
      Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, mul_one]
  have hAll : (∑ i : Fin n, ∑ j : Fin n, (if i < j then (1 : ℝ) else 0))
      + (∑ i : Fin n, ∑ j : Fin n, (if j < i then (1 : ℝ) else 0))
      + (∑ i : Fin n, ∑ j : Fin n, (if i = j then (1 : ℝ) else 0))
      = (n : ℝ) * (n : ℝ) := by
    rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
    have hstep : (∑ i : Fin n, ((∑ j : Fin n, (if i < j then (1 : ℝ) else 0))
        + (∑ j : Fin n, (if j < i then (1 : ℝ) else 0))
        + ∑ j : Fin n, (if i = j then (1 : ℝ) else 0)))
        = ∑ _i : Fin n, (n : ℝ) := by
      refine Finset.sum_congr rfl (fun i _ => ?_)
      rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib,
        Finset.sum_congr rfl (fun j _ => hpt i j), Finset.sum_const,
        Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, mul_one]
    rw [hstep, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  rw [← hUL, hD] at hAll
  have h2 : (∑ i : Fin n, ∑ j : Fin n, (if i < j then (1 : ℝ) else 0))
      = ((n : ℝ) * (n : ℝ) - (n : ℝ)) / 2 := by linarith
  rw [h2]; ring

Cost of a successful search for the i-th inserted key under a hash assignment a: one probe for k_i itself, plus one probe for every later-inserted key k_j (index j > i) that hashes to the same bucket (CLRS proof of Theorem 11.2, keys prepended so those ahead of k_i are exactly the later ones).

noncomputable def successfulSearchKeyCost {m n : Nat}
    (a : Fin n → Fin m) (i : Fin n) : ℝ :=
  1 + ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0)

Average successful-search cost over the n stored keys, for a fixed hash assignment a (the query key is uniform over the stored keys).

noncomputable def averageSuccessfulSearchCost {m n : Nat}
    (a : Fin n → Fin m) : ℝ :=
  (1 / (n : ℝ)) * ∑ i : Fin n, successfulSearchKeyCost a i

Expected successful-search cost = 1 + (n-1)/(2m) (true expectation). This is CLRS Theorem 11.2 (Θ(1 + α), exact form 1 + α/2 - α/(2n)), proved as a genuine double expectation: over the uniformly random query key and over the SUHA input distribution Fin n → Fin m.


theorem expectedRandomSuccessfulSearchCost {m n : Nat} (hm : 0 < m) (hn : 0 < n) :
    fintypeExpect (fun a : Fin n → Fin m => averageSuccessfulSearchCost a)
      = 1 + ((n : ℝ) - 1) / (2 * (m : ℝ)) := by
  haveI : Nonempty (Fin m) := ⟨⟨0, hm⟩⟩
  have hmcard : Fintype.card (Fin n → Fin m) ≠ 0 := Fintype.card_ne_zero
  have hn' : (n : ℝ) ≠ 0 := by exact_mod_cast hn.ne'
  have hm' : (m : ℝ) ≠ 0 := by exact_mod_cast hm.ne'
  have hE : fintypeExpect (fun a : Fin n → Fin m =>
      ∑ i : Fin n, ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0))
      = ∑ i : Fin n, ∑ j : Fin n, (if i < j then (1 / (m : ℝ)) else 0) := by
    rw [fintypeExpect_sum Finset.univ (fun (i : Fin n) (a : Fin n → Fin m) =>
      ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0))]
    refine Finset.sum_congr rfl (fun i _ => ?_)
    rw [fintypeExpect_sum Finset.univ (fun (j : Fin n) (a : Fin n → Fin m) =>
      if i < j then indicator (a i = a j) else 0)]
    refine Finset.sum_congr rfl (fun j _ => ?_)
    by_cases hlt : i < j
    · simp only [if_pos hlt]
      exact pairCollisionProb i j (ne_of_lt hlt) hm
    · simp only [if_neg hlt]
      exact fintypeExpect_const hmcard 0
  have hpair : (∑ i : Fin n, ∑ j : Fin n, (if i < j then (1 / (m : ℝ)) else 0))
      = (1 / (m : ℝ)) * ((n : ℝ) * ((n : ℝ) - 1) / 2) := by
    rw [← sum_upper_triangle n, Finset.mul_sum]
    refine Finset.sum_congr rfl (fun i _ => ?_)
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl (fun j _ => ?_)
    by_cases h : i < j <;> simp [h]
  have hG : fintypeExpect (fun a : Fin n → Fin m =>
        ∑ i : Fin n, successfulSearchKeyCost a i)
      = (n : ℝ) + (1 / (m : ℝ)) * ((n : ℝ) * ((n : ℝ) - 1) / 2) := by
    have hGkey : (fun a : Fin n → Fin m => ∑ i : Fin n, successfulSearchKeyCost a i)
        = (fun a => (fun _ : Fin n → Fin m => (n : ℝ)) a
            + (fun a => ∑ i : Fin n, ∑ j : Fin n,
                (if i < j then indicator (a i = a j) else 0)) a) := by
      funext a
      show (∑ i : Fin n, successfulSearchKeyCost a i)
          = (n : ℝ) + ∑ i : Fin n, ∑ j : Fin n,
              (if i < j then indicator (a i = a j) else 0)
      unfold successfulSearchKeyCost
      rw [Finset.sum_add_distrib, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
        nsmul_eq_mul, mul_one]
    rw [hGkey, fintypeExpect_add, fintypeExpect_const hmcard, hE, hpair]
  have key : (fun a : Fin n → Fin m => averageSuccessfulSearchCost a)
      = (fun a => (1 / (n : ℝ))
          * (fun a => ∑ i : Fin n, successfulSearchKeyCost a i) a) := rfl
  rw [key, fintypeExpect_const_mul, hG]
  field_simp

Random hash-function model (universal hashing)

The analysis above randomises key placement: keys hash independently and uniformly. Universal hashing instead fixes the keys and randomises the hash function, drawn uniformly from a family H : ι → (K → Fin m). The family is universal when any two distinct keys collide with probability at most 1/m (CLRS Definition of a universal family, equation (11.4)). From this hypothesis alone we recover the expected collision bound α = n/m and the expected search cost 1 + α (CLRS Theorem 11.3).

A finite family of hash functions H : ι → (K → Fin m) is universal if any two distinct keys collide under a uniformly random member of the family with probability at most 1/m (CLRS equation (11.4)).

def IsUniversal {ι K : Type} [Fintype ι] [DecidableEq ι] {m : Nat}
    (H : ι → (K → Fin m)) : Prop :=
  ∀ x y : K, x ≠ y →
    fintypeExpect (fun t : ι => indicator (H t x = H t y)) ≤ 1 / (m : ℝ)

Expected collisions under universal hashing ≤ α = n/m. Fix a query key x and n stored keys k i, all distinct from x. Under a uniformly random member of a universal family, the expected number of stored keys colliding with x is at most the load factor n/m (CLRS Theorem 11.3).


theorem universal_expected_collisions {ι K : Type} [Fintype ι] [DecidableEq ι]
    {m n : Nat} (H : ι → (K → Fin m)) (hU : IsUniversal H)
    (x : K) (k : Fin n → K) (hk : ∀ i, k i ≠ x) :
    fintypeExpect (fun t : ι => ∑ i : Fin n, indicator (H t x = H t (k i)))
      ≤ (n : ℝ) / (m : ℝ) := by
  rw [fintypeExpect_sum Finset.univ
    (fun (i : Fin n) (t : ι) => indicator (H t x = H t (k i)))]
  calc ∑ i : Fin n, fintypeExpect (fun t : ι => indicator (H t x = H t (k i)))
      ≤ ∑ _i : Fin n, (1 / (m : ℝ)) :=
        Finset.sum_le_sum (fun i _ => hU x (k i) (Ne.symm (hk i)))
    _ = (n : ℝ) / (m : ℝ) := by
        rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
        ring

Expected successful/unsuccessful search cost under universal hashing ≤ 1 + α. One probe plus the expected number of colliding stored keys (CLRS Theorem 11.3, the universal-hashing analogue of Theorems 11.1-11.2).


theorem universal_expected_search_cost {ι K : Type} [Fintype ι] [DecidableEq ι]
    [Nonempty ι] {m n : Nat} (H : ι → (K → Fin m)) (hU : IsUniversal H)
    (x : K) (k : Fin n → K) (hk : ∀ i, k i ≠ x) :
    fintypeExpect (fun t : ι => 1 + ∑ i : Fin n, indicator (H t x = H t (k i)))
      ≤ 1 + (n : ℝ) / (m : ℝ) := by
  have hcard : Fintype.card ι ≠ 0 := Fintype.card_ne_zero
  have key : (fun t : ι => 1 + ∑ i : Fin n, indicator (H t x = H t (k i)))
      = (fun t => (fun _ : ι => (1 : ℝ)) t
          + (fun t => ∑ i : Fin n, indicator (H t x = H t (k i))) t) := rfl
  rw [key, fintypeExpect_add, fintypeExpect_const hcard]
  have hbound := universal_expected_collisions H hU x k hk
  linarith

end Chapter11end CLRS

Definitions and proofs

CLRSLean.Probability.FiniteExpectation

Generic Fintype wrapper.

noncomputable def fintypeExpect {Ω : Type} [Fintype Ω] [DecidableEq Ω] (X : Ω → ℝ) : ℝ :=
  (∑ ω : Ω, X ω) / (Fintype.card Ω : ℝ)

Imports

import Mathlib
import CLRSLean.FourthEdition.Chapter_11.Section_11_2_Chained_Hash_Tables

11.3. Hash Functions

Section 11.2 defines the predicate IsUniversal (CLRS equation (11.4)) and proves, from that hypothesis alone, the universal-hashing costs universal_expected_collisions and universal_expected_search_cost. What was missing is an actual family that satisfies IsUniversal: until now universality was an unwitnessed assumption. This section closes that loop by constructing a concrete universal family and, additionally, records the two deterministic heuristics of CLRS §11.3.1-11.3.2.

Main results:

Definition divisionHash and lemma divisionHash_lt: the division method h(k) = k mod m with its range bound (CLRS §11.3.1).
Definition multiplicationHash and lemma multiplicationHash_lt: the multiplication method h(k) = floor (m * frac (k * A)) with its range bound (CLRS §11.3.2).
Definition affineHash: the prime-field affine family h_{a,b}(k) = a * k + b over the field ZMod p (p prime). This is the number-theoretic dot-product construction of CLRS §11.3.3 in the exact case m = p.
Theorem affineHash_isUniversal: the affine family satisfies IsUniversal (CLRS Theorem 11.5). Two distinct keys collide exactly when the multiplier a is zero, an event of probability 1/p = 1/m, so the collision probability is at most 1/m. This provides the first concrete witness discharging the IsUniversal hypothesis.
Theorems affineHash_expected_collisions and affineHash_expected_search_cost: the §11.2 universal-hashing bounds instantiated on the concrete family, i.e. expected collisions ≤ n/m and expected search cost ≤ 1 + n/m with no IsUniversal hypothesis left open.
Definition affineHashMod and theorem affineHashMod_isUniversal: the full CLRS Theorem 11.5 family for arbitrary m ≤ p, using the outer reduction modulo m.

Status: proved. Both the exact m = p family and the general m ≤ p form exist and instantiate the downstream §11.2 bounds; the deterministic heuristics are recorded with range lemmas.

Notation conventions used in this section:

p : a prime modulus, so ZMod p is a finite field of p elements
m : the table size (m = p for the affine family)
a, b : the slope and intercept of an affine hash h_{a,b}(k) = a * k + b
A : the multiplicative constant in (0, 1) of the multiplication method

Current gaps: none for the mathematical statement of CLRS Theorem 11.5. Operational RAM/probe accounting remains outside this section's advertised boundary.

              namespace CLRSnamespace Chapter11open CLRS.Probability

Deterministic hashing heuristics (CLRS §11.3.1-11.3.2)

The division method (CLRS §11.3.1): map a natural-number key to the remainder k mod m. This is a deterministic hash into {0, …, m-1}.

def divisionHash (m k : ℕ) : ℕ := k % m

The division method lands in the bucket range {0, …, m-1}.

theorem divisionHash_lt (m k : ℕ) (hm : 0 < m) : divisionHash m k < m :=
  Nat.mod_lt _ hm

The multiplication method (CLRS §11.3.2): with a real constant A, take the fractional part of k * A, scale by m, and take the floor. This is a deterministic hash into {0, …, m-1}.

noncomputable def multiplicationHash (m : ℕ) (A : ℝ) (k : ℕ) : ℕ :=
  ⌊(m : ℝ) * Int.fract ((k : ℝ) * A)⌋.toNat

The multiplication method lands in the bucket range {0, …, m-1}.


theorem multiplicationHash_lt (m : ℕ) (A : ℝ) (k : ℕ) (hm : 0 < m) :
    multiplicationHash m A k < m := by
  unfold multiplicationHash
  have hfract_lt : Int.fract ((k : ℝ) * A) < 1 := Int.fract_lt_one _
  have hmpos : (0 : ℝ) < (m : ℝ) := by exact_mod_cast hm
  have hlt : (m : ℝ) * Int.fract ((k : ℝ) * A) < (m : ℝ) := by
    calc (m : ℝ) * Int.fract ((k : ℝ) * A)
        < (m : ℝ) * 1 := by exact mul_lt_mul_of_pos_left hfract_lt hmpos
      _ = (m : ℝ) := by ring
  have h1 : ⌊(m : ℝ) * Int.fract ((k : ℝ) * A)⌋ < (m : ℤ) := by
    rw [Int.floor_lt]; push_cast; exact hlt
  omega

A concrete universal family (CLRS Theorem 11.5)

We construct the prime-field affine family h_{a,b}(k) = a * k + b over the finite field ZMod p. With m = p this is exactly the number-theoretic construction of CLRS §11.3.3. The family is indexed by all pairs (a, b) ∈ ZMod p × ZMod p, drawn uniformly.

Universality is genuinely number-theoretic: for distinct keys x ≠ y, the two hash values agree iff a * (x - y) = 0. In a field this forces a = 0 (since x - y ≠ 0 is a unit), an event of probability exactly 1/p.

The canonical representative of a residue in ZMod p as an element of Fin p, using the value map ZMod.val. This lets the affine family land in the Fin m codomain required by IsUniversal.

def toFin {p : ℕ} [NeZero p] (a : ZMod p) : Fin p := ⟨a.val, ZMod.val_lt a⟩

The representative map ZMod p → Fin p is injective, because ZMod.val is.

theorem toFin_injective {p : ℕ} [NeZero p] : Function.Injective (toFin (p := p)) := by
  intro a b hab
  have hval : a.val = b.val := congrArg Fin.val hab
  exact ZMod.val_injective p hval

The prime-field affine hash family (CLRS §11.3.3, Theorem 11.5, exact m = p case): h_{a,b}(k) = a * k + b, computed in the field ZMod p and represented in Fin p. The index (a, b) ranges over ZMod p × ZMod p.

def affineHash (p : ℕ) [NeZero p] (t : ZMod p × ZMod p) (k : ZMod p) : Fin p :=
  toFin (t.1 * k + t.2)

Theorem (CLRS Theorem 11.5). The prime-field affine family is universal: for any two distinct keys, a uniformly random member collides on them with probability at most 1/m (here m = p).

This is the first concrete witness of the IsUniversal predicate from Section 11.2, so the collision and search-cost bounds there are no longer conditional on an unproven hypothesis.


theorem affineHash_isUniversal (p : ℕ) [NeZero p] (hp : p.Prime) :
    IsUniversal (affineHash p) := by
  haveI : Fact p.Prime := ⟨hp⟩
  intro x y hxy
  -- The collision event `h x = h y` is exactly the event `a = 0`.
  have hiff : ∀ t : ZMod p × ZMod p,
      (affineHash p t x = affineHash p t y) ↔ (t.1 = 0) := by
    intro t
    constructor
    · intro h
      have h2 : t.1 * x + t.2 = t.1 * y + t.2 := toFin_injective h
      have h3 : t.1 * x = t.1 * y := add_right_cancel h2
      have h4 : t.1 * (x - y) = 0 := by rw [mul_sub, h3, sub_self]
      rcases mul_eq_zero.mp h4 with h5 | h5
      · exact h5
      · exact absurd (sub_eq_zero.mp h5) hxy
    · intro h
      show affineHash p t x = affineHash p t y
      unfold affineHash
      rw [h]; simp
  -- Rewrite the collision indicator as the indicator of `a = 0`.
  have hfun :
      (fun t : ZMod p × ZMod p => indicator (affineHash p t x = affineHash p t y))
        = (fun t : ZMod p × ZMod p => indicator (t.1 = 0)) := by
    funext t
    by_cases h : t.1 = 0
    · simp [indicator, (hiff t).mpr h, h]
    · have hne : ¬ (affineHash p t x = affineHash p t y) := fun hc => h ((hiff t).mp hc)
      simp [indicator, hne, h]
  rw [hfun]
  -- The probability that the first coordinate is `0` is `1/card = 1/p`.
  have hcardZ : Fintype.card (ZMod p) ≠ 0 := Fintype.card_ne_zero
  have hmarg := fintypeExpect_fst (Ω₁ := ZMod p) (Ω₂ := ZMod p) hcardZ
    (fun a => indicator (a = 0))
  have hrw : (fun t : ZMod p × ZMod p => indicator (t.1 = 0))
      = (fun t : ZMod p × ZMod p => (fun a : ZMod p => indicator (a = 0)) t.1) := rfl
  rw [hrw, hmarg, fintypeExpect_indicator_singleton, ZMod.card]

Corollary (concrete universal collision bound). Instantiating universal_expected_collisions on the affine family: for a query key x and n stored keys all distinct from x, the expected number of collisions under a uniformly random affine hash is at most the load factor n/m (m = p), with no IsUniversal hypothesis left open.

theorem affineHash_expected_collisions (p : ℕ) [NeZero p] (hp : p.Prime) {n : ℕ}
    (x : ZMod p) (k : Fin n → ZMod p) (hk : ∀ i, k i ≠ x) :
    fintypeExpect (fun t : ZMod p × ZMod p =>
        ∑ i : Fin n, indicator (affineHash p t x = affineHash p t (k i)))
      ≤ (n : ℝ) / (p : ℝ) :=
  universal_expected_collisions (affineHash p) (affineHash_isUniversal p hp) x k hk

Corollary (concrete universal search-cost bound). Instantiating universal_expected_search_cost on the affine family: the expected search cost (one probe plus expected collisions) is at most 1 + n/m (m = p), with no IsUniversal hypothesis left open (CLRS Theorem 11.3).

theorem affineHash_expected_search_cost (p : ℕ) [NeZero p] (hp : p.Prime) {n : ℕ}
    (x : ZMod p) (k : Fin n → ZMod p) (hk : ∀ i, k i ≠ x) :
    fintypeExpect (fun t : ZMod p × ZMod p =>
        1 + ∑ i : Fin n, indicator (affineHash p t x = affineHash p t (k i)))
      ≤ 1 + (n : ℝ) / (p : ℝ) := by
  haveI : Nonempty (ZMod p × ZMod p) := ⟨(0, 0)⟩
  exact universal_expected_search_cost (affineHash p) (affineHash_isUniversal p hp) x k hk

The general mod-`m` affine family (CLRS Theorem 11.5, full form)

The exact m = p construction above reduces each hash value into Fin p. CLRS Theorem 11.5 instead uses a larger prime modulus p and an outer reduction modulo the table size m ≤ p: h_{a,b}(k) = ((a·k + b) mod p) mod m. This subsection formalises that general family and proves it universal.

The proof is the standard counting argument of CLRS. For distinct keys x ≠ y and a nonzero multiplier a, the field values r = a·x + b and s = a·y + b differ (else a·(x - y) = 0 in the field ZMod p); the assignment (a,b) ↦ (r,s) is injective. A collision modulo m therefore corresponds to a pair of distinct residues r ≠ s with r ≡ s (mod m). The number of such residue pairs in {0,…,p-1}² is at most p·(p-1)/m, which gives the collision probability bound 1/m.

The number of s < p strictly greater than r and congruent to r modulo m is at most (p - 1 - r) / m.


lemma count_congruent_gt_le (p m r : ℕ) (hm : 0 < m) (hr : r < p) :
    (((Finset.range p).filter (fun s : ℕ => r < s ∧ s % m = r % m)).card : ℕ)
      ≤ (p - 1 - r) / m := by
  classical
  let f : ℕ → ℕ := fun s => (s - r) / m
  let S : Finset ℕ := (Finset.range p).filter (fun s : ℕ => r < s ∧ s % m = r % m)
  let T : Finset ℕ := Finset.Icc 1 ((p - 1 - r) / m)
  have hMt : Set.MapsTo f (S : Set ℕ) (T : Set ℕ) := by
    intro s hs
    rcases Finset.mem_filter.mp hs with ⟨hsp, hscond⟩
    rcases hscond with ⟨hrs, hmod⟩
    have hslt : s < p := Finset.mem_range.mp hsp
    have hme : s ≡ r [MOD m] := by
      change s % m = r % m
      exact hmod
    have hle : r ≤ s := le_of_lt hrs
    have hdvd : m ∣ s - r := (Nat.modEq_iff_dvd' hle).mp hme.symm
    have hge : m ≤ s - r := by
      obtain ⟨q, hq⟩ := hdvd
      have hne : s - r ≠ 0 := by omega
      have hqpos : 1 ≤ q := by
        by_contra hqn
        have hq0 : q = 0 := by omega
        subst q
        simp at hq
        exact hne hq
      nlinarith
    have hpos : 1 ≤ (s - r) / m := (Nat.le_div_iff_mul_le hm).mpr (by simpa using hge)
    have hsub : s - r ≤ p - 1 - r := by
      have hsp1 : s ≤ p - 1 := by omega
      exact Nat.sub_le_sub_right hsp1 r
    have hle2 : (s - r) / m ≤ (p - 1 - r) / m := Nat.div_le_div_right hsub
    simpa [f, T] using (Finset.mem_Icc.mpr ⟨hpos, hle2⟩)
  have hInj : (S : Set ℕ).InjOn f := by
    intro s hs t ht hf
    have hmes : s ≡ r [MOD m] := by
      have hmod : s % m = r % m := (Finset.mem_filter.mp hs).2.2
      change s % m = r % m
      exact hmod
    have hmet : t ≡ r [MOD m] := by
      have hmod : t % m = r % m := (Finset.mem_filter.mp ht).2.2
      change t % m = r % m
      exact hmod
    have hsle : r ≤ s := le_of_lt (Finset.mem_filter.mp hs).2.1
    have htle : r ≤ t := le_of_lt (Finset.mem_filter.mp ht).2.1
    have hdvdS : m ∣ s - r := (Nat.modEq_iff_dvd' hsle).mp hmes.symm
    have hdvdT : m ∣ t - r := (Nat.modEq_iff_dvd' htle).mp hmet.symm
    have hcal : s - r = t - r := by
      calc s - r = (s - r) / m * m := by rw [Nat.div_mul_cancel hdvdS]
        _ = (t - r) / m * m := by
              change f s * m = f t * m
              rw [hf]
        _ = t - r := by rw [Nat.div_mul_cancel hdvdT]
    omega
  have hle := Finset.card_le_card_of_injOn f hMt hInj
  have hT : T.card = (p - 1 - r) / m := by
    simp [T]
  rwa [hT] at hle

The number of s < p strictly less than r and congruent to r modulo m is at most r / m.


lemma count_congruent_lt_le (p m r : ℕ) (hm : 0 < m) (Variable name `hr` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hr : r < p) :
    (((Finset.range p).filter (fun s : ℕ => s < r ∧ s % m = r % m)).card : ℕ)
      ≤ r / m := by
  classical
  let f : ℕ → ℕ := fun s => (r - s) / m
  let S : Finset ℕ := (Finset.range p).filter (fun s : ℕ => s < r ∧ s % m = r % m)
  let T : Finset ℕ := Finset.Icc 1 (r / m)
  have hMt : Set.MapsTo f (S : Set ℕ) (T : Set ℕ) := by
    intro s hs
    rcases Finset.mem_filter.mp hs with ⟨hsp, hscond⟩
    rcases hscond with ⟨hsr, hmod⟩
    have hme : s ≡ r [MOD m] := by
      change s % m = r % m
      exact hmod
    have hle : s ≤ r := le_of_lt hsr
    have hdvd : m ∣ r - s := (Nat.modEq_iff_dvd' hle).mp hme
    have hge : m ≤ r - s := by
      obtain ⟨q, hq⟩ := hdvd
      have hne : r - s ≠ 0 := by omega
      have hqpos : 1 ≤ q := by
        by_contra hqn
        have hq0 : q = 0 := by omega
        subst q
        simp at hq
        exact hne hq
      nlinarith
    have hpos : 1 ≤ (r - s) / m := (Nat.le_div_iff_mul_le hm).mpr (by simpa using hge)
    have hle2 : (r - s) / m ≤ r / m := Nat.div_le_div_right (Nat.sub_le r s)
    simpa [f, T] using (Finset.mem_Icc.mpr ⟨hpos, hle2⟩)
  have hInj : (S : Set ℕ).InjOn f := by
    intro s hs t ht hf
    have hmes : s ≡ r [MOD m] := by
      have hmod : s % m = r % m := (Finset.mem_filter.mp hs).2.2
      change s % m = r % m
      exact hmod
    have hmet : t ≡ r [MOD m] := by
      have hmod : t % m = r % m := (Finset.mem_filter.mp ht).2.2
      change t % m = r % m
      exact hmod
    have hsle : s ≤ r := le_of_lt (Finset.mem_filter.mp hs).2.1
    have htle : t ≤ r := le_of_lt (Finset.mem_filter.mp ht).2.1
    have hdvdS : m ∣ r - s := (Nat.modEq_iff_dvd' hsle).mp hmes
    have hdvdT : m ∣ r - t := (Nat.modEq_iff_dvd' htle).mp hmet
    have hcal : r - s = r - t := by
      calc r - s = (r - s) / m * m := by rw [Nat.div_mul_cancel hdvdS]
        _ = (r - t) / m * m := by
              change f s * m = f t * m
              rw [hf]
        _ = r - t := by rw [Nat.div_mul_cancel hdvdT]
    omega
  have hle := Finset.card_le_card_of_injOn f hMt hInj
  have hT : T.card = r / m := by
    simp [T]
  rwa [hT] at hle

The number of pairs (r, s) with r < p, s < p, r ≠ s, and r % m = s % m is at most p·(p-1)/m.


lemma congruentPair_count_le (p m : ℕ) (hm : 0 < m) :
    (((Finset.range p).product (Finset.range p)).filter
        (fun rs : ℕ × ℕ => rs.1 ≠ rs.2 ∧ rs.1 % m = rs.2 % m)).card
      ≤ (p : ℝ) * (p - 1 : ℝ) / (m : ℝ) := by
  classical
  let S : ℕ → Finset ℕ := fun r =>
    (Finset.range p).filter (fun s : ℕ => s ≠ r ∧ s % m = r % m)
  have hper : ∀ r ∈ Finset.range p, ((S r).card : ℝ) ≤ (p - 1 : ℝ) / (m : ℝ) := by
    intro r hr
    have hrp : r < p := Finset.mem_range.mp hr
    let Sneg : Finset ℕ := (Finset.range p).filter (fun s : ℕ => s < r ∧ s % m = r % m)
    let Spos : Finset ℕ := (Finset.range p).filter (fun s : ℕ => r < s ∧ s % m = r % m)
    have hsplit : S r = Sneg ∪ Spos := by
      ext s
      constructor
      · intro hs
        rcases Finset.mem_filter.mp hs with ⟨hsp, hne, hmod⟩
        have hslt : s < r ∨ r < s := by omega
        rw [Finset.mem_union]
        rcases hslt with hslt | hslt
        · exact Or.inl (Finset.mem_filter.mpr ⟨hsp, ⟨hslt, hmod⟩⟩)
        · exact Or.inr (Finset.mem_filter.mpr ⟨hsp, ⟨hslt, hmod⟩⟩)
      · intro hs
        rw [Finset.mem_union] at hs
        rcases hs with hs | hs
        · rcases Finset.mem_filter.mp hs with ⟨hsp, hsr, hmod⟩
          exact Finset.mem_filter.mpr ⟨hsp, ⟨ne_of_lt hsr, hmod⟩⟩
        · rcases Finset.mem_filter.mp hs with ⟨hsp, hsr, hmod⟩
          exact Finset.mem_filter.mpr ⟨hsp, ⟨ne_of_gt hsr, hmod⟩⟩
    have hd : Disjoint Sneg Spos := by
      rw [Finset.disjoint_left]
      intro s hsneg hspos
      simp [Sneg, Spos] at hsneg hspos
      omega
    have hcard : (S r).card = Sneg.card + Spos.card := by
      rw [hsplit, Finset.card_union_of_disjoint hd]
    have hb1 : (Spos.card : ℝ) ≤ (p - 1 - r : ℝ) / (m : ℝ) := by
      calc
        (Spos.card : ℝ) ≤ (((p - 1 - r) / m : ℕ) : ℝ) := by
          exact_mod_cast (count_congruent_gt_le p m r hm hrp)
        _ ≤ (p - 1 - r : ℝ) / (m : ℝ) := by
          have hnum : ((p - 1 - r : ℕ) : ℝ) = (p - 1 - r : ℝ) := by
            rw [Nat.cast_sub (by omega : r ≤ p - 1)]
            rw [Nat.cast_sub (by omega : 1 ≤ p), Nat.cast_one]
          rw [← hnum]
          exact Nat.cast_div_le
    have hb2 : (Sneg.card : ℝ) ≤ (r : ℝ) / (m : ℝ) := by
      calc
        (Sneg.card : ℝ) ≤ ((r / m : ℕ) : ℝ) := by
          exact_mod_cast (count_congruent_lt_le p m r hm hrp)
        _ ≤ (r : ℝ) / (m : ℝ) := Nat.cast_div_le
    have hdiv : (r : ℝ) / (m : ℝ) + (p - 1 - r : ℝ) / (m : ℝ) = (p - 1 : ℝ) / (m : ℝ) := by
      rw [← add_div]
      ring
    rw [hcard, Nat.cast_add]
    calc (Sneg.card : ℝ) + (Spos.card : ℝ)
        ≤ (r : ℝ) / (m : ℝ) + (p - 1 - r : ℝ) / (m : ℝ) := add_le_add hb2 hb1
      _ = (p - 1 : ℝ) / (m : ℝ) := hdiv
  have hPsubset : (((Finset.range p).product (Finset.range p)).filter
        (fun rs : ℕ × ℕ => rs.1 ≠ rs.2 ∧ rs.1 % m = rs.2 % m))
      ⊆ (Finset.range p).biUnion (fun r : ℕ => ({r} : Finset ℕ).product (S r)) := by
    intro rs hrs
    rcases Finset.mem_filter.mp hrs with ⟨hrsprod, hne, hmod⟩
    rw [Finset.product_eq_sprod, Finset.mem_product] at hrsprod
    rcases hrsprod with ⟨hrp, hsp⟩
    rw [Finset.mem_biUnion]
    refine ⟨rs.1, hrp, ?_⟩
    rw [Finset.product_eq_sprod, Finset.mem_product]
    refine ⟨Finset.mem_singleton.mpr rfl, ?_⟩
    rw [Finset.mem_filter]
    exact ⟨hsp, hne.symm, hmod.symm⟩
  have hcb := Finset.card_biUnion_le (s := Finset.range p)
    (t := fun r : ℕ => ({r} : Finset ℕ).product (S r))
  calc
    ((((Finset.range p).product (Finset.range p)).filter
        (fun rs : ℕ × ℕ => rs.1 ≠ rs.2 ∧ rs.1 % m = rs.2 % m)).card : ℝ)
        ≤ (((Finset.range p).biUnion (fun r : ℕ => ({r} : Finset ℕ).product (S r))).card : ℝ) := by
            exact_mod_cast (Finset.card_le_card hPsubset)
    _ ≤ (∑ r ∈ (Finset.range p : Finset ℕ), ((({r} : Finset ℕ).product (S r)).card : ℝ)) := by
            exact_mod_cast hcb
    _ = (∑ r ∈ (Finset.range p : Finset ℕ), ((S r).card : ℝ)) := by
            apply Finset.sum_congr rfl
            intro r hr
            simp [This simp argument is unused:
  Finset.card_product

Hint: Omit it from the simp argument list.
  simp ̵[̵F̵i̵n̵s̵e̵t̵.̵c̵a̵r̵d̵_̵p̵r̵o̵d̵u̵c̵t̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Finset.card_product]
    _ ≤ (∑ r ∈ (Finset.range p : Finset ℕ), (p - 1 : ℝ) / (m : ℝ)) := by
            apply Finset.sum_le_sum
            intro r hr
            exact hper r hr
    _ = (p : ℝ) * (p - 1 : ℝ) / (m : ℝ) := by
            rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
            ring

The general mod-m affine family of CLRS Theorem 11.5: h_{a,b}(k) = ((a·k + b) mod p) mod m, computed in the field ZMod p and then reduced modulo the table size m. The index (a,b) ranges over ZMod p × ZMod p with a ≠ 0; the codomain is Fin m.

def affineHashMod (p m : ℕ) [NeZero p] [NeZero m]
    (t : {a : ZMod p // a ≠ 0} × ZMod p) (k : ZMod p) : Fin m :=
  ⟨ZMod.val (t.1.1 * k + t.2) % m, Nat.mod_lt _ (NeZero.pos m)⟩

Theorem (CLRS Theorem 11.5, full mod-m form). The general affine family h_{a,b}(k) = ((a·k + b) mod p) mod m (a ≠ 0) is universal: any two distinct keys collide under a uniformly random member with probability at most 1/m. This refines the exact m = p construction affineHash_isUniversal to arbitrary table sizes m ≤ p.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
theorem affineHashMod_isUniversal (p m : ℕ) [NeZero p] [NeZero m] (hp : p.Prime) :
    IsUniversal (affineHashMod p m) := by
  haveI : Fact p.Prime := ⟨hp⟩
  intro x y hxy
  let B : Finset ({a : ZMod p // a ≠ 0} × ZMod p) :=
    (Finset.univ : Finset ({a : ZMod p // a ≠ 0} × ZMod p)).filter
      (fun t => affineHashMod p m t x = affineHashMod p m t y)
  have hExpect :
      fintypeExpect (fun t : {a : ZMod p // a ≠ 0} × ZMod p =>
        indicator (affineHashMod p m t x = affineHashMod p m t y))
        = (B.card : ℝ) / (Fintype.card ({a : ZMod p // a ≠ 0} × ZMod p) : ℝ) := by
    unfold fintypeExpect indicator
    have hsum : (∑ t : {a : ZMod p // a ≠ 0} × ZMod p,
        (if affineHashMod p m t x = affineHashMod p m t y then (1 : ℝ) else 0))
        = (B.card : ℝ) := by
      simp [B]
    rw [hsum]
  rw [hExpect]
  let φ : ({a : ZMod p // a ≠ 0} × ZMod p) → ℕ × ℕ := fun t =>
    (ZMod.val (t.1.1 * x + t.2), ZMod.val (t.1.1 * y + t.2))
  have hφinj : (B : Set ({a : ZMod p // a ≠ 0} × ZMod p)).InjOn φ := by
    intro t1 ht1 t2 ht2 hφ
    rcases t1 with ⟨a1, b1⟩
    rcases t2 with ⟨a2, b2⟩
    have hfst : ZMod.val (a1.1 * x + b1) = ZMod.val (a2.1 * x + b2) :=
      congrArg Prod.fst hφ
    have hsnd : ZMod.val (a1.1 * y + b1) = ZMod.val (a2.1 * y + b2) :=
      congrArg Prod.snd hφ
    have h1 : a1.1 * x + b1 = a2.1 * x + b2 := ZMod.val_injective p hfst
    have h2 : a1.1 * y + b1 = a2.1 * y + b2 := ZMod.val_injective p hsnd
    have hxy0 : x - y ≠ 0 := sub_ne_zero.mpr hxy
    have hdiff : a1.1 - a2.1 = 0 := by
      have hsub : a1.1 * (x - y) = a2.1 * (x - y) := by
        calc a1.1 * (x - y) = (a1.1 * x + b1) - (a1.1 * y + b1) := by ring
          _ = (a2.1 * x + b2) - (a2.1 * y + b2) := by rw [h1, h2]
          _ = a2.1 * (x - y) := by ring
      have hmul : (a1.1 - a2.1) * (x - y) = 0 := by
        calc (a1.1 - a2.1) * (x - y) = a1.1 * (x - y) - a2.1 * (x - y) := by ring
          _ = 0 := by rw [hsub, sub_self]
      exact (mul_eq_zero.mp hmul).resolve_right hxy0
    have ha : a1.1 = a2.1 := sub_eq_zero.mp hdiff
    have hb : b1 = b2 := by
      have hx : a1.1 * x + b1 = a1.1 * x + b2 := by
        rwa [← ha] at h1
      exact add_left_cancel hx
    exact Prod.ext (Subtype.ext ha) hb
  let C : Finset (ℕ × ℕ) :=
    (Finset.range p).product (Finset.range p) |>.filter
      (fun rs : ℕ × ℕ => rs.1 ≠ rs.2 ∧ rs.1 % m = rs.2 % m)
  have hIm : B.image φ ⊆ C := by
    intro rs hrs
    rcases (Finset.mem_image.mp hrs) with ⟨t, htB, hφt⟩
    rcases t with ⟨a, b⟩
    rw [← hφt]
    change (ZMod.val (a.1 * x + b), ZMod.val (a.1 * y + b)) ∈ C
    have hcoll : affineHashMod p m ⟨a, b⟩ x = affineHashMod p m ⟨a, b⟩ y :=
      (Finset.mem_filter.mp htB).2
    simp [C]
    constructor
    · constructor
      · exact ZMod.val_lt (a.1 * x + b)
      · exact ZMod.val_lt (a.1 * y + b)
    · constructor
      · intro hval
        have h : a.1 * x + b = a.1 * y + b := ZMod.val_injective p hval
        have h' : a.1 * (x - y) = 0 := by
          calc a.1 * (x - y) = (a.1 * x + b) - (a.1 * y + b) := by ring
            _ = 0 := by rw [h, sub_self]
        have hxy0 : x - y ≠ 0 := sub_ne_zero.mpr hxy
        exact a.2 ((mul_eq_zero.mp h').resolve_right hxy0)
      · have hfin : (⟨ZMod.val (a.1 * x + b) % m, Nat.mod_lt _ (NeZero.pos m)⟩ : Fin m)
            = ⟨ZMod.val (a.1 * y + b) % m, Nat.mod_lt _ (NeZero.pos m)⟩ := by
          simpa [affineHashMod] using hcoll
        exact congrArg Fin.val hfin
  have hcardIm : (B.image φ).card = B.card := Finset.card_image_of_injOn hφinj
  have hleC : B.card ≤ C.card := by
    rw [← hcardIm]
    exact Finset.card_le_card hIm
  have hBcard : (B.card : ℝ) ≤ (p : ℝ) * (p - 1 : ℝ) / (m : ℝ) := by
    have hCbound : (C.card : ℝ) ≤ (p : ℝ) * (p - 1 : ℝ) / (m : ℝ) :=
      congruentPair_count_le p m (NeZero.pos m)
    exact le_trans (by exact_mod_cast hleC) hCbound
  have hIcard : (Fintype.card ({a : ZMod p // a ≠ 0} × ZMod p) : ℝ) = (p : ℝ) * (p - 1 : ℝ) := by
    rw [Fintype.card_prod]
    have hne0 : Fintype.card {a : ZMod p // a = 0} = 1 := by
      rw [Fintype.card_subtype_eq]
    have h1 : Fintype.card {a : ZMod p // a ≠ 0} = p - 1 := by
      have hc := Fintype.card_subtype_compl (p := fun a : ZMod p => a = 0)
      rw [hne0, ZMod.card] at hc
      try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [ne_eq, eq_comm] using hc
    rw [h1, ZMod.card]
    rw [Nat.cast_mul]
    rw [Nat.cast_sub hp.one_le]
    ring
  have hmne : (m : ℝ) ≠ 0 := by exact_mod_cast (NeZero.ne m)
  have hIpos : 0 < (p : ℝ) * (p - 1 : ℝ) := by
    have hp2 : (2 : ℝ) ≤ (p : ℝ) := by exact_mod_cast hp.two_le
    nlinarith
  have hdiv : (B.card : ℝ) / ((p : ℝ) * (p - 1 : ℝ)) ≤ 1 / (m : ℝ) := by
    rw [div_le_iff₀ hIpos]
    calc (B.card : ℝ) ≤ (p : ℝ) * (p - 1 : ℝ) / (m : ℝ) := hBcard
      _ = (1 : ℝ) / (m : ℝ) * ((p : ℝ) * (p - 1 : ℝ)) := by
        field_simp [hmne]
  rw [hIcard]
  exact hdiv

end Chapter11end CLRS

Imports

import Mathlib

11.4. Open Addressing

Open addressing stores every key directly in the table Fin m → Option K (no chains). Each key k has a probe sequence ⟨h(k,0), h(k,1), …, h(k,m-1)⟩, a permutation of the slots; a search or insertion walks the probe order until it finds the key (success), an empty slot (stop), or exhausts the table.

This section formalises three layers.

Main results:

Functional model (CLRS §11.4 operational layer).
- openInsert / openSearch: insert into the first empty slot along the probe order; search until the key or the first empty slot.
- Theorem openSearch_eq_false_of_absent: a key that is nowhere in the table is not found (absent key not found).
- Theorem openSearch_openInsert: after inserting a key along a duplicate-free probe order that has an empty slot, a search finds it (inserted key is found).
Probe schemes (CLRS §11.4, equations (11.5)-(11.7)).
- linearProbe, quadraticProbe, doubleHashProbe over ZMod m.
- Theorem linearProbe_bijective: linear probing enumerates every slot.
- Theorem doubleHashProbe_bijective: double hashing enumerates every slot when the second hash is a unit (coprime to m, CLRS requirement).
- Theorem quadraticProbe_zero: quadratic probing starts at the base slot.
Expected-probe bounds under uniform hashing (CLRS Theorems 11.6-11.8).
- probeTail: the uniform-hashing probability that the first i probes of an unsuccessful search all hit occupied slots, the without-replacement product ∏_{j<i} (n-j)/(m-j) (CLRS §11.4).
- Theorem probeTail_le_pow: each such probability is at most α^i, the per-factor bound (n-j)/(m-j) ≤ n/m that CLRS uses.
- Theorem expectedUnsuccessfulProbes_le: expected unsuccessful-search probes ≤ 1/(1-α) (CLRS Theorem 11.6), as the tail-sum ∑_i probeTail.
- Theorem expectedInsertionProbes_le: the same 1/(1-α) bound for an insertion (CLRS Corollary 11.7).
- Theorem expectedSuccessfulProbes_le: expected successful-search probes ≤ (1/α) * ∑_{j<n} 1/(m-j) = (1/α)(H_m - H_{m-n}), the harmonic form of CLRS Theorem 11.8.
- Theorem expectedSuccessfulProbes_le_ln: expected successful-search probes ≤ (1/α) * ln(1/(1-α)), the logarithmic (closed-form) version of CLRS Theorem 11.8.

Status: proved for the functional model, the probe schemes, and the uniform-hashing expected-probe bounds.

Notation conventions used in this section:

m : the number of table slots
n : the number of stored keys; α = n/m is the load factor (openLoadFactor)
K : the key type; a slot is Option K (none = empty)
probeTail m n i : P[first i probes all occupied], the uniform-hashing tail
H_k : the k-th harmonic number ∑_{r=1}^{k} 1/r

The companion UniformProbe development derives the without-replacement tails from an explicit uniform permutation sample space and identifies their tail sum with the actual first-empty-slot probe count. The upper bounds retain their non-full-load hypotheses; the logarithmic successful-search bound requires 0 < n < m. Successful expectation averages insertion-time occupancies. RAM and cache costs remain outside this model.

namespace CLRSnamespace Chapter11

Functional open-addressing model

The table maps each of the m slots to Option K (none = empty). A probe order is a List of slots (the slot type is left abstract; the probe schemes below instantiate it at ZMod m). scanFind and scanInsertPos walk a probe order once.

Walk a probe order looking for k, stopping at the first empty slot: return true if a slot holding k is reached before any empty slot (open-addressing search semantics).

def scanFind {S K : Type*} [DecidableEq K] (T : S → Option K) (k : K) :
    List S → Bool
  | [] => false
  | s :: rest =>
      if T s = some k then true
      else if T s = none then false
      else scanFind T k rest

Walk a probe order returning the first empty slot, or none if the order has no empty slot (table full along this probe order).

def scanInsertPos {S K : Type*} [DecidableEq K] (T : S → Option K) :
    List S → Option S
  | [] => none
  | s :: rest => if T s = none then some s else scanInsertPos T rest

Open-addressing search along a probe order.

def openSearch {S K : Type*} [DecidableEq K] (T : S → Option K)
    (order : List S) (k : K) : Bool :=
  scanFind T k order

Open-addressing insert along a probe order: place the key in the first empty slot. If the probe order has no empty slot the table is returned unchanged (the table-full junk value; totality over Option-slot tables).

def openInsert {S K : Type*} [DecidableEq S] [DecidableEq K] (T : S → Option K)
    (order : List S) (k : K) : S → Option K :=
  match scanInsertPos T order with
  | some s => Function.update T s (some k)
  | none => T

Model correctness (CLRS §11.4 insert/search behaviour)

If a key occupies no slot, an open-addressing search along any probe order fails.

theorem scanFind_absent {S K : Type*} [DecidableEq K] (T : S → Option K) (k : K)
    (h : ∀ s, T s ≠ some k) (order : List S) : scanFind T k order = false := by
  induction order with
  | nil => rfl
  | cons s rest ih =>
      simp only [scanFind, if_neg (h s)]
      by_cases he : T s = none
      · simp [he]
      · simp only [if_neg he]; exact ih

The first empty slot reported by scanInsertPos is a member of the probe order.


theorem scanInsertPos_mem {S K : Type*} [DecidableEq K] (T : S → Option K)
    (order : List S) (s : S) (h : scanInsertPos T order = some s) : s ∈ order := by
  induction order with
  | nil => simp [scanInsertPos] at h
  | cons a rest ih =>
      simp only [scanInsertPos] at h
      by_cases ha : T a = none
      · rw [if_pos ha, Option.some_inj] at h
        subst h; simp
      · rw [if_neg ha] at h
        exact List.mem_cons_of_mem _ (ih h)

If the probe order has an empty slot, scanInsertPos reports one.


theorem scanInsertPos_isSome_of_empty {S K : Type*} [DecidableEq K]
    (T : S → Option K) (order : List S) (h : ∃ s ∈ order, T s = none) :
    ∃ s, scanInsertPos T order = some s := by
  induction order with
  | nil => obtain ⟨s, hs, _⟩ := h; simp at hs
  | cons a rest ih =>
      by_cases ha : T a = none
      · exact ⟨a, by simp [scanInsertPos, ha]⟩
      · obtain ⟨s, hs, hTs⟩ := h
        rw [List.mem_cons] at hs
        rcases hs with rfl | hmem
        · exact absurd hTs ha
        · obtain ⟨s', hs'⟩ := ih ⟨s, hmem, hTs⟩
          exact ⟨s', by simp only [scanInsertPos, if_neg ha]; exact hs'⟩

After inserting a key into the first empty slot of a duplicate-free probe order, a search along that order finds it.


theorem scanFind_update_of_scanInsertPos {S K : Type*} [DecidableEq S]
    [DecidableEq K] (T : S → Option K) (k : K) (order : List S) (s : S)
    (hnd : order.Nodup) (hins : scanInsertPos T order = some s) :
    scanFind (Function.update T s (some k)) k order = true := by
  induction order with
  | nil => simp [scanInsertPos] at hins
  | cons a rest ih =>
      simp only [scanInsertPos] at hins
      by_cases ha : T a = none
      · rw [if_pos ha, Option.some_inj] at hins
        subst hins
        simp [scanFind, Function.update_self]
      · rw [if_neg ha] at hins
        have hmem : s ∈ rest := scanInsertPos_mem T rest s hins
        have hnd' := List.nodup_cons.mp hnd
        have has : a ≠ s := fun hEq => hnd'.1 (hEq ▸ hmem)
        simp only [scanFind, Function.update_of_ne has]
        by_cases hak : T a = some k
        · rw [if_pos hak]
        · rw [if_neg hak, if_neg ha]
          exact ih hnd'.2 hins

AC-1 (absent key not found). A key stored in no slot is not found by an open-addressing search along any probe order.

theorem openSearch_eq_false_of_absent {S K : Type*} [DecidableEq K]
    (T : S → Option K) (order : List S) (k : K) (h : ∀ s, T s ≠ some k) :
    openSearch T order k = false :=
  scanFind_absent T k h order

AC-1 (inserted key found). If a duplicate-free probe order has an empty slot, then after inserting a key it is found by a search along the same order.


theorem openSearch_openInsert {S K : Type*} [DecidableEq S] [DecidableEq K]
    (T : S → Option K) (order : List S) (k : K) (hnd : order.Nodup)
    (hempty : ∃ s ∈ order, T s = none) :
    openSearch (openInsert T order k) order k = true := by
  obtain ⟨s, hs⟩ := scanInsertPos_isSome_of_empty T order hempty
  have hupd : openInsert T order k = Function.update T s (some k) := by
    simp only [openInsert, hs]
  rw [openSearch, hupd]
  exact scanFind_update_of_scanInsertPos T k order s hnd hs

Probe schemes (CLRS §11.4, equations (11.5)-(11.7))

Each scheme is a function ZMod m → ZMod m mapping a probe number i to a slot, for a fixed key. CLRS requires each probe sequence to enumerate all m slots (be a permutation); linear probing always does, and double hashing does when the step size is a unit modulo m.

Linear probing (CLRS equation (11.5)): h(k,i) = (h'(k) + i) mod m.

def linearProbe {m : ℕ} (h0 : ZMod m) (i : ZMod m) : ZMod m := h0 + i

Quadratic probing (CLRS equation (11.6)): h(k,i) = (h'(k) + c₁ i + c₂ i²) mod m.

def quadraticProbe {m : ℕ} (h0 c1 c2 : ZMod m) (i : ZMod m) : ZMod m :=
  h0 + c1 * i + c2 * i * i

Double hashing (CLRS equation (11.7)): h(k,i) = (h₁(k) + i · h₂(k)) mod m.

def doubleHashProbe {m : ℕ} (h1 h2 : ZMod m) (i : ZMod m) : ZMod m := h1 + i * h2

Linear probing enumerates every slot: as a function of the probe number it is a bijection of ZMod m (CLRS: a linear probe sequence is a permutation).

theorem linearProbe_bijective {m : ℕ} (h0 : ZMod m) :
    Function.Bijective (linearProbe h0) := by
  refine Function.bijective_iff_has_inverse.mpr ⟨fun t => t - h0, ?_, ?_⟩
  · intro i; show (h0 + i) - h0 = i; ring
  · intro t; show h0 + (t - h0) = t; ring

Linear probing covers every slot (surjectivity form of the permutation property).

theorem linearProbe_surjective {m : ℕ} (h0 : ZMod m) :
    Function.Surjective (linearProbe h0) :=
  (linearProbe_bijective h0).surjective

Double hashing enumerates every slot when the step h₂ is a unit modulo m (CLRS: h₂(k) must be relatively prime to m for the probe sequence to be a permutation).


theorem doubleHashProbe_bijective {m : ℕ} (h1 h2 : ZMod m) (hu : IsUnit h2) :
    Function.Bijective (doubleHashProbe h1 h2) := by
  obtain ⟨u, rfl⟩ := hu
  refine Function.bijective_iff_has_inverse.mpr ⟨fun t => (t - h1) * ↑u⁻¹, ?_, ?_⟩
  · intro i
    show ((doubleHashProbe h1 (↑u) i) - h1) * ↑u⁻¹ = i
    have hu1 : (↑u : ZMod m) * ↑u⁻¹ = 1 := u.mul_inv
    unfold doubleHashProbe
    calc (h1 + i * ↑u - h1) * ↑u⁻¹ = i * (↑u * ↑u⁻¹) := by ring
      _ = i := by rw [hu1, mul_one]
  · intro t
    show doubleHashProbe h1 (↑u) ((t - h1) * ↑u⁻¹) = t
    have hu2 : (↑u⁻¹ : ZMod m) * ↑u = 1 := u.inv_mul
    unfold doubleHashProbe
    calc h1 + (t - h1) * ↑u⁻¹ * ↑u = h1 + (t - h1) * (↑u⁻¹ * ↑u) := by ring
      _ = t := by rw [hu2, mul_one]; ring

Double hashing covers every slot when the step is a unit.

theorem doubleHashProbe_surjective {m : ℕ} (h1 h2 : ZMod m) (hu : IsUnit h2) :
    Function.Surjective (doubleHashProbe h1 h2) :=
  (doubleHashProbe_bijective h1 h2 hu).surjective

Quadratic probing starts at the base slot h'(k) (probe number 0).

theorem quadraticProbe_zero {m : ℕ} (h0 c1 c2 : ZMod m) :
    quadraticProbe h0 c1 c2 0 = h0 := by
  unfold quadraticProbe; ring

Expected number of probes under uniform hashing (CLRS Theorems 11.6-11.8)

Under the uniform-hashing assumption the probe sequence of each key is equally likely to be any of the m! permutations of the slots. For an unsuccessful search with n occupied slots, the probability that the first i probes all hit occupied slots is the without-replacement product ∏_{j<i} (n-j)/(m-j). The expected number of probes is the tail-sum E[X] = ∑_{i≥0} P[X > i], which we bound by the geometric series ∑_i α^i = 1/(1-α) via CLRS's per-factor bound (n-j)/(m-j) ≤ n/m.

The load factor α = n/m of an open-addressing table.

noncomputable def openLoadFactor (m n : ℕ) : ℝ := (n : ℝ) / (m : ℝ)

Under uniform hashing, probeTail m n i is the probability that the first i probes of an unsuccessful search all hit occupied slots: the without-replacement product ∏_{j<i} (n-j)/(m-j) (CLRS §11.4, the factors leading to Theorem 11.6).

noncomputable def probeTail (m n i : ℕ) : ℝ :=
  ∏ j ∈ Finset.range i, ((n : ℝ) - (j : ℝ)) / ((m : ℝ) - (j : ℝ))

No probe is needed with certainty: probeTail _ _ 0 = 1.

theorem probeTail_zero (m n : ℕ) : probeTail m n 0 = 1 := by
  simp [probeTail]

The one-step recurrence of the tail probability.

theorem probeTail_succ (m n i : ℕ) :
    probeTail m n (i + 1)
      = probeTail m n i * (((n : ℝ) - (i : ℝ)) / ((m : ℝ) - (i : ℝ))) := by
  simp only [probeTail, Finset.prod_range_succ]

The tail probabilities are nonnegative (for i ≤ m, where all denominators are positive).


theorem probeTail_nonneg (m n : ℕ) (hnm : n ≤ m) (i : ℕ) (Variable name `hi` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hi : i ≤ m) :
    0 ≤ probeTail m n i := by
  by_cases hin : i ≤ n
  · apply Finset.prod_nonneg
    intro j hj
    have hji : j < i := Finset.mem_range.mp hj
    have hjn : (j : ℝ) ≤ (n : ℝ) := by
      have : j ≤ n := le_trans (Nat.le_of_lt hji) hin
      exact_mod_cast this
    have hjm : (j : ℝ) < (m : ℝ) := by
      have : j < m := lt_of_lt_of_le hji (le_trans hin hnm)
      exact_mod_cast this
    apply div_nonneg <;> linarith
  · have hni : n < i := not_le.mp hin
    have hmem : n ∈ Finset.range i := Finset.mem_range.mpr hni
    have hz : probeTail m n i = 0 := by
      rw [probeTail]; exact Finset.prod_eq_zero hmem (by simp)
    simp [hz]

CLRS per-factor bound. Each tail probability is at most α^i (α = n/m), because (n-j)/(m-j) ≤ n/m. This is the heart of Theorem 11.6.


theorem probeTail_le_pow (m n : ℕ) (hnm : n ≤ m) (i : ℕ) (hi : i ≤ m) :
    probeTail m n i ≤ (openLoadFactor m n) ^ i := by
  induction i with
  | zero => rw [probeTail_zero, pow_zero]
  | succ i ih =>
      have hile : i ≤ m := le_of_lt (Nat.lt_of_succ_le hi)
      have him : i < m := Nat.lt_of_succ_le hi
      have hprev : probeTail m n i ≤ (openLoadFactor m n) ^ i := ih hile
      have hptnn : 0 ≤ probeTail m n i := probeTail_nonneg m n hnm i hile
      have hmpos : (0 : ℝ) < (m : ℝ) := by
        have : 0 < m := lt_of_le_of_lt (Nat.zero_le i) him
        exact_mod_cast this
      have hden : (0 : ℝ) < (m : ℝ) - (i : ℝ) := by
        have : (i : ℝ) < (m : ℝ) := by exact_mod_cast him
        linarith
      have hαnn : 0 ≤ openLoadFactor m n := by
        rw [openLoadFactor]; exact div_nonneg (by positivity) (by positivity)
      rw [probeTail_succ, pow_succ]
      by_cases hin : i < n
      · have hile_n : (i : ℝ) ≤ (n : ℝ) := by exact_mod_cast Nat.le_of_lt hin
        have hfnn : 0 ≤ ((n : ℝ) - (i : ℝ)) / ((m : ℝ) - (i : ℝ)) :=
          div_nonneg (by linarith) (le_of_lt hden)
        have hfle : ((n : ℝ) - (i : ℝ)) / ((m : ℝ) - (i : ℝ)) ≤ openLoadFactor m n := by
          rw [openLoadFactor, div_le_div_iff₀ hden hmpos]
          have hnr : (n : ℝ) ≤ (m : ℝ) := by exact_mod_cast hnm
          have hir : (0 : ℝ) ≤ (i : ℝ) := by positivity
          nlinarith [mul_le_mul_of_nonneg_right hnr hir]
        exact mul_le_mul hprev hfle hfnn (pow_nonneg hαnn i)
      · have hni : n ≤ i := not_lt.mp hin
        have hnum : (n : ℝ) - (i : ℝ) ≤ 0 := by
          have : (n : ℝ) ≤ (i : ℝ) := by exact_mod_cast hni
          linarith
        have hinv : 0 ≤ ((m : ℝ) - (i : ℝ))⁻¹ := inv_nonneg.mpr (le_of_lt hden)
        have hfnp : ((n : ℝ) - (i : ℝ)) / ((m : ℝ) - (i : ℝ)) ≤ 0 := by
          rw [div_eq_mul_inv]; nlinarith [hnum, hinv]
        have hprod : probeTail m n i * (((n : ℝ) - (i : ℝ)) / ((m : ℝ) - (i : ℝ))) ≤ 0 := by
          nlinarith [hptnn, hfnp]
        have hpow : 0 ≤ (openLoadFactor m n) ^ i * openLoadFactor m n :=
          mul_nonneg (pow_nonneg hαnn i) hαnn
        linarith

A partial geometric sum is bounded by the full geometric series ∑_i α^i ≤ 1/(1-α) for 0 ≤ α < 1.


theorem geom_sum_le_inv (α : ℝ) (h0 : 0 ≤ α) (h1 : α < 1) (N : ℕ) :
    ∑ i ∈ Finset.range N, α ^ i ≤ 1 / (1 - α) := by
  have hpos : (0 : ℝ) < 1 - α := by linarith
  have hid : (∑ i ∈ Finset.range N, α ^ i) * (1 - α) = 1 - α ^ N := by
    have h := geom_sum_mul α N
    linear_combination (-1 : ℝ) * h
  rw [le_div_iff₀ hpos, hid]
  have hpN : (0 : ℝ) ≤ α ^ N := pow_nonneg h0 N
  linarith

The expected number of probes for an unsuccessful search under uniform hashing, as the tail-sum E[X] = ∑_{i} P[X > i] of the probe count X.

noncomputable def expectedUnsuccessfulProbes (m n : ℕ) : ℝ :=
  ∑ i ∈ Finset.range (m + 1), probeTail m n i

Theorem 11.6 (unsuccessful search). Under uniform hashing the expected number of probes in an unsuccessful search is at most 1/(1-α) (α = n/m < 1), proved as the tail-sum bounded by the geometric series.


theorem expectedUnsuccessfulProbes_le (m n : ℕ) (hn : n < m) :
    expectedUnsuccessfulProbes m n ≤ 1 / (1 - openLoadFactor m n) := by
  have hnm : n ≤ m := le_of_lt hn
  have hmpos : 0 < m := lt_of_le_of_lt (Nat.zero_le n) hn
  have hmr : (0 : ℝ) < (m : ℝ) := by exact_mod_cast hmpos
  have hα0 : 0 ≤ openLoadFactor m n :=
    div_nonneg (by positivity) (by positivity)
  have hα1 : openLoadFactor m n < 1 := by
    rw [openLoadFactor, div_lt_one hmr]; exact_mod_cast hn
  calc expectedUnsuccessfulProbes m n
      = ∑ i ∈ Finset.range (m + 1), probeTail m n i := rfl
    _ ≤ ∑ i ∈ Finset.range (m + 1), (openLoadFactor m n) ^ i := by
        apply Finset.sum_le_sum
        intro i hi
        exact probeTail_le_pow m n hnm i (Nat.lt_succ_iff.mp (Finset.mem_range.mp hi))
    _ ≤ 1 / (1 - openLoadFactor m n) := geom_sum_le_inv _ hα0 hα1 (m + 1)

Corollary 11.7 (insertion). Inserting a key probes exactly as an unsuccessful search does, so its expected number of probes is at most 1/(1-α).

theorem expectedInsertionProbes_le (m n : ℕ) (hn : n < m) :
    expectedUnsuccessfulProbes m n ≤ 1 / (1 - openLoadFactor m n) :=
  expectedUnsuccessfulProbes_le m n hn

The expected number of probes for a successful search under uniform hashing: averaging, over the n insertion times j = 0, …, n-1, the expected unsuccessful-search cost in a table already holding j keys (CLRS proof of Theorem 11.8: the (j+1)-st key's probe cost equals an unsuccessful search among j keys).

noncomputable def expectedSuccessfulProbes (m n : ℕ) : ℝ :=
  (1 / (n : ℝ)) * ∑ j ∈ Finset.range n, expectedUnsuccessfulProbes m j

Theorem 11.8 (successful search), harmonic form. Under uniform hashing the expected number of probes in a successful search is at most (1/α) * ∑_{j<n} 1/(m-j) = (1/α)(H_m - H_{m-n}) (α = n/m). The stated harmonic-sum bound is proved; the classical (1/α) ln(1/(1-α)) follows via sum_inv_shift_le_log and is proved as expectedSuccessfulProbes_le_ln.


theorem expectedSuccessfulProbes_le (m n : ℕ) (hn : n ≤ m) (hnpos : 0 < n) :
    expectedSuccessfulProbes m n
      ≤ (1 / openLoadFactor m n) * ∑ j ∈ Finset.range n, 1 / ((m : ℝ) - (j : ℝ)) := by
  have hmpos : 0 < m := lt_of_lt_of_le hnpos hn
  have hmpos' : (0 : ℝ) < (m : ℝ) := by exact_mod_cast hmpos
  have step1 : expectedSuccessfulProbes m n
      ≤ (1 / (n : ℝ)) * ∑ j ∈ Finset.range n, 1 / (1 - openLoadFactor m j) := by
    unfold expectedSuccessfulProbes
    apply mul_le_mul_of_nonneg_left _ (by positivity)
    apply Finset.sum_le_sum
    intro j hj
    exact expectedUnsuccessfulProbes_le m j (lt_of_lt_of_le (Finset.mem_range.mp hj) hn)
  have hrw : ∀ j ∈ Finset.range n,
      1 / (1 - openLoadFactor m j) = (m : ℝ) * (1 / ((m : ℝ) - (j : ℝ))) := by
    intro j hj
    have hjm : j < m := lt_of_lt_of_le (Finset.mem_range.mp hj) hn
    have hjmr : (j : ℝ) < (m : ℝ) := by exact_mod_cast hjm
    have hm0 : (m : ℝ) ≠ 0 := ne_of_gt hmpos'
    have hsub : (1 : ℝ) - (j : ℝ) / (m : ℝ) = ((m : ℝ) - (j : ℝ)) / (m : ℝ) := by
      rw [sub_div, div_self hm0]
    rw [openLoadFactor, hsub, one_div_div, mul_one_div]
  rw [Finset.sum_congr rfl hrw, ← Finset.mul_sum] at step1
  have hfin : (1 / (n : ℝ)) * ((m : ℝ) * ∑ j ∈ Finset.range n, 1 / ((m : ℝ) - (j : ℝ)))
      = (1 / openLoadFactor m n) * ∑ j ∈ Finset.range n, 1 / ((m : ℝ) - (j : ℝ)) := by
    rw [openLoadFactor, one_div_div]; ring
  rw [hfin] at step1
  exact step1

The free-capacity identity 1/(1 - n/m) = m/(m-n) for a non-full table (n < m): the reciprocal of the free capacity equals the ratio of the table size to the remaining slots. This is the ln(1/(1-α)) = ln(m/(m-n)) identity used to pass from the harmonic sum bound to the logarithmic form of Theorem 11.8.


lemma openLoadFactor_inv_eq (m n : ℕ) (hn : n < m) :
    (1 : ℝ) / (1 - (n : ℝ) / (m : ℝ)) = (m : ℝ) / ((m - n : ℕ) : ℝ) := by
  have hmpos : (0 : ℝ) < (m : ℝ) := by exact_mod_cast (lt_of_le_of_lt (Nat.zero_le n) hn)
  have hmne : (m : ℝ) ≠ 0 := ne_of_gt hmpos
  have hmncast : ((m - n : ℕ) : ℝ) = (m : ℝ) - (n : ℝ) := by
    rw [Nat.cast_sub (le_of_lt hn)]
  rw [hmncast]
  have hsub : (m : ℝ) - (n : ℝ) ≠ 0 := by
    have : (n : ℝ) < (m : ℝ) := by exact_mod_cast hn
    linarith
  have hαne : 1 - (n : ℝ) / (m : ℝ) ≠ 0 := by
    have hα : (n : ℝ) / (m : ℝ) < 1 := (div_lt_one hmpos).2 (by exact_mod_cast hn)
    linarith
  field_simp [hmne, hsub, hαne]

Harmonic-sum bound. For n < m, ∑_{j<n} 1/(m-j) ≤ ln(m/(m-n)): each term 1/(m-j) is at most ln((m-j)/(m-j-1)) (from the bound ln(1+x) ≥ x/(1+x) with x = 1/(m-j-1)), and the resulting sum telescopes to ln(m/(m-n)). This is the integral bound used to obtain the logarithmic form of Theorem 11.8 from its harmonic form.


lemma sum_inv_shift_le_log (m n : ℕ) (hn : n < m) :
    (∑ j ∈ Finset.range n, (1 : ℝ) / ((m : ℝ) - (j : ℝ)))
      ≤ Real.log ((m : ℝ) / ((m - n : ℕ) : ℝ)) := by
  classical
  have hterm (j : ℕ) (hj : j < n) : (1 : ℝ) / ((m : ℝ) - (j : ℝ))
      ≤ Real.log (((m : ℝ) - (j : ℝ)) / (((m : ℝ) - (j : ℝ)) - 1)) := by
    have hsucc : j + 1 < m := by omega
    have hjm1 : (j : ℝ) + 1 < (m : ℝ) := by exact_mod_cast hsucc
    have hden : 0 < ((m : ℝ) - (j : ℝ)) - 1 := by linarith
    have hnum : 0 < (m : ℝ) - (j : ℝ) := by linarith
    have hx : 0 < ((m : ℝ) - (j : ℝ)) / (((m : ℝ) - (j : ℝ)) - 1) := div_pos hnum hden
    have h := Real.one_sub_inv_le_log_of_pos hx
    have hlin : (1 : ℝ) - (((m : ℝ) - (j : ℝ)) / (((m : ℝ) - (j : ℝ)) - 1))⁻¹
        = (1 : ℝ) / ((m : ℝ) - (j : ℝ)) := by
      field_simp [hnum.ne', hden.ne']
      ring
    rwa [hlin] at h
  calc
    (∑ j ∈ Finset.range n, (1 : ℝ) / ((m : ℝ) - (j : ℝ)))
        ≤ ∑ j ∈ Finset.range n,
            Real.log (((m : ℝ) - (j : ℝ)) / (((m : ℝ) - (j : ℝ)) - 1)) := by
            apply Finset.sum_le_sum
            intro j hj
            exact hterm j (Finset.mem_range.mp hj)
    _ = Real.log ((m : ℝ) / ((m - n : ℕ) : ℝ)) := by
          have hsplit : ∀ j ∈ Finset.range n,
              Real.log (((m : ℝ) - (j : ℝ)) / (((m : ℝ) - (j : ℝ)) - 1))
                = Real.log ((m : ℝ) - (j : ℝ)) - Real.log (((m : ℝ) - (j : ℝ)) - 1) := by
            intro j hj
            have hjn : j < n := Finset.mem_range.mp hj
            have hsucc : j + 1 < m := by omega
            have hjm1 : (j : ℝ) + 1 < (m : ℝ) := by exact_mod_cast hsucc
            have hden : 0 < ((m : ℝ) - (j : ℝ)) - 1 := by linarith
            have hnum : 0 < (m : ℝ) - (j : ℝ) := by linarith
            exact Real.log_div hnum.ne' hden.ne'
          rw [Finset.sum_congr rfl hsplit]
          have htel : (∑ j ∈ Finset.range n,
                (Real.log ((m : ℝ) - (j : ℝ)) - Real.log (((m : ℝ) - (j : ℝ)) - 1)))
              = Real.log ((m : ℝ) - (0 : ℝ)) - Real.log ((m : ℝ) - (n : ℝ)) := by
            simpa [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub] using
              (Finset.sum_range_sub' (f := fun i : ℕ => Real.log ((m : ℝ) - (i : ℝ))) n)
          rw [htel, sub_zero, ← Nat.cast_sub (le_of_lt hn)]
          have hm : (m : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt (lt_of_le_of_lt (Nat.zero_le n) hn))
          have hmn : ((m - n : ℕ) : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt (Nat.sub_pos_of_lt hn))
          rw [← Real.log_div hm hmn]

Theorem 11.8 (successful search), logarithmic form. Under uniform hashing the expected number of probes in a successful search is at most (1/α) * ln(1/(1-α)) (α = n/m < 1), obtained from the harmonic form expectedSuccessfulProbes_le via the integral bound ∑_{j<n} 1/(m-j) ≤ ln(m/(m-n)) = ln(1/(1-α)).


theorem expectedSuccessfulProbes_le_ln (m n : ℕ) (hn : n < m) (hnpos : 0 < n) :
    expectedSuccessfulProbes m n
      ≤ (1 / openLoadFactor m n) * Real.log (1 / (1 - openLoadFactor m n)) := by
  have hharm := expectedSuccessfulProbes_le m n (le_of_lt hn) hnpos
  have hlog : (∑ j ∈ Finset.range n, (1 : ℝ) / ((m : ℝ) - (j : ℝ)))
      ≤ Real.log ((m : ℝ) / ((m - n : ℕ) : ℝ)) := sum_inv_shift_le_log m n hn
  have hαpos : 0 < openLoadFactor m n := by
    rw [openLoadFactor]
    exact div_pos (by exact_mod_cast hnpos) (by exact_mod_cast (lt_of_le_of_lt (Nat.zero_le n) hn))
  have hαnonneg : 0 ≤ 1 / openLoadFactor m n := by
    exact one_div_nonneg.mpr (le_of_lt hαpos)
  have hconv : Real.log (1 / (1 - openLoadFactor m n)) = Real.log ((m : ℝ) / ((m - n : ℕ) : ℝ)) := by
    congr 1
    rw [openLoadFactor]
    exact openLoadFactor_inv_eq m n hn
  have hmult := mul_le_mul_of_nonneg_left hlog hαnonneg
  calc
    expectedSuccessfulProbes m n
        ≤ (1 / openLoadFactor m n) * ∑ j ∈ Finset.range n, 1 / ((m : ℝ) - (j : ℝ)) := hharm
    _ ≤ (1 / openLoadFactor m n) * Real.log ((m : ℝ) / ((m - n : ℕ) : ℝ)) := hmult
    _ = (1 / openLoadFactor m n) * Real.log (1 / (1 - openLoadFactor m n)) := by rw [hconv]

end Chapter11end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_11.Section_11_4_Open_Addressing.UniformProbe.Counting

CLRS Section 11.4 - Counting uniform probe prefixes

We restrict a slot permutation to its first i positions. The symmetric group acts transitively on these prefix embeddings, so every embedding has the same number of permutation extensions. Counting all embeddings determines that extension count and then the number whose range lies in the occupied set.

namespace CLRSnamespace Chapter11

Inclusion of the first i probe positions into a table of size m.

def probePrefixEmbedding {m i : Nat} (hi : i ≤ m) : Fin i ↪ Fin m :=
  Fin.castLEEmb hi

Restriction of a full probe permutation to its first i positions.

def probePermutationPrefix {m i : Nat} (hi : i ≤ m)
    (σ : Equiv.Perm (Fin m)) : Fin i ↪ Fin m :=
  (probePrefixEmbedding hi).trans σ.toEmbedding

Left multiplication of permutations becomes the natural action on their prefix embeddings.

theorem probePermutationPrefix_mul {m i : Nat} (hi : i ≤ m)
    (τ σ : Equiv.Perm (Fin m)) :
    probePermutationPrefix hi (τ * σ) = τ • probePermutationPrefix hi σ := by
  ext j
  simp [probePermutationPrefix, probePrefixEmbedding,
    Function.Embedding.smul_apply, Equiv.Perm.smul_def, Equiv.Perm.mul_apply]

Every injective ordered prefix extends to a full slot permutation.

theorem probePermutationPrefix_surjective {m i : Nat} (hi : i ≤ m) :
    Function.Surjective (probePermutationPrefix hi) := by
  intro e
  obtain ⟨τ, hτ⟩ := Equiv.Perm.exists_smul_eq_embedding
    (probePrefixEmbedding hi) e
  refine ⟨τ, ?_⟩
  ext j
  have hj := DFunLike.congr_fun hτ j
  exact congrArg Fin.val hj

Fibers of prefix restriction have equal cardinality.


theorem probePermutationPrefix_fiber_card_eq {m i : Nat} (hi : i ≤ m)
    (e₁ e₂ : Fin i ↪ Fin m) :
    ((Finset.univ : Finset (Equiv.Perm (Fin m))).filter
      (fun σ => probePermutationPrefix hi σ = e₁)).card =
    ((Finset.univ : Finset (Equiv.Perm (Fin m))).filter
      (fun σ => probePermutationPrefix hi σ = e₂)).card := by
  classical
  obtain ⟨τ, hτ⟩ := Equiv.Perm.exists_smul_eq_embedding e₁ e₂
  have hτinv : τ⁻¹ • e₂ = e₁ := by
    rw [← hτ]
    simp
  refine Finset.card_bij' (fun σ _ => τ * σ) (fun σ _ => τ⁻¹ * σ) ?_ ?_ ?_ ?_
  · intro σ hσ
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hσ ⊢
    rw [probePermutationPrefix_mul, hσ, hτ]
  · intro σ hσ
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hσ ⊢
    rw [probePermutationPrefix_mul, hσ, hτinv]
  · intro σ hσ
    simp
  · intro σ hσ
    simp

A prescribed injective prefix has exactly (m-i)! extensions to a permutation of all table slots.


theorem probePermutationPrefix_fiber_card {m i : Nat} (hi : i ≤ m)
    (e : Fin i ↪ Fin m) :
    ((Finset.univ : Finset (Equiv.Perm (Fin m))).filter
      (fun σ => probePermutationPrefix hi σ = e)).card = (m - i).factorial := by
  classical
  let base : Fin i ↪ Fin m := probePrefixEmbedding hi
  let fiberCard := ((Finset.univ : Finset (Equiv.Perm (Fin m))).filter
    (fun σ => probePermutationPrefix hi σ = base)).card
  have htotal : m.factorial = m.descFactorial i * fiberCard := by
    have hpartition := Finset.card_eq_sum_card_fiberwise
      (s := (Finset.univ : Finset (Equiv.Perm (Fin m))))
      (t := (Finset.univ : Finset (Fin i ↪ Fin m)))
      (f := probePermutationPrefix hi) (by simp)
    rw [Finset.card_univ, Fintype.card_perm, Fintype.card_fin] at hpartition
    calc
      m.factorial = ∑ b : Fin i ↪ Fin m,
          ((Finset.univ : Finset (Equiv.Perm (Fin m))).filter
            (fun σ => probePermutationPrefix hi σ = b)).card := hpartition
      _ = ∑ _b : Fin i ↪ Fin m, fiberCard := by
        apply Finset.sum_congr rfl
        intro b hb
        exact probePermutationPrefix_fiber_card_eq hi b base
      _ = m.descFactorial i * fiberCard := by
        simp [Fintype.card_embedding_eq]
  have hfactorial : (m - i).factorial * m.descFactorial i = m.factorial :=
    Nat.factorial_mul_descFactorial hi
  have hprefixPos : 0 < m.descFactorial i := Nat.descFactorial_pos.mpr hi
  have hbase : fiberCard = (m - i).factorial := by
    apply Nat.eq_of_mul_eq_mul_left hprefixPos
    calc
      m.descFactorial i * fiberCard = m.factorial := htotal.symm
      _ = m.descFactorial i * (m - i).factorial := by
        rw [← hfactorial, Nat.mul_comm]
  calc
    ((Finset.univ : Finset (Equiv.Perm (Fin m))).filter
      (fun σ => probePermutationPrefix hi σ = e)).card = fiberCard :=
        probePermutationPrefix_fiber_card_eq hi e base
    _ = (m - i).factorial := hbase

Restrict the codomain of an embedding to a finite occupied set.

def embeddingIntoOccupied {m i : Nat} (occupied : Finset (Fin m))
    (e : Fin i ↪ Fin m) (he : ∀ j, e j ∈ occupied) : Fin i ↪ occupied where
  toFun j := ⟨e j, he j⟩
  inj' _a _b hab := e.injective (Subtype.ext_iff.mp hab)

@[simp] theorem embeddingIntoOccupied_val {m i : Nat} (occupied : Finset (Fin m))
    (e : Fin i ↪ Fin m) (he : ∀ j, e j ∈ occupied) (j : Fin i) :
    ((embeddingIntoOccupied occupied e he j : occupied) : Fin m) = e j := rfl

Number of injective ordered prefixes whose values all lie in a fixed occupied set.


theorem occupiedPrefixEmbedding_card {m i : Nat} (occupied : Finset (Fin m)) :
    ((Finset.univ : Finset (Fin i ↪ Fin m)).filter
      (fun e => ∀ j, e j ∈ occupied)).card = occupied.card.descFactorial i := by
  classical
  calc
    ((Finset.univ : Finset (Fin i ↪ Fin m)).filter
      (fun e => ∀ j, e j ∈ occupied)).card =
        (Finset.univ : Finset (Fin i ↪ occupied)).card := by
      refine Finset.card_bij
        (fun e he => by
          have he' : ∀ j, e j ∈ occupied := by
            simpa only [Finset.mem_filter, Finset.mem_univ, true_and] using he
          exact embeddingIntoOccupied occupied e he') ?_ ?_ ?_
      · intro e he
        simp
      · intro e₁ h₁ e₂ h₂ heq
        ext j
        have hj := congrArg Subtype.val (DFunLike.congr_fun heq j)
        have hfin : e₁ j = e₂ j := by
          simpa [embeddingIntoOccupied] using hj
        exact congrArg Fin.val hfin
      · intro e he
        let lifted : Fin i ↪ Fin m :=
          { toFun := fun j => e j
            inj' := fun a b hab => e.injective (Subtype.ext hab) }
        refine ⟨lifted, ?_, ?_⟩
        · simp only [Finset.mem_filter, Finset.mem_univ, true_and]
          intro j
          exact (e j).property
        · ext j
          rfl
    _ = occupied.card.descFactorial i := by
      simp [Fintype.card_embedding_eq]

The occupied-prefix event can be read from the restricted embedding.

theorem firstProbesOccupied_iff_prefix {m i : Nat} (occupied : Finset (Fin m))
    (hi : i ≤ m) (σ : Equiv.Perm (Fin m)) :
    firstProbesOccupied occupied i σ ↔
      ∀ j : Fin i, probePermutationPrefix hi σ j ∈ occupied := by
  constructor
  · intro h j
    exact h (probePrefixEmbedding hi j) j.isLt
  · intro h j hj
    let k : Fin i := ⟨j.val, hj⟩
    simpa [probePermutationPrefix, probePrefixEmbedding, k] using h k

Full probe permutations whose first i positions are occupied.

noncomputable def occupiedPrefixPermutations {m : Nat}
    (occupied : Finset (Fin m)) (i : Nat) : Finset (Equiv.Perm (Fin m)) := by
  classical
  exact Finset.univ.filter (firstProbesOccupied occupied i)

Exact number of full probe permutations whose first i positions are occupied.


theorem firstProbesOccupied_card {m i : Nat} (occupied : Finset (Fin m))
    (hi : i ≤ m) :
    (occupiedPrefixPermutations occupied i).card =
      occupied.card.descFactorial i * (m - i).factorial := by
  classical
  let good := (Finset.univ : Finset (Fin i ↪ Fin m)).filter
    (fun e => ∀ j, e j ∈ occupied)
  have hfiber := Finset.sum_card_fiberwise_eq_card_filter
    (Finset.univ : Finset (Equiv.Perm (Fin m))) good
    (probePermutationPrefix hi)
  have hfilter :
      ((Finset.univ : Finset (Equiv.Perm (Fin m))).filter
        (fun σ => probePermutationPrefix hi σ ∈ good)) =
      occupiedPrefixPermutations occupied i := by
    ext σ
    simp only [Finset.mem_filter, Finset.mem_univ, true_and, good,
      occupiedPrefixPermutations]
    exact (firstProbesOccupied_iff_prefix occupied hi σ).symm
  rw [hfilter] at hfiber
  calc
    (occupiedPrefixPermutations occupied i).card =
        ∑ e ∈ good,
          ((Finset.univ : Finset (Equiv.Perm (Fin m))).filter
            (fun σ => probePermutationPrefix hi σ = e)).card := hfiber.symm
    _ = ∑ _e ∈ good, (m - i).factorial := by
      apply Finset.sum_congr rfl
      intro e he
      exact probePermutationPrefix_fiber_card hi e
    _ = good.card * (m - i).factorial := by simp
    _ = occupied.card.descFactorial i * (m - i).factorial := by
      rw [show good.card = occupied.card.descFactorial i by
        exact occupiedPrefixEmbedding_card occupied]

end Chapter11end CLRS

CLRSLean.FourthEdition.Chapter_11.Section_11_4_Open_Addressing.UniformProbe.Definitions

CLRS Section 11.4 - Uniform probe-space definitions

The sample space is the finite type of permutations of the table slots. A permutation sends probe positions to distinct table slots, exactly matching the uniform-hashing assumption used in CLRS Theorems 11.6--11.8.

              namespace CLRSnamespace Chapter11open Probability

The first i positions of a probe permutation all hit occupied slots.

def firstProbesOccupied {m : Nat} (occupied : Finset (Fin m)) (i : Nat)
    (σ : Equiv.Perm (Fin m)) : Prop :=
  ∀ j : Fin m, j.val < i → σ j ∈ occupied

Indicator of the occupied-prefix event with its classical decision procedure fixed inside the definition.

noncomputable def firstProbesOccupiedIndicator {m : Nat}
    (occupied : Finset (Fin m)) (i : Nat) (σ : Equiv.Perm (Fin m)) : Real := by
  classical
  exact indicator (firstProbesOccupied occupied i σ)

Uniform probability of an occupied prefix in the explicit permutation sample space.

noncomputable def uniformProbeTailProbability {m : Nat}
    (occupied : Finset (Fin m)) (i : Nat) : Real := by
  classical
  exact fintypeExpect (firstProbesOccupiedIndicator occupied i)

Number of probes made before an unsuccessful search reaches its first empty slot, including that final empty-slot probe. The definition is the finite tail sum of the concrete permutation execution.

noncomputable def uniformUnsuccessfulProbeCount {m : Nat} (occupied : Finset (Fin m))
    (σ : Equiv.Perm (Fin m)) : Nat := by
  classical
  exact ∑ i ∈ Finset.range (m + 1),
    if firstProbesOccupied occupied i σ then 1 else 0

The explicit unsuccessful-search probe count is bounded by the number of its m + 1 possible tails.

theorem uniformUnsuccessfulProbeCount_le {m : Nat} (occupied : Finset (Fin m))
    (σ : Equiv.Perm (Fin m)) :
    uniformUnsuccessfulProbeCount occupied σ ≤ m + 1 := by
  classical
  unfold uniformUnsuccessfulProbeCount
  calc
    (∑ i ∈ Finset.range (m + 1), if firstProbesOccupied occupied i σ then 1 else 0)
        ≤ ∑ _i ∈ Finset.range (m + 1), 1 := by
          apply Finset.sum_le_sum
          intro i hi
          split <;> omega
    _ = m + 1 := by simp

Real-cast form of the concrete tail-count definition.

theorem uniformUnsuccessfulProbeCount_cast {m : Nat} (occupied : Finset (Fin m))
    (σ : Equiv.Perm (Fin m)) :
    (uniformUnsuccessfulProbeCount occupied σ : Real) =
      ∑ i ∈ Finset.range (m + 1),
        firstProbesOccupiedIndicator occupied i σ := by
  classical
  simp [uniformUnsuccessfulProbeCount, firstProbesOccupiedIndicator, indicator]

Canonical set consisting of the first n slots, used only to package the successful-search average over insertion times.

def canonicalOccupied (m n : Nat) : Finset (Fin m) :=
  Finset.univ.filter (fun x => x.val < n)

The canonical occupied prefix has the requested cardinality when it fits inside the table.


theorem canonicalOccupied_card (m n : Nat) (hn : n ≤ m) :
    (canonicalOccupied m n).card = n := by
  classical
  rw [canonicalOccupied]
  have heq : Finset.univ.filter (fun x : Fin m => x.val < n) =
      Finset.univ.map (Fin.castLEEmb hn) := by
    ext x
    simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_map]
    constructor
    · intro hx
      exact ⟨⟨x.val, hx⟩, by simp⟩
    · rintro ⟨y, _, rfl⟩
      exact y.isLt
  rw [heq, Finset.card_map, Finset.card_univ, Fintype.card_fin]

Explicit successful-search expectation: average the concrete unsuccessful probe count at the n insertion-time loads.

noncomputable def uniformSuccessfulExpectedProbes (m n : Nat) : Real :=
  (1 / (n : Real)) * ∑ j ∈ Finset.range n,
    fintypeExpect (fun σ : Equiv.Perm (Fin m) =>
      (uniformUnsuccessfulProbeCount (canonicalOccupied m j) σ : Real))

end Chapter11end CLRS

CLRSLean.FourthEdition.Chapter_11.Section_11_4_Open_Addressing.UniformProbe.Probability

CLRS Section 11.4 - Uniform permutation probabilities

The counting result is converted to the without-replacement product already used by the chapter. Finite-expectation linearity then identifies the concrete probe-count expectation with the existing tail sum and transports CLRS Theorems 11.6--11.8 to the explicit sample space.

              namespace CLRSnamespace Chapter11open Probability

The without-replacement product is the quotient of descending factorials.


theorem probeTail_eq_descFactorial_div (m n i : Nat) (hi : i ≤ m) :
    probeTail m n i = (n.descFactorial i : Real) / (m.descFactorial i : Real) := by
  by_cases hin : i ≤ n
  · rw [probeTail, Nat.descFactorial_eq_prod_range, Nat.descFactorial_eq_prod_range,
      Finset.prod_div_distrib]
    congr 1
    · rw [Nat.cast_prod]
      apply Finset.prod_congr rfl
      intro j hj
      rw [Nat.cast_sub]
      exact Nat.le_of_lt (lt_of_lt_of_le (Finset.mem_range.mp hj) hin)
    · rw [Nat.cast_prod]
      apply Finset.prod_congr rfl
      intro j hj
      rw [Nat.cast_sub]
      exact Nat.le_of_lt (lt_of_lt_of_le (Finset.mem_range.mp hj) hi)
  · have hni : n < i := Nat.lt_of_not_ge hin
    have hnmem : n ∈ Finset.range i := Finset.mem_range.mpr hni
    have hnum : n.descFactorial i = 0 := Nat.descFactorial_eq_zero_iff_lt.mpr hni
    rw [probeTail, Finset.prod_eq_zero hnmem (by simp), hnum, Nat.cast_zero, zero_div]

The explicit event probability is its satisfying-permutation count divided by m!.


theorem uniformProbeTailProbability_eq_card {m i : Nat}
    (occupied : Finset (Fin m)) :
    uniformProbeTailProbability occupied i =
      ((occupiedPrefixPermutations occupied i).card : Real) / (m.factorial : Real) := by
  classical
  unfold uniformProbeTailProbability Probability.fintypeExpect
  rw [show (∑ σ : Equiv.Perm (Fin m), firstProbesOccupiedIndicator occupied i σ) =
      ((occupiedPrefixPermutations occupied i).card : Real) by
    simp [firstProbesOccupiedIndicator, indicator, occupiedPrefixPermutations]]
  simp [Fintype.card_perm]

The probability of an occupied prefix under a uniform slot permutation is exactly the chapter's without-replacement product probeTail.


theorem uniformProbeTailProbability_eq_probeTail {m i : Nat}
    (occupied : Finset (Fin m)) (hi : i ≤ m) :
    uniformProbeTailProbability occupied i = probeTail m occupied.card i := by
  rw [uniformProbeTailProbability_eq_card, firstProbesOccupied_card occupied hi]
  have hfactorial : ((m.factorial : Nat) : Real) =
      ((m - i).factorial : Real) * (m.descFactorial i : Real) := by
    exact_mod_cast (Nat.factorial_mul_descFactorial hi).symm
  have hrest : ((m - i).factorial : Real) ≠ 0 := by positivity
  have hprefix : ((m.descFactorial i : Nat) : Real) ≠ 0 := by
    exact_mod_cast (Nat.ne_of_gt (Nat.descFactorial_pos.mpr hi))
  rw [hfactorial, probeTail_eq_descFactorial_div m occupied.card i hi]
  push_cast
  field_simp

The expected concrete unsuccessful-search probe count is the existing tail-sum model.

theorem uniformUnsuccessfulExpectedProbes_eq {m : Nat}
    (occupied : Finset (Fin m)) :
    fintypeExpect (fun σ : Equiv.Perm (Fin m) =>
      (uniformUnsuccessfulProbeCount occupied σ : Real)) =
      expectedUnsuccessfulProbes m occupied.card := by
  calc
    fintypeExpect (fun σ : Equiv.Perm (Fin m) =>
        (uniformUnsuccessfulProbeCount occupied σ : Real)) =
        fintypeExpect (fun σ : Equiv.Perm (Fin m) =>
          ∑ i ∈ Finset.range (m + 1), firstProbesOccupiedIndicator occupied i σ) := by
            apply congrArg fintypeExpect
            funext σ
            exact uniformUnsuccessfulProbeCount_cast occupied σ
    _ = ∑ i ∈ Finset.range (m + 1),
        fintypeExpect (firstProbesOccupiedIndicator occupied i) := by
          exact fintypeExpect_sum (Finset.range (m + 1))
            (fun i σ => firstProbesOccupiedIndicator occupied i σ)
    _ = ∑ i ∈ Finset.range (m + 1), probeTail m occupied.card i := by
      apply Finset.sum_congr rfl
      intro i hi
      exact uniformProbeTailProbability_eq_probeTail occupied
        (Nat.lt_succ_iff.mp (Finset.mem_range.mp hi))
    _ = expectedUnsuccessfulProbes m occupied.card := rfl

Explicit-sample-space form of CLRS Theorem 11.6.


theorem uniformUnsuccessfulExpectedProbes_le {m : Nat}
    (occupied : Finset (Fin m)) (hnotFull : occupied.card < m) :
    fintypeExpect (fun σ : Equiv.Perm (Fin m) =>
      (uniformUnsuccessfulProbeCount occupied σ : Real)) ≤
      1 / (1 - openLoadFactor m occupied.card) := by
  rw [uniformUnsuccessfulExpectedProbes_eq]
  exact expectedUnsuccessfulProbes_le m occupied.card hnotFull

Explicit-sample-space form of CLRS Corollary 11.7 for insertion.

theorem uniformInsertionExpectedProbes_le {m : Nat}
    (occupied : Finset (Fin m)) (hnotFull : occupied.card < m) :
    fintypeExpect (fun σ : Equiv.Perm (Fin m) =>
      (uniformUnsuccessfulProbeCount occupied σ : Real)) ≤
      1 / (1 - openLoadFactor m occupied.card) :=
  uniformUnsuccessfulExpectedProbes_le occupied hnotFull

The explicit successful-search average agrees with the chapter's insertion- time average.


theorem uniformSuccessfulExpectedProbes_eq (m n : Nat) (hn : n ≤ m) :
    uniformSuccessfulExpectedProbes m n = expectedSuccessfulProbes m n := by
  unfold uniformSuccessfulExpectedProbes expectedSuccessfulProbes
  congr 1
  apply Finset.sum_congr rfl
  intro j hj
  rw [uniformUnsuccessfulExpectedProbes_eq, canonicalOccupied_card]
  exact le_trans (Nat.le_of_lt (Finset.mem_range.mp hj)) hn

Explicit-sample-space logarithmic form of CLRS Theorem 11.8.


theorem uniformSuccessfulExpectedProbes_le_ln (m n : Nat)
    (hn : n < m) (hnpos : 0 < n) :
    uniformSuccessfulExpectedProbes m n ≤
      (1 / openLoadFactor m n) * Real.log (1 / (1 - openLoadFactor m n)) := by
  rw [uniformSuccessfulExpectedProbes_eq m n (le_of_lt hn)]
  exact expectedSuccessfulProbes_le_ln m n hn hnpos

end Chapter11end CLRS

Imports

import Mathlib
import CLRSLean.Probability.FiniteExpectation
import CLRSLean.FourthEdition.Chapter_11.Section_11_2_Chained_Hash_Tables

11.5. Perfect Hashing

This section formalises the two-level perfect-hashing scheme of CLRS §11.5: a static key set is stored using a primary universal hash into m = n buckets, and each bucket with n_j keys gets a secondary table of size m_j = n_j², which — by the birthday-style collision count — is collision-free with probability ≥ 1/2. The total expected secondary storage is O(n).

Main results:

Definition PerfectHashTable: two-level perfect hash data structure.
Theorem perfectSearch_iff_mem: membership correctness (perfectSearch T x ↔ x ∈ T.keys), establishing O(1) worst-case search.
Theorem perfectHash_collision_free_prob_ge_half (Theorem 11.9): when hashing n keys into m = n² slots under a universal family, the hash is collision-free with probability at least 1/2.
Theorem exists_collision_free_secondary: for n ≥ 2 keys into n² slots, an injective secondary hash exists.
Theorem perfectHash_expected_total_space_lt_2n (Theorem 11.10): when n keys are hashed uniformly and independently into m = n primary buckets, the expected total secondary storage E[Σ_j n_j²] is less than 2n (hence O(n)).
Theorem perfectHash_expected_trials_le_two: in a truncated model of t independent trials, the expected number of trials until a collision-free secondary hash is at most 2 (geometric bound with success probability ≥ 1/2).
Theorem perfectHash_expected_construction_time_le_const_n: the expected abstract budget constructionCost is less than 5n. This formula is not itself a counter attached to a table constructor.

The Construction companion supplies an executed finite-trial constructor with a guaranteed collision-free terminal fallback, array initialization and placement, and a separate expected-work refinement to this abstract budget. Secondary injectivity is required only for stored keys in the relevant bucket. The sampling model uses all local-index hash assignments under SUHA, not a constructed family of constant-time hash programs on arbitrary original keys. RAM, hash-code generation, and arithmetic implementation costs are excluded.

Notation conventions used in this section:

n : number of keys
m : number of primary buckets (and m = n for Theorem 11.10)
a : Fin n → Fin m : a hash assignment (SUHA independent-uniform model)
A : Fin t → (Fin n → Fin (n^2)) : a sequence of t independent trial hashes of n keys into n² slots (construction-trial model)
H : ι → (K → Fin m) : a universal family of hash functions
n_j : number of keys assigned to primary bucket j

              namespace CLRSnamespace Chapter11open CLRS.Probabilityopen Finsetopen scoped Classical

Two-level perfect hash model

A PerfectHashTable for a finite set of keys uses a primary hash into m buckets and, for each bucket j, a secondary hash that is collision-free on the keys assigned to that bucket. The deterministic two-level lookup completes in O(1) worst-case time (two table lookups, independent of n).

The fields sec and table are per-bucket; the invariant sec_inj ensures no two stored keys in the same primary bucket share a secondary slot. Nonmembers may collide with stored keys; lookup checks the stored value, so table j (sec j x) = some x identifies x uniquely.

The set of keys stored in the table.

Primary hash function mapping each key to a primary bucket.

For each primary bucket j, a secondary hash function mapping keys to slot indices. The codomain is ℕ; the actual table size per bucket is not needed for correctness, only for the probabilistic space bound.

The secondary table: for each bucket j and slot s, optionally a key.

The secondary hash is collision-free on the keys in each primary bucket: if x and y are both in keys, map to the same primary bucket, and get the same secondary slot, then x = y.

Every key is stored in the table at the slot determined by its primary and secondary hash.

If the table stores a key at a slot, that key maps to that slot.

              structure PerfectHashTable (K : Type) [DecidableEq K] (m : ℕ) : Type where  keys : Finset K  prim : K → Fin m  sec : Fin m → K → ℕ  table : Fin m → ℕ → Option K  sec_inj : ∀ (j : Fin m) (x y : K),
    x ∈ keys → y ∈ keys → prim x = j → prim y = j → sec j x = sec j y → x = y  table_stores_keys : ∀ x ∈ keys, table (prim x) (sec (prim x) x) = some x  table_only_keys : ∀ (j : Fin m) (s : ℕ) (x : K),
    table j s = some x → x ∈ keys ∧ prim x = j ∧ sec j x = s

Two-level perfect-hash search: compute the primary bucket j = prim x, the secondary slot s = sec j x, and check whether table j s holds x.

def perfectSearch [DecidableEq K] (T : PerfectHashTable K m) (x : K) : Prop :=
  T.table (T.prim x) (T.sec (T.prim x) x) = some x

Membership correctness of two-level perfect-hash search. A key x is found by perfectSearch exactly when x ∈ T.keys (CLRS §11.5). This establishes O(1) worst-case search time (two table lookups).

theorem perfectSearch_iff_mem [DecidableEq K] (T : PerfectHashTable K m) (x : K) :
    perfectSearch T x ↔ x ∈ T.keys := by
  constructor
  · intro h
    have hmem := T.table_only_keys (T.prim x) (T.sec (T.prim x) x) x h
    exact hmem.1
  · intro h
    exact T.table_stores_keys x h

Theorem 11.9: secondary collision-free with probability at least 1/2

The fintypeExpect operator is monotone: if X ω ≤ Y ω for all ω, then E[X] ≤ E[Y].

theorem fintypeExpect_mono {Ω : Type} [Fintype Ω] [DecidableEq Ω] {X Y : Ω → ℝ}
    (hXY : ∀ ω, X ω ≤ Y ω) : fintypeExpect X ≤ fintypeExpect Y := by
  unfold fintypeExpect
  refine div_le_div_of_nonneg_right (Finset.sum_le_sum (fun ω _ => hXY ω)) ?_
  positivity

fintypeExpect of a negated random variable is the negation of the expectation.

theorem fintypeExpect_neg {Ω : Type} [Fintype Ω] [DecidableEq Ω] (X : Ω → ℝ) :
    fintypeExpect (fun ω => -X ω) = -fintypeExpect X := by
  simp [fintypeExpect, Finset.sum_neg_distrib, neg_div]

Number of colliding unordered pairs {i, j} with i < j under a hash assignment a : Fin n → Fin m. Each pair of distinct indices that hash to the same bucket contributes 1.

noncomputable def collisionCount {m n : ℕ} (a : Fin n → Fin m) : ℝ :=
  ∑ i : Fin n, ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0)

collisionCount is nonnegative.


theorem collisionCount_nonneg {m n : ℕ} (a : Fin n → Fin m) : 0 ≤ collisionCount a := by
  unfold collisionCount
  apply Finset.sum_nonneg; intro i hi
  apply Finset.sum_nonneg; intro j hj
  by_cases h : i < j
  · have : 0 ≤ indicator (a i = a j) := by
      unfold indicator; split <;> norm_num
    simp [h, this]
  · simp [h, This simp argument is unused:
  indicator

Hint: Omit it from the simp argument list.
  simp [h,̵ ̵i̵n̵d̵i̵c̵a̵t̵o̵r̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`indicator]

Expected collisions under pairwise independent hashing (SUHA). For hash assignments a : Fin n → Fin m, the expected number of colliding unordered pairs is exactly n(n-1)/(2m).


theorem expectedCollisions_suha {m n : ℕ} (hm : 0 < m) :
    fintypeExpect (fun a : Fin n → Fin m => collisionCount a)
      = (n : ℝ) * ((n : ℝ) - 1) / (2 * (m : ℝ)) := by
  haveI : Nonempty (Fin m) := ⟨⟨0, hm⟩⟩
  unfold collisionCount
  have hE : fintypeExpect (fun a : Fin n → Fin m =>
      ∑ i : Fin n, ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0))
      = ∑ i : Fin n, ∑ j : Fin n, (if i < j then (1 / (m : ℝ)) else 0) := by
    rw [fintypeExpect_sum Finset.univ (fun (i : Fin n) (a : Fin n → Fin m) =>
      ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0))]
    refine Finset.sum_congr rfl (fun i _ => ?_)
    rw [fintypeExpect_sum Finset.univ (fun (j : Fin n) (a : Fin n → Fin m) =>
      if i < j then indicator (a i = a j) else 0)]
    refine Finset.sum_congr rfl (fun j _ => ?_)
    by_cases hlt : i < j
    · simp [hlt, pairCollisionProb i j (ne_of_lt hlt) hm]
    · have hcard : Fintype.card (Fin n → Fin m) ≠ 0 := Fintype.card_ne_zero
      simp [hlt, fintypeExpect_const hcard 0]
  have hpair : (∑ i : Fin n, ∑ j : Fin n, (if i < j then (1 / (m : ℝ)) else 0))
      = (1 / (m : ℝ)) * ((n : ℝ) * ((n : ℝ) - 1) / 2) := by
    rw [← sum_upper_triangle n, Finset.mul_sum]
    refine Finset.sum_congr rfl (fun i _ => ?_)
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl (fun j _ => ?_)
    by_cases h : i < j <;> simp [h]
  rw [hE, hpair]
  ring

When n keys are hashed into m = n² slots under SUHA, the expected number of collisions is less than 1/2 (for n ≥ 2).


theorem expectedCollisions_sq_lt_half {n : ℕ} (hn : 2 ≤ n) :
    fintypeExpect (fun a : Fin n → Fin (n^2) => collisionCount a) < 1/2 := by
  have hm : 0 < n^2 := by
    have hnpos : 0 < n := by omega
    positivity
  rw [expectedCollisions_suha hm]
  have hcalc : (n : ℝ) * ((n : ℝ) - 1) / (2 * ((n : ℝ)^2)) < 1/2 := by
    have hnpos' : (n : ℝ) > 0 := by exact_mod_cast (show 0 < n from by omega)
    have hpos : (0 : ℝ) < 2 * ((n : ℝ)^2) := by positivity
    field_simp [hpos.ne']
    nlinarith
  have hden : ((n ^ 2 : ℕ) : ℝ) = (n : ℝ)^2 := by simp
  simpa [hden] using hcalc

Markov's inequality for nonnegative-integer-valued random variables. If X : Ω → ℕ, then P[X ≥ 1] ≤ E[X].


theorem markov_integer {Ω : Type} [Fintype Ω] [DecidableEq Ω] (X : Ω → ℕ) :
    fintypeExpect (fun ω => if X ω ≥ 1 then (1 : ℝ) else 0) ≤
      fintypeExpect (fun ω => (X ω : ℝ)) := by
  have hpoint : ∀ ω, (if X ω ≥ 1 then (1 : ℝ) else 0) ≤ (X ω : ℝ) := by
    intro ω
    by_cases h : X ω ≥ 1
    · have h' : (1 : ℝ) ≤ (X ω : ℝ) := by exact_mod_cast h
      simp [h, h']
    · simp [h]
  exact fintypeExpect_mono hpoint

Theorem 11.9 (Perfect hashing: secondary collision-free with probability ≥ 1/2). Let n keys be hashed into m = n² slots under a universal family (or under SUHA). Then the hash assignment is collision-free with probability at least 1/2.

Equivalently, a secondary table of size n_j² for a bucket with n_j keys is collision-free with probability at least 1/2 (CLRS Theorem 11.9).

Try this: intro hzero i j heqTry this: intro hzero i j heqTry this: intro hzero i j heq
theorem perfectHash_collision_free_prob_ge_half {n : ℕ} (hn : 2 ≤ n) :
    fintypeExpect (fun a : Fin n → Fin (n^2) =>
      indicator (∀ i j : Fin n, a i = a j → i = j))
    ≥ 1/2 := by
  have hm : 0 < n^2 := by
    have hnpos' : 0 < n := by omega
    positivity
  have hnpos : 0 < n := by omega
  haveI : Nonempty (Fin n) := ⟨⟨0, hnpos⟩⟩
  haveI : Nonempty (Fin n → Fin (n^2)) :=
    ⟨fun _ => ⟨0, show 0 < n^2 from hm⟩⟩
  have hcard : Fintype.card (Fin n → Fin (n^2)) ≠ 0 := Fintype.card_ne_zero

  -- `X a` is the number of colliding unordered pairs under `a`, as a ℕ.
  let X (a : Fin n → Fin (n^2)) : ℕ :=
    (Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
      (Finset.univ : Finset (Fin n × Fin n))).card

  -- `X a = 0` exactly when `a` is injective (collision-free)
  have h_inj_iff : ∀ a : Fin n → Fin (n^2),
      (∀ i j : Fin n, a i = a j → i = j) ↔ X a = 0 := by
    intro a
    dsimp [X]
    constructor
    · intro hinj
      apply Finset.card_eq_zero.mpr
      apply Finset.not_nonempty_iff_eq_empty.mp
      intro hne
      rcases hne with ⟨p, hp⟩
      rcases Finset.mem_filter.mp hp with ⟨hp_univ, ⟨hlt, heq⟩⟩
      exact hlt.ne' (hinj p.1 p.2 heq).symm
    · Try this: intro hzero i j heqintro hzero
      intro i j heq
      by_contra! hne
      rcases lt_trichotomy i j with (hlt | heq' | hlt)
      · have hmem : (i, j) ∈ Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
            (Finset.univ : Finset (Fin n × Fin n)) := by
          simp [hlt, heq]
        have hcard_ne_zero : (Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
              (Finset.univ : Finset (Fin n × Fin n))).card ≠ 0 :=
          Finset.card_ne_zero.mpr ⟨(i, j), hmem⟩
        rw [hzero] at hcard_ne_zero
        exact hcard_ne_zero rfl
      · exact hne heq'
      · have hmem : (j, i) ∈ Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
            (Finset.univ : Finset (Fin n × Fin n)) := by
          simp [hlt, heq.symm]
        have hcard_ne_zero : (Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
              (Finset.univ : Finset (Fin n × Fin n))).card ≠ 0 :=
          Finset.card_ne_zero.mpr ⟨(j, i), hmem⟩
        rw [hzero] at hcard_ne_zero
        exact hcard_ne_zero rfl

  -- Rewrite the collision-free indicator in terms of `X`
  have h_indicator_eq : (fun a : Fin n → Fin (n^2) => indicator (∀ i j : Fin n, a i = a j → i = j))
      = (fun a : Fin n → Fin (n^2) => if X a = 0 then (1 : ℝ) else 0) := by
    funext a; simp [indicator, h_inj_iff a]

  rw [h_indicator_eq]

  -- Relate `collisionCount` (real-valued) to `X` (ℕ-valued)
  have h_collision_eq : (fun (a : Fin n → Fin (n^2)) => collisionCount a) =
      (fun (a : Fin n → Fin (n^2)) => (X a : ℝ)) := by
    funext a
    dsimp [collisionCount, X]
    have h1 : (∑ i : Fin n, ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0)) =
        (∑ p : Fin n × Fin n, (if p.1 < p.2 then indicator (a p.1 = a p.2) else 0)) := by
      simp [Fintype.sum_prod_type]
    have h2 : (∑ p : Fin n × Fin n, (if p.1 < p.2 then indicator (a p.1 = a p.2) else 0)) =
        (∑ p : Fin n × Fin n, (if p.1 < p.2 ∧ a p.1 = a p.2 then (1 : ℝ) else 0)) := by
      refine Finset.sum_congr rfl (fun p _ => ?_)
      by_cases hlt : p.1 < p.2
      · simp [hlt, indicator]
      · simp [hlt, This simp argument is unused:
  indicator

Hint: Omit it from the simp argument list.
  simp [hlt,̵ ̵i̵n̵d̵i̵c̵a̵t̵o̵r̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`indicator]
    have h3 : (∑ p : Fin n × Fin n, (if p.1 < p.2 ∧ a p.1 = a p.2 then (1 : ℝ) else 0)) =
        (Finset.card (Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
          (Finset.univ : Finset (Fin n × Fin n))) : ℝ) := by
      simp [This simp argument is unused:
  Finset.sum_filter

Hint: Omit it from the simp argument list.
  simp ̵[̵F̵i̵n̵s̵e̵t̵.̵s̵u̵m̵_̵f̵i̵l̵t̵e̵r̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Finset.sum_filter]
    calc
      collisionCount a = (∑ i : Fin n, ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0)) := rfl
      _ = (∑ p : Fin n × Fin n, (if p.1 < p.2 then indicator (a p.1 = a p.2) else 0)) := h1
      _ = (∑ p : Fin n × Fin n, (if p.1 < p.2 ∧ a p.1 = a p.2 then (1 : ℝ) else 0)) := h2
      _ = (Finset.card (Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
          (Finset.univ : Finset (Fin n × Fin n))) : ℝ) := h3
      _ = (X a : ℝ) := rfl

  have h_expected_X_lt_half :
      fintypeExpect (fun a : Fin n → Fin (n^2) => (X a : ℝ)) < 1/2 := by
    rw [← h_collision_eq]
    exact expectedCollisions_sq_lt_half hn

  -- Markov inequality: P[X ≥ 1] ≤ E[X]
  have h_markov : fintypeExpect (fun a : Fin n → Fin (n^2) => if X a ≥ 1 then (1 : ℝ) else 0) ≤
      fintypeExpect (fun a : Fin n → Fin (n^2) => (X a : ℝ)) :=
    markov_integer X

  -- `indicator(X = 0) = 1 - indicator(X ≥ 1)`
  have h_decomp : (fun a : Fin n → Fin (n^2) => (if X a = 0 then (1 : ℝ) else 0)) =
      (fun a : Fin n → Fin (n^2) => (1 : ℝ) - (if X a ≥ 1 then (1 : ℝ) else 0)) := by
    funext a
    by_cases h : X a = 0
    · simp [h]
    · have hpos : X a ≥ 1 := Nat.one_le_of_lt (Nat.pos_of_ne_zero h)
      simp [h, hpos]

  rw [h_decomp]
  have h_expect_sub : fintypeExpect (fun a : Fin n → Fin (n^2) =>
      (1 : ℝ) - (if X a ≥ 1 then (1 : ℝ) else 0)) =
    (1 : ℝ) - fintypeExpect (fun a : Fin n → Fin (n^2) => (if X a ≥ 1 then (1 : ℝ) else 0)) := by
    calc
      fintypeExpect (fun a : Fin n → Fin (n^2) =>
          (1 : ℝ) - (if X a ≥ 1 then (1 : ℝ) else 0))
          = fintypeExpect (fun a : Fin n → Fin (n^2) =>
              (1 : ℝ) + (-(if X a ≥ 1 then (1 : ℝ) else 0))) := by
            refine congrArg fintypeExpect (funext fun a => ?_)
            rfl
      _ = fintypeExpect (fun _ : Fin n → Fin (n^2) => (1 : ℝ)) +
            fintypeExpect (fun a : Fin n → Fin (n^2) =>
              -(if X a ≥ 1 then (1 : ℝ) else 0)) :=
            fintypeExpect_add _ _
      _ = (1 : ℝ) + (-fintypeExpect (fun a : Fin n → Fin (n^2) =>
            (if X a ≥ 1 then (1 : ℝ) else 0))) := by
        simp [fintypeExpect_const hcard, fintypeExpect_neg]
      _ = (1 : ℝ) - fintypeExpect (fun a : Fin n → Fin (n^2) =>
            (if X a ≥ 1 then (1 : ℝ) else 0)) := by ring

  rw [h_expect_sub]
  have h_bound : fintypeExpect (fun a : Fin n → Fin (n^2) => if X a ≥ 1 then (1 : ℝ) else 0) < 1/2 := by
    linarith
  linarith

Theorem 11.10: expected total space O(n)

The number of keys (out of n) that hash to a given bucket j under assignment a.

noncomputable def bucketSize {m n : ℕ} (a : Fin n → Fin m) (j : Fin m) : ℝ :=
  ∑ i : Fin n, indicator (a i = j)

The total secondary storage for a hash assignment a: sum over buckets of the square of the bucket size, i.e. Σ_j n_j². This is the space used if each bucket j gets a secondary table of size n_j².

noncomputable def totalSecondarySpace {m n : ℕ} (a : Fin n → Fin m) : ℝ :=
  ∑ j : Fin m, (bucketSize a j) ^ 2

The algebraic identity Σ_j n_j² = Σ_i Σ_k indicator(a i = a k). This expands the sum of squares into a double sum over key pairs (CLRS proof of Theorem 11.10).


theorem totalSecondarySpace_eq_sum_indicator {m n : ℕ} (a : Fin n → Fin m) :
    totalSecondarySpace a = ∑ i : Fin n, ∑ k : Fin n, indicator (a i = a k) := by
  unfold totalSecondarySpace bucketSize
  calc
    ∑ j : Fin m, ((∑ i : Fin n, indicator (a i = j)) : ℝ) ^ 2
        = ∑ j : Fin m, (∑ i : Fin n, indicator (a i = j)) * (∑ k : Fin n, indicator (a k = j)) := by
          simp [sq]
    _ = ∑ j : Fin m, ∑ i : Fin n, ∑ k : Fin n, indicator (a i = j) * indicator (a k = j) := by
      refine Finset.sum_congr rfl (fun j hj => ?_)
      calc
        (∑ i : Fin n, indicator (a i = j)) * (∑ k : Fin n, indicator (a k = j))
            = ∑ k : Fin n, (∑ i : Fin n, indicator (a i = j)) * indicator (a k = j) := by
              rw [Finset.mul_sum]
        _ = ∑ k : Fin n, ∑ i : Fin n, indicator (a i = j) * indicator (a k = j) := by
          refine Finset.sum_congr rfl (fun k hk => ?_)
          rw [Finset.sum_mul]
        _ = ∑ i : Fin n, ∑ k : Fin n, indicator (a i = j) * indicator (a k = j) := by
          rw [Finset.sum_comm]
    _ = ∑ i : Fin n, ∑ k : Fin n, ∑ j : Fin m, indicator (a i = j) * indicator (a k = j) := by
      calc
        ∑ j : Fin m, ∑ i : Fin n, ∑ k : Fin n, indicator (a i = j) * indicator (a k = j)
            = ∑ i : Fin n, ∑ j : Fin m, ∑ k : Fin n, indicator (a i = j) * indicator (a k = j) := by
              rw [Finset.sum_comm]
        _ = ∑ i : Fin n, ∑ k : Fin n, ∑ j : Fin m, indicator (a i = j) * indicator (a k = j) := by
          refine Finset.sum_congr rfl (fun i hi => ?_)
          rw [Finset.sum_comm]
    _ = ∑ i : Fin n, ∑ k : Fin n, indicator (a i = a k) := by
      refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun k _ => ?_))
      simp [indicator, Finset.sum_ite_eq, Finset.mem_univ]

Theorem 11.10 (Expected total space is O(n)). When n keys are hashed uniformly and independently into m = n primary buckets, the expected total secondary storage E[Σ_j n_j²] is strictly less than 2n (CLRS Theorem 11.10).


theorem perfectHash_expected_total_space_lt_2n {n : ℕ} (hn : 0 < n) :
    fintypeExpect (fun a : Fin n → Fin n => totalSecondarySpace a) < 2 * (n : ℝ) := by
  have hm : 0 < n := hn
  haveI : Nonempty (Fin n) := ⟨⟨0, hn⟩⟩
  have hcard : Fintype.card (Fin n → Fin n) ≠ 0 := Fintype.card_ne_zero

  -- Algebraic identity: Σ_j n_j² = n + Σ_{i≠k} indicator(a i = a k)
  have h_identity : ∀ a : Fin n → Fin n,
      totalSecondarySpace a = (n : ℝ) + ∑ i : Fin n, ∑ k : Fin n,
        (if i ≠ k then indicator (a i = a k) else 0) := by
    intro a
    calc
      totalSecondarySpace a = ∑ i : Fin n, ∑ k : Fin n, indicator (a i = a k) :=
        totalSecondarySpace_eq_sum_indicator a
      _ = (∑ i : Fin n, indicator (a i = a i)) +
          (∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) := by
        calc
          ∑ i : Fin n, ∑ k : Fin n, indicator (a i = a k)
              = ∑ i : Fin n, (indicator (a i = a i) + ∑ k : Fin n,
                  (if i ≠ k then indicator (a i = a k) else 0)) := by
            refine Finset.sum_congr rfl (fun i hi => ?_)
            have h_inner : ∑ k : Fin n, indicator (a i = a k)
                = indicator (a i = a i) + ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0) := by
              calc
                ∑ k : Fin n, indicator (a i = a k)
                    = ∑ k : Fin n, ((if i = k then indicator (a i = a i) else 0) +
                        (if i ≠ k then indicator (a i = a k) else 0)) := by
                      refine Finset.sum_congr rfl (fun k hk => ?_)
                      by_cases hik : i = k
                      · subst hik; simp
                      · simp [hik]
                _ = (∑ k : Fin n, (if i = k then indicator (a i = a i) else 0)) +
                    (∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) := by
                  simp [Finset.sum_add_distrib]
                _ = indicator (a i = a i) + ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0) := by
                  simp [Finset.sum_ite_eq, Finset.mem_univ]

            calc
              ∑ k : Fin n, indicator (a i = a k)
                  = indicator (a i = a i) + ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0) := h_inner
              _ = indicator (a i = a i) + ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0) := rfl
          _ = (∑ i : Fin n, indicator (a i = a i)) +
              (∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) := by
            simp [Finset.sum_add_distrib]
      _ = (n : ℝ) + ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0) := by
        simp [indicator, Finset.sum_const, Finset.card_univ, Fintype.card_fin]

  -- Use the identity inside the expectation
  have h_expect_identity :
      fintypeExpect (fun a : Fin n → Fin n => totalSecondarySpace a) =
      (n : ℝ) + fintypeExpect (fun a : Fin n → Fin n =>
        ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) := by
    calc
      fintypeExpect (fun a : Fin n → Fin n => totalSecondarySpace a) =
          fintypeExpect (fun a : Fin n → Fin n => (n : ℝ) + ∑ i : Fin n, ∑ k : Fin n,
            (if i ≠ k then indicator (a i = a k) else 0)) := by
            refine congrArg fintypeExpect (funext h_identity)
      _ = fintypeExpect (fun _ : Fin n → Fin n => (n : ℝ)) +
          fintypeExpect (fun a : Fin n → Fin n =>
            ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) :=
        fintypeExpect_add _ _
      _ = (n : ℝ) + fintypeExpect (fun a : Fin n → Fin n =>
            ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) := by
        simp [fintypeExpect_const hcard, This simp argument is unused:
  Fintype.card_fin

Hint: Omit it from the simp argument list.
  simp [fintypeExpect_const hcard,̵ ̵F̵i̵n̵t̵y̵p̵e̵.̵c̵a̵r̵d̵_̵f̵i̵n̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Fintype.card_fin]

  rw [h_expect_identity]

  -- Compute the remaining expectation: E[Σ_{i≠k} indicator(a i = a k)] = n*(n-1)*(1/n) = n-1
  have h_cross_expect :
      fintypeExpect (fun a : Fin n → Fin n =>
        ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0))
      = (n : ℝ) - 1 := by
    calc
      fintypeExpect (fun a : Fin n → Fin n =>
          ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0))
          = ∑ i : Fin n, fintypeExpect (fun a : Fin n → Fin n =>
              ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) := by
            rw [fintypeExpect_sum Finset.univ]
      _ = ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then
            fintypeExpect (fun a : Fin n → Fin n => indicator (a i = a k)) else 0) := by
        refine Finset.sum_congr rfl (fun i _ => ?_)
        rw [fintypeExpect_sum Finset.univ]
        refine Finset.sum_congr rfl (fun k _ => ?_)
        by_cases hne : i ≠ k
        · simp [hne, pairCollisionProb i k hne hm]
        · simp [hne, fintypeExpect_const hcard, This simp argument is unused:
  Fintype.card_fin

Hint: Omit it from the simp argument list.
  simp [hne, fintypeExpect_const hcard,̵ ̵F̵i̵n̵t̵y̵p̵e̵.̵c̵a̵r̵d̵_̵f̵i̵n̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Fintype.card_fin]
      _ = ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then (1 / (n : ℝ)) else 0) := by
        refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun k _ => ?_))
        by_cases hne : i ≠ k
        · rw [pairCollisionProb i k hne hm]
        · simp [hne]
      _ = (n : ℝ) - 1 := by
        have h_inner_sum : ∀ i : Fin n, (∑ k : Fin n, (if i ≠ k then (1 / (n : ℝ)) else 0)) = ((n : ℝ) - 1) / (n : ℝ) := by
          intro i
          calc
            (∑ k : Fin n, (if i ≠ k then (1 / (n : ℝ)) else 0))
                = (∑ k : Fin n, (if i ≠ k then (1 : ℝ) else 0)) * (1 / (n : ℝ)) := by
                  simp [Finset.mul_sum, mul_comm]
            _ = ((n : ℝ) - 1) * (1 / (n : ℝ)) := by
              have hsum : (∑ k : Fin n, (if i ≠ k then (1 : ℝ) else 0)) = (n : ℝ) - 1 := by
                calc
                  (∑ k : Fin n, (if i ≠ k then (1 : ℝ) else 0))
                      = (∑ k : Fin n, ((1 : ℝ) - (if i = k then (1 : ℝ) else 0))) := by
                        refine Finset.sum_congr rfl (fun k hk => ?_)
                        by_cases hik : i = k
                        · subst hik; simp
                        · simp [hik]
                  _ = (∑ k : Fin n, (1 : ℝ)) - (∑ k : Fin n, (if i = k then (1 : ℝ) else 0)) := by
                    simp [This simp argument is unused:
  Finset.sum_add_distrib

Hint: Omit it from the simp argument list.
  simp ̵[̵F̵i̵n̵s̵e̵t̵.̵s̵u̵m̵_̵a̵d̵d̵_̵d̵i̵s̵t̵r̵i̵b̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Finset.sum_add_distrib]
                  _ = (n : ℝ) - 1 := by simp [Fintype.card_fin, Finset.sum_ite_eq, Finset.mem_univ]
              rw [hsum]
            _ = ((n : ℝ) - 1) / (n : ℝ) := by ring
        calc
          (∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then (1 / (n : ℝ)) else 0))
              = ∑ i : Fin n, (((n : ℝ) - 1) / (n : ℝ)) := by
                refine Finset.sum_congr rfl (fun i hi => ?_); rw [h_inner_sum i]
          _ = (n : ℝ) * (((n : ℝ) - 1) / (n : ℝ)) := by
            simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin]
          _ = (n : ℝ) - 1 := by
            field_simp [show (n : ℝ) ≠ 0 from by exact_mod_cast hn.ne']

  rw [h_cross_expect]
  nlinarith

Construction trials: expected trials to a collision-free secondary hash

A hash assignment a : Fin n → Fin (n^2) of n keys into n² slots is collision-free exactly when it is injective.

abbrev collisionFree {n : ℕ} (a : Fin n → Fin (n^2)) : Prop :=
  ∀ i j : Fin n, a i = a j → i = j

Split a sequence of k + 1 independent trial hashes into the first k trials and the last trial. This witnesses that the prefix coordinates are independent of the last coordinate.


noncomputable def trialsSplitLast {n k : ℕ} :
    (Fin (k + 1) → (Fin n → Fin (n^2))) ≃
      (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) where
  toFun A := ((fun j : Fin k => A (Fin.castSucc j)), A ⟨k, Nat.lt_succ_self k⟩)
  invFun q := fun x : Fin (k + 1) =>
    if hx : x.val < k then q.1 ⟨x.val, hx⟩ else q.2
  left_inv A := by
    funext x
    by_cases hx : x.val < k
    · simp [hx]
    · simp [hx]
      have hx' : x = ⟨k, Nat.lt_succ_self k⟩ := by
        apply Fin.ext
        change x.val = k
        omega
      rw [hx']
  right_inv q := by
    obtain ⟨P, L⟩ := q
    refine Prod.ext ?_ ?_
    · funext j
      simp
    · simp

Split a sequence of t independent trial hashes into the first k trials and the remaining t - k trials, for k ≤ t. This witnesses that the prefix coordinates are independent of the suffix coordinates.


noncomputable def trialsSplitPrefix {n t k : ℕ} (hkt : k ≤ t) :
    (Fin t → (Fin n → Fin (n^2))) ≃
      (Fin k → (Fin n → Fin (n^2))) × (Fin (t - k) → (Fin n → Fin (n^2))) where
  toFun A := ((fun j : Fin k => A (Fin.castLE hkt j)),
              (fun j : Fin (t - k) => A ⟨k + j.val, by omega⟩))
  invFun q := fun x : Fin t =>
    if hx : x.val < k then q.1 ⟨x.val, hx⟩ else q.2 ⟨x.val - k, by omega⟩
  left_inv A := by
    funext x
    by_cases hx : x.val < k
    · simp [hx]
    · simp [hx]
      apply congrArg A
      apply Fin.ext
      change k + (x.val - k) = x.val
      omega
  right_inv q := by
    obtain ⟨P, S⟩ := q
    refine Prod.ext ?_ ?_
    · funext j
      simp
    · funext j
      have hnot : ¬ k + j.val < k := by omega
      simp [hnot]

Independent-trials failure bound. In k independent trials, each of which produces a collision-free hash of n ≥ 2 keys into n² slots with probability at least 1/2 (Theorem 11.9), the probability that all k trials fail is at most (1/2)^k (CLRS §11.5).


theorem perfectHash_prefix_fail_prob_le {n k : ℕ} (hn : 2 ≤ n) :
    fintypeExpect (fun A : Fin k → (Fin n → Fin (n^2)) =>
      indicator (∀ j : Fin k, ¬ collisionFree (A j))) ≤ (1/2 : ℝ)^k := by
  induction k with
  | zero =>
      have htrue : ∀ A : Fin 0 → (Fin n → Fin (n^2)),
          (∀ j : Fin 0, ¬ collisionFree (A j)) := by
        intro A j
        exact Fin.elim0 j
      haveI : Nonempty (Fin n → Fin (n^2)) := ⟨fun _ => ⟨0, by
        have hnpos : 0 < n := by omega
        positivity⟩⟩
      have hcard : Fintype.card (Fin 0 → (Fin n → Fin (n^2))) ≠ 0 := Fintype.card_ne_zero
      calc
        fintypeExpect (fun A : Fin 0 → (Fin n → Fin (n^2)) =>
            indicator (∀ j : Fin 0, ¬ collisionFree (A j)))
            = fintypeExpect (fun _ : Fin 0 → (Fin n → Fin (n^2)) => (1 : ℝ)) := by
              refine congrArg fintypeExpect (funext fun A => ?_)
              have hP : (∀ j : Fin 0, ¬ collisionFree (A j)) := htrue A
              unfold indicator
              rw [if_pos hP]
        _ = 1 := by
              simp [fintypeExpect_const hcard]
        _ ≤ (1/2 : ℝ)^0 := by
              simp
  | succ k ih =>
      have hnpos : 0 < n := by omega
      haveI : Nonempty (Fin n) := ⟨⟨0, hnpos⟩⟩
      haveI : Nonempty (Fin n → Fin (n^2)) := ⟨fun _ => ⟨0, by positivity⟩⟩
      have hcardΩ : Fintype.card (Fin n → Fin (n^2)) ≠ 0 := Fintype.card_ne_zero
      -- `∀ j : Fin (k+1), ¬ CF (A j)` splits as the prefix conjunction and the
      -- last trial
      have hsplit : ∀ A : Fin (k + 1) → (Fin n → Fin (n^2)),
          indicator (∀ j : Fin (k + 1), ¬ collisionFree (A j))
            = indicator ((∀ j : Fin k, ¬ collisionFree (A (Fin.castSucc j))) ∧
                ¬ collisionFree (A ⟨k, Nat.lt_succ_self k⟩)) := by
        intro A
        have hiff : (∀ j : Fin (k + 1), ¬ collisionFree (A j)) ↔
            (∀ j : Fin k, ¬ collisionFree (A (Fin.castSucc j))) ∧
              ¬ collisionFree (A ⟨k, Nat.lt_succ_self k⟩) := by
          constructor
          · intro h
            constructor
            · intro j
              exact h (Fin.castSucc j)
            · exact h ⟨k, Nat.lt_succ_self k⟩
          · rintro ⟨hpre, hlast⟩ j
            by_cases hj : j.val < k
            · have hj' : j = Fin.castSucc ⟨j.val, hj⟩ := by
                ext
                rfl
              rw [hj']
              exact hpre ⟨j.val, hj⟩
            · have hj' : j = ⟨k, Nat.lt_succ_self k⟩ := by
                apply Fin.ext
                change j.val = k
                omega
              rw [hj']
              exact hlast
        unfold indicator
        by_cases hP1 : ∀ j : Fin (k + 1), ¬collisionFree (A j)
        · rw [if_pos hP1, if_pos (hiff.mp hP1)]
        · rw [if_neg hP1, if_neg (fun hP2 => hP1 (hiff.mpr hP2))]
      -- reindex the product sample space so the prefix and last trial separate
      have he := fintypeExpect_equiv (trialsSplitLast (n := n) (k := k))
        (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) =>
          indicator ((∀ j : Fin k, ¬ collisionFree (p.1 j)) ∧ ¬ collisionFree (p.2)))
      have hLHS : fintypeExpect (fun A : Fin (k + 1) → (Fin n → Fin (n^2)) =>
            indicator (∀ j : Fin (k + 1), ¬ collisionFree (A j)))
          = fintypeExpect (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) =>
              indicator ((∀ j : Fin k, ¬ collisionFree (p.1 j)) ∧ ¬ collisionFree (p.2))) := by
        calc
          fintypeExpect (fun A : Fin (k + 1) → (Fin n → Fin (n^2)) =>
                indicator (∀ j : Fin (k + 1), ¬ collisionFree (A j)))
              = fintypeExpect (fun A : Fin (k + 1) → (Fin n → Fin (n^2)) =>
                  indicator ((∀ j : Fin k, ¬ collisionFree (A (Fin.castSucc j))) ∧
                    ¬ collisionFree (A ⟨k, Nat.lt_succ_self k⟩))) := by
                refine congrArg fintypeExpect (funext fun A => hsplit A)
          _ = fintypeExpect (fun A : Fin (k + 1) → (Fin n → Fin (n^2)) =>
                  indicator ((∀ j : Fin k, ¬ collisionFree ((trialsSplitLast (n := n) (k := k) A).1 j)) ∧
                    ¬ collisionFree ((trialsSplitLast (n := n) (k := k) A).2))) := by
                refine congrArg fintypeExpect (funext fun A => ?_)
                simp [trialsSplitLast]
          _ = fintypeExpect (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) =>
                  indicator ((∀ j : Fin k, ¬ collisionFree (p.1 j)) ∧ ¬ collisionFree (p.2))) := he
      -- the conjunction of the independent prefix event and the last-trial event
      -- factorizes as a product of expectations
      have hprod : fintypeExpect (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) =>
              indicator ((∀ j : Fin k, ¬ collisionFree (p.1 j)) ∧ ¬ collisionFree (p.2)))
          = fintypeExpect (fun B : Fin k → (Fin n → Fin (n^2)) =>
              indicator (∀ j : Fin k, ¬ collisionFree (B j)))
            * fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a)) := by
        have hsplit2 : (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) =>
              indicator ((∀ j : Fin k, ¬ collisionFree (p.1 j)) ∧ ¬ collisionFree (p.2)))
            = (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) =>
                (fun B : Fin k → (Fin n → Fin (n^2)) => indicator (∀ j : Fin k, ¬ collisionFree (B j))) p.1
                  * (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a)) p.2) := by
          funext p
          by_cases hpre : ∀ j : Fin k, ¬ collisionFree (p.1 j)
          · by_cases hlast : ¬ collisionFree (p.2)
            · simp [indicator, hpre, hlast]
            · simp [indicator, hpre, hlast]
          · by_cases hlast : ¬ collisionFree (p.2)
            · simp [indicator, This simp argument is unused:
  hpre

Hint: Omit it from the simp argument list.
  simp [indicator, hp̵r̵e̵,̵ ̵h̵last]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hpre, hlast]
            · simp [indicator, This simp argument is unused:
  hpre

Hint: Omit it from the simp argument list.
  simp [indicator, hp̵r̵e̵,̵ ̵h̵last]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hpre, hlast]
        rw [hsplit2]
        exact expect_mul_of_indep (fun B : Fin k → (Fin n → Fin (n^2)) =>
          indicator (∀ j : Fin k, ¬ collisionFree (B j)))
          (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a))
      -- a single trial fails with probability at most 1/2 (Theorem 11.9)
      have hfail : fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a)) ≤ 1/2 := by
        have hE : fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a))
            = 1 - fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (collisionFree a)) := by
          calc
            fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a))
                = fintypeExpect (fun a : Fin n → Fin (n^2) => (1 : ℝ) - indicator (collisionFree a)) := by
                  refine congrArg fintypeExpect (funext fun a => ?_)
                  by_cases h : collisionFree a
                  · unfold indicator
                    rw [if_neg (fun hna => hna h), if_pos h]
                    simp
                  · unfold indicator
                    rw [if_pos h, if_neg h]
                    simp
            _ = fintypeExpect (fun a : Fin n → Fin (n^2) => (1 : ℝ) + (-indicator (collisionFree a))) := by
                  refine congrArg fintypeExpect (funext fun a => ?_)
                  ring
            _ = fintypeExpect (fun _ : Fin n → Fin (n^2) => (1 : ℝ)) +
                  fintypeExpect (fun a : Fin n → Fin (n^2) => -indicator (collisionFree a)) := fintypeExpect_add _ _
            _ = 1 - fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (collisionFree a)) := by
                  rw [fintypeExpect_const hcardΩ, fintypeExpect_neg]
                  ring
        rw [hE]
        have hcf : 1/2 ≤ fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (collisionFree a)) := by
          simpa [collisionFree] using (perfectHash_collision_free_prob_ge_half (n := n) hn)
        linarith
      -- assemble: E[prefix ∧ last] = E[prefix] · E[last] ≤ (1/2)^k · (1/2)
      calc
        fintypeExpect (fun A : Fin (k + 1) → (Fin n → Fin (n^2)) =>
            indicator (∀ j : Fin (k + 1), ¬ collisionFree (A j)))
            = fintypeExpect (fun B : Fin k → (Fin n → Fin (n^2)) =>
                indicator (∀ j : Fin k, ¬ collisionFree (B j)))
              * fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a)) := by
              rw [hLHS, hprod]
        _ ≤ (1/2 : ℝ)^k * (1/2) := by
              exact mul_le_mul ih hfail
                (fintypeExpect_nonneg (fun a : Fin n → Fin (n^2) => by
                  unfold indicator
                  split <;> norm_num))
                (by positivity)
        _ = (1/2 : ℝ)^(k + 1) := by
              simp [pow_succ]

The probability that the first k of t independent trials all fail is at most (1/2)^k: the remaining t - k trials are independent of the prefix and marginalise out.


theorem perfectHash_trials_prefix_fail_prob_le {n k t : ℕ} (hn : 2 ≤ n) (hkt : k ≤ t) :
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
      indicator (∀ j : Fin k, ¬ collisionFree (A (Fin.castLE hkt j)))) ≤ (1/2 : ℝ)^k := by
  haveI : Nonempty (Fin n → Fin (n^2)) := ⟨fun _ => ⟨0, by
    have hnpos : 0 < n := by omega
    positivity⟩⟩
  have hcard_suffix : Fintype.card (Fin (t - k) → (Fin n → Fin (n^2))) ≠ 0 := Fintype.card_ne_zero
  have hpre : fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
        indicator (∀ j : Fin k, ¬ collisionFree (A (Fin.castLE hkt j))))
      = fintypeExpect (fun B : Fin k → (Fin n → Fin (n^2)) =>
        indicator (∀ j : Fin k, ¬ collisionFree (B j))) := by
    calc
      fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
            indicator (∀ j : Fin k, ¬ collisionFree (A (Fin.castLE hkt j))))
          = fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
              indicator (∀ j : Fin k, ¬ collisionFree ((trialsSplitPrefix hkt A).1 j))) := by
            refine congrArg fintypeExpect (funext fun A => ?_)
            simp [trialsSplitPrefix]
      _ = fintypeExpect (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin (t - k) → (Fin n → Fin (n^2))) =>
            indicator (∀ j : Fin k, ¬ collisionFree (p.1 j))) := by
            exact fintypeExpect_equiv (trialsSplitPrefix hkt)
              (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin (t - k) → (Fin n → Fin (n^2))) =>
                indicator (∀ j : Fin k, ¬ collisionFree (p.1 j)))
      _ = fintypeExpect (fun B : Fin k → (Fin n → Fin (n^2)) =>
            indicator (∀ j : Fin k, ¬ collisionFree (B j))) := by
            exact fintypeExpect_fst hcard_suffix
              (fun B : Fin k → (Fin n → Fin (n^2)) => indicator (∀ j : Fin k, ¬ collisionFree (B j)))
  rw [hpre]
  exact perfectHash_prefix_fail_prob_le hn

The number of failed trials before the first collision-free trial in a sequence of t independent trials. Equivalently, the sum over k of the indicators "the first k + 1 trials all fail": each failing trial before the first success contributes exactly one such prefix. If every trial fails, the value is t.

noncomputable def failedTrials {n t : ℕ} (A : Fin t → (Fin n → Fin (n^2))) : ℕ :=
  (Finset.univ.filter (fun k : Fin t =>
    ∀ j : Fin (k.val + 1), ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j)))).card

failedTrials decomposes as the sum over trial prefixes of the indicator that the first k + 1 trials all fail.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
theorem failedTrials_eq_sum {n t : ℕ} (A : Fin t → (Fin n → Fin (n^2))) :
    failedTrials A = ∑ k : Fin t, (if (∀ j : Fin (k.val + 1),
      ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j))) then 1 else 0) := by
  unfold failedTrials
  -- (Finset.univ.filter p).card = ∑ k ∈ univ, if p k then 1 else 0
  try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa using (Finset.sum_boole (fun k : Fin t => ∀ j : Fin (k.val + 1),
    ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j)))
    (Finset.univ : Finset (Fin t))).symm

Expected failed trials before a collision-free hash. In the truncated model of t independent trials (each collision-free with probability at least 1/2, Theorem 11.9), the expected number of failed trials before the first collision-free trial is at most 1 — via the tail-sum identity E[F] = Σ_k P[first k trials fail] ≤ Σ_k (1/2)^k = 1 (CLRS §11.5).


theorem perfectHash_expected_failedTrials_le_one {n t : ℕ} (hn : 2 ≤ n) :
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ)) ≤ 1 := by
  have hdecomp : (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ))
      = (fun A : Fin t → (Fin n → Fin (n^2)) => ∑ k : Fin t,
          indicator (∀ j : Fin (k.val + 1),
            ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j)))) := by
    funext A
    rw [failedTrials_eq_sum A]
    simp [indicator, This simp argument is unused:
  Nat.cast_sum

Hint: Omit it from the simp argument list.
  simp [indicator,̵ ̵N̵a̵t̵.̵c̵a̵s̵t̵_̵s̵u̵m̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Nat.cast_sum]
  have hlin : fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ))
      = ∑ k : Fin t, fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
          indicator (∀ j : Fin (k.val + 1),
            ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j)))) := by
    rw [hdecomp]
    exact fintypeExpect_sum Finset.univ _
  have hterm : ∀ k : Fin t, fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
        indicator (∀ j : Fin (k.val + 1),
          ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j)))) ≤ (1/2 : ℝ)^(k.val + 1) := by
    intro k
    exact perfectHash_trials_prefix_fail_prob_le hn (Nat.succ_le_of_lt k.isLt)
  calc
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ))
        ≤ ∑ k : Fin t, (1/2 : ℝ)^(k.val + 1) := by
          rw [hlin]
          exact Finset.sum_le_sum (fun k _ => hterm k)
    _ ≤ 1 := by
          -- ∑ k : Fin t, (1/2)^(k.val + 1) = (1/2) · ∑ k : Fin t, (1/2)^k.val ≤ (1/2) · 2 = 1
          have hfactor : (∑ k : Fin t, (1/2 : ℝ)^(k.val + 1)) = (1/2) * (∑ k : Fin t, (1/2 : ℝ)^k.val) := by
            calc
              (∑ k : Fin t, (1/2 : ℝ)^(k.val + 1))
                  = (∑ k : Fin t, (1/2 : ℝ)^k.val * (1/2)) := by
                    refine Finset.sum_congr rfl (fun k _ => ?_)
                    rw [pow_succ]
              _ = (1/2) * (∑ k : Fin t, (1/2 : ℝ)^k.val) := by
                    rw [Finset.mul_sum]
                    simp [mul_comm]
          rw [hfactor]
          have hgeom : (∑ k : Fin t, (1/2 : ℝ)^k.val) ≤ 2 := by
            have hrange : (∑ k : Fin t, (1/2 : ℝ)^k.val) = ∑ i ∈ Finset.range t, (1/2 : ℝ)^i := by
              rw [Fin.sum_univ_eq_sum_range (fun i : ℕ => (1/2 : ℝ)^i) t]
            rw [hrange]
            have hgeom_mul := geom_sum_mul_of_le_one (x := (1/2 : ℝ)) (by norm_num) t
            -- (∑ i ∈ range t, (1/2)^i) * (1 - 1/2) = 1 - (1/2)^t, so the product is ≤ 1
            have hmul : (∑ i ∈ Finset.range t, (1/2 : ℝ)^i) * (1/2) ≤ 1 := by
              norm_num at hgeom_mul
              rw [hgeom_mul]
              have hpow : 0 ≤ (1/2 : ℝ)^t := by positivity
              nlinarith
            nlinarith
          nlinarith

The number of trials performed until a collision-free secondary hash is obtained, in a truncated model of t independent trials: the failed trials before the first collision-free trial, plus the successful trial itself. If none of the t trials is collision-free, the value is t + 1. This is a lower truncation of an unbounded waiting time, not an upper estimate. A constructor using a guaranteed terminal fallback may instead interpret the last unit as its successful fallback attempt; that requires a separate bridge.

noncomputable def trialsUntilCollisionFree {n t : ℕ} (A : Fin t → (Fin n → Fin (n^2))) : ℕ :=
  failedTrials A + 1

Expected number of trials to obtain a collision-free secondary hash. In the truncated model of t independent trials — each trial hashes n ≥ 2 keys into n² slots and is collision-free with probability at least 1/2 (Theorem 11.9) — the expected number of trials performed up to and including the first collision-free trial is at most 2 (CLRS §11.5). This theorem bounds each finite truncation. It does not by itself supply an infinite trial process or a limit theorem for its expectation.


theorem perfectHash_expected_trials_le_two {n t : ℕ} (hn : 2 ≤ n) :
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (trialsUntilCollisionFree A : ℝ)) ≤ 2 := by
  unfold trialsUntilCollisionFree
  calc
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => ((failedTrials A + 1 : ℕ) : ℝ))
        = fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ) + 1) := by
          refine congrArg fintypeExpect (funext fun A => ?_)
          simp
    _ = fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ)) + 1 := by
          calc
            fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ) + 1)
                = fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ)) +
                    fintypeExpect (fun _ : Fin t → (Fin n → Fin (n^2)) => (1 : ℝ)) := fintypeExpect_add _ _
            _ = fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ)) + 1 := by
                  haveI : Nonempty (Fin n → Fin (n^2)) := ⟨fun _ => ⟨0, by
                    have hnpos : 0 < n := by omega
                    positivity⟩⟩
                  have hcard : Fintype.card (Fin t → (Fin n → Fin (n^2))) ≠ 0 := Fintype.card_ne_zero
                  simp [fintypeExpect_const hcard]
    _ ≤ 2 := by
          linarith [perfectHash_expected_failedTrials_le_one (n := n) (t := t) hn]

Existence of a collision-free secondary hash. For n ≥ 2 keys hashed into n² slots, some hash assignment is injective. This follows from Theorem 11.9: the collision-free probability is at least 1/2 > 0, so the event cannot be empty (CLRS §11.5).


theorem exists_collision_free_secondary {n : ℕ} (hn : 2 ≤ n) :
    ∃ a : Fin n → Fin (n^2), ∀ i j : Fin n, a i = a j → i = j := by
  by_contra h
  have hnone : ∀ a : Fin n → Fin (n^2), ¬ (∀ i j : Fin n, a i = a j → i = j) := by
    intro a ha
    exact h ⟨a, ha⟩
  have hzero : fintypeExpect (fun a : Fin n → Fin (n^2) =>
      indicator (∀ i j : Fin n, a i = a j → i = j)) = 0 := by
    unfold fintypeExpect
    rw [show (∑ a : Fin n → Fin (n ^ 2), indicator (∀ i j : Fin n, a i = a j → i = j)) = 0 by
      apply Finset.sum_eq_zero
      intro a ha
      exact if_neg (hnone a)]
    simp
  have hcf := perfectHash_collision_free_prob_ge_half (n := n) hn
  linarith

Abstract construction budget and its finite expectation

Historical abstract two-level budget: primary size plus twice the sum of squared bucket sizes. This is an analysis expression, not measured execution. The companion Construction module supplies a counted constructor and a constant-factor conditional-expectation bridge to this expression.

noncomputable def constructionCost {n : ℕ} (a : Fin n → Fin n) : ℝ :=
  (n : ℝ) + 2 * totalSecondarySpace a

Expected finite trial-count budget times squared bucket size, for at least two keys. The expression charges a supplied square cost per trial; actual collision checking, initialization, and placement are counted in the companion.


theorem perfectHash_expected_bucket_cost_le {n t : ℕ} (hn : 2 ≤ n) :
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
      (trialsUntilCollisionFree A : ℝ) * (n : ℝ)^2) ≤ 2 * (n : ℝ)^2 := by
  have hsq : 0 ≤ (n : ℝ)^2 := by positivity
  calc
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
        (trialsUntilCollisionFree A : ℝ) * (n : ℝ)^2)
        = (n : ℝ)^2 * fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
            (trialsUntilCollisionFree A : ℝ)) := by
          have hswap : (fun A : Fin t → (Fin n → Fin (n^2)) =>
              (trialsUntilCollisionFree A : ℝ) * (n : ℝ)^2)
              = (fun A : Fin t → (Fin n → Fin (n^2)) => (n : ℝ)^2 * (trialsUntilCollisionFree A : ℝ)) := by
            funext A
            ring
          rw [hswap]
          exact fintypeExpect_const_mul ((n : ℝ)^2) (fun A : Fin t → (Fin n → Fin (n^2)) =>
            (trialsUntilCollisionFree A : ℝ))
    _ ≤ (n : ℝ)^2 * 2 := by
          exact mul_le_mul_of_nonneg_left (perfectHash_expected_trials_le_two hn) hsq
    _ = 2 * (n : ℝ)^2 := by
          ring

The historical abstract construction budget has expectation below 5n under uniform primary assignment. The theorem name is retained for compatibility; executed construction costs require the companion's refinement theorem.


theorem perfectHash_expected_construction_time_le_const_n {n : ℕ} (hn : 0 < n) :
    fintypeExpect (fun a : Fin n → Fin n => constructionCost a) < 5 * (n : ℝ) := by
  have hlin : fintypeExpect (fun a : Fin n → Fin n => constructionCost a)
      = (n : ℝ) + 2 * fintypeExpect (fun a : Fin n → Fin n => totalSecondarySpace a) := by
    unfold constructionCost
    calc
      fintypeExpect (fun a : Fin n → Fin n => (n : ℝ) + 2 * totalSecondarySpace a)
          = fintypeExpect (fun _ : Fin n → Fin n => (n : ℝ)) +
              fintypeExpect (fun a : Fin n → Fin n => 2 * totalSecondarySpace a) :=
            fintypeExpect_add _ _
      _ = (n : ℝ) + 2 * fintypeExpect (fun a : Fin n → Fin n => totalSecondarySpace a) := by
            haveI : Nonempty (Fin n) := ⟨⟨0, hn⟩⟩
            have hcard : Fintype.card (Fin n → Fin n) ≠ 0 := Fintype.card_ne_zero
            rw [fintypeExpect_const hcard, fintypeExpect_const_mul]
  rw [hlin]
  have hspace := perfectHash_expected_total_space_lt_2n hn
  nlinarith

end Chapter11end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_11.Section_11_5_Perfect_Hashing.Construction.Secondary

Executed finite secondary perfect-hash construction

Every candidate runs a collision check, initializes its secondary slot array, and places its local key indices. The returned ledger counts hash evaluations, equality comparisons, slot initialization, and indexed writes. Supplied finite traces stop on success; exhaustion executes a deterministic injective fallback. Thus the actual attempts equal the existing failedTrials + 1 statistic.

Hashes act on local indices Fin n. Hash-family sampling and representation costs are outside this indexed-operation model. The finite expectation concerns uniform full assignments, and is not a theorem about an unbounded retry process.

namespace CLRS.Chapter11.PerfectConstruction

Hash equality tests, charged for two hash evaluations and one comparison.

def differsFrom (a : α → β) [DecidableEq β] (x : α) : List α → Bool × Nat
  | [] => (true, 0)
  | y :: ys =>
      if a x = a y then (false, 3)
      else let rest := differsFrom a x ys; (rest.1, rest.2 + 3)

theorem differsFrom_correct (a : α → β) [DecidableEq β] (x : α) (xs : List α) :
    (differsFrom a x xs).1 = true ↔ ∀ y ∈ xs, a x ≠ a y := by
  induction xs with
  | nil => simp [differsFrom]
  | cons y ys ih => by_cases h : a x = a y <;> simp [differsFrom, h, ih]

theorem differsFrom_work_le (a : α → β) [DecidableEq β] (x : α) (xs : List α) :
    (differsFrom a x xs).2 ≤ 3 * xs.length := by
  induction xs with
  | nil => simp [differsFrom]
  | cons y ys ih => simp only [differsFrom]; split <;> simp_all; omega

Check all distinct input positions, stopping at the first duplicate hash.

def checkDistinct (a : α → β) [DecidableEq β] : List α → Bool × Nat
  | [] => (true, 0)
  | x :: xs =>
      let head := differsFrom a x xs
      if head.1 then
        let tail := checkDistinct a xs
        (tail.1, head.2 + tail.2)
      else (false, head.2)

              theorem checkDistinct_correct (a : α → β) [DecidableEq β] (xs : List α) :
    (checkDistinct a xs).1 = true ↔ (xs.map a).Nodup := by
  induction xs with
  | nil => simp [checkDistinct]
  | cons x xs ih =>
      simp only [checkDistinct]
      split
      next h =>
        have hh := (differsFrom_correct a x xs).mp h
        simp only [List.map_cons, List.nodup_cons, List.mem_map]
        constructor
        · intro ht
          exact ⟨by rintro ⟨y, hy, he⟩; exact hh y hy he.symm, ih.mp ht⟩
        · intro ht; exact ih.mpr ht.2
      next h =>
        simp only [Bool.false_eq_true, List.map_cons, List.nodup_cons, false_iff]
        intro hn
        apply h
        apply (differsFrom_correct a x xs).mpr
        intro y hy he
        exact hn.1 (List.mem_map.mpr ⟨y, hy, he.symm⟩)theorem checkDistinct_work_le (a : α → β) [DecidableEq β] (xs : List α) :
    (checkDistinct a xs).2 ≤ 3 * xs.length ^ 2 := by
  induction xs with
  | nil => simp [checkDistinct]
  | cons x xs ih =>
      have hh := differsFrom_work_le a x xs
      simp only [checkDistinct]
      split <;> simp only [List.length_cons] <;> nlinarithabbrev Hash (n : Nat) := Fin n → Fin (n ^ 2)

theorem check_hash_correct {n : Nat} (a : Hash n) :
    (checkDistinct a (List.finRange n)).1 = true ↔ collisionFree a := by
  rw [checkDistinct_correct, List.nodup_map_iff_inj_on (List.nodup_finRange n)]
  simp [collisionFree]

Initialize actual empty secondary slots, counting each array push.

def emptySlots (α : Type*) : Nat → Array (Option α) × Nat
  | 0 => (#[], 0)
  | m + 1 => let prev := emptySlots α m; (prev.1.push none, prev.2 + 1)

@[simp] theorem emptySlots_array (α : Type*) (m : Nat) :
    (emptySlots α m).1 = Array.replicate m none := by
  induction m with
  | zero => simp [emptySlots]
  | succ m ih => simp [emptySlots, ih, Array.replicate_succ]

@[simp] theorem emptySlots_work (α : Type*) (m : Nat) : (emptySlots α m).2 = m := by
  induction m with
  | zero => rfl
  | succ m ih => simp [emptySlots, ih]

Place each key in its selected slot. A step charges a hash evaluation and an indexed write; initialization and collision checks are counted separately.

def place {n : Nat} (a : Hash n) : List (Fin n) → Array (Option (Fin n)) →
    Array (Option (Fin n)) × Nat
  | [], out => (out, 0)
  | i :: is, out =>
      let rest := place a is out
      (rest.1.setIfInBounds (a i).val (some i), rest.2 + 2)

@[simp] theorem place_size {n : Nat} (a : Hash n) (xs : List (Fin n)) (out : Array (Option (Fin n))) :
    (place a xs out).1.size = out.size := by
  induction xs with
  | nil => rfl
  | cons i xs ih => simp [place, ih]

@[simp] theorem place_work {n : Nat} (a : Hash n) (xs : List (Fin n)) (out : Array (Option (Fin n))) :
    (place a xs out).2 = 2 * xs.length := by
  induction xs with
  | nil => simp [place]
  | cons i xs ih => simp [place, ih]; omega

Each slot contains the first input key assigned there, or its initial value.


theorem place_get {n : Nat} (a : Hash n) (xs : List (Fin n))
    (out : Array (Option (Fin n))) (s : Nat) (hs : s < out.size) :
    (place a xs out).1[s]'(by simpa using hs) =
      (xs.find? (fun i => (a i).val == s)).orElse (fun _ => out[s]) := by
  induction xs with
  | nil => simp [place]
  | cons i xs ih =>
      simp only [place]
      rw [Array.getElem_setIfInBounds (by simpa using hs)]
      by_cases he : (a i).val = s <;> simp [he, List.find?, ih, Bool.beq_eq_decide_eq]

structure Attempt (n : Nat) where
  hash : Hash n
  slots : Array (Option (Fin n))
  success : Bool
  work : Nat

An actual collision check followed by secondary-array placement.

def attempt {n : Nat} (a : Hash n) : Attempt n :=
  let checked := checkDistinct a (List.finRange n)
  let initial := emptySlots (Fin n) (n ^ 2)
  let filled := place a (List.finRange n) initial.1
  ⟨a, filled.1, checked.1, checked.2 + initial.2 + filled.2⟩

              @[simp] theorem attempt_hash {n : Nat} (a : Hash n) : (attempt a).hash = a := rfl@[simp] theorem attempt_size {n : Nat} (a : Hash n) : (attempt a).slots.size = n ^ 2 := by
  simp [attempt]@[simp] theorem attempt_success {n : Nat} (a : Hash n) :
    (attempt a).success = true ↔ collisionFree a := check_hash_correct a

theorem attempt_work_le {n : Nat} (a : Hash n) : (attempt a).work ≤ 6 * n ^ 2 := by
  have h := checkDistinct_work_le a (List.finRange n)
  have hn : n ≤ n ^ 2 := by nlinarith
  simpa only [attempt, emptySlots_work, place_work, List.length_finRange] using
    (show (checkDistinct a (List.finRange n)).2 + n ^ 2 + 2 * n ≤ 6 * n ^ 2 by
      simp only [List.length_finRange] at h
      nlinarith)

theorem attempt_get {n : Nat} (a : Hash n) (s : Nat) (hs : s < n ^ 2) :
    (attempt a).slots[s]'(by simpa using hs) =
      (List.finRange n).find? (fun i => (a i).val == s) := by
  have h := place_get a (List.finRange n) (emptySlots (Fin n) (n ^ 2)).1 s (by simpa using hs)
  simpa [attempt] using h

theorem attempt_stores {n : Nat} (a : Hash n) (ha : collisionFree a) (i : Fin n) :
    (attempt a).slots[(a i).val]'(by simp) = some i := by
  rw [attempt_get a _ (a i).isLt]
  cases h : (List.finRange n).find? (fun j => (a j).val == (a i).val) with
  | none =>
      have hh := List.find?_eq_none.mp h i (by simp)
      simp at hh
  | some j =>
      have hh := List.find?_some h
      have he : a j = a i := Fin.ext (by simpa using hh)
      rw [ha j i he]

The terminal assignment is explicitly injective, including the empty domain.

def fallback (n : Nat) : Hash n := fun i =>
  ⟨i.val, lt_of_lt_of_le i.isLt (by nlinarith : n ≤ n ^ 2)⟩

theorem fallback_injective (n : Nat) : collisionFree (fallback n) := by
  intro i j hij
  exact Fin.ext (congrArg (fun x : Fin (n ^ 2) => x.val) hij)

structure Build (n : Nat) where
  selected : Attempt n
  attempts : Nat
  work : Nat

Try supplied candidates in order; after their exhaustion execute one explicit injective fallback. Every returned table therefore succeeds.

def build {n : Nat} : List (Hash n) → Build n
  | [] => let final := attempt (fallback n); ⟨final, 1, final.work⟩
  | a :: as =>
      let trial := attempt a
      if trial.success then ⟨trial, 1, trial.work⟩
      else let rest := build as; ⟨rest.selected, rest.attempts + 1, trial.work + rest.work⟩

              theorem build_success {n : Nat} (as : List (Hash n)) : (build as).selected.success = true := by
  induction as with
  | nil => simpa [build] using (attempt_success (fallback n)).mpr (fallback_injective n)
  | cons a as ih =>
      simp only [build]
      split
      · assumption
      · exact ihtheorem build_work_le {n : Nat} (as : List (Hash n)) :
    (build as).work ≤ 6 * n ^ 2 * (build as).attempts := by
  induction as with
  | nil => simpa [build] using attempt_work_le (fallback n)
  | cons a as ih =>
      have h := attempt_work_le a
      simp only [build]
      split <;> simp only <;> nlinarithdef failedPrefix {n : Nat} : List (Hash n) → Nat
  | [] => 0
  | a :: as => if (attempt a).success then 0 else failedPrefix as + 1theorem build_attempts {n : Nat} (as : List (Hash n)) :
    (build as).attempts = failedPrefix as + 1 := by
  induction as with
  | nil => simp [build, failedPrefix]
  | cons a as ih => simp only [build, failedPrefix]; split <;> simp_all


lemma failedTrials_cons {n t : Nat} (A : Fin (t + 1) → Hash n) :
    failedTrials A = if collisionFree (A 0) then 0 else
      failedTrials (fun j : Fin t => A j.succ) + 1 := by
  classical
  rw [failedTrials_eq_sum, Fin.sum_univ_succ]
  have htail (k : Fin t) :
      (∀ j : Fin (k.succ.val + 1),
        ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.succ.isLt) j))) ↔
      (¬ collisionFree (A 0) ∧ ∀ j : Fin (k.val + 1),
        ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j).succ)) := by
    rw [Fin.forall_fin_succ]
    rfl
  have hzero :
      (∀ j : Fin ((0 : Fin (t + 1)).val + 1),
        ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt (0 : Fin (t + 1)).isLt) j))) ↔
      ¬ collisionFree (A 0) := by
    constructor
    · intro hh
      exact hh 0
    · intro hh j
      have hj : Fin.castLE (Nat.succ_le_of_lt (0 : Fin (t + 1)).isLt) j = 0 := by
        apply Fin.ext
        have h := j.isLt
        change j.val < 1 at h
        change j.val = 0
        omega
      rw [hj]
      exact hh
  simp_rw [htail, hzero]
  by_cases h : collisionFree (A 0)
  · have hh : collisionFree (A 0) ↔ True := iff_true_intro h
    simp only [hh, not_true_eq_false, false_and, ite_false, Finset.sum_const_zero,
      zero_add, ite_true]
  · simp only [h, not_false_eq_true, true_and, ite_true, ite_false]
    rw [failedTrials_eq_sum]
    omega

theorem failedPrefix_ofFn {n t : Nat} (A : Fin t → Hash n) :
    failedPrefix (List.ofFn A) = failedTrials A := by
  classical
  induction t with
  | zero => simp [List.ofFn_zero, failedPrefix, failedTrials]
  | succ t ih =>
      rw [List.ofFn_succ, failedPrefix, failedTrials_cons]
      simp only [attempt_success, ih]def buildTrace {n : Nat} : {t : Nat} → (Fin t → Hash n) → Build n
  | 0, _ => build []
  | _ + 1, A =>
      let current := attempt (A 0)
      if current.success then ⟨current, 1, current.work⟩
      else
        let rest := buildTrace (fun j => A j.succ)
        ⟨rest.selected, rest.attempts + 1, current.work + rest.work⟩theorem buildTrace_eq {n t : Nat} (A : Fin t → Hash n) :
    buildTrace A = build (List.ofFn A) := by
  induction t with
  | zero => simp [buildTrace]
  | succ t ih => simp [buildTrace, List.ofFn_succ, build, ih]

The legacy finite trial random variable is the exact attempt count of finite sampling followed by the terminal injective fallback.


theorem buildTrace_attempts {n t : Nat} (A : Fin t → Hash n) :
    (buildTrace A).attempts = trialsUntilCollisionFree A := by
  rw [buildTrace_eq, build_attempts, failedPrefix_ofFn, trialsUntilCollisionFree]

theorem buildTrace_work_le {n t : Nat} (A : Fin t → Hash n) :
    (buildTrace A).work ≤ 6 * n ^ 2 * trialsUntilCollisionFree A := by
  simpa [← buildTrace_attempts A, buildTrace_eq] using build_work_le (List.ofFn A)

open CLRS.Probability

Expected measured secondary work over the stated finite SUHA trace space.

theorem expected_buildTrace_work_le {n t : Nat} (hn : 2 ≤ n) :
    fintypeExpect (fun A : Fin t → Hash n => ((buildTrace A).work : ℝ)) ≤
      12 * (n : ℝ) ^ 2 := by
  classical
  calc
    fintypeExpect (fun A : Fin t → Hash n => ((buildTrace A).work : ℝ)) ≤
        fintypeExpect (fun A : Fin t → Hash n =>
          6 * (n : ℝ) ^ 2 * (trialsUntilCollisionFree A : ℝ)) := by
      apply fintypeExpect_mono
      intro A
      exact_mod_cast buildTrace_work_le A
    _ = (6 * (n : ℝ) ^ 2) *
        fintypeExpect (fun A : Fin t → Hash n => (trialsUntilCollisionFree A : ℝ)) :=
      fintypeExpect_const_mul _ _
    _ ≤ (6 * (n : ℝ) ^ 2) * 2 :=
      mul_le_mul_of_nonneg_left (perfectHash_expected_trials_le_two hn) (by positivity)
    _ = _ := by ring

Every selected result is a real executed secondary attempt.

theorem build_selected_eq {n : Nat} (as : List (Hash n)) :
    (build as).selected = attempt (build as).selected.hash := by
  induction as with
  | nil => rfl
  | cons a as ih => simp only [build]; split <;> first | rfl | exact ih



theorem build_hash_injective {n : Nat} (as : List (Hash n)) :
    collisionFree (build as).selected.hash := by
  have h := build_success as
  rw [build_selected_eq] at h
  exact attempt_success _ |>.mp h



theorem attempt_only {n : Nat} (a : Hash n) (s : Nat) (i : Fin n)
    (h : (attempt a).slots[s]?.join = some i) : (a i).val = s := by
  by_cases hs : s < n ^ 2
  · have hsize : s < (attempt a).slots.size := by simpa using hs
    rw [Array.getElem?_eq_getElem hsize, Option.join_some, attempt_get a s hs] at h
    have hh := List.find?_some h
    simpa using hh
  · have hsize : ¬ s < (attempt a).slots.size := by simpa using hs
    simp [Array.getElem?_eq_none (Nat.le_of_not_gt hsize)] at h

Package the constructed array as a one-bucket perfect table. All key slots come from the returned placement execution, rather than from a specification search.


def tableOfBuild {n : Nat} (as : List (Hash n)) : PerfectHashTable (Fin n) 1 where
  keys := Finset.univ
  prim := fun _ => 0
  sec := fun _ i => ((build as).selected.hash i).val
  table := fun _ s => (build as).selected.slots[s]?.join
  sec_inj := by
    intro j x y hx hy hpx hpy hs
    exact build_hash_injective as x y (Fin.ext hs)
  table_stores_keys := by
    intro i hi
    rw [build_selected_eq]
    have hs := attempt_stores (build as).selected.hash (build_hash_injective as) i
    simp only [attempt_hash]
    rw [Array.getElem?_eq_getElem (by simp), Option.join_some]
    exact hs
  table_only_keys := by
    intro j s i hi
    refine ⟨by simp, Subsingleton.elim _ _, ?_⟩
    rw [build_selected_eq] at hi
    exact attempt_only _ s i hi

The successful finite builder has a verified membership-query interface.


theorem tableOfBuild_search {n : Nat} (as : List (Hash n)) (i : Fin n) :
    perfectSearch (tableOfBuild as) i := by
  rw [perfectSearch_iff_mem]
  simp [tableOfBuild]




theorem build_work_le_small {n : Nat} (hn : n ≤ 1) (as : List (Hash n)) :
    (build as).work ≤ 6 * n ^ 2 := by
  cases as with
  | nil => simpa [build] using attempt_work_le (fallback n)
  | cons a as =>
      have hc : collisionFree a := by
        intro i j hij
        apply Fin.ext
        have hi := i.isLt
        have hj := j.isLt
        omega
      have hs := (attempt_success a).mpr hc
      simpa only [build, hs, Bool.true_eq, ↓reduceIte] using attempt_work_le a

Empty and singleton buckets are handled directly; the SUHA retry bound is needed only for buckets with at least two keys.


theorem expected_buildTrace_work_le_all (n t : Nat) :
    fintypeExpect (fun A : Fin t → Hash n => ((buildTrace A).work : ℝ)) ≤
      12 * (n : ℝ) ^ 2 := by
  classical
  by_cases hn : 2 ≤ n
  · exact expected_buildTrace_work_le hn
  haveI : Nonempty (Fin t → Hash n) := ⟨fun _ => fallback n⟩
  calc
    fintypeExpect (fun A : Fin t → Hash n => ((buildTrace A).work : ℝ)) ≤
        fintypeExpect (fun _ : Fin t → Hash n => 6 * (n : ℝ) ^ 2) := by
      apply fintypeExpect_mono
      intro A
      rw [buildTrace_eq]
      exact_mod_cast build_work_le_small (by omega : n ≤ 1) (List.ofFn A)
    _ = 6 * (n : ℝ) ^ 2 := fintypeExpect_const Fintype.card_ne_zero _
    _ ≤ _ := by nlinarith [sq_nonneg (n : ℝ)]

end CLRS.Chapter11.PerfectConstruction

CLRSLean.FourthEdition.Chapter_11.Section_11_5_Perfect_Hashing.Construction.TwoLevel

Measured assembly of all secondary tables

The constructor actually distributes original Fin n payloads into primary buckets, caches bucket sizes, and executes and retains every secondary builder. The measured indexed-operation work has conditional expectation at most nine times constructionCost and unconditional expectation below 45 * n.

Secondary tables hash and store local bucket indices. Original payload buckets remain in the result; converting an original query key to its local index is a separate representation boundary. This does not claim constant-time hashing on an arbitrary original key universe or machine runtime for persistent arrays.

namespace CLRS.Chapter11.PerfectConstructionopen CLRS.Probability

Uniform dependent-product sampling has the expected one-coordinate marginal.

theorem expect_pi_apply {ι : Type} [Fintype ι] [DecidableEq ι]
    (Ω : ι → Type) [∀ i, Fintype (Ω i)] [∀ i, DecidableEq (Ω i)]
    [∀ i, Nonempty (Ω i)] (j : ι) (X : Ω j → ℝ) :
    fintypeExpect (fun w : (i : ι) → Ω i => X (w j)) = fintypeExpect X := by
  classical
  calc
    fintypeExpect (fun w : (i : ι) → Ω i => X (w j)) =
        fintypeExpect (fun p : Ω j × ((i : {i : ι // i ≠ j}) → Ω i.val) => X p.1) :=
      fintypeExpect_equiv (Equiv.piSplitAt j Ω) (fun p => X p.1)
    _ = _ := fintypeExpect_fst Fintype.card_ne_zero X

structure Assembly {m : Nat} (sizes : Fin m → Nat) where
  buckets : Array (Σ j : Fin m, Build (sizes j))
  work : Nat

Execute every bucket constructor, storing its returned table in the output array. Each push of a completed bucket record contributes one more operation.

def assemble {m t : Nat} (sizes : Fin m → Nat)
    (A : (j : Fin m) → Fin t → Hash (sizes j)) :
    List (Fin m) → Array (Σ j : Fin m, Build (sizes j)) → Assembly sizes
  | [], out => ⟨out, 0⟩
  | j :: js, out =>
      let built := buildTrace (A j)
      let rest := assemble sizes A js (out.push ⟨j, built⟩)
      ⟨rest.buckets, built.work + 1 + rest.work⟩

              theorem assemble_result {m t : Nat} (sizes : Fin m → Nat)
    (A : (j : Fin m) → Fin t → Hash (sizes j))
    (js : List (Fin m)) (out : Array (Σ j : Fin m, Build (sizes j))) :
    (assemble sizes A js out).buckets.toList =
      out.toList ++ js.map (fun j => ⟨j, buildTrace (A j)⟩) := by
  induction js generalizing out with
  | nil => simp [assemble]
  | cons j js ih => simp [assemble, ih, List.append_assoc]theorem assemble_work {m t : Nat} (sizes : Fin m → Nat)
    (A : (j : Fin m) → Fin t → Hash (sizes j))
    (js : List (Fin m)) (out : Array (Σ j : Fin m, Build (sizes j))) :
    (assemble sizes A js out).work = js.length + (js.map (fun j => (buildTrace (A j)).work)).sum := by
  induction js generalizing out with
  | nil => simp [assemble]
  | cons j js ih => simp [assemble, ih]; omega

theorem assemble_success {m t : Nat} (sizes : Fin m → Nat)
    (A : (j : Fin m) → Fin t → Hash (sizes j)) :
    ∀ entry ∈ (assemble sizes A (List.finRange m) #[]).buckets.toList,
      entry.2.selected.success = true := by
  rw [assemble_result]
  simp only [List.nil_append, List.mem_map]
  rintro entry ⟨j, hj, rfl⟩
  simpa only [buildTrace_eq] using build_success _

Expected work of the actual assembly over independent finite per-bucket trace spaces; no assumption on empty/singleton bucket sizes is needed.


theorem expected_assemble_work_le {m : Nat} (sizes : Fin m → Nat) (t : Nat) :
    fintypeExpect (fun A : (j : Fin m) → Fin t → Hash (sizes j) =>
      ((assemble sizes A (List.finRange m) #[]).work : ℝ)) ≤
      (m : ℝ) + 12 * ∑ j : Fin m, (sizes j : ℝ) ^ 2 := by
  classical
  haveI (j : Fin m) : Nonempty (Fin t → Hash (sizes j)) := ⟨fun _ => fallback (sizes j)⟩
  have hex : (fun A : (j : Fin m) → Fin t → Hash (sizes j) =>
      ((assemble sizes A (List.finRange m) #[]).work : ℝ)) =
      (fun A => (m : ℝ) + ∑ j : Fin m, ((buildTrace (A j)).work : ℝ)) := by
    funext A
    rw [assemble_work]
    simp [← List.ofFn_id, List.map_ofFn, List.sum_ofFn]
  rw [hex, fintypeExpect_add, fintypeExpect_const Fintype.card_ne_zero,
    fintypeExpect_sum]
  have hmarginal (j : Fin m) :
      fintypeExpect (fun A : (j : Fin m) → Fin t → Hash (sizes j) =>
        ((buildTrace (A j)).work : ℝ)) ≤ 12 * (sizes j : ℝ) ^ 2 := by
    rw [expect_pi_apply (fun j : Fin m => Fin t → Hash (sizes j)) j
      (fun B : Fin t → Hash (sizes j) => ((buildTrace B).work : ℝ))]
    exact expected_buildTrace_work_le_all (sizes j) t
  calc
    (m : ℝ) + ∑ j : Fin m,
        fintypeExpect (fun A : (j : Fin m) → Fin t → Hash (sizes j) =>
          ((buildTrace (A j)).work : ℝ)) ≤
        (m : ℝ) + ∑ j : Fin m, 12 * (sizes j : ℝ) ^ 2 := by
      gcongr with j
      exact hmarginal j
    _ = _ := by rw [Finset.mul_sum]

Count a bucket's length by traversing its elements once.

def measureLength : List α → Nat × Nat
  | [] => (0, 0)
  | _ :: xs => let rest := measureLength xs; (rest.1 + 1, rest.2 + 1)

@[simp] theorem measureLength_result (xs : List α) : (measureLength xs).1 = xs.length := by
  induction xs <;> simp_all [measureLength]

@[simp] theorem measureLength_work (xs : List α) : (measureLength xs).2 = xs.length := by
  induction xs <;> simp_all [measureLength]

Cache bucket cardinalities once, counting both visits and cache writes.

def measureBuckets : List (List α) → Array Nat → Array Nat × Nat
  | [], out => (out, 0)
  | b :: bs, out =>
      let measured := measureLength b
      let rest := measureBuckets bs (out.push measured.1)
      (rest.1, measured.2 + 1 + rest.2)

              theorem measureBuckets_result (bs : List (List α)) (out : Array Nat) :
    (measureBuckets bs out).1.toList = out.toList ++ bs.map List.length := by
  induction bs generalizing out with
  | nil => simp [measureBuckets]
  | cons b bs ih => simp [measureBuckets, ih, List.append_assoc]theorem measureBuckets_work (bs : List (List α)) (out : Array Nat) :
    (measureBuckets bs out).2 = bs.length + bs.flatten.length := by
  induction bs generalizing out with
  | nil => simp [measureBuckets]
  | cons b bs ih => simp [measureBuckets, ih]; omegastructure Primary (n : Nat) where
  buckets : Array (List (Fin n))
  sizes : Array Nat
  work : Nat

One primary distribution and one bucket-cardinality traversal. Subsequent secondary attempts read cached sizes instead of recomputing the partition.

def preparePrimary {n : Nat} (a : Fin n → Fin n) : Primary n :=
  let initial := Chapter08.CountingExecution.initializeBuckets (α := Fin n) n
  let distributed := Chapter08.CountingExecution.distribute
    (fun i => (a i).val) (List.finRange n) initial.1
  let measured := measureBuckets distributed.buckets.toList #[]
  ⟨distributed.buckets, measured.1,
    initial.2 + 2 * distributed.inputs + 3 * distributed.updates + measured.2⟩

              @[simp] theorem preparePrimary_bucket_size {n : Nat} (a : Fin n → Fin n) :
    (preparePrimary a).buckets.size = n := by
  simp [preparePrimary]theorem preparePrimary_buckets {n : Nat} (a : Fin n → Fin n) :
    (preparePrimary a).buckets.toList =
      (List.range n).map (Chapter08.bucket (fun i => (a i).val) (List.finRange n)) := by
  simp [preparePrimary, Chapter08.CountingExecution.distribute_toList]theorem preparePrimary_sizes {n : Nat} (a : Fin n → Fin n) :
    (preparePrimary a).sizes.toList =
      (preparePrimary a).buckets.toList.map List.length := by
  simp [preparePrimary, measureBuckets_result]

@[simp] theorem preparePrimary_sizes_size {n : Nat} (a : Fin n → Fin n) :
    (preparePrimary a).sizes.size = n := by
  rw [← Array.length_toList, preparePrimary_sizes]
  simp

theorem preparePrimary_total_length {n : Nat} (a : Fin n → Fin n) :
    (preparePrimary a).buckets.toList.flatten.length = n := by
  rw [preparePrimary_buckets]
  cases n with
  | zero => simp
  | succ n =>
      change (Chapter08.countingSortBy n (fun i => (a i).val) (List.finRange (n + 1))).length = n + 1
      have hp := Chapter08.countingSortBy_perm n (fun i => (a i).val) (List.finRange (n + 1))
        (by intro i hi; change (a i).val ≤ n; have h := (a i).isLt; omega)
      simpa using hp.length_eq

theorem preparePrimary_work {n : Nat} (a : Fin n → Fin n) :
    (preparePrimary a).work = 8 * n := by
  have hu : (Chapter08.CountingExecution.distribute
      (fun i : Fin n => (a i).val) (List.finRange n) (Array.replicate n [])).updates = n := by
    simpa using Chapter08.CountingExecution.distribute_updates_eq
      (fun i : Fin n => (a i).val) (List.finRange n) (Array.replicate n [])
      (by intro i hi; simp)
  have hl := preparePrimary_total_length a
  unfold preparePrimary at hl ⊢
  simp only [Chapter08.CountingExecution.initializeBuckets_visits,
    Chapter08.CountingExecution.distribute_inputs, hu, List.length_finRange,
    measureBuckets_work, Array.length_toList, Chapter08.CountingExecution.distribute_size,
    Chapter08.CountingExecution.initializeBuckets_array, Array.size_replicate] at hl ⊢
  rw [hl]
  omega

A stored cached cardinality, not a repeated list-length computation.

def bucketCard {n : Nat} (a : Fin n → Fin n) (j : Fin n) : Nat :=
  (preparePrimary a).sizes[j.val]'(by simp)

              theorem bucketCard_eq {n : Nat} (a : Fin n → Fin n) (j : Fin n) :
    bucketCard a j = (Chapter08.bucket (fun i => (a i).val) (List.finRange n) j.val).length := by
  unfold bucketCard
  simp only [← Array.getElem_toList, preparePrimary_sizes, preparePrimary_buckets,
    List.getElem_map, List.getElem_range]

theorem bucketCard_cast {n : Nat} (a : Fin n → Fin n) (j : Fin n) :
    (bucketCard a j : ℝ) = bucketSize a j := by
  rw [bucketCard_eq, Chapter08.bucket_length_eq_card]
  exact (Chapter08.bucketOccupancy_eq_card a j).symm

theorem bucketCard_sq_sum {n : Nat} (a : Fin n → Fin n) :
    (∑ j : Fin n, (bucketCard a j : ℝ) ^ 2) = totalSecondarySpace a := by
  unfold totalSecondarySpace
  exact Finset.sum_congr rfl (fun j _ => by rw [bucketCard_cast])structure TwoLevel {n : Nat} (a : Fin n → Fin n) where
  primary : Primary n
  secondary : Assembly (bucketCard a)
  work : Nat

Construct every actual secondary array from finite supplied trial traces, retaining the primary payload buckets and all completed secondary arrays.

def buildTwoLevel {n t : Nat} (a : Fin n → Fin n)
    (A : (j : Fin n) → Fin t → Hash (bucketCard a j)) : TwoLevel a :=
  let primary := preparePrimary a
  let secondary := assemble (fun j => primary.sizes[j.val]'(by simp [primary])) A (List.finRange n) #[]
  ⟨primary, secondary, primary.work + secondary.work⟩

All secondary tables returned by the complete constructor succeeded.

theorem buildTwoLevel_success {n t : Nat} (a : Fin n → Fin n)
    (A : (j : Fin n) → Fin t → Hash (bucketCard a j)) :
    ∀ entry ∈ (buildTwoLevel a A).secondary.buckets.toList,
      entry.2.selected.success = true :=
  assemble_success (bucketCard a) A

Conditional expected measured work is bounded by the pre-existing analytic budget up to an explicit operation-count constant.


theorem expected_buildTwoLevel_work_le_budget {n : Nat} (a : Fin n → Fin n) (t : Nat) :
    fintypeExpect (fun A : (j : Fin n) → Fin t → Hash (bucketCard a j) =>
      ((buildTwoLevel a A).work : ℝ)) ≤ 9 * constructionCost a := by
  classical
  haveI (j : Fin n) : Nonempty (Fin t → Hash (bucketCard a j)) :=
    ⟨fun _ => fallback (bucketCard a j)⟩
  have he := expected_assemble_work_le (bucketCard a) t
  rw [bucketCard_sq_sum] at he
  have hex : (fun A : (j : Fin n) → Fin t → Hash (bucketCard a j) =>
      ((buildTwoLevel a A).work : ℝ)) =
      (fun A => (8 * n : ℝ) + ((assemble (bucketCard a) A (List.finRange n) #[]).work : ℝ)) := by
    funext A
    change (((preparePrimary a).work + (assemble (bucketCard a) A (List.finRange n) #[]).work : Nat) : ℝ) = _
    rw [preparePrimary_work]
    push_cast
    rfl
  rw [hex, fintypeExpect_add, fintypeExpect_const Fintype.card_ne_zero]
  have hs : 0 ≤ totalSecondarySpace a := by
    unfold totalSecondarySpace
    exact Finset.sum_nonneg (fun j _ => sq_nonneg _)
  unfold constructionCost
  nlinarith

Average actual finite-with-fallback construction work is linear under the primary SUHA assignment and the conditional independent secondary trace spaces.

theorem expected_buildTwoLevel_work_lt {n : Nat} (hn : 0 < n) (t : Nat) :
    fintypeExpect (fun a : Fin n → Fin n =>
      fintypeExpect (fun A : (j : Fin n) → Fin t → Hash (bucketCard a j) =>
        ((buildTwoLevel a A).work : ℝ))) < 45 * (n : ℝ) := by
  classical
  calc
    fintypeExpect (fun a : Fin n → Fin n =>
        fintypeExpect (fun A : (j : Fin n) → Fin t → Hash (bucketCard a j) =>
          ((buildTwoLevel a A).work : ℝ))) ≤
        fintypeExpect (fun a : Fin n → Fin n => 9 * constructionCost a) := by
      apply fintypeExpect_mono
      intro a
      exact expected_buildTwoLevel_work_le_budget a t
    _ = 9 * fintypeExpect (fun a : Fin n → Fin n => constructionCost a) :=
      fintypeExpect_const_mul 9 _
    _ < 9 * (5 * (n : ℝ)) :=
      mul_lt_mul_of_pos_left (perfectHash_expected_construction_time_le_const_n hn) (by norm_num)
    _ = _ := by ring

Each returned secondary array stores every local key index at the slot selected by the hash returned by that same execution.


theorem buildTwoLevel_stores {n t : Nat} (a : Fin n → Fin n)
    (A : (j : Fin n) → Fin t → Hash (bucketCard a j)) :
    ∀ entry ∈ (buildTwoLevel a A).secondary.buckets.toList,
      ∀ i : Fin (bucketCard a entry.1),
        entry.2.selected.slots[(entry.2.selected.hash i).val]?.join = some i := by
  change ∀ entry ∈ (assemble (bucketCard a) A (List.finRange n) #[]).buckets.toList, _
  rw [assemble_result]
  simp only [List.nil_append, List.mem_map]
  rintro entry ⟨j, hj, rfl⟩ i
  simp only [buildTrace_eq]
  change (build (List.ofFn (A j))).selected.slots[
    ((build (List.ofFn (A j))).selected.hash i).val]?.join = some i
  rw [build_selected_eq]
  simp only [attempt_hash]
  rw [Array.getElem?_eq_getElem (by simp), Option.join_some]
  exact attempt_stores _ (build_hash_injective (List.ofFn (A j))) i




theorem preparePrimary_bucket_length {n : Nat} (a : Fin n → Fin n) (j : Fin n) :
    ((preparePrimary a).buckets[j.val]'(by simp)).length = bucketCard a j := by
  rw [bucketCard_eq]
  simp only [← Array.getElem_toList, preparePrimary_buckets,
    List.getElem_map, List.getElem_range]

Resolve a supplied local index through its selected secondary slot to the original payload. Supplying the local index is an explicit interface requirement.

def recoverPayload {n : Nat} {a : Fin n → Fin n} (built : TwoLevel a)
    (entry : Σ j : Fin n, Build (bucketCard a j)) (i : Fin (bucketCard a entry.1)) :
    Option (Fin n) := do
  let localIndex ← entry.2.selected.slots[(entry.2.selected.hash i).val]?.join
  let payloads ← built.primary.buckets[entry.1.val]?
  payloads[localIndex.val]?



theorem buildTwoLevel_recovers {n t : Nat} (a : Fin n → Fin n)
    (A : (j : Fin n) → Fin t → Hash (bucketCard a j))
    (entry : Σ j : Fin n, Build (bucketCard a j))
    (he : entry ∈ (buildTwoLevel a A).secondary.buckets.toList)
    (i : Fin (bucketCard a entry.1)) :
    recoverPayload (buildTwoLevel a A) entry i =
      some (((preparePrimary a).buckets[entry.1.val]'(by simp))[i.val]'(by
        rw [preparePrimary_bucket_length]; exact i.isLt)) := by
  unfold recoverPayload
  rw [buildTwoLevel_stores a A entry he i]
  change ((preparePrimary a).buckets[entry.1.val]?.bind fun xs => xs[i.val]?) = _
  rw [Array.getElem?_eq_getElem (by simp), Option.bind_some,
    List.getElem?_eq_getElem (by rw [preparePrimary_bucket_length]; exact i.isLt)]




theorem preparePrimary_covers {n : Nat} (a : Fin n → Fin n) (x : Fin n) :
    ∃ i : Fin (bucketCard a (a x)),
      ((preparePrimary a).buckets[(a x).val]'(by simp))[i.val]'(by
        rw [preparePrimary_bucket_length]; exact i.isLt) = x := by
  have hm : x ∈ (preparePrimary a).buckets[(a x).val]'(by simp) := by
    simp only [← Array.getElem_toList, preparePrimary_buckets,
      List.getElem_map, List.getElem_range]
    simp [CLRS.Chapter08.bucket]
  obtain ⟨i, hi, hx⟩ := List.getElem_of_mem hm
  exact ⟨⟨i, by rwa [preparePrimary_bucket_length] at hi⟩, hx⟩

Every original stored payload can be recovered through its actual returned secondary table, given its local index. This does not construct an inverse map from arbitrary original query keys to local indices.


theorem buildTwoLevel_recovers_original {n t : Nat} (a : Fin n → Fin n)
    (A : (j : Fin n) → Fin t → Hash (bucketCard a j)) (x : Fin n) :
    ∃ i : Fin (bucketCard a (a x)),
      recoverPayload (buildTwoLevel a A) ⟨a x, buildTrace (A (a x))⟩ i = some x := by
  obtain ⟨i, hi⟩ := preparePrimary_covers a x
  refine ⟨i, ?_⟩
  rw [buildTwoLevel_recovers, hi]
  change (⟨a x, buildTrace (A (a x))⟩ : Σ j : Fin n, Build (bucketCard a j)) ∈
    (assemble (bucketCard a) A (List.finRange n) #[]).buckets.toList
  rw [assemble_result]
  simp only [List.nil_append, List.mem_map]
  exact ⟨a x, List.mem_finRange _, rfl⟩

end CLRS.Chapter11.PerfectConstruction

Scope and implementation notes

Imports

import CLRSLean.FourthEdition.Chapter_11.Section_11_5_Perfect_Hashing.Construction
import CLRSLean.FourthEdition.Chapter_11.Section_11_1_Direct_Address_Tables
import CLRSLean.FourthEdition.Chapter_11.Section_11_2_Chained_Hash_Tables
import CLRSLean.FourthEdition.Chapter_11.Section_11_3_Hash_Functions
import CLRSLean.FourthEdition.Chapter_11.Section_11_4_Open_Addressing
import CLRSLean.FourthEdition.Chapter_11.Section_11_4_Open_Addressing.UniformProbe
import CLRSLean.FourthEdition.Chapter_11.Section_11_5_Perfect_Hashing

Native fourth-edition chapter guide.

Current source

This guide sources fourth-edition §11.1–§11.5 from the native section modules under CLRSLean.FourthEdition.Chapter_11. Declarations retain the CLRS.Chapter11 namespace; the legacy import CLRSLean.Chapter_11 and its Section_11_* modules forward to these sources during the compatibility period.

Chapter 11 introduces direct-address tables and hash tables. The current CLRS-Lean pass separates deterministic table correctness from probabilistic performance analysis. Section 11.2 now includes a finite-uniform bucket interface: when the searched bucket is uniformly distributed, expected chain length is exactly the load factor, and one insertion increases load factor and unsuccessful-search cost by 1/m.

Sections

11.1 Direct-address tables: proved for the functional table model. Main results: CLRS.Chapter11.search_insert_same, CLRS.Chapter11.search_insert_other, CLRS.Chapter11.search_delete_same.
11.2 Hash tables: proved for the advertised functional and finite probability models. Main results: CLRS.Chapter11.bucket_hashInsert_same, CLRS.Chapter11.hashSearch_hashInsert_self, CLRS.Chapter11.hashSearch_hashInsert_iff, CLRS.Chapter11.hashSearch_hashDelete_self, CLRS.Chapter11.hashSearch_hashDelete_iff, CLRS.Chapter11.uniformAverageFin_indicator_singleton, CLRS.Chapter11.uniformAverageFin_add, CLRS.Chapter11.uniformAverageFin_nonneg, CLRS.Chapter11.finiteHashLoadFactor_nonneg, CLRS.Chapter11.expectedSearchChainLength_eq_loadFactor, CLRS.Chapter11.expectedSearchChainLength_nonneg, CLRS.Chapter11.expectedUnsuccessfulSearchCost_eq_one_plus_loadFactor, CLRS.Chapter11.expectedUnsuccessfulSearchCost_ge_one, CLRS.Chapter11.expectedSearchChainLength_finiteHashInsert, CLRS.Chapter11.finiteHashLoadFactor_finiteHashInsert, CLRS.Chapter11.expectedUnsuccessfulSearchCost_finiteHashInsert, CLRS.Chapter11.expectedRandomChainLength_eq_loadFactor, CLRS.Chapter11.expectedRandomUnsuccessfulSearchCost, CLRS.Chapter11.pairCollisionProb, CLRS.Chapter11.expectedRandomSuccessfulSearchCost, CLRS.Chapter11.universal_expected_collisions, and CLRS.Chapter11.universal_expected_search_cost.
11.3 Hash functions: proved. Main results: CLRS.Chapter11.divisionHash_lt, CLRS.Chapter11.multiplicationHash_lt, CLRS.Chapter11.affineHash_isUniversal, CLRS.Chapter11.affineHash_expected_collisions, CLRS.Chapter11.affineHash_expected_search_cost, and CLRS.Chapter11.affineHashMod_isUniversal (CLRS Theorem 11.5, the general mod-m affine family).
11.4 Open addressing: proved. Main results: CLRS.Chapter11.openSearch_openInsert, CLRS.Chapter11.openSearch_eq_false_of_absent, CLRS.Chapter11.linearProbe_bijective, CLRS.Chapter11.doubleHashProbe_bijective, CLRS.Chapter11.firstProbesOccupied_card, CLRS.Chapter11.uniformProbeTailProbability_eq_probeTail, CLRS.Chapter11.uniformUnsuccessfulExpectedProbes_eq, CLRS.Chapter11.uniformUnsuccessfulExpectedProbes_le, CLRS.Chapter11.expectedUnsuccessfulProbes_le, CLRS.Chapter11.expectedSuccessfulProbes_le, and CLRS.Chapter11.expectedSuccessfulProbes_le_ln (CLRS Theorem 11.8, logarithmic form).
11.5 Perfect hashing: proved. Main results: CLRS.Chapter11.perfectSearch_iff_mem, CLRS.Chapter11.perfectHash_collision_free_prob_ge_half, CLRS.Chapter11.perfectHash_expected_total_space_lt_2n, and the PerfectConstruction companion's successful finite-trial array construction and expected executed-work bounds.

Current Gaps

The deterministic insert/delete/search layer is compiler-clean, and the finite-uniform bucket layer proves the load-factor, nonnegativity, and single-insert expected-cost interfaces. The SUHA layer proves the expected chain length, unsuccessful-search cost 1 + α, and successful-search cost 1 + (n-1)/(2m) as true expectations, and a universal random-hash-function family bounds expected collisions by α and search cost by 1 + α. Section 11.3 supplies a concrete universal family (the prime-field affine family h_{a,b}(k) = a * k + b) that discharges the IsUniversal hypothesis, so the universal-hashing bounds are no longer conditional. Section 11.4 formalises the open addressing model with probe sequences (linear, quadratic, double hashing). Its uniform-hashing assumption is now realized by the finite sample space Equiv.Perm (Fin m): every injective prefix has exactly (m-i)! full-permutation extensions, the occupied-prefix probability is proved equal to the without-replacement product probeTail, and the expected concrete probe count is proved equal to the chapter's tail sum. This gives explicit-sample-space versions of the expected-probe bounds: unsuccessful search and insertion ≤ 1/(1-α) (CLRS Theorems 11.6-11.7) and successful search (1/α) · ∑_{j<n} 1/(m-j) (CLRS Theorem 11.8 harmonic form), refined to the closed form (1/α) · ln(1/(1-α)) (CLRS.Chapter11.uniformSuccessfulExpectedProbes_le_ln). Section 11.5 formalises the two-level perfect-hashing scheme: a primary hash into m = n buckets plus per-bucket secondary tables of size n_j², which are collision-free with probability ≥ 1/2 (Theorem 11.9) and collectively use expected O(n) space (Theorem 11.10). Secondary injectivity is required only for stored keys in their primary bucket, allowing unstored keys to collide.

The PerfectConstruction companion builds primary payload buckets and secondary arrays, trying supplied random local-index hashes before a guaranteed injective fallback. Actual attempts agree with the finite trial-count model. Counted collision checks, initialization, placement, and assembly have conditional expectation at most 9 * constructionCost, and nested uniform expectation below 45n for positive n. The older theorem named perfectHash_expected_construction_time_le_const_n bounds the abstract budget itself by 5n; it is not the executed counter.

This SUHA construction samples functions on local bucket indices. Conversion from arbitrary original-key queries to constant-time hash programs, hash-code generation, persistent allocation, and machine arithmetic are not established by these execution bounds.

See docs/clrs-fourth-edition-map.csv for the section-level mapping and docs/migrations/clrs4.md for compatibility and deprecation policy.

CLRS, fourth edition · Chapter 11 of 35

11.1. Direct-Address Tables

Direct-address table model

Operation correctness

11.2. Chained Hash Tables

Chained table model

Deterministic correctness

Finite-uniform hashing interface

Expected search cost as a true expectation (SUHA)

Successful search as a true expectation (SUHA)

Random hash-function model (universal hashing)

Definitions and proofs

CLRSLean.Probability.FiniteExpectation

11.3. Hash Functions

Deterministic hashing heuristics (CLRS §11.3.1-11.3.2)

A concrete universal family (CLRS Theorem 11.5)

The general mod-m affine family (CLRS Theorem 11.5, full form)

11.4. Open Addressing

Functional open-addressing model

Model correctness (CLRS §11.4 insert/search behaviour)

Probe schemes (CLRS §11.4, equations (11.5)-(11.7))

Expected number of probes under uniform hashing (CLRS Theorems 11.6-11.8)

Definitions and proofs

CLRSLean.FourthEdition.Chapter_11.Section_11_4_Open_Addressing.UniformProbe.Counting

CLRS Section 11.4 - Counting uniform probe prefixes

CLRSLean.FourthEdition.Chapter_11.Section_11_4_Open_Addressing.UniformProbe.Definitions

CLRS Section 11.4 - Uniform probe-space definitions

CLRSLean.FourthEdition.Chapter_11.Section_11_4_Open_Addressing.UniformProbe.Probability

CLRS Section 11.4 - Uniform permutation probabilities

11.5. Perfect Hashing

Two-level perfect hash model

Theorem 11.9: secondary collision-free with probability at least 1/2

Theorem 11.10: expected total space O(n)

Construction trials: expected trials to a collision-free secondary hash

Abstract construction budget and its finite expectation

Definitions and proofs

CLRSLean.FourthEdition.Chapter_11.Section_11_5_Perfect_Hashing.Construction.Secondary

Executed finite secondary perfect-hash construction

CLRSLean.FourthEdition.Chapter_11.Section_11_5_Perfect_Hashing.Construction.TwoLevel

Measured assembly of all secondary tables

Scope and implementation notes

Current source

Sections

Current Gaps

The general mod-`m` affine family (CLRS Theorem 11.5, full form)