Mathlib.Data.ENNReal.BigOperators

ENNReal.coe_finset_sum theorem

{s : Finset α} {f : α → ℝ≥0} : ↑(∑ a ∈ s, f a) = ∑ a ∈ s, (f a : ℝ≥0∞)

Full source

@[simp, norm_cast]
theorem coe_finset_sum {s : Finset α} {f : α → ℝ≥0} : ↑(∑ a ∈ s, f a) = ∑ a ∈ s, (f a : ℝ≥0∞) :=
  map_sum ofNNRealHom f s

Canonical Extension of Finite Sum to Extended Non-Negative Reals

Informal description

For any finite set $s$ and any function $f$ from $α$ to the non-negative real numbers $\mathbb{R}_{\geq 0}$, the canonical extension of the sum $\sum_{a \in s} f(a)$ to the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the sum of the canonical extensions of each $f(a)$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$. In symbols: $$ \left(\sum_{a \in s} f(a)\right)_{\mathbb{R}_{\geq 0} \cup \{\infty\}} = \sum_{a \in s} (f(a))_{\mathbb{R}_{\geq 0} \cup \{\infty\}} $$

ENNReal.coe_finset_prod theorem

{s : Finset α} {f : α → ℝ≥0} : ↑(∏ a ∈ s, f a) = ∏ a ∈ s, (f a : ℝ≥0∞)

Full source

@[simp, norm_cast]
theorem coe_finset_prod {s : Finset α} {f : α → ℝ≥0} : ↑(∏ a ∈ s, f a) = ∏ a ∈ s, (f a : ℝ≥0∞) :=
  map_prod ofNNRealHom f s

Canonical Extension of Finite Product to Extended Non-Negative Reals

Informal description

For any finite set $s$ and any function $f$ from $\alpha$ to the non-negative real numbers $\mathbb{R}_{\geq 0}$, the canonical extension of the product $\prod_{a \in s} f(a)$ to the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the product of the canonical extensions of each $f(a)$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$. In symbols: $$ \left(\prod_{a \in s} f(a)\right)_{\mathbb{R}_{\geq 0} \cup \{\infty\}} = \prod_{a \in s} (f(a))_{\mathbb{R}_{\geq 0} \cup \{\infty\}} $$

ENNReal.toNNReal_prod theorem

{ι : Type*} {s : Finset ι} {f : ι → ℝ≥0∞} : (∏ i ∈ s, f i).toNNReal = ∏ i ∈ s, (f i).toNNReal

Full source

@[simp]
theorem toNNReal_prod {ι : Type*} {s : Finset ι} {f : ι → ℝ≥0∞} :
    (∏ i ∈ s, f i).toNNReal = ∏ i ∈ s, (f i).toNNReal :=
  map_prod toNNRealHom _ _

Non-Negative Real Part of Product Equals Product of Non-Negative Real Parts

Informal description

For any finite set $s$ and any function $f$ from $\iota$ to the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the non-negative real part of the product $\prod_{i \in s} f(i)$ is equal to the product of the non-negative real parts of each $f(i)$. In symbols: $$ \left(\prod_{i \in s} f(i)\right)_{\mathbb{R}_{\geq 0}} = \prod_{i \in s} (f(i))_{\mathbb{R}_{\geq 0}} $$

ENNReal.toReal_prod theorem

{ι : Type*} {s : Finset ι} {f : ι → ℝ≥0∞} : (∏ i ∈ s, f i).toReal = ∏ i ∈ s, (f i).toReal

Full source

@[simp]
theorem toReal_prod {ι : Type*} {s : Finset ι} {f : ι → ℝ≥0∞} :
    (∏ i ∈ s, f i).toReal = ∏ i ∈ s, (f i).toReal :=
  map_prod toRealHom _ _

Real Part of Product Equals Product of Real Parts in Extended Non-Negative Reals

Informal description

For any finite set $s$ and any function $f$ from $\iota$ to the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the real part of the product $\prod_{i \in s} f(i)$ is equal to the product of the real parts of each $f(i)$. In symbols: $$ \left(\prod_{i \in s} f(i)\right)_{\mathbb{R}} = \prod_{i \in s} (f(i))_{\mathbb{R}} $$

ENNReal.ofReal_prod_of_nonneg theorem

 {α : Type*} {s : Finset α} {f : α → ℝ} (hf : ∀ i, i ∈ s → 0 ≤ f i) :
  ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i)

Full source

theorem ofReal_prod_of_nonneg {α : Type*} {s : Finset α} {f : α → ℝ} (hf : ∀ i, i ∈ s → 0 ≤ f i) :
    ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i) := by
  simp_rw [ENNReal.ofReal, ← coe_finset_prod, coe_inj]
  exact Real.toNNReal_prod_of_nonneg hf

Product of Non-Negative Reals Preserved Under `ofReal`

Informal description

For any finite set $s$ and any function $f \colon \alpha \to \mathbb{R}$ such that $f(i) \geq 0$ for all $i \in s$, the extended non-negative real number obtained by applying the `ofReal` function to the product of $f$ over $s$ is equal to the product over $s$ of the `ofReal` function applied to each $f(i)$. That is, \[ \text{ofReal}\left(\prod_{i \in s} f(i)\right) = \prod_{i \in s} \text{ofReal}(f(i)). \]

ENNReal.iInf_sum theorem

 {ι α : Type*} {f : ι → α → ℝ≥0∞} {s : Finset α} [Nonempty ι]
  (h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a) :
  ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a

Full source

theorem iInf_sum {ι α : Type*} {f : ι → α → ℝ≥0∞} {s : Finset α} [Nonempty ι]
    (h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a) :
    ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a := by
  induction' s using Finset.cons_induction_on with a s ha ih
  · simp only [Finset.sum_empty, ciInf_const]
  · simp only [Finset.sum_cons, ← ih]
    refine (iInf_add_iInf fun i j => ?_).symm
    refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
    rw [Finset.forall_mem_cons] at hk
    exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)

Infimum-Sum Exchange in Extended Non-Negative Reals under Pairwise Dominance Condition

Informal description

Let $\iota$ and $\alpha$ be types, with $\iota$ nonempty. Given a family of functions $f_i : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ indexed by $i \in \iota$, and a finite set $s \subset \alpha$, suppose that for any finite subset $t \subset s$ and any indices $i, j \in \iota$, there exists $k \in \iota$ such that for all $a \in t$, $f_k(a) \leq f_i(a)$ and $f_k(a) \leq f_j(a)$. Then: \[ \bigsqcap_{i \in \iota} \sum_{a \in s} f_i(a) = \sum_{a \in s} \bigsqcap_{i \in \iota} f_i(a). \]

ENNReal.prod_ne_top theorem

(h : ∀ a ∈ s, f a ≠ ∞) : ∏ a ∈ s, f a ≠ ∞

Full source

/-- A product of finite numbers is still finite. -/
lemma prod_ne_top (h : ∀ a ∈ s, f a ≠ ∞) : ∏ a ∈ s, f a∏ a ∈ s, f a ≠ ∞ := WithTop.prod_ne_top h

Finite Product of Finite Extended Non-Negative Reals is Finite

Informal description

For any finite set $s$ and any function $f$ from $s$ to the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, if $f(a) \neq \infty$ for all $a \in s$, then the product $\prod_{a \in s} f(a)$ is also finite (i.e., not equal to $\infty$).

ENNReal.prod_lt_top theorem

(h : ∀ a ∈ s, f a < ∞) : ∏ a ∈ s, f a < ∞

Full source

/-- A product of finite numbers is still finite. -/
lemma prod_lt_top (h : ∀ a ∈ s, f a < ∞) : ∏ a ∈ s, f a < ∞ := WithTop.prod_lt_top h

Finite Product of Finite Extended Non-Negative Reals is Finite

Informal description

For any finite set $s$ and any function $f$ from $s$ to the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, if $f(a) < \infty$ for every $a \in s$, then the product $\prod_{a \in s} f(a)$ is finite (i.e., strictly less than $\infty$).

ENNReal.sum_eq_top theorem

: ∑ x ∈ s, f x = ∞ ↔ ∃ a ∈ s, f a = ∞

Full source

/-- A sum is infinite iff one of the summands is infinite. -/
@[simp] lemma sum_eq_top : ∑ x ∈ s, f x∑ x ∈ s, f x = ∞ ↔ ∃ a ∈ s, f a = ∞ := WithTop.sum_eq_top

Sum is Infinite if and only if a Summand is Infinite in Extended Non-Negative Reals

