Mathlib.Algebra.BigOperators.WithTop

WithTop.coe_sum theorem

(s : Finset ι) (f : ι → α) : ∑ i ∈ s, f i = ∑ i ∈ s, (f i : WithTop α)

Full source

@[simp, norm_cast] lemma coe_sum (s : Finset ι) (f : ι → α) :
    ∑ i ∈ s, f i = ∑ i ∈ s, (f i : WithTop α) := map_sum addHom f s

Sum Inclusion into Extended Monoid Preserves Value

Informal description

For any finite set $s$ and any function $f$ from an index type $\iota$ to an additive commutative monoid $\alpha$, the sum of $f$ over $s$ in $\alpha$ is equal to the sum of the canonical inclusion of $f$ into $\alpha \cup \{\top\}$ over $s$.

WithTop.sum_eq_top theorem

: ∑ i ∈ s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤

Full source

/-- A sum is infinite iff one term is infinite. -/
@[simp] lemma sum_eq_top : ∑ i ∈ s, f i∑ i ∈ s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤ := by
  induction s using Finset.cons_induction <;> simp [*]

Sum Equals Top if and only if Some Term is Top

Informal description

For a finite set $s$ and a function $f$ mapping elements of $s$ to $\alpha \cup \{\top\}$, the sum $\sum_{i \in s} f(i)$ equals $\top$ if and only if there exists an element $i \in s$ such that $f(i) = \top$.

WithTop.sum_ne_top theorem

: ∑ i ∈ s, f i ≠ ⊤ ↔ ∀ i ∈ s, f i ≠ ⊤

Full source

/-- A sum is finite iff all terms are finite. -/
lemma sum_ne_top : ∑ i ∈ s, f i∑ i ∈ s, f i ≠ ⊤∑ i ∈ s, f i ≠ ⊤ ↔ ∀ i ∈ s, f i ≠ ⊤ := by simp

Sum in $\alpha \cup \{\top\}$ is not top if and only if all terms are not top

Informal description

For any finite set $s$ and function $f$ from $s$ to $\alpha \cup \{\top\}$, the sum $\sum_{i \in s} f(i) \neq \top$ if and only if $f(i) \neq \top$ for all $i \in s$.

WithTop.sum_lt_top theorem

: ∑ i ∈ s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤

Full source

/-- A sum is finite iff all terms are finite. -/
@[simp] lemma sum_lt_top : ∑ i ∈ s, f i∑ i ∈ s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤ := by
  simp [WithTop.lt_top_iff_ne_top]

Sum Strictly Below Top in $\alpha \cup \{\top\}$

Informal description

For any additive commutative monoid $\alpha$ extended with a top element $\top$, a finite set $s$, and a function $f$ from $s$ to $\alpha \cup \{\top\}$, the sum $\sum_{i \in s} f(i)$ is strictly less than $\top$ if and only if $f(i) < \top$ for all $i \in s$.

WithTop.prod_ne_top theorem

(h : ∀ i ∈ s, f i ≠ ⊤) : ∏ i ∈ s, f i ≠ ⊤

Full source

/-- A product of finite terms is finite. -/
lemma prod_ne_top (h : ∀ i ∈ s, f i ≠ ⊤) : ∏ i ∈ s, f i∏ i ∈ s, f i ≠ ⊤ :=
  prod_induction f (· ≠ ⊤) (fun _ _ ↦ mul_ne_top) coe_ne_top h

Finite Product of Non-Top Elements is Non-Top in $\text{WithTop }\alpha$

Informal description

For any finite set $s$ and function $f$ from $s$ to $\text{WithTop }\alpha$, if $f(i) \neq \top$ for all $i \in s$, then the product $\prod_{i \in s} f(i) \neq \top$.

WithTop.prod_lt_top theorem

[LT α] (h : ∀ i ∈ s, f i < ⊤) : ∏ i ∈ s, f i < ⊤

Full source

/-- A product of finite terms is finite. -/
lemma prod_lt_top [LT α] (h : ∀ i ∈ s, f i < ⊤) : ∏ i ∈ s, f i < ⊤ :=
  prod_induction f (· < ⊤) (fun _ _ ↦ mul_lt_top) (coe_lt_top _) h

Finite Product Below Top in $\text{WithTop }\alpha$

Informal description

For any type $\alpha$ with a strict order relation $<$, and for any finite set $s$ and function $f$ from $s$ to $\text{WithTop }\alpha$, if $f(i) < \top$ for all $i \in s$, then the product $\prod_{i \in s} f(i) < \top$.

WithBot.coe_sum theorem

(s : Finset ι) (f : ι → α) : ∑ i ∈ s, f i = ∑ i ∈ s, (f i : WithBot α)

Full source

@[simp, norm_cast] lemma coe_sum (s : Finset ι) (f : ι → α) :
    ∑ i ∈ s, f i = ∑ i ∈ s, (f i : WithBot α) := map_sum addHom f s

