Properties of big operators extended non-negative real numbers #

theorem ENNReal.iInf_sum {ι : Type u_3} {α : Type u_4} {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

Documentation

Mathlib.Data.ENNReal.BigOperators

Properties of big operators extended non-negative real numbers #