Informal description

For a function $f$ defined on a set $s$ with values in the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the sum $\sum_{x \in s} f(x)$ is infinite if and only if there exists an element $a \in s$ such that $f(a) = \infty$.

ENNReal.sum_ne_top theorem

: ∑ a ∈ s, f a ≠ ∞ ↔ ∀ a ∈ s, f a ≠ ∞

Full source

/-- A sum is finite iff all summands are finite. -/
lemma sum_ne_top : ∑ a ∈ s, f a∑ a ∈ s, f a ≠ ∞∑ a ∈ s, f a ≠ ∞ ↔ ∀ a ∈ s, f a ≠ ∞ := WithTop.sum_ne_top

Sum is Finite if and only if All Summands are Finite

Informal description

For a finite set $s$ and a function $f : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, the sum $\sum_{a \in s} f(a)$ is not equal to $\infty$ if and only if $f(a) \neq \infty$ for all $a \in s$.

ENNReal.sum_lt_top theorem

: ∑ a ∈ s, f a < ∞ ↔ ∀ a ∈ s, f a < ∞

Full source

/-- A sum is finite iff all summands are finite. -/
@[simp] lemma sum_lt_top : ∑ a ∈ s, f a∑ a ∈ s, f a < ∞ ↔ ∀ a ∈ s, f a < ∞ := WithTop.sum_lt_top

Sum Finiteness Criterion for Extended Non-Negative Reals

Informal description

For a finite set $s$ and a function $f : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, the sum $\sum_{a \in s} f(a)$ is finite if and only if $f(a) < \infty$ for every $a \in s$.

ENNReal.lt_top_of_sum_ne_top theorem

{s : Finset α} {f : α → ℝ≥0∞} (h : ∑ x ∈ s, f x ≠ ∞) {a : α} (ha : a ∈ s) : f a < ∞

Full source

theorem lt_top_of_sum_ne_top {s : Finset α} {f : α → ℝ≥0∞} (h : ∑ x ∈ s, f x∑ x ∈ s, f x ≠ ∞) {a : α}
    (ha : a ∈ s) : f a < ∞ :=
  sum_lt_top.1 h.lt_top a ha

Finiteness of Summands in Finite Sum of Extended Non-Negative Reals

Informal description

For any finite set $s$, any function $f : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, and any element $a \in s$, if the sum $\sum_{x \in s} f(x)$ is finite, then $f(a) < \infty$.

ENNReal.toNNReal_sum theorem

 {s : Finset α} {f : α → ℝ≥0∞} (hf : ∀ a ∈ s, f a ≠ ∞) :
  ENNReal.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, ENNReal.toNNReal (f a)

Full source

/-- Seeing `ℝ≥0∞` as `ℝ≥0` does not change their sum, unless one of the `ℝ≥0∞` is
infinity -/
theorem toNNReal_sum {s : Finset α} {f : α → ℝ≥0∞} (hf : ∀ a ∈ s, f a ≠ ∞) :
    ENNReal.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, ENNReal.toNNReal (f a) := by
  rw [← coe_inj, coe_toNNReal, coe_finset_sum, sum_congr rfl]
  · intro x hx
    exact (coe_toNNReal (hf x hx)).symm
  · exact sum_ne_top.2 hf

Sum Preservation under `toNNReal` for Finite Sums in Extended Non-Negative Reals

Informal description

For any finite set $s$ and any function $f : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $f(a) \neq \infty$ for all $a \in s$, the canonical map to non-negative real numbers preserves the sum: \[ \text{toNNReal}\left(\sum_{a \in s} f(a)\right) = \sum_{a \in s} \text{toNNReal}(f(a)). \]

ENNReal.toReal_sum theorem

 {s : Finset α} {f : α → ℝ≥0∞} (hf : ∀ a ∈ s, f a ≠ ∞) : ENNReal.toReal (∑ a ∈ s, f a) = ∑ a ∈ s, ENNReal.toReal (f a)

Full source

/-- seeing `ℝ≥0∞` as `Real` does not change their sum, unless one of the `ℝ≥0∞` is infinity -/
theorem toReal_sum {s : Finset α} {f : α → ℝ≥0∞} (hf : ∀ a ∈ s, f a ≠ ∞) :
    ENNReal.toReal (∑ a ∈ s, f a) = ∑ a ∈ s, ENNReal.toReal (f a) := by
  rw [ENNReal.toReal, toNNReal_sum hf, NNReal.coe_sum]
  rfl

Sum Preservation under `toReal` for Finite Sums in Extended Non-Negative Reals

Informal description

For any finite set $s$ and any function $f : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $f(a) \neq \infty$ for all $a \in s$, the canonical map to real numbers preserves the sum: \[ \text{toReal}\left(\sum_{a \in s} f(a)\right) = \sum_{a \in s} \text{toReal}(f(a)). \]

ENNReal.ofReal_sum_of_nonneg theorem

 {s : Finset α} {f : α → ℝ} (hf : ∀ i, i ∈ s → 0 ≤ f i) : ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)

Full source

theorem ofReal_sum_of_nonneg {s : Finset α} {f : α → ℝ} (hf : ∀ i, i ∈ s → 0 ≤ f i) :
    ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i) := by
  simp_rw [ENNReal.ofReal, ← coe_finset_sum, coe_inj]
  exact Real.toNNReal_sum_of_nonneg hf

Sum of Nonnegative Reals Preserved under `ofReal`

Informal description

For any finite set $s$ and any function $f : \alpha \to \mathbb{R}$ such that $f(i) \geq 0$ for all $i \in s$, the extended non-negative real number obtained by applying the `ofReal` function to the sum of $f$ over $s$ is equal to the sum over $s$ of the `ofReal` function applied to each $f(i)$. That is, \[ \text{ofReal}\left(\sum_{i \in s} f(i)\right) = \sum_{i \in s} \text{ofReal}(f(i)). \]

ENNReal.sum_lt_sum_of_nonempty theorem

 {s : Finset α} (hs : s.Nonempty) {f g : α → ℝ≥0∞} (Hlt : ∀ i ∈ s, f i < g i) : ∑ i ∈ s, f i < ∑ i ∈ s, g i

Full source

theorem sum_lt_sum_of_nonempty {s : Finset α} (hs : s.Nonempty) {f g : α → ℝ≥0∞}
    (Hlt : ∀ i ∈ s, f i < g i) : ∑ i ∈ s, f i < ∑ i ∈ s, g i := by
  induction hs using Finset.Nonempty.cons_induction with
  | singleton => simp [Hlt _ (Finset.mem_singleton_self _)]
  | cons _ _ _ _ ih =>
    simp only [Finset.sum_cons, forall_mem_cons] at Hlt ⊢
    exact ENNReal.add_lt_add Hlt.1 (ih Hlt.2)

Strict Sum Inequality for Extended Non-Negative Reals on Nonempty Finite Sets

Informal description

For any nonempty finite set $s$ and functions $f, g : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $f(i) < g(i)$ for every $i \in s$, then the sum of $f$ over $s$ is strictly less than the sum of $g$ over $s$.

ENNReal.exists_le_of_sum_le theorem

 {s : Finset α} (hs : s.Nonempty) {f g : α → ℝ≥0∞} (Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i) : ∃ i ∈ s, f i ≤ g i

Full source

theorem exists_le_of_sum_le {s : Finset α} (hs : s.Nonempty) {f g : α → ℝ≥0∞}
    (Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i) : ∃ i ∈ s, f i ≤ g i := by
  contrapose! Hle
  apply ENNReal.sum_lt_sum_of_nonempty hs Hle

Existence of Element with $f(i) \leq g(i)$ under Sum Inequality in Extended Non-Negative Reals

Informal description

For any nonempty finite set $s$ and functions $f, g : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, if the sum of $f$ over $s$ is less than or equal to the sum of $g$ over $s$, then there exists an element $i \in s$ such that $f(i) \leq g(i)$.

