proposition: Lemma nonincreasing_at_right_cvgr f a (b : itv_bound R) : (BRight a < b)%O -> {in Interval (BRight a) b &, nonincreasing_fun f} -> has_ubound (f @` [set` Interval (BRight a) b]) -> f x @[x --> a ^'+] --> sup (f @` [set` Interval (BRight a) b]).
proof: Proof. move=> ab lef ubf; set M := sup _. have supf : has_sup [set f x | x in [set` Interval (BRight a) b]]. split => //; case: b ab {lef ubf M} => [[|] t ta|[]] /=. - exists (f ((a + t) / 2)), ((a + t) / 2) => //=. by rewrite in_itv/= !midf_lt. - exists (f ((a + t) / 2)), ((a + t) / 2) => //=. by rewrite in_itv/= midf_lt// midf_le// ltW. - by exists (f (a + 1)), (a + 1). - by exists (f (a + 1)), (a + 1) => //=; rewrite in_itv/= ltrDl andbT. apply/cvgrPdist_le => _/posnumP[e]. have {supf} [p [ap pb]] : exists p, [/\ a < p, (BLeft p < b)%O & M - e%:num <= f p]. have [_ -[p apb] <- /ltW efp] := sup_adherent (gt0 e) supf. move: apb; rewrite /= in_itv/= -[X in _ && X]/(BLeft p < b)%O => /andP[ap pb]. by exists p; split. rewrite lerBlDr {}/M. move: b ab pb lef ubf => [[|] b|[//|]] ab pb lef ubf; set M := sup _ => Mefp. - near=> r; rewrite ler_distl; apply/andP; split. + suff: f r <= M by apply: le_trans; rewrite lerBlDr lerDl. apply: sup_ub => //=; exists r => //; rewrite in_itv/=. by apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_lt]. + rewrite (le_trans Mefp)// lerD2r lef//=; last 2 first. by rewrite in_itv/= ap. by near: r; exact: nbhs_right_le. apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_lt]. - near=> r; rewrite ler_distl; apply/andP; split. + suff: f r <= M by apply: le_trans; rewrite lerBlDr lerDl. apply: sup_ub => //=; exists r => //; rewrite in_itv/=. by apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_le]. + rewrite (le_trans Mefp)// lerD2r lef//=; last 2 first. by rewrite in_itv/= ap. by near: r; exact: nbhs_right_le. by apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_le]. - near=> r; rewrite ler_distl; apply/andP; split. suff: f r <= M by apply: le_trans; rewrite lerBlDr lerDl. apply: sup_ub => //=; exists r => //; rewrite in_itv/= andbT. by near: r; apply: nbhs_right_gt. rewrite (le_trans Mefp)// lerD2r lef//. - by rewrite in_itv/= andbT; near: r; exact: nbhs_right_gt. - by rewrite in_itv/= ap. - by near: r; exact: nbhs_right_le. 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)