left version of a lemma

CHANGELOG_UNRELEASED.md

@@ -67,6 +67,7 @@
   + lemma `cvg_at_rightP`
   + lemma `cvg_at_leftP`
   + lemma `cvge_at_rightP`
+  + lemma `cvge_at_leftP`
   + lemma `lime_sup`
   + lemma `lime_inf`
   + lemma `lime_supE`
@@ -80,9 +81,13 @@
   + lemma `lime_inf_sup`
   + lemma `lim_lime_inf`
   + lemma `lim_lime_sup`
+  + lemma `lime_sup_inf_at_right`
+  + lemma `lime_sup_inf_at_left`
 
 - in `normedtype.v`:
   + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP`
+  + lemma `dnbhsN`
+  + lemma `limf_esup_dnbhsN`
 
 - in `topology.v`:
   + lemma `dnbhs_ball`

theories/normedtype.v

@@ -150,7 +150,7 @@ Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
 Section limf_esup_einf.
-Variables (T : choiceType) (X : filteredType T) (R : realType).
+Variables (T : choiceType) (X : filteredType T) (R : realFieldType).
 Implicit Types (f : X -> \bar R) (F : set (set X)).
 Local Open Scope ereal_scope.
 
@@ -248,6 +248,20 @@ move=> [y [[z Az oppzey] [t Bt opptey]]]; exists (- y).
 by split; [rewrite -oppzey opprK|rewrite -opptey opprK].
 Qed.
 
+Lemma dnbhsN {R : numFieldType} (r : R) :
+  (- r)%R^' = (fun A => -%R @` A) @` r^'.
+Proof.
+apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]].
+  exists (-%R @` A).
+    exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//.
+    by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC.
+  rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=.
+  by rewrite opprK.
+exists e => //= x/=; rewrite -opprD normrN => axe xa.
+exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=.
+by rewrite opprK.
+Qed.
+
 Module PseudoMetricNormedZmodule.
 Section ClassDef.
 Variable R : numDomainType.
@@ -1663,6 +1677,15 @@ End Exports.
 End numFieldNormedType.
 Import numFieldNormedType.Exports.
 
+Lemma limf_esup_dnbhsN {R : realType} (f : R -> \bar R) (a : R) :
+  limf_esup f a^' = limf_esup (fun x => f (- x)%R) (- a)%R^'.
+Proof.
+rewrite /limf_esup dnbhsN image_comp/=.
+congr (ereal_inf [set _ | _ in _]); apply/funext => A /=.
+rewrite image_comp/= -compA (_ : _ \o _ = idfun)// funeqE => x/=.
+by rewrite opprK.
+Qed.
+
 Section NormedModule_numDomainType.
 Variables (R : numDomainType) (V : normedModType R).
 
@@ -2131,18 +2154,25 @@ move=> r aer ar; rewrite -(opprK r); apply: aeE; last by rewrite -memNE.
 by rewrite /= opprK -normrN opprD.
 Qed.
 
+Let fun_predC (T : choiceType) (f : T -> T) (p : pred T) : involutive f ->
+  [set f x | x in p] = [set x | x in p \o f].
+Proof.
+by move=> fi; apply/seteqP; split => _/= [y hy <-];
+  exists (f y) => //; rewrite fi.
+Qed.
+
 Lemma at_rightN a : (- a)^'+ = -%R @ a^'-.
 Proof.
-rewrite /at_right withinN (_ : [set - x | x in _] = (fun u => u < a))//.
-apply/seteqP; split=> [x [r /[1!ltr_oppl] ? <-//]|x xa/=].
-by exists (- x); rewrite 1?ltr_oppr ?opprK.
+rewrite /at_right withinN [X in within X _](_ : _ = [set u | u < a])//.
+rewrite (@fun_predC _ -%R)/=; last exact: opprK.
+by rewrite image_id; under eq_fun do rewrite ltr_oppl opprK.
 Qed.
 
 Lemma at_leftN a : (- a)^'- = -%R @ a^'+.
 Proof.
-rewrite /at_left withinN (_ : [set - x | x in _] = (fun u => a < u))//.
-apply/seteqP; split=> [x [r /[1!ltr_oppr] ? <-//]|x xa/=].
-by exists (- x); rewrite 1?ltr_oppr ?opprK.
+rewrite /at_left withinN [X in within X _](_ : _ = [set u | a < u])//.
+rewrite (@fun_predC _ -%R)/=; last exact: opprK.
+by rewrite image_id; under eq_fun do rewrite ltr_oppl opprK.
 Qed.
 
 End at_left_right.

theories/realfun.v

@@ -199,6 +199,18 @@ have {mn} := mfy_ _ mn.
 rewrite /y_ /sval; case: cid2 => /= x _.
 Unshelve. all: by end_near. Qed.
 
+Lemma cvge_at_leftP (f : R -> \bar R) (p l : R) :
+  f x @[x --> p^'-] --> l%:E <->
+  (forall u : R^nat, (forall n, u n < p) /\ u --> p ->
+    f (u n) @[n --> \oo] --> l%:E).
+Proof.
+apply: (iff_trans (cvg_at_leftNP f p l%:E)).
+apply: (iff_trans (cvge_at_rightP _ _ l)); split=> h u [up pu].
+- rewrite (_ : u = \- (\- u))%R; last by apply/funext => ?/=; rewrite opprK.
+  by apply: h; split; [by move=> n; rewrite ltr_oppl opprK|exact: cvgN].
+- by apply: h; split => [n|]; [rewrite ltr_oppl|move/cvgN : pu; rewrite opprK].
+Qed.
+
 End cvge_fun_cvg_seq.
 
 Section fun_cvg_realType.
@@ -744,7 +756,7 @@ have [d {}H] := H e.
 by exists d => r /H; rewrite lte_oppl oppeD// EFinN oppeK.
 Qed.
 
-Lemma lime_inf_sup_lim f a l :
+Lemma lime_sup_inf_at_right f a l :
   lime_sup f a = l%:E -> lime_inf f a = l%:E -> f x @[x --> a^'+] --> l%:E.
 Proof.
 move=> supfpl inffpl; apply/cvge_at_rightP => u [pu up].
@@ -797,6 +809,14 @@ apply: ereal_sup_ub => /=; exists (u n).
 by rewrite fineK//; near: n.
 Unshelve. all: by end_near. Qed.
 
+Lemma lime_sup_inf_at_left f a l :
+  lime_sup f a = l%:E -> lime_inf f a = l%:E -> f x @[x --> a^'-] --> l%:E.
+Proof.
+move=> supfal inffal; apply/cvg_at_leftNP/lime_sup_inf_at_right.
+- by rewrite /lime_sup -limf_esup_dnbhsN.
+- by rewrite /lime_inf /lime_sup -(limf_esup_dnbhsN (-%E \o f)) limf_esupN oppeK.
+Qed.
+
 End lime_sup_inf.
 
 Section derivable_oo_continuous_bnd.