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∞.

@[simp]

theorem ENNReal.ofNNReal_finsetSum {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

@[deprecated ENNReal.ofNNReal_finsetSum (since := "2026-06-04")]

theorem ENNReal.coe_finsetSum {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

Alias of ENNReal.ofNNReal_finsetSum.

@[simp]

theorem ENNReal.ofNNReal_finsetProd {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

@[deprecated ENNReal.ofNNReal_finsetProd (since := "2026-06-04")]

theorem ENNReal.coe_finsetProd {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

Alias of ENNReal.ofNNReal_finsetProd.

@[simp]

theorem ENNReal.ofNNReal_finsuppSum {ι : Type u_1} {M : Type u_2} [Zero M] (f : ι →₀ M) (g : ι → M → NNReal) : ↑(f.sum g) = f.sum fun (i : ι) (m : M) => ↑(g i m)

@[simp]

theorem ENNReal.ofNNReal_finsuppProd {ι : Type u_1} {M : Type u_2} [Zero M] (f : ι →₀ M) (g : ι → M → NNReal) : ↑(f.prod g) = f.prod fun (i : ι) (m : M) => ↑(g i m)

@[simp]

theorem ENNReal.toNNReal_prod {ι : Type u_1} (s : Finset ι) (f : ι → ENNReal) : (∏ i ∈ s, f i).toNNReal = ∏ i ∈ s, (f i).toNNReal

@[simp]

theorem ENNReal.toReal_prod {ι : Type u_1} (s : Finset ι) (f : ι → ENNReal) : (∏ i ∈ s, f i).toReal = ∏ i ∈ s, (f i).toReal

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

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

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.

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.

@[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.

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.

@[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.

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 < ⊤

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

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

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)

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

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

theorem ENNReal.sum_div {α : Type u_1} {s : Finset α} {f : α → ENNReal} (a : ENNReal) : (∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a

Finset.sum_div does not apply since ℝ≥0∞ is not a DivisionSemiring. Although the proof of Finset.sum_div only needs DivInvMonoid and NonUnitalNonAssocSemiring, the best typeclass including these is DivisionSemiring.

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)⁻¹

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

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

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

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

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