Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Finset.prod_sigma theorem

 {σ : α → Type*} (s : Finset α) (t : ∀ a, Finset (σ a)) (f : Sigma σ → β) :
  ∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩

Full source

/-- The product over a sigma type equals the product of the fiberwise products.
For rewriting in the reverse direction, use `Finset.prod_sigma'`.

See also `Fintype.prod_sigma` for the product over the whole type. -/
@[to_additive "The sum over a sigma type equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use `Finset.sum_sigma'`.

See also `Fintype.sum_sigma` for the sum over the whole type."]
theorem prod_sigma {σ : α → Type*} (s : Finset α) (t : ∀ a, Finset (σ a)) (f : Sigma σ → β) :
    ∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩ := by
  simp_rw [← disjiUnion_map_sigma_mk, prod_disjiUnion, prod_map, Function.Embedding.sigmaMk_apply]

Product over Dependent Sum Equals Iterated Product: $\prod_{\Sigma a, t(a)} f = \prod_{a \in s} \prod_{s' \in t(a)} f(a, s')$

Informal description

Let $\alpha$ be a type, $\sigma \colon \alpha \to \text{Type}^*$ a family of types, $s$ a finite subset of $\alpha$, and for each $a \in s$, let $t(a)$ be a finite subset of $\sigma(a)$. Given a commutative monoid $\beta$ and a function $f \colon \Sigma a, \sigma(a) \to \beta$, the product of $f$ over the dependent sum $s.\text{sigma}\, t$ equals the iterated product over $s$ of the products of $f$ over each $t(a)$. That is, \[ \prod_{x \in s.\text{sigma}\, t} f(x) = \prod_{a \in s} \prod_{s' \in t(a)} f(\langle a, s' \rangle). \]

Finset.prod_sigma' theorem

 {σ : α → Type*} (s : Finset α) (t : ∀ a, Finset (σ a)) (f : ∀ a, σ a → β) :
  (∏ a ∈ s, ∏ s ∈ t a, f a s) = ∏ x ∈ s.sigma t, f x.1 x.2

Full source

/-- The product over a sigma type equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Finset.prod_sigma`. -/
@[to_additive "The sum over a sigma type equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use `Finset.sum_sigma`"]
theorem prod_sigma' {σ : α → Type*} (s : Finset α) (t : ∀ a, Finset (σ a)) (f : ∀ a, σ a → β) :
    (∏ a ∈ s, ∏ s ∈ t a, f a s) = ∏ x ∈ s.sigma t, f x.1 x.2 :=
  Eq.symm <| prod_sigma s t fun x => f x.1 x.2

Iterated Product Equals Product over Dependent Sum: $\prod_{a \in s} \prod_{s' \in t(a)} f(a)(s') = \prod_{x \in \Sigma a, t(a)} f(x.1)(x.2)$

Informal description

Let $\alpha$ be a type, $\sigma \colon \alpha \to \text{Type}^*$ a family of types, $s$ a finite subset of $\alpha$, and for each $a \in s$, let $t(a)$ be a finite subset of $\sigma(a)$. Given a commutative monoid $\beta$ and a function $f \colon \alpha \to \sigma(a) \to \beta$, the iterated product over $s$ of the products of $f(a)(s')$ over each $t(a)$ equals the product of $f(x.1)(x.2)$ over the dependent sum $s.\text{sigma}\, t$. That is, \[ \prod_{a \in s} \prod_{s' \in t(a)} f(a)(s') = \prod_{x \in s.\text{sigma}\, t} f(x.1)(x.2). \]

Finset.prod_finset_product theorem

 (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ p : γ × α, p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1)
  {f : γ × α → β} : ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a)

Full source

@[to_additive]
theorem prod_finset_product (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α)
    (h : ∀ p : γ × α, p ∈ rp ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ × α → β} :
    ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a) := by
  refine Eq.trans ?_ (prod_sigma s t fun p => f (p.1, p.2))
  apply prod_equiv (Equiv.sigmaEquivProd _ _).symm <;> simp [h]

Product over Cartesian Product Equals Iterated Product: $\prod_{r} f = \prod_{s} \prod_{t(c)} f(c, a)$

Informal description

Let $r$ be a finite subset of $\gamma \times \alpha$, $s$ a finite subset of $\gamma$, and $t \colon \gamma \to \text{Finset}(\alpha)$ a family of finite subsets of $\alpha$ indexed by $\gamma$. Suppose that for any pair $p = (c, a) \in \gamma \times \alpha$, $p \in r$ if and only if $c \in s$ and $a \in t(c)$. Then, for any function $f \colon \gamma \times \alpha \to \beta$ where $\beta$ is a commutative monoid, we have: \[ \prod_{p \in r} f(p) = \prod_{c \in s} \prod_{a \in t(c)} f(c, a). \]

Finset.prod_finset_product' theorem

 (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ p : γ × α, p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1)
  {f : γ → α → β} : ∏ p ∈ r, f p.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f c a

Full source

@[to_additive]
theorem prod_finset_product' (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α)
    (h : ∀ p : γ × α, p ∈ rp ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ → α → β} :
    ∏ p ∈ r, f p.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f c a :=
  prod_finset_product r s t h

Product Equality for Finite Cartesian Product: $\prod_{r} f = \prod_{s} \prod_{t(c)} f(c, a)$

Informal description

Let $r$ be a finite subset of $\gamma \times \alpha$, $s$ a finite subset of $\gamma$, and for each $c \in \gamma$, let $t(c)$ be a finite subset of $\alpha$. Suppose that for any pair $p = (c, a) \in \gamma \times \alpha$, $p \in r$ if and only if $c \in s$ and $a \in t(c)$. Then, for any function $f \colon \gamma \times \alpha \to \beta$ where $\beta$ is a commutative monoid, the following equality holds: \[ \prod_{(c, a) \in r} f(c, a) = \prod_{c \in s} \prod_{a \in t(c)} f(c, a). \]

Finset.prod_finset_product_right theorem

 (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ p : α × γ, p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2)
  {f : α × γ → β} : ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c)

Full source

@[to_additive]
theorem prod_finset_product_right (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α)
    (h : ∀ p : α × γ, p ∈ rp ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α × γ → β} :
    ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c) := by
  refine Eq.trans ?_ (prod_sigma s t fun p => f (p.2, p.1))
  apply prod_equiv ((Equiv.prodComm _ _).trans (Equiv.sigmaEquivProd _ _).symm) <;> simp [h]

Product Equality for Right-Factorized Finite Sets: $\prod_{r} f = \prod_{s} \prod_{t(c)} f(a, c)$

Informal description

Let $r$ be a finite subset of $\alpha \times \gamma$, $s$ a finite subset of $\gamma$, and for each $c \in \gamma$, let $t(c)$ be a finite subset of $\alpha$. Suppose that for any pair $p = (a, c) \in \alpha \times \gamma$, $p \in r$ if and only if $c \in s$ and $a \in t(c)$. Then, for any function $f \colon \alpha \times \gamma \to \beta$ where $\beta$ is a commutative monoid, the following equality holds: \[ \prod_{p \in r} f(p) = \prod_{c \in s} \prod_{a \in t(c)} f(a, c). \]

Finset.prod_finset_product_right' theorem

 (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ p : α × γ, p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2)
  {f : α → γ → β} : ∏ p ∈ r, f p.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f a c

Full source

@[to_additive]
theorem prod_finset_product_right' (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α)
    (h : ∀ p : α × γ, p ∈ rp ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α → γ → β} :
    ∏ p ∈ r, f p.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f a c :=
  prod_finset_product_right r s t h

Product Equality for Right-Factorized Finite Sets with Curried Function: $\prod_{r} f(a, c) = \prod_{s} \prod_{t(c)} f(a, c)$

Informal description

Let $r$ be a finite subset of $\alpha \times \gamma$, $s$ a finite subset of $\gamma$, and for each $c \in \gamma$, let $t(c)$ be a finite subset of $\alpha$. Suppose that for any pair $p = (a, c) \in \alpha \times \gamma$, $p \in r$ if and only if $c \in s$ and $a \in t(c)$. Then, for any function $f \colon \alpha \to \gamma \to \beta$ where $\beta$ is a commutative monoid, the following equality holds: \[ \prod_{(a, c) \in r} f(a, c) = \prod_{c \in s} \prod_{a \in t(c)} f(a, c). \]

Finset.prod_product theorem

(s : Finset γ) (t : Finset α) (f : γ × α → β) : ∏ x ∈ s ×ˢ t, f x = ∏ x ∈ s, ∏ y ∈ t, f (x, y)

Full source

/-- The product over a product set equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Finset.prod_product'`. -/
@[to_additive "The sum over a product set equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use `Finset.sum_product'`"]
theorem prod_product (s : Finset γ) (t : Finset α) (f : γ × α → β) :
    ∏ x ∈ s ×ˢ t, f x = ∏ x ∈ s, ∏ y ∈ t, f (x, y) :=
  prod_finset_product (s ×ˢ t) s (fun _a => t) fun _p => mem_product

Product over Cartesian Product Equals Iterated Product: $\prod_{s \times t} f = \prod_s \prod_t f$

Informal description

Let $s$ be a finite subset of $\gamma$, $t$ a finite subset of $\alpha$, and $f \colon \gamma \times \alpha \to \beta$ a function where $\beta$ is a commutative monoid. Then the product of $f$ over the Cartesian product $s \times t$ equals the iterated product over $s$ and $t$: \[ \prod_{(x,y) \in s \times t} f(x,y) = \prod_{x \in s} \prod_{y \in t} f(x,y). \]

Finset.prod_product' theorem

 (s : Finset γ) (t : Finset α) (f : γ → α → β) : ∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ x ∈ s, ∏ y ∈ t, f x y

Full source

/-- The product over a product set equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Finset.prod_product`. -/
@[to_additive "The sum over a product set equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use `Finset.sum_product`"]
theorem prod_product' (s : Finset γ) (t : Finset α) (f : γ → α → β) :
    ∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ x ∈ s, ∏ y ∈ t, f x y :=
  prod_product ..

Product over Cartesian Product Equals Iterated Product: $\prod_{s \times t} f = \prod_s \prod_t f$

Informal description

Let $s$ be a finite subset of $\gamma$, $t$ a finite subset of $\alpha$, and $f \colon \gamma \times \alpha \to \beta$ a function where $\beta$ is a commutative monoid. Then the product of $f$ over the Cartesian product $s \times t$ equals the iterated product over $s$ and $t$: \[ \prod_{(x,y) \in s \times t} f(x,y) = \prod_{x \in s} \prod_{y \in t} f(x,y). \]

Finset.prod_product_right theorem

(s : Finset γ) (t : Finset α) (f : γ × α → β) : ∏ x ∈ s ×ˢ t, f x = ∏ y ∈ t, ∏ x ∈ s, f (x, y)

Full source

@[to_additive]
theorem prod_product_right (s : Finset γ) (t : Finset α) (f : γ × α → β) :
    ∏ x ∈ s ×ˢ t, f x = ∏ y ∈ t, ∏ x ∈ s, f (x, y) :=
  prod_finset_product_right (s ×ˢ t) t (fun _a => s) fun _p => mem_product.trans and_comm

Product over Cartesian Product Equals Iterated Product in Reverse Order

Informal description

Let $s$ be a finite subset of $\gamma$, $t$ a finite subset of $\alpha$, and $f \colon \gamma \times \alpha \to \beta$ a function where $\beta$ is a commutative monoid. Then the product of $f$ over the Cartesian product $s \times t$ can be expressed as: \[ \prod_{(x,y) \in s \times t} f(x,y) = \prod_{y \in t} \prod_{x \in s} f(x,y). \]

Finset.prod_product_right' theorem

 (s : Finset γ) (t : Finset α) (f : γ → α → β) : ∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ y ∈ t, ∏ x ∈ s, f x y

Full source

/-- An uncurried version of `Finset.prod_product_right`. -/
@[to_additive "An uncurried version of `Finset.sum_product_right`"]
theorem prod_product_right' (s : Finset γ) (t : Finset α) (f : γ → α → β) :
    ∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ y ∈ t, ∏ x ∈ s, f x y :=
  prod_product_right ..

Product over Cartesian Product Equals Iterated Product in Reverse Order (Uncurried Version)

Informal description

Let $s$ be a finite subset of $\gamma$, $t$ a finite subset of $\alpha$, and $f \colon \gamma \times \alpha \to \beta$ a function where $\beta$ is a commutative monoid. Then the product of $f$ over the Cartesian product $s \times t$ can be expressed as: \[ \prod_{(x,y) \in s \times t} f(x,y) = \prod_{y \in t} \prod_{x \in s} f(x,y). \]

Finset.prod_comm' theorem

 {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ} (h : ∀ x y, x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t')
  {f : γ → α → β} : (∏ x ∈ s, ∏ y ∈ t x, f x y) = ∏ y ∈ t', ∏ x ∈ s' y, f x y

Full source

/-- Generalization of `Finset.prod_comm` to the case when the inner `Finset`s depend on the outer
variable. -/
@[to_additive "Generalization of `Finset.sum_comm` to the case when the inner `Finset`s depend on
the outer variable."]
theorem prod_comm' {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ}
    (h : ∀ x y, x ∈ sx ∈ s ∧ y ∈ t xx ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') {f : γ → α → β} :
    (∏ x ∈ s, ∏ y ∈ t x, f x y) = ∏ y ∈ t', ∏ x ∈ s' y, f x y := by
  classical
    have : ∀ z : γ × α, (z ∈ s.biUnion fun x => (t x).map <| Function.Embedding.sectR x _) ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1 := by
      rintro ⟨x, y⟩
      simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq,
        exists_eq_right, ← and_assoc]
    exact
      (prod_finset_product' _ _ _ this).symm.trans
        ((prod_finset_product_right' _ _ _) fun ⟨x, y⟩ => (this _).trans ((h x y).trans and_comm))

Commutativity of Iterated Products over Dependent Finite Sets: $\prod_{s} \prod_{t(x)} f(x,y) = \prod_{t'} \prod_{s'(y)} f(x,y)$

Informal description

Let $s$ be a finite subset of $\gamma$, and for each $x \in \gamma$, let $t(x)$ be a finite subset of $\alpha$. Let $t'$ be a finite subset of $\alpha$, and for each $y \in \alpha$, let $s'(y)$ be a finite subset of $\gamma$. Suppose that for any $x \in \gamma$ and $y \in \alpha$, we have $x \in s$ and $y \in t(x)$ if and only if $x \in s'(y)$ and $y \in t'$. Then, for any function $f \colon \gamma \times \alpha \to \beta$ where $\beta$ is a commutative monoid, the following equality holds: \[ \prod_{x \in s} \prod_{y \in t(x)} f(x, y) = \prod_{y \in t'} \prod_{x \in s'(y)} f(x, y). \]

Finset.prod_comm theorem

 {s : Finset γ} {t : Finset α} {f : γ → α → β} : (∏ x ∈ s, ∏ y ∈ t, f x y) = ∏ y ∈ t, ∏ x ∈ s, f x y

Full source

@[to_additive]
theorem prod_comm {s : Finset γ} {t : Finset α} {f : γ → α → β} :
    (∏ x ∈ s, ∏ y ∈ t, f x y) = ∏ y ∈ t, ∏ x ∈ s, f x y :=
  prod_comm' fun _ _ => Iff.rfl

Commutativity of Iterated Products over Finite Sets: $\prod_{s} \prod_{t} f(x,y) = \prod_{t} \prod_{s} f(x,y)$

Informal description

Let $s$ be a finite subset of $\gamma$, $t$ a finite subset of $\alpha$, and $f \colon \gamma \times \alpha \to \beta$ a function where $\beta$ is a commutative monoid. Then the iterated products satisfy: \[ \prod_{x \in s} \prod_{y \in t} f(x, y) = \prod_{y \in t} \prod_{x \in s} f(x, y). \]

Finset.prod_comm_cycle theorem

 {s : Finset γ} {t : Finset α} {u : Finset κ} {f : γ → α → κ → β} :
  (∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z) = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z

Full source

/-- Cyclically permute 3 nested instances of `Finset.prod`. -/
@[to_additive]
theorem prod_comm_cycle {s : Finset γ} {t : Finset α} {u : Finset κ} {f : γ → α → κ → β} :
    (∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z) = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z := by
  simp_rw [prod_comm (s := t), prod_comm (s := s)]

Cyclic Permutation of Triple Iterated Products over Finite Sets: $\prod_{s} \prod_{t} \prod_{u} f(x,y,z) = \prod_{u} \prod_{s} \prod_{t} f(x,y,z)$

Informal description

Let $s$, $t$, and $u$ be finite subsets of types $\gamma$, $\alpha$, and $\kappa$ respectively, and let $f \colon \gamma \times \alpha \times \kappa \to \beta$ be a function where $\beta$ is a commutative monoid. Then the iterated products satisfy: \[ \prod_{x \in s} \prod_{y \in t} \prod_{z \in u} f(x, y, z) = \prod_{z \in u} \prod_{x \in s} \prod_{y \in t} f(x, y, z). \]

Finset.card_sigma theorem

{σ : α → Type*} (s : Finset α) (t : ∀ a, Finset (σ a)) : #(s.sigma t) = ∑ a ∈ s, #(t a)

Full source

@[simp]
theorem card_sigma {σ : α → Type*} (s : Finset α) (t : ∀ a, Finset (σ a)) :
    #(s.sigma t) = ∑ a ∈ s, #(t a) :=
  Multiset.card_sigma _ _

Cardinality of Dependent Sum of Finite Sets Equals Sum of Cardinalities

Informal description

For any finite set $s$ indexed by type $\alpha$ and any family of finite sets $t(a)$ indexed by $\sigma(a)$ for each $a \in \alpha$, the cardinality of the dependent sum $\Sigma(s, t)$ is equal to the sum of the cardinalities of the sets $t(a)$ for each $a \in s$. In symbols: \[ |\Sigma(s, t)| = \sum_{a \in s} |t(a)| \]