feat(big_operators/basic): sum of count over finset.filter equals cou…

…ntp (#15393)

The sum of `l.count x` over `x` in `l.to_finset.filter p` is equal to `l.countp p`.
Also includes `prod_eq_one` instances for `list` and `multiset`

src/algebra/big_operators/basic.lean

@@ -1015,6 +1015,10 @@ begin
   rw [count_eq_zero_of_not_mem hx, pow_zero],
 end
 
+lemma sum_filter_count_eq_countp [decidable_eq α] (p : α → Prop) [decidable_pred p] (l : list α) :
+  ∑ x in l.to_finset.filter p, l.count x = l.countp p :=
+by simp [finset.sum, sum_map_count_dedup_filter_eq_countp p l]
+
 open multiset
 
 @[to_additive] lemma prod_multiset_map_count [decidable_eq α] (s : multiset α)

src/algebra/big_operators/multiset.lean

@@ -84,6 +84,22 @@ lemma prod_nsmul (m : multiset α) : ∀ (n : ℕ), (n • m).prod = m.prod ^ n
 @[simp, to_additive] lemma prod_repeat (a : α) (n : ℕ) : (repeat a n).prod = a ^ n :=
 by simp [repeat, list.prod_repeat]
 
+@[to_additive]
+lemma prod_map_eq_pow_single [decidable_eq ι] (i : ι) (hf : ∀ i' ≠ i, i' ∈ m → f i' = 1) :
+  (m.map f).prod = f i ^ m.count i :=
+begin
+  induction m using quotient.induction_on with l,
+  simp [list.prod_map_eq_pow_single i f hf],
+end
+
+@[to_additive]
+lemma prod_eq_pow_single [decidable_eq α] (a : α) (h : ∀ a' ≠ a, a' ∈ s → a' = 1) :
+  s.prod = a ^ (s.count a) :=
+begin
+  induction s using quotient.induction_on with l,
+  simp [list.prod_eq_pow_single a h],
+end
+
 @[to_additive]
 lemma pow_count [decidable_eq α] (a : α) : a ^ s.count a = (s.filter (eq a)).prod :=
 by rw [filter_eq, prod_repeat]
@@ -325,6 +341,15 @@ lemma prod_eq_one_iff [canonically_ordered_monoid α] {m : multiset α} :
   m.prod = 1 ↔ ∀ x ∈ m, x = (1 : α) :=
 quotient.induction_on m $ λ l, by simpa using list.prod_eq_one_iff l
 
+/-- Slightly more general version of `multiset.prod_eq_one_iff` for a non-ordered `monoid` -/
+@[to_additive "Slightly more general version of `multiset.sum_eq_zero_iff`
+  for a non-ordered `add_monoid`"]
+lemma prod_eq_one [comm_monoid α] {m : multiset α} (h : ∀ x ∈ m, x = (1 : α)) : m.prod = 1 :=
+begin
+  induction m using quotient.induction_on with l,
+  simp [list.prod_eq_one h],
+end
+
 @[to_additive]
 lemma le_prod_of_mem [canonically_ordered_monoid α] {m : multiset α} {a : α} (h : a ∈ m) :
   a ≤ m.prod :=

src/data/list/big_operators.lean

@@ -434,6 +434,12 @@ le_antisymm (hl₂ ▸ single_le_prod hl₁ _ hx) (hl₁ x hx)
 ⟨all_one_of_le_one_le_of_prod_eq_one (λ _ _, one_le _),
   λ h, by rw [eq_repeat.2 ⟨rfl, h⟩, prod_repeat, one_pow]⟩
 
+/-- Slightly more general version of `list.prod_eq_one_iff` for a non-ordered `monoid` -/
+@[to_additive "Slightly more general version of `list.sum_eq_zero_iff`
+  for a non-ordered `add_monoid`"]
+lemma prod_eq_one [monoid M] {l : list M} (hl : ∀ (x ∈ l), x = (1 : M)) : l.prod = 1 :=
+trans (prod_eq_pow_card l 1 hl) (one_pow l.length)
+
 /-- If all elements in a list are bounded below by `1`, then the length of the list is bounded
 by the sum of the elements. -/
 lemma length_le_sum_of_one_le (L : list ℕ) (h : ∀ i ∈ L, 1 ≤ i) : L.length ≤ L.sum :=

src/data/list/count.lean

@@ -207,6 +207,24 @@ begin
   { rw [count_cons', count_cons', count_erase_of_ne] }
 end
 
+@[to_additive]
+lemma prod_map_eq_pow_single [monoid β] {l : list α} (a : α) (f : α → β)
+  (hf : ∀ a' ≠ a, a' ∈ l → f a' = 1) : (l.map f).prod = (f a) ^ (l.count a) :=
+begin
+  induction l with a' as h generalizing a,
+  { rw [map_nil, prod_nil, count_nil, pow_zero] },
+  { specialize h a (λ a' ha' hfa', hf a' ha' (mem_cons_of_mem _ hfa')),
+    rw [list.map_cons, list.prod_cons, count_cons, h],
+    split_ifs with ha',
+    { rw [ha', pow_succ] },
+    { rw [hf a' (ne.symm ha') (list.mem_cons_self a' as), one_mul] } }
+end
+
+@[to_additive]
+lemma prod_eq_pow_single [monoid α] {l : list α} (a : α)
+  (h : ∀ a' ≠ a, a' ∈ l → a' = 1) : l.prod = a ^ (l.count a) :=
+trans (by rw [map_id'']) (prod_map_eq_pow_single a id h)
+
 end count
 
 end list

src/data/list/dedup.lean

@@ -77,4 +77,35 @@ lemma repeat_dedup {x : α} : ∀ {k}, k ≠ 0 → (repeat x k).dedup = [x]
 | (n+2) _ := by rw [repeat_succ, dedup_cons_of_mem (mem_repeat.2 ⟨n.succ_ne_zero, rfl⟩),
     repeat_dedup n.succ_ne_zero]
 
+lemma count_dedup (l : list α) (a : α) :
+  l.dedup.count a = if a ∈ l then 1 else 0 :=
+by simp_rw [count_eq_of_nodup $ nodup_dedup l, mem_dedup]
+
+/-- Summing the count of `x` over a list filtered by some `p` is just `countp` applied to `p` -/
+lemma sum_map_count_dedup_filter_eq_countp (p : α → Prop) [decidable_pred p]
+  (l : list α) : ((l.dedup.filter p).map $ λ x, l.count x).sum = l.countp p :=
+begin
+  induction l with a as h,
+  { simp },
+  { simp_rw [list.countp_cons, list.count_cons', list.sum_map_add],
+    congr' 1,
+    { refine trans _ h,
+      by_cases ha : a ∈ as,
+      { simp [dedup_cons_of_mem ha] },
+      { simp only [dedup_cons_of_not_mem ha, list.filter],
+        split_ifs with hp; simp [list.map_cons, list.sum_cons,
+          list.count_eq_zero.2 ha, zero_add] } },
+    { by_cases hp : p a,
+      { refine trans (sum_map_eq_nsmul_single a _ (λ _ h _, by simp [h])) _,
+        simp [hp, count_dedup] },
+      { refine trans (list.sum_eq_zero $ λ n hn, _) (by simp [hp]),
+        obtain ⟨a', ha'⟩ := list.mem_map.1 hn,
+        simp only [(λ h, hp (h ▸ (list.mem_filter.1 ha'.1).2) : a' ≠ a), if_false] at ha',
+        exact ha'.2.symm } } },
+end
+
+lemma sum_map_count_dedup_eq_length (l : list α) :
+  (l.dedup.map $ λ x, l.count x).sum = l.length :=
+by simpa using sum_map_count_dedup_filter_eq_countp (λ _, true) l
+
 end list

src/data/list/nodup.lean

@@ -135,6 +135,14 @@ theorem nodup_repeat (a : α) : ∀ {n : ℕ}, nodup (repeat a n) ↔ n ≤ 1
   (d : nodup l) (h : a ∈ l) : count a l = 1 :=
 le_antisymm (nodup_iff_count_le_one.1 d a) (count_pos.2 h)
 
+lemma count_eq_of_nodup [decidable_eq α] {a : α} {l : list α}
+  (d : nodup l) : count a l = if a ∈ l then 1 else 0 :=
+begin
+  split_ifs with h,
+  { exact count_eq_one_of_mem d h },
+  { exact count_eq_zero_of_not_mem h },
+end
+
 lemma nodup.of_append_left : nodup (l₁ ++ l₂) → nodup l₁ :=
 nodup.sublist (sublist_append_left l₁ l₂)
 

src/data/multiset/nodup.lean

@@ -60,6 +60,14 @@ quot.induction_on s $ λ l, nodup_iff_count_le_one
   (d : nodup s) (h : a ∈ s) : count a s = 1 :=
 le_antisymm (nodup_iff_count_le_one.1 d a) (count_pos.2 h)
 
+lemma count_eq_of_nodup [decidable_eq α] {a : α} {s : multiset α}
+  (d : nodup s) : count a s = if a ∈ s then 1 else 0 :=
+begin
+  split_ifs with h,
+  { exact count_eq_one_of_mem d h },
+  { exact count_eq_zero_of_not_mem h },
+end
+
 lemma nodup_iff_pairwise {α} {s : multiset α} : nodup s ↔ pairwise (≠) s :=
 quotient.induction_on s $ λ l, (pairwise_coe_iff_pairwise (by exact λ a b, ne.symm)).symm