feat(data/finsupp/indicator, algebra/big_operators/finsupp): add some lemmas about finsupp.indicator (#17413)

mathlib4 PR: leanprover-community/mathlib4#2258

Author: astrainfinita

src/algebra/big_operators/finsupp.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 
-import data.finsupp.defs
+import data.finsupp.indicator
 import algebra.big_operators.pi
 import algebra.big_operators.ring
 import algebra.big_operators.order
@@ -488,6 +488,26 @@ begin
   exact h2,
 end
 
+lemma indicator_eq_sum_single [add_comm_monoid M] (s : finset α) (f : Π a ∈ s, M) :
+  indicator s f = ∑ x in s.attach, single x (f x x.2) :=
+begin
+  rw [← sum_single (indicator s f), sum, sum_subset (support_indicator_subset _ _), ← sum_attach],
+  { refine finset.sum_congr rfl (λ x hx, _),
+    rw [indicator_of_mem], },
+  intros i _ hi,
+  rw [not_mem_support_iff.mp hi, single_zero],
+end
+
+@[simp, to_additive]
+lemma prod_indicator_index [has_zero M] [comm_monoid N]
+  {s : finset α} (f : Π a ∈ s, M) {h : α → M → N} (h_zero : ∀ a ∈ s, h a 0 = 1) :
+  (indicator s f).prod h = ∏ x in s.attach, h x (f x x.2) :=
+begin
+  rw [prod_of_support_subset _ (support_indicator_subset _ _) h h_zero, ← prod_attach],
+  refine finset.prod_congr rfl (λ x hx, _),
+  rw [indicator_of_mem],
+end
+
 end finsupp
 
 

src/data/finsupp/defs.lean

@@ -232,7 +232,7 @@ lemma single_apply_left {f : α → β} (hf : function.injective f)
   single (f x) y (f z) = single x y z :=
 by { classical, simp only [single_apply, hf.eq_iff] }
 
-lemma single_eq_indicator : ⇑(single a b) = set.indicator {a} (λ _, b) :=
+lemma single_eq_set_indicator : ⇑(single a b) = set.indicator {a} (λ _, b) :=
 by { classical, ext, simp [single_apply, set.indicator, @eq_comm _ a] }
 
 @[simp] lemma single_eq_same : (single a b : α →₀ M) a = b :=
@@ -242,7 +242,7 @@ by { classical, exact pi.single_eq_same a b }
 by { classical, exact pi.single_eq_of_ne' h _ }
 
 lemma single_eq_update [decidable_eq α] (a : α) (b : M) : ⇑(single a b) = function.update 0 a b :=
-by rw [single_eq_indicator, ← set.piecewise_eq_indicator, set.piecewise_singleton]
+by rw [single_eq_set_indicator, ← set.piecewise_eq_indicator, set.piecewise_singleton]
 
 lemma single_eq_pi_single [decidable_eq α] (a : α) (b : M) : ⇑(single a b) = pi.single a b :=
 single_eq_update a b
@@ -284,7 +284,7 @@ have (single a b₁ : α →₀ M) a = (single a b₂ : α →₀ M) a, by rw eq
 by rwa [single_eq_same, single_eq_same] at this
 
 lemma single_apply_eq_zero {a x : α} {b : M} : single a b x = 0 ↔ (x = a → b = 0) :=
-by simp [single_eq_indicator]
+by simp [single_eq_set_indicator]
 
 lemma single_apply_ne_zero {a x : α} {b : M} : single a b x ≠ 0 ↔ (x = a ∧ b ≠ 0) :=
 by simp [single_apply_eq_zero]
@@ -337,7 +337,7 @@ lemma support_single_disjoint {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α
 by rw [support_single_ne_zero _ hb, support_single_ne_zero _ hb', disjoint_singleton]
 
 @[simp] lemma single_eq_zero : single a b = 0 ↔ b = 0 :=
-by simp [ext_iff, single_eq_indicator]
+by simp [ext_iff, single_eq_set_indicator]
 
 lemma single_swap (a₁ a₂ : α) (b : M) : single a₁ b a₂ = single a₂ b a₁ :=
 by { classical, simp only [single_apply], ac_refl }

src/data/finsupp/indicator.lean

@@ -66,4 +66,8 @@ begin
   exact hi (indicator_of_not_mem h _),
 end
 
+lemma single_eq_indicator (i : ι) (b : α) :
+  single i b = indicator {i} (λ _ _, b) :=
+by { classical, ext, simp [single_apply, indicator_apply, @eq_comm _ a] }
+
 end finsupp