Grace/Cumulus/Probability/Birthday.g17

Open in Workbench Download source

Imports

Uniform · Combinatorics.FallingBounds · Real.Metric

Declarations

Source

1-- The birthday problem2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Probability.Birthday8import Uniform9import Combinatorics.FallingBounds10import Real.Metric1112-- An assignment of birthdays to the people of A from the days of B is a13-- function A → B. Under the assignments outside the injections, two14-- people share a birthday.15def sharedBirthday (A B : Set) : Set :=16  functionSpace(A, B) ∖ injections(A, B)1718theorem sharedBirthday.value (A B : Set)19  shows sharedBirthday(A, B) = functionSpace(A, B) ∖ injections(A, B)20proof21  simp [sharedBirthday]2223theorem sharedBirthday.membership (f A B : Set)24  shows f ∈ sharedBirthday(A, B) ↔25    (f : A → B) ∧ (∃ x ∈ A, ∃ y ∈ A, x ≠ y ∧ f(x) = f(y))26proof27  rw sharedBirthday.value28  constructor29  . intro member30    obtain ⟨inSpace, notInjective⟩ :=31      difference.membership.forward with member32    have function := functionSpace.mem_iff.forward with inSpace33    refine ⟨function, ?_⟩34    by_contra none35    apply notInjective36    have cancel : ∀ x ∈ A, ∀ y ∈ A, f(x) = f(y) → x = y37      intros x hx y hy same38      by_contra different39      apply none40      exact ⟨x, hx, y, hy, different, same⟩41    have injective := Injective.of_pointwise with function, cancel42    exact injections.of_injective with injective43  . intro shape44    obtain ⟨function, x, hx, y, hy, different, same⟩ := shape45    have inSpace := functionSpace.mem_iff.backward with function46    have notInjective : ¬(f ∈ injections(A, B))47      intro member48      have injective := injections.injective with member49      have equal := Injective.apply_cancel with injective, hx, hy, same50      exact different with equal51    have both : f ∈ functionSpace(A, B) ∧ ¬(f ∈ injections(A, B)) :=52      ⟨inSpace, notInjective⟩53    exact difference.membership.backward with both5455theorem sharedBirthday.subset (A B : Set)56  shows sharedBirthday(A, B) ⊆ functionSpace(A, B)57proof58  rw sharedBirthday.value59  exact difference.subset_left at functionSpace(A, B), injections(A, B)6061-- The counting fact: the injective assignments of 365 days to 23 people62-- are fewer than half of all assignments. The difference between all63-- assignments and twice the injective ones is a 58-digit natural, written64-- in two blocks of thirty digits so that it is typed as a natural.65theorem birthday.counting66  shows 2 * fallingFactorial(365, 23) < 365 ^ 2367proof68  have gap : 2 * fallingFactorial(365, 23) + 1 +69      (1250040748965601492022941694 * 1000000000000000000000000000000 +70        577238181855100962491293453124) = 365 ^ 23 by compute71  have grow := LessEqual.add_right at 2 * fallingFactorial(365, 23) + 1,72    1250040748965601492022941694 * 1000000000000000000000000000000 +73      57723818185510096249129345312474  rw gap at grow75  exact Less.of_add_one_le with grow7677theorem birthday.injections (A B : Set)78  requires finiteA : Finite(A)79  requires finiteB : Finite(B)80  requires people : cardinality(A) = 2381  requires days : cardinality(B) = 36582  shows 2 * cardinality(injections(A, B)) < cardinality(functionSpace(A, B))83proof84  have left := injections.count with finiteA, finiteB85  have right := functionSpace.count with finiteA, finiteB86  rw [left, right, people, days]87  exact birthday.counting8889-- The probability that two of n people share one of d birthdays, under90-- the uniform distribution on all assignments, is91-- 1 - d(d - 1)⋯(d - n + 1) / dⁿ.92theorem sharedBirthday.probability (A B : Set)93  requires finiteA : Finite(A)94  requires finiteB : Finite(B)95  requires inhabited : Nonempty(B)96  shows prob(uniformWeight(functionSpace(A, B)), sharedBirthday(A, B)) =97    (1:R) - (realNat(fallingFactorial(cardinality(B), cardinality(A))):R) /98      (realNat(cardinality(B) ^ cardinality(A)):R)99proof100  have finite := functionSpace.finite with finiteA, finiteB101  have spaceInhabited := functionSpace.nonempty at A, B with inhabited102  have event := injections.subset at A, B103  have complement := prob.uniform_complement with finite, spaceInhabited, event104  have left := injections.count with finiteA, finiteB105  have right := functionSpace.count with finiteA, finiteB106  rw sharedBirthday.value107  rw complement108  rw [realSize.value, realSize.value, left, right]109  rfl110111-- The birthday problem: among 23 people with uniformly random birthdays112-- in a year of 365 days, two share a birthday with probability above 1/2.113theorem birthday.problem (A B : Set)114  requires finiteA : Finite(A)115  requires finiteB : Finite(B)116  requires people : cardinality(A) = 23117  requires days : cardinality(B) = 365118  shows (1:R) / 2 <119    (prob(uniformWeight(functionSpace(A, B)), sharedBirthday(A, B)):R)120proof121  have positiveDays : 0 < cardinality(B)122    rw days123    arith124  have characterization := cardinality.positive_iff_nonempty with finiteB125  have inhabited := characterization.backward with positiveDays126  have formula := sharedBirthday.probability with finiteA, finiteB, inhabited127  rw [people, days] at formula128  rw formula129  have counting := birthday.counting130  have bound := Less.add_one_le_of_lt with counting131  have scaled := realNat.le_of_natural_le with bound132  have two := realNumeral.nat at 2133  rw [realNat.add, realNat.mul, realNat.one] at scaled134  rw ← two at scaled135  have numeratorReal := realNat.real at fallingFactorial(365, 23)136  have denominatorReal := realNat.real at 365 ^ 23137  have nonnegative := realNat.zero_le at fallingFactorial(365, 23)138  have positive : (0:R) < realNat(365 ^ 23) by linarith139  have strict : 2 * realNat(fallingFactorial(365, 23)) < realNat(365 ^ 23)140    linarith141  have half := realDiv.lt_half with positive, strict142  have twice := realHalf.add_self143  linarith144