Sum Preservation Under Canonical Embedding into $\alpha \cup \{\bot\}$

Informal description

For any finite set $s$ and function $f$ from $s$ to an additive commutative monoid $\alpha$, the sum $\sum_{i \in s} f(i)$ in $\alpha$ is equal to the sum $\sum_{i \in s} (f(i) : \alpha \cup \{\bot\})$ in $\alpha \cup \{\bot\}$, where the embedding of $\alpha$ into $\alpha \cup \{\bot\}$ is via the canonical inclusion map.

WithBot.sum_eq_bot_iff theorem

: ∑ i ∈ s, f i = ⊥ ↔ ∃ i ∈ s, f i = ⊥

Full source

/-- A sum is infinite iff one term is infinite. -/
lemma sum_eq_bot_iff : ∑ i ∈ s, f i∑ i ∈ s, f i = ⊥ ↔ ∃ i ∈ s, f i = ⊥ := by
  induction s using Finset.cons_induction <;> simp [*]

Sum Equals Bottom if and only if Some Term is Bottom in $\text{WithBot } α$

Informal description

Let $α$ be an additive commutative monoid extended with a bottom element $\bot$, and let $s$ be a finite set. For a function $f$ mapping elements of $s$ to $\text{WithBot } α$, the sum $\sum_{i \in s} f(i)$ equals $\bot$ if and only if there exists an element $i \in s$ such that $f(i) = \bot$.

WithBot.bot_lt_sum_iff theorem

: ⊥ < ∑ i ∈ s, f i ↔ ∀ i ∈ s, ⊥ < f i

Full source

/-- A sum is finite iff all terms are finite. -/
lemma bot_lt_sum_iff : ⊥⊥ < ∑ i ∈ s, f i ↔ ∀ i ∈ s, ⊥ < f i := by
  simp only [WithBot.bot_lt_iff_ne_bot, ne_eq, sum_eq_bot_iff, not_exists, not_and]

Sum in $\alpha \cup \{\bot\}$ is greater than bottom iff all terms are greater than bottom

Informal description

For a finite set $s$ and a function $f$ mapping elements of $s$ to $\alpha \cup \{\bot\}$, the sum $\sum_{i \in s} f(i)$ is strictly greater than the bottom element $\bot$ if and only if every term $f(i)$ in the sum is strictly greater than $\bot$.

WithBot.sum_lt_bot theorem

(h : ∀ i ∈ s, f i ≠ ⊥) : ⊥ < ∑ i ∈ s, f i

Full source

/-- A sum of finite terms is finite. -/
lemma sum_lt_bot (h : ∀ i ∈ s, f i ≠ ⊥) : ⊥ < ∑ i ∈ s, f i :=
  bot_lt_sum_iff.2 fun i hi ↦ WithBot.bot_lt_iff_ne_bot.2 (h i hi)

Sum of Non-Bottom Elements in $\alpha \cup \{\bot\}$ is Above Bottom

Informal description

For any finite set $s$ and function $f$ such that $f(i) \neq \bot$ for all $i \in s$, the sum $\sum_{i \in s} f(i)$ is strictly greater than the bottom element $\bot$.

WithBot.prod_ne_bot theorem

(h : ∀ i ∈ s, f i ≠ ⊥) : ∏ i ∈ s, f i ≠ ⊥

Full source

/-- A product of finite terms is finite. -/
lemma prod_ne_bot (h : ∀ i ∈ s, f i ≠ ⊥) : ∏ i ∈ s, f i∏ i ∈ s, f i ≠ ⊥ :=
  prod_induction f (· ≠ ⊥) (fun _ _ ↦ mul_ne_bot) coe_ne_bot h

Finite Product of Non-Bottom Elements is Non-Bottom in `WithBot`

Informal description

For any finite set $s$ and function $f$ such that $f(i) \neq \bot$ for all $i \in s$, the product $\prod_{i \in s} f(i)$ is not equal to $\bot$.

WithBot.bot_lt_prod theorem

[LT α] (h : ∀ i ∈ s, ⊥ < f i) : ⊥ < ∏ i ∈ s, f i

Full source

/-- A product of finite terms is finite. -/
lemma bot_lt_prod [LT α] (h : ∀ i ∈ s, ⊥ < f i) : ⊥ < ∏ i ∈ s, f i :=
  prod_induction f (⊥ < ·) (fun _ _ ↦ bot_lt_mul) (bot_lt_coe _) h

Product of Elements Above Bottom in $\text{WithBot }\alpha$ is Above Bottom

Informal description

Let $\alpha$ be a type equipped with a strict order relation $<$, and let $s$ be a finite subset of some index type. For a function $f$ mapping elements of $s$ to $\text{WithBot }\alpha$, if $\bot < f(i)$ for every $i \in s$, then the product $\prod_{i \in s} f(i)$ is also strictly greater than $\bot$.