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