proposition: Lemma psum_fin (f : I -> R) : psum f = \sum_i `|f i|.
proof: Proof. pose S := \sum_(i : [fset i | i : I]) `|f (val i)|. rewrite /psum (asboolT (summable_fin f)) (@max_sup _ S). rewrite /=; split; first by exists [fset i | i : I]%fset. apply/ubP=> y [J ->]; apply/(big_fset_subset (F := \`|_|)). by move=> i; rewrite normr_ge0. by move=> j jJ; apply/in_imfset. rewrite /S -(big_map val xpredT \`|f|); apply/perm_big. rewrite /index_enum -!enumT; apply/(perm_trans _ enum_fsetT). apply/uniq_perm; rewrite ?map_inj_uniq ?enum_uniq //=. by apply/val_inj. by rewrite -enumT enum_uniq. move=> i /=; rewrite mem_enum in_imfset //; apply/mapP. have h: i \in [fset j | j : I] by rewrite in_imfset. by exists (FSetSub h) => //; rewrite mem_enum. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology