proposition: Lemma psum_bigop (F : I -> T -> R) P r : (forall i x, 0 <= F i x) -> (forall i, summable (F i)) -> \sum_(i <- r | P i) psum (F i) = psum (fun x => \sum_(i <- r | P i) F i x).
proof: Proof. move=> ge0_F sm_F; elim: r => [|i r ih]. by rewrite big_nil; apply/esym/psum_eq0 => x; rewrite big_nil. rewrite big_cons ih; case: ifP => Pi; last first. by apply/eq_psum=> x /=; rewrite big_cons Pi. rewrite -psumD //; first by move=> x; apply/sumr_ge0. by apply/summable_sum. by apply/eq_psum=> x /=; rewrite big_cons Pi. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology