feat(combinatorics/pigeonhole): Pigeons in linear commutative rings (#…

…13308)

Duplicate almost all the pigeonhole principle API to work in `linear_ordered_comm_ring`s.

Co-authored-by: Bhavik Mehta <bhavik.mehta8@gmail.com>

src/algebra/module/basic.lean

@@ -39,9 +39,8 @@ semimodule, module, vector space
 open function
 open_locale big_operators
 
-universes u u' v w x y z
-variables {R : Type u} {k : Type u'} {S : Type v} {M : Type w} {M₂ : Type x} {M₃ : Type y}
-  {ι : Type z}
+universes u v
+variables {α R k S M M₂ M₃ ι : Type*}
 
 /-- A module is a generalization of vector spaces to a scalar semiring.
   It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
@@ -618,3 +617,6 @@ by rw [nsmul_eq_mul, mul_one]
 @[simp] lemma int.smul_one_eq_coe {R : Type*} [ring R] (m : ℤ) :
   m • (1 : R) = ↑m :=
 by rw [zsmul_eq_mul, mul_one]
+
+lemma finset.cast_card [comm_semiring R] (s : finset α) : (s.card : R) = ∑ a in s, 1 :=
+by rw [finset.sum_const, nat.smul_one_eq_coe]

src/combinatorics/pigeonhole.lean

@@ -54,15 +54,22 @@ docstrings instead of the names.
   `measure_theory.exists_nonempty_inter_of_measure_univ_lt_sum_measure`: pigeonhole principle in a
   measure space.
 
+## TODO
+
+The `_nsmul` lemmas could be generalized from `linear_ordered_comm_ring` to
+`linear_ordered_comm_semiring` if the latter existed (or some combination of
+`covariant`/`contravariant` classes once the refactor has gone deep enough). This would allow
+deriving the `_mul` lemmas from the `_nsmul` ones.
+
 ## Tags
 
 pigeonhole principle
 -/
 
 universes u v w
-variables {α : Type u} {β : Type v} {M : Type w} [linear_ordered_cancel_add_comm_monoid M]
-  [decidable_eq β]
+variables {α : Type u} {β : Type v} {M : Type w} [decidable_eq β]
 
+open nat
 open_locale big_operators
 
 namespace finset
@@ -94,6 +101,9 @@ There are a few bits we can change in this theorem:
 We can do all these variations independently, so we have eight versions of the theorem.
 -/
 
+section
+variables [linear_ordered_cancel_add_comm_monoid M]
+
 /-!
 #### Strict inequality versions
 -/
@@ -186,6 +196,10 @@ lemma exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul
   ∃ y ∈ t, (∑ x in s.filter (λ x, f x = y), w x) ≤ b :=
 @exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum α β (order_dual M) _ _ _ _ _ _ _ hf ht hb
 
+end
+
+variables [linear_ordered_comm_ring M]
+
 /-!
 ### The pigeonhole principles on `finset`s, pigeons counted by heads
 
@@ -203,6 +217,16 @@ So, we prove four theorems: `finset.exists_lt_card_fiber_of_maps_to_of_mul_lt_ca
 `finset.exists_le_card_fiber_of_maps_to_of_mul_le_card`,
 `finset.exists_card_fiber_lt_of_card_lt_mul`, and `finset.exists_card_fiber_le_of_card_le_mul`. -/
 
+/-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
+at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes. -/
+lemma exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to (hf : ∀ a ∈ s, f a ∈ t)
+  (ht : t.card • b < s.card) :
+  ∃ y ∈ t, b < (s.filter $ λ x, f x = y).card :=
+begin
+  simp_rw cast_card at ⊢ ht,
+  exact exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum hf ht,
+end
+
 /-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
 at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes.
 ("The maximum is at least the mean" specialized to integers.)
@@ -219,6 +243,16 @@ begin
   simpa
 end
 
+/-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
+at most as many pigeons as the floor of the average number of pigeons across all pigeonholes. -/
+lemma exists_card_fiber_lt_of_card_lt_nsmul (ht : ↑(s.card) < t.card • b) :
+  ∃ y ∈ t, ↑((s.filter $ λ x, f x = y).card) < b :=
+begin
+  simp_rw cast_card at ⊢ ht,
+  exact exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul
+    (λ _ _, sum_nonneg $ λ _ _, zero_le_one) ht,
+end
+
 /-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
 at most as many pigeons as the floor of the average number of pigeons across all pigeonholes.  ("The
 minimum is at most the mean" specialized to integers.)
@@ -235,7 +269,19 @@ begin
 end
 
 /-- The pigeonhole principle for finitely many pigeons counted by heads: given a function between
-finite sets `s` and `t` and a natural number `n` such that `card t * n ≤ card s`, there exists `y ∈
+finite sets `s` and `t` and a number `b` such that `card t • b ≤ card s`, there exists `y ∈ t` such
+that its preimage in `s` has at least `b` elements.
+See also `finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to` for a stronger statement. -/
+lemma exists_le_card_fiber_of_nsmul_le_card_of_maps_to (hf : ∀ a ∈ s, f a ∈ t) (ht : t.nonempty)
+  (hb : t.card • b ≤ s.card) :
+  ∃ y ∈ t, b ≤ (s.filter $ λ x, f x = y).card :=
+begin
+  simp_rw cast_card at ⊢ hb,
+  exact exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum hf ht hb,
+end
+
+/-- The pigeonhole principle for finitely many pigeons counted by heads: given a function between
+finite sets `s` and `t` and a natural number `b` such that `card t * n ≤ card s`, there exists `y ∈
 t` such that its preimage in `s` has at least `n` elements. See also
 `finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to` for a stronger statement. -/
 lemma exists_le_card_fiber_of_mul_le_card_of_maps_to (hf : ∀ a ∈ s, f a ∈ t) (ht : t.nonempty)
@@ -247,6 +293,18 @@ begin
   simpa
 end
 
+/-- The pigeonhole principle for finitely many pigeons counted by heads: given a function `f`, a
+finite sets `s` and `t`, and a number `b` such that `card s ≤ card t • b`, there exists `y ∈ t` such
+that its preimage in `s` has no more than `b` elements.
+See also `finset.exists_card_fiber_lt_of_card_lt_nsmul` for a stronger statement. -/
+lemma exists_card_fiber_le_of_card_le_nsmul (ht : t.nonempty) (hb : ↑(s.card) ≤ t.card • b) :
+  ∃ y ∈ t, ↑((s.filter $ λ x, f x = y).card) ≤ b :=
+begin
+  simp_rw cast_card at ⊢ hb,
+  refine exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul
+    (λ _ _, sum_nonneg $ λ _ _, zero_le_one) ht hb,
+end
+
 /-- The pigeonhole principle for finitely many pigeons counted by heads: given a function `f`, a
 finite sets `s` in its domain, a finite set `t` in its codomain, and a natural number `n` such that
 `card s ≤ card t * n`, there exists `y ∈ t` such that its preimage in `s` has no more than `n`
@@ -266,6 +324,9 @@ open finset
 
 variables [fintype α] [fintype β] (f : α → β) {w : α → M} {b : M} {n : ℕ}
 
+section
+variables [linear_ordered_cancel_add_comm_monoid M]
+
 /-!
 ### The pigeonhole principles on `fintypes`s, pigeons counted by weight
 
@@ -295,15 +356,27 @@ version: there is a pigeonhole with the total weight of pigeons in it less than
 the total number of pigeonholes times `b` is greater than the total weight of all pigeons. -/
 lemma exists_sum_fiber_lt_of_sum_lt_nsmul (hb : (∑ x, w x) < card β • b) :
   ∃ y, (∑ x in univ.filter (λ x, f x = y), w x) < b :=
-@exists_lt_sum_fiber_of_nsmul_lt_sum α β (order_dual M) _ _ _ _ _ w b hb
+@exists_lt_sum_fiber_of_nsmul_lt_sum α β (order_dual M) _ _ _ _ _ _ _ hb
 
 /-- The pigeonhole principle for finitely many pigeons of different weights, non-strict inequality
 version: there is a pigeonhole with the total weight of pigeons in it less than or equal to `b`
 provided that the total number of pigeonholes times `b` is greater than or equal to the total weight
 of all pigeons. -/
 lemma exists_sum_fiber_le_of_sum_le_nsmul [nonempty β] (hb : (∑ x, w x) ≤ card β • b) :
   ∃ y, (∑ x in univ.filter (λ x, f x = y), w x) ≤ b :=
-@exists_le_sum_fiber_of_nsmul_le_sum α β (order_dual M) _ _ _ _ _ w b _ hb
+@exists_le_sum_fiber_of_nsmul_le_sum α β (order_dual M) _ _ _ _ _ _ _ _ hb
+
+end
+
+variables [linear_ordered_comm_ring M]
+
+/--
+The strong pigeonhole principle for finitely many pigeons and pigeonholes. There is a pigeonhole
+with at least as many pigeons as the ceiling of the average number of pigeons across all
+pigeonholes. -/
+lemma exists_lt_card_fiber_of_nsmul_lt_card (hb : card β • b < card α) :
+  ∃ y : β, b < (univ.filter (λ x, f x = y)).card :=
+let ⟨y, _, h⟩ := exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to (λ _ _, mem_univ _) hb in ⟨y, h⟩
 
 /--
 The strong pigeonhole principle for finitely many pigeons and pigeonholes.
@@ -318,6 +391,13 @@ lemma exists_lt_card_fiber_of_mul_lt_card (hn : card β * n < card α) :
   ∃ y : β, n < (univ.filter (λ x, f x = y)).card :=
 let ⟨y, _, h⟩ := exists_lt_card_fiber_of_mul_lt_card_of_maps_to (λ _ _, mem_univ _) hn in ⟨y, h⟩
 
+/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes. There is a pigeonhole
+with at most as many pigeons as the floor of the average number of pigeons across all pigeonholes.
+-/
+lemma exists_card_fiber_lt_of_card_lt_nsmul (hb : ↑(card α) < card β • b) :
+  ∃ y : β, ↑((univ.filter $ λ x, f x = y).card) < b :=
+let ⟨y, _, h⟩ := exists_card_fiber_lt_of_card_lt_nsmul hb in ⟨y, h⟩
+
 /--
 The strong pigeonhole principle for finitely many pigeons and pigeonholes.
 There is a pigeonhole with at most as many pigeons as
@@ -331,6 +411,15 @@ lemma exists_card_fiber_lt_of_card_lt_mul (hn : card α < card β * n) :
   ∃ y : β, (univ.filter (λ x, f x = y)).card < n :=
 let ⟨y, _, h⟩ := exists_card_fiber_lt_of_card_lt_mul hn in ⟨y, h⟩
 
+/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes.  Given a function `f`
+between finite types `α` and `β` and a number `b` such that `card β • b ≤ card α`, there exists an
+element `y : β` such that its preimage has at least `b` elements.
+See also `fintype.exists_lt_card_fiber_of_nsmul_lt_card` for a stronger statement. -/
+lemma exists_le_card_fiber_of_nsmul_le_card [nonempty β] (hb : card β • b ≤ card α) :
+  ∃ y : β, b ≤ (univ.filter $ λ x, f x = y).card :=
+let ⟨y, _, h⟩ := exists_le_card_fiber_of_nsmul_le_card_of_maps_to (λ _ _, mem_univ _) univ_nonempty
+  hb in ⟨y, h⟩
+
 /-- The strong pigeonhole principle for finitely many pigeons and pigeonholes.  Given a function `f`
 between finite types `α` and `β` and a number `n` such that `card β * n ≤ card α`, there exists an
 element `y : β` such that its preimage has at least `n` elements. See also
@@ -340,6 +429,14 @@ lemma exists_le_card_fiber_of_mul_le_card [nonempty β] (hn : card β * n ≤ ca
 let ⟨y, _, h⟩ := exists_le_card_fiber_of_mul_le_card_of_maps_to (λ _ _, mem_univ _) univ_nonempty hn
 in ⟨y, h⟩
 
+/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes.  Given a function `f`
+between finite types `α` and `β` and a number `b` such that `card α ≤ card β • b`, there exists an
+element `y : β` such that its preimage has at most `b` elements.
+See also `fintype.exists_card_fiber_lt_of_card_lt_nsmul` for a stronger statement. -/
+lemma exists_card_fiber_le_of_card_le_nsmul [nonempty β] (hb : ↑(card α) ≤ card β • b) :
+  ∃ y : β, ↑((univ.filter $ λ x, f x = y).card) ≤ b :=
+let ⟨y, _, h⟩ := exists_card_fiber_le_of_card_le_nsmul univ_nonempty hb in ⟨y, h⟩
+
 /-- The strong pigeonhole principle for finitely many pigeons and pigeonholes.  Given a function `f`
 between finite types `α` and `β` and a number `n` such that `card α ≤ card β * n`, there exists an
 element `y : β` such that its preimage has at most `n` elements. See also