Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 5. Probabilistic Analysis and Randomized Algorithms
Browse chapters

Chapter 5 — Probabilistic Analysis and Randomized Algorithms

CLRS, fourth edition · Lean 4 formalization

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

Imports
import CLRSLean.FourthEdition.Chapter_03.Section_03_2_Standard_Functions import CLRSLean.Probability.FiniteExpectation import Mathlib
open Finsetopen Filteropen scoped BigOperators

5.1. The Hiring Problem

This file proves the finite symmetry calculation behind the CLRS hiring problem. At step n+1, the new candidate is hired exactly when the best among the first n+1 candidates is in the new candidate's position. Under the uniform rank model, that event has probability 1/(n+1). Summing these indicator expectations gives the harmonic number.

Main result:

  • Theorem CLRS.Chapter05.uniformAverage_indicator_singleton: a singleton event in a finite uniform space has probability 1/m.

  • Theorem CLRS.Chapter05.hireProbability_eq: the hire probability at step n+1 is 1/(n+1).

  • Theorem CLRS.Chapter05.expectedHiresByIndicators_eq_harmonic: summing the indicator expectations gives the harmonic number.

  • Theorem CLRS.Chapter05.expectedHires_eq_harmonic: the equivalent recurrence solution equals the harmonic number.

  • Theorem CLRS.Chapter05.expectedHires_isBigTheta_log: expected hires grow logarithmically.

Status: proved for the finite rank-symmetry hiring model, including the executable HIRE-ASSISTANT pseudocode (CLRS.Chapter05.hireAssistant).

Probability model: uses CLRS.Probability.uniformAverage from the shared finite-expectation toolkit (CLRSLean/Probability/FiniteExpectation.lean); uniform random-permutation sampling is supplied by Section 5.3 (CLRS.Chapter05.randomizeInPlace_uniform, Lemma 5.4).

The executable layer below formalizes the HIRE-ASSISTANT pseudocode: the first candidate is always hired, and each later candidate is hired exactly when their rank is a new left-to-right maximum.

namespace CLRSnamespace Chapter05open CLRS.Probability

Finite uniform expectation model

Uniform average over the finite sample space {0, ..., m-1}. This is an alias for CLRS.Probability.uniformAverage for backward compatibility.

noncomputable def uniformAverageRange (m : ℕ) (X : ℕ → ℝ) : ℝ := uniformAverage m X

A 0/1 indicator as a real-valued random variable. Alias for CLRS.Probability.indicator.

def indicator (P : Prop) [Decidable P] : ℝ := CLRS.Probability.indicator P

In a finite uniform space of size m, a singleton event has probability 1/m.

theorem uniformAverage_indicator_singleton {m j : ℕ} (hj : j ∈ range m) : uniformAverageRange m (fun i => indicator (i = j)) = 1 / (m : ℝ) := by unfold uniformAverageRange indicator rw [CLRS.Probability.uniformAverage_indicator_singleton hj]

Hiring probabilities from symmetry

At step n+1, index n is the new candidate's position in a rank-symmetry sample space of size n+1.

def newCandidateIsBest (n rankOfBest : ℕ) : Prop := rankOfBest = n
instance newCandidateIsBestDecidable (n rankOfBest : ℕ) : Decidable (newCandidateIsBest n rankOfBest) := inferInstanceAs (Decidable (rankOfBest = n))

The probability that the new candidate is the best among the first n+1.

noncomputable def hireProbability (n : ℕ) : ℝ := uniformAverageRange (n + 1) (fun rankOfBest => indicator (rankOfBest = n))

The single-step hiring probability is 1/(n+1) by finite symmetry.

theorem hireProbability_eq (n : ℕ) : hireProbability n = 1 / ((n : ℝ) + 1) := by classical have hn_mem : n ∈ range (n + 1) := by rw [Finset.mem_range] exact Nat.lt_succ_self n have hsingleton := uniformAverage_indicator_singleton (m := n + 1) (j := n) hn_mem simpa [hireProbability, Nat.cast_add, Nat.cast_one] using hsingleton

Harmonic numbers

The n-th harmonic number, written as Σ_{i=0}^{n-1} 1/(i+1).

noncomputable def harmonic (n : ℕ) : ℝ := ∑ i ∈ range n, 1 / ((i : ℝ) + 1)
@[simp] lemma harmonic_zero : harmonic 0 = 0 := by simp [harmonic]

Successor recurrence for harmonic numbers.

lemma harmonic_succ (n : ℕ) : harmonic (n + 1) = harmonic n + 1 / ((n : ℝ) + 1) := by simp [harmonic, sum_range_succ]

Harmonic numbers are positive once the index is positive.

lemma harmonic_pos {n : ℕ} (hn : 0 < n) : 0 < harmonic n := by refine Finset.sum_pos (fun i _ => div_pos (by norm_num) (by positivity)) ?_ rw [Finset.nonempty_range_iff] exact Nat.ne_of_gt hn

Expected number of hires

Expected hires as a sum of indicator expectations.

noncomputable def expectedHiresByIndicators (n : ℕ) : ℝ := ∑ i ∈ range n, hireProbability i

Linearity of expectation reduces the hiring problem to the harmonic sum.

theorem expectedHiresByIndicators_eq_harmonic (n : ℕ) : expectedHiresByIndicators n = harmonic n := by unfold expectedHiresByIndicators harmonic refine Finset.sum_congr rfl ?_ intro i _hi exact hireProbability_eq i

Expected number of hires from n candidates, assuming the CLRS recurrence obtained from the finite rank-symmetry argument.

noncomputable def expectedHires : ℕ → ℝ | 0 => 0 | n + 1 => expectedHires n + 1 / ((n : ℝ) + 1)

The expected-hire recurrence has the harmonic-number closed form.

theorem expectedHires_eq_harmonic (n : ℕ) : expectedHires n = harmonic n := by induction' n with n ih · simp [expectedHires] · rw [expectedHires, harmonic_succ, ih]

The recurrence and indicator-sum views of the expected hires agree.

theorem expectedHires_eq_expectedHiresByIndicators (n : ℕ) : expectedHires n = expectedHiresByIndicators n := by rw [expectedHires_eq_harmonic, expectedHiresByIndicators_eq_harmonic]

Asymptotic growth

The real harmonic sum used in this section agrees with Mathlib's rational harmonic numbers after casting to ℝ.

theorem harmonic_eq_mathlib_harmonic (n : ℕ) : harmonic n = (_root_.harmonic n : ℝ) := by simp [harmonic, _root_.harmonic, one_div]

The real harmonic sum in this section has logarithmic growth.

theorem harmonic_isBigTheta_log : Chapter03.isBigTheta (fun n : ℕ => harmonic n) (fun n : ℕ => Real.log (n : ℝ)) := by have heq : (fun n : ℕ => harmonic n) =ᶠ[atTop] (fun n : ℕ => (_root_.harmonic n : ℝ)) := by filter_upwards with n exact harmonic_eq_mathlib_harmonic n have hO : Chapter03.isBigO (fun n : ℕ => harmonic n) (fun n : ℕ => Real.log (n : ℝ)) := by unfold Chapter03.isBigO exact heq.trans_isBigO Chapter03.isBigTheta_harmonic_log.1 have hΩ : Chapter03.isBigOmega (fun n : ℕ => harmonic n) (fun n : ℕ => Real.log (n : ℝ)) := by unfold Chapter03.isBigOmega exact Chapter03.isBigTheta_harmonic_log.2.trans_eventuallyEq heq.symm exact ⟨hO, hΩ⟩

The CLRS expected number of hires is logarithmic: E[X] = Θ(log n).

theorem expectedHires_isBigTheta_log : Chapter03.isBigTheta expectedHires (fun n : ℕ => Real.log (n : ℝ)) := by have heq : expectedHires =ᶠ[atTop] harmonic := by filter_upwards with n exact expectedHires_eq_harmonic n have hExpectedHarmonic : Chapter03.isBigTheta expectedHires harmonic := by unfold Chapter03.isBigTheta Chapter03.isBigO Chapter03.isBigOmega exact ⟨heq.isBigO, heq.symm.isBigO⟩ exact Chapter03.isBigTheta_trans hExpectedHarmonic harmonic_isBigTheta_log

Executable HIRE-ASSISTANT (pseudocode execution)

Count the records among rest given the best rank best seen so far: each rank strictly greater than best is a new hire and becomes the running best. This is the inner loop of HIRE-ASSISTANT.

def recordsFrom (best : ℕ) : List ℕ → ℕ | [] => 0 | r :: rest => if best < r then 1 + recordsFrom r rest else recordsFrom best rest

HIRE-ASSISTANT. The number of candidates hired when the interview order is the rank sequence ranks: the first candidate is always hired, and each later candidate is hired exactly when their rank exceeds every rank seen so far (they are a left-to-right maximum). The empty list hires nobody.

def hireAssistant : List ℕ → ℕ | [] => 0 | r :: rest => 1 + recordsFrom r rest

One accumulator step adds a hire exactly when the new rank exceeds the running best, and it advances the running best to the maximum.

theorem recordsFrom_step (best r : ℕ) (rest : List ℕ) : recordsFrom best (r :: rest) = (if best < r then 1 else 0) + recordsFrom (max best r) rest := by by_cases h : best < r · have hm : max best r = r := by omega simp [recordsFrom, h, hm] · have hm : max best r = best := by omega simp [recordsFrom, h, hm]

The first candidate is always hired.

theorem hireAssistant_cons (r : ℕ) (rest : List ℕ) : hireAssistant (r :: rest) = 1 + recordsFrom r rest := rfl

The accumulator counts at most one hire per candidate.

theorem recordsFrom_le_length (best : ℕ) : ∀ xs : List ℕ, recordsFrom best xs ≤ xs.length | [] => by simp [recordsFrom] | r :: rest => by simp [recordsFrom] split · have h := recordsFrom_le_length r rest omega · have h := recordsFrom_le_length best rest omega

HIRE-ASSISTANT hires at most one candidate per interviewed candidate.

theorem hireAssistant_le_length : ∀ xs : List ℕ, hireAssistant xs ≤ xs.length | [] => by simp [hireAssistant] | r :: rest => by simp [hireAssistant] have h := recordsFrom_le_length r rest omega

HIRE-ASSISTANT always hires at least one candidate when there is at least one candidate.

theorem hireAssistant_pos {r : ℕ} {rest : List ℕ} : 0 < hireAssistant (r :: rest) := by simp [hireAssistant]
end Chapter05end CLRS
Imports
import CLRSLean.Probability.FiniteExpectation import Mathlib

5.2. Indicator random variables

This section formalizes the CLRS §5.2 indicator random variable technique and linearity of expectation as a general tool, with the hat-check problem as the canonical worked example (CLRS eq. (5.1)-(5.2)).

The sample space is Ω = Equiv.Perm (Fin n), a uniform random permutation of n elements, evaluated with the shared finite-expectation toolkit CLRS.Probability.fintypeExpect from CLRSLean/Probability/FiniteExpectation.lean. The key primitives reused are fintypeExpect_sum (linearity over a finite indicator sum), fintypeExpect_const, fintypeExpect_equiv (reindexing invariance), and fintypeExpect_indicator_singleton.

Main results:

  • Theorem CLRS.Chapter05.permSendProb_eq: the target π i of a fixed point i under a uniform random permutation is uniformly distributed; the probability of sending i to any k equals the probability of sending it to any l. This is proved by translation invariance of the uniform measure on the permutation group under left multiplication by a transposition.

  • Theorem CLRS.Chapter05.probFixesPoint: a uniform random permutation of Fin n fixes a given point i with probability exactly 1/n (the indicator expectation of the event π i = i).

  • Theorem CLRS.Chapter05.expectedFixedPoints_eq_one: the hat-check problem — the expected number of fixed points of a uniform random permutation of Fin n equals 1, independent of n (for n ≥ 1), by linearity of expectation over the n fixed-point indicators.

Status: proved for the uniform-permutation model over Equiv.Perm (Fin n).

Notation conventions used in this section:

  • π : a permutation in Equiv.Perm (Fin n) (a bijection of Fin n)

  • i, k, l, q : points of Fin n

  • indicator P : the 0/1 indicator random variable of the event P

namespace CLRSnamespace Chapter05open CLRS.Probability

The uniform-permutation sample space

The hat-check problem draws a permutation π uniformly from Equiv.Perm (Fin n) (customer i receives the hat π i). Mathlib supplies the Fintype and DecidableEq instances for Equiv.Perm (Fin n), so the toolkit's fintypeExpect applies directly.

The probability that a uniform random permutation of Fin n sends the point i to the point k, i.e. the expectation of the indicator random variable of the event π i = k.

noncomputable def permSendProb {n : ℕ} (i k : Fin n) : ℝ := fintypeExpect (fun π : Equiv.Perm (Fin n) => indicator (π i = k))

Uniformity of the image of a point. Under a uniform random permutation, the image π i of a fixed point i is uniformly distributed over Fin n: the probability of sending i to k equals the probability of sending i to l.

The proof is translation invariance of the uniform measure on the permutation group: left multiplication by the transposition swap k l is a bijection of the sample space (an Equiv), so by fintypeExpect_equiv it preserves expectations, and it converts the event π i = l into the event π i = k.

theorem permSendProb_eq {n : ℕ} (i k l : Fin n) : permSendProb i k = permSendProb i l := by have hfun : (fun π : Equiv.Perm (Fin n) => indicator ((Equiv.mulLeft (Equiv.swap k l) π) i = k)) = (fun π : Equiv.Perm (Fin n) => indicator (π i = l)) := by funext π rw [Equiv.coe_mulLeft, Equiv.Perm.mul_apply] by_cases h : π i = l · rw [h] simp [indicator, Equiv.swap_apply_right] · have h2 : ¬ (Equiv.swap k l (π i) = k) := by intro hc exact h (by simpa [Equiv.swap_apply_self, Equiv.swap_apply_left] using congrArg (Equiv.swap k l) hc) simp [indicator, h, h2] have he := fintypeExpect_equiv (Equiv.mulLeft (Equiv.swap k l)) (fun π : Equiv.Perm (Fin n) => indicator (π i = k)) rw [hfun] at he unfold permSendProb rw [he]

Fixed-point probability = 1/n (hat-check indicator, CLRS eq. (5.1)). A uniform random permutation of Fin n fixes a given point i with probability exactly 1/n.

Because the n events π i = k (for k : Fin n) partition the sample space, their probabilities sum to 1; and by permSendProb_eq they are all equal, so each equals 1/n.

theorem probFixesPoint {n : ℕ} (i : Fin n) : fintypeExpect (fun π : Equiv.Perm (Fin n) => indicator (π i = i)) = 1 / (n : ℝ) := by have hn : 0 < n := Fin.pos i haveI : Nonempty (Equiv.Perm (Fin n)) := ⟨1⟩ -- The `n` events `π i = k` partition the sample space, so their indicators sum -- to `1` at every `π`. have hsum1 : ∀ π : Equiv.Perm (Fin n), (∑ k : Fin n, indicator (π i = k)) = 1 := by intro π rw [Finset.sum_eq_single (π i)] · simp [indicator] · intro b _ hb simp only [indicator, if_neg (Ne.symm hb)] · intro hmem exact absurd (Finset.mem_univ (π i)) hmem -- Linearity of expectation: the point probabilities sum to `1`. have hsumProb : (∑ k : Fin n, permSendProb i k) = 1 := by have hlin := fintypeExpect_sum (Ω := Equiv.Perm (Fin n)) (Finset.univ : Finset (Fin n)) (fun (k : Fin n) (π : Equiv.Perm (Fin n)) => indicator (π i = k)) have hconst : fintypeExpect (fun π : Equiv.Perm (Fin n) => ∑ k : Fin n, indicator (π i = k)) = 1 := by have hone : (fun π : Equiv.Perm (Fin n) => ∑ k : Fin n, indicator (π i = k)) = (fun _ : Equiv.Perm (Fin n) => (1 : ℝ)) := by funext π; exact hsum1 π rw [hone, fintypeExpect_const Fintype.card_ne_zero] calc (∑ k : Fin n, permSendProb i k) = ∑ k : Fin n, fintypeExpect (fun π : Equiv.Perm (Fin n) => indicator (π i = k)) := rfl _ = fintypeExpect (fun π : Equiv.Perm (Fin n) => ∑ k : Fin n, indicator (π i = k)) := hlin.symm _ = 1 := hconst -- All point probabilities are equal, hence each is `1/n`. have hall : ∀ k : Fin n, permSendProb i k = permSendProb i i := fun k => permSendProb_eq i k i have hcollapse : (∑ k : Fin n, permSendProb i i) = 1 := by rw [← hsumProb] exact Finset.sum_congr rfl (fun k _ => (hall k).symm) rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] at hcollapse have hn' : (n : ℝ) ≠ 0 := by exact_mod_cast hn.ne' have hgoal : permSendProb i i = 1 / (n : ℝ) := by rw [eq_div_iff hn', mul_comm] exact hcollapse exact hgoal

Hat-check problem (CLRS §5.2, eq. (5.2)). The expected number of customers who get their own hat back — equivalently, the expected number of fixed points of a uniform random permutation of Fin n — equals exactly 1, for every n ≥ 1, independent of n.

This is the paradigmatic application of linearity of expectation: the number of fixed points is the sum ∑ i, indicator (π i = i) of n indicator random variables, each with expectation 1/n by probFixesPoint, and fintypeExpect_sum sums the expectations to n · (1/n) = 1.

theorem expectedFixedPoints_eq_one {n : ℕ} (hn : 0 < n) : fintypeExpect (fun π : Equiv.Perm (Fin n) => ∑ i : Fin n, indicator (π i = i)) = 1 := by have hn' : (n : ℝ) ≠ 0 := by exact_mod_cast hn.ne' rw [fintypeExpect_sum Finset.univ (fun (i : Fin n) (π : Equiv.Perm (Fin n)) => indicator (π i = i))] rw [Finset.sum_congr rfl (fun i (_ : i ∈ Finset.univ) => probFixesPoint i)] rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] field_simp
end Chapter05end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_05.Section_05_2_Indicator_Expectation

5.2. Indicator expectation as event probability

This small interface file exposes the textbook identity used throughout Chapter 5: the expectation of an indicator random variable is the probability of its event. Both sides use the same finite uniform sample space, so this is an interface theorem rather than a second probability model.

namespace CLRSnamespace Chapter05open CLRS.Probability

The probability of an event in a finite uniform sample space.

noncomputable def eventProbability {Omega : Type} [Fintype Omega] [DecidableEq Omega] (P : Omega -> Prop) [DecidablePred P] : Real := fintypeExpect (fun omega => indicator (P omega))

Indicator expectation identity (CLRS Lemma 5.1 interface). The expectation of an event's indicator is the probability of that event.

theorem indicator_expectation_eq_probability {Omega : Type} [Fintype Omega] [DecidableEq Omega] (P : Omega -> Prop) [DecidablePred P] : fintypeExpect (fun omega => indicator (P omega)) = eventProbability P := rfl
end Chapter05end CLRS
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
Imports
import CLRSLean.FourthEdition.Chapter_03.Section_03_1_Asymptotic_Notation import CLRSLean.Probability.FiniteExpectation import Mathlib

5.4. Probabilistic analysis

This section applies the CLRS §5.2 indicator-random-variable technique (see CLRSLean/Chapter_05/Section_05_2_Indicator_Random_Variables.lean) to the birthday and balls-and-bins analyses from CLRS §5.4, both over a product uniform sample space evaluated with the shared toolkit CLRS.Probability.fintypeExpect.

  • Birthday paradox (CLRS eq. (5.6)-(5.8)): with k people and n equally likely birthdays, the expected number of unordered pairs sharing a birthday is C(k,2)/n = k(k-1)/(2n).

  • Balls and bins (CLRS eq. (5.9)-(5.10)): throwing k balls independently and uniformly into n bins, the expected number of balls landing in a fixed bin is k/n.

Both are pure indicator-plus-linearity arguments. The sample space is Fin k → Fin n (each person's birthday / each ball's bin an independent uniform coordinate). The section re-derives the two coordinate-marginal primitives it needs — a single coordinate is uniform (singleBinProb) and a pair of distinct coordinates collides with probability 1/n (pairSameProb) — directly from the toolkit's fintypeExpect_equiv, fintypeExpect_fst (product independence) and fintypeExpect_indicator_singleton, keeping the file self-contained and citing only the shared toolkit. This mirrors, without modifying, the balls-and-bins analyses of §8.4 (bucket sort) and §11.2 (chained hashing).

The fair-coin development uses CoinFlip n = Fin n → Fin 2. It studies the maximum run of heads across the whole sequence. Its tail bound and tail-sum identity prove E[L] ≤ log₂ n + 2; independent disjoint blocks prove E[L] ≥ log₂ n / 8 for n ≥ 16. Together these give the expected longest streak logarithmic growth.

Main results:

  • Theorem CLRS.Chapter05.singleBinProb: a fixed ball lands in a fixed bin with probability 1/n.

  • Theorem CLRS.Chapter05.pairSameProb: two distinct people share a birthday with probability 1/n.

  • Theorem CLRS.Chapter05.expectedBallsInBin_eq: the expected number of balls in a fixed bin is k/n.

  • Theorem CLRS.Chapter05.expectedCollisions_eq: the expected number of same-birthday pairs is k(k-1)/(2n).

  • Theorem CLRS.Chapter05.longestStreak_upperBound: for positive t, the chance of a run of at least t heads is at most n / 2^t.

  • Theorem CLRS.Chapter05.expectedLongestStreak_le: the expected maximum run is at most log₂ n + 2.

  • Theorem CLRS.Chapter05.expectedLongestStreak_lowerBound: for n ≥ 16, the expected maximum run is at least log₂ n / 8.

Status: proved for the birthday/occupancy product-uniform model and the longest-run upper and lower bounds in the independent fair-coin model.

Notation conventions used in this section:

  • k : number of people / balls; n : number of birthdays / bins

  • a : Fin k → Fin n : an assignment (each person's birthday / each ball's bin)

  • i, j : people / balls in Fin k; q : a fixed bin in Fin n

  • indicator P : the 0/1 indicator random variable of the event P

Implementation details

The on-line hiring analysis (CLRS §5.4.4) is a support page outside the reader sidebar:

namespace CLRSnamespace Chapter05open CLRS.Probability

Coordinate marginals of the product-uniform space

The sample space is Fin k → Fin n: each of k coordinates is an independent uniform draw from Fin n. We first isolate the two marginal facts the two expectations need.

Split an assignment a : Fin k → Fin n into the value of one coordinate i and the assignment of the remaining coordinates. This is the product decomposition witnessing that coordinate i is independent of the rest.

noncomputable def binSplit {k n : Nat} (i : Fin k) : (Fin k → Fin n) ≃ Fin n × ({x : Fin k // x ≠ i} → Fin n) 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 coordinate equals the expectation over the single-coordinate space Fin n.

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

Single-coordinate probability = 1/n. A fixed ball i lands in a fixed bin q — equivalently, a fixed person i has a fixed birthday q — with probability exactly 1/n.

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

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

noncomputable def binSplitPair {k n : Nat} (i j : Fin k) (hij : i ≠ j) : (Fin k → Fin n) ≃ (Fin n × Fin n) × ({x : Fin k // x ≠ i ∧ x ≠ j} → Fin n) 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 n agree is 1/n: the diagonal of Fin n × Fin n has n of the n² points.

theorem fintypeExpect_prod_diag {n : Nat} (hn : 0 < n) : fintypeExpect (fun q : Fin n × Fin n => indicator (q.1 = q.2)) = 1 / (n : ℝ) := by have hn' : (n : ℝ) ≠ 0 := by exact_mod_cast hn.ne' have hnum : (∑ q : Fin n × Fin n, indicator (q.1 = q.2)) = (n : ℝ) := by unfold indicator rw [Fintype.sum_prod_type] have hinner : ∀ a : Fin n, (∑ b : Fin n, (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 hn']

Pairwise collision probability = 1/n (CLRS eq. (5.7)). Two distinct people i ≠ j share a birthday — equivalently, two distinct balls land in the same bin — with probability exactly 1/n, as a genuine expectation over the product-uniform input distribution Fin k → Fin n, using pairwise independence.

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

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

theorem sum_upper_triangle (k : Nat) : (∑ i : Fin k, ∑ j : Fin k, (if i < j then (1 : ℝ) else 0)) = (k : ℝ) * ((k : ℝ) - 1) / 2 := by have hpt : ∀ i j : Fin k, (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 k, ∑ j : Fin k, (if i < j then (1 : ℝ) else 0)) = ∑ i : Fin k, ∑ j : Fin k, (if j < i then (1 : ℝ) else 0) := Finset.sum_comm have hD : (∑ i : Fin k, ∑ j : Fin k, (if i = j then (1 : ℝ) else 0)) = (k : ℝ) := by have hone : ∀ i : Fin k, (∑ j : Fin k, (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 k, ∑ j : Fin k, (if i < j then (1 : ℝ) else 0)) + (∑ i : Fin k, ∑ j : Fin k, (if j < i then (1 : ℝ) else 0)) + (∑ i : Fin k, ∑ j : Fin k, (if i = j then (1 : ℝ) else 0)) = (k : ℝ) * (k : ℝ) := by rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib] have hstep : (∑ i : Fin k, ((∑ j : Fin k, (if i < j then (1 : ℝ) else 0)) + (∑ j : Fin k, (if j < i then (1 : ℝ) else 0)) + ∑ j : Fin k, (if i = j then (1 : ℝ) else 0))) = ∑ _i : Fin k, (k : ℝ) := 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 k, ∑ j : Fin k, (if i < j then (1 : ℝ) else 0)) = ((k : ℝ) * (k : ℝ) - (k : ℝ)) / 2 := by linarith rw [h2]; ring

Birthday paradox

The number of same-birthday pairs under a birthday assignment a: one for each unordered pair {i, j} with i < j and a i = a j.

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

Expected number of same-birthday pairs among k people with n uniform birthdays.

noncomputable def expectedCollisions (k n : Nat) : ℝ := fintypeExpect (fun a : Fin k → Fin n => sameBirthdayPairs a)

Birthday paradox (CLRS §5.4, eq. (5.8)). The expected number of unordered same-birthday pairs among k people with n equally likely birthdays is exactly C(k,2)/n = k(k-1)/(2n), by linearity of expectation over the C(k,2) pair indicators, each with collision probability 1/n.

theorem expectedCollisions_eq {k n : Nat} (hn : 0 < n) : expectedCollisions k n = (k : ℝ) * ((k : ℝ) - 1) / (2 * (n : ℝ)) := by unfold expectedCollisions sameBirthdayPairs haveI : Nonempty (Fin n) := ⟨⟨0, hn⟩⟩ have hcard : Fintype.card (Fin k → Fin n) ≠ 0 := Fintype.card_ne_zero have hn' : (n : ℝ) ≠ 0 := by exact_mod_cast hn.ne' have hE : fintypeExpect (fun a : Fin k → Fin n => ∑ i : Fin k, ∑ j : Fin k, (if i < j then indicator (a i = a j) else 0)) = ∑ i : Fin k, ∑ j : Fin k, (if i < j then (1 / (n : ℝ)) else 0) := by rw [fintypeExpect_sum Finset.univ (fun (i : Fin k) (a : Fin k → Fin n) => ∑ j : Fin k, (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 k) (a : Fin k → Fin n) => 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 pairSameProb i j (ne_of_lt hlt) hn · simp only [if_neg hlt] exact fintypeExpect_const hcard 0 rw [hE] have hpair : (∑ i : Fin k, ∑ j : Fin k, (if i < j then (1 / (n : ℝ)) else 0)) = (1 / (n : ℝ)) * ((k : ℝ) * ((k : ℝ) - 1) / 2) := by rw [← sum_upper_triangle k, 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 [hpair] field_simp

Balls and bins

The number of balls that land in bin q under an assignment a.

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

Expected number of balls landing in a fixed bin q when k balls are thrown independently and uniformly into n bins.

noncomputable def expectedBallsInBin (k n : Nat) (q : Fin n) : ℝ := fintypeExpect (fun a : Fin k → Fin n => ballsInBin a q)

Balls and bins (CLRS §5.4, eq. (5.10)). The expected number of balls landing in a fixed bin q, when k balls are thrown independently and uniformly into n bins, is exactly k/n, by linearity of expectation over the k per-ball indicators, each with probability 1/n.

theorem expectedBallsInBin_eq {k n : Nat} (q : Fin n) (hn : 0 < n) : expectedBallsInBin k n q = (k : ℝ) / (n : ℝ) := by unfold expectedBallsInBin ballsInBin rw [fintypeExpect_sum Finset.univ (fun (i : Fin k) (a : Fin k → Fin n) => indicator (a i = q))] simp only [singleBinProb _ q hn] rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, mul_one_div]

Streaks (longest run of heads)

Sample space of n independent fair coin flips (0 = tails, 1 = heads).

def CoinFlip (n : ℕ) : Type := Fin n → Fin 2
instance (n : ℕ) : Fintype (CoinFlip n) := inferInstanceAs (Fintype (Fin n → Fin 2))instance (n : ℕ) : DecidableEq (CoinFlip n) := inferInstanceAs (DecidableEq (Fin n → Fin 2))

Read position k of coin-flip sequence a, returning 0 if out of bounds.

def headAt (n : ℕ) (a : CoinFlip n) (k : ℕ) : Fin 2 := if h : k < n then a ⟨k, h⟩ else (0 : Fin 2)

hasRunOfLength n t a iff sequence a contains at least t consecutive heads.

def hasRunOfLength (n t : ℕ) (a : CoinFlip n) : Prop := t ≤ n ∧ ∃ (i : ℕ), i ∈ Finset.range (n+1) ∧ i + t ≤ n ∧ (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2))
instance (n t : ℕ) (a : CoinFlip n) : Decidable (hasRunOfLength n t a) := by unfold hasRunOfLength; infer_instance

Length of the longest run of heads in a.

noncomputable def longestStreak (n : ℕ) (a : CoinFlip n) : ℕ := (Nat.find (⟨n+1, by intro h; rcases h with ⟨hle, hi⟩; omega ⟩ : ∃ t, ¬ hasRunOfLength n t a)).pred
open CLRS.Probability

The probability that all t coin flips in a sequence of exactly t flips are heads is 1 / 2^t.

lemma prob_first_t_heads (t : ℕ) : fintypeExpect (fun (a : CoinFlip t) => indicator (∀ j : Fin t, a j = (1 : Fin 2))) = 1 / ((2 : ℝ) ^ t) := by let constOne : CoinFlip t := fun _ => (1 : Fin 2) have h_indicator : (fun (a : CoinFlip t) => indicator (∀ j : Fin t, a j = (1 : Fin 2))) = (fun a => indicator (a = constOne)) := by ext a have h_eq : (∀ j : Fin t, a j = (1 : Fin 2)) ↔ (a = constOne) := by constructor · intro h; apply funext; exact h · intro h j; simp [h, constOne] simp [h_eq] rw [h_indicator] have h_card : (Fintype.card (CoinFlip t) : ℝ) = (2 : ℝ) ^ t := by have h_nat : Fintype.card (CoinFlip t) = 2 ^ t := by calc Fintype.card (CoinFlip t) = Fintype.card (Fin t → Fin 2) := rfl _ = (Fintype.card (Fin 2)) ^ (Fintype.card (Fin t)) := by rw [Fintype.card_fun] _ = 2 ^ t := by simp rw [h_nat] simp calc fintypeExpect (fun (a : CoinFlip t) => indicator (a = constOne)) = 1 / (Fintype.card (CoinFlip t) : ℝ) := fintypeExpect_indicator_singleton constOne _ = 1 / ((2 : ℝ) ^ t) := by rw [h_card]

For k < n, headAt is the same as direct indexing.

lemma headAt_eq_of_lt (n : ℕ) (a : CoinFlip n) (k : ℕ) (hk : k < n) : headAt n a k = a ⟨k, hk⟩ := by simp [headAt, hk]

If k ≥ n, headAt returns 0.

lemma headAt_eq_zero_of_ge (n : ℕ) (a : CoinFlip n) (k : ℕ) (hk : n ≤ k) : headAt n a k = (0 : Fin 2) := by simp [headAt, hk]

The Finset of positions {i, i+1, ..., i+t-1} in Fin n, given i + t ≤ n.

def streakS (n t i : ℕ) (h : i + t ≤ n) : Finset (Fin n) := Finset.image (λ (j : Fin t) => ⟨i + j.val, by have := j.isLt; omega⟩) (Finset.univ : Finset (Fin t))
lemma card_streakS (n t i : ℕ) (h : i + t ≤ n) : (streakS n t i h).card = t := by unfold streakS have hinj : Function.Injective (λ (j : Fin t) => ⟨i + j.val, by have := j.isLt; omega⟩ : Fin t → Fin n) := by intro x y h apply Fin.ext have hval : (i + x.val : ℕ) = i + y.val := congr_arg (λ (z : Fin n) => z.val) h omega simp [Finset.card_image_of_injective, hinj, Fintype.card_fin]

A run of t consecutive heads starting at position i expressed via the streakS Finset is equivalent to the same run expressed via headAt.

lemma streakS_all_heads_iff (n t i : ℕ) (h : i + t ≤ n) (a : CoinFlip n) : (∀ x ∈ streakS n t i h, a x = (1 : Fin 2)) ↔ (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2)) := by constructor · intro hS j hj have hj_lt_t : (j : ℕ) < t := Finset.mem_range.1 hj have hpos : i + j < n := by omega let j_fin : Fin t := ⟨j, hj_lt_t⟩ have hmem : (⟨i + j, hpos⟩ : Fin n) ∈ streakS n t i h := by apply Finset.mem_image.mpr exact ⟨j_fin, Finset.mem_univ _, rfl⟩ rw [headAt_eq_of_lt n a (i + j) hpos] exact hS ⟨i + j, hpos⟩ hmem · intro hheads x hx rcases Finset.mem_image.mp hx with ⟨j_fin, _, hx_eq⟩ have hj_val_lt_t : j_fin.val < t := j_fin.isLt have hj_val_mem_range : j_fin.val ∈ Finset.range t := Finset.mem_range.mpr hj_val_lt_t have hpos : i + j_fin.val < n := by omega subst hx_eq rw [← headAt_eq_of_lt n a (i + j_fin.val) hpos] exact hheads (j_fin.val) hj_val_mem_range

Bijection between sequences where every position in a Finset S is heads and functions on the complement of S. Used to count sequences with a fixed pattern of heads.

noncomputable def headsSetBijection {n : ℕ} (S : Finset (Fin n)) : {a : CoinFlip n // ∀ x ∈ S, a x = (1 : Fin 2)} ≃ (↥(Finset.univ \ S) → Fin 2) where toFun a := λ x : ↥(Finset.univ \ S) => a.1 x.val invFun f := { val := λ x : Fin n => if h : x ∈ S then (1 : Fin 2) else f ⟨x, by have hmem : x ∈ (Finset.univ : Finset (Fin n)) := Finset.mem_univ x exact Finset.mem_sdiff.mpr ⟨hmem, h⟩ ⟩ property := by intro x hx; simp [hx] } left_inv a := by apply Subtype.ext funext x dsimp split_ifs with hx · exact (a.property x hx).symm · rfl right_inv f := by ext x dsimp have hx : x.val ∉ S := by have hx_mem : x.val ∈ Finset.univ \ S := x.property exact (Finset.mem_sdiff.mp hx_mem).2 simp [hx]

The probability that the t consecutive positions {i, ..., i + t - 1} are all heads in a sequence of n fair coin flips (given i + t ≤ n) is exactly 1 / 2^t.

lemma prob_run_at (n t i : ℕ) (h : i + t ≤ n) : fintypeExpect (fun (a : CoinFlip n) => indicator (∀ x ∈ streakS n t i h, a x = (1 : Fin 2))) = 1 / ((2 : ℝ) ^ t) := by let S := streakS n t i h have hScard : S.card = t := card_streakS n t i h have h_total_card : (Fintype.card (CoinFlip n) : ℝ) = (2 : ℝ) ^ n := by have h_nat : Fintype.card (CoinFlip n) = 2 ^ n := by calc Fintype.card (CoinFlip n) = Fintype.card (Fin n → Fin 2) := rfl _ = (Fintype.card (Fin 2)) ^ (Fintype.card (Fin n)) := by rw [Fintype.card_fun] _ = 2 ^ n := by simp rw [h_nat]; simp have h_heads_card : (Fintype.card {a : CoinFlip n // ∀ x ∈ S, a x = (1 : Fin 2)} : ℝ) = (2 : ℝ) ^ (n - t) := by have h_card_nat : Fintype.card {a : CoinFlip n // ∀ x ∈ S, a x = (1 : Fin 2)} = 2 ^ (n - t) := by calc Fintype.card {a : CoinFlip n // ∀ x ∈ S, a x = (1 : Fin 2)} = Fintype.card (↥(Finset.univ \ S) → Fin 2) := Fintype.card_congr (headsSetBijection S) _ = (Fintype.card (Fin 2)) ^ Fintype.card (↥(Finset.univ \ S)) := by rw [Fintype.card_fun] _ = 2 ^ (Finset.card (Finset.univ \ S)) := by rw [Fintype.card_coe, Fintype.card_fin] _ = 2 ^ (n - t) := by have htle : t ≤ n := by omega have huniv : (Finset.univ : Finset (Fin n)).card = n := by simp have hsub : S ⊆ Finset.univ := Finset.subset_univ _ have hsum : (Finset.univ \ S).card + S.card = (Finset.univ : Finset (Fin n)).card := Finset.card_sdiff_add_card_eq_card hsub rw [hScard, huniv] at hsum have : (Finset.univ \ S).card = n - t := (Nat.add_right_cancel (calc (Finset.univ \ S).card + t = n := hsum _ = (n - t) + t := by rw [Nat.sub_add_cancel htle])) rw [this] simpa using congrArg (fun (x : ℕ) => (x : ℝ)) h_card_nat calc fintypeExpect (fun (a : CoinFlip n) => indicator (∀ x ∈ S, a x = (1 : Fin 2))) = (∑ a : CoinFlip n, indicator (∀ x ∈ S, a x = (1 : Fin 2))) / (Fintype.card (CoinFlip n) : ℝ) := rfl _ = ((Fintype.card {a : CoinFlip n // ∀ x ∈ S, a x = (1 : Fin 2)} : ℝ)) / (Fintype.card (CoinFlip n) : ℝ) := by simp [indicator, Fintype.card_subtype] _ = ((2 : ℝ) ^ (n - t)) / ((2 : ℝ) ^ n) := by rw [h_heads_card, h_total_card] _ = 1 / ((2 : ℝ) ^ t) := by have hpos' : (2 : ℝ) ^ t ≠ 0 := by positivity field_simp [hpos'] have h_eq : (n - t) + t = n := Nat.sub_add_cancel (by omega) calc ((2 : ℝ) ^ (n - t)) * ((2 : ℝ) ^ t) = (2 : ℝ) ^ ((n - t) + t) := by rw [pow_add] _ = (2 : ℝ) ^ n := by rw [h_eq]
lemma hasRunOfLength_mono (n m t : ℕ) (a : CoinFlip n) (hmn : m ≤ t) (h : hasRunOfLength n t a) : hasRunOfLength n m a := by rcases h with ⟨hn_t, i, hi, hiadd, hrun⟩ refine ⟨by omega, i, hi, by omega, ?_⟩ intro j hj have : j ∈ Finset.range t := Finset.mem_range.mpr (by have hjt : j < m := Finset.mem_range.1 hj omega) exact hrun j this lemma longestStreak_ge_iff_hasRunOfLength (n t : ℕ) (a : CoinFlip n) : longestStreak n a ≥ t ↔ hasRunOfLength n t a := by constructor · intro hge have h_m_exists : ∃ t', ¬ hasRunOfLength n t' a := ⟨n+1, by intro h; rcases h with ⟨hle, hi⟩; omega⟩ set m := Nat.find h_m_exists with hm have hm_spec : ¬ hasRunOfLength n m a := Nat.find_spec h_m_exists have hm_min : ∀ k < m, hasRunOfLength n k a := λ k hk => by by_contra hnk exact (Nat.find_min h_m_exists hk) hnk have hm_pos : 0 < m := by by_contra! hzero have hmzero : m = 0 := by omega have : hasRunOfLength n 0 a := by refine ⟨by omega, ?_⟩ refine ⟨0, by simp, by omega, ?_⟩ simp rw [hmzero] at hm_spec exact hm_spec this have hpred : longestStreak n a = m.pred := rfl have hge' : m.pred ≥ t := by rw [← hpred]; exact hge have hm_gt_t : m > t := by by_contra! hle have h_eq : m = m.pred + 1 := (Nat.succ_pred_eq_of_pos hm_pos).symm have h_ge : m ≥ t + 1 := by linarith linarith exact hm_min t (by omega) · intro hrun have h_m_exists : ∃ t', ¬ hasRunOfLength n t' a := ⟨n+1, by intro h; rcases h with ⟨hle, hi⟩; omega⟩ set m := Nat.find h_m_exists with hm have hm_spec : ¬ hasRunOfLength n m a := Nat.find_spec h_m_exists have hm_min : ∀ k < m, hasRunOfLength n k a := λ k hk => by by_contra hnk exact (Nat.find_min h_m_exists hk) hnk have hm_pos : 0 < m := by by_contra! hzero have hmzero : m = 0 := by omega have : hasRunOfLength n 0 a := by refine ⟨by omega, ?_⟩ refine ⟨0, by simp, by omega, ?_⟩ simp rw [hmzero] at hm_spec exact hm_spec this have hm_gt_t : m > t := by by_contra! hle have : hasRunOfLength n m a := hasRunOfLength_mono n m t a hle hrun exact hm_spec this have hpred : longestStreak n a = m.pred := rfl rw [hpred] have : m.pred ≥ t := by have h_ge : t + 1 ≤ m := Nat.succ_le_of_lt hm_gt_t have h_succ : m.pred + 1 = m := Nat.succ_pred_eq_of_pos hm_pos have h_sum : t + 1 ≤ m.pred + 1 := by calc t + 1 ≤ m := h_ge _ = m.pred + 1 := h_succ.symm exact Nat.le_of_add_le_add_right h_sum exact this lemma fintypeExpect_mono {Ω : Type} [Fintype Ω] [DecidableEq Ω] {X Y : Ω → ℝ} (Variable name `hX` 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`hX : ∀ ω, 0 ≤ X ω) (Variable name `hY` 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`hY : ∀ ω, 0 ≤ Y ω) (hXY : ∀ ω, X ω ≤ Y ω) : fintypeExpect X ≤ fintypeExpect Y := by have h_nonneg_diff : ∀ ω, 0 ≤ Y ω - X ω := by intro ω; have h := hXY ω; linarith have h_nonneg_expect_diff : 0 ≤ fintypeExpect (Y - X) := fintypeExpect_nonneg h_nonneg_diff have h_add : fintypeExpect (X + (Y - X)) = fintypeExpect X + fintypeExpect (Y - X) := fintypeExpect_add X (Y - X) have h_eq : X + (Y - X) = Y := by ext ω; dsimp; ring rw [h_eq] at h_add linarith lemma prob_run_at_bound (n t i : ℕ) : fintypeExpect (fun (a : CoinFlip n) => indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2))) ≤ 1 / ((2 : ℝ) ^ t) := by by_cases h : i + t ≤ n · have h_equiv : (fun (a : CoinFlip n) => indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2))) = (fun a => indicator (∀ x ∈ streakS n t i h, a x = (1 : Fin 2))) := by ext a; simp [streakS_all_heads_iff n t i h a] rw [h_equiv] linarith [prob_run_at n t i h] · by_cases ht0 : 0 < t · have h_impossible : ∀ a : CoinFlip n, ¬ (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2)) := by intro a hall by_cases hi_lt_n : i < n · have hn_minus_i_lt_t : n - i < t := by omega have hj_mem : n - i ∈ Finset.range t := Finset.mem_range.mpr hn_minus_i_lt_t have h_val : headAt n a (i + (n - i)) = (0 : Fin 2) := by have : i + (n - i) = n := Nat.add_sub_cancel' (by omega) rw [this] exact headAt_eq_zero_of_ge n a n (le_refl n) have h_should : headAt n a (i + (n - i)) = (1 : Fin 2) := hall (n - i) hj_mem have : (0 : Fin 2) ≠ (1 : Fin 2) := by decide apply this calc (0 : Fin 2) = headAt n a (i + (n - i)) := Eq.symm h_val _ = (1 : Fin 2) := h_should · have hi_ge_n : n ≤ i := by omega have h0_mem : 0 ∈ Finset.range t := Finset.mem_range.mpr ht0 have h_val : headAt n a (i + 0) = (0 : Fin 2) := by simp exact headAt_eq_zero_of_ge n a i hi_ge_n have h_should : headAt n a (i + 0) = (1 : Fin 2) := by simpa using hall 0 h0_mem have : (0 : Fin 2) ≠ (1 : Fin 2) := by decide apply this calc (0 : Fin 2) = headAt n a (i + 0) := Eq.symm h_val _ = (1 : Fin 2) := h_should have h_zero : fintypeExpect (fun (a : CoinFlip n) => indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2))) = 0 := by have h_sum_zero : (∑ a : CoinFlip n, indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2))) = 0 := by apply Finset.sum_eq_zero intro a ha have h_not : ¬ (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2)) := h_impossible a simp [indicator] classical have h_exists := not_forall.mp h_not rcases h_exists with ⟨j, hj⟩ rcases Classical.not_imp.mp hj with ⟨hj_mem, hj_neq⟩ have hj_lt : j < t := Finset.mem_range.1 hj_mem refine ⟨j, hj_lt, hj_neq⟩ unfold fintypeExpect rw [h_sum_zero, zero_div] rw [h_zero] positivity · have h_t0 : t = 0 := by omega subst h_t0 haveI : Nonempty (CoinFlip n) := ⟨fun _ => (0 : Fin 2)⟩ have h_one : fintypeExpect (fun (a : CoinFlip n) => (1 : ℝ)) = 1 := fintypeExpect_const Fintype.card_ne_zero 1 calc fintypeExpect (fun (a : CoinFlip n) => indicator (∀ j ∈ Finset.range 0, headAt n a (i + j) = (1 : Fin 2))) = fintypeExpect (fun (a : CoinFlip n) => (1 : ℝ)) := by simp [indicator] _ = 1 := h_one _ ≤ 1 / (1 : ℝ) := by norm_num _ = 1 / ((2 : ℝ) ^ 0) := by norm_num theorem longestStreak_upperBound (n t : ℕ) (ht : 0 < t) : fintypeExpect (fun (a : CoinFlip n) => indicator (longestStreak n a ≥ t)) ≤ (n : ℝ) / ((2 : ℝ) ^ t) := by by_cases hnt : t ≤ n · have h_union_bound : ∀ a : CoinFlip n, indicator (longestStreak n a ≥ t) ≤ Finset.sum (Finset.range n) (λ i => indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2))) := by intro a by_cases hge : longestStreak n a ≥ t · have hrun : hasRunOfLength n t a := (longestStreak_ge_iff_hasRunOfLength n t a).mp hge rcases hrun with ⟨hle, i, himem, hiadd, hi_run⟩ have hi_lt_n : i < n := by have : i < n+1 := Finset.mem_range.1 himem omega have hi_mem : i ∈ Finset.range n := Finset.mem_range.mpr hi_lt_n have h_all' : ∀ j : ℕ, j < t → headAt n a (i + j) = (1 : Fin 2) := by intro j hj; apply hi_run; exact Finset.mem_range.mpr hj have h_run_val : indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2)) = 1 := by simp [indicator]; exact h_all' have h_nonneg_indic : ∀ (k : ℕ), 0 ≤ indicator (∀ j ∈ Finset.range t, headAt n a (k + j) = (1 : Fin 2)) := by intro k; unfold indicator; split <;> norm_num have h_single : indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2)) ≤ Finset.sum (Finset.range n) (λ k => indicator (∀ j ∈ Finset.range t, headAt n a (k + j) = (1 : Fin 2))) := Finset.single_le_sum (s := Finset.range n) (f := λ k => indicator (∀ j ∈ Finset.range t, headAt n a (k + j) = (1 : Fin 2))) (λ k hk => h_nonneg_indic k) hi_mem calc indicator (longestStreak n a ≥ t) = 1 := by simp [indicator, hge] _ = indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2)) := by rw [h_run_val] _ ≤ Finset.sum (Finset.range n) (λ k => indicator (∀ j ∈ Finset.range t, headAt n a (k + j) = (1 : Fin 2))) := h_single · simp [indicator, hge] have h_expect_sum_le : fintypeExpect (fun a : CoinFlip n => Finset.sum (Finset.range n) (λ i => indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2)))) ≤ (n : ℝ) * (1 / ((2 : ℝ) ^ t)) := by calc fintypeExpect (fun a : CoinFlip n => Finset.sum (Finset.range n) (λ i => indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2)))) = Finset.sum (Finset.range n) (λ i => fintypeExpect (fun (a : CoinFlip n) => indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2)))) := fintypeExpect_sum (Finset.range n) (λ i a => indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2))) _ ≤ Finset.sum (Finset.range n) (λ _ => 1 / ((2 : ℝ) ^ t)) := by refine Finset.sum_le_sum (λ i hi => ?_) exact prob_run_at_bound n t i _ = (n : ℝ) * (1 / ((2 : ℝ) ^ t)) := by simp [Finset.card_range] have h_expect_bound : fintypeExpect (fun a : CoinFlip n => Finset.sum (Finset.range n) (λ i => indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2)))) ≤ (n : ℝ) / ((2 : ℝ) ^ t) := by calc fintypeExpect (fun a : CoinFlip n => Finset.sum (Finset.range n) (λ i => indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2)))) ≤ (n : ℝ) * (1 / ((2 : ℝ) ^ t)) := h_expect_sum_le _ = (n : ℝ) / ((2 : ℝ) ^ t) := by ring have h_nonneg_ind : ∀ a : CoinFlip n, 0 ≤ indicator (longestStreak n a ≥ t) := by intro a; unfold indicator; split <;> norm_num have h_nonneg_sum : ∀ a : CoinFlip n, 0 ≤ Finset.sum (Finset.range n) (λ i => indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2))) := by intro a; apply Finset.sum_nonneg; intro i hi; unfold indicator; split <;> norm_num calc fintypeExpect (fun a : CoinFlip n => indicator (longestStreak n a ≥ t)) ≤ fintypeExpect (fun a : CoinFlip n => Finset.sum (Finset.range n) (λ i => indicator (∀ j ∈ Finset.range t, headAt n a (i + j) = (1 : Fin 2)))) := fintypeExpect_mono h_nonneg_ind h_nonneg_sum h_union_bound _ ≤ (n : ℝ) / ((2 : ℝ) ^ t) := h_expect_bound · have : ∀ a : CoinFlip n, ¬ (longestStreak n a ≥ t) := by intro a rw [longestStreak_ge_iff_hasRunOfLength n t a] intro hrun rcases hrun with ⟨hle, _⟩ omega have h_zero : fintypeExpect (fun (a : CoinFlip n) => indicator (longestStreak n a ≥ t)) = 0 := by have h_sum_zero : (∑ a : CoinFlip n, indicator (longestStreak n a ≥ t)) = 0 := by apply Finset.sum_eq_zero intro a ha have h_not : ¬ (longestStreak n a ≥ t) := this a simp [indicator, h_not] unfold fintypeExpect rw [h_sum_zero, zero_div] rw [h_zero] have hn_nonneg : 0 ≤ (n : ℝ) := Nat.cast_nonneg _ positivity

