From aa0f33a524d745d7dac130aaa4bc62a6db8a01b7 Mon Sep 17 00:00:00 2001 From: negiizhao Date: Mon, 20 Mar 2023 22:50:20 +0000 Subject: [PATCH] feat: add some lemmas about `Finsupp.indicator` (#2258) mathlib3 PR: https://github.com/leanprover-community/mathlib/pull/17413 Co-authored-by: Eric Wieser --- Mathlib/Algebra/BigOperators/Finsupp.lean | 23 +++++++++++++++++++++-- Mathlib/Data/Finsupp/Defs.lean | 13 +++++++------ Mathlib/Data/Finsupp/Indicator.lean | 8 +++++++- 3 files changed, 35 insertions(+), 9 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Finsupp.lean b/Mathlib/Algebra/BigOperators/Finsupp.lean index dfb02f83f222a..c66ac2219d28e 100644 --- a/Mathlib/Algebra/BigOperators/Finsupp.lean +++ b/Mathlib/Algebra/BigOperators/Finsupp.lean @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau ! This file was ported from Lean 3 source module algebra.big_operators.finsupp -! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c +! leanprover-community/mathlib commit 842328d9df7e96fd90fc424e115679c15fb23a71 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathlib.Data.Finsupp.Defs +import Mathlib.Data.Finsupp.Indicator import Mathlib.Algebra.BigOperators.Pi import Mathlib.Algebra.BigOperators.Ring import Mathlib.Algebra.BigOperators.Order @@ -602,6 +602,25 @@ theorem prod_dvd_prod_of_subset_of_dvd [AddCommMonoid M] [CommMonoid N] {f1 f2 : exact h2 #align finsupp.prod_dvd_prod_of_subset_of_dvd Finsupp.prod_dvd_prod_of_subset_of_dvd +lemma indicator_eq_sum_single [AddCommMonoid M] (s : Finset α) (f : ∀ a ∈ s, M) : + indicator s f = ∑ x in s.attach, single ↑x (f x x.2) := by + rw [← sum_single (indicator s f), sum, sum_subset (support_indicator_subset _ _), ← sum_attach] + · refine' Finset.sum_congr rfl (fun _ _ => _) + rw [indicator_of_mem] + · intro i _ hi + rw [not_mem_support_iff.mp hi, single_zero] +#align finsupp.indicator_eq_sum_single Finsupp.indicator_eq_sum_single + +@[to_additive (attr := simp)] +lemma prod_indicator_index [Zero M] [CommMonoid 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) := by + rw [prod_of_support_subset _ (support_indicator_subset _ _) h h_zero, ← prod_attach] + refine' Finset.prod_congr rfl (fun _ _ => _) + rw [indicator_of_mem] +#align finsupp.prod_indicator_index Finsupp.prod_indicator_index +#align finsupp.sum_indicator_index Finsupp.sum_indicator_index + end Finsupp theorem Finset.sum_apply' : (∑ k in s, f k) i = ∑ k in s, f k i := diff --git a/Mathlib/Data/Finsupp/Defs.lean b/Mathlib/Data/Finsupp/Defs.lean index 29d12654607b9..7b5cd0fcefbaf 100644 --- a/Mathlib/Data/Finsupp/Defs.lean +++ b/Mathlib/Data/Finsupp/Defs.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Scott Morrison ! This file was ported from Lean 3 source module data.finsupp.defs -! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1 +! leanprover-community/mathlib commit 842328d9df7e96fd90fc424e115679c15fb23a71 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -317,11 +317,11 @@ theorem single_apply_left {f : α → β} (hf : Function.Injective f) (x z : α) single (f x) y (f z) = single x y z := by classical simp only [single_apply, hf.eq_iff] #align finsupp.single_apply_left Finsupp.single_apply_left -theorem single_eq_indicator : ⇑(single a b) = Set.indicator {a} fun _ => b := by +theorem single_eq_set_indicator : ⇑(single a b) = Set.indicator {a} fun _ => b := by classical ext simp [single_apply, Set.indicator, @eq_comm _ a] -#align finsupp.single_eq_indicator Finsupp.single_eq_indicator +#align finsupp.single_eq_set_indicator Finsupp.single_eq_set_indicator @[simp] theorem single_eq_same : (single a b : α →₀ M) a = b := by @@ -335,7 +335,7 @@ theorem single_eq_of_ne (h : a ≠ a') : (single a b : α →₀ M) a' = 0 := by theorem single_eq_update [DecidableEq α] (a : α) (b : M) : ⇑(single a b) = Function.update (0 : _) a b := - by classical rw [single_eq_indicator, ← Set.piecewise_eq_indicator, Set.piecewise_singleton] + by classical rw [single_eq_set_indicator, ← Set.piecewise_eq_indicator, Set.piecewise_singleton] #align finsupp.single_eq_update Finsupp.single_eq_update theorem single_eq_pi_single [DecidableEq α] (a : α) (b : M) : ⇑(single a b) = Pi.single a b := @@ -382,7 +382,7 @@ theorem single_injective (a : α) : Function.Injective (single a : M → α → #align finsupp.single_injective Finsupp.single_injective theorem single_apply_eq_zero {a x : α} {b : M} : single a b x = 0 ↔ x = a → b = 0 := by - simp [single_eq_indicator] + simp [single_eq_set_indicator] #align finsupp.single_apply_eq_zero Finsupp.single_apply_eq_zero theorem single_apply_ne_zero {a x : α} {b : M} : single a b x ≠ 0 ↔ x = a ∧ b ≠ 0 := by @@ -438,7 +438,8 @@ theorem support_single_disjoint {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : #align finsupp.support_single_disjoint Finsupp.support_single_disjoint @[simp] -theorem single_eq_zero : single a b = 0 ↔ b = 0 := by simp [FunLike.ext_iff, single_eq_indicator] +theorem single_eq_zero : single a b = 0 ↔ b = 0 := by + simp [FunLike.ext_iff, single_eq_set_indicator] #align finsupp.single_eq_zero Finsupp.single_eq_zero theorem single_swap (a₁ a₂ : α) (b : M) : single a₁ b a₂ = single a₂ b a₁ := by diff --git a/Mathlib/Data/Finsupp/Indicator.lean b/Mathlib/Data/Finsupp/Indicator.lean index d4886ae1c5fba..a6dede302d11c 100644 --- a/Mathlib/Data/Finsupp/Indicator.lean +++ b/Mathlib/Data/Finsupp/Indicator.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies ! This file was ported from Lean 3 source module data.finsupp.indicator -! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c +! leanprover-community/mathlib commit 842328d9df7e96fd90fc424e115679c15fb23a71 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -74,4 +74,10 @@ theorem support_indicator_subset : ((indicator s f).support : Set ι) ⊆ s := b exact hi (indicator_of_not_mem h _) #align finsupp.support_indicator_subset Finsupp.support_indicator_subset +lemma single_eq_indicator (b : α) : single i b = indicator {i} (fun _ _ => b) := by + classical + ext j + simp [single_apply, indicator_apply, @eq_comm _ j] +#align finsupp.single_eq_indicator Finsupp.single_eq_indicator + end Finsupp