CLRS-Lean
CLRS Fourth Edition
Chapter 5. Probabilistic Analysis and Randomized Algorithms
5.2. Indicator random variables

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