ENNReal.prod_inv_distrib theorem

 {ι : Type*} {f : ι → ℝ≥0∞} {s : Finset ι} (hf : s.toSet.Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) :
  (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹

Full source

lemma prod_inv_distrib {ι : Type*} {f : ι → ℝ≥0∞} {s : Finset ι}
    (hf : s.toSet.Pairwise fun i j ↦ f i ≠ 0f i ≠ 0 ∨ f j ≠ ∞) : (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹ := by
  induction' s using Finset.cons_induction with i s hi ih
  · simp
  simp [← ih (hf.mono <| by simp)]
  refine ENNReal.mul_inv (not_or_of_imp fun hi₀ ↦ prod_ne_top fun j hj ↦ ?_)
    (not_or_of_imp fun hi₀ ↦ Finset.prod_ne_zero_iff.2 fun j hj ↦ ?_)
  · exact imp_iff_not_or.2 (hf (by simp) (by simp [hj]) <| .symm <| ne_of_mem_of_not_mem hj hi) hi₀
  · exact imp_iff_not_or.2 (hf (by simp [hj]) (by simp) <| ne_of_mem_of_not_mem hj hi).symm hi₀

Inverse of Product Equals Product of Inverses in Extended Non-Negative Reals

Informal description

For any finite set $s$ and any function $f \colon \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, if for every pair of distinct elements $i, j \in s$ we have $f(i) \neq 0$ or $f(j) \neq \infty$, then the inverse of the product of $f$ over $s$ equals the product of the inverses of $f$ over $s$, i.e., $$ \left(\prod_{i \in s} f(i)\right)^{-1} = \prod_{i \in s} (f(i))^{-1}. $$

ENNReal.finsetSum_iSup theorem

 {α ι : Type*} {s : Finset α} {f : α → ι → ℝ≥0∞} (hf : ∀ i j, ∃ k, ∀ a, f a i ≤ f a k ∧ f a j ≤ f a k) :
  ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i

Full source

lemma finsetSum_iSup {α ι : Type*} {s : Finset α} {f : α → ι → ℝ≥0∞}
    (hf : ∀ i j, ∃ k, ∀ a, f a i ≤ f a k ∧ f a j ≤ f a k) :
    ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i := by
  induction' s using Finset.cons_induction with a s ha ihs
  · simp
  simp_rw [Finset.sum_cons, ihs]
  refine iSup_add_iSup fun i j ↦ (hf i j).imp fun k hk ↦ ?_
  gcongr
  exacts [(hk a).1, (hk _).2]

Supremum and Finite Sum Commutativity in Extended Non-Negative Reals

Informal description

Let $\alpha$ and $\iota$ be types, $s$ be a finite subset of $\alpha$, and $f : \alpha \to \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ be a family of functions. If for any $i, j \in \iota$ there exists $k \in \iota$ such that for all $a \in \alpha$, both $f(a)(i) \leq f(a)(k)$ and $f(a)(j) \leq f(a)(k)$ hold, then the sum over $a \in s$ of the suprema $\bigsqcup_i f(a)(i)$ equals the supremum over $i$ of the sums $\sum_{a \in s} f(a)(i)$. In symbols: \[ \sum_{a \in s} \bigsqcup_i f(a)(i) = \bigsqcup_i \sum_{a \in s} f(a)(i). \]

ENNReal.finsetSum_iSup_of_monotone theorem

 {α ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {s : Finset α} {f : α → ι → ℝ≥0∞} (hf : ∀ a, Monotone (f a)) :
  (∑ a ∈ s, iSup (f a)) = ⨆ n, ∑ a ∈ s, f a n

Full source

lemma finsetSum_iSup_of_monotone {α ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {s : Finset α}
    {f : α → ι → ℝ≥0∞} (hf : ∀ a, Monotone (f a)) : (∑ a ∈ s, iSup (f a)) = ⨆ n, ∑ a ∈ s, f a n :=
  finsetSum_iSup fun i j ↦ (exists_ge_ge i j).imp fun _k ⟨hi, hj⟩ a ↦ ⟨hf a hi, hf a hj⟩

Monotone Supremum and Finite Sum Commutativity in Extended Non-Negative Reals

Informal description

Let $\alpha$ and $\iota$ be types, with $\iota$ equipped with a preorder $\leq$ such that $\iota$ is directed (i.e., every pair of elements has a common upper bound). Let $s$ be a finite subset of $\alpha$, and let $f \colon \alpha \to \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ be a family of functions such that for each $a \in \alpha$, the function $f(a)$ is monotone. Then the sum over $a \in s$ of the suprema $\bigsqcup_i f(a)(i)$ equals the supremum over $i$ of the sums $\sum_{a \in s} f(a)(i)$. In symbols: \[ \sum_{a \in s} \bigsqcup_i f(a)(i) = \bigsqcup_i \sum_{a \in s} f(a)(i). \]