Revision #3039 → #3563 · back to history
modifiedBirthday problem5818e3c78edc
| Field | From #3039 | To #3563 |
|---|
| note | No formalization of the birthday problem appears in Mathlib (grep for 'Birthday' returns nothing). | No formalization of the birthday problem appears in Mathlib (grep for 'birthday' returns no hits). |
modifiedBirthday paradox (23 people)b776a4744123
| Field | From #3039 | To #3563 |
|---|
| note | The 23-person threshold is not proved in Mathlib. | The 23-person 50% threshold is not proved in Mathlib. |
addedBirthday attack0ad3261afa6e
modifiedEvents A and B8a96a2ec42b0
| Field | From #3039 | To #3563 |
|---|
| note | These birthday events are not defined in Mathlib. | The specific birthday events A and B are not defined in Mathlib. |
modifiedComplementary probability relation1b6cde6d1e6b
| Field | From #3039 | To #3563 |
|---|
| mathlib.module | Mathlib.MeasureTheory.Measure.MeasureSpace | Mathlib.MeasureTheory.Measure.Typeclasses.Probability |
| note | General complement-probability identities exist in Mathlib but not specialized to the birthday events. | The general complement-probability identity `μ sᶜ = 1 - μ s` is in Mathlib, but not specialized to the birthday events. |
modifiedGeneral formula for p(n)66d8cafecb60
| Field | From #3039 | To #3563 |
|---|
| note | Mathlib counts injections as descFactorial (the numerator of the no-collision probability) but does not state the birthday probability formula. | Mathlib counts injections via `Fintype.card_embedding_eq` (the numerator of the no-collision probability) but does not state the birthday probability formula. |
modifiedPigeonhole boundfab3b419e178
| Field | From #3039 | To #3563 |
|---|
| mathlib.decl | Fintype.card_embedding_eq_of_infinite | Finset.exists_ne_map_eq_of_card_lt_of_maps_to |
| mathlib.module | Mathlib.Data.Fintype.CardEmbedding | Mathlib.Data.Finset.Basic |
| note | The pigeonhole principle is formalized in Mathlib (e.g. `Finset.exists_ne_map_eq_of_card_lt_of_maps_to`), but the birthday-specific consequence is not stated. | Mathlib formalizes the pigeonhole principle in general (e.g. `Finset.exists_ne_map_eq_of_card_lt_of_maps_to`), but the birthday-specific consequence is not stated. |
| provenance | ai | ai-moderated |
modifiedTaylor series first-order approximation2687010eb411
| Field | From #3039 | To #3563 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Exp | Mathlib.Analysis.Complex.Exponential |
| note | Mathlib has the inequality `1 + x ≤ exp x` and exponential Taylor series; the birthday-context use is not stated. | Mathlib has the inequality `x + 1 ≤ exp x` as `Real.add_one_le_exp`; its birthday-context use is not stated. |
modifiedSimple exponentiation approximation3e04cdf156d7
| Field | From #3039 | To #3563 |
|---|
| note | This independence-based approximation is not formalized. | This independence-based birthday approximation is not formalized. |
modifiedPoisson approximation37325d006cbd
| Field | From #3039 | To #3563 |
|---|
| note | Mathlib has the Poisson distribution but not the Poisson approximation to the binomial for birthdays. | Mathlib has the Poisson distribution but no Poisson-to-binomial approximation for the birthday setup. |
modified23 people suffice0e21026f6499
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedGeneralized birthday problem n(d)6a65572cffd9
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedBounds on n(d)a87b5a5e7c9c
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedAsymptotic optimality of boundsd75a0d88f88e
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedFormula holds for 73% of integers9c3198e2f74b
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedFormula holds for almost all d944eeb674238
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedConjecture with counterexamplesc07049edba52
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedConjectured formula for all d28b5b818d90a
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modified3 and 4 person sharing thresholds32bebcbc9b20
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedStrong birthday problem6b714dfcc5be
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedCollision probability p(n;d)7c3e162b8bc1
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedHash collision expected count4b57ea5c5ea7
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedProbability of exactly one matching pair24f40229a4b0
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedMaximum of unique-match probabilityfd9faba38b8c
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedTwo-types generalization probabilityb782f96aa28b
| Field | From #3039 | To #3563 |
|---|
| mathlib.decl | — | Nat.stirlingSecond |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Combinatorics.Enumerative.Stirling |
| note | Not formalized. | Mathlib defines Stirling numbers of the second kind as `Nat.stirlingSecond`, which appear in the closed form, but not the two-types birthday probability itself. |
| status | not_formalized | partial |
modifiedNon-uniqueness of m+n solution00f7afb7c005
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedFirst match position7f19309ea3fe
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedSame birthday as you probability089ef412b59c
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modified253 people for 50% match with you85a5a8502a78
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedExpected number with shared birthday21530b4f5258
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedNear matches generalizationac4130598dc4
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedSeven people within a week76950721b174
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedExpected number of distinct birthdays5a0176cae911
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedExpected days with at least two birthdaysa3dcb6ef3bb4
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedExpected number of repeats1bc7f795cc15
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedAverage number of people Q(M)8bf58c8ab7d5
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedRamanujan asymptotic expansion7371bb6f9fa9
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedAverage of 24.61659 people7af82e38b318
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedIndicator variable analysisb596c504f230
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedFIFA World Cup 2014 squadsfb653f9e0969
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |
modifiedPartition problem answer is 23f0a38e098706
| Field | From #3039 | To #3563 |
|---|
| note | Not formalized. | Not formalized in Mathlib. |