Birthday Problem

This file proves Theorem 93 from the 100 Theorems List.

As opposed to the standard probabilistic statement, we instead state the birthday problem in terms of injective functions. The general result about Fintype.card (α ↪ β) which this proof uses is Fintype.card_embedding_eq.

theorem Theorems100.birthday : 2 * Fintype.card (Fin 23 ↪ Fin 365) < Fintype.card (Fin 23 → Fin 365) ∧ 2 * Fintype.card (Fin 22 ↪ Fin 365) > Fintype.card (Fin 22 → Fin 365)

Birthday Problem: set cardinality interpretation.

instance Theorems100.instMeasurableSpaceFin_archive {m : ℕ} : MeasurableSpace (Fin m)

Equations

• Theorems100.instMeasurableSpaceFin_archive = ⊤

instance Theorems100.instMeasurableSingletonClassFin_archive {m : ℕ} : MeasurableSingletonClass (Fin m)

Equations

• ⋯ = ⋯

noncomputable instance Theorems100.instMeasureSpaceForallFin_archive {n : ℕ} {m : ℕ} : MeasureTheory.MeasureSpace (Fin n → Fin m)

Equations

• Theorems100.instMeasureSpaceForallFin_archive = MeasureTheory.MeasureSpace.mk (ProbabilityTheory.condCount Set.univ)

instance Theorems100.instIsProbabilityMeasureForallFinHAddNatOfNatVolume_archive {n : ℕ} {m : ℕ} : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

Equations

• ⋯ = ⋯

theorem Theorems100.FinFin.measure_apply {n : ℕ} {m : ℕ} {s : Set (Fin n → Fin m)} : MeasureTheory.volume s = ↑⋯.toFinset.card / ↑(Fintype.card (Fin n → Fin m))

theorem Theorems100.birthday_measure : MeasureTheory.volume {f : Fin 23 → Fin 365 | Function.Injective f} < 1 / 2

Birthday Problem: first probabilistic interpretation.