proposition: Lemma reindex_esum (R : realType) (T T' : choiceType) (P : set T) (Q : set T') (e : T -> T') (a : T' -> \bar R) : set_bij P Q e -> \esum_(j in Q) a j = \esum_(i in P) a (e i).
proof: Proof. elim/choicePpointed: T => T in e P *. rewrite !emptyE => /Pbij[{}e ->]. by rewrite -[in LHS](image_eq e) image_set0 !esum_set0. elim/choicePpointed: T' => T' in a e Q *; first by have := no (e point). move=> /(@pPbij _ _ _)[{}e ->]. gen have le_esum : T T' a P Q e / \esum_(j in Q) a j <= \esum_(i in P) a (e i); last first. apply/eqP; rewrite eq_le le_esum//=. rewrite [leRHS](_ : _ = \esum_(j in Q) a (e (e^-1%FUN j))); last first. by apply: eq_esum => i Qi; rewrite invK ?inE. by rewrite le_esum => //= i Qi; rewrite a_ge0//; exact: funS. rewrite ub_ereal_sup => //= _ [X [finX XQ] <-]; rewrite ereal_sup_ub => //=. exists [set` (e^-1 @` (fset_set X))%fset]. split=> [|t /= /imfsetP[t'/=]]; first exact: finite_fset. by rewrite in_fset_set// inE => /XQ Qt' ->; exact: funS. rewrite fsbig_finite//= set_fsetK big_imfset => //=; last first. move=> x y; rewrite !in_fset_set// !inE => /XQ ? /XQ ? /(congr1 e). by rewrite !invK ?inE. by rewrite -fsbig_finite//; apply: eq_fsbigr=> x /[!inE]/XQ ?; rewrite invK ?inE. 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