proposition: Lemma esum_bigcup J a : trivIset [set i | a @` J i != [set 0]] J -> (forall x : T, (\bigcup_(k in K) J k) x -> 0 <= a x) -> \esum_(i in \bigcup_(k in K) J k) a i = \esum_(k in K) \esum_(j in J k) a j.
proof: Proof. move=> Jtriv a_ge0. pose J' i := if a @` J i == [set 0] then set0 else J i. pose a' x := if x \in \bigcup_(k in K) J k then a x else 0. have a'E k x : K k -> J k x -> a' x = a x. move=> Kk Jkx; rewrite /a'; case: ifPn; rewrite ?(inE, notin_set)//=. by case; exists k. have a'_ge0 x : a' x >= 0 by rewrite /a'; case: ifPn; rewrite // ?inE => /a_ge0. transitivity (\esum_(i in \bigcup_(k in K) J' k) a' i). rewrite esum_mkcond [RHS]esum_mkcond /a'; apply: eq_esum => x _. do 2!case: ifPn; rewrite ?(inE, notin_set)//= => J'x Jx. apply: contra_not_eq J'x => Nax. move: Jx => [k kK Jkx]; exists k=> //; rewrite /J'/=; case: ifPn=> //=. move=> /eqP/(congr1 (@^~ (a x)))/=; rewrite propeqE => -[+ _]. by apply: contra_neq_not Nax; apply; exists x. rewrite esum_bigcupT//; last first. move=> i j _ _ [x []]; rewrite /J'/=. case: eqVneq => //= Ai0 Jix; case: eqVneq => //= Aj0 Jjx. by have := Jtriv i j Ai0 Aj0; apply; exists x. apply: eq_esum => i Ki. rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum => x _. do 2!case: ifPn; rewrite ?(inE, notin_set)//=. - by move=> /a'E->//. - by rewrite /J'; case: ifPn => //. move=> Jix; rewrite /J'; case: ifPn=> //=. by move=> /eqP/(congr1 (@^~ (a x)))/=; rewrite propeqE => -[->]//; exists x. 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