Mathlib.Algebra.BigOperators.Option

Module docstring

{"# Lemmas about products and sums over finite sets in Option α

In this file we prove formulas for products and sums over Finset.insertNone s and Finset.eraseNone s. "}

Finset.prod_insertNone theorem

(f : Option α → M) (s : Finset α) : ∏ x ∈ insertNone s, f x = f none * ∏ x ∈ s, f (some x)

Full source

@[to_additive (attr := simp)]
theorem prod_insertNone (f : Option α → M) (s : Finset α) :
    ∏ x ∈ insertNone s, f x = f none * ∏ x ∈ s, f (some x) := by simp [insertNone]

Product over $\operatorname{insertNone}(s)$ equals $f(\operatorname{none})$ times product over $s$ of $f(\operatorname{some}(x))$

Informal description

Let $M$ be a commutative monoid, $s$ a finite subset of a type $\alpha$, and $f : \operatorname{Option} \alpha \to M$ a function. Then the product of $f$ over the finite set $\operatorname{insertNone}(s)$ (which is $s$ embedded into $\operatorname{Option} \alpha$ with $\operatorname{none}$ added) satisfies \[ \prod_{x \in \operatorname{insertNone}(s)} f(x) = f(\operatorname{none}) \cdot \prod_{x \in s} f(\operatorname{some}(x)). \]

Finset.mul_prod_eq_prod_insertNone theorem

(f : α → M) (x : M) (s : Finset α) : x * ∏ i ∈ s, f i = ∏ i ∈ insertNone s, i.elim x f

Full source

@[to_additive]
theorem mul_prod_eq_prod_insertNone (f : α → M) (x : M) (s : Finset α) :
    x * ∏ i ∈ s, f i = ∏ i ∈ insertNone s, i.elim x f :=
  (prod_insertNone (fun i => i.elim x f) _).symm

Product over $\operatorname{insertNone}(s)$ as elimination of $\operatorname{none}$ to $x$

Informal description

Let $M$ be a commutative monoid, $s$ a finite subset of a type $\alpha$, $f : \alpha \to M$ a function, and $x \in M$ an element. Then the product of $x$ with the product of $f$ over $s$ equals the product over $\operatorname{insertNone}(s)$ of the function that eliminates $\operatorname{none}$ to $x$ and applies $f$ to $\operatorname{some}(i)$: \[ x \cdot \prod_{i \in s} f(i) = \prod_{i \in \operatorname{insertNone}(s)} \operatorname{Option.elim}(x, f, i). \]

Finset.prod_eraseNone theorem

(f : α → M) (s : Finset (Option α)) : ∏ x ∈ eraseNone s, f x = ∏ x ∈ s, Option.elim' 1 f x

Full source

@[to_additive]
theorem prod_eraseNone (f : α → M) (s : Finset (Option α)) :
    ∏ x ∈ eraseNone s, f x = ∏ x ∈ s, Option.elim' 1 f x := by
  classical calc
      ∏ x ∈ eraseNone s, f x = ∏ x ∈ (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
        (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
      _ = ∏ x ∈ s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
      _ = ∏ x ∈ s, Option.elim' 1 f x := prod_erase _ rfl

Product over $\operatorname{eraseNone}(s)$ equals product over $s$ of $\operatorname{Option.elim}(1, f, x)$

Informal description

Let $M$ be a commutative monoid, $s$ a finite subset of $\operatorname{Option} \alpha$, and $f : \alpha \to M$ a function. Then the product of $f$ over the finite set $\operatorname{eraseNone}(s)$ equals the product over $s$ of the function that eliminates $\operatorname{none}$ to $1$ and applies $f$ to $\operatorname{some}(x)$: \[ \prod_{x \in \operatorname{eraseNone}(s)} f(x) = \prod_{x \in s} \operatorname{Option.elim}(1, f, x). \]