proposition: Lemma ereal_nondecreasing_cvgn (R : realType) (u_ : (\bar R)^nat) : nondecreasing_seq u_ -> u_ @ \oo --> ereal_sup (range u_).
proof: Proof. move=> nd_u_; set S := u_ @` setT; set l := ereal_sup S. have [Spoo|Spoo] := pselect (S +oo). have [N Nu] : exists N, forall n, (n >= N)%nat -> u_ n = +oo. case: Spoo => N _ uNoo; exists N => n Nn. by move: (nd_u_ _ _ Nn); rewrite uNoo leye_eq => /eqP. have -> : l = +oo by rewrite /l /ereal_sup; exact: supremum_pinfty. rewrite -(cvg_shiftn N); set f := (X in X @ \oo --> _). rewrite (_ : f = cst +oo); first exact: cvg_cst. by rewrite funeqE => n; rewrite /f /= Nu // leq_addl. have [/funext Snoo|Snoo] := pselect (forall n, u_ n = -oo). rewrite /l (_ : S = [set -oo]). by rewrite ereal_sup1 Snoo; exact: cvg_cst. apply/seteqP; split => [_ [n _] <- /[!Snoo]//|_ ->]. by rewrite /S Snoo; exists 0%N. have [/ereal_sup_ninfty loo|lnoo] := eqVneq l -oo. by exfalso; apply: Snoo => n; rewrite (loo (u_ n))//; exists n. have {Snoo}[N Snoo] : exists N, forall n, (n >= N)%N -> u_ n != -oo. move/existsNP : Snoo => [m /eqP]. rewrite neq_lt => /orP[|umoo]; first by rewrite ltNge leNye. by exists m => k mk; rewrite gt_eqF// (lt_le_trans umoo)// nd_u_. have u_fin_num n : (n >= N)%N -> u_ n \is a fin_num. move=> Nn; rewrite fin_numE Snoo//=; apply: contra_notN Spoo => /eqP unpoo. by exists n. have [{lnoo}loo|lpoo] := eqVneq l +oo. rewrite loo; apply/cvgeyPge => M. have /ereal_sup_gt[_ [n _] <- Mun] : M%:E < l by rewrite loo// ltry. by exists n => // m /= nm; rewrite (le_trans (ltW Mun))// nd_u_. have l_fin_num : l \is a fin_num by rewrite fin_numE lpoo lnoo. rewrite -(@fineK _ l)//; apply/fine_cvgP; split. near=> n; rewrite fin_numE Snoo/=; last by near: n; exists N. by apply: contra_notN Spoo => /eqP unpoo; exists n. rewrite -(cvg_shiftn N); set v_ := [sequence _]_ _. have <- : sup (range v_) = fine l. apply: EFin_inj; rewrite -ereal_sup_EFin//; last 2 first. - exists (fine l) => /= _ [m _ <-]; rewrite /v_ /= fine_le//. by rewrite u_fin_num// leq_addl. by apply: ereal_sup_ub; exists (m + N)%N. - by exists (v_ 0%N), 0%N. rewrite fineK//; apply/eqP; rewrite eq_le; apply/andP; split. apply: le_ereal_sup => _ /= [_ [m _] <-] <-. by exists (m + N)%N => //; rewrite /v_/= fineK// u_fin_num// leq_addl. apply: ub_ereal_sup => /= _ [m _] <-. rewrite (@le_trans _ _ (u_ (m + N)%N))//; first by rewrite nd_u_// leq_addr. apply: ereal_sup_ub => /=; exists (fine (u_ (m + N)%N)); first by exists m. by rewrite fineK// u_fin_num// leq_addl. apply: nondecreasing_cvgn. - move=> m n mn /=; rewrite /v_ /= fine_le ?u_fin_num ?leq_addl//. by rewrite nd_u_// leq_add2r. - exists (fine l) => /= _ [m _ <-]; rewrite /v_ /= fine_le//. by rewrite u_fin_num// leq_addl. by apply: ereal_sup_ub; exists (m + N)%N. Unshelve. all: by end_near. 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