Big operators on extended real numbers

This file contains elementary lemmas about finite sums in EReal.

theorem EReal.sum_mul_of_nonneg {ι : Type u_1} {s : Finset ι} {f : ι → EReal} {a : EReal} (hf : ∀ i ∈ s, 0 ≤ f i) : (∑ i ∈ s, f i) * a = ∑ i ∈ s, f i * a

theorem EReal.mul_sum_of_nonneg {ι : Type u_1} {s : Finset ι} {f : ι → EReal} {a : EReal} (hf : ∀ i ∈ s, 0 ≤ f i) : a * ∑ i ∈ s, f i = ∑ i ∈ s, a * f i

theorem EReal.mul_sum_of_nonneg_of_ne_top {ι : Type u_1} {s : Finset ι} {f : ι → EReal} {a : EReal} (ha : 0 ≤ a) (ha' : a ≠ ⊤) : a * ∑ i ∈ s, f i = ∑ i ∈ s, a * f i

theorem EReal.sum_mul_of_nonneg_of_ne_top {ι : Type u_1} {s : Finset ι} {f : ι → EReal} {a : EReal} (ha : 0 ≤ a) (ha' : a ≠ ⊤) : (∑ i ∈ s, f i) * a = ∑ i ∈ s, f i * a

@[simp]

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