Expected longest streak

The expected longest streak of heads satisfies E[L] = Θ(log n). The upper bound O(log n) follows from the tail bound longestStreak_upperBound via the layer-cake identity E[L] = Σ_{t≥1} Pr[L ≥ t] (expectedLongestStreak_le); the matching lower bound Ω(log n) is proved below with a block-partition argument: the m = ⌊n/k⌋ disjoint blocks of size k = ⌊log₂ n / 2⌋ are independent, so the exact count prob_noFullHeadBlock gives Pr[L ≥ k] ≥ 1 - (1 - 2^{-k})^m ≥ 1/2, and the layer-cake lower bound expectedLongestStreak_ge_mul_tail yields E[L] ≥ k/2 ≥ (log₂ n - 2)/4 ≥ log₂ n / 8 (expectedLongestStreak_lowerBound).

Expected value of the longest streak of heads in n independent fair coin flips.

noncomputable def expectedLongestStreak (n : ℕ) : ℝ := fintypeExpect (fun a : CoinFlip n => (longestStreak n a : ℝ))

The longest streak of heads never exceeds the number n of flips: a run of n + 1 heads would require n + 1 ≤ n positions.

`push_neg` has been deprecated. Prefer using `push Not` instead. If you'd rather continue using `push_neg` in your project, you can implement it as follows: ``` open Lean.Parser.Tactic in macro "push_neg" cfg:optConfig loc:(location)? : tactic => `(tactic| push $cfg:optConfig Not $[$loc]?) ``` lemma longestStreak_le (n : ℕ) (a : CoinFlip n) : longestStreak n a ≤ n := by by_contra h `push_neg` has been deprecated. Prefer using `push Not` instead. If you'd rather continue using `push_neg` in your project, you can implement it as follows: ``` open Lean.Parser.Tactic in macro "push_neg" cfg:optConfig loc:(location)? : tactic => `(tactic| push $cfg:optConfig Not $[$loc]?) ``` push_neg at h have hrun := (longestStreak_ge_iff_hasRunOfLength n (n + 1) a).mp h rcases hrun with ⟨hle, _⟩ omega

Pointwise layer-cake: every m ≤ B equals the number of thresholds t ∈ [1, B] that it reaches.

lemma natCast_eq_sum_ite_Icc (m B : ℕ) (hm : m ≤ B) : (m : ℝ) = ∑ t ∈ Finset.Icc 1 B, (if m ≥ t then (1 : ℝ) else 0) := by have hfilter : (Finset.Icc 1 B).filter (fun t => m ≥ t) = Finset.Icc 1 m := by ext t simp only [Finset.mem_filter, Finset.mem_Icc] constructor · rintro ⟨⟨h1t, -⟩, htm⟩ exact ⟨h1t, htm⟩ · rintro ⟨h1t, htm⟩ exact ⟨⟨h1t, by omega⟩, htm⟩ rw [← Finset.sum_filter, hfilter, Finset.sum_const, Nat.card_Icc, nsmul_eq_mul] simp

The expected longest streak equals the sum of the tail probabilities Pr[L ≥ t] over t = 1, …, n (the layer-cake / tail-sum formula for the ℕ-valued random variable longestStreak n, which is bounded by n).

lemma expectedLongestStreak_eq_tailSum (n : ℕ) : expectedLongestStreak n = ∑ t ∈ Finset.Icc 1 n, fintypeExpect (fun a : CoinFlip n => indicator (longestStreak n a ≥ t)) := by have hpoint : ∀ a : CoinFlip n, (longestStreak n a : ℝ) = ∑ t ∈ Finset.Icc 1 n, indicator (longestStreak n a ≥ t) := by intro a show (longestStreak n a : ℝ) = ∑ t ∈ Finset.Icc 1 n, (if longestStreak n a ≥ t then (1 : ℝ) else 0) exact natCast_eq_sum_ite_Icc (longestStreak n a) n (longestStreak_le n a) unfold expectedLongestStreak rw [← fintypeExpect_sum (Finset.Icc 1 n) (fun t (a : CoinFlip n) => indicator (longestStreak n a ≥ t))] exact congrArg fintypeExpect (funext hpoint)

Expected longest streak upper bound (CLRS §5.4.3): the expected length of the longest run of heads in n independent fair coin flips is at most log₂ n + 2. The tail-sum formula expectedLongestStreak_eq_tailSum splits the thresholds at Nat.log 2 n + 1: thresholds below the split contribute at most 1 each, and thresholds above it are summable thanks to longestStreak_upperBound, whose geometric tail adds at most 1.

theorem expectedLongestStreak_le (n : ℕ) : expectedLongestStreak n ≤ Real.logb 2 n + 2 := by rcases Nat.eq_zero_or_pos n with rfl | hn · rw [expectedLongestStreak_eq_tailSum, Finset.Icc_eq_empty_of_lt (by norm_num : (0 : ℕ) < 1), Finset.sum_empty] simp [Real.logb_zero] · have hcard : Fintype.card (CoinFlip n) ≠ 0 := by haveI : Nonempty (CoinFlip n) := ⟨fun _ => (0 : Fin 2)⟩ exact Fintype.card_ne_zero -- Each tail probability is at most `1`, since an indicator is bounded by `1`. have hlow : ∀ t ∈ Finset.Icc 1 n, t ≤ Nat.log 2 n + 1 → fintypeExpect (fun a : CoinFlip n => indicator (longestStreak n a ≥ t)) ≤ 1 := by intro t _ _ have h0 : ∀ a : CoinFlip n, (0 : ℝ) ≤ indicator (longestStreak n a ≥ t) := by intro a; unfold indicator; split <;> norm_num have h1 : ∀ a : CoinFlip n, indicator (longestStreak n a ≥ t) ≤ 1 := by intro a; unfold indicator; split <;> norm_num have hle := fintypeExpect_mono h0 (fun _ => zero_le_one) h1 rwa [fintypeExpect_const hcard 1] at hle -- The partial geometric series `∑ k < m, 2⁻ᵏ` is bounded by `2`. have hgeo : ∀ m : ℕ, ∑ k ∈ Finset.range m, (1 / 2 : ℝ) ^ k ≤ 2 := by intro m rw [geom_sum_eq (by norm_num : (1 / 2 : ℝ) ≠ 1)] have hpos1 : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ m := by positivity have heq : ((1 / 2 : ℝ) ^ m - 1) / ((1 / 2 : ℝ) - 1) = 2 * (1 - (1 / 2 : ℝ) ^ m) := by field_simp ring rw [heq] linarith -- The geometric tail past the split point is at most `2^{-(Nat.log 2 n + 1)}`. have htail : ∑ t ∈ Finset.Ioc (Nat.log 2 n + 1) n, (1 / 2 : ℝ) ^ t ≤ (1 / 2 : ℝ) ^ (Nat.log 2 n + 1) := by have hset : Finset.Ioc (Nat.log 2 n + 1) n = Finset.Ico (Nat.log 2 n + 1 + 1) (n + 1) := by ext t simp only [Finset.mem_Ioc, Finset.mem_Ico] omega rw [hset, Finset.sum_Ico_eq_sum_range] have hterm : ∀ i : ℕ, (1 / 2 : ℝ) ^ (Nat.log 2 n + 1 + 1 + i) = (1 / 2 : ℝ) ^ (Nat.log 2 n + 1 + 1) * (1 / 2 : ℝ) ^ i := fun i => pow_add _ _ _ rw [Finset.sum_congr rfl (fun i _ => hterm i), ← Finset.mul_sum] calc (1 / 2 : ℝ) ^ (Nat.log 2 n + 1 + 1) * ∑ i ∈ Finset.range (n + 1 - (Nat.log 2 n + 1 + 1)), (1 / 2 : ℝ) ^ i ≤ (1 / 2 : ℝ) ^ (Nat.log 2 n + 1 + 1) * 2 := mul_le_mul_of_nonneg_left (hgeo _) (by positivity) _ = (1 / 2 : ℝ) ^ (Nat.log 2 n + 1) := by rw [pow_succ]; ring -- Thresholds below the split contribute at most `Nat.log 2 n + 1` in total. have hsumlow : ∑ t ∈ (Finset.Icc 1 n).filter (fun t => t ≤ Nat.log 2 n + 1), fintypeExpect (fun a : CoinFlip n => indicator (longestStreak n a ≥ t)) ≤ (Nat.log 2 n + 1 : ℝ) := by have hsub : (Finset.Icc 1 n).filter (fun t => t ≤ Nat.log 2 n + 1) ⊆ Finset.Icc 1 (Nat.log 2 n + 1) := by intro t ht rw [Finset.mem_filter, Finset.mem_Icc] at ht rw [Finset.mem_Icc] exact ⟨ht.1.1, ht.2⟩ calc ∑ t ∈ (Finset.Icc 1 n).filter (fun t => t ≤ Nat.log 2 n + 1), fintypeExpect (fun a : CoinFlip n => indicator (longestStreak n a ≥ t)) ≤ ∑ t ∈ (Finset.Icc 1 n).filter (fun t => t ≤ Nat.log 2 n + 1), (1 : ℝ) := by refine Finset.sum_le_sum (fun t ht => hlow t (Finset.mem_of_mem_filter t ht) (Finset.mem_filter.mp ht).2) _ = (((Finset.Icc 1 n).filter (fun t => t ≤ Nat.log 2 n + 1)).card : ℝ) := by rw [Finset.sum_const, nsmul_eq_mul, mul_one] _ ≤ (Nat.log 2 n + 1 : ℝ) := by have hcardle : ((Finset.Icc 1 n).filter (fun t => t ≤ Nat.log 2 n + 1)).card ≤ Nat.log 2 n + 1 := by calc _ ≤ (Finset.Icc 1 (Nat.log 2 n + 1)).card := Finset.card_le_card hsub _ = Nat.log 2 n + 1 := by simp exact_mod_cast hcardle -- Thresholds above the split contribute at most `1`, by the union bound -- `longestStreak_upperBound` and the geometric tail `htail`. have hsumhigh : ∑ t ∈ (Finset.Icc 1 n).filter (fun t => ¬ t ≤ Nat.log 2 n + 1), fintypeExpect (fun a : CoinFlip n => indicator (longestStreak n a ≥ t)) ≤ 1 := by have hsub : (Finset.Icc 1 n).filter (fun t => ¬ t ≤ Nat.log 2 n + 1) ⊆ Finset.Ioc (Nat.log 2 n + 1) n := by intro t ht rw [Finset.mem_filter, Finset.mem_Icc] at ht rw [Finset.mem_Ioc] exact ⟨Nat.lt_of_not_le ht.2, ht.1.2⟩ have hn2 : (n : ℝ) ≤ (2 : ℝ) ^ (Nat.log 2 n + 1) := by have h : n < 2 ^ (Nat.log 2 n + 1) := Nat.lt_pow_succ_log_self (by norm_num) n exact_mod_cast h.le calc ∑ t ∈ (Finset.Icc 1 n).filter (fun t => ¬ t ≤ Nat.log 2 n + 1), fintypeExpect (fun a : CoinFlip n => indicator (longestStreak n a ≥ t)) ≤ ∑ t ∈ (Finset.Icc 1 n).filter (fun t => ¬ t ≤ Nat.log 2 n + 1), (n : ℝ) / (2 : ℝ) ^ t := by refine Finset.sum_le_sum (fun t ht => ?_) have htmem := Finset.mem_Icc.mp (Finset.mem_of_mem_filter t ht) exact longestStreak_upperBound n t htmem.1 _ ≤ ∑ t ∈ Finset.Ioc (Nat.log 2 n + 1) n, (n : ℝ) / (2 : ℝ) ^ t := Finset.sum_le_sum_of_subset_of_nonneg hsub (fun t _ _ => by positivity) _ = (n : ℝ) * ∑ t ∈ Finset.Ioc (Nat.log 2 n + 1) n, (1 / 2 : ℝ) ^ t := by rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun t _ => ?_) rw [div_pow, one_pow, mul_one_div] _ ≤ (n : ℝ) * (1 / 2 : ℝ) ^ (Nat.log 2 n + 1) := mul_le_mul_of_nonneg_left htail (by positivity) _ ≤ 1 := by have hpos : (0 : ℝ) < (2 : ℝ) ^ (Nat.log 2 n + 1) := by positivity rw [one_div, inv_pow, ← div_eq_mul_inv, div_le_one hpos] exact hn2 -- `Nat.log 2 n + 1 ≤ log₂ n + 1`, by monotonicity of `Real.logb`. have hlog : (Nat.log 2 n + 1 : ℝ) ≤ Real.logb 2 n + 1 := by have h2le : (2 : ℝ) ^ Nat.log 2 n ≤ (n : ℝ) := by exact_mod_cast Nat.pow_log_le_self 2 hn.ne' have hmono := Real.logb_le_logb_of_le (by norm_num : (1 : ℝ) < 2) (by positivity : (0 : ℝ) < (2 : ℝ) ^ Nat.log 2 n) h2le rw [Real.logb_pow, Real.logb_self_eq_one (by norm_num : (1 : ℝ) < 2), mul_one] at hmono linarith rw [expectedLongestStreak_eq_tailSum, ← Finset.sum_filter_add_sum_filter_not (Finset.Icc 1 n) (fun t => t ≤ Nat.log 2 n + 1) (fun t => fintypeExpect (fun a : CoinFlip n => indicator (longestStreak n a ≥ t)))] linarith [hsumlow, hsumhigh, hlog]

Expected longest streak: lower bound (block partition)

The lower bound E[L] ≥ c · log₂ n uses the standard block-partition argument. Fix a block size k and let m = ⌊n/k⌋. The m disjoint blocks of k consecutive positions are independent; a block is full if all its positions are heads. The exact count of sequences with no full block is (2^k - 1)^m · 2^(n - m·k) (card_noFullHeadBlock), witnessed by the bijection noFullHeadBlockBijection that decomposes a sequence into its m block restrictions plus a free tail. Hence Pr[no full block] = (1 - 2^{-k})^m (prob_noFullHeadBlock). Since a full block is a run of k heads, Pr[L < k] ≤ (1 - 2^{-k})^m (prob_longestStreak_lt_le), so Pr[L ≥ k] ≥ 1 - (1 - 2^{-k})^m. The Bernoulli bound (1 - 2^{-k})^m ≤ 1/(1 + m·2^{-k}) (one_sub_pow_le_inv_one_add_mul) gives Pr[L ≥ k] ≥ m·2^{-k}/(1 + m·2^{-k}) (prob_longestStreak_ge_mul), and the layer-cake identity lower bound E[L] ≥ k · Pr[L ≥ k] (expectedLongestStreak_ge_mul_tail).

Choosing k = ⌊log₂ n / 2⌋ and m = ⌊n/k⌋, the estimates m ≥ 2^k and 2^k·(k+1) ≤ n show m·2^{-k} ≥ 1, hence Pr[L ≥ k] ≥ 1/2 and E[L] ≥ k/2. With k ≥ (log₂ n - 2)/2, this yields E[L] ≥ (log₂ n - 2)/4 ≥ log₂ n / 8 for n ≥ 16 (expectedLongestStreak_lowerBound).

A block of k consecutive flips, viewed as a standalone sequence, is all heads.

def blockAllHeads (k : ℕ) (w : Fin k → Fin 2) : Prop := ∀ r : Fin k, w r = (1 : Fin 2)
instance (k : ℕ) (w : Fin k → Fin 2) : Decidable (blockAllHeads k w) := by unfold blockAllHeads; infer_instance

Restriction of a sequence to the block of k consecutive positions starting at j * k.

def blockRestriction (n k j : ℕ) (a : CoinFlip n) : Fin k → Fin 2 := fun r => headAt n a (j * k + r.val)

The block of k consecutive positions starting at j * k is all heads.

def blockIsAllHeads (n k j : ℕ) (a : CoinFlip n) : Prop := blockAllHeads k (blockRestriction n k j a)

Among the first m blocks of size k (positions 0..m*k-1), none is all heads.

def noFullHeadBlock (n k m : ℕ) (a : CoinFlip n) : Prop := ∀ j : Fin m, ¬ blockIsAllHeads n k j.val a
instance (n k m : ℕ) (a : CoinFlip n) : Decidable (noFullHeadBlock n k m a) := by unfold noFullHeadBlock blockIsAllHeads blockRestriction headAt infer_instance

A full block inside the first m*k positions gives a run of k heads.

lemma blockIsAllHeads_hasRunOfLength (n k j : ℕ) (a : CoinFlip n) (hj : j * k + k ≤ n) : blockIsAllHeads n k j a → hasRunOfLength n k a := by intro hblock refine ⟨by omega, j * k, ?_, ?_, ?_⟩ · exact Finset.mem_range.mpr (by omega) · simpa using hj · intro t ht exact hblock ⟨t, Finset.mem_range.mp ht⟩

If the longest streak is below k, then none of the first m blocks is full.

lemma noFullHeadBlock_of_lt (n k m : ℕ) (hmk : m * k ≤ n) (a : CoinFlip n) : longestStreak n a < k → noFullHeadBlock n k m a := by intro hl j hblock have hjm : j.val + 1 ≤ m := Nat.succ_le_of_lt j.isLt have hjmk : (j.val + 1) * k ≤ m * k := Nat.mul_le_mul_right k hjm have hcalc : j.val * k + k ≤ m * k := by simpa [Nat.succ_mul] using hjmk have hjk : j.val * k + k ≤ n := le_trans hcalc hmk have hrun := blockIsAllHeads_hasRunOfLength n k j.val a hjk hblock have hge : longestStreak n a ≥ k := (longestStreak_ge_iff_hasRunOfLength n k a).mpr hrun omega

The number of non-all-heads block sequences of length k is 2^k - 1.

lemma card_notBlockAllHeads (k : ℕ) : Fintype.card {w : Fin k → Fin 2 // ¬ blockAllHeads k w} = 2 ^ k - 1 := by classical let constOne : Fin k → Fin 2 := fun _ => (1 : Fin 2) have hcard_all : Fintype.card {w : Fin k → Fin 2 // blockAllHeads k w} = 1 := by have hbio : {w : Fin k → Fin 2 // blockAllHeads k w} ≃ {w : Fin k → Fin 2 // w = constOne} := { toFun := fun w => ⟨w.1, by funext r change w.1 r = (1 : Fin 2) exact w.2 r⟩ invFun := fun w => ⟨w.1, by intro r have h := congrFun w.2 r change w.1 r = (1 : Fin 2) simpa [constOne] using h⟩ left_inv := fun w => rfl right_inv := fun w => rfl } rw [Fintype.card_congr hbio] simp calc Fintype.card {w : Fin k → Fin 2 // ¬ blockAllHeads k w} = Fintype.card (Fin k → Fin 2) - Fintype.card {w : Fin k → Fin 2 // blockAllHeads k w} := by rw [Fintype.card_subtype_compl (fun w : Fin k → Fin 2 => blockAllHeads k w)] _ = 2 ^ k - 1 := by simp [hcard_all]

The tuple of the first m block restrictions of a sequence.

def blocksOf (n k m : ℕ) (a : CoinFlip n) : Π Variable name `j` 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`j : Fin m, Fin k → Fin 2 := fun j => blockRestriction n k j.val a

