feat(algebra/big_operators/order): Bounding on a sum of cards by doub…

…le counting (#10389)

If every element of `s` is in at least/most `n` finsets of `B : finset (finset α)`, then the sum of `(s ∩ t).card` over `t ∈ B` is at most/least `s.card * n`.

src/algebra/big_operators/order.lean

@@ -241,6 +241,57 @@ mul_card_image_le_card_of_maps_to (λ x, mem_image_of_mem _) n hn
 
 end pigeonhole
 
+section double_counting
+variables [decidable_eq α] {s : finset α} {B : finset (finset α)} {n : ℕ}
+
+/-- If every element belongs to at most `n` finsets, then the sum of their sizes is at most `n`
+times how many they are. -/
+lemma sum_card_inter_le (h : ∀ a ∈ s, (B.filter $ (∈) a).card ≤ n) :
+  ∑ t in B, (s ∩ t).card ≤ s.card * n :=
+begin
+  refine le_trans _ (s.sum_le_of_forall_le _ _ h),
+  simp_rw [←filter_mem_eq_inter, card_eq_sum_ones, sum_filter],
+  exact sum_comm.le,
+end
+
+/-- If every element belongs to at most `n` finsets, then the sum of their sizes is at most `n`
+times how many they are. -/
+lemma sum_card_le [fintype α] (h : ∀ a, (B.filter $ (∈) a).card ≤ n) :
+  ∑ s in B, s.card ≤ fintype.card α * n :=
+calc ∑ s in B, s.card = ∑ s in B, (univ ∩ s).card : by simp_rw univ_inter
+                  ... ≤ fintype.card α * n        : sum_card_inter_le (λ a _, h a)
+
+/-- If every element belongs to at least `n` finsets, then the sum of their sizes is at least `n`
+times how many they are. -/
+lemma le_sum_card_inter (h : ∀ a ∈ s, n ≤ (B.filter $ (∈) a).card) :
+  s.card * n ≤ ∑ t in B, (s ∩ t).card :=
+begin
+  apply (s.le_sum_of_forall_le _ _ h).trans,
+  simp_rw [←filter_mem_eq_inter, card_eq_sum_ones, sum_filter],
+  exact sum_comm.le,
+end
+
+/-- If every element belongs to at least `n` finsets, then the sum of their sizes is at least `n`
+times how many they are. -/
+lemma le_sum_card [fintype α] (h : ∀ a, n ≤ (B.filter $ (∈) a).card) :
+  fintype.card α * n ≤ ∑ s in B, s.card :=
+calc fintype.card α * n ≤ ∑ s in B, (univ ∩ s).card : le_sum_card_inter (λ a _, h a)
+                    ... = ∑ s in B, s.card          : by simp_rw univ_inter
+
+/-- If every element belongs to exactly `n` finsets, then the sum of their sizes is `n` times how
+many they are. -/
+lemma sum_card_inter (h : ∀ a ∈ s, (B.filter $ (∈) a).card = n) :
+  ∑ t in B, (s ∩ t).card = s.card * n :=
+(sum_card_inter_le $ λ a ha, (h a ha).le).antisymm (le_sum_card_inter $ λ a ha, (h a ha).ge)
+
+/-- If every element belongs to exactly `n` finsets, then the sum of their sizes is `n` times how
+many they are. -/
+lemma sum_card [fintype α] (h : ∀ a, (B.filter $ (∈) a).card = n) :
+  ∑ s in B, s.card = fintype.card α * n :=
+by simp_rw [fintype.card, ←sum_card_inter (λ a _, h a), univ_inter]
+
+end double_counting
+
 section canonically_ordered_monoid
 
 variables [canonically_ordered_monoid M] {f : ι → M} {s t : finset ι}