[Merged by Bors] - feat(data/fintype): pigeonhole principles

[kmill]

Add pigeonhole principles for finitely and infinitely many pigeons in finitely many holes. There are also strong versions of these, which say that there is a hole containing at least as many pigeons as the average number of pigeons per hole. Fixes #2272.

---

I'm not sure what they should be called or where they should go. Also, the proof of fintype.strong_pigeonhole can surely be simplified!

[kmill]

This now should contain all the pigeonhole principles in the linked issue (along with some versions for infinitely many pigeons). I'm still not sure what all these lemmas should be called or where they should go, especially the ones that are currently in algebra/big_operators/order.lean.

For the strong pigeonhole principles, I opted to have them include a nonemptiness hypothesis:

lemma strong_pigeonhole [fintype α] [fintype β] [nonempty β] [decidable_eq β] (f : α → β)
  (n : ℕ) (hn : fintype.card β * n ≤ fintype.card α) :
  ∃ y : β, n ≤ (univ.filter (λ x, f x = y)).card := sorry

This can be eliminated with a trick (as in the linked issue) like so:

lemma strong_pigeonhole [fintype α] [fintype β] [decidable_eq β] (f : α → β)
  (n : ℕ) (hn : fintype.card β * n < fintype.card α) :
  ∃ y : β, n < (univ.filter (λ x, f x = y)).card := sorry

The rationale is that in the first case, n is the quotient of fintype.card α by fintype.card β rounded down, where in the second case it is almost the the same, but with the difference that if the quotient yields no remainder then n is one less than the quotient, which seemed potentially difficult to work with. Edit: I analyzed this incorrectly. The second case is one less than the ceiling, so it gives a stronger statement.

[kmill]

Some things that still need to be figured out are (1) what to call these lemmas and (2) where these lemmas should live. (Started a thread on Zulip.)

[urkud]

@semorrison or @robertylewis Could you please look at this one more time? I did some golfing, so I should be the one who merges it into master.

[robertylewis]

Other than naming, it looks good to me. I agree with the discussion on Zulip that we should keep the declaration names (approximately) following the naming scheme and save the word "pigeonhole" for the doc strings.

[urkud]

Forgot to rename 2 lemmas.

[semorrison]

Looks good to me! Let's merge.

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests