proposition: Lemma nondecreasing_at_right_cvge (f : R -> \bar R) a (b : itv_bound R) : (BRight a < b)%O -> {in Interval (BRight a) b &, nondecreasing_fun f} -> f x @[x --> a ^'+] --> ereal_inf (f @` [set` Interval (BRight a) b]).
proof: Proof. move=> ab ndf; set S := (X in ereal_inf X); set l := ereal_inf S. have [Snoo|Snoo] := pselect (S -oo). case: (Snoo) => N/=. rewrite in_itv/= -[X in _ && X]/(BLeft N < b)%O => /andP[aN Nb] fNpoo. have Nf n : (a < n <= N)%R -> f n = -oo. move=> /andP[an nN]; apply/eqP. rewrite eq_le leNye andbT -fNpoo ndf//. by rewrite in_itv/= -[X in _ && X]/(BLeft n < b)%O an (le_lt_trans _ Nb). by rewrite in_itv/= -[X in _ && X]/(BLeft N < b)%O (lt_le_trans an nN). have -> : l = -oo. by rewrite /l /ereal_inf /ereal_sup supremum_pinfty//=; exists -oo. apply: cvg_near_cst; exists (N - a)%R => /=; first by rewrite subr_gt0. move=> y /= + ay; rewrite ltr0_norm ?subr_lt0// opprB => ayNa. by rewrite Nf// ay/= -(subrK a y) -lerBrDr ltW. have [lnoo|lnoo] := eqVneq l -oo. rewrite lnoo; apply/cvgeNyPle => M. have /ereal_inf_lt[x [y]]/= : M%:E > l by rewrite lnoo ltNyr. rewrite in_itv/= -[X in _ && X]/(BLeft y < b)%O/= => /andP[ay yb] <- fyM. exists (y - a)%R => /=; first by rewrite subr_gt0. move=> z /= + az. rewrite ltr0_norm ?subr_lt0// opprB ltrBlDr subrK => zy. rewrite (le_trans _ (ltW fyM))// ndf ?ltW//. by rewrite in_itv/= -[X in _ && X]/(BLeft z < b)%O/= az/= (lt_trans _ yb). by rewrite in_itv/= -[X in _ && X]/(BLeft y < b)%O/= (lt_trans az zy). have [fpoo|fpoo] := pselect {in Interval (BRight a) b, forall x, f x = +oo}. rewrite {}/l in lnoo *; rewrite {}/S in Snoo lnoo *. rewrite [X in ereal_inf X](_ : _ = [set +oo]). rewrite ereal_inf1; apply/cvgeyPgey; near=> M. move: b ab {ndf lnoo Snoo} fpoo => [[|] b|[//|]] ab fpoo. - near=> x; rewrite fpoo ?leey// in_itv/=. by apply/andP; split; near: x; [exact: nbhs_right_gt|exact: nbhs_right_lt]. - near=> x; rewrite fpoo ?leey// in_itv/=. by apply/andP; split; near: x; [exact: nbhs_right_gt|exact: nbhs_right_le]. - near=> x; rewrite fpoo ?leey// in_itv/= andbT. by near: x; exact: nbhs_right_gt. apply/seteqP; split => [_ [n _] <- /[!fpoo]//|_ ->]. move: b ab ndf lnoo Snoo fpoo => [[|] s|[//|]] ab ndf lnoo Snoo fpoo /=. - by exists ((a + s) / 2)%R; rewrite ?fpoo// in_itv/= !midf_lt. - by exists ((a + s) / 2)%R; rewrite ?fpoo// in_itv/= !(midf_lt, midf_le)// ltW. - by exists (a + 1)%R; rewrite ?fpoo// in_itv/= andbT ltrDl. have [/ereal_inf_pinfty lpoo|lpoo] := eqVneq l +oo. by exfalso; apply/fpoo => r rab; rewrite (lpoo (f r))//; exists r. have l_fin_num : l \is a fin_num by rewrite fin_numE lpoo lnoo. set A := [set r | [/\ (a < r)%R, (BLeft r < b)%O & f r != +oo]]. have f_fin_num r : r \in A -> f r \is a fin_num. rewrite inE /A/= => -[ar rb] frnoo; rewrite fin_numE frnoo andbT. apply: contra_notN Snoo => /eqP frpoo. by exists r => //=; rewrite in_itv/= -[X in _ && X]/(BLeft r < b)%O ar rb. have [x [ax xb fxpoo]] : A !=set0. apply/set0P/negP => /eqP A0; apply/fpoo => x. rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O => /andP[ax xb]. apply/eqP/negPn/negP => unnoo. by move/seteqP : A0 => [+ _] => /(_ x); apply; rewrite /A/= ax. have axA r : (a < r <= x)%R -> r \in A. move=> /andP[ar rx]; move: (rx) => /ndf rafx; rewrite /A /= inE; split => //. by rewrite (le_lt_trans _ xb). apply/negP => /eqP urnoo. move: rafx; rewrite urnoo. rewrite in_itv/= -[X in _ && X]/(BLeft r < b)%O ar/=. rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O ax/=. by rewrite leye_eq (negbTE fxpoo) -falseE; apply; rewrite (le_lt_trans _ xb). rewrite -(@fineK _ l)//; apply/fine_cvgP; split. exists (x - a)%R => /=; first by rewrite subr_gt0. move=> z /= + az. rewrite ltr0_norm ?subr_lt0// opprB ltrBlDr subrK// => zx. by rewrite f_fin_num// axA// az/= ltW. set g := fun n => if (a < n < x)%R then fine (f n) else fine (f x). have <- : inf [set g x | x in [set` Interval (BRight a) b]] = fine l. apply: EFin_inj; rewrite -ereal_inf_EFin//; last 2 first. - exists (fine l) => /= _ [m _ <-]; rewrite /g /=. case: ifPn => [/andP[am mx]|]. rewrite fine_le// ?f_fin_num//; first by rewrite axA// am (ltW mx). apply: ereal_inf_lb; exists m => //=. rewrite in_itv/= -[X in _ && X]/(BLeft m < b)%O am/=. by rewrite (le_lt_trans _ xb) ?ltW. rewrite negb_and -!leNgt => /orP[ma|xm]. rewrite fine_le// ?f_fin_num ?inE//. apply: ereal_inf_lb; exists x => //=. by rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O ax xb. rewrite fine_le// ?f_fin_num ?inE//. apply: ereal_inf_lb; exists x => //=. by rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O ax xb. - rewrite {}/l in lnoo lpoo l_fin_num *. rewrite {}/S in Snoo lnoo lpoo l_fin_num *. rewrite {}/A in f_fin_num axA *. move: b ab {xb ndf lnoo lpoo l_fin_num f_fin_num Snoo fpoo axA} => [[|] s|[//|]] ab /=. + exists (g ((a + s) / 2))%R, ((a + s) / 2)%R => //=. by rewrite /= in_itv/= !midf_lt. + exists (g ((a + s) / 2))%R, ((a + s) / 2)%R => //=. by rewrite /= in_itv/= !(midf_lt, midf_le)// ltW. + exists (g (a + 1)%R), (a + 1)%R => //=. by rewrite in_itv/= andbT ltrDl. rewrite fineK//; apply/eqP; rewrite eq_le; apply/andP; split; last first. apply: le_ereal_inf => _ /= [_ [m _] <-] <-. rewrite /g; case: ifPn => [/andP[am mx]|]. rewrite fineK// ?f_fin_num//; last by rewrite axA// am ltW. exists m => //=. by rewrite in_itv/= -[X in _ && X]/(BLeft m < b)%O am/= (lt_trans _ xb). rewrite negb_and -!leNgt => /orP[ma|xm]. rewrite fineK//; last by rewrite f_fin_num ?inE. exists x => //=. by rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O ax xb. exists x => /=. by rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O ax xb. by rewrite fineK// f_fin_num ?inE. apply: lb_ereal_inf => /= y [m] /=. rewrite in_itv/= -[X in _ && X]/(BLeft m < b)%O => /andP[am mb] <-{y}. have [mx|xm] := ltP m x. apply: ereal_inf_lb => /=; exists (fine (f m)); last first. by rewrite fineK// f_fin_num// axA// am (ltW mx). by exists m; [rewrite in_itv/= am|rewrite /g am mx]. rewrite (@le_trans _ _ (f x))//; last first. by apply: ndf => //; rewrite in_itv//= ?ax ?am. apply: ereal_inf_lb => /=; exists (fine (f x)); last first. by rewrite fineK// f_fin_num ?inE. by exists x; [rewrite in_itv/= ax|rewrite /g ltxx andbF]. suff: g x @[x --> a^'+] --> inf [set g x | x in [set` Interval (BRight a) b]]. apply: cvg_trans; apply: near_eq_cvg; near=> n. rewrite /g /=; case: ifPn => [//|]. rewrite negb_and -!leNgt => /orP[na|xn]. exfalso. move: na; rewrite leNgt => /negP; apply. by near: n; exact: nbhs_right_gt. suff nx : (n < x)%R by rewrite ltNge xn in nx. near: n; exists ((x - a) / 2)%R; first by rewrite /= divr_gt0// subr_gt0. move=> y /= /[swap] ay. rewrite ltr0_norm// ?subr_lt0// opprB ltrBlDr => /lt_le_trans; apply. by rewrite -lerBrDr ler_pdivrMr// ler_pMr// ?ler1n// subr_gt0. apply: nondecreasing_at_right_cvgr => //. - move=> m n; rewrite !in_itv/= -[X in _ && X]/(BLeft m < b)%O. rewrite -[X in _ -> _ && X -> _]/(BLeft n < b)%O. move=> /andP[am mb] /andP[an nb] mn. rewrite /g /=; case: ifPn => [/andP[_ mx]|]. rewrite (lt_le_trans am mn) /=; have [nx|nn0] := ltP n x. rewrite fine_le ?f_fin_num ?ndf//; first by rewrite axA// am (ltW mx). by rewrite axA// (ltW nx) andbT (lt_le_trans am). by rewrite in_itv/= am. by rewrite in_itv/= an. rewrite fine_le ?f_fin_num//. + by rewrite axA// am (ltW (lt_le_trans mx _)). + by rewrite inE. + rewrite ndf//; last exact/ltW. by rewrite !in_itv/= am. by rewrite !in_itv/= ax. rewrite negb_and -!leNgt => /orP[|xm]; first by rewrite leNgt am. by rewrite (lt_le_trans am mn)/= ltNge (le_trans xm mn). - exists (fine l) => /= _ [m _ <-]; rewrite /g /=. rewrite -lee_fin (fineK l_fin_num); apply: ereal_inf_lb. case: ifPn => [/andP[am mn0]|]. rewrite fineK//; last by rewrite f_fin_num// axA// am (ltW mn0). exists m => //=. by rewrite in_itv/= -[X in _ && X]/(BLeft m < b)%O am (lt_trans _ xb). rewrite negb_and -!leNgt => /orP[ma|xm]. rewrite fineK//; first by exists x => //=; rewrite in_itv/= ax. by rewrite f_fin_num ?inE. by rewrite fineK// ?f_fin_num ?inE//; exists x => //=; rewrite in_itv/= ax. 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)