feat(archive/birthday): improve birthday problem (#16528)

This adds a measure-theoretic interpretation of the birthday problem; not yet the one with independent uniform random variables, but some form of a step in that direction.

It also removes a misleading statement from the YAML to make it clearer that `card_embedding_eq` is not all the work done on the Birthday problem on mathlib. cc @digama0



Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

Author: ericrbg

archive/100-theorems-list/93_birthday_problem.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 -/
 import data.fintype.card_embedding
-import tactic.norm_num
+import probability.cond_count
+import probability.notation
 
 /-!
 # Birthday Problem
@@ -16,12 +17,69 @@ in terms of injective functions. The general result about `fintype.card (α ↪
 uses is `fintype.card_embedding_eq`.
 -/
 
-local notation `‖` x `‖` := fintype.card x
+local notation (name := finset.card)  `|` x `|` := finset.card x
+local notation (name := fintype.card) `‖` x `‖` := fintype.card x
 
-/-- **Birthday Problem** -/
+/-- **Birthday Problem**: set cardinality interpretation. -/
 theorem birthday :
   2 * ‖fin 23 ↪ fin 365‖ < ‖fin 23 → fin 365‖ ∧ 2 * ‖fin 22 ↪ fin 365‖ > ‖fin 22 → fin 365‖ :=
 begin
   simp only [nat.desc_factorial, fintype.card_fin, fintype.card_embedding_eq, fintype.card_fun],
   norm_num
 end
+
+section measure_theory
+
+open measure_theory probability_theory
+open_locale probability_theory ennreal
+
+variables {n m : ℕ}
+
+/- In order for Lean to understand that we can take probabilities in `fin 23 → fin 365`, we must
+tell Lean that there is a `measurable_space` structure on the space. Note that this instance
+is only for `fin m` - Lean automatically figures out that the function space `fin n → fin m`
+is _also_ measurable, by using `measurable_space.pi` -/
+
+instance : measurable_space (fin m) := ⊤
+
+/- We then endow the space with a canonical measure, which is called ℙ.
+We define this to be the conditional counting measure. -/
+noncomputable instance : measure_space (fin n → fin m) := ⟨cond_count set.univ⟩
+
+-- Singletons are measurable; therefore, as `fin n → fin m` is finite, all sets are measurable.
+instance : measurable_singleton_class (fin n → fin m) :=
+⟨λ f, begin
+  convert measurable_set.pi set.finite_univ.countable
+    (show ∀ i, i ∈ set.univ → measurable_set ({f i} : set (fin m)), from λ _ _, trivial),
+  ext g,
+  simp only [function.funext_iff, set.mem_singleton_iff, set.mem_univ_pi],
+end⟩
+
+/- The canonical measure on `fin n → fin m` is a probability measure (except on an empty space). -/
+example : is_probability_measure (ℙ : measure (fin n → fin (m + 1))) :=
+cond_count_is_probability_measure set.finite_univ set.univ_nonempty
+
+lemma fin_fin.measure_apply {s : set $ fin n → fin m} :
+  ℙ s = (|s.to_finite.to_finset|) / ‖fin n → fin m‖ :=
+by erw [cond_count_univ, measure.count_apply_finite]
+
+/-- **Birthday Problem**: first probabilistic interpretation. -/
+theorem birthday_measure : ℙ {f : fin 23 → fin 365 | function.injective f} < 1 / 2 :=
+begin
+  -- most of this proof is essentially converting it to the same form as `birthday`.
+  rw [fin_fin.measure_apply],
+  generalize_proofs hfin,
+  have : |hfin.to_finset| = 42200819302092359872395663074908957253749760700776448000000,
+  { transitivity ‖fin 23 ↪ fin 365‖,
+    { simp_rw [←fintype.card_coe, set.finite.coe_sort_to_finset, set.coe_set_of],
+      exact fintype.card_congr (equiv.subtype_injective_equiv_embedding _ _) },
+    { simp only [fintype.card_embedding_eq, fintype.card_fin, nat.desc_factorial],
+      norm_num } },
+  rw [this, ennreal.lt_div_iff_mul_lt, mul_comm, mul_div, ennreal.div_lt_iff],
+  rotate, iterate 2 { right, norm_num }, iterate 2 { left, norm_num },
+  norm_cast,
+  simp only [fintype.card_pi, fintype.card_fin],
+  norm_num
+end
+
+end measure_theory

docs/100.yaml

@@ -379,7 +379,6 @@
   title  : Pick’s Theorem
 93:
   title  : The Birthday Problem
-  decl   : fintype.card_embedding_eq
   links  :
     mathlib archive: https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/93_birthday_problem.lean
   author : Eric Rodriguez

src/data/set/finite.lean

@@ -141,6 +141,10 @@ by rw [← finset.coe_sort_coe _, h.coe_to_finset]
 @[simp] lemma finite_empty_to_finset (h : (∅ : set α).finite) : h.to_finset = ∅ :=
 by rw [← finset.coe_inj, h.coe_to_finset, finset.coe_empty]
 
+@[simp] lemma finite_univ_to_finset [fintype α] (h : (set.univ : set α).finite) :
+  h.to_finset = finset.univ :=
+finset.ext $ by simp
+
 @[simp] lemma finite.to_finset_inj {s t : set α} {hs : s.finite} {ht : t.finite} :
   hs.to_finset = ht.to_finset ↔ s = t :=
 by simp only [←finset.coe_inj, finite.coe_to_finset]

src/measure_theory/measure/measure_space.lean

@@ -2337,6 +2337,10 @@ begin
   exact ne_of_lt (measure_lt_top _ _)
 end
 
+instance [finite α] [measurable_space α] : is_finite_measure (measure.count : measure α) :=
+⟨by { casesI nonempty_fintype α,
+      simpa [measure.count_apply, tsum_fintype] using (ennreal.nat_ne_top _).lt_top }⟩
+
 end is_finite_measure
 
 section is_probability_measure

src/probability/cond_count.lean

@@ -62,6 +62,16 @@ begin
   simpa [cond_count, cond, measure.count_apply_infinite hs'] using h,
 end
 
+lemma cond_count_univ [fintype Ω] {s : set Ω} :
+  cond_count set.univ s = measure.count s / fintype.card Ω :=
+begin
+  rw [cond_count, cond_apply _ measurable_set.univ, ←ennreal.div_eq_inv_mul, set.univ_inter],
+  congr',
+  rw [←finset.coe_univ, measure.count_apply, finset.univ.tsum_subtype' (λ _, (1 : ennreal))],
+  { simp [finset.card_univ] },
+  { exact (@finset.coe_univ Ω _).symm ▸ measurable_set.univ }
+end
+
 variables [measurable_singleton_class Ω]
 
 lemma cond_count_is_probability_measure {s : set Ω} (hs : s.finite) (hs' : s.nonempty) :
@@ -126,7 +136,7 @@ lemma cond_count_eq_zero_iff (hs : s.finite) :
 by simp [cond_count, cond_apply _ hs.measurable_set, measure.count_apply_eq_top,
     set.not_infinite.2 hs, measure.count_apply_finite _ (hs.inter_of_left _)]
 
-lemma cond_count_univ (hs : s.finite) (hs' : s.nonempty) :
+lemma cond_count_of_univ (hs : s.finite) (hs' : s.nonempty) :
   cond_count s set.univ = 1 :=
 cond_count_eq_one_of hs hs' s.subset_univ