The restriction of a sequence to the free tail positions m*k, ..., n-1.

def freeOf (n k m : ℕ) (a : CoinFlip n) : Fin (n - m * k) → Fin 2 := fun t => headAt n a (m * k + t.val)

Reconstruct a full sequence from the m block restrictions and the free tail.

def reconstructBlocks (n k m : ℕ) (hk : 0 < k) (hmk : m * k ≤ n) (w : Π Variable name `j` 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`j : Fin m, Fin k → Fin 2) (u : Fin (n - m * k) → Fin 2) : CoinFlip n := fun x : Fin n => if hx : x.val < m * k then (w ⟨x.val / k, by exact (Nat.div_lt_iff_lt_mul hk).mpr hx⟩) ⟨x.val % k, by exact Nat.mod_lt x.val hk⟩ else u ⟨x.val - m * k, by omega⟩

On a position inside block j, the reconstruction returns the block's own value.

lemma reconstruct_in_block (n k m : ℕ) (hk : 0 < k) (hmk : m * k ≤ n) (w : Π Variable name `j` 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`j : Fin m, Fin k → Fin 2) (u : Fin (n - m * k) → Fin 2) (j : Fin m) (r : Fin k) (h : j.val * k + r.val < n) : headAt n (reconstructBlocks n k m hk hmk w u) (j.val * k + r.val) = w j r := by rw [headAt_eq_of_lt n (reconstructBlocks n k m hk hmk w u) (j.val * k + r.val) h] have hxlt : j.val * k + r.val < m * k := by have hjm : j.val + 1 ≤ m := Nat.succ_le_of_lt j.isLt have hjmk : (j.val + 1) * k ≤ m * k := Nat.mul_le_mul_right k hjm have hcalc : j.val * k + k ≤ m * k := by simpa [Nat.succ_mul] using hjmk omega have hdiv : (j.val * k + r.val) / k = j.val := by calc (j.val * k + r.val) / k = (r.val + j.val * k) / k := by rw [Nat.add_comm] _ = r.val / k + j.val := Nat.add_mul_div_right r.val j.val hk _ = j.val := by rw [Nat.div_eq_of_lt r.isLt]; simp have hmod : (j.val * k + r.val) % k = r.val := Nat.mul_add_mod_of_lt r.isLt have hf_j : (⟨(j.val * k + r.val) / k, by exact (Nat.div_lt_iff_lt_mul hk).mpr hxlt⟩ : Fin m) = j := by apply Fin.ext change (j.val * k + r.val) / k = j.val rw [hdiv] have hf_r : (⟨(j.val * k + r.val) % k, by exact Nat.mod_lt (j.val * k + r.val) hk⟩ : Fin k) = r := by apply Fin.ext change (j.val * k + r.val) % k = r.val rw [hmod] unfold reconstructBlocks simp [hxlt, hf_j, This simp argument is unused: hf_r Hint: Omit it from the simp argument list. simp [hxlt, hf_j, h̵f̵_̵r̵,̵ ̵Nat.mod_eq_of_lt r.isLt] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hf_r, Nat.mod_eq_of_lt r.isLt]

On a free position, the reconstruction returns the free tail's own value.

lemma reconstruct_out_block (n k m : ℕ) (hk : 0 < k) (hmk : m * k ≤ n) (w : Π Variable name `j` 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`j : Fin m, Fin k → Fin 2) (u : Fin (n - m * k) → Fin 2) (t : Fin (n - m * k)) (h : m * k + t.val < n) : headAt n (reconstructBlocks n k m hk hmk w u) (m * k + t.val) = u t := by rw [headAt_eq_of_lt n (reconstructBlocks n k m hk hmk w u) (m * k + t.val) h] have hge : m * k ≤ m * k + t.val := by omega have hsub : m * k + t.val - m * k = t.val := by omega have hf_t : (⟨t.val, by omega⟩ : Fin (n - m * k)) = t := by apply Fin.ext; rfl simp [reconstructBlocks, This simp argument is unused: hge Hint: Omit it from the simp argument list. simp [reconstructBlocks, hg̵e̵,̵ ̵h̵sub, hf_t] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hge, hsub, hf_t]

Bijection between sequences with no full block among the first m blocks and tuples of m non-all-heads blocks plus a free tail. This is the product decomposition witnessing independence of the m disjoint blocks.

noncomputable def noFullHeadBlockBijection (n k m : ℕ) (hk : 0 < k) (hmk : m * k ≤ n) : {a : CoinFlip n // noFullHeadBlock n k m a} ≃ (Π Variable name `j` 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`j : Fin m, {w : Fin k → Fin 2 // ¬ blockAllHeads k w}) × (Fin (n - m * k) → Fin 2) where toFun a := ( (fun j : Fin m => ⟨blockRestriction n k j.val a.1, a.2 j⟩), (fun t : Fin (n - m * k) => headAt n a.1 (m * k + t.val)) ) invFun wu := ⟨ reconstructBlocks n k m hk hmk (fun j => (wu.1 j).1) wu.2, by intro j hblock have hw : blockAllHeads k (wu.1 j).1 := by intro r have hr := hblock r have hxlt' : j.val * k + r.val < n := by have hjm : j.val + 1 ≤ m := Nat.succ_le_of_lt j.isLt have hjmk : (j.val + 1) * k ≤ m * k := Nat.mul_le_mul_right k hjm have hcalc : j.val * k + k ≤ m * k := by simpa [Nat.succ_mul] using hjmk omega rw [blockRestriction] at hr rw [reconstruct_in_block n k m hk hmk (fun j => (wu.1 j).1) wu.2 j r hxlt'] at hr exact hr exact (wu.1 j).2 hw ⟩ left_inv := by intro a apply Subtype.ext funext x by_cases hx : x.val < m * k · have hdiv : (x.val / k) * k + x.val % k = x.val := Nat.div_add_mod' x.val k have hxval : x.val / k < m := by exact (Nat.div_lt_iff_lt_mul hk).mpr hx have hmod : x.val % k < k := Nat.mod_lt x.val hk calc reconstructBlocks n k m hk hmk (blocksOf n k m a.1) (freeOf n k m a.1) x = (blocksOf n k m a.1) ⟨x.val / k, hxval⟩ ⟨x.val % k, hmod⟩ := by simp [reconstructBlocks, hx] _ = blockRestriction n k (x.val / k) a.1 ⟨x.val % k, hmod⟩ := by rfl _ = headAt n a.1 ((x.val / k) * k + (x.val % k)) := by rfl _ = headAt n a.1 (x.val) := by rw [hdiv] _ = a.1 x := by rw [headAt_eq_of_lt n a.1 x.val x.isLt] · have hge : m * k ≤ x.val := Nat.le_of_not_gt hx calc reconstructBlocks n k m hk hmk (blocksOf n k m a.1) (freeOf n k m a.1) x = (freeOf n k m a.1) ⟨x.val - m * k, by omega⟩ := by simp [reconstructBlocks, hx] _ = headAt n a.1 (m * k + (x.val - m * k)) := by rfl _ = headAt n a.1 (x.val) := by rw [Nat.add_sub_of_le hge] _ = a.1 x := by rw [headAt_eq_of_lt n a.1 x.val x.isLt] right_inv := by intro wu apply Prod.ext · funext j apply Subtype.ext funext r have hxlt' : j.val * k + r.val < n := by have hjm : j.val + 1 ≤ m := Nat.succ_le_of_lt j.isLt have hjmk : (j.val + 1) * k ≤ m * k := Nat.mul_le_mul_right k hjm have hcalc : j.val * k + k ≤ m * k := by simpa [Nat.succ_mul] using hjmk omega calc blockRestriction n k j.val (reconstructBlocks n k m hk hmk (fun j => (wu.1 j).1) wu.2) r = headAt n (reconstructBlocks n k m hk hmk (fun j => (wu.1 j).1) wu.2) (j.val * k + r.val) := rfl _ = (fun j => (wu.1 j).1) j r := reconstruct_in_block n k m hk hmk (fun j => (wu.1 j).1) wu.2 j r hxlt' _ = (wu.1 j).1 r := rfl · funext t have hxlt' : m * k + t.val < n := by have ht : t.val < n - m * k := t.isLt omega calc headAt n (reconstructBlocks n k m hk hmk (fun j => (wu.1 j).1) wu.2) (m * k + t.val) = wu.2 t := reconstruct_out_block n k m hk hmk (fun j => (wu.1 j).1) wu.2 t hxlt'

The number of sequences with no full block among the first m blocks is (2^k - 1)^m · 2^(n - m*k).

lemma card_noFullHeadBlock (n k m : ℕ) (hk : 0 < k) (hmk : m * k ≤ n) : Fintype.card {a : CoinFlip n // noFullHeadBlock n k m a} = (2 ^ k - 1) ^ m * 2 ^ (n - m * k) := by calc Fintype.card {a : CoinFlip n // noFullHeadBlock n k m a} = Fintype.card ((Π j : Fin m, {w : Fin k → Fin 2 // ¬ blockAllHeads k w}) × (Fin (n - m * k) → Fin 2)) := Fintype.card_congr (noFullHeadBlockBijection n k m hk hmk) _ = Fintype.card (Π j : Fin m, {w : Fin k → Fin 2 // ¬ blockAllHeads k w}) * Fintype.card (Fin (n - m * k) → Fin 2) := by simp _ = (∏ j : Fin m, Fintype.card {w : Fin k → Fin 2 // ¬ blockAllHeads k w}) * Fintype.card (Fin (n - m * k) → Fin 2) := by rw [Fintype.card_pi] _ = (2 ^ k - 1) ^ m * 2 ^ (n - m * k) := by have hprod : (∏ j : Fin m, Fintype.card {w : Fin k → Fin 2 // ¬ blockAllHeads k w}) = (2 ^ k - 1) ^ m := by rw [Finset.prod_const, card_notBlockAllHeads k] simp rw [hprod] simp [This simp argument is unused: Fintype.card_fun Hint: Omit it from the simp argument list. simp ̵[̵F̵i̵n̵t̵y̵p̵e̵.̵c̵a̵r̵d̵_̵f̵u̵n̵]̵ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Fintype.card_fun]

Bernoulli-type bound: for 0 ≤ x ≤ 1, (1 - x)^m ≤ 1 / (1 + m·x).

lemma one_sub_pow_le_inv_one_add_mul {m : ℕ} {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : (1 - x) ^ m ≤ (1 + (m : ℝ) * x)⁻¹ := by have hx_pos : (0 : ℝ) < 1 + x := by nlinarith have hle1 : 1 - x ≤ (1 + x)⁻¹ := by have hdiv : 1 - x ≤ 1 / (1 + x) := by rw [le_div_iff₀ hx_pos] nlinarith [sq_nonneg x] simpa using hdiv have hle2 : (1 - x) ^ m ≤ (1 + x)⁻¹ ^ m := by exact pow_le_pow_left₀ (by linarith : 0 ≤ 1 - x) hle1 m have hbern : 1 + (m : ℝ) * x ≤ (1 + x) ^ m := by exact one_add_mul_le_pow (by nlinarith : -2 ≤ x) m have hpos : (0 : ℝ) < (1 + x) ^ m := by positivity have hpos2 : (0 : ℝ) < 1 + (m : ℝ) * x := by nlinarith calc (1 - x) ^ m ≤ (1 + x)⁻¹ ^ m := hle2 _ = ((1 + x) ^ m)⁻¹ := by rw [← inv_pow] _ ≤ (1 + (m : ℝ) * x)⁻¹ := by rw [inv_le_inv₀ hpos hpos2] exact hbern

If x ≥ 1, then x/(1+x) ≥ 1/2.

lemma half_le_self_div_one_add_self {x : ℝ} (hx : 1 ≤ x) : (1 / 2 : ℝ) ≤ x / (1 + x) := by have hpos : (0 : ℝ) < 1 + x := by linarith have hnum : (1 / 2 : ℝ) * (1 + x) ≤ x := by nlinarith exact (le_div_iff₀ hpos).mpr hnum

The probability that no full block appears among the first m blocks of size k (within n flips) is exactly (1 - 2^{-k})^m.

lemma prob_noFullHeadBlock (n k m : ℕ) (hk : 0 < k) (hmk : m * k ≤ n) : fintypeExpect (fun a : CoinFlip n => indicator (noFullHeadBlock n k m a)) = (1 - 1 / (2 : ℝ) ^ k) ^ m := by have htotal : (Fintype.card (CoinFlip n) : ℝ) = (2 : ℝ) ^ n := by have h_nat : Fintype.card (CoinFlip n) = 2 ^ n := by calc Fintype.card (CoinFlip n) = Fintype.card (Fin n → Fin 2) := rfl _ = (Fintype.card (Fin 2)) ^ (Fintype.card (Fin n)) := by rw [Fintype.card_fun] _ = 2 ^ n := by simp rw [h_nat]; simp have hcard := card_noFullHeadBlock n k m hk hmk have hcardsub : (Fintype.card {a : CoinFlip n // noFullHeadBlock n k m a} : ℝ) = ((2 ^ k - 1) ^ m * 2 ^ (n - m * k) : ℕ) := by exact_mod_cast hcard calc fintypeExpect (fun a => indicator (noFullHeadBlock n k m a)) = (∑ a : CoinFlip n, indicator (noFullHeadBlock n k m a)) / (Fintype.card (CoinFlip n) : ℝ) := rfl _ = ((Fintype.card {a : CoinFlip n // noFullHeadBlock n k m a} : ℝ)) / (Fintype.card (CoinFlip n) : ℝ) := by simp [indicator, Fintype.card_subtype] _ = ((2 ^ k - 1) ^ m * 2 ^ (n - m * k) : ℕ) / ((2 : ℝ) ^ n) := by rw [hcardsub, htotal] _ = (1 - 1 / (2 : ℝ) ^ k) ^ m := by have hnat : (((2 ^ k - 1) ^ m * 2 ^ (n - m * k) : ℕ) : ℝ) = ((2 : ℝ) ^ k - 1) ^ m * (2 : ℝ) ^ (n - m * k) := by norm_num rw [hnat] have hpow : (2 : ℝ) ^ n = (2 : ℝ) ^ (m * k) * (2 : ℝ) ^ (n - m * k) := by rw [← pow_add, Nat.add_sub_of_le hmk] rw [hpow] have hmain : (1 - 1 / (2 : ℝ) ^ k) ^ m = (((2 : ℝ) ^ k - 1) / (2 : ℝ) ^ k) ^ m := by congr 1 field_simp rw [hmain] rw [show (2 : ℝ) ^ (m * k) = ((2 : ℝ) ^ k) ^ m by rw [mul_comm, pow_mul]] field_simp rw [div_pow] field_simp

If the longest streak is below k, the indicator of L < k is bounded by the indicator that no full block occurs.

lemma prob_longestStreak_lt_le (n k m : ℕ) (hk : 0 < k) (hmk : m * k ≤ n) : fintypeExpect (fun a => indicator (longestStreak n a < k)) ≤ (1 - 1 / (2 : ℝ) ^ k) ^ m := by have hX : ∀ a : CoinFlip n, 0 ≤ indicator (longestStreak n a < k) := by intro a; unfold indicator; split <;> norm_num have hY : ∀ a : CoinFlip n, 0 ≤ indicator (noFullHeadBlock n k m a) := by intro a; unfold indicator; split <;> norm_num have hXY : ∀ a : CoinFlip n, indicator (longestStreak n a < k) ≤ indicator (noFullHeadBlock n k m a) := by intro a by_cases hL : longestStreak n a < k · have hnf : noFullHeadBlock n k m a := noFullHeadBlock_of_lt n k m hmk a hL simp [indicator, hL, hnf] · simp [indicator, hL] split <;> norm_num have hmono : fintypeExpect (fun a => indicator (longestStreak n a < k)) ≤ fintypeExpect (fun a => indicator (noFullHeadBlock n k m a)) := fintypeExpect_mono hX hY hXY rwa [prob_noFullHeadBlock n k m hk hmk] at hmono

The tail probability Pr[L ≥ k] is at least 1 - (1 - 2^{-k})^m.

lemma prob_longestStreak_ge_lower (n k m : ℕ) (hk : 0 < k) (hmk : m * k ≤ n) : 1 - (1 - 1 / (2 : ℝ) ^ k) ^ m ≤ fintypeExpect (fun a => indicator (longestStreak n a ≥ k)) := by have hpoint : (fun a => indicator (longestStreak n a ≥ k)) = (fun a => 1 - indicator (longestStreak n a < k)) := by funext a by_cases h : longestStreak n a ≥ k · have hnot : ¬ longestStreak n a < k := by omega simp [indicator, h, hnot] · have hlt : longestStreak n a < k := by omega simp [indicator, h, hlt] have hcomp : fintypeExpect (fun a => indicator (longestStreak n a ≥ k)) = 1 - fintypeExpect (fun a => indicator (longestStreak n a < k)) := by rw [hpoint] unfold fintypeExpect rw [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_univ, nsmul_eq_mul] rw [sub_div] have hcard : (Fintype.card (CoinFlip n) : ℝ) ≠ 0 := by haveI : Nonempty (CoinFlip n) := ⟨fun _ => (0 : Fin 2)⟩ exact_mod_cast (Fintype.card_ne_zero) field_simp [hcard] rw [hcomp] linarith [prob_longestStreak_lt_le n k m hk hmk]

The tail probability Pr[L ≥ k] is at least m·2^{-k} / (1 + m·2^{-k}).

lemma prob_longestStreak_ge_mul (n k m : ℕ) (hk : 0 < k) (hmk : m * k ≤ n) : (m : ℝ) * (1 / (2 : ℝ) ^ k) / (1 + (m : ℝ) * (1 / (2 : ℝ) ^ k)) ≤ fintypeExpect (fun a => indicator (longestStreak n a ≥ k)) := by let x : ℝ := 1 / (2 : ℝ) ^ k have hx0 : 0 ≤ x := by unfold x; positivity have hx1 : x ≤ 1 := by unfold x rw [one_div] have h2 : (1 : ℝ) ≤ (2 : ℝ) ^ k := by simpa using (pow_le_pow_left₀ (by norm_num : 0 ≤ (1 : ℝ)) (by norm_num : (1 : ℝ) ≤ (2 : ℝ)) k) exact inv_le_one_of_one_le₀ h2 have hbern : (1 - x) ^ m ≤ (1 + (m : ℝ) * x)⁻¹ := one_sub_pow_le_inv_one_add_mul hx0 hx1 have hlow : 1 - (1 - x) ^ m ≥ (m : ℝ) * x / (1 + (m : ℝ) * x) := by have hden : (0 : ℝ) < 1 + (m : ℝ) * x := by positivity have hcomp : 1 - (1 + (m : ℝ) * x)⁻¹ = (m : ℝ) * x / (1 + (m : ℝ) * x) := by field_simp [hden.ne'] ring rw [← hcomp] linarith unfold x at hlow linarith [prob_longestStreak_ge_lower n k m hk hmk, hlow]

Tail probabilities Pr[L ≥ t] are monotone in the threshold.

lemma tailProb_mono (n k t : ℕ) (htk : t ≤ k) : fintypeExpect (fun a => indicator (longestStreak n a ≥ k)) ≤ fintypeExpect (fun a => indicator (longestStreak n a ≥ t)) := by have hX : ∀ a : CoinFlip n, 0 ≤ indicator (longestStreak n a ≥ k) := by intro a; unfold indicator; split <;> norm_num have hY : ∀ a : CoinFlip n, 0 ≤ indicator (longestStreak n a ≥ t) := by intro a; unfold indicator; split <;> norm_num have hXY : ∀ a : CoinFlip n, indicator (longestStreak n a ≥ k) ≤ indicator (longestStreak n a ≥ t) := by intro a by_cases hk : longestStreak n a ≥ k · have ht : longestStreak n a ≥ t := le_trans htk hk simp [indicator, hk, ht] · simp [indicator, hk] split <;> norm_num exact fintypeExpect_mono hX hY hXY

The layer-cake identity lower bound: E[L] ≥ k · Pr[L ≥ k].

lemma expectedLongestStreak_ge_mul_tail (n k : ℕ) (Variable name `hk` 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`hk : 0 < k) (hkn : k ≤ n) : (k : ℝ) * fintypeExpect (fun a => indicator (longestStreak n a ≥ k)) ≤ expectedLongestStreak n := by rw [expectedLongestStreak_eq_tailSum] have hsum_le : (k : ℝ) * fintypeExpect (fun a => indicator (longestStreak n a ≥ k)) ≤ ∑ t ∈ Finset.Icc 1 k, fintypeExpect (fun a => indicator (longestStreak n a ≥ t)) := by calc (k : ℝ) * fintypeExpect (fun a => indicator (longestStreak n a ≥ k)) = ∑ t ∈ Finset.Icc 1 k, fintypeExpect (fun a => indicator (longestStreak n a ≥ k)) := by simp [Finset.sum_const, nsmul_eq_mul] _ ≤ ∑ t ∈ Finset.Icc 1 k, fintypeExpect (fun a => indicator (longestStreak n a ≥ t)) := by refine Finset.sum_le_sum (fun t ht => tailProb_mono n k t (Finset.mem_Icc.mp ht).2) have hsubset : ∑ t ∈ Finset.Icc 1 k, fintypeExpect (fun a => indicator (longestStreak n a ≥ t)) ≤ ∑ t ∈ Finset.Icc 1 n, fintypeExpect (fun a => indicator (longestStreak n a ≥ t)) := by exact Finset.sum_le_sum_of_subset_of_nonneg (Finset.Icc_subset_Icc_right (by omega : k ≤ n)) (fun t _ _ => fintypeExpect_nonneg (fun a => by unfold indicator; split <;> norm_num)) linarith

Expected longest streak lower bound (CLRS §5.4.3): for n ≥ 16 flips the expected longest run of heads is at least log₂ n / 8. With k = ⌊log₂ n / 2⌋ and m = ⌊n / k⌋, the m disjoint blocks of size k give Pr[L ≥ k] ≥ 1/2 (via the exact count (1 - 2^{-k})^m), and the layer-cake lower bound E[L] ≥ k·Pr[L ≥ k] yields E[L] ≥ k/2 ≥ (log₂ n - 2)/4 ≥ log₂ n / 8.

theorem expectedLongestStreak_lowerBound (n : ℕ) (hn : 16 ≤ n) : Real.logb 2 n / 8 ≤ expectedLongestStreak n := by let k : ℕ := Nat.log 2 n / 2 let m : ℕ := n / k let ℓ : ℝ := Real.logb 2 n have hL2ge : 4 ≤ Nat.log 2 n := by have hmono := Nat.log_mono_right (b := 2) (by omega : 16 ≤ n) norm_num at hmono exact hmono have h1le_L2 : 1 ≤ Nat.log 2 n := by omega have hL2le : (Nat.log 2 n : ℝ) ≤ ℓ := by have hpow_n : (2 : ℝ) ^ Nat.log 2 n ≤ (n : ℝ) := by exact_mod_cast (Nat.pow_log_le_self 2 (by omega : n ≠ 0)) have hmono := Real.logb_le_logb_of_le (by norm_num : (1 : ℝ) < 2) (by positivity : (0 : ℝ) < (2 : ℝ) ^ Nat.log 2 n) hpow_n simpa [ℓ, Real.logb_pow, Real.logb_self_eq_one] using hmono have hlt : ℓ - 1 < (Nat.log 2 n : ℝ) := by have hlt_nat : n < 2 ^ (Nat.log 2 n + 1) := Nat.lt_pow_succ_log_self (by norm_num : 1 < 2) n have hmono := Real.logb_lt_logb (by norm_num : (1 : ℝ) < 2) (by positivity : (0 : ℝ) < (n : ℝ)) (by exact_mod_cast hlt_nat : (n : ℝ) < (2 : ℝ) ^ (Nat.log 2 n + 1)) have hrhs : Real.logb 2 (2 ^ (Nat.log 2 n + 1)) = (Nat.log 2 n + 1 : ℝ) := by simp [Real.logb_pow, Real.logb_self_eq_one] rw [hrhs] at hmono linarith have hk : 0 < k := by have : 0 < Nat.log 2 n / 2 := by omega simpa [k] using this have hkn : k ≤ n := by have hL2lt : Nat.log 2 n < n := by have h1 : Nat.log 2 n < 2 ^ Nat.log 2 n := Nat.lt_two_pow_self exact lt_of_lt_of_le h1 (Nat.pow_log_le_self 2 (by omega : n ≠ 0)) have hk_le_L2 : k ≤ Nat.log 2 n := by have : Nat.log 2 n / 2 ≤ Nat.log 2 n := by omega simpa [k] using this omega have hmk : m * k ≤ n := by have : n / k * k ≤ n := Nat.div_mul_le_self n k simpa [m] using this have h2k_le_L2 : 2 * k ≤ Nat.log 2 n := by have : 2 * (Nat.log 2 n / 2) ≤ Nat.log 2 n := by omega simpa [k] using this have hk2k : k * 2 ^ k ≤ n := by have hpow_le : (2 : ℕ) ^ (2 * k) ≤ 2 ^ Nat.log 2 n := Nat.pow_le_pow_right (by norm_num : 0 < 2) h2k_le_L2 have hpow_n : 2 ^ Nat.log 2 n ≤ n := Nat.pow_log_le_self 2 (by omega : n ≠ 0) have hle : 2 ^ (2 * k) ≤ n := le_trans hpow_le hpow_n have hk1 : k + 1 ≤ 2 ^ k := Nat.succ_le_of_lt Nat.lt_two_pow_self have hbound : k * 2 ^ k + k ≤ 2 ^ (2 * k) := by calc k * 2 ^ k + k ≤ k * 2 ^ k + 2 ^ k := by omega _ = (k + 1) * 2 ^ k := by ring _ ≤ 2 ^ k * 2 ^ k := Nat.mul_le_mul_right (2 ^ k) hk1 _ = 2 ^ (2 * k) := by rw [← pow_two, ← pow_mul, mul_comm] omega have hmge2k : 2 ^ k ≤ m := by have hle : k * 2 ^ k ≤ n := hk2k have hdiv : 2 ^ k ≤ n / k := by exact (Nat.le_div_iff_mul_le hk).mpr (by simpa [Nat.mul_comm] using hle) simpa [m] using hdiv have hP : (m : ℝ) * (1 / (2 : ℝ) ^ k) / (1 + (m : ℝ) * (1 / (2 : ℝ) ^ k)) ≤ fintypeExpect (fun a => indicator (longestStreak n a ≥ k)) := prob_longestStreak_ge_mul n k m hk hmk have hx : (1 : ℝ) ≤ (m : ℝ) * (1 / (2 : ℝ) ^ k) := by have hc : ((2 ^ k : ℕ) : ℝ) ≤ (m : ℝ) := by exact_mod_cast hmge2k have h2k_pos : (0 : ℝ) < (2 : ℝ) ^ k := by positivity calc (1 : ℝ) = ((2 ^ k : ℕ) : ℝ) / (2 : ℝ) ^ k := by simp _ ≤ (m : ℝ) / (2 : ℝ) ^ k := by exact div_le_div_of_nonneg_right hc (le_of_lt h2k_pos) _ = (m : ℝ) * (1 / (2 : ℝ) ^ k) := by ring have hP2 : (1 / 2 : ℝ) ≤ fintypeExpect (fun a => indicator (longestStreak n a ≥ k)) := by have hdiv : (1 / 2 : ℝ) ≤ (m : ℝ) * (1 / (2 : ℝ) ^ k) / (1 + (m : ℝ) * (1 / (2 : ℝ) ^ k)) := half_le_self_div_one_add_self hx linarith [hP, hdiv] have hE : (k : ℝ) / 2 ≤ expectedLongestStreak n := by have hmul : (k : ℝ) * (1 / 2 : ℝ) ≤ expectedLongestStreak n := by exact le_trans (mul_le_mul_of_nonneg_left hP2 (by positivity : 0 ≤ (k : ℝ))) (expectedLongestStreak_ge_mul_tail n k hk hkn) linarith have h2k_ge : Nat.log 2 n - 1 ≤ 2 * k := by have : Nat.log 2 n - 1 ≤ 2 * (Nat.log 2 n / 2) := by omega simpa [k] using this have hk_ge : (ℓ - 2) / 2 ≤ (k : ℝ) := by have hlt2 : ℓ - 2 < (2 * k : ℝ) := by have h1 : ℓ - 2 < (Nat.log 2 n : ℝ) - 1 := by linarith have h2 : (Nat.log 2 n : ℝ) - 1 ≤ (2 : ℝ) * (k : ℝ) := by have hcast : ((Nat.log 2 n - 1 : ℕ) : ℝ) ≤ ((2 * k : ℕ) : ℝ) := by exact_mod_cast h2k_ge have hsub : ((Nat.log 2 n - 1 : ℕ) : ℝ) = (Nat.log 2 n : ℝ) - 1 := by rw [Nat.cast_sub h1le_L2] norm_num rwa [hsub, Nat.cast_mul] at hcast linarith have hdiv : (ℓ - 2) / 2 < (k : ℝ) := by have h2pos : (0 : ℝ) < 2 := by norm_num have hlt2' : ℓ - 2 < (k : ℝ) * 2 := by simpa [mul_comm] using hlt2 exact (div_lt_iff₀ h2pos).mpr hlt2' linarith have hℓ : (4 : ℝ) ≤ ℓ := by have hmono := Real.logb_le_logb_of_le (by norm_num : (1 : ℝ) < 2) (by norm_num : (0 : ℝ) < (16 : ℝ)) (by exact_mod_cast (by omega : (16 : ℕ) ≤ n) : (16 : ℝ) ≤ (n : ℝ)) have h16 : Real.logb 2 (16 : ℝ) = 4 := by have hpow : (16 : ℝ) = (2 : ℝ) ^ 4 := by norm_num rw [hpow, Real.logb_pow, Real.logb_self_eq_one (by norm_num : (1 : ℝ) < 2)] norm_num rw [h16] at hmono simpa [ℓ] using hmono have hfinal : ℓ / 8 ≤ (ℓ - 2) / 4 := by nlinarith linarith
end Chapter05end CLRS

Root compatibility aliases

The streak development predated the CLRS.Chapter05 namespace. Keep its original root-level proof surface available to downstream users while the new chapter-facing declarations remain namespaced.

abbrev CoinFlip := CLRS.Chapter05.CoinFlipabbrev headAt := CLRS.Chapter05.headAtabbrev hasRunOfLength := CLRS.Chapter05.hasRunOfLengthnoncomputable abbrev longestStreak := CLRS.Chapter05.longestStreakabbrev streakS := CLRS.Chapter05.streakSnoncomputable abbrev headsSetBijection {n : ℕ} (S : Finset (Fin n)) := CLRS.Chapter05.headsSetBijection Salias prob_first_t_heads := CLRS.Chapter05.prob_first_t_headsalias headAt_eq_of_lt := CLRS.Chapter05.headAt_eq_of_ltalias headAt_eq_zero_of_ge := CLRS.Chapter05.headAt_eq_zero_of_gealias card_streakS := CLRS.Chapter05.card_streakSalias streakS_all_heads_iff := CLRS.Chapter05.streakS_all_heads_iffalias prob_run_at := CLRS.Chapter05.prob_run_atalias hasRunOfLength_mono := CLRS.Chapter05.hasRunOfLength_monoalias longestStreak_ge_iff_hasRunOfLength := CLRS.Chapter05.longestStreak_ge_iff_hasRunOfLengthalias fintypeExpect_mono := CLRS.Chapter05.fintypeExpect_monoalias prob_run_at_bound := CLRS.Chapter05.prob_run_at_boundalias longestStreak_upperBound := CLRS.Chapter05.longestStreak_upperBoundalias longestStreak_le := CLRS.Chapter05.longestStreak_lealias natCast_eq_sum_ite_Icc := CLRS.Chapter05.natCast_eq_sum_ite_Iccalias expectedLongestStreak_eq_tailSum := CLRS.Chapter05.expectedLongestStreak_eq_tailSumalias expectedLongestStreak_le := CLRS.Chapter05.expectedLongestStreak_le

Definitions and proofs

CLRSLean.FourthEdition.Chapter_05.Section_05_4_Probabilistic_Analysis.OnlineHiring

CLRS §5.4.4 — The On-line Hiring Problem

We model the on-line hiring problem (CLRS §5.4.4). n candidates arrive in random order (uniform over all n! permutations). After each interview the algorithm must decide immediately whether to hire the current candidate and stop, or to continue. The goal is to maximize the probability of hiring the best candidate.

The threshold strategy interviews the first k applicants without hiring (the observation phase), then hires the first applicant who is better than every applicant seen so far.

Status: The finite record-selection strategy is executable and comes with exact some and none contracts, and its success probability has the harmonic closed form (k/n) * (H_{n-1} - H_{k-1}) (probHireBest_eq). The 1/e asymptotic is proved for the threshold ⌊n/e⌋ (probHireBest_asymptotic).

namespace CLRSnamespace Chapter05open CLRS.Probabilityopen Filteropen scoped Topologynamespace OnlineHiring
Model

The sample space is the uniform distribution over Equiv.Perm (Fin n). Candidate i has score π i (0 = best, n-1 = worst). The absolute best candidate is the one with score 0.

The absolute best candidate: the one mapped to 0 (smallest score) by the permutation.

def isAbsoluteBest {n : ℕ} (π : Equiv.Perm (Fin n)) (i : Fin n) : Prop := (π i).val = 0

Candidate j is a record when its score is better (numerically smaller) than every earlier candidate's score.

def isRecordAt {n : ℕ} (π : Equiv.Perm (Fin n)) (j : Fin n) : Prop := ∀ i : Fin n, i.val < j.val → (π j).val < (π i).val

isRecordAt is decidable: it is a finite universal over the scores.

instance {n : ℕ} (π : Equiv.Perm (Fin n)) (j : Fin n) : Decidable (isRecordAt π j) := by unfold isRecordAt infer_instance

The record positions at or after the natural-number observation threshold.

def eligiblePositions {n : ℕ} (k : ℕ) (π : Equiv.Perm (Fin n)) : Finset (Fin n) := Finset.univ.filter fun j => k ≤ j.val ∧ isRecordAt π j

The executable threshold strategy selects the earliest eligible record.

def hiringStrategy {n : ℕ} (k : ℕ) (π : Equiv.Perm (Fin n)) : Option (Fin n) := let eligible := eligiblePositions k π if h : eligible.Nonempty then some (eligible.min' h) else none

Membership in the executable candidate set is exactly the threshold and record condition.

theorem mem_eligiblePositions_iff {n : ℕ} {k : ℕ} {π : Equiv.Perm (Fin n)} {j : Fin n} : j ∈ eligiblePositions k π ↔ k ≤ j.val ∧ isRecordAt π j := by simp [eligiblePositions]

Exact contract for a successful threshold selection: the returned position is an eligible record and is no later than any other eligible record.

theorem hiringStrategy_some_iff {n : ℕ} {k : ℕ} {π : Equiv.Perm (Fin n)} {j : Fin n} : hiringStrategy k π = some j ↔ k ≤ j.val ∧ isRecordAt π j ∧ ∀ i : Fin n, k ≤ i.val → isRecordAt π i → j ≤ i := by classical unfold hiringStrategy dsimp only split_ifs with hne · constructor · intro h have hj : (eligiblePositions k π).min' hne = j := Option.some.inj h subst j have hmem : (eligiblePositions k π).min' hne ∈ eligiblePositions k π := Finset.min'_mem _ hne have helig := mem_eligiblePositions_iff.mp hmem refine ⟨helig.1, helig.2, ?_⟩ intro i hi hrecord exact Finset.min'_le _ i (mem_eligiblePositions_iff.mpr ⟨hi, hrecord⟩) · rintro ⟨hj, hrecord, hleast⟩ apply congrArg some apply le_antisymm · exact Finset.min'_le _ j (mem_eligiblePositions_iff.mpr ⟨hj, hrecord⟩) · have hminmem : (eligiblePositions k π).min' hne ∈ eligiblePositions k π := Finset.min'_mem _ hne have hmin := mem_eligiblePositions_iff.mp hminmem exact hleast _ hmin.1 hmin.2 · constructor · intro h simp at h · rintro ⟨hj, hrecord, _⟩ exact False.elim (hne ⟨j, mem_eligiblePositions_iff.mpr ⟨hj, hrecord⟩⟩)

Exact contract for failure: there is no record position at or after the observation threshold.

theorem hiringStrategy_none_iff {n : ℕ} {k : ℕ} {π : Equiv.Perm (Fin n)} : hiringStrategy k π = none ↔ ∀ j : Fin n, k ≤ j.val → ¬ isRecordAt π j := by classical constructor · intro hnone j hj hrecord have hne : (eligiblePositions k π).Nonempty := ⟨j, mem_eligiblePositions_iff.mpr ⟨hj, hrecord⟩⟩ simp [hiringStrategy, hne] at hnone · intro hnone have hempty : ¬ (eligiblePositions k π).Nonempty := by rintro ⟨j, hjmem⟩ have hj := mem_eligiblePositions_iff.mp hjmem exact hnone j hj.1 hj.2 simp [hiringStrategy, hempty]

A successful hire occurs at or after the observation threshold.

theorem hiringStrategy_after_observation {n : ℕ} {k : ℕ} {π : Equiv.Perm (Fin n)} {j : Fin n} (h : hiringStrategy k π = some j) : k ≤ j.val := (hiringStrategy_some_iff.mp h).1

A successfully hired candidate is a record at their interview position.

theorem hiringStrategy_record {n : ℕ} {k : ℕ} {π : Equiv.Perm (Fin n)} {j : Fin n} (h : hiringStrategy k π = some j) : isRecordAt π j := (hiringStrategy_some_iff.mp h).2.1

Finite success probability of the threshold strategy under the uniform distribution on permutations of the candidate positions.

noncomputable def probHireBest (n k : ℕ) : ℝ := by classical exact fintypeExpect fun π : Equiv.Perm (Fin n) => match hiringStrategy k π with | some i => if isAbsoluteBest π i then 1 else 0 | none => 0
Closed form of the success probability

The strategy succeeds exactly when it hires the absolute best candidate. We prove the classic harmonic closed form (CLRS §5.4.4): the success probability is (k/n) * (H_{n-1} - H_{k-1}), the product of k/n with the harmonic difference.

The proof conditions on the position j of the best candidate. Given the best is at j (probability 1/n), the strategy hires it exactly when no record occurs in positions {k, ..., j-1}; a record is a left-to-right minimum of the scores (0 = best), so no record occurs there exactly when the minimum score among the first j.val positions is already achieved at a position < k. The minimum's position is uniformly distributed over the first j.val positions (transposition symmetry), giving probability k / j.val. Summing over j yields the harmonic closed form.

Embed the first m positions {0,...,m-1} into Fin n.

def liftFirst {n m : ℕ} (hm : m ≤ n) (t : Fin m) : Fin n := ⟨t.val, lt_of_lt_of_le t.isLt hm⟩

Position p (among the first m) holds the minimum score among the first m positions. Scores are Fin n elements and 0 is the best.

def isMinInFirst {n m : ℕ} (hm : m ≤ n) (π : Equiv.Perm (Fin n)) (p : Fin m) : Prop := ∀ t : Fin m, (π (liftFirst hm p)).val ≤ (π (liftFirst hm t)).val

isMinInFirst is decidable: it is a finite universal over the first m positions.

instance isMinInFirst_decidable {n m : ℕ} (hm : m ≤ n) (π : Equiv.Perm (Fin n)) (p : Fin m) : Decidable (isMinInFirst hm π p) := by unfold isMinInFirst infer_instance

Two Fin elements with the same value are equal, whatever bound proofs are supplied (proof irrelevance of the val < n witness).

@[simp] theorem Fin.mk_val_mk_val {n : ℕ} {a : ℕ} (h1 h2 : a < n) : (⟨a, h1⟩ : Fin n) = ⟨a, h2⟩ := by apply Fin.ext rfl

⟨x.val, h⟩ is x for any valid bound proof h.

theorem Fin.eq_of_val_mk {n : ℕ} (x : Fin n) (h : x.val < n) : (⟨x.val, h⟩ : Fin n) = x := by apply Fin.ext rfl

A position holding the minimum among the first j positions is strictly smaller in score than every other position of the first j.

lemma isMinInFirst_lt {n j : ℕ} (hjn : j ≤ n) (π : Equiv.Perm (Fin n)) (p : Fin j) (hp : isMinInFirst hjn π p) (i : Fin n) (hpi : i.val < j) (hne : i ≠ liftFirst hjn p) : (π ⟨p.val, lt_of_lt_of_le p.isLt hjn⟩).val < (π i).val := by have hle : (π ⟨p.val, lt_of_lt_of_le p.isLt hjn⟩).val ≤ (π i).val := by have hbi : liftFirst hjn ⟨i.val, hpi⟩ = i := by change ⟨i.val, lt_of_lt_of_le hpi hjn⟩ = i exact Fin.eq_of_val_mk i (lt_of_lt_of_le hpi hjn) rw [← hbi] exact hp ⟨i.val, hpi⟩ have hne_val : (π ⟨p.val, lt_of_lt_of_le p.isLt hjn⟩).val ≠ (π i).val := by intro h have hπeq : π ⟨p.val, lt_of_lt_of_le p.isLt hjn⟩ = π i := Fin.ext h exact hne (π.injective hπeq).symm exact lt_of_le_of_ne hle hne_val

Swap the scores at positions a and b of a permutation (right-composition with the transposition).

def swapValues {n : ℕ} (a b : Fin n) (π : Equiv.Perm (Fin n)) : Equiv.Perm (Fin n) := π * Equiv.swap a b

Swapping the scores at a and b is the same as swapping b and a.

lemma swapValues_comm {n : ℕ} (a b : Fin n) (π : Equiv.Perm (Fin n)) : swapValues a b π = swapValues b a π := by unfold swapValues rw [Equiv.swap_comm a b]

swapValues is an involution: swapping the same two positions twice is the identity.

lemma swapValues_involutive {n : ℕ} (a b : Fin n) (π : Equiv.Perm (Fin n)) : swapValues a b (swapValues a b π) = π := by unfold swapValues simp [mul_assoc, This simp argument is unused: Equiv.swap_inv Hint: Omit it from the simp argument list. simp [mul_assoc,̵ ̵E̵q̵u̵i̵v̵.̵s̵w̵a̵p̵_̵i̵n̵v̵] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Equiv.swap_inv]

The minimum of the first m positions exists (for 0 < m).

lemma isMinInFirst_exists {n m : ℕ} (hm : m ≤ n) (hmpos : 0 < m) (π : Equiv.Perm (Fin n)) : ∃ p : Fin m, isMinInFirst hm π p := by let S : Finset ℕ := Finset.image (fun t : Fin m => (π (liftFirst hm t)).val) Finset.univ have hne : S.Nonempty := by exact ⟨(π (liftFirst hm ⟨0, hmpos⟩)).val, Finset.mem_image.mpr ⟨⟨0, hmpos⟩, Finset.mem_univ _, rfl⟩⟩ rcases Finset.mem_image.mp (Finset.min'_mem S hne) with ⟨p, hp, hpm⟩ refine ⟨p, ?_⟩ intro t have ht_mem : (π (liftFirst hm t)).val ∈ S := Finset.mem_image.mpr ⟨t, Finset.mem_univ _, rfl⟩ have hle : S.min' hne ≤ (π (liftFirst hm t)).val := Finset.min'_le S _ ht_mem rwa [← hpm] at hle

liftFirst is injective: the embedding of the first m positions is one-to-one.

lemma liftFirst_injective {n m : ℕ} (hm : m ≤ n) {a b : Fin m} (h : liftFirst hm a = liftFirst hm b) : a = b := by apply Fin.ext change (liftFirst hm a).val = (liftFirst hm b).val exact congrArg Fin.val h

The minimum of the first m positions is unique (scores are distinct).

lemma isMinInFirst_unique {n m : ℕ} (hm : m ≤ n) (π : Equiv.Perm (Fin n)) {p q : Fin m} (hp : isMinInFirst hm π p) (hq : isMinInFirst hm π q) : p = q := by have hle1 : (π (liftFirst hm p)).val ≤ (π (liftFirst hm q)).val := hp q have hle2 : (π (liftFirst hm q)).val ≤ (π (liftFirst hm p)).val := hq p have hval : (π (liftFirst hm p)).val = (π (liftFirst hm q)).val := le_antisymm hle1 hle2 have hπeq : π (liftFirst hm p) = π (liftFirst hm q) := Fin.ext hval exact liftFirst_injective hm (π.injective hπeq)

Swapping the scores at positions p and q (both in the first m) moves the minimum of the first m positions from p to q.

try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` lemma isMinInFirst_swap {n m : ℕ} (hm : m ≤ n) {p q : Fin m} (Variable name `hne` 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`hne : p ≠ q) (π : Equiv.Perm (Fin n)) (hp : isMinInFirst hm π p) : isMinInFirst hm (swapValues (liftFirst hm p) (liftFirst hm q) π) q := by classical intro t -- new score at position q is the old minimum `π (liftFirst hm p)` have hL : (swapValues (liftFirst hm p) (liftFirst hm q) π (liftFirst hm q)).val = (π (liftFirst hm p)).val := by unfold swapValues simp [Equiv.swap_apply_right] rw [hL] by_cases htq : t = q · subst t -- new score at q equals the old minimum, so the inequality is reflexive try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hL] · by_cases htp : t = p · subst t -- new score at p is the old score at q, which is above the old minimum have hR : (swapValues (liftFirst hm p) (liftFirst hm q) π (liftFirst hm p)).val = (π (liftFirst hm q)).val := by unfold swapValues simp [Equiv.swap_apply_left] rw [hR] exact hp q · -- t is neither p nor q, so the swap fixes it have hfix : (Equiv.swap (liftFirst hm p) (liftFirst hm q)) (liftFirst hm t) = liftFirst hm t := by apply Equiv.swap_apply_of_ne_of_ne · intro h exact htp (liftFirst_injective hm h) · intro h exact htq (liftFirst_injective hm h) have hR : (swapValues (liftFirst hm p) (liftFirst hm q) π (liftFirst hm t)).val = (π (liftFirst hm t)).val := by unfold swapValues simp [hfix] rw [hR] exact hp t

The transposition of two positions other than pos preserves the property "score 0 is at pos".

lemma bestAt_swap (pos : Fin n) {a b : Fin n} (hpa : a ≠ pos) (hpb : b ≠ pos) (π : Equiv.Perm (Fin n)) (h : (π pos).val = 0) : (swapValues a b π pos).val = 0 := by have hfix : (Equiv.swap a b) pos = pos := Equiv.swap_apply_of_ne_of_ne (fun hx => hpa hx.symm) (fun hx => hpb hx.symm) unfold swapValues simp [hfix, h]

The set of permutations with score 0 at pos and the minimum of the first m positions at p.

noncomputable def bestMinSet (n m : ℕ) (hm : m ≤ n) (pos : Fin n) (p : Fin m) : Finset (Equiv.Perm (Fin n)) := (Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π pos).val = 0 ∧ isMinInFirst hm π p)

The number of permutations with score 0 at pos and the minimum of the first m positions at p.

noncomputable def bestMinCount (n m : ℕ) (hm : m ≤ n) (pos : Fin n) (p : Fin m) : ℕ := (bestMinSet n m hm pos p).card

The sets bestMinSet ... p for p : Fin m are pairwise disjoint, because the minimum of the first m positions is unique.

lemma bestMinSet_disjoint {n m : ℕ} (hm : m ≤ n) (pos : Fin n) : (Set.univ : Set (Fin m)).PairwiseDisjoint (fun p => bestMinSet n m hm pos p) := by intro p _ q _ hpq change Disjoint (bestMinSet n m hm pos p) (bestMinSet n m hm pos q) rw [Finset.disjoint_left] intro π hπ hπ' rw [bestMinSet, Finset.mem_filter] at hπ hπ' exact hpq (isMinInFirst_unique hm π hπ.2.2 hπ'.2.2)

The sets bestMinSet ... p for p : Fin m cover the permutations with score 0 at pos (for 0 < m), since the minimum of the first m positions always exists.

lemma bestMinSet_cover {n m : ℕ} (hm : m ≤ n) (hmpos : 0 < m) (pos : Fin n) : Finset.biUnion Finset.univ (fun p : Fin m => bestMinSet n m hm pos p) = (Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π pos).val = 0) := by ext π constructor · intro hπ rcases Finset.mem_biUnion.mp hπ with ⟨p, _, hp⟩ simp [bestMinSet] at hp exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, hp.1⟩ · intro hπ rw [Finset.mem_filter] at hπ rcases isMinInFirst_exists hm hmpos π with ⟨p, hpmin⟩ refine Finset.mem_biUnion.mpr ⟨p, Finset.mem_univ _, ?_⟩ simp [bestMinSet, hπ.2, hpmin]

The number of best-at-pos permutations with minimum at p is independent of p: transposition symmetry moves the minimum position anywhere within the first m positions.

lemma bestMinCount_eq {n m : ℕ} (hm : m ≤ n) (pos : Fin n) (hpos : m ≤ pos.val) {p q : Fin m} (hne : p ≠ q) : bestMinCount n m hm pos p = bestMinCount n m hm pos q := by classical apply Finset.card_bij (fun π hπ => swapValues (liftFirst hm p) (liftFirst hm q) π) ?_ ?_ ?_ · intro π hπ rw [bestMinSet, Finset.mem_filter] at hπ ⊢ rcases hπ with ⟨hπu, hbest, hmin⟩ refine ⟨Finset.mem_univ _, ?_⟩ have hpos_ne_p : liftFirst hm p ≠ pos := by intro h have : p.val < pos.val := by omega exact (ne_of_lt this) (congrArg Fin.val h) have hpos_ne_q : liftFirst hm q ≠ pos := by intro h have : q.val < pos.val := by omega exact (ne_of_lt this) (congrArg Fin.val h) exact ⟨bestAt_swap pos hpos_ne_p hpos_ne_q π hbest, isMinInFirst_swap hm hne π hmin⟩ · intro π₁ _ π₂ _ h -- swap is an involution, so apply it again on both sides have h₁ : swapValues (liftFirst hm p) (liftFirst hm q) (swapValues (liftFirst hm p) (liftFirst hm q) π₁) = swapValues (liftFirst hm p) (liftFirst hm q) (swapValues (liftFirst hm p) (liftFirst hm q) π₂) := by rw [h] simpa [swapValues_involutive] using h₁ · intro π hπ rw [bestMinSet, Finset.mem_filter] at hπ rcases hπ with ⟨hπu, hbest, hmin⟩ have hpos_ne_p : liftFirst hm p ≠ pos := by intro h have : p.val < pos.val := by omega exact (ne_of_lt this) (congrArg Fin.val h) have hpos_ne_q : liftFirst hm q ≠ pos := by intro h have : q.val < pos.val := by omega exact (ne_of_lt this) (congrArg Fin.val h) refine ⟨swapValues (liftFirst hm p) (liftFirst hm q) π, ?_, ?_⟩ · rw [bestMinSet, Finset.mem_filter] refine ⟨Finset.mem_univ _, ?_⟩ exact ⟨bestAt_swap pos hpos_ne_p hpos_ne_q π hbest, by simpa [swapValues_comm] using isMinInFirst_swap hm (Ne.symm hne) π hmin⟩ · simp [swapValues_involutive]

The sets bestMinSet ... p for p : Fin m partition the best-at-pos permutations, so their counts sum to the number of best-at-pos permutations.

lemma sum_bestMinCount {n m : ℕ} (hm : m ≤ n) (hmpos : 0 < m) (pos : Fin n) : (∑ p : Fin m, bestMinCount n m hm pos p) = ((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π pos).val = 0)).card := by have hpair : (((Finset.univ : Finset (Fin m)) : Set (Fin m))).PairwiseDisjoint (fun p => bestMinSet n m hm pos p) := by simpa using bestMinSet_disjoint hm pos calc (∑ p : Fin m, bestMinCount n m hm pos p) = ∑ p : Fin m, (bestMinSet n m hm pos p).card := by simp [bestMinCount] _ = (Finset.biUnion Finset.univ (fun p : Fin m => bestMinSet n m hm pos p)).card := by rw [Finset.card_biUnion (h := hpair)] _ = ((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π pos).val = 0)).card := by rw [bestMinSet_cover hm hmpos pos]

The number of best-at-pos permutations is the same for every position: swapping the scores at a and b maps the score-0-at-a permutations bijectively onto the score-0-at-b permutations.

lemma card_bestAt_eq (n : ℕ) (a b : Fin n) : ((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π a).val = 0)).card = ((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π b).val = 0)).card := by classical apply Finset.card_bij (fun π hπ => swapValues a b π) ?_ ?_ ?_ · intro π hπ rw [Finset.mem_filter] at hπ ⊢ rcases hπ with ⟨hπu, h⟩ refine ⟨Finset.mem_univ _, ?_⟩ unfold swapValues rw [Equiv.Perm.mul_apply, Equiv.swap_apply_right] exact h · intro π₁ _ π₂ _ h have h₁ : swapValues a b (swapValues a b π₁) = swapValues a b (swapValues a b π₂) := by rw [h] simpa [swapValues_involutive] using h₁ · intro π hπ rw [Finset.mem_filter] at hπ rcases hπ with ⟨hπu, h⟩ refine ⟨swapValues a b π, ?_, ?_⟩ · refine Finset.mem_filter.mpr ⟨Finset.mem_univ _, ?_⟩ unfold swapValues rw [Equiv.Perm.mul_apply, Equiv.swap_apply_left] exact h · simp [swapValues_involutive]

Each permutation has score 0 at exactly one position, so the best-at-a counts over all positions sum to n! (for 0 < n, so that Fin n is nonempty).

lemma sum_card_bestAt (n : ℕ) (hn : 0 < n) : (∑ a : Fin n, ((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π a).val = 0)).card) = n.factorial := by classical haveI : NeZero n := ⟨Nat.ne_of_gt hn⟩ calc (∑ a : Fin n, ((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π a).val = 0)).card) = ∑ a : Fin n, ∑ π : Equiv.Perm (Fin n), (if (π a).val = 0 then (1 : ℕ) else 0) := by refine Finset.sum_congr rfl (fun a _ => ?_) rw [Finset.card_filter] _ = ∑ π : Equiv.Perm (Fin n), ∑ a : Fin n, (if (π a).val = 0 then (1 : ℕ) else 0) := by rw [Finset.sum_comm] _ = ∑ π : Equiv.Perm (Fin n), (1 : ℕ) := by refine Finset.sum_congr rfl (fun π _ => ?_) let a0 : Fin n := π.symm (0 : Fin n) have hmem : (π a0).val = 0 := by simp [a0] have hiff : ∀ a : Fin n, (π a).val = 0 ↔ a = a0 := by intro a constructor · intro h have hπeq : π a = π a0 := by apply Fin.ext rw [h, hmem] exact (Equiv.bijective π).1 hπeq · intro h; rw [h]; exact hmem calc ∑ a : Fin n, (if (π a).val = 0 then (1 : ℕ) else 0) = ∑ a : Fin n, (if a = a0 then (1 : ℕ) else 0) := by refine Finset.sum_congr rfl (fun a _ => ?_) exact if_congr (hiff a) rfl rfl _ = 1 := by simp _ = n.factorial := by simp [Fintype.card_perm]
The per-position probabilities

We combine the counting lemmas into the two probabilities the closed form needs: score 0 is at pos with probability 1/n, and (given the minimum of the first m positions is at p) that joint event has probability 1/(nm).

A position other than the best has nonzero score.

lemma val_ne_zero_of_ne_best {n : ℕ} (j i : Fin n) (π : Equiv.Perm (Fin n)) (hbest : (π j).val = 0) (hne : i ≠ j) : (π i).val ≠ 0 := by intro h apply hne apply π.injective apply Fin.ext rw [hbest, h]

The real-valued sum of indicators over a finite type is the cardinality of the corresponding filtered set.

lemma sum_indicator_eq_card {α : Type} [Fintype α] (p : α → Prop) [DecidablePred p] : (∑ a : α, indicator (p a)) = (((Finset.univ : Finset α).filter p).card : ℝ) := by unfold indicator rw [Finset.card_filter] push_cast rfl

The best score 0 is at position pos with probability 1/n, by the uniformity of the position of score 0 over the n positions.

theorem prob_bestAt (n : ℕ) (pos : Fin n) (hn : 0 < n) : fintypeExpect (fun π : Equiv.Perm (Fin n) => indicator ((π pos).val = 0)) = 1 / (n : ℝ) := by classical have hfac_card : (Fintype.card (Equiv.Perm (Fin n)) : ℝ) = (n.factorial : ℝ) := by rw [Fintype.card_perm] simp have hnum : (∑ π : Equiv.Perm (Fin n), indicator ((π pos).val = 0)) = (((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π pos).val = 0)).card : ℝ) := by exact sum_indicator_eq_card (fun π : Equiv.Perm (Fin n) => (π pos).val = 0) rw [fintypeExpect, hnum, hfac_card] let c : ℕ := ((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π pos).val = 0)).card have h_uniform : (∑ a : Fin n, (((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π a).val = 0)).card : ℝ)) = (n : ℝ) * (c : ℝ) := by calc (∑ a : Fin n, (((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π a).val = 0)).card : ℝ)) = ∑ a : Fin n, (c : ℝ) := by refine Finset.sum_congr rfl (fun a _ => ?_) have h := card_bestAt_eq n a pos exact_mod_cast h _ = (n : ℝ) * (c : ℝ) := by simp have h_sum : (∑ a : Fin n, (((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π a).val = 0)).card : ℝ)) = (n.factorial : ℝ) := by exact_mod_cast sum_card_bestAt n hn have h_eq : (n : ℝ) * (c : ℝ) = (n.factorial : ℝ) := by rw [← h_uniform] exact h_sum have hposn : (n : ℝ) ≠ 0 := by positivity have hposfact : (n.factorial : ℝ) ≠ 0 := by positivity have hfrac : (c : ℝ) / (n.factorial : ℝ) = 1 / (n : ℝ) := by field_simp [hposn, hposfact] linarith [h_eq] change (c : ℝ) / (n.factorial : ℝ) = 1 / (n : ℝ) exact hfrac

Given score 0 at pos and the minimum of the first m positions at p, the probability is 1/(n·m): the joint event counts, for each of the n choices of the position of score 0 and the m choices of the minimum position, the same number of permutations.

theorem prob_bestMin (n m : ℕ) (hm : m ≤ n) (hmpos : 0 < m) (pos : Fin n) (hpos : m ≤ pos.val) (hn : 0 < n) (p : Fin m) : fintypeExpect (fun π : Equiv.Perm (Fin n) => indicator ((π pos).val = 0 ∧ isMinInFirst hm π p)) = (1 : ℝ) / (n : ℝ) * (1 : ℝ) / (m : ℝ) := by classical have hfac_card : (Fintype.card (Equiv.Perm (Fin n)) : ℝ) = (n.factorial : ℝ) := by rw [Fintype.card_perm] simp have hnum : (∑ π : Equiv.Perm (Fin n), indicator ((π pos).val = 0 ∧ isMinInFirst hm π p)) = (bestMinCount n m hm pos p : ℝ) := by rw [bestMinCount, bestMinSet] exact sum_indicator_eq_card (fun π : Equiv.Perm (Fin n) => (π pos).val = 0 ∧ isMinInFirst hm π p) rw [fintypeExpect, hnum, hfac_card] let T : ℕ := bestMinCount n m hm pos p have h_uniform : (∑ q : Fin m, (bestMinCount n m hm pos q : ℝ)) = (m : ℝ) * (T : ℝ) := by calc (∑ q : Fin m, (bestMinCount n m hm pos q : ℝ)) = ∑ q : Fin m, (T : ℝ) := by refine Finset.sum_congr rfl (fun q _ => ?_) have h : bestMinCount n m hm pos p = bestMinCount n m hm pos q := by by_cases hpq : p = q · subst q; rfl · exact bestMinCount_eq hm pos hpos hpq exact_mod_cast h.symm _ = (m : ℝ) * (T : ℝ) := by simp have h_sum : (∑ q : Fin m, (bestMinCount n m hm pos q : ℝ)) = (((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π pos).val = 0)).card : ℝ) := by exact_mod_cast sum_bestMinCount hm hmpos pos have h_eq : (m : ℝ) * (T : ℝ) = (((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π pos).val = 0)).card : ℝ) := by rw [← h_uniform] exact h_sum -- restate prob_bestAt as `#(bestAt pos)/n! = 1/n` have h_pb : (((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π pos).val = 0)).card : ℝ) / (n.factorial : ℝ) = 1 / (n : ℝ) := by have h' := prob_bestAt n pos hn rw [fintypeExpect, hfac_card] at h' have hnum' : (∑ π : Equiv.Perm (Fin n), indicator ((π pos).val = 0)) = (((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π pos).val = 0)).card : ℝ) := by exact sum_indicator_eq_card (fun π : Equiv.Perm (Fin n) => (π pos).val = 0) rw [hnum'] at h' exact h' have hposn : (n : ℝ) ≠ 0 := by positivity have hposm : (m : ℝ) ≠ 0 := by positivity have hposfact : (n.factorial : ℝ) ≠ 0 := by positivity have hfrac : (T : ℝ) / (n.factorial : ℝ) = (1 : ℝ) / (n : ℝ) * (1 : ℝ) / (m : ℝ) := by field_simp [hposn, hposm, hposfact] -- goal: T * n * m = n! ; from h_eq: m·T = B and h_pb: B/n! = 1/n have h_pb_mul : (((Finset.univ : Finset (Equiv.Perm (Fin n))).filter (fun π => (π pos).val = 0)).card : ℝ) * (n : ℝ) = (n.factorial : ℝ) := by field_simp [hposn, hposfact] at h_pb exact h_pb nlinarith [h_eq, h_pb_mul] change (T : ℝ) / (n.factorial : ℝ) = (1 : ℝ) / (n : ℝ) * (1 : ℝ) / (m : ℝ) exact hfrac
Characterizing when the best candidate is hired

Given the best candidate is at position j, the strategy hires it exactly when no record occurs in positions {k, ..., j-1}. A record is a left-to-right minimum of the scores, so this is equivalent to the minimum score among the first j.val positions already being achieved at a position below k.

The minimum score among the first j.val positions is achieved at a position below the threshold k.

def minInFirstK (n k : ℕ) (j : Fin n) (hkj : k ≤ j.val) (hjn : j.val ≤ n) (π : Equiv.Perm (Fin n)) : Prop := ∃ p : Fin k, isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩

minInFirstK is decidable: it is a finite existential over Fin k.

instance minInFirstK_decidable (n k : ℕ) (j : Fin n) (hkj : k ≤ j.val) (hjn : j.val ≤ n) (π : Equiv.Perm (Fin n)) : Decidable (minInFirstK n k j hkj hjn π) := by unfold minInFirstK infer_instance

Best-candidate characterization. The strategy hires the best candidate at position j if and only if the best is at j and the minimum score among the first j.val positions is among the first k positions.

theorem hiringStrategy_some_iff_minInFirstK (n k : ℕ) (hk : 0 < k) (j : Fin n) (hkj : k ≤ j.val) (hjn : j.val ≤ n) (π : Equiv.Perm (Fin n)) : (hiringStrategy k π = some j ∧ isAbsoluteBest π j) ↔ (isAbsoluteBest π j ∧ minInFirstK n k j hkj hjn π) := by classical constructor · intro h rcases h with ⟨hsj, hbest⟩ refine ⟨hbest, ?_⟩ have hs := hiringStrategy_some_iff.mp hsj rcases hs with ⟨_, _, hno_rec⟩ have hjpos : 0 < j.val := lt_of_lt_of_le hk hkj rcases isMinInFirst_exists hjn hjpos π with ⟨m, hm⟩ have hmln : m.val < n := lt_of_lt_of_le m.isLt hjn have hk_le_m : ¬ k ≤ m.val := by intro hkm have hrec_m : isRecordAt π ⟨m.val, hmln⟩ := by unfold isRecordAt intro i hi change i.val < m.val at hi exact isMinInFirst_lt hjn π m hm i (lt_trans hi m.isLt) (by intro h have hval : m.val = i.val := by simpa [liftFirst] using congrArg Fin.val h.symm exact (ne_of_lt hi) hval.symm) have hjm : j ≤ ⟨m.val, hmln⟩ := hno_rec ⟨m.val, hmln⟩ hkm hrec_m have hjm_val : j.val ≤ m.val := Fin.le_def.mp hjm omega exact ⟨⟨m.val, lt_of_not_ge hk_le_m⟩, hm⟩ · intro h rcases h with ⟨hbest, hmin⟩ refine ⟨?_, hbest⟩ refine (hiringStrategy_some_iff.mpr ⟨hkj, ?_, ?_⟩) · unfold isRecordAt intro i hi have h0 : (π i).val ≠ 0 := by apply val_ne_zero_of_ne_best j i π hbest intro hij have : i.val = j.val := congrArg Fin.val hij omega have hpos : 0 < (π i).val := Nat.pos_of_ne_zero h0 rw [hbest] exact hpos · intro i hki hrec_i by_contra hji have hiltj : i.val < j.val := Fin.lt_def.mp (lt_of_not_ge hji) rcases hmin with ⟨p, hp⟩ have hplj : p.val < j.val := lt_of_lt_of_le p.isLt hkj have hplti : p.val < i.val := by omega have hne : i ≠ liftFirst hjn ⟨p.val, hplj⟩ := by intro h have : p.val = i.val := congrArg Fin.val h.symm omega have hlt : (π ⟨p.val, lt_of_lt_of_le hplj hjn⟩).val < (π i).val := isMinInFirst_lt hjn π ⟨p.val, hplj⟩ hp i hiltj hne have hpln : p.val < n := lt_of_lt_of_le hplj hjn have hlt2 : (π i).val < (π ⟨p.val, hpln⟩).val := hrec_i ⟨p.val, hpln⟩ hplti exact (lt_asymm hlt (by simpa using hlt2)).elim

The indicator of minInFirstK is the sum over p : Fin k of the indicators of the individual minimum positions (the minimum is unique).

lemma indicator_minInFirstK_eq (n k : ℕ) (Variable name `hk` 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`hk : 0 < k) (j : Fin n) (hkj : k ≤ j.val) (hjn : j.val ≤ n) (π : Equiv.Perm (Fin n)) : indicator (minInFirstK n k j hkj hjn π) = ∑ p : Fin k, indicator (isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩) := by classical unfold minInFirstK indicator by_cases h : ∃ p : Fin k, isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩ · rcases h with ⟨p0, hp0⟩ have honly : ∀ p : Fin k, isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩ ↔ p = p0 := by intro p constructor · intro hpp have he := isMinInFirst_unique hjn π hpp hp0 exact Fin.ext (by simpa using congrArg Fin.val he) · intro hpp; subst p; exact hp0 have hsum : (∑ p : Fin k, indicator (isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩)) = 1 := by have hre : (∑ p : Fin k, indicator (isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩)) = ∑ p : Fin k, indicator (p = p0) := by refine Finset.sum_congr rfl (fun p _ => ?_) unfold indicator exact if_congr (honly p) rfl rfl rw [hre] simp [indicator] rw [if_pos ⟨p0, hp0⟩] exact hsum.symm · have hsum : (∑ p : Fin k, indicator (isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩)) = 0 := by apply Finset.sum_eq_zero intro p _ have : ¬ isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩ := by intro hpp exact h ⟨p, hpp⟩ simp [indicator, this] rw [if_neg h] exact hsum.symm
The closed form

Combining the per-position probability with the harmonic sum gives the textbook closed form for the on-line hiring success probability.

The event "the strategy hires the best at position j" is decidable.

noncomputable instance hiringStrategy_best_decidable (n k : ℕ) (j : Fin n) (π : Equiv.Perm (Fin n)) : Decidable (hiringStrategy k π = some j ∧ isAbsoluteBest π j) := Classical.propDecidable _

Per-position success probability. The probability that the strategy hires the best candidate at position j is k/(n·j.val): the best is at j with probability 1/n, and given that, the minimum of the first j.val positions is below k with probability k/j.val.

try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` theorem probBestAt (n k : ℕ) (hk : 0 < k) (j : Fin n) (hkj : k ≤ j.val) : fintypeExpect (fun π : Equiv.Perm (Fin n) => indicator (hiringStrategy k π = some j ∧ isAbsoluteBest π j)) = (1 : ℝ) / (n : ℝ) * (k : ℝ) / (j.val : ℝ) := by classical let hjn : j.val ≤ n := j.isLt.le have hn : 0 < n := lt_of_lt_of_le (lt_of_lt_of_le hk hkj) j.isLt.le have hrewrite : fintypeExpect (fun π => indicator (hiringStrategy k π = some j ∧ isAbsoluteBest π j)) = fintypeExpect (fun π => indicator (isAbsoluteBest π j ∧ minInFirstK n k j hkj hjn π)) := by apply congrArg fintypeExpect funext π unfold indicator exact if_congr (hiringStrategy_some_iff_minInFirstK n k hk j hkj hjn π) rfl rfl rw [hrewrite] have hsplit : ∀ π : Equiv.Perm (Fin n), indicator (isAbsoluteBest π j ∧ minInFirstK n k j hkj hjn π) = ∑ p : Fin k, indicator (isAbsoluteBest π j ∧ isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩) := by intro π have hmul : indicator (isAbsoluteBest π j ∧ minInFirstK n k j hkj hjn π) = indicator (isAbsoluteBest π j) * indicator (minInFirstK n k j hkj hjn π) := by by_cases hb : isAbsoluteBest π j <;> by_cases hmin : minInFirstK n k j hkj hjn π <;> simp [indicator, hb, hmin] rw [hmul] rw [indicator_minInFirstK_eq n k hk j hkj hjn π] rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun p _ => ?_) by_cases hb : isAbsoluteBest π j <;> by_cases hmin : isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩ <;> simp [indicator, hb, hmin] have hEsum : fintypeExpect (fun π => indicator (isAbsoluteBest π j ∧ minInFirstK n k j hkj hjn π)) = ∑ p : Fin k, fintypeExpect (fun π => indicator (isAbsoluteBest π j ∧ isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩)) := by rw [show fintypeExpect (fun π => indicator (isAbsoluteBest π j ∧ minInFirstK n k j hkj hjn π)) = fintypeExpect (fun π => ∑ p : Fin k, indicator (isAbsoluteBest π j ∧ isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩)) from by apply congrArg fintypeExpect funext π exact hsplit π] try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [fintypeExpect_sum] rw [hEsum] have hterm : ∀ p : Fin k, fintypeExpect (fun π => indicator (isAbsoluteBest π j ∧ isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩)) = (1 : ℝ) / (n : ℝ) * (1 : ℝ) / (j.val : ℝ) := by intro p have hif : ∀ π, indicator (isAbsoluteBest π j ∧ isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩) = indicator ((π j).val = 0 ∧ isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩) := by intro π unfold indicator exact if_congr Iff.rfl rfl rfl have heq : fintypeExpect (fun π => indicator (isAbsoluteBest π j ∧ isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩)) = fintypeExpect (fun π => indicator ((π j).val = 0 ∧ isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩)) := by apply congrArg fintypeExpect funext π exact hif π rw [heq] exact prob_bestMin n (j.val) hjn (lt_of_lt_of_le hk hkj) j (le_refl (j.val)) hn ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩ rw [show (∑ p : Fin k, fintypeExpect (fun π => indicator (isAbsoluteBest π j ∧ isMinInFirst hjn π ⟨p.val, lt_of_lt_of_le p.isLt hkj⟩))) = (k : ℝ) * ((1 : ℝ) / (n : ℝ) * (1 : ℝ) / (j.val : ℝ)) from by rw [Finset.sum_congr rfl (fun p _ => hterm p)] simp] ring

The sum Σ_{j=k}^{n-1} 1/j equals the harmonic difference H_{n-1} - H_{k-1}.

lemma sum_recip_Icc_eq_harmonic_sub (k n : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n) : ∑ j ∈ Finset.Icc k (n - 1), (1 : ℝ) / (j : ℝ) = (harmonic (n - 1) : ℝ) - (harmonic (k - 1) : ℝ) := by have hharm : ∀ m : ℕ, (harmonic m : ℝ) = ∑ i ∈ Finset.range m, (1 : ℝ) / ((i : ℝ) + 1) := by intro m unfold harmonic simp [one_div] have hset : Finset.Icc k (n - 1) = Finset.Ico k n := by ext j constructor · intro hj rw [Finset.mem_Icc] at hj rw [Finset.mem_Ico] rcases hj with ⟨hkj, hjn1⟩ refine ⟨hkj, ?_⟩ omega · intro hj rw [Finset.mem_Ico] at hj rw [Finset.mem_Icc] rcases hj with ⟨hkj, hjn⟩ refine ⟨hkj, ?_⟩ omega calc ∑ j ∈ Finset.Icc k (n - 1), (1 : ℝ) / (j : ℝ) = ∑ j ∈ Finset.Ico k n, (1 : ℝ) / (j : ℝ) := by rw [hset] _ = (harmonic (n - 1) : ℝ) - (harmonic (k - 1) : ℝ) := by have hleft : ∑ j ∈ Finset.Ico k n, (1 : ℝ) / (j : ℝ) = ∑ t ∈ Finset.range (n - k), (1 : ℝ) / ((k + t : ℕ) : ℝ) := by rw [Finset.sum_Ico_eq_sum_range] have hright : (harmonic (n - 1) : ℝ) - (harmonic (k - 1) : ℝ) = ∑ t ∈ Finset.range (n - k), (1 : ℝ) / ((k + t : ℕ) : ℝ) := by rw [hharm (n - 1), hharm (k - 1)] rw [← Finset.sum_Ico_eq_sub (f := fun i : ℕ => (1 : ℝ) / ((i : ℝ) + 1)) (m := k - 1) (n := n - 1) (by omega : k - 1 ≤ n - 1)] rw [Finset.sum_Ico_eq_sum_range] have hsub : (n - 1) - (k - 1) = n - k := by omega rw [hsub] refine Finset.sum_congr rfl (fun t _ => ?_) have hden : (↑((k - 1) + t) : ℝ) + 1 = ↑(k + t) := by have hnat : ((k - 1) + t) + 1 = k + t := by omega exact_mod_cast hnat rw [hden] rw [hleft, hright]

On-line hiring closed form (CLRS §5.4.4). The success probability of the threshold strategy that observes the first k candidates and then hires the first record is (k/n) · (H_{n-1} - H_{k-1}).

theorem probHireBest_eq (n k : ℕ) (hk : 0 < k) (hkn : k ≤ n) : probHireBest n k = (k : ℝ) / (n : ℝ) * ((harmonic (n - 1) : ℝ) - (harmonic (k - 1) : ℝ)) := by classical have hn : 0 < n := lt_of_lt_of_le hk hkn have hsuccess : ∀ π : Equiv.Perm (Fin n), (match hiringStrategy k π with | some i => if isAbsoluteBest π i then 1 else 0 | none => 0) = ∑ j : Fin n, indicator (hiringStrategy k π = some j ∧ isAbsoluteBest π j) := by intro π by_cases hs : ∃ j0 : Fin n, hiringStrategy k π = some j0 · rcases hs with ⟨j0, hsj0⟩ have hL : (match hiringStrategy k π with | some i => if isAbsoluteBest π i then (1 : ℝ) else 0 | none => 0) = if isAbsoluteBest π j0 then (1 : ℝ) else 0 := by rw [hsj0] have hR : (∑ j : Fin n, indicator (hiringStrategy k π = some j ∧ isAbsoluteBest π j)) = if isAbsoluteBest π j0 then (1 : ℝ) else 0 := by have h0 : indicator (hiringStrategy k π = some j0 ∧ isAbsoluteBest π j0) = if isAbsoluteBest π j0 then (1 : ℝ) else 0 := by simp [indicator, hsj0] rw [← h0] exact Finset.sum_eq_single (s := Finset.univ) (a := j0) (by intro j _ hne have hnot : ¬ (hiringStrategy k π = some j ∧ isAbsoluteBest π j) := by intro h rcases h with ⟨hsj, _⟩ exact hne (Option.some.inj (hsj0.symm.trans hsj)).symm simp [indicator, hnot]) (by intro hj0; exact False.elim (hj0 (Finset.mem_univ _))) exact hL.trans hR.symm · have hnone : hiringStrategy k π = none := by cases hg : hiringStrategy k π with | none => rfl | some j => exact False.elim (hs ⟨j, hg⟩) have hL : (match hiringStrategy k π with | some i => if isAbsoluteBest π i then (1 : ℝ) else 0 | none => 0) = 0 := by rw [hnone] have hR : (∑ j : Fin n, indicator (hiringStrategy k π = some j ∧ isAbsoluteBest π j)) = 0 := by have hnot : ∀ j : Fin n, ¬ (hiringStrategy k π = some j ∧ isAbsoluteBest π j) := by intro j h rcases h with ⟨hsj, _⟩ rw [hnone] at hsj simp at hsj rw [Finset.sum_eq_zero] intro j _ simp [indicator, hnot j] exact hL.trans hR.symm have hsum : probHireBest n k = ∑ j : Fin n, fintypeExpect (fun π : Equiv.Perm (Fin n) => indicator (hiringStrategy k π = some j ∧ isAbsoluteBest π j)) := by unfold probHireBest rw [show fintypeExpect (fun π : Equiv.Perm (Fin n) => (match hiringStrategy k π with | some i => if isAbsoluteBest π i then 1 else 0 | none => 0)) = fintypeExpect (fun π : Equiv.Perm (Fin n) => ∑ j : Fin n, indicator (hiringStrategy k π = some j ∧ isAbsoluteBest π j)) from by apply congrArg fintypeExpect funext π exact hsuccess π] rw [fintypeExpect_sum (S := Finset.univ) (f := fun j π => indicator (hiringStrategy k π = some j ∧ isAbsoluteBest π j))] rw [hsum] have hterm_zero : ∀ j : Fin n, j.val < k → fintypeExpect (fun π => indicator (hiringStrategy k π = some j ∧ isAbsoluteBest π j)) = 0 := by intro j hjlt have hzero : ∀ π, indicator (hiringStrategy k π = some j ∧ isAbsoluteBest π j) = 0 := by intro π have hnot : ¬ (hiringStrategy k π = some j ∧ isAbsoluteBest π j) := by intro h rcases h with ⟨hsj, _⟩ have hk_le : k ≤ j.val := hiringStrategy_after_observation hsj omega simp [indicator, hnot] have hcongr : fintypeExpect (fun π => indicator (hiringStrategy k π = some j ∧ isAbsoluteBest π j)) = fintypeExpect (fun π : Equiv.Perm (Fin n) => (0 : ℝ)) := by apply congrArg fintypeExpect funext π exact hzero π rw [hcongr] rw [fintypeExpect_const Fintype.card_ne_zero] have hsum_range : (∑ j : Fin n, fintypeExpect (fun π => indicator (hiringStrategy k π = some j ∧ isAbsoluteBest π j))) = ∑ m ∈ Finset.range n, (if m < k then (0 : ℝ) else (1 : ℝ) / (n : ℝ) * (k : ℝ) / (m : ℝ)) := by rw [Finset.sum_fin_eq_sum_range] refine Finset.sum_congr rfl (fun m hm => ?_) have hmn : m < n := Finset.mem_range.mp hm rw [dif_pos hmn] by_cases hmk : m < k · simp [hmk, hterm_zero ⟨m, hmn⟩ hmk] · have hterm := probBestAt n k hk ⟨m, hmn⟩ (Nat.le_of_not_lt hmk) simp [hmk, hterm] rw [hsum_range] have hdrop : (∑ m ∈ Finset.range n, (if m < k then (0 : ℝ) else (1 : ℝ) / (n : ℝ) * (k : ℝ) / (m : ℝ))) = ∑ m ∈ Finset.Icc k (n - 1), (1 : ℝ) / (n : ℝ) * (k : ℝ) / (m : ℝ) := by have hite : (∑ m ∈ Finset.range n, (if m < k then (0 : ℝ) else (1 : ℝ) / (n : ℝ) * (k : ℝ) / (m : ℝ))) = ∑ m ∈ Finset.range n, (if ¬ m < k then (1 : ℝ) / (n : ℝ) * (k : ℝ) / (m : ℝ) else (0 : ℝ)) := by refine Finset.sum_congr rfl (fun m _ => ?_) by_cases hmk : m < k <;> simp [hmk] rw [hite] rw [← Finset.sum_filter] have hset : (Finset.range n).filter (fun m => ¬ m < k) = Finset.Icc k (n - 1) := by ext m constructor · intro hm rw [Finset.mem_filter, Finset.mem_range] at hm rw [Finset.mem_Icc] rcases hm with ⟨hmn, hk_le⟩ refine ⟨Nat.le_of_not_lt hk_le, ?_⟩ omega · intro hm rw [Finset.mem_Icc] at hm rw [Finset.mem_filter, Finset.mem_range] rcases hm with ⟨hkm, hmn1⟩ refine ⟨by omega, ?_⟩ exact Nat.not_lt_of_ge hkm rw [hset] rw [hdrop] have hfactor : (∑ m ∈ Finset.Icc k (n - 1), (1 : ℝ) / (n : ℝ) * (k : ℝ) / (m : ℝ)) = (k : ℝ) / (n : ℝ) * (∑ m ∈ Finset.Icc k (n - 1), (1 : ℝ) / (m : ℝ)) := by rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun m _ => ?_) field_simp rw [hfactor] rw [sum_recip_Icc_eq_harmonic_sub k n hk hkn]
The 1/e asymptotic

The classic secretary-problem optimum threshold k ≈ n/e makes the success probability tend to 1/e (CLRS §5.4.4). The closed form probHireBest_eq gives (k/n)(H_{n-1} - H_{k-1}); the factor k/n tends to 1/e (floor asymptotics), and the harmonic difference tends to 1 (the Euler-Mascheroni asymptotics of the harmonic numbers cancel the shared γ, leaving log(n/k) → log e = 1).

Euler's number e.

noncomputable def e0 : ℝ := Real.exp 1
noncomputable section

The optimal threshold ⌊n/e⌋.

def optThreshold (n : ℕ) : ℕ := ⌊(n : ℝ) / e0⌋₊

e > 0.

lemma e0_pos : 0 < e0 := by unfold e0 positivity

e ≠ 0.

lemma e0_ne_zero : e0 ≠ 0 := ne_of_gt e0_pos

log e = 1.

lemma log_e0 : Real.log e0 = 1 := by unfold e0 rw [Real.log_exp]

(n : ℝ) / e tends to infinity.

lemma tendsto_div_e0_atTop : Tendsto (fun n : ℕ => (n : ℝ) / e0) atTop atTop := by simpa [div_eq_mul_inv] using (Filter.Tendsto.atTop_mul_const (inv_pos.mpr e0_pos) tendsto_natCast_atTop_atTop)

⌊n/e⌋ tends to infinity.

lemma tendsto_optThreshold_atTop : Tendsto (fun n : ℕ => optThreshold n) atTop atTop := by unfold optThreshold exact tendsto_nat_floor_atTop.comp tendsto_div_e0_atTop

⌊n/e⌋ / n tends to 1/e.

lemma tendsto_optThreshold_div_n : Tendsto (fun n : ℕ => (optThreshold n : ℝ) / (n : ℝ)) atTop (𝓝 (1 / e0)) := by let x : ℕ → ℝ := fun n => (n : ℝ) / e0 have hx_atTop : Tendsto x atTop atTop := tendsto_div_e0_atTop have hf : Tendsto (fun n : ℕ => (⌊x n⌋₊ : ℝ) / x n) atTop (𝓝 1) := tendsto_nat_floor_div_atTop.comp hx_atTop have hg : Tendsto (fun n : ℕ => x n / (n : ℝ)) atTop (𝓝 (1 / e0)) := by have h : (fun n : ℕ => x n / (n : ℝ)) =ᶠ[atTop] fun _ : ℕ => 1 / e0 := by filter_upwards [eventually_ge_atTop 1] with n hn unfold x field_simp [e0_ne_zero, (show (n : ℝ) ≠ 0 from by exact_mod_cast (Nat.ne_of_gt hn))] exact (tendsto_const_nhds : Tendsto (fun _ : ℕ => 1 / e0) atTop (𝓝 (1 / e0))).congr' h.symm have hmul : Tendsto (fun n : ℕ => (⌊x n⌋₊ : ℝ) / x n * (x n / (n : ℝ))) atTop (𝓝 (1 * (1 / e0))) := hf.mul hg have hid : (fun n : ℕ => (⌊x n⌋₊ : ℝ) / x n * (x n / (n : ℝ))) =ᶠ[atTop] fun n : ℕ => (optThreshold n : ℝ) / (n : ℝ) := by filter_upwards [eventually_ge_atTop 1] with n hn have hx0 : x n ≠ 0 := by unfold x exact div_ne_zero (by exact_mod_cast (Nat.ne_of_gt hn)) e0_ne_zero field_simp [hx0, (show (n : ℝ) ≠ 0 from by exact_mod_cast (Nat.ne_of_gt hn))] unfold optThreshold x ring simpa using hmul.congr' hid

log (n - 1) - log n tends to 0.

lemma tendsto_log_pred_sub_log : Tendsto (fun n : ℕ => Real.log (n - 1 : ℕ) - Real.log (n : ℝ)) atTop (𝓝 0) := by have h := Real.tendsto_log_comp_add_sub_log (-1 : ℝ) have h' : Tendsto (fun n : ℕ => Real.log ((n : ℝ) - 1) - Real.log (n : ℝ)) atTop (𝓝 0) := h.comp tendsto_natCast_atTop_atTop have hid : (fun n : ℕ => Real.log ((n : ℝ) - 1) - Real.log (n : ℝ)) =ᶠ[atTop] fun n : ℕ => Real.log (n - 1 : ℕ) - Real.log (n : ℝ) := by filter_upwards [eventually_ge_atTop 1] with n hn have hcast : ((n : ℝ) - 1) = (n - 1 : ℕ) := by rw [Nat.cast_sub hn] norm_num rw [hcast] exact h'.congr' hid

log (n - 1) - log n over the threshold tends to 0.

lemma tendsto_log_opt_pred_sub_log : Tendsto (fun n : ℕ => Real.log (optThreshold n - 1 : ℕ) - Real.log (optThreshold n : ℝ)) atTop (𝓝 0) := by have h := Real.tendsto_log_comp_add_sub_log (-1 : ℝ) have h' : Tendsto (fun n : ℕ => Real.log ((n : ℝ) - 1) - Real.log (n : ℝ)) atTop (𝓝 0) := h.comp tendsto_natCast_atTop_atTop have hcomp : Tendsto (fun n : ℕ => Real.log ((optThreshold n : ℝ) - 1) - Real.log (optThreshold n : ℝ)) atTop (𝓝 0) := h'.comp tendsto_optThreshold_atTop have hid : (fun n : ℕ => Real.log ((optThreshold n : ℝ) - 1) - Real.log (optThreshold n : ℝ)) =ᶠ[atTop] fun n : ℕ => Real.log (optThreshold n - 1 : ℕ) - Real.log (optThreshold n : ℝ) := by filter_upwards [tendsto_optThreshold_atTop.eventually_gt_atTop 0] with n hn have hcast : ((optThreshold n : ℝ) - 1) = (optThreshold n - 1 : ℕ) := by rw [Nat.cast_sub hn] norm_num rw [hcast] exact hcomp.congr' hid

log n - log ⌊n/e⌋ tends to 1.

lemma tendsto_log_sub_log_opt : Tendsto (fun n : ℕ => Real.log (n : ℝ) - Real.log (optThreshold n : ℝ)) atTop (𝓝 1) := by have hn : Tendsto (fun n : ℕ => (n : ℝ) / (optThreshold n : ℝ)) atTop (𝓝 e0) := by have h := tendsto_optThreshold_div_n -- inverse of k/n → 1/e0 is n/k → e0 have hinv : Tendsto (fun n : ℕ => (((optThreshold n : ℝ) / (n : ℝ))⁻¹)) atTop (𝓝 (1 / e0)⁻¹) := h.inv₀ (ne_of_gt (one_div_pos.mpr e0_pos)) have hb : (1 / e0)⁻¹ = e0 := by field_simp [e0_ne_zero] -- (k/n)⁻¹ = n/k have hid : (fun n : ℕ => (((optThreshold n : ℝ) / (n : ℝ))⁻¹)) =ᶠ[atTop] fun n : ℕ => (n : ℝ) / (optThreshold n : ℝ) := by filter_upwards [eventually_ge_atTop 1, tendsto_optThreshold_atTop.eventually_gt_atTop 0] with n hn hk field_simp [(show (optThreshold n : ℝ) ≠ 0 from by exact_mod_cast (Nat.ne_of_gt hk)), (show (n : ℝ) ≠ 0 from by exact_mod_cast (Nat.ne_of_gt hn))] have hgoal : Tendsto (fun n : ℕ => (n : ℝ) / (optThreshold n : ℝ)) atTop (𝓝 ((1 / e0)⁻¹)) := hinv.congr' hid rw [hb] at hgoal exact hgoal -- log(n/k) → log e0 = 1 have hlog : Tendsto (fun n : ℕ => Real.log ((n : ℝ) / (optThreshold n : ℝ))) atTop (𝓝 (Real.log e0)) := (ContinuousAt.tendsto (Real.continuousAt_log e0_ne_zero)).comp hn have hid : (fun n : ℕ => Real.log ((n : ℝ) / (optThreshold n : ℝ))) =ᶠ[atTop] fun n : ℕ => Real.log (n : ℝ) - Real.log (optThreshold n : ℝ) := by filter_upwards [eventually_ge_atTop 1, tendsto_optThreshold_atTop.eventually_gt_atTop 0] with n hn hk rw [Real.log_div (by exact_mod_cast (Nat.ne_of_gt hn)) (by exact_mod_cast (Nat.ne_of_gt hk))] simpa [log_e0] using hlog.congr' hid

log (n-1) - log ⌊n/e⌋-1 tends to 1.

lemma tendsto_log_pred_sub_log_opt : Tendsto (fun n : ℕ => Real.log (n - 1 : ℕ) - Real.log (optThreshold n - 1 : ℕ)) atTop (𝓝 1) := by -- decompose: (log(n-1)-log n) + (log n - log k) + (log k - log(k-1)) have h1 := tendsto_log_pred_sub_log have h2 := tendsto_log_sub_log_opt have h3 : Tendsto (fun n : ℕ => Real.log (optThreshold n : ℝ) - Real.log (optThreshold n - 1 : ℕ)) atTop (𝓝 0) := by have h := tendsto_log_opt_pred_sub_log simpa using h.neg have hsum : Tendsto (fun n : ℕ => (Real.log (n - 1 : ℕ) - Real.log (n : ℝ)) + (Real.log (n : ℝ) - Real.log (optThreshold n : ℝ)) + (Real.log (optThreshold n : ℝ) - Real.log (optThreshold n - 1 : ℕ))) atTop (𝓝 (0 + 1 + 0)) := (h1.add h2).add h3 have hid : (fun n : ℕ => (Real.log (n - 1 : ℕ) - Real.log (n : ℝ)) + (Real.log (n : ℝ) - Real.log (optThreshold n : ℝ)) + (Real.log (optThreshold n : ℝ) - Real.log (optThreshold n - 1 : ℕ))) =ᶠ[atTop] fun n : ℕ => Real.log (n - 1 : ℕ) - Real.log (optThreshold n - 1 : ℕ) := by filter_upwards with n ring simpa using hsum.congr' hid

H_{n-1} - H_{⌊n/e⌋-1} tends to 1.

lemma tendsto_harmonic_diff : Tendsto (fun n : ℕ => (harmonic (n - 1) : ℝ) - (harmonic (optThreshold n - 1) : ℝ)) atTop (𝓝 1) := by let γ : ℝ := Real.eulerMascheroniConstant have hpred : Tendsto (fun n : ℕ => n - 1) atTop atTop := by rw [tendsto_atTop] intro m filter_upwards [eventually_ge_atTop (m + 1)] with n hn omega have hpred_opt : Tendsto (fun n : ℕ => optThreshold n - 1) atTop atTop := hpred.comp tendsto_optThreshold_atTop have h_n : Tendsto (fun n : ℕ => (harmonic (n - 1) : ℝ) - Real.log (n - 1 : ℕ)) atTop (𝓝 γ) := by have h := Real.tendsto_harmonic_sub_log.comp hpred change Tendsto (fun n : ℕ => (harmonic (n - 1) : ℝ) - Real.log (↑(n - 1) : ℝ)) atTop (𝓝 γ) exact h have h_k : Tendsto (fun n : ℕ => (harmonic (optThreshold n - 1) : ℝ) - Real.log (optThreshold n - 1 : ℕ)) atTop (𝓝 γ) := by have h := Real.tendsto_harmonic_sub_log.comp hpred_opt change Tendsto (fun n : ℕ => (harmonic (optThreshold n - 1) : ℝ) - Real.log (↑(optThreshold n - 1) : ℝ)) atTop (𝓝 γ) exact h have h_log := tendsto_log_pred_sub_log_opt have hcomb : Tendsto (fun n : ℕ => ((harmonic (n - 1) : ℝ) - Real.log (n - 1 : ℕ)) - ((harmonic (optThreshold n - 1) : ℝ) - Real.log (optThreshold n - 1 : ℕ)) + (Real.log (n - 1 : ℕ) - Real.log (optThreshold n - 1 : ℕ))) atTop (𝓝 (γ - γ + 1)) := (h_n.sub h_k).add h_log have hid : (fun n : ℕ => ((harmonic (n - 1) : ℝ) - Real.log (n - 1 : ℕ)) - ((harmonic (optThreshold n - 1) : ℝ) - Real.log (optThreshold n - 1 : ℕ)) + (Real.log (n - 1 : ℕ) - Real.log (optThreshold n - 1 : ℕ))) =ᶠ[atTop] fun n : ℕ => (harmonic (n - 1) : ℝ) - (harmonic (optThreshold n - 1) : ℝ) := by filter_upwards with n ring simpa using hcomb.congr' hid

On-line hiring 1/e asymptotic. Choosing the threshold k = ⌊n/e⌋ makes the success probability tend to 1/e as n → ∞ (CLRS §5.4.4).

try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` theorem probHireBest_asymptotic : Tendsto (fun n : ℕ => probHireBest n (optThreshold n)) atTop (𝓝 (1 / e0)) := by have hk_pos : ∀ᶠ n in atTop, 0 < optThreshold n := tendsto_optThreshold_atTop.eventually_gt_atTop 0 have hk_le : ∀ᶠ n in atTop, optThreshold n ≤ n := by filter_upwards [eventually_ge_atTop 1] with n hn unfold optThreshold have h1 : (⌊(n : ℝ) / e0⌋₊ : ℝ) ≤ (n : ℝ) / e0 := Nat.floor_le (div_nonneg (by positivity) (le_of_lt e0_pos)) have h2 : (n : ℝ) / e0 ≤ (n : ℝ) := by have he1 : 1 ≤ e0 := by have hlt : (1 : ℝ) < e0 := by unfold e0 try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa using (Real.exp_lt_exp.mpr (by 'norm_num' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false`this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false`norm_num : (0 : ℝ) < 1)) exact le_of_lt hlt exact (div_le_iff₀ e0_pos).mpr (by nlinarith [he1]) exact_mod_cast (le_trans h1 h2) have hclosed : (fun n : ℕ => probHireBest n (optThreshold n)) =ᶠ[atTop] fun n : ℕ => (optThreshold n : ℝ) / (n : ℝ) * ((harmonic (n - 1) : ℝ) - (harmonic (optThreshold n - 1) : ℝ)) := by filter_upwards [hk_pos, hk_le] with n hpos hle rw [probHireBest_eq n (optThreshold n) hpos hle] have ht : Tendsto (fun n : ℕ => (optThreshold n : ℝ) / (n : ℝ) * ((harmonic (n - 1) : ℝ) - (harmonic (optThreshold n - 1) : ℝ))) atTop (𝓝 ((1 / e0) * 1)) := tendsto_optThreshold_div_n.mul tendsto_harmonic_diff have hfinal : (1 / e0) * 1 = 1 / e0 := by ring simpa [hfinal] using ht.congr' hclosed.symm
endend OnlineHiringend Chapter05end CLRS

Scope and implementation notes

Imports
import CLRSLean.FourthEdition.Chapter_05.Section_05_1_Hiring_Problem import CLRSLean.FourthEdition.Chapter_05.Section_05_2_Indicator_Random_Variables import CLRSLean.FourthEdition.Chapter_05.Section_05_2_Indicator_Expectation import CLRSLean.FourthEdition.Chapter_05.Section_05_3_Randomized_Algorithms import CLRSLean.FourthEdition.Chapter_05.Section_05_3_Randomized_Hiring import CLRSLean.FourthEdition.Chapter_05.Section_05_3_Randomized_Hiring.ExpectationBridge import CLRSLean.FourthEdition.Chapter_05.Section_05_4_Probabilistic_Analysis import CLRSLean.FourthEdition.Chapter_05.Section_05_4_Probabilistic_Analysis.OnlineHiring

Native fourth-edition chapter guide.

Current source

This guide sources fourth-edition §5.1–§5.4 from the native section modules under CLRSLean.FourthEdition.Chapter_05. Declarations retain the CLRS.Chapter05 namespace; the legacy import CLRSLean.Chapter_05 and its Section_05_* modules forward to these sources during the compatibility period.

The hiring problem studies the expected number of times a new best candidate is hired in a random interview order. Section 5.1 proves the finite rank-symmetry calculation that the step probability is 1/(n+1), sums the indicator expectations, proves the equivalent recurrence solution, derives the logarithmic asymptotic growth of the expected number of hires, and formalizes the executable HIRE-ASSISTANT pseudocode (CLRS.Chapter05.hireAssistant) with its one-step record-counting recurrence.

Section 5.2 formalizes the indicator random variable technique and linearity of expectation with the hat-check problem (expected fixed points of a uniform random permutation of Fin n equal 1). Its textbook boundary also exposes CLRS.Chapter05.indicator_expectation_eq_probability: the expectation of an event indicator is its finite-uniform probability.

Section 5.3 proves the central result of CLRS §5.3: the RANDOMIZE-IN-PLACE procedure (Fisher–Yates shuffle) yields a uniform random permutation of Fin n (Lemma 5.4). The functional implementation CLRS.Chapter05.fisherYates recursively performs one explicit placement swap and continues on the remaining suffix. Its equations are packaged as CLRS.Chapter05.fisherYates_succ_invariant; the current selection is uniform by CLRS.Chapter05.fisherYates_first_uniform, and the completed permutation is uniform by CLRS.Chapter05.fisherYates_uniform. The public randomizeInPlace name is pointwise equal to this executable definition, not merely distributionally equivalent. The companion CLRS.Chapter05.randomizedHireAssistant composes that randomization with the executable hiring loop. The exact transport theorem CLRS.Chapter05.randomizedExpectedHiringCost_eq_uniform moves its expected cost to the uniform-permutation space. The companion record-indicator proof then identifies the executable counter with a sum of prefix-record events, proves that the event at position i has probability 1/(i+1), and closes the expectation bridge as CLRS.Chapter05.hiringExpectationBridge. Consequently CLRS.Chapter05.randomizedExpectedHiringCost_isBigO_log is premise-free.

Section 5.4 applies indicators plus independence to two classic probabilistic analyses: the birthday paradox (expected number of same-birthday pairs is k(k-1)/(2n)) and balls and bins (expected number of balls in a fixed bin is k/n). It also proves the longest streak result that the expected longest run of heads in n fair coin flips is Θ(log n) — upper bound E[L] ≤ log₂ n + 2 and lower bound E[L] ≥ log₂ n / 8 for n ≥ 16. Its on-line hiring model provides an executable threshold strategy over finite permutations, the finite success probability CLRS.Chapter05.OnlineHiring.probHireBest, its harmonic closed form (k/n)(H_{n-1} - H_{k-1}), and the asymptotic 1/e success probability for the threshold ⌊n/e⌋.

  • Section 5.1: proved for the finite rank-symmetry model, including CLRS.Chapter05.expectedHires_isBigTheta_log.

  • Section 5.2: proved for the uniform-permutation model, including CLRS.Chapter05.indicator_expectation_eq_probability and CLRS.Chapter05.expectedFixedPoints_eq_one.

  • Section 5.3: proved for the executable independent-swap-choice model, including the recursive placement invariant (CLRS.Chapter05.fisherYates_succ_invariant), current-choice uniformity (CLRS.Chapter05.fisherYates_first_uniform), and completed-permutation uniformity (CLRS.Chapter05.randomizeInPlace_uniform, Lemma 5.4), plus the exact randomized-hiring transport to the uniform-permutation expectation, the executable record-count identity (CLRS.Chapter05.hireAssistant_eq_sum_prefixRecordIndicators), the prefix-record probability (CLRS.Chapter05.prefixRecord_probability), and the resulting harmonic expectation and logarithmic expected-cost bound.

  • Section 5.4: proved for the product-uniform birthday and balls-and-bins models (CLRS.Chapter05.expectedCollisions_eq, CLRS.Chapter05.expectedBallsInBin_eq), the longest-streak Θ(log n) bounds (CLRS.Chapter05.expectedLongestStreak_le, CLRS.Chapter05.expectedLongestStreak_lowerBound), and on-line hiring, whose success probability has the harmonic closed form (CLRS.Chapter05.OnlineHiring.probHireBest_eq) and the 1/e asymptotic (CLRS.Chapter05.OnlineHiring.probHireBest_asymptotic).

Coverage boundary

The represented finite-probability developments are reused under the unchanged chapter number.

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 5 of 35