proposition: Lemma nneseries_sum I (r : seq I) (P : {pred I}) [R : realType] [f : I -> nat -> \bar R] : (forall i j, P i -> 0 <= f i j) -> \sum_(j <oo) \sum_(i <- r | P i) f i j = \sum_(i <- r | P i) \sum_(j <oo) f i j.
proof: Proof. move=> f_ge0; case Dr : r => [|i r']; rewrite -?{}[_ :: _]Dr. by rewrite big_nil eseries0// => i; rewrite big_nil. rewrite {r'}(big_nth i) big_mkcond. rewrite (eq_eseriesr (fun _ _ => big_nth i _ _)). rewrite (eq_eseriesr (fun _ _ => big_mkcond _ _))/=. rewrite nneseries_sum_nat; last by move=> ? ?; case: ifP => // /f_ge0. by apply: eq_bigr => j _; case: ifP => //; rewrite eseries0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau