CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 5. Probabilistic Analysis and Randomized Algorithms
5.3. Randomized algorithms

Imports

import CLRSLean.FourthEdition.Chapter_05.Section_05_3_Randomized_Algorithms.FisherYates.Uniformity

5.3. Randomized algorithms

This public wrapper proves CLRS Lemma 5.4 for a constructive Fisher–Yates execution. The implementation is split into small modules for its dependent choice-vector decomposition, executable placement recursion, loop invariant, and finite uniformity proof.

Main results:

Theorem fisherYates_succ_invariant: the selected element occupies the current position and the recursive suffix is relabelled by exactly one swap.
Theorem fisherYates_first_uniform: the current placement is uniform over all currently available positions, and the statement recurses on the suffix.
Theorem fisherYates_uniform / randomizeInPlace_uniform (Lemma 5.4): every output permutation has probability 1/n!.

Status: proved for the explicit independent-swap-choice model. Current gaps: none.

              namespace CLRSnamespace Chapter05open CLRS.Probability

The public RANDOMIZE-IN-PLACE equivalence is now the constructive Fisher–Yates equivalence.

def randomizeInPlace_equiv (n : Nat) : ChoiceVector n ≃ Equiv.Perm (Fin n) :=
  fisherYatesEquiv n

RANDOMIZE-IN-PLACE (Fisher–Yates shuffle). Given a choice vector c, produce the permutation of Fin n obtained by the Fisher–Yates process.

def randomizeInPlace {n : Nat} (choices : ChoiceVector n) : Equiv.Perm (Fin n) :=
  fisherYates choices

Compatibility is pointwise, not merely distributional.

theorem randomizeInPlace_eq_fisherYates {n : Nat} (choices : ChoiceVector n) :
    randomizeInPlace choices = fisherYates choices := rfl

Lemma 5.4 (Uniform random permutation). Under the uniform distribution on ChoiceVector n, the permutation produced by RANDOMIZE-IN-PLACE is uniformly distributed over Equiv.Perm (Fin n). Equivalently, for every permutation σ, the probability that randomizeInPlace(c) = σ equals 1/n!.

theorem randomizeInPlace_uniform (n : Nat) (sigma : Equiv.Perm (Fin n)) :
    fintypeExpect (fun choices : ChoiceVector n =>
      indicator (randomizeInPlace choices = sigma)) =
      1 / (Fintype.card (Equiv.Perm (Fin n)) : Real) := by
  calc
    fintypeExpect (fun choices : ChoiceVector n =>
        indicator (randomizeInPlace choices = sigma)) =
        fintypeExpect (fun perm : Equiv.Perm (Fin n) => indicator (perm = sigma)) :=
      fintypeExpect_equiv (randomizeInPlace_equiv n)
        (fun perm : Equiv.Perm (Fin n) => indicator (perm = sigma))
    _ = 1 / (Fintype.card (Equiv.Perm (Fin n)) : Real) :=
      fintypeExpect_indicator_singleton sigma

end Chapter05end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_05.Section_05_3_Randomized_Algorithms.ChoiceVector

5.3. Fisher–Yates choice vectors

The choice at position i is an offset in Fin (n - i), hence selects one of the positions i, ..., n - 1. The product sample space has cardinality n!.

namespace CLRSnamespace Chapter05

Independent finite choices used by forward Fisher–Yates.

def ChoiceVector (n : Nat) : Type := (i : Fin n) -> Fin (n - i.val)

instance (n : Nat) : Fintype (ChoiceVector n) :=
  inferInstanceAs (Fintype ((i : Fin n) -> Fin (n - i.val)))

instance (n : Nat) : DecidableEq (ChoiceVector n) :=
  inferInstanceAs (DecidableEq ((i : Fin n) -> Fin (n - i.val)))

The cardinality of ChoiceVector n is n!.


theorem card_choiceVector (n : Nat) :
    Fintype.card (ChoiceVector n) = (Nat.factorial n : Nat) := by
  induction' n with n ih
  · simp [ChoiceVector]
  · calc
    Fintype.card (ChoiceVector (n + 1)) =
        Fintype.card (forall i : Fin (n + 1), Fin ((n + 1) - i.val)) := rfl
    _ = ∏ i : Fin (n + 1), Fintype.card (Fin ((n + 1) - i.val)) := by
      simp [Fintype.card_pi]
    _ = Fintype.card (Fin ((n + 1) - ((0 : Fin (n + 1)).val))) *
        (∏ i : Fin n, Fintype.card (Fin ((n + 1) - (Fin.succ i).val))) := by
      simp [Fin.prod_univ_succ]
    _ = (n + 1 : Nat) * (∏ i : Fin n, Fintype.card (Fin (n - i.val))) := by
      simp [Fintype.card_fin]
    _ = (n + 1) * Fintype.card (forall i : Fin n, Fin (n - i.val)) := by
      simp [Fintype.card_pi]
    _ = (n + 1) * Fintype.card (ChoiceVector n) := rfl
    _ = (n + 1) * (Nat.factorial n : Nat) := by rw [ih]
    _ = (Nat.factorial (n + 1) : Nat) := by
      simp [Nat.factorial_succ, mul_comm]

Choices that always select the current position.

def zeroChoiceVector (n : Nat) : ChoiceVector n :=
  fun i => ⟨0, by omega⟩

Choices that always select the last remaining position.

def lastChoiceVector (n : Nat) : ChoiceVector n :=
  fun i => ⟨n - i.val - 1, by omega⟩

end Chapter05end CLRS

CLRSLean.FourthEdition.Chapter_05.Section_05_3_Randomized_Algorithms.FisherYates.ChoiceVectorSplit

Splitting the first Fisher–Yates choice

This module isolates the dependent-type bookkeeping that splits a choice vector of length n + 1 into its first choice and the choices for the remaining suffix.

namespace CLRSnamespace Chapter05

Reindex the tail family after removing position zero.

private def choiceVectorTailEquiv (n : Nat) :
    ((i : Fin n) -> Fin ((n + 1) - (Fin.succ i).val)) ≃ ChoiceVector n :=
  Equiv.piCongrRight (fun i => Equiv.cast (congrArg Fin (by simp [Fin.val_succ])))

A length-n+1 choice vector is a first choice in Fin (n+1) followed by a length-n choice vector for the suffix.

def choiceVectorSuccEquiv (n : Nat) :
    ChoiceVector (n + 1) ≃ Fin (n + 1) × ChoiceVector n :=
  (Fin.consEquiv (fun i : Fin (n + 1) => Fin ((n + 1) - i.val))).symm |>.trans
    (Equiv.prodCongr
      (Equiv.cast (congrArg Fin (by simp)))
      (choiceVectorTailEquiv n))

              @[simp] theorem choiceVectorSuccEquiv_fst (n : Nat) (choices : ChoiceVector (n + 1)) :
    (choiceVectorSuccEquiv n choices).1 = choices 0 := rflend Chapter05end CLRS

CLRSLean.FourthEdition.Chapter_05.Section_05_3_Randomized_Algorithms.FisherYates.Execution

Executable Fisher–Yates

The recursion places the first selected rank and continues on the remaining suffix. Equiv.Perm.decomposeFin.symm is constructive; its equations say exactly that position zero is swapped with the selected position and that the recursive permutation acts only on the suffix.

namespace CLRSnamespace Chapter05

One constructive placement step: put selected at the current position and relabel the recursively permuted suffix by the corresponding swap.

def fisherYatesStep {n : Nat} (selected : Fin (n + 1))
    (suffix : Equiv.Perm (Fin n)) : Equiv.Perm (Fin (n + 1)) :=
  Equiv.Perm.decomposeFin.symm (selected, suffix)

@[simp] theorem fisherYatesStep_zero {n : Nat} (selected : Fin (n + 1))
    (suffix : Equiv.Perm (Fin n)) :
    fisherYatesStep selected suffix 0 = selected := by
  exact Equiv.Perm.decomposeFin_symm_apply_zero selected suffix

@[simp] theorem fisherYatesStep_succ {n : Nat} (selected : Fin (n + 1))
    (suffix : Equiv.Perm (Fin n)) (i : Fin n) :
    fisherYatesStep selected suffix i.succ =
      Equiv.swap 0 selected (suffix i).succ := by
  exact Equiv.Perm.decomposeFin_symm_apply_succ suffix selected i

The executable Fisher–Yates map, packaged as a bijection from choice vectors to permutations.

def fisherYatesEquiv : (n : Nat) -> ChoiceVector n ≃ Equiv.Perm (Fin n)
  | 0 =>
      { toFun := fun _ => 1
        invFun := fun _ i => Fin.elim0 i
        left_inv := fun _ => funext fun i => Fin.elim0 i
        right_inv := fun _ => Equiv.ext fun i => Fin.elim0 i }
  | n + 1 =>
      (choiceVectorSuccEquiv n).trans <|
        (Equiv.prodCongr (Equiv.refl _) (fisherYatesEquiv n)).trans
          Equiv.Perm.decomposeFin.symm

Run Fisher–Yates using the supplied finite choice vector.

def fisherYates {n : Nat} (choices : ChoiceVector n) : Equiv.Perm (Fin n) :=
  fisherYatesEquiv n choices

              @[simp] theorem fisherYates_zero (choices : ChoiceVector 0) :
    fisherYates choices = 1 := by
  ext i
  exact Fin.elim0 i@[simp] theorem fisherYates_succ_zero (n : Nat) (choices : ChoiceVector (n + 1)) :
    fisherYates choices 0 = (choiceVectorSuccEquiv n choices).1 := by
  change fisherYatesStep (choiceVectorSuccEquiv n choices).1
    (fisherYatesEquiv n (choiceVectorSuccEquiv n choices).2) 0 = _
  exact fisherYatesStep_zero _ _@[simp] theorem fisherYates_succ_succ (n : Nat) (choices : ChoiceVector (n + 1))
    (i : Fin n) :
    fisherYates choices i.succ =
      Equiv.swap 0 (choiceVectorSuccEquiv n choices).1
        (fisherYates (choiceVectorSuccEquiv n choices).2 i).succ := by
  change fisherYatesStep (choiceVectorSuccEquiv n choices).1
    (fisherYatesEquiv n (choiceVectorSuccEquiv n choices).2) i.succ = _
  exact fisherYatesStep_succ _ _ _

Textbook loop invariant, recursive form. After the current placement, the selected element occupies the current position; every suffix position is obtained by recursively permuting the suffix and relabelling by precisely that one swap. Applying this theorem recursively gives the invariant at every prefix/suffix boundary.

theorem fisherYates_succ_invariant (n : Nat) (choices : ChoiceVector (n + 1)) :
    fisherYates choices 0 = (choiceVectorSuccEquiv n choices).1 ∧
      forall i : Fin n,
        fisherYates choices i.succ =
          Equiv.swap 0 (choiceVectorSuccEquiv n choices).1
            (fisherYates (choiceVectorSuccEquiv n choices).2 i).succ := by
  exact ⟨fisherYates_succ_zero n choices, fisherYates_succ_succ n choices⟩

Every placement step preserves the multiset of positions.

theorem fisherYatesStep_map_finRange_perm {n : Nat} (selected : Fin (n + 1))
    (suffix : Equiv.Perm (Fin n)) :
    ((List.finRange (n + 1)).map (fisherYatesStep selected suffix)).Perm
      (List.finRange (n + 1)) :=
  Equiv.Perm.map_finRange_perm _

The completed executable output is a permutation of all positions.

theorem fisherYates_map_finRange_perm {n : Nat} (choices : ChoiceVector n) :
    ((List.finRange n).map (fisherYates choices)).Perm (List.finRange n) :=
  Equiv.Perm.map_finRange_perm _

end Chapter05end CLRS

CLRSLean.FourthEdition.Chapter_05.Section_05_3_Randomized_Algorithms.FisherYates.Uniformity

Uniformity of executable Fisher–Yates

Because fisherYatesEquiv is a bijection between the n! choice vectors and the n! permutations, uniform independent choices produce every permutation with probability exactly 1 / n!.

              namespace CLRSnamespace Chapter05open CLRS.Probability

The first choice made by executable Fisher–Yates is uniform over the currently available positions. The same theorem applies recursively to every remaining suffix.


theorem fisherYates_first_uniform (n : Nat) (selected : Fin (n + 1)) :
    fintypeExpect (fun choices : ChoiceVector (n + 1) =>
      indicator (fisherYates choices 0 = selected)) =
      1 / (n + 1 : Real) := by
  have hcard : Fintype.card (ChoiceVector n) ≠ 0 := by
    rw [card_choiceVector]
    exact Nat.factorial_ne_zero n
  calc
    fintypeExpect (fun choices : ChoiceVector (n + 1) =>
        indicator (fisherYates choices 0 = selected)) =
        fintypeExpect (fun choices : ChoiceVector (n + 1) =>
          indicator ((choiceVectorSuccEquiv n choices).1 = selected)) := by
      congr 1
      funext choices
      rw [fisherYates_succ_zero]
    _ = fintypeExpect (fun pair : Fin (n + 1) × ChoiceVector n =>
          indicator (pair.1 = selected)) :=
      fintypeExpect_equiv (choiceVectorSuccEquiv n)
        (fun pair : Fin (n + 1) × ChoiceVector n => indicator (pair.1 = selected))
    _ = fintypeExpect (fun i : Fin (n + 1) => indicator (i = selected)) :=
      fintypeExpect_fst hcard (fun i : Fin (n + 1) => indicator (i = selected))
    _ = 1 / (Fintype.card (Fin (n + 1)) : Real) :=
      fintypeExpect_indicator_singleton selected
    _ = 1 / (n + 1 : Real) := by simp

Fisher–Yates uniformity (CLRS Lemma 5.4).

theorem fisherYates_uniform (n : Nat) (sigma : Equiv.Perm (Fin n)) :
    fintypeExpect (fun choices : ChoiceVector n => indicator (fisherYates choices = sigma)) =
      1 / (Fintype.card (Equiv.Perm (Fin n)) : Real) := by
  calc
    fintypeExpect (fun choices : ChoiceVector n => indicator (fisherYates choices = sigma)) =
        fintypeExpect (fun perm : Equiv.Perm (Fin n) => indicator (perm = sigma)) :=
      fintypeExpect_equiv (fisherYatesEquiv n)
        (fun perm : Equiv.Perm (Fin n) => indicator (perm = sigma))
    _ = 1 / (Fintype.card (Equiv.Perm (Fin n)) : Real) :=
      fintypeExpect_indicator_singleton sigma

end Chapter05end CLRS

CLRSLean.FourthEdition.Chapter_05.Section_05_3_Randomized_Hiring

5.3. RANDOMIZED-HIRE-ASSISTANT

This file joins the executable hireAssistant loop to the uniform randomization interface from Section 5.3. It also packages the textbook expected hiring-cost calculation without conflating two distinct facts:

randomization transports the execution expectation to the uniform permutation space;
the rank-symmetry calculation identifies the latter with expectedHires.

The second fact has the named interface HiringExpectationBridge; the small companion modules under Randomized_Hiring/ prove it from prefix-record indicators and finite permutation symmetry.

              namespace CLRSnamespace Chapter05open Filteropen CLRS.Probability

Read a permutation as the list of candidate ranks in interview order.

def permutationRanks {n : Nat} (sigma : Equiv.Perm (Fin n)) : List Nat :=
  (List.finRange n).map (fun i => (sigma i : Nat))

RANDOMIZED-HIRE-ASSISTANT. Randomize the interview order, then run the executable hiring loop on the resulting rank list.

noncomputable def randomizedHireAssistant {n : Nat} (choices : ChoiceVector n) : Nat :=
  hireAssistant (permutationRanks (randomizeInPlace choices))

Expected hiring cost in the finite rank-symmetry analysis.

noncomputable def expectedHiringCost (hireCost : Real) (n : Nat) : Real :=
  hireCost * expectedHires n

The expected hiring cost is the hiring-cost constant times the harmonic number.


theorem expectedHiringCost_eq_harmonic (hireCost : Real) (n : Nat) :
    expectedHiringCost hireCost n = hireCost * harmonic n := by
  rw [expectedHiringCost, expectedHires_eq_harmonic]

Scaling the expected number of hires by a fixed nonnegative hiring cost preserves its logarithmic upper bound.

theorem expectedHiringCost_isBigO_log (hireCost : Real) (_hcost : 0 <= hireCost) :
    Chapter03.isBigO (expectedHiringCost hireCost)
      (fun n : Nat => Real.log (n : Real)) := by
  unfold expectedHiringCost Chapter03.isBigO
  exact expectedHires_isBigTheta_log.1.const_mul_left hireCost

Expected number of hires after running the randomized executable.

noncomputable def randomizedExpectedHires (n : Nat) : Real :=
  fintypeExpect (fun choices : ChoiceVector n => (randomizedHireAssistant choices : Real))

Expected number of hires when the permutation itself is sampled uniformly.

noncomputable def uniformPermutationExpectedHires (n : Nat) : Real :=
  fintypeExpect (fun sigma : Equiv.Perm (Fin n) =>
    (hireAssistant (permutationRanks sigma) : Real))

Uniform randomization transports the executable hire count exactly to the uniform-permutation sample space.

theorem randomizedExpectedHires_eq_uniform (n : Nat) :
    randomizedExpectedHires n = uniformPermutationExpectedHires n := by
  unfold randomizedExpectedHires uniformPermutationExpectedHires
  change fintypeExpect (fun choices : ChoiceVector n =>
      (hireAssistant (permutationRanks (fisherYates choices)) : Real)) = _
  exact fintypeExpect_equiv (fisherYatesEquiv n)
    (fun sigma : Equiv.Perm (Fin n) =>
      (hireAssistant (permutationRanks sigma) : Real))

The actual expected cost of the randomized executable.

noncomputable def randomizedExpectedHiringCost (hireCost : Real) (n : Nat) : Real :=
  fintypeExpect (fun choices : ChoiceVector n =>
    hireCost * (randomizedHireAssistant choices : Real))

Expected cost over a directly sampled uniform permutation.

noncomputable def uniformPermutationExpectedHiringCost (hireCost : Real) (n : Nat) : Real :=
  fintypeExpect (fun sigma : Equiv.Perm (Fin n) =>
    hireCost * (hireAssistant (permutationRanks sigma) : Real))

Randomization transports the expected execution cost exactly to the uniform-permutation model.

theorem randomizedExpectedHiringCost_eq_uniform (hireCost : Real) (n : Nat) :
    randomizedExpectedHiringCost hireCost n =
      uniformPermutationExpectedHiringCost hireCost n := by
  unfold randomizedExpectedHiringCost uniformPermutationExpectedHiringCost
  change fintypeExpect (fun choices : ChoiceVector n =>
      hireCost * (hireAssistant (permutationRanks (fisherYates choices)) : Real)) = _
  exact fintypeExpect_equiv (fisherYatesEquiv n)
    (fun sigma : Equiv.Perm (Fin n) =>
      hireCost * (hireAssistant (permutationRanks sigma) : Real))

The remaining textbook bridge: the expectation of the executable record counter over uniform permutations agrees with the rank-symmetry recurrence.

def HiringExpectationBridge : Prop :=
  forall n, uniformPermutationExpectedHires n = expectedHires n

Compatibility wrapper: under an explicitly supplied execution-to-analysis bridge, the randomized executable has the analytic expected hiring cost. The companion ExpectationBridge module proves the bridge and exposes a premise-free theorem under the original public name.


theorem randomizedExpectedHiringCost_eq_of_bridge (hbridge : HiringExpectationBridge)
    (hireCost : Real) (n : Nat) :
    randomizedExpectedHiringCost hireCost n = expectedHiringCost hireCost n := by
  rw [randomizedExpectedHiringCost_eq_uniform]
  unfold uniformPermutationExpectedHiringCost expectedHiringCost
  unfold fintypeExpect
  have hb := hbridge n
  unfold uniformPermutationExpectedHires fintypeExpect at hb
  calc
    (Finset.univ.sum fun sigma : Equiv.Perm (Fin n) =>
        hireCost * (hireAssistant (permutationRanks sigma) : Real)) /
        (Fintype.card (Equiv.Perm (Fin n)) : Real) =
      (hireCost * (Finset.univ.sum fun sigma : Equiv.Perm (Fin n) =>
        (hireAssistant (permutationRanks sigma) : Real))) /
        (Fintype.card (Equiv.Perm (Fin n)) : Real) := by
          rw [Finset.mul_sum]
    _ = hireCost *
        ((Finset.univ.sum fun sigma : Equiv.Perm (Fin n) =>
          (hireAssistant (permutationRanks sigma) : Real)) /
            (Fintype.card (Equiv.Perm (Fin n)) : Real)) := by ring
    _ = hireCost * expectedHires n := by rw [hb]

Compatibility wrapper for the logarithmic bound with an explicitly supplied bridge.


theorem randomizedExpectedHiringCost_isBigO_log_of_bridge
    (hbridge : HiringExpectationBridge) (hireCost : Real) (hcost : 0 <= hireCost) :
    Chapter03.isBigO (randomizedExpectedHiringCost hireCost)
      (fun n : Nat => Real.log (n : Real)) := by
  have heq : randomizedExpectedHiringCost hireCost = expectedHiringCost hireCost := by
    funext n
    exact randomizedExpectedHiringCost_eq_of_bridge hbridge hireCost n
  rw [heq]
  exact expectedHiringCost_isBigO_log hireCost hcost

end Chapter05end CLRS

CLRSLean.FourthEdition.Chapter_05.Section_05_3_Randomized_Hiring.ExpectationBridge

Expected record count of RANDOMIZED-HIRE-ASSISTANT

The executable counter is first rewritten as a finite sum of prefix-record indicators. Finite linearity of expectation and the 1/(i+1) record probability then give the harmonic sum. No independence between record events is assumed or needed.

              namespace CLRSnamespace Chapter05open CLRS.Probability

Casting the executable hire count gives the real-valued sum of its record indicators.


theorem hireAssistant_permutationRanks_cast {n : Nat}
    (sigma : Equiv.Perm (Fin n)) :
    (hireAssistant (permutationRanks sigma) : Real) =
      ∑ i : Fin n, indicator (permutationPrefixRecordAt sigma i) := by
  rw [hireAssistant_permutationRanks_eq_sum]
  push_cast
  apply Finset.sum_congr rfl
  intro i _
  by_cases hrecord : permutationPrefixRecordAt sigma i
  · simp [CLRS.Chapter05.indicator, CLRS.Probability.indicator, hrecord]
  · simp [CLRS.Chapter05.indicator, CLRS.Probability.indicator, hrecord]

The executable record counter over uniform permutations has harmonic expectation.


theorem uniformPermutationExpectedHires_eq_harmonic (n : Nat) :
    uniformPermutationExpectedHires n = harmonic n := by
  unfold uniformPermutationExpectedHires
  rw [show (fun sigma : Equiv.Perm (Fin n) =>
      (hireAssistant (permutationRanks sigma) : Real)) =
      (fun sigma : Equiv.Perm (Fin n) =>
        ∑ i : Fin n, indicator (permutationPrefixRecordAt sigma i)) by
    funext sigma
    exact hireAssistant_permutationRanks_cast sigma]
  calc
    fintypeExpect (fun sigma : Equiv.Perm (Fin n) =>
        ∑ i : Fin n, indicator (permutationPrefixRecordAt sigma i)) =
        ∑ i : Fin n, fintypeExpect (fun sigma : Equiv.Perm (Fin n) =>
          indicator (permutationPrefixRecordAt sigma i)) := by
      simpa using fintypeExpect_sum (Finset.univ : Finset (Fin n))
        (fun (i : Fin n) (sigma : Equiv.Perm (Fin n)) =>
          indicator (permutationPrefixRecordAt sigma i))
    _ = ∑ i : Fin n, 1 / ((i.val + 1 : Nat) : Real) := by
      apply Finset.sum_congr rfl
      intro i _
      exact prefixRecord_probability i
    _ = harmonic n := by
      rw [Fin.sum_univ_eq_sum_range
        (fun i : Nat => 1 / ((i + 1 : Nat) : Real)) n]
      simp [harmonic]

The former open bridge is now inhabited by the finite permutation proof.


theorem hiringExpectationBridge : HiringExpectationBridge := by
  intro n
  rw [uniformPermutationExpectedHires_eq_harmonic,
    expectedHires_eq_harmonic]

The expected number of hires of the randomized executable is exactly the textbook recurrence value.


theorem randomizedExpectedHires_eq (n : Nat) :
    randomizedExpectedHires n = expectedHires n := by
  rw [randomizedExpectedHires_eq_uniform]
  exact hiringExpectationBridge n

The randomized executable has exactly the analytic expected hiring cost, with no bridge premise.

theorem randomizedExpectedHiringCost_eq (hireCost : Real) (n : Nat) :
    randomizedExpectedHiringCost hireCost n = expectedHiringCost hireCost n :=
  randomizedExpectedHiringCost_eq_of_bridge hiringExpectationBridge hireCost n

RANDOMIZED-HIRE-ASSISTANT has logarithmic expected hiring cost.

theorem randomizedExpectedHiringCost_isBigO_log
    (hireCost : Real) (hcost : 0 <= hireCost) :
    Chapter03.isBigO (randomizedExpectedHiringCost hireCost)
      (fun n : Nat => Real.log (n : Real)) :=
  randomizedExpectedHiringCost_isBigO_log_of_bridge
    hiringExpectationBridge hireCost hcost

end Chapter05end CLRS

CLRSLean.FourthEdition.Chapter_05.Section_05_3_Randomized_Hiring.RecordIndicators

Executable hiring as a sum of prefix-record indicators

This file is the operational half of the hiring expectation bridge. It is kept separate from the finite permutation counting argument so changes to the list execution do not force recompilation of the probability proof.

namespace CLRSnamespace Chapter05

Position i of xs is a strict record relative to the earlier prefix and an initial best rank.

def recordAfter (best : Nat) (xs : List Nat) (i : Fin xs.length) : Prop :=
  best < xs[i.val] ∧ ∀ x ∈ xs.take i.val, x < xs[i.val]

instance recordAfter_decidable (best : Nat) (xs : List Nat) (i : Fin xs.length) :
    Decidable (recordAfter best xs i) := by
  unfold recordAfter
  infer_instance

Executable natural-valued indicator of recordAfter.

def recordAfterBit (best : Nat) (xs : List Nat) (i : Fin xs.length) : Nat :=
  if recordAfter best xs i then 1 else 0

Adding a head to the scanned list turns tail records into records relative to the maximum of the previous best and that head.

theorem recordAfter_cons_succ_iff (best r : Nat) (rest : List Nat)
    (i : Fin rest.length) :
    recordAfter best (r :: rest) i.succ ↔ recordAfter (max best r) rest i := by
  simp only [recordAfter, List.getElem_cons_succ, Fin.val_succ, List.take_succ_cons,
    List.mem_cons]
  constructor
  · rintro ⟨hbest, hall⟩
    refine ⟨?_, ?_⟩
    · have hr := hall r (Or.inl rfl)
      omega
    · intro x hx
      exact hall x (Or.inr hx)
  · rintro ⟨hmax, hall⟩
    refine ⟨by omega, ?_⟩
    intro x hx
    rcases hx with rfl | hx
    · omega
    · exact hall x hx

The head position is a record exactly when it improves the initial best.

theorem recordAfter_cons_zero_iff (best r : Nat) (rest : List Nat) :
    recordAfter best (r :: rest) 0 ↔ best < r := by
  simp [recordAfter]

The executable accumulator is exactly the sum of its strict-record bits.


theorem recordsFrom_eq_sum_recordAfterBit (best : Nat) (xs : List Nat) :
    recordsFrom best xs = ∑ i : Fin xs.length, recordAfterBit best xs i := by
  induction xs generalizing best with
  | nil => simp [recordsFrom]
  | cons r rest ih =>
      rw [recordsFrom_step]
      simp only [List.length_cons]
      rw [Fin.sum_univ_succ]
      rw [ih (max best r)]
      have hhead : (if best < r then 1 else 0) =
          recordAfterBit best (r :: rest) 0 := by
        simp [recordAfterBit, recordAfter_cons_zero_iff]
      rw [hhead]
      apply congrArg (fun tail => recordAfterBit best (r :: rest) 0 + tail)
      apply Finset.sum_congr rfl
      intro i _
      unfold recordAfterBit
      exact if_congr (recordAfter_cons_succ_iff best r rest i).symm rfl rfl

Position i is a left-to-right maximum of xs.

def prefixRecordAt (xs : List Nat) (i : Fin xs.length) : Prop :=
  ∀ x ∈ xs.take i.val, x < xs[i.val]

instance prefixRecordAt_decidable (xs : List Nat) (i : Fin xs.length) :
    Decidable (prefixRecordAt xs i) := by
  unfold prefixRecordAt
  infer_instance

Natural-valued prefix-record indicator.

def prefixRecordBit (xs : List Nat) (i : Fin xs.length) : Nat :=
  if prefixRecordAt xs i then 1 else 0

HIRE-ASSISTANT is pointwise the sum of its prefix-record indicators.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
theorem hireAssistant_eq_sum_prefixRecordIndicators (xs : List Nat) :
    hireAssistant xs = ∑ i : Fin xs.length, prefixRecordBit xs i := by
  cases xs with
  | nil => simp [hireAssistant]
  | cons r rest =>
      rw [hireAssistant_cons]
      simp only [List.length_cons]
      rw [Fin.sum_univ_succ]
      rw [recordsFrom_eq_sum_recordAfterBit]
      have hhead : prefixRecordBit (r :: rest) 0 = 1 := by
        simp [prefixRecordBit, prefixRecordAt]
      rw [hhead]
      apply congrArg (fun tail => 1 + tail)
      apply Finset.sum_congr rfl
      intro i _
      unfold prefixRecordBit recordAfterBit prefixRecordAt recordAfter
      simp only [List.getElem_cons_succ, Fin.val_succ, List.take_succ_cons,
        List.mem_cons]
      have hiff :
          (∀ x, x = r ∨ x ∈ rest.take i.val → x < rest[i.val]) ↔
            r < rest[i.val] ∧ ∀ x ∈ rest.take i.val, x < rest[i.val] := by
        constructor
        · intro h
          exact ⟨h r (Or.inl rfl), fun x hx => h x (Or.inr hx)⟩
        · rintro ⟨hr, hrest⟩ x (rfl | hx)
          · exact hr
          · exact hrest x hx
      exact if_congr (by try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [List.mem_cons] using hiff.symm) rfl rfl

@[simp] theorem permutationRanks_length {n : Nat} (sigma : Equiv.Perm (Fin n)) :
    (permutationRanks sigma).length = n := by
  simp [permutationRanks]

The prefix-record event at a fixed position of a sampled permutation.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
def permutationPrefixRecordAt {n : Nat} (sigma : Equiv.Perm (Fin n)) (i : Fin n) : Prop :=
  prefixRecordAt (permutationRanks sigma)
    ⟨i.val, by try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [permutationRanks] using i.isLt⟩

instance permutationPrefixRecordAt_decidable {n : Nat}
    (sigma : Equiv.Perm (Fin n)) (i : Fin n) :
    Decidable (permutationPrefixRecordAt sigma i) := by
  unfold permutationPrefixRecordAt
  infer_instance

A permutation position is a list prefix record exactly when its rank is strictly larger than every earlier rank.


theorem permutationPrefixRecordAt_iff {n : Nat} (sigma : Equiv.Perm (Fin n))
    (i : Fin n) :
    permutationPrefixRecordAt sigma i ↔
      ∀ j : Fin n, j.val < i.val → (sigma j).val < (sigma i).val := by
  unfold permutationPrefixRecordAt prefixRecordAt
  constructor
  · intro h j hji
    have hmem : (sigma j).val ∈ (permutationRanks sigma).take i.val := by
      rw [List.mem_take_iff_getElem]
      refine ⟨j.val, ?_, ?_⟩
      · simp [permutationRanks]
        omega
      · simp [permutationRanks]
    have := h (sigma j).val hmem
    simpa [permutationRanks] using this
  · intro h x hx
    rw [List.mem_take_iff_getElem] at hx
    rcases hx with ⟨j, hj, hx⟩
    have hjn : j < n := by
      simp [permutationRanks] at hj
      omega
    let fj : Fin n := ⟨j, hjn⟩
    have hji : fj.val < i.val := by
      simp [permutationRanks] at hj
      omega
    have hvalue : x = (sigma fj).val := by
      rw [← hx]
      simp [permutationRanks, fj]
    rw [hvalue]
    simpa [permutationRanks] using h fj hji

HIRE-ASSISTANT on a permutation is the sum of its fixed-position record indicators.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
theorem hireAssistant_permutationRanks_eq_sum {n : Nat}
    (sigma : Equiv.Perm (Fin n)) :
    hireAssistant (permutationRanks sigma) =
      ∑ i : Fin n, if permutationPrefixRecordAt sigma i then 1 else 0 := by
  rw [hireAssistant_eq_sum_prefixRecordIndicators]
  let e : Fin n ≃ Fin (permutationRanks sigma).length :=
    (Fin.castOrderIso (permutationRanks_length sigma).symm).toEquiv
  rw [← Equiv.sum_comp e
    (fun i : Fin (permutationRanks sigma).length =>
      prefixRecordBit (permutationRanks sigma) i)]
  apply Finset.sum_congr rfl
  intro i _
  unfold prefixRecordBit permutationPrefixRecordAt
  have he : e i =
      (⟨i.val, by try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [permutationRanks] using i.isLt⟩ :
        Fin (permutationRanks sigma).length) := by
    apply Fin.ext
    simp [e, Fin.castOrderIso_apply]
  rw [he]
  simp

end Chapter05end CLRS

