proposition: Lemma esum_esum [R : realType] [T1 T2 : choiceType] (I : set T1) (J : T1 -> set T2) (a : T1 -> T2 -> \bar R) : (forall i j, I i -> J i j -> 0 <= a i j) -> \esum_(i in I) \esum_(j in J i) a i j = \esum_(k in I `*`` J) a k.1 k.2.
proof: Proof. move=> a_ge0; apply/eqP; rewrite eq_le; apply/andP; split. apply: ub_ereal_sup => /= _ [X [finX XI]] <-. under eq_fsbigr do rewrite esum_mkcond. rewrite fsbig_finite//= big_seq -esum_sum; last first. move=> i j _ /[!in_fset_set]// /[!inE] /XI Ij. by case: ifPn => // /[!inE] /a_ge0-/(_ Ij). under eq_esum do rewrite -big_seq -big_mkcond/=. apply: ub_ereal_sup => /= _ [Y [finY _] <-]; apply: ereal_sup_ub => /=. set XYJ := [set z | z \in X `*` Y /\ z.2 \in J z.1]. have ? : finite_set XYJ. apply: sub_finite_set (finite_setM finX finY) => z/=. by rewrite /XYJ/= in_setM => -[/andP[] /[!inE]]. exists XYJ => /=; first by split => //= z; rewrite /XYJ/= 2!inE=> -[[/XI]]. rewrite [in RHS]fsbig_finite//= (exchange_big_dep xpredT)// pair_big_dep_cond. rewrite fsbig_finite//; apply: eq_fbigl => -[/= x y]; rewrite in_fset_set//. apply/idP/imfset2P. rewrite /XYJ !inE/= !inE/= -andA => -[Xx [Yy Jxy]]. exists x; first by rewrite !inE in_fset_set// mem_set. by exists y => //; rewrite !inE mem_set// in_fset_set// mem_set. move=> [t1]; rewrite !inE andbT/= in_fset_set// inE => Xt1. by move=> [t2]; rewrite !inE in_fset_set /XYJ//= =>/andP[/[!inE] ? ?] [-> ->]. apply: ub_ereal_sup => _ /= [X/= [finX XIJ]] <-; apply: esum_ge. exists X.`1; first by split=> [|x [y /XIJ[]//]]; exact: finite_set_fst. apply: (@le_trans _ _ (\sum_(i <- fset_set X.`1) \sum_(j <- fset_set X.`2 | j \in J i) a i j)). rewrite pair_big_dep_cond//=; set Y := Imfset.imfset2 _ _ _ _. rewrite [leRHS](big_fsetID _ (mem X))/=. rewrite (_ : [fset x | x in Y & x \in X] = Y `&` fset_set X)%fset; last first. by apply/fsetP => x; rewrite 2!inE/= in_fset_set. rewrite (fsetIidPr _). rewrite fsbig_finite// leeDl// big_seq sume_ge0//=. move=> [x y] /imfsetP[[x1 y1]] /[!inE] /andP[] /imfset2P[x2]/= /[!inE]. rewrite andbT in_fset_set//; last exact: finite_set_fst. move=> /[!inE] x2X [y2] /[!inE] /andP[] /[!in_fset_set]; last first. exact: finite_set_snd. move=> /[!inE] y2X y2J [-> ->] _ [-> ->]; rewrite a_ge0//. by move: x2X => [y3 /XIJ []]. apply/fsubsetP => -[i j]; rewrite in_fset_set// inE => Xij; apply/imfset2P. exists i => /=. rewrite !inE/= in_fset_set//; last exact: finite_set_fst. by rewrite andbT mem_set//; move/fst_set_fst : Xij. exists j => //; rewrite !inE/= in_fset_set; last exact: finite_set_snd. rewrite mem_set/=; last by move/snd_set_snd : Xij. by rewrite mem_set//; move/XIJ : Xij => []. rewrite -fsbig_finite; last exact: finite_set_fst. apply lee_fsum=> [|i Xi]; first exact: finite_set_fst. rewrite ereal_sup_ub => //=; have ? : finite_set (X.`2 `&` J i). by apply: finite_setI; left; exact: finite_set_snd. exists (X.`2 `&` J i) => //. rewrite [in RHS]big_fset_condE/= fsbig_finite//; apply eq_fbigl => j. by rewrite in_fset_set// !inE/= in_setI in_fset_set//; exact: finite_set_snd. 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