feat(data/fintype): pigeonhole principles (#4096)

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.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/algebra/big_operators/basic.lean

@@ -246,7 +246,7 @@ end
 @[to_additive]
 lemma prod_product' {s : finset γ} {t : finset α} {f : γ → α → β} :
   (∏ x in s.product t, f x.1 x.2) = ∏ x in s, ∏ y in t, f x y :=
-by rw prod_product
+prod_product
 
 @[to_additive]
 lemma prod_sigma {σ : α → Type*}
@@ -262,24 +262,26 @@ calc (∏ x in s.sigma t, f x) =
   ... = ∏ a in s, ∏ s in t a, f ⟨a, s⟩ :
     prod_congr rfl $ λ _ _, prod_map _ _ _
 
+@[to_additive]
+lemma prod_fiberwise_of_maps_to [decidable_eq γ] {s : finset α} {t : finset γ} {g : α → γ}
+  (h : ∀ x ∈ s, g x ∈ t) (f : α → β) :
+  (∏ y in t, ∏ x in s.filter (λ x, g x = y), f x) = ∏ x in s, f x :=
+begin
+  letI := classical.dec_eq α,
+  rw [← bind_filter_eq_of_maps_to h] {occs := occurrences.pos [2]},
+  refine (prod_bind $ λ x' hx y' hy hne, _).symm,
+  rw [disjoint_filter],
+  rintros x hx rfl,
+  exact hne
+end
+
 @[to_additive]
 lemma prod_image' [decidable_eq α] {s : finset γ} {g : γ → α} (h : γ → β)
   (eq : ∀c∈s, f (g c) = ∏ x in s.filter (λc', g c' = g c), h x) :
   (∏ x in s.image g, f x) = ∏ x in s, h x :=
-begin
-  letI := classical.dec_eq γ,
-  rw [← image_bind_filter_eq s g] {occs := occurrences.pos [2]},
-  rw [finset.prod_bind],
-  { refine finset.prod_congr rfl (assume a ha, _),
-    rcases finset.mem_image.1 ha with ⟨b, hb, rfl⟩,
-    exact eq b hb },
-  assume a₀ _ a₁ _ ne,
-  refine (disjoint_iff_ne.2 _),
-  assume c₀ h₀ c₁ h₁,
-  rcases mem_filter.1 h₀ with ⟨h₀, rfl⟩,
-  rcases mem_filter.1 h₁ with ⟨h₁, rfl⟩,
-  exact mt (congr_arg g) ne
-end
+calc (∏ x in s.image g, f x) = ∏ x in s.image g, ∏ x in s.filter (λ c', g c' = x), h x :
+  prod_congr rfl $ λ x hx, let ⟨c, hcs, hc⟩ := mem_image.1 hx in hc ▸ (eq c hcs)
+... = ∏ x in s, h x : prod_fiberwise_of_maps_to (λ x, mem_image_of_mem g) _
 
 @[to_additive]
 lemma prod_mul_distrib : ∏ x in s, (f x * g x) = (∏ x in s, f x) * (∏ x in s, g x) :=
@@ -954,16 +956,14 @@ finset.induction_on s (by simp)
     ... ≤ ∑ a in insert a s, card (t a) :
     by rw sum_insert has; exact add_le_add_left ih _)
 
+theorem card_eq_sum_card_fiberwise [decidable_eq β] {f : α → β} {s : finset α} {t : finset β}
+  (H : ∀ x ∈ s, f x ∈ t) :
+  s.card = ∑ a in t, (s.filter (λ x, f x = a)).card :=
+by simp only [card_eq_sum_ones, sum_fiberwise_of_maps_to H]
+
 theorem card_eq_sum_card_image [decidable_eq β] (f : α → β) (s : finset α) :
   s.card = ∑ a in s.image f, (s.filter (λ x, f x = a)).card :=
-by letI := classical.dec_eq α; exact
-calc s.card = ((s.image f).bind (λ a, s.filter (λ x, f x = a))).card :
-  congr_arg _ (finset.ext $ λ x,
-    ⟨λ hs, mem_bind.2 ⟨f x, mem_image_of_mem _ hs,
-      mem_filter.2 ⟨hs, rfl⟩⟩,
-    λ h, let ⟨a, ha₁, ha₂⟩ := mem_bind.1 h in by convert filter_subset s ha₂⟩)
-... = ∑ a in s.image f, (s.filter (λ x, f x = a)).card :
-  card_bind (by simp [disjoint_left, finset.ext_iff] {contextual := tt})
+card_eq_sum_card_fiberwise (λ _, mem_image_of_mem _)
 
 lemma gsmul_sum [add_comm_group β] {f : α → β} {s : finset α} (z : ℤ) :
   gsmul z (∑ a in s, f a) = ∑ a in s, gsmul z (f a) :=

src/algebra/big_operators/order.lean

@@ -49,13 +49,17 @@ begin
   by simpa only [sum_insert ha]
 end
 
+theorem card_le_mul_card_image_of_maps_to [decidable_eq γ] {f : α → γ} {s : finset α} {t : finset γ}
+  (Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ) (hn : ∀ a ∈ t, (s.filter (λ x, f x = a)).card ≤ n) :
+  s.card ≤ n * t.card :=
+calc s.card = (∑ a in t, (s.filter (λ x, f x = a)).card) : card_eq_sum_card_fiberwise Hf
+        ... ≤ (∑ _ in t, n)                              : sum_le_sum hn
+        ... = _                                          : by simp [mul_comm]
+
 theorem card_le_mul_card_image [decidable_eq γ] {f : α → γ} (s : finset α)
   (n : ℕ) (hn : ∀ a ∈ s.image f, (s.filter (λ x, f x = a)).card ≤ n) :
   s.card ≤ n * (s.image f).card :=
-calc s.card = (∑ a in s.image f, (s.filter (λ x, f x = a)).card) :
-  card_eq_sum_card_image _ _
-... ≤ (∑ _ in s.image f, n) : sum_le_sum hn
-... = _ : by simp [mul_comm]
+card_le_mul_card_image_of_maps_to (λ x, mem_image_of_mem _) n hn
 
 lemma sum_nonneg (h : ∀x∈s, 0 ≤ f x) : 0 ≤ (∑ x in s, f x) :=
 le_trans (by rw [sum_const_zero]) (sum_le_sum h)
@@ -74,6 +78,20 @@ calc (∑ x in s₁, f x) ≤ (∑ x in s₂ \ s₁, f x) + (∑ x in s₁, f x)
 lemma sum_mono_set_of_nonneg (hf : ∀ x, 0 ≤ f x) : monotone (λ s, ∑ x in s, f x) :=
 λ s₁ s₂ hs, sum_le_sum_of_subset_of_nonneg hs $ λ x _ _, hf x
 
+lemma sum_fiberwise_le_sum_of_sum_fiber_nonneg [decidable_eq γ] {s : finset α} {t : finset γ}
+  {g : α → γ} {f : α → β} (h : ∀ y ∉ t, (0 : β) ≤ ∑ x in s.filter (λ x, g x = y), f x) :
+  (∑ y in t, ∑ x in s.filter (λ x, g x = y), f x) ≤ ∑ x in s, f x :=
+calc (∑ y in t, ∑ x in s.filter (λ x, g x = y), f x) ≤
+  (∑ y in t ∪ s.image g, ∑ x in s.filter (λ x, g x = y), f x) :
+  sum_le_sum_of_subset_of_nonneg (subset_union_left _ _) $ λ y hyts, h y
+... = ∑ x in s, f x :
+  sum_fiberwise_of_maps_to (λ x hx, mem_union.2 $ or.inr $ mem_image_of_mem _ hx) _
+
+lemma sum_le_sum_fiberwise_of_sum_fiber_nonpos [decidable_eq γ] {s : finset α} {t : finset γ}
+  {g : α → γ} {f : α → β} (h : ∀ y ∉ t, (∑ x in s.filter (λ x, g x = y), f x) ≤ 0) :
+  (∑ x in s, f x) ≤ ∑ y in t, ∑ x in s.filter (λ x, g x = y), f x :=
+@sum_fiberwise_le_sum_of_sum_fiber_nonneg α (order_dual β) _ _ _ _ _ _ _ h
+
 lemma sum_eq_zero_iff_of_nonneg : (∀x∈s, 0 ≤ f x) → ((∑ x in s, f x) = 0 ↔ ∀x∈s, f x = 0) :=
 begin
   classical,
@@ -169,10 +187,16 @@ section decidable_linear_ordered_cancel_comm_monoid
 
 variables [decidable_linear_ordered_cancel_add_comm_monoid β]
 
+theorem exists_lt_of_sum_lt (Hlt : (∑ x in s, f x) < ∑ x in s, g x) :
+  ∃ i ∈ s, f i < g i :=
+begin
+  contrapose! Hlt with Hle,
+  exact sum_le_sum Hle
+end
+
 theorem exists_le_of_sum_le (hs : s.nonempty) (Hle : (∑ x in s, f x) ≤ ∑ x in s, g x) :
   ∃ i ∈ s, f i ≤ g i :=
 begin
-  classical,
   contrapose! Hle with Hlt,
   rcases hs with ⟨i, hi⟩,
   exact sum_lt_sum (λ i hi, le_of_lt (Hlt i hi)) ⟨i, hi, Hlt i hi⟩
@@ -185,7 +209,7 @@ begin
   contrapose! h₁,
   obtain ⟨x, m, x_nz⟩ : ∃ x ∈ s, f x ≠ 0 := h₂,
   apply ne_of_lt,
-  calc ∑ e in s, f e < ∑ e in s, 0 : by { apply sum_lt_sum h₁ ⟨x, m, lt_of_le_of_ne (h₁ x m) x_nz⟩ }
+  calc ∑ e in s, f e < ∑ e in s, 0 : sum_lt_sum h₁ ⟨x, m, lt_of_le_of_ne (h₁ x m) x_nz⟩
                  ... = 0           : by rw [finset.sum_const, nsmul_zero],
 end
 

src/algebra/ordered_group.lean

@@ -1895,6 +1895,11 @@ instance [decidable_linear_ordered_add_comm_group α] :
   ..order_dual.decidable_linear_order α,
   ..show add_comm_group α, by apply_instance }
 
+instance [decidable_linear_ordered_cancel_add_comm_monoid α] :
+  decidable_linear_ordered_cancel_add_comm_monoid (order_dual α) :=
+{ .. order_dual.decidable_linear_order α,
+  .. order_dual.ordered_cancel_add_comm_monoid }
+
 end order_dual
 
 section type_tags