Birthday Problem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

theorem theorems_100.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.

source

@[protected, instance]

def theorems_100.fin.measurable_space {m : ℕ} :

measurable_space (fin m)

Equations

theorems_100.fin.measurable_space = ⊤

source

@[protected, instance]

def theorems_100.fin.measurable_singleton_class {m : ℕ} :

measurable_singleton_class (fin m)

source

@[protected, instance]

noncomputable def theorems_100.pi.measure_theory.measure_space {n m : ℕ} :

measure_theory.measure_space (fin n → fin m)

Equations

theorems_100.pi.measure_theory.measure_space = {to_measurable_space := measurable_space.pi (λ (a : fin n), theorems_100.fin.measurable_space), volume := probability_theory.cond_count set.univ}

source

@[protected, instance]

def theorems_100.measure_theory.measure_space.volume.measure_theory.is_probability_measure {n m : ℕ} :

measure_theory.is_probability_measure measure_theory.measure_space.volume

source

theorem theorems_100.fin_fin.measure_apply {n m : ℕ} {s : set (fin n → fin m)} :

⇑measure_theory.measure_space.volume s = ↑(_.to_finset.card) / ↑(fintype.card (fin n → fin m))

source

theorem theorems_100.birthday_measure :

⇑measure_theory.measure_space.volume {f : fin 23 → fin 365 | function.injective f} < 1 / 2

Birthday Problem: first probabilistic interpretation.