proposition: Lemma nondecreasing_cvge (f : R -> \bar R) : nondecreasing_fun f -> f r @[r --> +oo%R] --> ereal_sup (range f).
proof: Proof. move=> ndf; set S := range f; set l := ereal_sup S. have [Spoo|Spoo] := pselect (S +oo). have [N Nf] : exists N, forall n, (n >= N)%R -> f n = +oo. case: Spoo => N _ uNoo; exists N => n Nn. by have := ndf _ _ Nn; rewrite uNoo leye_eq => /eqP. have -> : l = +oo by rewrite /l /ereal_sup; exact: supremum_pinfty. rewrite -(cvg_shiftr `|N|); apply: cvg_near_cst. exists N; split; first by rewrite num_real. by move=> x /ltW Nx; rewrite Nf// ler_wpDr. have [lpoo|lpoo] := eqVneq l +oo. rewrite lpoo; apply/cvgeyPge => M. have /ereal_sup_gt[_ [n _] <- Mun] : M%:E < l by rewrite lpoo// ltry. exists n; split; first by rewrite num_real. by move=> m /= nm; rewrite (le_trans (ltW Mun))// ndf// ltW. have [fnoo|fnoo] := pselect (f = cst -oo). rewrite /l (_ : S = [set -oo]). by rewrite ereal_sup1 fnoo; exact: cvg_cst. apply/seteqP; split => [_ [n _] <- /[!fnoo]//|_ ->]. by rewrite /S fnoo; exists 0%R. have [/ereal_sup_ninfty lnoo|lnoo] := eqVneq l -oo. by exfalso; apply/fnoo/funext => n; rewrite (lnoo (f n))//; exists n. have l_fin_num : l \is a fin_num by rewrite fin_numE lpoo lnoo. set A := [set n | f n = -oo]; set B := [set n | f n != -oo]. have f_fin_num n : B n -> f n \is a fin_num. move=> Bn; rewrite fin_numE Bn/=. by apply: contra_notN Spoo => /eqP unpoo; exists n. have [x Bx] : B !=set0. apply/set0P/negP => /eqP B0; apply/fnoo/funext => n. apply/eqP/negPn/negP => unnoo. by move/seteqP : B0 => [+ _] => /(_ n); apply. have xB r : (x <= r)%R -> B r. move=> /ndf xr; apply/negP => /eqP urnoo. by move: xr; rewrite urnoo leeNy_eq; exact/negP. rewrite -(@fineK _ l)//; apply/fine_cvgP; split. exists x; split; first by rewrite num_real. by move=> r A1r; rewrite f_fin_num //; exact/xB/ltW. set g := fun n => if (n < x)%R then fine (f x) else fine (f n). have <- : sup (range g) = fine l. apply: EFin_inj; rewrite -ereal_sup_EFin//; last 2 first. - exists (fine l) => /= _ [m _ <-]; rewrite /g /=. have [mx|xm] := ltP m x. by rewrite fine_le// ?f_fin_num//; apply: ereal_sup_ub; exists x. rewrite fine_le// ?f_fin_num//; first exact/xB. by apply: ereal_sup_ub; exists m. - by exists (g 0%R), 0%R. rewrite fineK//; apply/eqP; rewrite eq_le; apply/andP; split. apply: le_ereal_sup => _ /= [_ [m _] <-] <-. rewrite /g; have [_|xm] := ltP m x. by rewrite fineK// ?f_fin_num//; exists x. by rewrite fineK// ?f_fin_num//; [exists m|exact/xB]. apply: ub_ereal_sup => /= _ [m _] <-. have [mx|xm] := ltP m x. rewrite (le_trans (ndf _ _ (ltW mx)))//. apply: ereal_sup_ub => /=; exists (fine (f x)); last first. by rewrite fineK// f_fin_num. by exists m => //; rewrite /g mx. apply: ereal_sup_ub => /=; exists (fine (f m)) => //. by exists m => //; rewrite /g ltNge xm. by rewrite fineK ?f_fin_num//; exact: xB. suff: g x @[x --> +oo%R] --> sup (range g). apply: cvg_trans; apply: near_eq_cvg; near=> n. rewrite /g ifF//; apply/negbTE; rewrite -leNgt. by near: n; apply: nbhs_pinfty_ge; rewrite num_real. apply: nondecreasing_cvgr. - move=> m n mn; rewrite /g /=; have [_|xm] := ltP m x. + have [nx|nx] := ltP n x; first by rewrite fine_le// f_fin_num. by rewrite fine_le// ?f_fin_num//; [exact: xB|exact: ndf]. + rewrite ltNge (le_trans xm mn)//= fine_le ?f_fin_num//. * exact: xB. * by apply: xB; rewrite (le_trans xm). * exact/ndf. - exists (fine l) => /= _ [m _ <-]; rewrite /g /=. rewrite -lee_fin (fineK l_fin_num); apply: ereal_sup_ub. have [_|xm] := ltP m x; first by rewrite fineK// ?f_fin_num//; eexists. by rewrite fineK// ?f_fin_num//; [exists m|exact/xB]. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)