fact: Definition esum S a := ereal_sup [set \sum_(x \in A) a x | A in fsets S].
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun