fixes #1797 (add cvg_dnbhs_at_right)

CHANGELOG_UNRELEASED.md

@@ -85,6 +85,8 @@
   + lemmas `limit_point_closed`
 - in `convex.v`:
   + lemma `convex_setW`
+- in `num_topology.v`:
+  + lemmas `cvg_dnbhs_at_right`, `cvg_dnbhs_at_left`
 
 ### Changed
 
@@ -246,6 +248,12 @@
 - moved from `tvs.v` to `convex.v`
   + definition `convex`, renamed to `convex_set`
 
+- moved from `realfun.v` to `metric_structure.v`:
+  + lemma `cvg_at_right_left_dnbhs` and generalized to `metricType R`
+
+- moved from `realfun.v` to `num_topology.v`:
+  + lemma `left_right_continuousP`
+
 ### Renamed
 
 - in `topology_structure.v`

theories/ftc.v

@@ -94,7 +94,7 @@ Proof.
 move=> intf F x ax fx.
 have locf : locally_integrable setT f.
   by apply: open_integrable_locally => //; exact: openT.
-apply: cvg_at_right_left_dnbhs.
+apply: (@cvg_at_right_left_dnbhs _ R^o).
 - apply/cvg_at_rightP => d [d_gt0 d0].
   pose E x n := `[x, x + d n[%classic%R.
   have muE y n : mu (E y n) = (d n)%:E.

theories/realfun.v

@@ -103,37 +103,6 @@ apply: near_eq_cvg; near do rewrite subrK; exists M.
 by rewrite num_real.
 Unshelve. all: by end_near. Qed.
 
-Lemma left_right_continuousP {T : topologicalType} (f : R -> T) x :
-  f @ x^'- --> f x /\ f @ x^'+ --> f x <-> f @ x --> f x.
-Proof.
-split; last by move=> cts; split; exact: cvg_within_filter.
-move=> [+ +] U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl.
-rewrite !near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf.
-near=> t => xlt xgt; have := @real_leVge R x t; rewrite !num_real.
-move=> /(_ isT isT) /orP; rewrite !le_eqVlt => -[|] /predU1P[|//].
-- by move=> <-; exact: nbhs_singleton.
-- by move=> ->; exact: nbhs_singleton.
-Unshelve. all: by end_near. Qed.
-
-Lemma cvg_at_right_left_dnbhs (f : R -> R) (p : R) (l : R) :
-  f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l ->
-  f x @[x --> p^'] --> l.
-Proof.
-move=> /cvgrPdist_le fppl /cvgrPdist_le fpnl; apply/cvgrPdist_le => e e0.
-have {fppl}[a /= a0 fppl] := fppl _ e0; have {fpnl}[b /= b0 fpnl] := fpnl _ e0.
-near=> t.
-have : t != p by near: t; exact: nbhs_dnbhs_neq.
-rewrite neq_lt => /orP[tp|pt].
-- apply: fpnl => //=; near: t.
-  exists (b / 2) => //=; first by rewrite divr_gt0.
-  move=> z/= + _ => /lt_le_trans; apply.
-  by rewrite ler_pdivrMr// ler_pMr// ler1n.
-- apply: fppl =>//=; near: t.
-  exists (a / 2) => //=; first by rewrite divr_gt0.
-  move=> z/= + _ => /lt_le_trans; apply.
-  by rewrite ler_pdivrMr// ler_pMr// ler1n.
-Unshelve. all: by end_near. Qed.
-
 End fun_cvg_realFieldType.
 
 Section cvgr_fun_cvg_seq.
@@ -197,7 +166,7 @@ split=> [/cvgrPdist_le fpl u [up /cvgrPdist_lt put]|pfl].
   apply/cvgrPdist_le => e /fpl [r /=] /put[n _ {}put] {}fpl.
   near=> t; apply: fpl => //=; apply: put.
   by near: t; exact: nbhs_infty_ge.
-apply: cvg_at_right_left_dnbhs.
+apply: (@cvg_at_right_left_dnbhs _ R^o).
 - by apply/cvg_at_rightP => u [pu ?]; apply: pfl; split => // n; rewrite gt_eqF.
 - by apply/cvg_at_leftP => u [pu ?]; apply: pfl; split => // n; rewrite lt_eqF.
 Unshelve. all: end_near. Qed.
@@ -2947,7 +2916,7 @@ Hypotheses (fa0 : f x @[x --> c] --> 0) (ga0 : g x @[x --> c] --> 0)
 Lemma lhopital :
   df x / dg x @[x --> c] --> l -> f x / g x @[x --> c^'] --> l.
 Proof.
-move=> fgcl; apply/cvg_at_right_left_dnbhs.
+move=> fgcl; apply/(@cvg_at_right_left_dnbhs _ R^o).
 - apply: (@lhopital_at_right R f df g dg c b l); try exact/cvg_at_right_filter.
   + by move: cab; rewrite in_itv/= => /andP[].
   + move=> x xac; apply: fdf; rewrite set_itv_splitU ?in_setU//=.

theories/topology_theory/metric_structure.v

@@ -314,3 +314,30 @@ by rewrite ltNge metric_sym => /negP.
 Unshelve. all: end_near. Qed.
 
 End cvg_nbhsP.
+
+Section cvg_at_right_left_dnbhs.
+Variables (R : realFieldType) (T : metricType R).
+
+Import metricType_numDomainType.
+
+Lemma cvg_at_right_left_dnbhs (f : R -> T) (p : R) (l : T) :
+  f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l ->
+  f x @[x --> p^'] --> l.
+Proof.
+move=> /cvgrPdist_le fppl /cvgrPdist_le fpnl; apply/cvgrPdist_le => e e0.
+have {fppl}[a /= a0 fppl] := fppl (at_right_proper_filter p) _ e0.
+have {fpnl}[b /= b0 fpnl] := fpnl (at_left_proper_filter p) _ e0.
+near=> t.
+have : t != p by near: t; exact: nbhs_dnbhs_neq.
+rewrite neq_lt => /orP[tp|pt].
+- apply: fpnl => //=; near: t.
+  exists (b / 2) => //=; first by rewrite divr_gt0.
+  move=> z/= + _ => /lt_le_trans; apply.
+  by rewrite ler_pdivrMr// ler_pMr// ler1n.
+- apply: fppl =>//=; near: t.
+  exists (a / 2) => //=; first by rewrite divr_gt0.
+  move=> z/= + _ => /lt_le_trans; apply.
+  by rewrite ler_pdivrMr// ler_pMr// ler1n.
+Unshelve. all: by end_near. Qed.
+
+End cvg_at_right_left_dnbhs.

theories/topology_theory/num_topology.v

@@ -171,6 +171,18 @@ apply; last by rewrite gtrBl.
 by rewrite /= opprB addrC subrK ger0_norm// gtr_pMr// invf_lt1// ltr1n.
 Qed.
 
+Lemma cvg_dnbhs_at_right (T : topologicalType) (f : R -> T) (p : R) (l : T) :
+  f x @[x --> p^'] --> l -> f x @[x --> p^'+] --> l.
+Proof.
+by apply: cvg_trans; apply: cvg_app; apply: within_subset=> r ?; rewrite gt_eqF.
+Qed.
+
+Lemma cvg_dnbhs_at_left (T : topologicalType) (f : R -> T) (p : R) (l : T) :
+  f x @[x --> p^'] --> l -> f x @[x --> p^'-] --> l.
+Proof.
+by apply: cvg_trans; apply: cvg_app; apply: within_subset=> r ?; rewrite lt_eqF.
+Qed.
+
 Lemma nbhs_right_gt x : \forall y \near x^'+, x < y.
 Proof. by rewrite near_withinE; apply: nearW. Qed.
 
@@ -240,6 +252,19 @@ Notation "x ^'+" := (at_right x) : classical_set_scope.
 #[global] Hint Extern 0 (Filter (nbhs _^'-)) =>
   (apply: at_left_proper_filter) : typeclass_instances.
 
+Lemma left_right_continuousP {R : realFieldType} {T : topologicalType}
+    (f : R -> T) x :
+  f @ x^'- --> f x /\ f @ x^'+ --> f x <-> f @ x --> f x.
+Proof.
+split; last by move=> cts; split; exact: cvg_within_filter.
+move=> [+ +] U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl.
+rewrite !near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf.
+near=> t => xlt xgt; have := @real_leVge R x t; rewrite !num_real.
+move=> /(_ isT isT) /orP; rewrite !le_eqVlt => -[|] /predU1P[|//].
+- by move=> <-; exact: nbhs_singleton.
+- by move=> ->; exact: nbhs_singleton.
+Unshelve. all: by end_near. Qed.
+
 Lemma closure_sup (R : realType) (A : set R) :
   A !=set0 -> has_ubound A -> closure A (sup A).
 Proof.