Mathlib.Algebra.BigOperators.Finsupp.Basic

Finsupp.prod definition

[Zero M] [CommMonoid N] (f : α →₀ M) (g : α → M → N) : N

Full source

/-- `prod f g` is the product of `g a (f a)` over the support of `f`. -/
@[to_additive "`sum f g` is the sum of `g a (f a)` over the support of `f`. "]
def prod [Zero M] [CommMonoid N] (f : α →₀ M) (g : α → M → N) : N :=
  ∏ a ∈ f.support, g a (f a)

Product over the support of a finitely supported function

Informal description

Given a commutative monoid $N$, a finitely supported function $f \colon \alpha \to M$ (where $M$ has a zero element), and a function $g \colon \alpha \to M \to N$, the product $\prod_{a \in \text{supp}(f)} g(a)(f(a))$ is defined as the product over the support of $f$ of the values $g(a)(f(a))$.

Finsupp.prod_of_support_subset theorem

 (f : α →₀ M) {s : Finset α} (hs : f.support ⊆ s) (g : α → M → N) (h : ∀ i ∈ s, g i 0 = 1) :
  f.prod g = ∏ x ∈ s, g x (f x)

Full source

@[to_additive]
theorem prod_of_support_subset (f : α →₀ M) {s : Finset α} (hs : f.support ⊆ s) (g : α → M → N)
    (h : ∀ i ∈ s, g i 0 = 1) : f.prod g = ∏ x ∈ s, g x (f x) := by
  refine Finset.prod_subset hs fun x hxs hx => h x hxs ▸ (congr_arg (g x) ?_)
  exact not_mem_support_iff.1 hx

Product Equality for Finitely Supported Functions with Trivial Extension

Informal description

Let $f \colon \alpha \to_{\text{f}} M$ be a finitely supported function from $\alpha$ to $M$ (where $M$ has a zero element), and let $s$ be a finite subset of $\alpha$ such that the support of $f$ is contained in $s$. Given a function $g \colon \alpha \to M \to N$ where $N$ is a commutative monoid, suppose that for every $i \in s$, $g(i)(0) = 1$. Then the product of $g$ over the support of $f$ equals the product of $g$ over $s$ evaluated at $f$, i.e., \[ \prod_{a \in \text{supp}(f)} g(a)(f(a)) = \prod_{x \in s} g(x)(f(x)). \]

Finsupp.prod_fintype theorem

[Fintype α] (f : α →₀ M) (g : α → M → N) (h : ∀ i, g i 0 = 1) : f.prod g = ∏ i, g i (f i)

Full source

@[to_additive]
theorem prod_fintype [Fintype α] (f : α →₀ M) (g : α → M → N) (h : ∀ i, g i 0 = 1) :
    f.prod g = ∏ i, g i (f i) :=
  f.prod_of_support_subset (subset_univ _) g fun x _ => h x

Product over Support Equals Product over Entire Finite Type for Finitely Supported Functions

Informal description

Let $\alpha$ be a finite type, $M$ a type with a zero element, and $N$ a commutative monoid. Given a finitely supported function $f \colon \alpha \to M$ and a function $g \colon \alpha \to M \to N$ such that $g(i)(0) = 1$ for all $i \in \alpha$, the product over the support of $f$ satisfies \[ \prod_{a \in \text{supp}(f)} g(a)(f(a)) = \prod_{i \in \alpha} g(i)(f(i)). \]

Finsupp.prod_single_index theorem

{a : α} {b : M} {h : α → M → N} (h_zero : h a 0 = 1) : (single a b).prod h = h a b

Full source

@[to_additive (attr := simp)]
theorem prod_single_index {a : α} {b : M} {h : α → M → N} (h_zero : h a 0 = 1) :
    (single a b).prod h = h a b :=
  calc
    (single a b).prod h = ∏ x ∈ {a}, h x (single a b x) :=
      prod_of_support_subset _ support_single_subset h fun _ hx =>
        (mem_singleton.1 hx).symm ▸ h_zero
    _ = h a b := by simp

Product over Single-Point Finitely Supported Function Equals Function Value

Informal description

Let $a \in \alpha$, $b \in M$, and $h \colon \alpha \to M \to N$ be a function such that $h(a, 0) = 1$ where $N$ is a commutative monoid. Then the product of $h$ over the support of the finitely supported function $\text{single}(a, b)$ equals $h(a, b)$, i.e., \[ \prod_{x \in \text{supp}(\text{single}(a, b))} h(x, \text{single}(a, b)(x)) = h(a, b). \]

Finsupp.prod_mapRange_index theorem

 {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h : α → M' → N} (h0 : ∀ a, h a 0 = 1) :
  (mapRange f hf g).prod h = g.prod fun a b => h a (f b)

Full source

@[to_additive]
theorem prod_mapRange_index {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h : α → M' → N}
    (h0 : ∀ a, h a 0 = 1) : (mapRange f hf g).prod h = g.prod fun a b => h a (f b) :=
  Finset.prod_subset support_mapRange fun _ _ H => by rw [not_mem_support_iff.1 H, h0]

Product Equality under Composition of Finitely Supported Functions: $\prod_{\text{supp}(f \circ g)} h = \prod_{\text{supp}(g)} h \circ f$

Informal description

Let $f \colon M \to M'$ be a function with $f(0) = 0$, and let $g \colon \alpha \to_{\text{f}} M$ be a finitely supported function. For any function $h \colon \alpha \to M' \to N$ where $N$ is a commutative monoid, if $h(a, 0) = 1$ for all $a \in \alpha$, then the product over the support of the composition $f \circ g$ satisfies \[ \prod_{a \in \text{supp}(f \circ g)} h(a, f(g(a))) = \prod_{a \in \text{supp}(g)} h(a, f(g(a))). \]

Finsupp.prod_zero_index theorem

{h : α → M → N} : (0 : α →₀ M).prod h = 1

Full source

@[to_additive (attr := simp)]
theorem prod_zero_index {h : α → M → N} : (0 : α →₀ M).prod h = 1 :=
  rfl

Product over Zero Finsupp Yields Identity

Informal description

For any function $h \colon \alpha \to M \to N$ where $N$ is a commutative monoid, the product over the support of the zero finitely supported function $0 \colon \alpha \to M$ is equal to the multiplicative identity $1$ in $N$, i.e., $\prod_{a \in \text{supp}(0)} h(a)(0(a)) = 1$.

Finsupp.prod_comm theorem

 (f : α →₀ M) (g : β →₀ M') (h : α → M → β → M' → N) :
  (f.prod fun x v => g.prod fun x' v' => h x v x' v') = g.prod fun x' v' => f.prod fun x v => h x v x' v'

Full source

@[to_additive]
theorem prod_comm (f : α →₀ M) (g : β →₀ M') (h : α → M → β → M' → N) :
    (f.prod fun x v => g.prod fun x' v' => h x v x' v') =
      g.prod fun x' v' => f.prod fun x v => h x v x' v' :=
  Finset.prod_comm

Commutativity of Double Product over Finitely Supported Functions

Informal description

Let $f \colon \alpha \to₀ M$ and $g \colon \beta \to₀ M'$ be finitely supported functions, and let $h \colon \alpha \to M \to \beta \to M' \to N$ be a function. Then the double product \[ \prod_{x \in \text{supp}(f)} \prod_{x' \in \text{supp}(g)} h(x, f(x), x', g(x')) \] is equal to the double product \[ \prod_{x' \in \text{supp}(g)} \prod_{x \in \text{supp}(f)} h(x, f(x), x', g(x')). \]

Finsupp.prod_ite_eq theorem

 [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M → N) :
  (f.prod fun x v => ite (a = x) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1

Full source

@[to_additive (attr := simp)]
theorem prod_ite_eq [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M → N) :
    (f.prod fun x v => ite (a = x) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1 := by
  dsimp [Finsupp.prod]
  rw [f.support.prod_ite_eq]

Product over Support with Indicator Function

Informal description

Let $\alpha$ be a type with decidable equality, $M$ a type with a zero element, and $N$ a commutative monoid. Given a finitely supported function $f \colon \alpha \to M$, an element $a \in \alpha$, and a function $b \colon \alpha \to M \to N$, we have: \[ \prod_{x \in \text{supp}(f)} \text{ite}(a = x, b(x)(f(x)), 1) = \text{ite}(a \in \text{supp}(f), b(a)(f(a)), 1) \] where $\text{ite}(P, x, y)$ denotes $x$ if $P$ is true and $y$ otherwise, and $\text{supp}(f)$ is the support of $f$.

Finsupp.sum_ite_self_eq theorem

[DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) : (f.sum fun x v => ite (a = x) v 0) = f a

Full source

theorem sum_ite_self_eq [DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) :
    (f.sum fun x v => ite (a = x) v 0) = f a := by
  classical
    convert f.sum_ite_eq a fun _ => id
    simp [ite_eq_right_iff.2 Eq.symm]

Sum of Indicator Function Equals Function Value for Finitely Supported Functions

Informal description

Let $\alpha$ be a type with decidable equality, $N$ an additive commutative monoid, and $f \colon \alpha \to₀ N$ a finitely supported function. For any $a \in \alpha$, we have \[ \sum_{x \in \text{supp}(f)} \text{ite}(a = x, f(x), 0) = f(a), \] where $\text{ite}(P, x, y)$ denotes $x$ if $P$ is true and $y$ otherwise, and $\text{supp}(f)$ is the support of $f$.

Finsupp.if_mem_support theorem

[DecidableEq α] {N : Type*} [Zero N] (f : α →₀ N) (a : α) : (if a ∈ f.support then f a else 0) = f a

Full source

/--
The left hand side of `sum_ite_self_eq` simplifies; this is the variant that is useful for `simp`.
-/
@[simp]
theorem if_mem_support [DecidableEq α] {N : Type*} [Zero N] (f : α →₀ N) (a : α) :
    (if a ∈ f.support then f a else 0) = f a := by
  simp only [mem_support_iff, ne_eq, ite_eq_left_iff, not_not]
  exact fun h ↦ h.symm

Value of Finitely Supported Function at Point in Support

Informal description

For a finitely supported function $f \colon \alpha \to N$ with $N$ having a zero element, and for any element $a \in \alpha$, the value of $f$ at $a$ is equal to $f(a)$ if $a$ is in the support of $f$, and zero otherwise. In other words, $\text{if } a \in \text{support}(f) \text{ then } f(a) \text{ else } 0 = f(a)$.

Finsupp.prod_ite_eq' theorem

 [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M → N) :
  (f.prod fun x v => ite (x = a) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1

Full source

/-- A restatement of `prod_ite_eq` with the equality test reversed. -/
@[to_additive (attr := simp) "A restatement of `sum_ite_eq` with the equality test reversed."]
theorem prod_ite_eq' [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M → N) :
    (f.prod fun x v => ite (x = a) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1 := by
  dsimp [Finsupp.prod]
  rw [f.support.prod_ite_eq']

Product of Indicator Function over Support of Finitely Supported Function

Informal description

Let $\alpha$ be a type with decidable equality, $M$ a type with a zero element, and $N$ a commutative monoid. Given a finitely supported function $f \colon \alpha \to M$, an element $a \in \alpha$, and a function $b \colon \alpha \to M \to N$, we have \[ \prod_{x \in \text{supp}(f)} \text{ite}(x = a, b(x, f(x)), 1) = \text{ite}(a \in \text{supp}(f), b(a, f(a)), 1), \] where $\text{ite}(P, x, y)$ denotes the value $x$ if $P$ is true and $y$ otherwise, and $\text{supp}(f)$ is the support of $f$.

Finsupp.sum_ite_self_eq' theorem

[DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) : (f.sum fun x v => ite (x = a) v 0) = f a

Full source

/-- A restatement of `sum_ite_self_eq` with the equality test reversed. -/
theorem sum_ite_self_eq' [DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) :
    (f.sum fun x v => ite (x = a) v 0) = f a := by
  classical
    convert f.sum_ite_eq' a fun _ => id
    simp [ite_eq_right_iff.2 Eq.symm]

Sum over Support Evaluates to Function Value at Point

Informal description

Let $\alpha$ be a type with decidable equality and $N$ be an additive commutative monoid. Given a finitely supported function $f \colon \alpha \to N$ and an element $a \in \alpha$, the sum over the support of $f$ of the function $x \mapsto \text{ite}(x = a, f(x), 0)$ equals $f(a)$. In other words, \[ \sum_{x \in \text{supp}(f)} \begin{cases} f(x) & \text{if } x = a, \\ 0 & \text{otherwise} \end{cases} = f(a). \]

Finsupp.prod_pow theorem

[Fintype α] (f : α →₀ ℕ) (g : α → N) : (f.prod fun a b => g a ^ b) = ∏ a, g a ^ f a

Full source

@[to_additive (attr := simp)]
theorem prod_pow [Fintype α] (f : α →₀ ℕ) (g : α → N) :
    (f.prod fun a b => g a ^ b) = ∏ a, g a ^ f a :=
  f.prod_fintype _ fun _ ↦ pow_zero _

Product of Powers over Support Equals Product over Entire Finite Type

Informal description

Let $\alpha$ be a finite type and $N$ a commutative monoid. Given a finitely supported function $f \colon \alpha \to \mathbb{N}$ and a function $g \colon \alpha \to N$, the product over the support of $f$ of $g(a)^{f(a)}$ equals the product over all $a \in \alpha$ of $g(a)^{f(a)}$. That is, \[ \prod_{a \in \text{supp}(f)} g(a)^{f(a)} = \prod_{a \in \alpha} g(a)^{f(a)}. \]

Finsupp.prod_zpow theorem

 {N} [DivisionCommMonoid N] [Fintype α] (f : α →₀ ℤ) (g : α → N) : (f.prod fun a b => g a ^ b) = ∏ a, g a ^ f a

Full source

@[to_additive (attr := simp)]
theorem prod_zpow {N} [DivisionCommMonoid N] [Fintype α] (f : α →₀ ℤ) (g : α → N) :
    (f.prod fun a b => g a ^ b) = ∏ a, g a ^ f a :=
  f.prod_fintype _ fun _ ↦ zpow_zero _

Product of Integer Powers over Support Equals Product over Entire Finite Type for Finitely Supported Functions

Informal description

Let $\alpha$ be a finite type and $N$ be a commutative division monoid. Given a finitely supported function $f \colon \alpha \to \mathbb{Z}$ and a function $g \colon \alpha \to N$, the product over the support of $f$ of the terms $g(a)^{f(a)}$ equals the product over all elements $a \in \alpha$ of the terms $g(a)^{f(a)}$. In other words, \[ \prod_{a \in \text{supp}(f)} g(a)^{f(a)} = \prod_{a \in \alpha} g(a)^{f(a)}. \]

Finsupp.onFinset_prod theorem

 {s : Finset α} {f : α → M} {g : α → M → N} (hf : ∀ a, f a ≠ 0 → a ∈ s) (hg : ∀ a, g a 0 = 1) :
  (onFinset s f hf).prod g = ∏ a ∈ s, g a (f a)

Full source

/-- If `g` maps a second argument of 0 to 1, then multiplying it over the
result of `onFinset` is the same as multiplying it over the original `Finset`. -/
@[to_additive
      "If `g` maps a second argument of 0 to 0, summing it over the
      result of `onFinset` is the same as summing it over the original `Finset`."]
theorem onFinset_prod {s : Finset α} {f : α → M} {g : α → M → N} (hf : ∀ a, f a ≠ 0 → a ∈ s)
    (hg : ∀ a, g a 0 = 1) : (onFinset s f hf).prod g = ∏ a ∈ s, g a (f a) :=
  Finset.prod_subset support_onFinset_subset <| by simp +contextual [*]

Product over Support of Finitely Supported Function Equals Product over Given Finite Set

Informal description

Let $s$ be a finite subset of a type $\alpha$, $f \colon \alpha \to M$ a function (where $M$ has a zero element), and $g \colon \alpha \to M \to N$ a function (where $N$ is a commutative monoid). Suppose that: 1. $f$ is zero outside $s$ (i.e., $f(a) \neq 0$ implies $a \in s$), and 2. $g(a, 0) = 1$ for all $a \in \alpha$. Then the product of $g$ over the support of the finitely supported function $\text{onFinset}\, s\, f\, hf$ equals the product of $g(a, f(a))$ over $s$: \[ \prod_{a \in \text{supp}(\text{onFinset}\, s\, f\, hf)} g(a, f(a)) = \prod_{a \in s} g(a, f(a)). \]

Finsupp.mul_prod_erase theorem

(f : α →₀ M) (y : α) (g : α → M → N) (hyf : y ∈ f.support) : g y (f y) * (erase y f).prod g = f.prod g

Full source

/-- Taking a product over `f : α →₀ M` is the same as multiplying the value on a single element
`y ∈ f.support` by the product over `erase y f`. -/
@[to_additive
      " Taking a sum over `f : α →₀ M` is the same as adding the value on a
      single element `y ∈ f.support` to the sum over `erase y f`. "]
theorem mul_prod_erase (f : α →₀ M) (y : α) (g : α → M → N) (hyf : y ∈ f.support) :
    g y (f y) * (erase y f).prod g = f.prod g := by
  classical
    rw [Finsupp.prod, Finsupp.prod, ← Finset.mul_prod_erase _ _ hyf, Finsupp.support_erase,
      Finset.prod_congr rfl]
    intro h hx
    rw [Finsupp.erase_ne (ne_of_mem_erase hx)]

Product Decomposition for Finitely Supported Functions: $g(y, f(y)) \cdot \prod_{x \neq y} g(x, f(x)) = \prod_x g(x, f(x))$

Informal description

Let $M$ be a type with a zero element, $N$ a commutative monoid, $f \colon \alpha \to_{\text{f}} M$ a finitely supported function, and $g \colon \alpha \to M \to N$ a function. For any $y \in \alpha$ in the support of $f$, we have \[ g(y, f(y)) \cdot \prod_{x \in \text{supp}(f) \setminus \{y\}} g(x, f(x)) = \prod_{x \in \text{supp}(f)} g(x, f(x)). \]

Finsupp.mul_prod_erase' theorem

 (f : α →₀ M) (y : α) (g : α → M → N) (hg : ∀ i : α, g i 0 = 1) : g y (f y) * (erase y f).prod g = f.prod g

Full source

/-- Generalization of `Finsupp.mul_prod_erase`: if `g` maps a second argument of 0 to 1,
then its product over `f : α →₀ M` is the same as multiplying the value on any element
`y : α` by the product over `erase y f`. -/
@[to_additive
      " Generalization of `Finsupp.add_sum_erase`: if `g` maps a second argument of 0
      to 0, then its sum over `f : α →₀ M` is the same as adding the value on any element
      `y : α` to the sum over `erase y f`. "]
theorem mul_prod_erase' (f : α →₀ M) (y : α) (g : α → M → N) (hg : ∀ i : α, g i 0 = 1) :
    g y (f y) * (erase y f).prod g = f.prod g := by
  classical
    by_cases hyf : y ∈ f.support
    · exact Finsupp.mul_prod_erase f y g hyf
    · rw [not_mem_support_iff.mp hyf, hg y, erase_of_not_mem_support hyf, one_mul]

Generalized Product Decomposition for Finitely Supported Functions with $g(i,0)=1$

Informal description

Let $M$ be a type with a zero element, $N$ a commutative monoid, $f \colon \alpha \to_{\text{f}} M$ a finitely supported function, and $g \colon \alpha \to M \to N$ a function such that $g(i, 0) = 1$ for all $i \in \alpha$. Then for any $y \in \alpha$, we have \[ g(y, f(y)) \cdot \prod_{x \in \text{supp}(f) \setminus \{y\}} g(x, f(x)) = \prod_{x \in \text{supp}(f)} g(x, f(x)). \]

SubmonoidClass.finsuppProd_mem theorem

 {S : Type*} [SetLike S N] [SubmonoidClass S N] (s : S) (f : α →₀ M) (g : α → M → N)
  (h : ∀ c, f c ≠ 0 → g c (f c) ∈ s) : f.prod g ∈ s

Full source

@[to_additive]
theorem _root_.SubmonoidClass.finsuppProd_mem {S : Type*} [SetLike S N] [SubmonoidClass S N]
    (s : S) (f : α →₀ M) (g : α → M → N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ s) : f.prod g ∈ s :=
  prod_mem fun _i hi => h _ (Finsupp.mem_support_iff.mp hi)

Product of Finitely Supported Function Values Belongs to Submonoid

Informal description

Let $N$ be a commutative monoid, $S$ a submonoid of $N$ (represented by a set-like structure with submonoid properties), and $f \colon \alpha \to_{\text{f}} M$ a finitely supported function. Given a function $g \colon \alpha \to M \to N$ such that for every $c \in \alpha$ with $f(c) \neq 0$, we have $g(c)(f(c)) \in S$, then the product $\prod_{a \in \text{supp}(f)} g(a)(f(a))$ belongs to $S$.

Finsupp.prod_congr theorem

{f : α →₀ M} {g1 g2 : α → M → N} (h : ∀ x ∈ f.support, g1 x (f x) = g2 x (f x)) : f.prod g1 = f.prod g2

Full source

@[to_additive]
theorem prod_congr {f : α →₀ M} {g1 g2 : α → M → N} (h : ∀ x ∈ f.support, g1 x (f x) = g2 x (f x)) :
    f.prod g1 = f.prod g2 :=
  Finset.prod_congr rfl h

Product Equality for Finitely Supported Functions under Pointwise Congruence

Informal description

Let $f \colon \alpha \to₀ M$ be a finitely supported function, and let $g_1, g_2 \colon \alpha \to M \to N$ be functions where $N$ is a commutative monoid. If for every $x$ in the support of $f$ we have $g_1(x)(f(x)) = g_2(x)(f(x))$, then the products of $g_1$ and $g_2$ over the support of $f$ are equal, i.e., \[ \prod_{x \in \text{supp}(f)} g_1(x)(f(x)) = \prod_{x \in \text{supp}(f)} g_2(x)(f(x)). \]

Finsupp.prod_eq_single theorem

 {f : α →₀ M} (a : α) {g : α → M → N} (h₀ : ∀ b, f b ≠ 0 → b ≠ a → g b (f b) = 1) (h₁ : f a = 0 → g a 0 = 1) :
  f.prod g = g a (f a)

Full source

@[to_additive]
theorem prod_eq_single {f : α →₀ M} (a : α) {g : α → M → N}
    (h₀ : ∀ b, f b ≠ 0 → b ≠ a → g b (f b) = 1) (h₁ : f a = 0 → g a 0 = 1) :
    f.prod g = g a (f a) := by
  refine Finset.prod_eq_single a (fun b hb₁ hb₂ => ?_) (fun h => ?_)
  · exact h₀ b (mem_support_iff.mp hb₁) hb₂
  · simp only [not_mem_support_iff] at h
    rw [h]
    exact h₁ h

Product over Finitely Supported Function Equals Single Non-Trivial Value

Informal description

Let $f \colon \alpha \to_{\text{f}} M$ be a finitely supported function, $N$ a commutative monoid, and $g \colon \alpha \to M \to N$ a function. Given an element $a \in \alpha$ such that: 1. For all $b \in \alpha$ with $f(b) \neq 0$ and $b \neq a$, we have $g(b)(f(b)) = 1$, and 2. If $f(a) = 0$, then $g(a)(0) = 1$, then the product $\prod_{x \in \text{supp}(f)} g(x)(f(x))$ equals $g(a)(f(a))$, i.e., \[ \prod_{x \in \text{supp}(f)} g(x)(f(x)) = g(a)(f(a)). \]

Finsupp.prod_eq_zero_iff theorem

: f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0

Full source

@[simp]
lemma prod_eq_zero_iff : f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0 := Finset.prod_eq_zero_iff

Product over Finitely Supported Function Equals Zero Iff Some Term is Zero

Informal description

For a finitely supported function $f \colon \alpha \to M$ (where $M$ has a zero element), a commutative monoid $N$, and a function $g \colon \alpha \to M \to N$, the product $\prod_{i \in \text{supp}(f)} g(i)(f(i))$ equals zero if and only if there exists an element $i$ in the support of $f$ such that $g(i)(f(i)) = 0$.

Finsupp.prod_ne_zero_iff theorem

: f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0

Full source

lemma prod_ne_zero_iff : f.prod g ≠ 0f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0 := Finset.prod_ne_zero_iff

Nonzero Product Condition for Finitely Supported Functions

Informal description

For a finitely supported function $f \colon \alpha \to M$ (where $M$ has a zero element), a commutative monoid $N$, and a function $g \colon \alpha \to M \to N$, the product $\prod_{i \in \text{supp}(f)} g(i)(f(i))$ is nonzero if and only if $g(i)(f(i)) \neq 0$ for every $i$ in the support of $f$.

map_finsuppProd theorem

 [Zero M] [CommMonoid N] [CommMonoid P] {H : Type*} [FunLike H N P] [MonoidHomClass H N P] (h : H) (f : α →₀ M)
  (g : α → M → N) : h (f.prod g) = f.prod fun a b => h (g a b)

Full source

@[to_additive]
theorem map_finsuppProd [Zero M] [CommMonoid N] [CommMonoid P] {H : Type*}
    [FunLike H N P] [MonoidHomClass H N P]
    (h : H) (f : α →₀ M) (g : α → M → N) : h (f.prod g) = f.prod fun a b => h (g a b) :=
  map_prod h _ _

Monoid Homomorphism Commutes with Finite Product over Finitely Supported Function

Informal description

Let $M$ be a type with a zero element, and let $N$ and $P$ be commutative monoids. Given a monoid homomorphism $h \colon N \to P$, a finitely supported function $f \colon \alpha \to M$, and a function $g \colon \alpha \to M \to N$, we have \[ h\left( \prod_{a \in \text{supp}(f)} g(a)(f(a)) \right) = \prod_{a \in \text{supp}(f)} h(g(a)(f(a))). \]

MonoidHom.coe_finsuppProd theorem

 [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β) (g : α → β → N →* P) : ⇑(f.prod g) = f.prod fun i fi => ⇑(g i fi)

Full source

@[to_additive]
theorem MonoidHom.coe_finsuppProd [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β)
    (g : α → β → N →* P) : ⇑(f.prod g) = f.prod fun i fi => ⇑(g i fi) :=
  MonoidHom.coe_finset_prod _ _

Coefficient of Product of Monoid Homomorphisms Equals Pointwise Product of Coefficients

Informal description

Let $\beta$ be a type with a zero element, $N$ a monoid, and $P$ a commutative monoid. Given a finitely supported function $f \colon \alpha \to \beta$ and a family of monoid homomorphisms $g_i \colon \beta \to (N \to^* P)$ indexed by $\alpha$, the underlying function of the product homomorphism $\prod_{i \in \alpha} g_i(f(i))$ is equal to the pointwise product $\prod_{i \in \text{supp}(f)} g_i(f(i))$.

MonoidHom.finsuppProd_apply theorem

 [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β) (g : α → β → N →* P) (x : N) :
  f.prod g x = f.prod fun i fi => g i fi x

Full source

@[to_additive (attr := simp)]
theorem MonoidHom.finsuppProd_apply [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β)
    (g : α → β → N →* P) (x : N) : f.prod g x = f.prod fun i fi => g i fi x :=
  MonoidHom.finset_prod_apply _ _ _

Evaluation of Product of Monoid Homomorphisms over Finitely Supported Function

Informal description

Let $\beta$ be a type with a zero element, $N$ a multiplicative monoid with identity, and $P$ a commutative monoid. Given a finitely supported function $f \colon \alpha \to \beta$, a family of monoid homomorphisms $g \colon \alpha \to \beta \to (N \to^* P)$, and an element $x \in N$, the evaluation of the product $\prod_{i \in \text{supp}(f)} g(i)(f(i))$ at $x$ is equal to the product $\prod_{i \in \text{supp}(f)} (g(i)(f(i)))(x)$.

Finsupp.single_multiset_sum theorem

[AddCommMonoid M] (s : Multiset M) (a : α) : single a s.sum = (s.map (single a)).sum

Full source

theorem single_multiset_sum [AddCommMonoid M] (s : Multiset M) (a : α) :
    single a s.sum = (s.map (single a)).sum :=
  Multiset.induction_on s (single_zero _) fun a s ih => by
    rw [Multiset.sum_cons, single_add, ih, Multiset.map_cons, Multiset.sum_cons]

Sum of Single-Point Finitely Supported Functions over a Multiset

Informal description

Let $M$ be an additive commutative monoid and $\alpha$ be a type. For any multiset $s$ of elements in $M$ and any element $a \in \alpha$, the finitely supported function $\operatorname{single}(a, \sum s)$ is equal to the sum of the multiset obtained by applying $\operatorname{single}(a, \cdot)$ to each element of $s$. That is, \[ \operatorname{single}\left(a, \sum_{x \in s} x\right) = \sum_{x \in s} \operatorname{single}(a, x). \]

Finsupp.single_finset_sum theorem

[AddCommMonoid M] (s : Finset ι) (f : ι → M) (a : α) : single a (∑ b ∈ s, f b) = ∑ b ∈ s, single a (f b)

Full source

theorem single_finset_sum [AddCommMonoid M] (s : Finset ι) (f : ι → M) (a : α) :
    single a (∑ b ∈ s, f b) = ∑ b ∈ s, single a (f b) := by
  trans
  · apply single_multiset_sum
  · rw [Multiset.map_map]
    rfl

Sum of Single-Point Finitely Supported Functions over a Finite Set

Informal description

Let $M$ be an additive commutative monoid, $\alpha$ and $\iota$ be types, $s$ be a finite subset of $\iota$, and $f \colon \iota \to M$ be a function. For any element $a \in \alpha$, the finitely supported function $\operatorname{single}(a, \sum_{b \in s} f(b))$ is equal to the sum over $s$ of the finitely supported functions $\operatorname{single}(a, f(b))$. That is, \[ \operatorname{single}\left(a, \sum_{b \in s} f(b)\right) = \sum_{b \in s} \operatorname{single}(a, f(b)). \]

Finsupp.single_sum theorem

 [Zero M] [AddCommMonoid N] (s : ι →₀ M) (f : ι → M → N) (a : α) :
  single a (s.sum f) = s.sum fun d c => single a (f d c)

Full source

theorem single_sum [Zero M] [AddCommMonoid N] (s : ι →₀ M) (f : ι → M → N) (a : α) :
    single a (s.sum f) = s.sum fun d c => single a (f d c) :=
  single_finset_sum _ _ _

Sum of Single-Point Finitely Supported Functions over a Finitely Supported Function

Informal description

Let $M$ be a type with a zero element, $N$ an additive commutative monoid, $s \colon \iota \to_{\text{f}} M$ a finitely supported function, and $f \colon \iota \to M \to N$ a function. For any $a \in \alpha$, the finitely supported function $\operatorname{single}(a, \sum_{d \in \iota} f(d, s(d)))$ is equal to the sum over $\iota$ of the finitely supported functions $\operatorname{single}(a, f(d, s(d)))$. That is, \[ \operatorname{single}\left(a, \sum_{d \in \iota} f(d, s(d))\right) = \sum_{d \in \iota} \operatorname{single}(a, f(d, s(d))). \]

Finsupp.prod_neg_index theorem

 [SubtractionMonoid G] [CommMonoid M] {g : α →₀ G} {h : α → G → M} (h0 : ∀ a, h a 0 = 1) :
  (-g).prod h = g.prod fun a b => h a (-b)

Full source

@[to_additive]
theorem prod_neg_index [SubtractionMonoid G] [CommMonoid M] {g : α →₀ G} {h : α → G → M}
    (h0 : ∀ a, h a 0 = 1) : (-g).prod h = g.prod fun a b => h a (-b) :=
  prod_mapRange_index h0

Product Equality under Negation of Finitely Supported Function: $\prod_{\text{supp}(-g)} h = \prod_{\text{supp}(g)} h \circ (-)$

Informal description

Let $G$ be a subtraction monoid, $M$ a commutative monoid, and $g \colon \alpha \to_{\text{f}} G$ a finitely supported function. For any function $h \colon \alpha \to G \to M$ satisfying $h(a, 0) = 1$ for all $a \in \alpha$, the product over the support of $-g$ satisfies \[ \prod_{a \in \text{supp}(-g)} h(a, -g(a)) = \prod_{a \in \text{supp}(g)} h(a, -g(a)). \]

Finsupp.finset_sum_apply theorem

[AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) (a : α) : (∑ i ∈ S, f i) a = ∑ i ∈ S, f i a

Full source

theorem finset_sum_apply [AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) (a : α) :
    (∑ i ∈ S, f i) a = ∑ i ∈ S, f i a :=
  map_sum (applyAddHom a) _ _

Evaluation of Finite Sum of Finitely Supported Functions is Sum of Evaluations

Informal description

Let $N$ be an additive commutative monoid, $S$ a finite set of indices, and $f \colon \iota \to (\alpha \to_{\text{f}} N)$ a family of finitely supported functions from $\alpha$ to $N$. For any $a \in \alpha$, the evaluation of the sum of the family $f$ at $a$ is equal to the sum of the evaluations of each $f_i$ at $a$: \[ \left( \sum_{i \in S} f_i \right)(a) = \sum_{i \in S} f_i(a). \]

Finsupp.sum_apply theorem

 [Zero M] [AddCommMonoid N] {f : α →₀ M} {g : α → M → β →₀ N} {a₂ : β} : (f.sum g) a₂ = f.sum fun a₁ b => g a₁ b a₂

Full source

@[simp]
theorem sum_apply [Zero M] [AddCommMonoid N] {f : α →₀ M} {g : α → M → β →₀ N} {a₂ : β} :
    (f.sum g) a₂ = f.sum fun a₁ b => g a₁ b a₂ :=
  finset_sum_apply _ _ _

Evaluation of Sum of Finitely Supported Functions is Sum of Evaluations

Informal description

Let $M$ be a type with a zero element and $N$ be an additive commutative monoid. Given a finitely supported function $f \colon \alpha \to_{\text{f}} M$, a function $g \colon \alpha \to M \to (\beta \to_{\text{f}} N)$, and an element $a_2 \in \beta$, the evaluation of the sum $f.sum \, g$ at $a_2$ is equal to the sum over $f$ of the evaluations of $g$ at $a_2$: \[ (f.sum \, g)(a_2) = \sum_{(a_1, b) \in f} g(a_1, b)(a_2). \]

Finsupp.coe_finset_sum theorem

[AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) : ⇑(∑ i ∈ S, f i) = ∑ i ∈ S, ⇑(f i)

Full source

@[simp, norm_cast] theorem coe_finset_sum [AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) :
    ⇑(∑ i ∈ S, f i) = ∑ i ∈ S, ⇑(f i) :=
  map_sum (coeFnAddHom : (α →₀ N) →+ _) _ _

Pointwise Sum of Finitely Supported Functions

Informal description

Let $N$ be an additive commutative monoid, $S$ be a finite set of indices $\iota$, and $f : \iota \to \alpha \to_{\text{f}} N$ be a family of finitely supported functions. Then the underlying function of the sum $\sum_{i \in S} f_i$ is equal to the pointwise sum of the underlying functions, i.e., \[ \left(\sum_{i \in S} f_i\right)(a) = \sum_{i \in S} f_i(a) \] for all $a \in \alpha$.

Finsupp.coe_sum theorem

 [Zero M] [AddCommMonoid N] (f : α →₀ M) (g : α → M → β →₀ N) : ⇑(f.sum g) = f.sum fun a₁ b => ⇑(g a₁ b)

Full source

@[simp, norm_cast] theorem coe_sum [Zero M] [AddCommMonoid N] (f : α →₀ M) (g : α → M → β →₀ N) :
    ⇑(f.sum g) = f.sum fun a₁ b => ⇑(g a₁ b) :=
  coe_finset_sum _ _

Pointwise Sum of Finitely Supported Functions via Summation

Informal description

Let $M$ be a type with a zero element and $N$ be an additive commutative monoid. Given a finitely supported function $f \colon \alpha \to_{\text{f}} M$ and a function $g \colon \alpha \to M \to (\beta \to_{\text{f}} N)$, the underlying function of the sum $f.sum \, g$ is equal to the pointwise sum of the underlying functions of $g$ evaluated over $f$: \[ (f.sum \, g)(a) = \sum_{(a_1, b) \in f} g(a_1, b)(a) \] for all $a \in \beta$.

Finsupp.support_sum theorem

 [DecidableEq β] [Zero M] [AddCommMonoid N] {f : α →₀ M} {g : α → M → β →₀ N} :
  (f.sum g).support ⊆ f.support.biUnion fun a => (g a (f a)).support

Full source

theorem support_sum [DecidableEq β] [Zero M] [AddCommMonoid N] {f : α →₀ M} {g : α → M → β →₀ N} :
    (f.sum g).support ⊆ f.support.biUnion fun a => (g a (f a)).support := by
  have : ∀ c, (f.sum fun a b => g a b c) ≠ 0 → ∃ a, f a ≠ 0 ∧ ¬(g a (f a)) c = 0 := fun a₁ h =>
    let ⟨a, ha, ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
    ⟨a, mem_support_iff.mp ha, ne⟩
  simpa only [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply, exists_prop]

Support of Sum of Finitely Supported Functions is Contained in Union of Supports

Informal description

Let $\beta$ be a type with decidable equality, $M$ a type with a zero element, and $N$ an additive commutative monoid. Given a finitely supported function $f \colon \alpha \to_{\text{f}} M$ and a function $g \colon \alpha \to M \to (\beta \to_{\text{f}} N)$, the support of the sum $f.sum \, g$ is contained in the union of the supports of the functions $g(a, f(a))$ for $a$ in the support of $f$. That is, \[ \operatorname{supp}(f.sum \, g) \subseteq \bigcup_{a \in \operatorname{supp}(f)} \operatorname{supp}(g(a, f(a))). \]

Finsupp.support_finset_sum theorem

 [DecidableEq β] [AddCommMonoid M] {s : Finset α} {f : α → β →₀ M} :
  (Finset.sum s f).support ⊆ s.biUnion fun x => (f x).support

Full source

theorem support_finset_sum [DecidableEq β] [AddCommMonoid M] {s : Finset α} {f : α → β →₀ M} :
    (Finset.sum s f).support ⊆ s.biUnion fun x => (f x).support := by
  rw [← Finset.sup_eq_biUnion]
  induction s using Finset.cons_induction_on with
  | empty => rfl
  | cons _ _ _ ih =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)

Support of Finite Sum of Finitely Supported Functions is Contained in Union of Supports

Informal description

Let $\beta$ be a type with decidable equality and $M$ an additive commutative monoid. For any finite set $s$ of type $\alpha$ and any family of finitely supported functions $f \colon \alpha \to (\beta \to_{\text{f}} M)$, the support of the sum $\sum_{x \in s} f(x)$ is contained in the union of the supports of the $f(x)$ for $x \in s$. That is, \[ \operatorname{supp}\left(\sum_{x \in s} f(x)\right) \subseteq \bigcup_{x \in s} \operatorname{supp}(f(x)). \]

Finsupp.sum_zero theorem

[Zero M] [AddCommMonoid N] {f : α →₀ M} : (f.sum fun _ _ => (0 : N)) = 0

Full source

@[simp]
theorem sum_zero [Zero M] [AddCommMonoid N] {f : α →₀ M} : (f.sum fun _ _ => (0 : N)) = 0 :=
  Finset.sum_const_zero

Sum of Zero Function over Finitely Supported Function is Zero

Informal description

For any finitely supported function $f \colon \alpha \to M$ (where $M$ has a zero element) and any additive commutative monoid $N$, the sum of the zero function over the support of $f$ is equal to zero. That is, \[ \sum_{a \in \text{supp}(f)} 0 = 0. \]

Finsupp.prod_mul theorem

 [Zero M] [CommMonoid N] {f : α →₀ M} {h₁ h₂ : α → M → N} : (f.prod fun a b => h₁ a b * h₂ a b) = f.prod h₁ * f.prod h₂

Full source

@[to_additive (attr := simp)]
theorem prod_mul [Zero M] [CommMonoid N] {f : α →₀ M} {h₁ h₂ : α → M → N} :
    (f.prod fun a b => h₁ a b * h₂ a b) = f.prod h₁ * f.prod h₂ :=
  Finset.prod_mul_distrib

Product of Pointwise Products Equals Product of Products for Finitely Supported Functions

Informal description

Let $M$ be a type with a zero element and $N$ be a commutative monoid. For any finitely supported function $f \colon \alpha \to M$ and any two functions $h_1, h_2 \colon \alpha \to M \to N$, the product over the support of $f$ of the pointwise product $h_1(a, b) \cdot h_2(a, b)$ is equal to the product of the individual products: \[ \prod_{a \in \text{supp}(f)} (h_1(a, f(a)) \cdot h_2(a, f(a))) = \left(\prod_{a \in \text{supp}(f)} h_1(a, f(a))\right) \cdot \left(\prod_{a \in \text{supp}(f)} h_2(a, f(a))\right). \]

Finsupp.prod_inv theorem

[Zero M] [CommGroup G] {f : α →₀ M} {h : α → M → G} : (f.prod fun a b => (h a b)⁻¹) = (f.prod h)⁻¹

Full source

@[to_additive (attr := simp)]
theorem prod_inv [Zero M] [CommGroup G] {f : α →₀ M} {h : α → M → G} :
    (f.prod fun a b => (h a b)⁻¹) = (f.prod h)⁻¹ :=
  (map_prod (MonoidHom.id G)⁻¹ _ _).symm

Inverse of Product Equals Product of Inverses for Finitely Supported Functions

Informal description

Let $M$ be a type with a zero element and $G$ be a commutative group. For any finitely supported function $f \colon \alpha \to M$ and any function $h \colon \alpha \to M \to G$, the product of the inverses of $h(a)(f(a))$ over the support of $f$ equals the inverse of the product of $h(a)(f(a))$ over the same support. That is, \[ \prod_{a \in \text{supp}(f)} (h(a)(f(a)))^{-1} = \left( \prod_{a \in \text{supp}(f)} h(a)(f(a)) \right)^{-1}. \]

Finsupp.sum_sub theorem

 [Zero M] [SubtractionCommMonoid G] {f : α →₀ M} {h₁ h₂ : α → M → G} :
  (f.sum fun a b => h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂

Full source

@[simp]
theorem sum_sub [Zero M] [SubtractionCommMonoid G] {f : α →₀ M} {h₁ h₂ : α → M → G} :
    (f.sum fun a b => h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂ :=
  Finset.sum_sub_distrib

Linearity of Summation over Differences in Finitely Supported Functions

Informal description

Let $\alpha$ be a type, $M$ a type with a zero element, and $G$ a commutative subtraction monoid. For any finitely supported function $f \colon \alpha \to₀ M$ and any two functions $h_1, h_2 \colon \alpha \to M \to G$, the sum over $f$ of the differences $h_1(a, b) - h_2(a, b)$ equals the difference of the sums $\sum_{a \in \alpha} h_1(a, f(a)) - \sum_{a \in \alpha} h_2(a, f(a))$.

Finsupp.prod_add_index theorem

 [DecidableEq α] [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} {h : α → M → N}
  (h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1)
  (h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂), h a (b₁ + b₂) = h a b₁ * h a b₂) :
  (f + g).prod h = f.prod h * g.prod h

Full source

/-- Taking the product under `h` is an additive-to-multiplicative homomorphism of finsupps,
if `h` is an additive-to-multiplicative homomorphism on the support.
This is a more general version of `Finsupp.prod_add_index'`; the latter has simpler hypotheses. -/
@[to_additive
      "Taking the product under `h` is an additive homomorphism of finsupps, if `h` is an
      additive homomorphism on the support. This is a more general version of
      `Finsupp.sum_add_index'`; the latter has simpler hypotheses."]
theorem prod_add_index [DecidableEq α] [AddZeroClass M] [CommMonoid N] {f g : α →₀ M}
    {h : α → M → N} (h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1)
    (h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂), h a (b₁ + b₂) = h a b₁ * h a b₂) :
    (f + g).prod h = f.prod h * g.prod h := by
  rw [Finsupp.prod_of_support_subset f subset_union_left h h_zero,
    Finsupp.prod_of_support_subset g subset_union_right h h_zero, ←
    Finset.prod_mul_distrib, Finsupp.prod_of_support_subset (f + g) Finsupp.support_add h h_zero]
  exact Finset.prod_congr rfl fun x hx => by apply h_add x hx

Product over Sum of Finitely Supported Functions Equals Product of Products under Multiplicative Homomorphism

Informal description

Let $\alpha$ be a type with decidable equality, $M$ an additive monoid, and $N$ a commutative monoid. Given two finitely supported functions $f, g \colon \alpha \to_{\text{f}} M$ and a function $h \colon \alpha \to M \to N$ such that: 1. For all $a$ in the union of the supports of $f$ and $g$, $h(a, 0) = 1$ (where $0$ is the zero element of $M$). 2. For all $a$ in the union of the supports of $f$ and $g$, and for all $b_1, b_2 \in M$, $h(a, b_1 + b_2) = h(a, b_1) \cdot h(a, b_2)$ (i.e., $h(a, \cdot)$ is multiplicative). Then the product of $h$ over the support of $f + g$ equals the product of $h$ over the support of $f$ multiplied by the product of $h$ over the support of $g$: \[ \prod_{a \in \text{supp}(f + g)} h(a, (f + g)(a)) = \left(\prod_{a \in \text{supp}(f)} h(a, f(a))\right) \cdot \left(\prod_{a \in \text{supp}(g)} h(a, g(a))\right). \]

Finsupp.prod_add_index' theorem

 [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ a, h a 0 = 1)
  (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) : (f + g).prod h = f.prod h * g.prod h

Full source

/-- Taking the product under `h` is an additive-to-multiplicative homomorphism of finsupps,
if `h` is an additive-to-multiplicative homomorphism.
This is a more specialized version of `Finsupp.prod_add_index` with simpler hypotheses. -/
@[to_additive
      "Taking the sum under `h` is an additive homomorphism of finsupps,if `h` is an additive
      homomorphism. This is a more specific version of `Finsupp.sum_add_index` with simpler
      hypotheses."]
theorem prod_add_index' [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} {h : α → M → N}
    (h_zero : ∀ a, h a 0 = 1) (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
    (f + g).prod h = f.prod h * g.prod h := by
  classical exact prod_add_index (fun a _ => h_zero a) fun a _ => h_add a

Product over Sum of Finitely Supported Functions Equals Product of Products under Pointwise Multiplicative Homomorphism

Informal description

Let $M$ be an additive monoid and $N$ a commutative monoid. Given two finitely supported functions $f, g \colon \alpha \to_{\text{f}} M$ and a function $h \colon \alpha \to M \to N$ such that: 1. For all $a \in \alpha$, $h(a, 0) = 1$ (where $0$ is the zero element of $M$). 2. For all $a \in \alpha$ and $b_1, b_2 \in M$, $h(a, b_1 + b_2) = h(a, b_1) \cdot h(a, b_2)$ (i.e., $h(a, \cdot)$ is multiplicative). Then the product of $h$ over the support of $f + g$ equals the product of $h$ over the support of $f$ multiplied by the product of $h$ over the support of $g$: \[ \prod_{a \in \text{supp}(f + g)} h(a, (f + g)(a)) = \left(\prod_{a \in \text{supp}(f)} h(a, f(a))\right) \cdot \left(\prod_{a \in \text{supp}(g)} h(a, g(a))\right). \]

Finsupp.sum_hom_add_index theorem

 [AddZeroClass M] [AddCommMonoid N] {f g : α →₀ M} (h : α → M →+ N) :
  ((f + g).sum fun x => h x) = (f.sum fun x => h x) + g.sum fun x => h x

Full source

@[simp]
theorem sum_hom_add_index [AddZeroClass M] [AddCommMonoid N] {f g : α →₀ M} (h : α → M →+ N) :
    ((f + g).sum fun x => h x) = (f.sum fun x => h x) + g.sum fun x => h x :=
  sum_add_index' (fun a => (h a).map_zero) fun a => (h a).map_add

Additivity of Sum over Finitely Supported Functions under Additive Homomorphisms

Informal description

Let $M$ be an additive monoid and $N$ an additive commutative monoid. Given two finitely supported functions $f, g \colon \alpha \to_{\text{f}} M$ and a family of additive monoid homomorphisms $h \colon \alpha \to (M \to^+ N)$, the sum of $h$ over the support of $f + g$ equals the sum of $h$ over the support of $f$ plus the sum of $h$ over the support of $g$: \[ \sum_{x \in \text{supp}(f + g)} h(x)((f + g)(x)) = \left(\sum_{x \in \text{supp}(f)} h(x)(f(x))\right) + \left(\sum_{x \in \text{supp}(g)} h(x)(g(x))\right). \]

Finsupp.prod_hom_add_index theorem

 [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} (h : α → Multiplicative M →* N) :
  ((f + g).prod fun a b => h a (Multiplicative.ofAdd b)) =
    (f.prod fun a b => h a (Multiplicative.ofAdd b)) * g.prod fun a b => h a (Multiplicative.ofAdd b)

Full source

@[simp]
theorem prod_hom_add_index [AddZeroClass M] [CommMonoid N] {f g : α →₀ M}
    (h : α → MultiplicativeMultiplicative M →* N) :
    ((f + g).prod fun a b => h a (Multiplicative.ofAdd b)) =
      (f.prod fun a b => h a (Multiplicative.ofAdd b)) *
        g.prod fun a b => h a (Multiplicative.ofAdd b) :=
  prod_add_index' (fun a => (h a).map_one) fun a => (h a).map_mul

Product Homomorphism Property for Sum of Finitely Supported Functions via Multiplicative Tag

Informal description

Let $M$ be an additive monoid and $N$ a commutative monoid. Given two finitely supported functions $f, g \colon \alpha \to_{\text{f}} M$ and a family of monoid homomorphisms $h \colon \alpha \to \text{Multiplicative}\,M \to^* N$, the product over the support of $f + g$ satisfies: \[ \prod_{a \in \text{supp}(f + g)} h(a, \text{ofAdd}((f + g)(a))) = \left(\prod_{a \in \text{supp}(f)} h(a, \text{ofAdd}(f(a)))\right) \cdot \left(\prod_{a \in \text{supp}(g)} h(a, \text{ofAdd}(g(a)))\right), \] where $\text{ofAdd} \colon M \to \text{Multiplicative}\,M$ is the canonical bijection between the additive and multiplicative structures.

Finsupp.liftAddHom definition

[AddZeroClass M] [AddCommMonoid N] : (α → M →+ N) ≃+ ((α →₀ M) →+ N)

Full source

/-- The canonical isomorphism between families of additive monoid homomorphisms `α → (M →+ N)`
and monoid homomorphisms `(α →₀ M) →+ N`. -/
def liftAddHom [AddZeroClass M] [AddCommMonoid N] : (α → M →+ N) ≃+ ((α →₀ M) →+ N) where
  toFun F :=
    { toFun := fun f ↦ f.sum fun x ↦ F x
      map_zero' := Finset.sum_empty
      map_add' := fun _ _ => sum_add_index' (fun x => (F x).map_zero) fun x => (F x).map_add }
  invFun F x := F.comp (singleAddHom x)
  left_inv F := by
    ext
    simp [singleAddHom]
  right_inv F := by
    ext
    simp [singleAddHom, AddMonoidHom.comp, Function.comp_def]
  map_add' F G := by
    ext x
    exact sum_add

Additive equivalence between families of additive homomorphisms and homomorphisms on finitely supported functions

Informal description

The canonical additive equivalence between families of additive monoid homomorphisms $\alpha \to (M \to^+ N)$ and additive monoid homomorphisms $(\alpha \to_{\text{f}} M) \to^+ N$. More precisely, for any types $\alpha$, $M$, and $N$ where $M$ is an add-zero class and $N$ is an additive commutative monoid, there exists an isomorphism (bijective additive homomorphism) between: 1. The type of families of additive monoid homomorphisms $F : \alpha \to (M \to^+ N)$, and 2. The type of additive monoid homomorphisms $G : (\alpha \to_{\text{f}} M) \to^+ N$. The isomorphism is given by: - Forward map: $F \mapsto \left( f \mapsto \sum_{x \in \text{supp}(f)} F(x)(f(x)) \right)$ - Inverse map: $G \mapsto \left( x \mapsto G \circ \text{singleAddHom}(x) \right)$ where $\text{singleAddHom}(x) : M \to^+ (\alpha \to_{\text{f}} M)$ is the additive monoid homomorphism sending $m \in M$ to the finitely supported function that is $m$ at $x$ and zero elsewhere.

Finsupp.liftAddHom_apply theorem

 [AddZeroClass M] [AddCommMonoid N] (F : α → M →+ N) (f : α →₀ M) :
  (liftAddHom (α := α) (M := M) (N := N)) F f = f.sum fun x => F x

Full source

@[simp]
theorem liftAddHom_apply [AddZeroClass M] [AddCommMonoid N] (F : α → M →+ N) (f : α →₀ M) :
    (liftAddHom (α := α) (M := M) (N := N)) F f = f.sum fun x => F x :=
  rfl

Evaluation of Lifted Additive Homomorphism on Finitely Supported Functions

Informal description

Let $M$ be an add-zero class and $N$ an additive commutative monoid. For any family of additive monoid homomorphisms $F : \alpha \to (M \to^+ N)$ and any finitely supported function $f : \alpha \to_{\text{f}} M$, the evaluation of the lifted homomorphism $\text{liftAddHom}(F)$ at $f$ is equal to the sum $\sum_{x \in \text{supp}(f)} F(x)(f(x))$.

Finsupp.liftAddHom_symm_apply theorem

 [AddZeroClass M] [AddCommMonoid N] (F : (α →₀ M) →+ N) (x : α) :
  (liftAddHom (α := α) (M := M) (N := N)).symm F x = F.comp (singleAddHom x)

Full source

@[simp]
theorem liftAddHom_symm_apply [AddZeroClass M] [AddCommMonoid N] (F : (α →₀ M) →+ N) (x : α) :
    (liftAddHom (α := α) (M := M) (N := N)).symm F x = F.comp (singleAddHom x) :=
  rfl

Inverse of `liftAddHom` Equivalence via Composition with `singleAddHom`

Informal description

Let $M$ be an add-zero class and $N$ an additive commutative monoid. For any additive monoid homomorphism $F \colon (\alpha \to_{\text{f}} M) \to^+ N$ and any element $x \in \alpha$, the inverse of the `liftAddHom` equivalence evaluated at $F$ and $x$ is equal to the composition of $F$ with the additive monoid homomorphism $\operatorname{singleAddHom}(x) \colon M \to^+ (\alpha \to_{\text{f}} M)$. That is, \[ (\operatorname{liftAddHom})^{-1}(F)(x) = F \circ \operatorname{singleAddHom}(x). \]

Finsupp.liftAddHom_symm_apply_apply theorem

 [AddZeroClass M] [AddCommMonoid N] (F : (α →₀ M) →+ N) (x : α) (y : M) :
  (liftAddHom (α := α) (M := M) (N := N)).symm F x y = F (single x y)

Full source

theorem liftAddHom_symm_apply_apply [AddZeroClass M] [AddCommMonoid N] (F : (α →₀ M) →+ N) (x : α)
    (y : M) : (liftAddHom (α := α) (M := M) (N := N)).symm F x y = F (single x y) :=
  rfl

Inverse Lift Additive Homomorphism Evaluated at Single Element

Informal description

Let $M$ be an add-zero class and $N$ an additive commutative monoid. For any additive monoid homomorphism $F \colon (\alpha \to_{\text{f}} M) \to^+ N$, element $x \in \alpha$, and $y \in M$, the inverse of the lift additive homomorphism satisfies $$ \text{liftAddHom}^{-1}(F)(x)(y) = F(\text{single}(x, y)), $$ where $\text{single}(x, y) \colon \alpha \to_{\text{f}} M$ is the finitely supported function that takes value $y$ at $x$ and zero elsewhere.

Finsupp.liftAddHom_singleAddHom theorem

 [AddCommMonoid M] : (liftAddHom (α := α) (M := M) (N := α →₀ M)) (singleAddHom : α → M →+ α →₀ M) = AddMonoidHom.id _

Full source

@[simp]
theorem liftAddHom_singleAddHom [AddCommMonoid M] :
    (liftAddHom (α := α) (M := M) (N := α →₀ M)) (singleAddHom : α → M →+ α →₀ M) =
      AddMonoidHom.id _ :=
  liftAddHom.toEquiv.apply_eq_iff_eq_symm_apply.2 rfl

Lifting of Single-Point Homomorphisms Yields Identity Homomorphism

Informal description

Let $M$ be an additive commutative monoid. The additive homomorphism obtained by applying the lifting equivalence $\operatorname{liftAddHom}$ to the family of single-point additive homomorphisms $\operatorname{singleAddHom} : \alpha \to (M \to^+ \alpha \to_{\text{f}} M)$ is equal to the identity homomorphism on $\alpha \to_{\text{f}} M$. That is, \[ \operatorname{liftAddHom}(\operatorname{singleAddHom}) = \operatorname{id}. \]

Finsupp.sum_single theorem

[AddCommMonoid M] (f : α →₀ M) : f.sum single = f

Full source

@[simp]
theorem sum_single [AddCommMonoid M] (f : α →₀ M) : f.sum single = f :=
  DFunLike.congr_fun liftAddHom_singleAddHom f

Sum of Single-Point Functions Equals Original Finitely Supported Function

Informal description

Let $M$ be an additive commutative monoid. For any finitely supported function $f \colon \alpha \to_{\text{f}} M$, the sum over the support of $f$ of the single-point functions $\operatorname{single}(a, f(a))$ equals $f$ itself. That is, \[ \sum_{a \in \operatorname{supp}(f)} \operatorname{single}(a, f(a)) = f. \]

Finsupp.univ_sum_single theorem

[Fintype α] [AddCommMonoid M] (f : α →₀ M) : ∑ a : α, single a (f a) = f

Full source

/-- The `Finsupp` version of `Finset.univ_sum_single` -/
@[simp]
theorem univ_sum_single [Fintype α] [AddCommMonoid M] (f : α →₀ M) :
    ∑ a : α, single a (f a) = f := by
  classical
  refine DFunLike.coe_injective ?_
  simp_rw [coe_finset_sum, single_eq_pi_single, Finset.univ_sum_single]

Sum of Single-Point Functions Equals Original Function in Finite Type

Informal description

Let $\alpha$ be a finite type and $M$ an additive commutative monoid. For any finitely supported function $f : \alpha \to_{\text{f}} M$, the sum over all $a \in \alpha$ of the single-point functions $\text{single}_a(f(a))$ equals $f$. That is, \[ \sum_{a \in \alpha} \text{single}_a(f(a)) = f, \] where $\text{single}_a(f(a))$ is the function that takes value $f(a)$ at $a$ and zero elsewhere.

Finsupp.univ_sum_single_apply theorem

[AddCommMonoid M] [Fintype α] (i : α) (m : M) : ∑ j : α, single i m j = m

Full source

@[simp]
theorem univ_sum_single_apply [AddCommMonoid M] [Fintype α] (i : α) (m : M) :
    ∑ j : α, single i m j = m := by
  classical rw [single, coe_mk, Finset.sum_pi_single']
  simp

Sum of Single Finitely Supported Function Evaluations Equals Its Value

Informal description

Let $M$ be an additive commutative monoid and $\alpha$ a finite type. For any element $i \in \alpha$ and $m \in M$, the sum over all $j \in \alpha$ of the finitely supported function $\text{single}_i(m)$ evaluated at $j$ equals $m$. That is, $$\sum_{j \in \alpha} (\text{single}_i(m))(j) = m$$ where $\text{single}_i(m)$ is the function that takes value $m$ at $i$ and $0$ elsewhere.

Finsupp.univ_sum_single_apply' theorem

[AddCommMonoid M] [Fintype α] (i : α) (m : M) : ∑ j : α, single j m i = m

Full source

@[simp]
theorem univ_sum_single_apply' [AddCommMonoid M] [Fintype α] (i : α) (m : M) :
    ∑ j : α, single j m i = m := by
  simp_rw [single, coe_mk]
  classical rw [Finset.sum_pi_single]
  simp

Sum of Single Functions over Finite Type Evaluates to Value

Informal description

Let $M$ be an additive commutative monoid and $\alpha$ a finite type. For any element $i \in \alpha$ and any $m \in M$, the sum over all $j \in \alpha$ of the finitely supported function $\text{single}_j(m)$ evaluated at $i$ equals $m$. In other words, \[ \sum_{j \in \alpha} (\text{single}_j(m))(i) = m. \]

Finsupp.equivFunOnFinite_symm_eq_sum theorem

[Fintype α] [AddCommMonoid M] (f : α → M) : equivFunOnFinite.symm f = ∑ a, Finsupp.single a (f a)

Full source

theorem equivFunOnFinite_symm_eq_sum [Fintype α] [AddCommMonoid M] (f : α → M) :
    equivFunOnFinite.symm f = ∑ a, Finsupp.single a (f a) := by
  rw [← univ_sum_single (equivFunOnFinite.symm f)]
  ext
  simp

Inverse of Finitely Supported Function Equivalence as Sum of Single-Point Functions

Informal description

Let $\alpha$ be a finite type and $M$ an additive commutative monoid. For any function $f \colon \alpha \to M$, the inverse of the equivalence `equivFunOnFinite` applied to $f$ is equal to the sum over all $a \in \alpha$ of the single-point functions $\text{single}_a(f(a))$. That is, \[ \text{equivFunOnFinite}^{-1}(f) = \sum_{a \in \alpha} \text{single}_a(f(a)), \] where $\text{single}_a(f(a))$ is the finitely supported function that takes value $f(a)$ at $a$ and zero elsewhere.

Finsupp.liftAddHom_apply_single theorem

 [AddZeroClass M] [AddCommMonoid N] (f : α → M →+ N) (a : α) (b : M) :
  (liftAddHom (α := α) (M := M) (N := N)) f (single a b) = f a b

Full source

theorem liftAddHom_apply_single [AddZeroClass M] [AddCommMonoid N] (f : α → M →+ N) (a : α)
    (b : M) : (liftAddHom (α := α) (M := M) (N := N)) f (single a b) = f a b :=
  sum_single_index (f a).map_zero

Evaluation of Lifted Additive Homomorphism on Single-Point Function

Informal description

Let $M$ be an add-zero class and $N$ an additive commutative monoid. For any family of additive monoid homomorphisms $f \colon \alpha \to (M \to^+ N)$, any element $a \in \alpha$, and any $b \in M$, the evaluation of the lifted homomorphism $\text{liftAddHom}(f)$ at the single-point function $\text{single}_a(b)$ equals $f(a)(b)$. That is, \[ \text{liftAddHom}(f)(\text{single}_a(b)) = f(a)(b). \]

Finsupp.liftAddHom_comp_single theorem

 [AddZeroClass M] [AddCommMonoid N] (f : α → M →+ N) (a : α) :
  ((liftAddHom (α := α) (M := M) (N := N)) f).comp (singleAddHom a) = f a

Full source

@[simp]
theorem liftAddHom_comp_single [AddZeroClass M] [AddCommMonoid N] (f : α → M →+ N) (a : α) :
    ((liftAddHom (α := α) (M := M) (N := N)) f).comp (singleAddHom a) = f a :=
  AddMonoidHom.ext fun b => liftAddHom_apply_single f a b

Composition of Lifted Homomorphism with Single-Point Homomorphism Equals Original Homomorphism

Informal description

Let $M$ be an add-zero class and $N$ an additive commutative monoid. For any family of additive monoid homomorphisms $f \colon \alpha \to (M \to^+ N)$ and any element $a \in \alpha$, the composition of the lifted homomorphism $\text{liftAddHom}(f)$ with $\text{singleAddHom}(a)$ equals $f(a)$. That is, \[ \text{liftAddHom}(f) \circ \text{singleAddHom}(a) = f(a). \]

Finsupp.comp_liftAddHom theorem

 [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P) (f : α → M →+ N) :
  g.comp ((liftAddHom (α := α) (M := M) (N := N)) f) = (liftAddHom (α := α) (M := M) (N := P)) fun a => g.comp (f a)

Full source

theorem comp_liftAddHom [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P)
    (f : α → M →+ N) :
    g.comp ((liftAddHom (α := α) (M := M) (N := N)) f) =
      (liftAddHom (α := α) (M := M) (N := P)) fun a => g.comp (f a) :=
  liftAddHom.symm_apply_eq.1 <|
    funext fun a => by
      rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]

Composition of Homomorphisms Commutes with Lifting for Finitely Supported Functions

Informal description

Let $M$ be an add-zero class, and $N$, $P$ be additive commutative monoids. For any additive monoid homomorphism $g \colon N \to^+ P$ and any family of additive monoid homomorphisms $f \colon \alpha \to (M \to^+ N)$, the composition of $g$ with the lifted homomorphism $\operatorname{liftAddHom}(f) \colon (\alpha \to_{\text{f}} M) \to^+ N$ is equal to the lifted homomorphism of the family $\lambda a, g \circ f(a) \colon \alpha \to (M \to^+ P)$. That is, \[ g \circ \operatorname{liftAddHom}(f) = \operatorname{liftAddHom}(\lambda a, g \circ f(a)). \]

Finsupp.sum_sub_index theorem

 [AddGroup β] [AddCommGroup γ] {f g : α →₀ β} {h : α → β → γ} (h_sub : ∀ a b₁ b₂, h a (b₁ - b₂) = h a b₁ - h a b₂) :
  (f - g).sum h = f.sum h - g.sum h

Full source

theorem sum_sub_index [AddGroup β] [AddCommGroup γ] {f g : α →₀ β} {h : α → β → γ}
    (h_sub : ∀ a b₁ b₂, h a (b₁ - b₂) = h a b₁ - h a b₂) : (f - g).sum h = f.sum h - g.sum h :=
  ((liftAddHom (α := α) (M := β) (N := γ)) fun a =>
    AddMonoidHom.ofMapSub (h a) (h_sub a)).map_sub f g

Subtraction Commutes with Summation for Finitely Supported Functions

Informal description

Let $\beta$ be an additive group and $\gamma$ an additive commutative group. For any finitely supported functions $f, g \colon \alpha \to \beta$ and any function $h \colon \alpha \to \beta \to \gamma$ satisfying the condition that for all $a \in \alpha$ and $b_1, b_2 \in \beta$, the equality $h(a)(b_1 - b_2) = h(a)(b_1) - h(a)(b_2)$ holds, we have \[ \sum_{a \in \text{supp}(f - g)} h(a)((f - g)(a)) = \left( \sum_{a \in \text{supp}(f)} h(a)(f(a)) \right) - \left( \sum_{a \in \text{supp}(g)} h(a)(g(a)) \right). \]

Finsupp.prod_embDomain theorem

 [Zero M] [CommMonoid N] {v : α →₀ M} {f : α ↪ β} {g : β → M → N} : (v.embDomain f).prod g = v.prod fun a b => g (f a) b

Full source

@[to_additive]
theorem prod_embDomain [Zero M] [CommMonoid N] {v : α →₀ M} {f : α ↪ β} {g : β → M → N} :
    (v.embDomain f).prod g = v.prod fun a b => g (f a) b := by
  rw [prod, prod, support_embDomain, Finset.prod_map]
  simp_rw [embDomain_apply]

Product Equality for Embedded Finitely Supported Functions

Informal description

Let $M$ be a type with a zero element, $N$ a commutative monoid, $v \colon \alpha \to M$ a finitely supported function, $f \colon \alpha \hookrightarrow \beta$ an injective embedding, and $g \colon \beta \to M \to N$ a function. Then the product of $g$ over the support of the embedded function $\text{embDomain}\, f\, v$ equals the product over the support of $v$ of the values $g(f(a))(v(a))$, i.e., \[ \prod_{b \in \text{supp}(\text{embDomain}\, f\, v)} g(b)((\text{embDomain}\, f\, v)(b)) = \prod_{a \in \text{supp}(v)} g(f(a))(v(a)). \]

Finsupp.prod_finset_sum_index theorem

 [AddCommMonoid M] [CommMonoid N] {s : Finset ι} {g : ι → α →₀ M} {h : α → M → N} (h_zero : ∀ a, h a 0 = 1)
  (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) : (∏ i ∈ s, (g i).prod h) = (∑ i ∈ s, g i).prod h

Full source

@[to_additive]
theorem prod_finset_sum_index [AddCommMonoid M] [CommMonoid N] {s : Finset ι} {g : ι → α →₀ M}
    {h : α → M → N} (h_zero : ∀ a, h a 0 = 1) (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
    (∏ i ∈ s, (g i).prod h) = (∑ i ∈ s, g i).prod h :=
  Finset.cons_induction_on s rfl fun a s has ih => by
    rw [prod_cons, ih, sum_cons, prod_add_index' h_zero h_add]

Product of Products Equals Product of Sum for Finitely Supported Functions

Informal description

Let $M$ be an additive commutative monoid and $N$ a commutative monoid. Given a finite set $s$ of indices, a family of finitely supported functions $g_i \colon \alpha \to M$ indexed by $i \in s$, and a function $h \colon \alpha \to M \to N$ such that: 1. For all $a \in \alpha$, $h(a, 0) = 1$ (where $0$ is the zero element of $M$). 2. For all $a \in \alpha$ and $b_1, b_2 \in M$, $h(a, b_1 + b_2) = h(a, b_1) \cdot h(a, b_2)$ (i.e., $h(a, \cdot)$ is multiplicative). Then the product over $s$ of the products of $h$ over the supports of the $g_i$ equals the product of $h$ over the support of the sum of the $g_i$: \[ \prod_{i \in s} \left( \prod_{a \in \text{supp}(g_i)} h(a, g_i(a)) \right) = \prod_{a \in \text{supp}(\sum_{i \in s} g_i)} h\left(a, \left(\sum_{i \in s} g_i\right)(a)\right). \]

Finsupp.prod_sum_index theorem

 [Zero M] [AddCommMonoid N] [CommMonoid P] {f : α →₀ M} {g : α → M → β →₀ N} {h : β → N → P} (h_zero : ∀ a, h a 0 = 1)
  (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) : (f.sum g).prod h = f.prod fun a b => (g a b).prod h

Full source

@[to_additive]
theorem prod_sum_index [Zero M] [AddCommMonoid N] [CommMonoid P] {f : α →₀ M}
    {g : α → M → β →₀ N} {h : β → N → P} (h_zero : ∀ a, h a 0 = 1)
    (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
    (f.sum g).prod h = f.prod fun a b => (g a b).prod h :=
  (prod_finset_sum_index h_zero h_add).symm

Product-Sum Interchange for Finitely Supported Functions

Informal description

Let $M$ be a type with a zero element, $N$ an additive commutative monoid, and $P$ a commutative monoid. Given a finitely supported function $f \colon \alpha \to M$, a family of finitely supported functions $g_a \colon M \to \beta \to N$ for each $a \in \alpha$, and a function $h \colon \beta \to N \to P$ such that: 1. For all $b \in \beta$, $h(b, 0) = 1$ (where $0$ is the zero element of $N$). 2. For all $b \in \beta$ and $n_1, n_2 \in N$, $h(b, n_1 + n_2) = h(b, n_1) \cdot h(b, n_2)$ (i.e., $h(b, \cdot)$ is multiplicative). Then the product of $h$ over the support of the sum $\sum_{a \in \alpha} g_a(f(a))$ equals the product over the support of $f$ of the products of $h$ over the supports of the $g_a(f(a))$: \[ \prod_{b \in \text{supp}(\sum_{a \in \alpha} g_a(f(a)))} h\left(b, \left(\sum_{a \in \alpha} g_a(f(a))\right)(b)\right) = \prod_{a \in \text{supp}(f)} \left( \prod_{b \in \text{supp}(g_a(f(a)))} h(b, g_a(f(a))(b)) \right). \]

Finsupp.multiset_sum_sum_index theorem

 [AddCommMonoid M] [AddCommMonoid N] (f : Multiset (α →₀ M)) (h : α → M → N) (h₀ : ∀ a, h a 0 = 0)
  (h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) : f.sum.sum h = (f.map fun g : α →₀ M => g.sum h).sum

Full source

theorem multiset_sum_sum_index [AddCommMonoid M] [AddCommMonoid N] (f : Multiset (α →₀ M))
    (h : α → M → N) (h₀ : ∀ a, h a 0 = 0)
    (h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) :
    f.sum.sum h = (f.map fun g : α →₀ M => g.sum h).sum :=
  Multiset.induction_on f rfl fun a s ih => by
    rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]

Sum of Sums Equals Sum over Multiset of Finitely Supported Functions

Informal description

Let $M$ and $N$ be additive commutative monoids. Given a multiset $f$ of finitely supported functions from $\alpha$ to $M$, and a function $h \colon \alpha \to M \to N$ such that: 1. $h(a, 0) = 0$ for all $a \in \alpha$, 2. $h(a, b_1 + b_2) = h(a, b_1) + h(a, b_2)$ for all $a \in \alpha$ and $b_1, b_2 \in M$, then the sum of $h$ over the sum of the functions in $f$ equals the sum of the individual sums of $h$ over each function in $f$. That is, \[ \sum_{g \in f} \left( \sum_{a \in \alpha} h(a, g(a)) \right) = \sum_{a \in \alpha} h\left(a, \sum_{g \in f} g(a)\right). \]

Finsupp.support_sum_eq_biUnion theorem

 {α : Type*} {ι : Type*} {M : Type*} [DecidableEq α] [AddCommMonoid M] {g : ι → α →₀ M} (s : Finset ι)
  (h : ∀ i₁ i₂, i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support) :
  (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support

Full source

theorem support_sum_eq_biUnion {α : Type*} {ι : Type*} {M : Type*} [DecidableEq α]
    [AddCommMonoid M] {g : ι → α →₀ M} (s : Finset ι)
    (h : ∀ i₁ i₂, i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support) :
    (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support := by
  classical
  refine Finset.induction_on s ?_ ?_
  · simp
  · intro i s hi
    simp only [hi, sum_insert, not_false_iff, biUnion_insert]
    intro hs
    rw [Finsupp.support_add_eq, hs]
    rw [hs, Finset.disjoint_biUnion_right]
    intro j hj
    exact h _ _ (ne_of_mem_of_not_mem hj hi).symm

Support of Sum of Finitely Supported Functions with Pairwise Disjoint Supports Equals Union of Supports

Informal description

Let $\alpha$ and $\iota$ be types with $\alpha$ having decidable equality, and let $M$ be an additive commutative monoid. Given a family of finitely supported functions $g_i : \alpha \to M$ indexed by $\iota$ and a finite subset $s \subseteq \iota$, if the supports of $g_{i_1}$ and $g_{i_2}$ are disjoint for any distinct $i_1, i_2 \in s$, then the support of the sum $\sum_{i \in s} g_i$ is equal to the union of the supports of the $g_i$ for $i \in s$. That is, \[ \operatorname{supp}\left( \sum_{i \in s} g_i \right) = \bigcup_{i \in s} \operatorname{supp}(g_i). \]

Finsupp.multiset_map_sum theorem

 [Zero M] {f : α →₀ M} {m : β → γ} {h : α → M → Multiset β} : Multiset.map m (f.sum h) = f.sum fun a b => (h a b).map m

Full source

theorem multiset_map_sum [Zero M] {f : α →₀ M} {m : β → γ} {h : α → M → Multiset β} :
    Multiset.map m (f.sum h) = f.sum fun a b => (h a b).map m :=
  map_sum (Multiset.mapAddMonoidHom m) _ f.support

Multiset Image of Finitely Supported Function Sum

Informal description

Let $f : \alpha \to₀ M$ be a finitely supported function, $m : \beta \to \gamma$ a function, and $h : \alpha \to M \to \text{Multiset } \beta$ a family of multisets. Then the image of the multiset sum $\sum_{a \in \alpha} h(a, f(a))$ under $m$ is equal to the sum over $\alpha$ of the images of $h(a, f(a))$ under $m$, i.e., \[ \text{map } m \left( \sum_{a \in \alpha} h(a, f(a)) \right) = \sum_{a \in \alpha} \text{map } m (h(a, f(a))). \]

Finsupp.multiset_sum_sum theorem

 [Zero M] [AddCommMonoid N] {f : α →₀ M} {h : α → M → Multiset N} :
  Multiset.sum (f.sum h) = f.sum fun a b => Multiset.sum (h a b)

Full source

theorem multiset_sum_sum [Zero M] [AddCommMonoid N] {f : α →₀ M} {h : α → M → Multiset N} :
    Multiset.sum (f.sum h) = f.sum fun a b => Multiset.sum (h a b) :=
  map_sum Multiset.sumAddMonoidHom _ f.support

Sum of Multiset Sums Equals Sum of Multiset Elements for Finitely Supported Functions

Informal description

Let $M$ be a type with a zero element and $N$ be an additive commutative monoid. Given a finitely supported function $f : \alpha \to₀ M$ and a family of multisets $h : \alpha \to M \to \text{Multiset } N$, the sum of the multiset obtained by summing $h(a, f(a))$ over all $a \in \alpha$ is equal to the sum over $\alpha$ of the sums of the multisets $h(a, f(a))$. In other words, \[ \sum \left( \sum_{a \in \alpha} h(a, f(a)) \right) = \sum_{a \in \alpha} \sum h(a, f(a)). \]

Finsupp.prod_add_index_of_disjoint theorem

 [AddCommMonoid M] {f1 f2 : α →₀ M} (hd : Disjoint f1.support f2.support) {β : Type*} [CommMonoid β] (g : α → M → β) :
  (f1 + f2).prod g = f1.prod g * f2.prod g

Full source

/-- For disjoint `f1` and `f2`, and function `g`, the product of the products of `g`
over `f1` and `f2` equals the product of `g` over `f1 + f2` -/
@[to_additive
      "For disjoint `f1` and `f2`, and function `g`, the sum of the sums of `g`
      over `f1` and `f2` equals the sum of `g` over `f1 + f2`"]
theorem prod_add_index_of_disjoint [AddCommMonoid M] {f1 f2 : α →₀ M}
    (hd : Disjoint f1.support f2.support) {β : Type*} [CommMonoid β] (g : α → M → β) :
    (f1 + f2).prod g = f1.prod g * f2.prod g := by
  have :
    ∀ {f1 f2 : α →₀ M},
      Disjoint f1.support f2.support → (∏ x ∈ f1.support, g x (f1 x + f2 x)) = f1.prod g :=
    fun hd =>
    Finset.prod_congr rfl fun x hx => by
      simp only [not_mem_support_iff.mp (disjoint_left.mp hd hx), add_zero]
  classical simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd,
      prod_union hd, add_apply]

Product over Sum of Disjointly Supported Functions Equals Product of Products

Informal description

Let $M$ be an additive commutative monoid and $\beta$ a commutative monoid. Given two finitely supported functions $f_1, f_2 \colon \alpha \to M$ with disjoint supports and a function $g \colon \alpha \to M \to \beta$, the product of $g$ over $f_1 + f_2$ equals the product of the products of $g$ over $f_1$ and $f_2$, i.e., \[ \prod_{a \in \alpha} g(a)((f_1 + f_2)(a)) = \left(\prod_{a \in \alpha} g(a)(f_1(a))\right) \cdot \left(\prod_{a \in \alpha} g(a)(f_2(a))\right). \]

Finsupp.prod_dvd_prod_of_subset_of_dvd theorem

 [Zero M] [CommMonoid N] {f1 f2 : α →₀ M} {g1 g2 : α → M → N} (h1 : f1.support ⊆ f2.support)
  (h2 : ∀ a : α, a ∈ f1.support → g1 a (f1 a) ∣ g2 a (f2 a)) : f1.prod g1 ∣ f2.prod g2

Full source

theorem prod_dvd_prod_of_subset_of_dvd [Zero M] [CommMonoid N] {f1 f2 : α →₀ M}
    {g1 g2 : α → M → N} (h1 : f1.support ⊆ f2.support)
    (h2 : ∀ a : α, a ∈ f1.support → g1 a (f1 a) ∣ g2 a (f2 a)) : f1.prod g1 ∣ f2.prod g2 := by
  classical
    simp only [Finsupp.prod, Finsupp.prod_mul]
    rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]
    apply dvd_mul_of_dvd_right
    apply prod_dvd_prod_of_dvd
    exact h2

Divisibility of Products for Finitely Supported Functions with Subset Support Condition: $\prod_{\text{supp}(f_1)} g_1 \mid \prod_{\text{supp}(f_2)} g_2$

Informal description

Let $M$ be a type with a zero element and $N$ a commutative monoid. Given two finitely supported functions $f_1, f_2 \colon \alpha \to M$ such that the support of $f_1$ is contained in the support of $f_2$, and two functions $g_1, g_2 \colon \alpha \to M \to N$ such that for every $a$ in the support of $f_1$, $g_1(a)(f_1(a))$ divides $g_2(a)(f_2(a))$, then the product $\prod_{a \in \text{supp}(f_1)} g_1(a)(f_1(a))$ divides the product $\prod_{a \in \text{supp}(f_2)} g_2(a)(f_2(a))$.

Finsupp.indicator_eq_sum_attach_single theorem

[AddCommMonoid M] {s : Finset α} (f : ∀ a ∈ s, M) : indicator s f = ∑ x ∈ s.attach, single ↑x (f x x.2)

Full source

lemma indicator_eq_sum_attach_single [AddCommMonoid M] {s : Finset α} (f : ∀ a ∈ s, M) :
    indicator s f = ∑ x ∈ 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]

Decomposition of Indicator Function into Single-Point Functions

Informal description

Let $M$ be an additive commutative monoid and $s$ a finite subset of $\alpha$. For any function $f$ defined on $s$ (i.e., for each $a \in s$, $f$ provides a value $f(a) \in M$), the finitely supported indicator function $\text{indicator}(s, f)$ can be expressed as the sum over the attached set $s.\text{attach}$ of single-point functions: \[ \text{indicator}(s, f) = \sum_{x \in s.\text{attach}} \text{single}(x, f(x)). \] Here, $s.\text{attach}$ is the finite set consisting of elements of $s$ paired with their membership proofs, and $\text{single}(x, f(x))$ denotes the finitely supported function that takes the value $f(x)$ at $x$ and zero elsewhere.

Finsupp.indicator_eq_sum_single theorem

[AddCommMonoid M] (s : Finset α) (f : α → M) : indicator s (fun x _ ↦ f x) = ∑ x ∈ s, single x (f x)

Full source

lemma indicator_eq_sum_single [AddCommMonoid M] (s : Finset α) (f : α → M) :
    indicator s (fun x _ ↦ f x) = ∑ x ∈ s, single x (f x) :=
  (indicator_eq_sum_attach_single _).trans <| sum_attach _ fun x ↦ single x (f x)

Decomposition of Indicator Function into Single-Point Functions via Summation

Informal description

Let $M$ be an additive commutative monoid, $s$ a finite subset of $\alpha$, and $f \colon \alpha \to M$ a function. The finitely supported indicator function $\text{indicator}(s, f)$ (which equals $f(x)$ when $x \in s$ and zero otherwise) can be expressed as the sum over $s$ of single-point functions: \[ \text{indicator}(s, f) = \sum_{x \in s} \text{single}(x, f(x)), \] where $\text{single}(x, f(x))$ is the finitely supported function that takes the value $f(x)$ at $x$ and zero elsewhere.

Finsupp.prod_indicator_index_eq_prod_attach theorem

 [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 ∈ s.attach, h ↑x (f x x.2)

Full source

@[to_additive (attr := simp)]
lemma prod_indicator_index_eq_prod_attach [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 ∈ 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]

Product Equality for Indicator Function and Attached Set

Informal description

Let $M$ be a type with a zero element and $N$ a commutative monoid. Given a finite set $s \subseteq \alpha$, a function $f \colon \{a \in \alpha \mid a \in s\} \to M$, and a function $h \colon \alpha \to M \to N$ such that $h(a)(0) = 1$ for all $a \in s$, the product of $h$ over the support of the indicator function $\text{indicator}(s, f)$ equals the product of $h$ over the attached set $s.\text{attach}$ evaluated at $f$, i.e., \[ \prod_{a \in \text{supp}(\text{indicator}(s, f))} h(a)(f(a)) = \prod_{x \in s.\text{attach}} h(x)(f(x)). \]

Finsupp.prod_indicator_index theorem

 [Zero M] [CommMonoid N] {s : Finset α} (f : α → M) {h : α → M → N} (h_zero : ∀ a ∈ s, h a 0 = 1) :
  (indicator s (fun x _ ↦ f x)).prod h = ∏ x ∈ s, h x (f x)

Full source

@[to_additive (attr := simp)]
lemma prod_indicator_index [Zero M] [CommMonoid N]
    {s : Finset α} (f : α → M) {h : α → M → N} (h_zero : ∀ a ∈ s, h a 0 = 1) :
    (indicator s (fun x _ ↦ f x)).prod h = ∏ x ∈ s, h x (f x) :=
  (prod_indicator_index_eq_prod_attach _ h_zero).trans <| prod_attach _ fun x ↦ h x (f x)

Product over Indicator Function Support Equals Product over Finite Set

Informal description

Let $M$ be a type with a zero element and $N$ a commutative monoid. Given a finite set $s \subseteq \alpha$, a function $f \colon \alpha \to M$, and a function $h \colon \alpha \to M \to N$ such that $h(a)(0) = 1$ for all $a \in s$, the product of $h$ over the support of the indicator function $\text{indicator}(s, f)$ equals the product of $h(x)(f(x))$ over $x \in s$, i.e., \[ \prod_{a \in \text{supp}(\text{indicator}(s, f))} h(a)(f(a)) = \prod_{x \in s} h(x)(f(x)). \]

Finsupp.prod_mul_eq_prod_mul_of_exists theorem

 [Zero M] [CommMonoid N] {f : α →₀ M} {g : α → M → N} {n₁ n₂ : N} (a : α) (ha : a ∈ f.support)
  (h : g a (f a) * n₁ = g a (f a) * n₂) : f.prod g * n₁ = f.prod g * n₂

Full source

@[to_additive]
lemma prod_mul_eq_prod_mul_of_exists [Zero M] [CommMonoid N]
    {f : α →₀ M} {g : α → M → N} {n₁ n₂ : N}
    (a : α) (ha : a ∈ f.support)
    (h : g a (f a) * n₁ = g a (f a) * n₂) :
    f.prod g * n₁ = f.prod g * n₂ := by
  classical
  exact Finset.prod_mul_eq_prod_mul_of_exists a ha h

Product Equality under Cancellation for Finitely Supported Functions

Informal description

Let $M$ be a type with a zero element, $N$ a commutative monoid, $f \colon \alpha \to₀ M$ a finitely supported function, and $g \colon \alpha \to M \to N$ a function. For any elements $n_1, n_2 \in N$ and any element $a$ in the support of $f$ such that $g(a)(f(a)) \cdot n_1 = g(a)(f(a)) \cdot n_2$, we have $$\left(\prod_{x \in \text{supp}(f)} g(x)(f(x))\right) \cdot n_1 = \left(\prod_{x \in \text{supp}(f)} g(x)(f(x))\right) \cdot n_2.$$

Finset.sum_apply' theorem

: (∑ k ∈ s, f k) i = ∑ k ∈ s, f k i

Full source

theorem Finset.sum_apply' : (∑ k ∈ s, f k) i = ∑ k ∈ s, f k i :=
  map_sum (Finsupp.applyAddHom i) f s

Evaluation Commutes with Finite Summation of Functions

Informal description

For a finite set $s$ and a family of functions $f_k$ indexed by $k \in s$, the evaluation of the sum $\sum_{k \in s} f_k$ at a point $i$ is equal to the sum of the evaluations $\sum_{k \in s} f_k(i)$.

Finsupp.sum_apply' theorem

: g.sum k x = g.sum fun i b => k i b x

Full source

theorem Finsupp.sum_apply' : g.sum k x = g.sum fun i b => k i b x :=
  Finset.sum_apply _ _ _

Summation over Finitely Supported Function's Support

Informal description

For a finitely supported function $g : \alpha \to₀ M$ and a function $k : \alpha \to M \to \beta$, the sum $\sum_{i \in \text{supp}(g)} k_i (g_i) x$ is equal to $\sum_{i \in \text{supp}(g)} (k_i (g_i) x)$.

Finsupp.sum_apply'' theorem

 {A F : Type*} [AddZeroClass A] [AddCommMonoid F] [FunLike F γ B] (g : ι →₀ A) (k : ι → A → F) (x : γ)
  (hg0 : ∀ (i : ι), k i 0 = 0) (hgadd : ∀ (i : ι) (a₁ a₂ : A), k i (a₁ + a₂) = k i a₁ + k i a₂) (h0 : (0 : F) x = 0)
  (hadd : ∀ (f g : F), (f + g : F) x = f x + g x) : g.sum k x = g.sum (fun i a ↦ k i a x)

Full source

/-- Version of `Finsupp.sum_apply'` that applies in large generality to linear combinations
of functions in any `FunLike` type on which addition is defined pointwise.

At the time of writing Mathlib does not have a typeclass to express the condition
that addition on a `FunLike` type is pointwise; hence this is asserted via explicit hypotheses. -/
theorem Finsupp.sum_apply'' {A F : Type*} [AddZeroClass A] [AddCommMonoid F] [FunLike F γ B]
    (g : ι →₀ A) (k : ι → A → F) (x : γ)
    (hg0 : ∀ (i : ι), k i 0 = 0) (hgadd : ∀ (i : ι) (a₁ a₂ : A), k i (a₁ + a₂) = k i a₁ + k i a₂)
    (h0 : (0 : F) x = 0) (hadd : ∀ (f g : F), (f + g : F) x = f x + g x) :
    g.sum k x = g.sum (fun i a ↦ k i a x) := by
  induction g using Finsupp.induction with
  | zero => simp [h0]
  | single_add i a f hf ha ih =>
    rw [Finsupp.sum_add_index' hg0 hgadd, Finsupp.sum_add_index', hadd, ih]
    · congr 1
      rw [Finsupp.sum_single_index (hg0 i), Finsupp.sum_single_index]
      simp [hg0, h0]
    · simp [hg0, h0]
    · simp [hgadd, hadd]

Evaluation Commutes with Summation of Finitely Supported Linear Combinations

Informal description

Let $A$ and $F$ be types, where $A$ is equipped with an additive zero class structure and $F$ is an additive commutative monoid. Suppose $F$ is a `FunLike` type with elements acting as functions from $\gamma$ to some type $B$. Given a finitely supported function $g \colon \iota \to_{\text{f}} A$, a family of functions $k_i \colon A \to F$ for each $i \in \iota$, and a point $x \in \gamma$, assume the following: 1. Each $k_i$ preserves zero: $k_i(0) = 0$ for all $i \in \iota$. 2. Each $k_i$ is additive: $k_i(a_1 + a_2) = k_i(a_1) + k_i(a_2)$ for all $i \in \iota$ and $a_1, a_2 \in A$. 3. The zero function in $F$ evaluates to zero at $x$: $0(x) = 0$. 4. Evaluation at $x$ is additive: $(f + g)(x) = f(x) + g(x)$ for all $f, g \in F$. Then, the evaluation at $x$ of the sum $\sum_{i \in \text{supp}(g)} k_i(g_i)$ equals the sum $\sum_{i \in \text{supp}(g)} k_i(g_i)(x)$.

Finsupp.sum_sum_index' theorem

 (h0 : ∀ i, t i 0 = 0) (h1 : ∀ i x y, t i (x + y) = t i x + t i y) : (∑ x ∈ s, f x).sum t = ∑ x ∈ s, (f x).sum t

Full source

theorem Finsupp.sum_sum_index' (h0 : ∀ i, t i 0 = 0) (h1 : ∀ i x y, t i (x + y) = t i x + t i y) :
    (∑ x ∈ s, f x).sum t = ∑ x ∈ s, (f x).sum t := by
  classical
  exact Finset.induction_on s rfl fun a s has ih => by
    simp_rw [Finset.sum_insert has, Finsupp.sum_add_index' h0 h1, ih]

Double Summation Equality for Finitely Supported Functions with Additive Weightings

Informal description

Let $M$ be an additive commutative monoid, $s$ a finite set, and $f$ a function assigning to each $x \in s$ a finitely supported function $f(x) : \alpha \to M$. For a family of functions $t_i : M \to N$ indexed by $i \in \alpha$, suppose each $t_i$ satisfies: 1. $t_i(0) = 0$ for all $i$, and 2. $t_i(x + y) = t_i(x) + t_i(y)$ for all $x, y \in M$ (i.e., each $t_i$ is additive). Then we have the equality: \[ \left(\sum_{x \in s} f(x)\right).\text{sum}\, t = \sum_{x \in s} \left(f(x).\text{sum}\, t\right) \] where the left side first sums the $f(x)$ pointwise and then applies the sum with weights $t$, while the right side sums the individual weighted sums of each $f(x)$.

Finsupp.sum_mul theorem

(b : S) (s : α →₀ R) {f : α → R → S} : s.sum f * b = s.sum fun a c => f a c * b

Full source

theorem Finsupp.sum_mul (b : S) (s : α →₀ R) {f : α → R → S} :
    s.sum f * b = s.sum fun a c => f a c * b := by simp only [Finsupp.sum, Finset.sum_mul]

Distributivity of Summation over Multiplication: $\left(\sum f\right) \cdot b = \sum (f \cdot b)$ for Finitely Supported Functions

Informal description

Let $R$ and $S$ be types with appropriate algebraic structures, and let $s : \alpha \to₀ R$ be a finitely supported function from $\alpha$ to $R$. For any $b \in S$ and any function $f : \alpha \to R \to S$, we have \[ \left(\sum_{a \in \alpha} f(a, s(a))\right) \cdot b = \sum_{a \in \alpha} \left(f(a, s(a)) \cdot b\right). \]

Finsupp.mul_sum theorem

(b : S) (s : α →₀ R) {f : α → R → S} : b * s.sum f = s.sum fun a c => b * f a c

Full source

theorem Finsupp.mul_sum (b : S) (s : α →₀ R) {f : α → R → S} :
    b * s.sum f = s.sum fun a c => b * f a c := by simp only [Finsupp.sum, Finset.mul_sum]

Distributivity of scalar multiplication over sum of finitely supported functions

Informal description

Let $S$ be a type with multiplication, $R$ a type, and $s : \alpha \to₀ R$ a finitely supported function. For any $b \in S$ and any function $f : \alpha \to R \to S$, we have: \[ b \cdot \left( \sum_{x \in s} f(x) \right) = \sum_{x \in s} (b \cdot f(x)) \] where the sum is taken over the support of $s$.

Multiset.card_finsuppSum theorem

[Zero M] (f : ι →₀ M) (g : ι → M → Multiset α) : card (f.sum g) = f.sum fun i m ↦ card (g i m)

Full source

@[simp] lemma Multiset.card_finsuppSum [Zero M] (f : ι →₀ M) (g : ι → M → Multiset α) :
    card (f.sum g) = f.sum fun i m ↦ card (g i m) := map_finsuppSum cardHom ..

Cardinality of Multiset Sum Equals Sum of Cardinalities for Finitely Supported Functions

Informal description

Let $M$ be a type with a zero element, $f : \iota \to₀ M$ a finitely supported function, and $g : \iota \to M \to \text{Multiset } \alpha$ a family of functions. Then the cardinality of the multiset sum $\sum_{i \in \iota} g(i, f(i))$ is equal to the sum $\sum_{i \in \iota} |g(i, f(i))|$, where $|\cdot|$ denotes the cardinality of a multiset.

Nat.prod_pow_pos_of_zero_not_mem_support theorem

{f : ℕ →₀ ℕ} (nhf : 0 ∉ f.support) : 0 < f.prod (· ^ ·)

Full source

/-- If `0 : ℕ` is not in the support of `f : ℕ →₀ ℕ` then `0 < ∏ x ∈ f.support, x ^ (f x)`. -/
theorem prod_pow_pos_of_zero_not_mem_support {f : ℕℕ →₀ ℕ} (nhf : 0 ∉ f.support) :
    0 < f.prod (· ^ ·) :=
  Nat.pos_iff_ne_zero.mpr <| Finset.prod_ne_zero_iff.mpr fun _ hf =>
    pow_ne_zero _ fun H => by subst H; exact nhf hf

Positivity of Product of Powers with Zero Not in Support

Informal description

For any finitely supported function $f \colon \mathbb{N} \to \mathbb{N}$ such that $0$ is not in the support of $f$, the product $\prod_{x \in \text{supp}(f)} x^{f(x)}$ is strictly positive.