CLRSLean.FourthEdition.Chapter_05.Section_05_3_Randomized_Hiring.RecordProbability

Prefix-record probability under a uniform permutation

This file reuses the position-transposition lemmas from the on-line hiring development. A value-reversing involution turns the executable model's left-to-right maxima into the existing score model's left-to-right minima.

              namespace CLRSnamespace Chapter05open CLRS.Probabilityopen OnlineHiring

The number of permutations whose minimum among the first m positions is at p does not depend on p.


lemma card_isMinInFirst_eq {n m : Nat} (hm : m <= n) (p q : Fin m) :
    ((Finset.univ : Finset (Equiv.Perm (Fin n))).filter
      (fun sigma => isMinInFirst hm sigma p)).card =
    ((Finset.univ : Finset (Equiv.Perm (Fin n))).filter
      (fun sigma => isMinInFirst hm sigma q)).card := by
  classical
  by_cases hpq : p = q
  · subst q
    rfl
  · apply Finset.card_bij
      (fun sigma _ => swapValues (liftFirst hm p) (liftFirst hm q) sigma)
    · intro sigma hsigma
      rw [Finset.mem_filter] at hsigma ⊢
      exact ⟨Finset.mem_univ _, isMinInFirst_swap hm hpq sigma hsigma.2⟩
    · intro sigma1 _ sigma2 _ heq
      have h := congrArg
        (swapValues (liftFirst hm p) (liftFirst hm q)) heq
      simpa [swapValues_involutive] using h
    · intro sigma hsigma
      rw [Finset.mem_filter] at hsigma
      refine ⟨swapValues (liftFirst hm p) (liftFirst hm q) sigma, ?_, ?_⟩
      · rw [Finset.mem_filter]
        refine ⟨Finset.mem_univ _, ?_⟩
        simpa [swapValues_comm] using
          isMinInFirst_swap hm (Ne.symm hpq) sigma hsigma.2
      · simp [swapValues_involutive]

The minimum-position event sets partition the full permutation space.


lemma sum_card_isMinInFirst {n m : Nat} (hm : m <= n) (hmpos : 0 < m) :
    (∑ p : Fin m,
      ((Finset.univ : Finset (Equiv.Perm (Fin n))).filter
        (fun sigma => isMinInFirst hm sigma p)).card) =
      Fintype.card (Equiv.Perm (Fin n)) := by
  classical
  calc
    (∑ p : Fin m,
        ((Finset.univ : Finset (Equiv.Perm (Fin n))).filter
          (fun sigma => isMinInFirst hm sigma p)).card) =
        ∑ p : Fin m, ∑ sigma : Equiv.Perm (Fin n),
          if isMinInFirst hm sigma p then 1 else 0 := by
      apply Finset.sum_congr rfl
      intro p _
      rw [Finset.card_filter]
    _ = ∑ sigma : Equiv.Perm (Fin n), ∑ p : Fin m,
          if isMinInFirst hm sigma p then 1 else 0 := by
      rw [Finset.sum_comm]
    _ = ∑ _sigma : Equiv.Perm (Fin n), 1 := by
      apply Finset.sum_congr rfl
      intro sigma _
      rcases isMinInFirst_exists hm hmpos sigma with ⟨p0, hp0⟩
      have hiff (p : Fin m) : isMinInFirst hm sigma p ↔ p = p0 := by
        constructor
        · intro hp
          exact isMinInFirst_unique hm sigma hp hp0
        · rintro rfl
          exact hp0
      simp_rw [hiff]
      simp
    _ = Fintype.card (Equiv.Perm (Fin n)) := by simp

Every one of the first m positions is equally likely to contain their minimum, hence has probability 1/m.


theorem isMinInFirst_probability {n m : Nat} (hm : m <= n) (hmpos : 0 < m)
    (p : Fin m) :
    fintypeExpect (fun sigma : Equiv.Perm (Fin n) =>
      indicator (isMinInFirst hm sigma p)) = 1 / (m : Real) := by
  classical
  have hnum :
      (∑ sigma : Equiv.Perm (Fin n), indicator (isMinInFirst hm sigma p)) =
        (((Finset.univ : Finset (Equiv.Perm (Fin n))).filter
          (fun sigma => isMinInFirst hm sigma p)).card : Real) :=
    sum_indicator_eq_card (fun sigma : Equiv.Perm (Fin n) =>
      isMinInFirst hm sigma p)
  rw [fintypeExpect, hnum]
  let count : Nat :=
    ((Finset.univ : Finset (Equiv.Perm (Fin n))).filter
      (fun sigma => isMinInFirst hm sigma p)).card
  have huniform :
      (∑ q : Fin m,
        (((Finset.univ : Finset (Equiv.Perm (Fin n))).filter
          (fun sigma => isMinInFirst hm sigma q)).card : Real)) =
        (m : Real) * (count : Real) := by
    calc
      _ = ∑ _q : Fin m, (count : Real) := by
        apply Finset.sum_congr rfl
        intro q _
        exact_mod_cast card_isMinInFirst_eq hm q p
      _ = (m : Real) * (count : Real) := by simp
  have htotal :
      (∑ q : Fin m,
        (((Finset.univ : Finset (Equiv.Perm (Fin n))).filter
          (fun sigma => isMinInFirst hm sigma q)).card : Real)) =
        (Fintype.card (Equiv.Perm (Fin n)) : Real) := by
    exact_mod_cast sum_card_isMinInFirst hm hmpos
  have heq : (m : Real) * (count : Real) =
      (Fintype.card (Equiv.Perm (Fin n)) : Real) := by
    rw [← huniform]
    exact htotal
  have hmne : (m : Real) ≠ 0 := by positivity
  have hcardne : (Fintype.card (Equiv.Perm (Fin n)) : Real) ≠ 0 := by
    rw [Fintype.card_perm]
    positivity
  change (count : Real) / (Fintype.card (Equiv.Perm (Fin n)) : Real) =
    1 / (m : Real)
  field_simp [hmne, hcardne]
  nlinarith

Being the best score seen at position i is the same as being the minimum of the first i+1 positions.


theorem isRecordAt_iff_isMinInFirst {n : Nat} (sigma : Equiv.Perm (Fin n))
    (i : Fin n) :
    isRecordAt sigma i ↔
      isMinInFirst (Nat.succ_le_iff.mpr i.isLt) sigma
        ⟨i.val, Nat.lt_succ_self i.val⟩ := by
  let hm : i.val + 1 <= n := Nat.succ_le_iff.mpr i.isLt
  let last : Fin (i.val + 1) := ⟨i.val, Nat.lt_succ_self i.val⟩
  change isRecordAt sigma i ↔ isMinInFirst hm sigma last
  constructor
  · intro hrecord t
    by_cases hti : t.val = i.val
    · have hlift : liftFirst hm t = i := by
        apply Fin.ext
        exact hti
      rw [hlift, show liftFirst hm last = i by
        apply Fin.ext
        rfl]
    · have htlt : t.val < i.val := by omega
      have hstrict := hrecord (liftFirst hm t) (by simpa [liftFirst] using htlt)
      exact le_of_lt (by simpa [liftFirst] using hstrict)
  · intro hmin j hji
    have hjfirst : j.val < i.val + 1 := by omega
    have hjne : j ≠ liftFirst hm last := by
      intro heq
      have hval := congrArg Fin.val heq
      simp [liftFirst, last] at hval
      omega
    have hstrict := isMinInFirst_lt hm sigma last hmin j hjfirst hjne
    simpa [liftFirst, last] using hstrict

Under a uniform permutation, position i is a score-record (a new minimum) with probability 1/(i+1).

theorem scoreRecord_probability {n : Nat} (i : Fin n) :
    fintypeExpect (fun sigma : Equiv.Perm (Fin n) =>
      indicator (isRecordAt sigma i)) = 1 / ((i.val + 1 : Nat) : Real) := by
  let hm : i.val + 1 <= n := Nat.succ_le_iff.mpr i.isLt
  let last : Fin (i.val + 1) := ⟨i.val, Nat.lt_succ_self i.val⟩
  calc
    fintypeExpect (fun sigma : Equiv.Perm (Fin n) =>
        indicator (isRecordAt sigma i)) =
        fintypeExpect (fun sigma : Equiv.Perm (Fin n) =>
          indicator (isMinInFirst hm sigma last)) := by
      apply congrArg fintypeExpect
      funext sigma
      unfold indicator
      exact if_congr (by simpa [hm, last] using isRecordAt_iff_isMinInFirst sigma i) rfl rfl
    _ = 1 / ((i.val + 1 : Nat) : Real) :=
      isMinInFirst_probability hm (Nat.succ_pos _) last

Reverse every sampled rank. This is an involutive equivalence of the uniform permutation sample space.

def reverseRanksEquiv (n : Nat) :
    Equiv.Perm (Fin n) ≃ Equiv.Perm (Fin n) where
  toFun sigma := sigma.trans Fin.revPerm
  invFun sigma := sigma.trans Fin.revPerm
  left_inv sigma := by
    ext i
    simp [Fin.revPerm_apply, Fin.rev_rev]
  right_inv sigma := by
    ext i
    simp [Fin.revPerm_apply, Fin.rev_rev]

Reversing the rank order turns an executable left-to-right maximum into the on-line hiring model's left-to-right minimum.


theorem permutationPrefixRecordAt_iff_scoreRecord {n : Nat}
    (sigma : Equiv.Perm (Fin n)) (i : Fin n) :
    permutationPrefixRecordAt sigma i ↔
      isRecordAt (reverseRanksEquiv n sigma) i := by
  rw [permutationPrefixRecordAt_iff]
  unfold isRecordAt
  constructor
  · intro h j hji
    change (Fin.revPerm (sigma i)).val < (Fin.revPerm (sigma j)).val
    exact (Fin.rev_lt_rev (i := sigma i) (j := sigma j)).2 (h j hji)
  · intro h j hji
    have hrev := h j hji
    change (Fin.revPerm (sigma i)).val < (Fin.revPerm (sigma j)).val at hrev
    exact (Fin.rev_lt_rev (i := sigma i) (j := sigma j)).1 hrev

Uniform prefix-record probability. Position i is a new maximum in the executable hiring rank order with probability 1/(i+1).

theorem prefixRecord_probability {n : Nat} (i : Fin n) :
    fintypeExpect (fun sigma : Equiv.Perm (Fin n) =>
      indicator (permutationPrefixRecordAt sigma i)) =
      1 / ((i.val + 1 : Nat) : Real) := by
  calc
    fintypeExpect (fun sigma : Equiv.Perm (Fin n) =>
        indicator (permutationPrefixRecordAt sigma i)) =
        fintypeExpect (fun sigma : Equiv.Perm (Fin n) =>
          indicator (isRecordAt (reverseRanksEquiv n sigma) i)) := by
      apply congrArg fintypeExpect
      funext sigma
      unfold indicator
      exact if_congr (permutationPrefixRecordAt_iff_scoreRecord sigma i) rfl rfl
    _ = fintypeExpect (fun sigma : Equiv.Perm (Fin n) =>
          indicator (isRecordAt sigma i)) :=
      fintypeExpect_equiv (reverseRanksEquiv n)
        (fun sigma : Equiv.Perm (Fin n) => indicator (isRecordAt sigma i))
    _ = 1 / ((i.val + 1 : Nat) : Real) := scoreRecord_probability i

end Chapter05end CLRS