Infinite sums of ENNReal and Set.encard

This file provides lemmas relating sums of constants to the cardinality of the domain of these sums.

TODO

• Once we have a topology on ENat, provide an ENat valued version
• Once we replace PartENat entirely with ENat (and replace PartENat.card with a ENat.card), provide versions which sum over the whole type.

theorem ENNReal.tsum_set_one {α : Type u_1} (s : Set α) : ∑' (x : ↑s), 1 = ↑s.encard

theorem ENNReal.tsum_set_const {α : Type u_1} (s : Set α) (c : ENNReal) : ∑' (x : ↑s), c = ↑s.encard * c

@[deprecated ENNReal.tsum_set_one (since := "2025-02-06")]

theorem ENNReal.tsum_set_one_eq {α : Type u_1} (s : Set α) : ∑' (x : ↑s), 1 = ↑s.encard

Alias of ENNReal.tsum_set_one.

@[deprecated ENNReal.tsum_set_const (since := "2025-02-06")]

theorem ENNReal.tsum_set_const_eq {α : Type u_1} (s : Set α) (c : ENNReal) : ∑' (x : ↑s), c = ↑s.encard * c

Alias of ENNReal.tsum_set_const.

@[simp]

theorem ENNReal.tsum_one {α : Type u_1} : ∑' (x : α), 1 = ↑(ENat.card α)

@[simp]

theorem ENNReal.tsum_const {α : Type u_1} (c : ENNReal) : ∑' (x : α), c = ↑(ENat.card α) * c