proposition: Lemma esum_mkcond [R : realType] [T : choiceType] (I : set T) (a : T -> \bar R) : \esum_(i in I) a i = \esum_(i in [set: T]) if i \in I then a i else 0.
proof: Proof. apply/eqP; rewrite eq_le !ub_ereal_sup//= => _ [X [finX XI]] <-. rewrite -big_mkcond/= big_fset_condE/=; set Y := [fset _ | _ in _ & _]%fset. rewrite ereal_sup_ub//=; exists [set` Y]; last by rewrite fsbig_finite// set_fsetK. by split => // i/=; rewrite !inE/= => /andP[_]; rewrite inE. rewrite ereal_sup_ub//; exists X => //; apply: eq_fsbigr => x; rewrite inE => Xx. by rewrite ifT// inE; exact: XI. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun