proposition: Lemma sum_ncvg l : ncvg (fun n => \sum_(i < n) S i) l%:E -> summable S.
proof: Proof. Proof using ge0_S. Abort. End PSumCnv. Section PSumAsLim. Context {R : realType} {T : choiceType}. Variable (S : T -> R) (P : nat -> {fset T}). Hypothesis ge0_S : (forall x, 0 <= S x). Hypothesis smS : summable S. Hypothesis homo_P : forall n m, (n <= m)%N -> (P n `<=` P m). Hypothesis cover_P : forall x, S x != 0 -> exists n, x \in P n. Lemma psum_as_lim : psum S = fine (nlim (fun n => \sum_(j : P n) (S (val j)))). Proof. set v := fun n => _; have hm_v m n: (m <= n)%N -> v m <= v n. by move=> le_mn; apply/big_fset_subset/fsubsetP/homo_P. have bd_v n : v n <= psum S. apply/(le_trans _ (gerfin_psum _ smS))/ler_sum. by move=> J _; apply/ler_norm. case: (ncvg_mono_bnd hm_v) => [|l cv]. apply/asboolP/nboundedP; exists (psum S + 1) => //. by apply/(le_lt_trans (ge0_psum S)); rewrite ltrDl ltr01. move=> n; rewrite ger0_norm ?sumr_ge0 //. by rewrite (le_lt_trans (bd_v n)) // ltrDl ltr01. have le_lS: l <= psum S by rewrite -lee_fin (ncvg_leC _ cv). rewrite (nlimE cv) /= (rwP eqP) eq_le le_lS andbT. rewrite leNgt; apply/negP=> {le_lS} /(lt_psum smS)[J]. rewrite (big_fset_seq \`|_|) /=; case: J => /= J. move/canonical_uniq=> uqJ lt_jS; pose K := [seq x <- J | S x != 0]. have [n]: exists n, {subset K <= P n}; first rewrite {}/K. elim: {uqJ lt_jS} J => /= [|x J [n ih]]; first by exists 0%N. case: (S x =P 0) => /=; first by move=> _; exists n. move/eqP/cover_P=> [k Pk_x]; exists (maxn n k)=> y. rewrite inE => /orP[/eqP->|/=]. by apply/fsubsetP/homo_P/leq_maxr: x Pk_x. by move/ih; apply/fsubsetP/homo_P/leq_maxl: y. move=> le_K_Pn; have: l < v n; first apply/(lt_le_trans lt_jS). rewrite (eq_bigr S) => [x _|]; first by rewrite ger0_norm. rewrite /v (bigID (fun x => S x == 0)) /= big1 => [x /eqP|] //. rewrite add0r -big_filter -/K -big_seq_fset ?filter_uniq //=. by apply/big_fset_subset => // x; rewrite in_fset => /le_K_Pn. by apply/negP; rewrite -leNgt -lee_fin ncvg_homo_le. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology