Documentation

Mathlib.Topology.Algebra.InfiniteSum.ENNReal

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 #

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