Documentation

Mathlib.Data.ENNReal.BigOperators

Properties of big operators extended non-negative real numbers #

In this file we prove elementary properties of sums and products on ℝ≥0∞, as well as how these interact with the order structure on ℝ≥0∞.

source
@[simp]
theorem ENNReal.coe_finset_sum {α : Type u_1} {s : Finset α} {f : α → NNReal} :
↑(∑ a ∈ s, f a) = ∑ a ∈ s, ↑(f a)
source
@[simp]
theorem ENNReal.coe_finset_prod {α : Type u_1} {s : Finset α} {f : α → NNReal} :
↑(∏ a ∈ s, f a) = ∏ a ∈ s, ↑(f a)
source
@[simp]
theorem ENNReal.toNNReal_prod {ι : Type u_2} {s : Finset ι} {f : ι → ENNReal} :
(∏ i ∈ s, f i).toNNReal = ∏ i ∈ s, (f i).toNNReal
source
@[simp]
theorem ENNReal.toReal_prod {ι : Type u_2} {s : Finset ι} {f : ι → ENNReal} :
(∏ i ∈ s, f i).toReal = ∏ i ∈ s, (f i).toReal
source
theorem ENNReal.ofReal_prod_of_nonneg {α : Type u_2} {s : Finset α} {f : α → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i) :
ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i)
source
theorem ENNReal.iInf_sum {ι : Type u_2} {α : Type u_3} {f : ι → α → ENNReal} {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
source
theorem ENNReal.prod_ne_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} (h : ∀ a ∈ s, f a ≠ ⊤) :
∏ a ∈ s, f a ≠ ⊤

A product of finite numbers is still finite.

source
theorem ENNReal.prod_lt_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} (h : ∀ a ∈ s, f a < ⊤) :
∏ a ∈ s, f a < ⊤

A product of finite numbers is still finite.

source
@[simp]
theorem ENNReal.sum_eq_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} :
∑ x ∈ s, f x = ⊤ ↔ ∃ a ∈ s, f a = ⊤

A sum is infinite iff one of the summands is infinite.

source
theorem ENNReal.sum_ne_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} :
∑ a ∈ s, f a ≠ ⊤ ↔ ∀ a ∈ s, f a ≠ ⊤

A sum is finite iff all summands are finite.

source
@[simp]
theorem ENNReal.sum_lt_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} :
∑ a ∈ s, f a < ⊤ ↔ ∀ a ∈ s, f a < ⊤

A sum is finite iff all summands are finite.

source
theorem ENNReal.lt_top_of_sum_ne_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} (h : ∑ x ∈ s, f x ≠ ⊤) {a : α} (ha : a ∈ s) :
f a < ⊤
source
theorem ENNReal.toNNReal_sum {α : Type u_1} {s : Finset α} {f : α → ENNReal} (hf : ∀ a ∈ s, f a ≠ ⊤) :
(∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal

Seeing ℝ≥0∞ as ℝ≥0 does not change their sum, unless one of the ℝ≥0∞ is infinity

source
theorem ENNReal.toReal_sum {α : Type u_1} {s : Finset α} {f : α → ENNReal} (hf : ∀ a ∈ s, f a ≠ ⊤) :
(∑ a ∈ s, f a).toReal = ∑ a ∈ s, (f a).toReal

seeing ℝ≥0∞ as Real does not change their sum, unless one of the ℝ≥0∞ is infinity

source
theorem ENNReal.ofReal_sum_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i) :
ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)
source
theorem ENNReal.sum_lt_sum_of_nonempty {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {f g : α → ENNReal} (Hlt : ∀ i ∈ s, f i < g i) :
∑ i ∈ s, f i < ∑ i ∈ s, g i
source
theorem ENNReal.exists_le_of_sum_le {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {f g : α → ENNReal} (Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i) :
∃ i ∈ s, f i ≤ g i
source
theorem ENNReal.prod_inv_distrib {ι : Type u_1} {f : ι → ENNReal} {s : Finset ι} (hf : (↑s).Pairwise fun (i j : ι) => f i ≠ 0 ∨ f j ≠ ⊤) :
(∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
source
theorem ENNReal.prod_div_distrib {ι : Type u_1} {f g : ι → ENNReal} {s : Finset ι} (hg : (↑s).Pairwise fun (i j : ι) => g i ≠ 0 ∨ g j ≠ ⊤) :
∏ i ∈ s, f i / g i = (∏ i ∈ s, f i) / ∏ i ∈ s, g i
source
theorem ENNReal.prod_div_distrib_of_ne_top {ι : Type u_1} {f g : ι → ENNReal} {s : Finset ι} (hg : ∀ i ∈ s, g i ≠ ⊤) :
∏ i ∈ s, f i / g i = (∏ i ∈ s, f i) / ∏ i ∈ s, g i
source
theorem ENNReal.prod_div_distrib_of_ne_zero {ι : Type u_1} {f g : ι → ENNReal} {s : Finset ι} (hg : ∀ i ∈ s, g i ≠ 0) :
∏ i ∈ s, f i / g i = (∏ i ∈ s, f i) / ∏ i ∈ s, g i
source
theorem ENNReal.finsetSum_iSup {ι : Type u_1} {α : Type u_2} {s : Finset α} {f : α → ι → ENNReal} (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
source
theorem ENNReal.finsetSum_iSup_of_monotone {ι : Type u_1} {α : Type u_2} [Preorder ι] [IsDirectedOrder ι] {s : Finset α} {f : α → ι → ENNReal} (hf : ∀ (a : α), Monotone (f a)) :
∑ a ∈ s, iSup (f a) = ⨆ (n : ι), ∑ a ∈ s, f a n