normed type neighborhood lemmas

CHANGELOG_UNRELEASED.md

@@ -21,13 +21,26 @@
   + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`,
     `at_left_shift`, `at_right_shift`
 
+- in `num_normedtype.v`,
+  + lemmas `pinftyV`, `ninftyV`, `cvgryV`, `cvgrNyV`, `lt0_cvgMlNy`, 
+    `lt0_cvgMrNy`, `lt0_cvgMly`, `lt0_cvgMry`
+
+- in `pseudometric_normed_Zmodule.v`,
+  + lemmas `fmap_at_left0P`, `fmap_at_right0E`
+
+- in `tvs.v`,
+  + lemmas `near_shiftE`, `nearZE`
+
+- in `num_topology.v`:
+  + lemmas `near_right_in_itv`, `near_left_in_itv`
+
 ### Changed
 
 - in `derive.v`:
   + instance `is_derive_mx` is now a lemma
 
 - moved from `metric_structure.v` to `num_topology.v`: 
-  + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`.
+  + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`
 
 ### Renamed
 

theories/normedtype_theory/num_normedtype.v

@@ -245,6 +245,53 @@ apply/seteqP; split => [A [M [Mreal MA]]|A [M [Mreal MA]]].
 by exists (- M); rewrite ?realN; split=> // x; rewrite ltrNl => /MA.
 Qed.
 
+Lemma pinftyV (R : numFieldType) : x^-1 @[x --> +oo] = (0 : R)^'+.
+Proof.
+apply/seteqP; split=> [A [M [Mreal MA]]|A [r /= r0 rA]].
+- have mM1_gt0 : 0 < Num.max M 1.
+    case: (@real_leP _ M 1) => //.
+    by apply: lt_trans.
+  exists (Num.max M 1)^-1; first by rewrite /= invr_gt0.
+  move=> x /= /[swap] x_gt0.
+  rewrite distrC subr0 gtr0_norm// invf_pgt ?posrE// => mM1_lt_xV.
+  rewrite -(invrK x); apply: MA.
+  apply: le_lt_trans mM1_lt_xV.
+  by case: (@real_leP _ M 1).
+- exists r^-1; split; first by rewrite realV gtr0_real.
+  move=> x /[dup] rV_lt_x.
+  have x_gt0 : x > 0.
+    apply: lt_trans rV_lt_x.
+    by rewrite invr_gt0.
+  rewrite invf_plt// => xV_lt_r.
+  apply: rA; last by rewrite invr_gt0.
+  by rewrite /= distrC subr0 gtr0_norm// invr_gt0.
+Qed.
+
+Lemma ninftyV (R : numFieldType) : x^-1 @[x --> -oo] = (0 : R)^'-.
+Proof.
+apply/seteqP; split=> [A [M [Mreal MA]]|A [r /= r0 rA]].
+- pose M' := Num.min M (-1).
+  have M'_lt0 : M' < 0.
+    rewrite /M'.
+    case: (@real_leP _ M (-1)) => // /le_lt_trans.
+    by apply.
+  exists (-M')^-1; first by rewrite /= invr_gt0 oppr_gt0.
+  move=> x /= /[swap] x_lt0.
+  rewrite distrC subr0 ltr0_norm// invrN ltrN2 => x_gt_VM'.
+  rewrite -(invrK x); apply: MA.
+  apply: (lt_le_trans (y := M')).
+  + by rewrite invf_nlt.
+  + by rewrite /M'; case: (@real_ltP _ M (-1)).
+- exists (- r^-1); split; first by rewrite realN realV gtr0_real.
+  move=> x /[dup] x_lt_NrV.
+  have x_lt0 : x < 0.
+    apply: (lt_trans x_lt_NrV).
+    by rewrite oppr_lt0 invr_gt0.
+  rewrite ltrNr invf_plt// ?posrE ?oppr_gt0// => NxV_lt_r.
+  apply: rA; last by rewrite invr_lt0.
+  by rewrite /= distrC subr0 ltr0_norm ?invr_lt0// -invrN.
+Qed.
+
 Section infty_nbhs_instances.
 Context {R : numFieldType}.
 Implicit Types r : R.
@@ -441,6 +488,20 @@ Unshelve. all: end_near. Qed.
 Lemma cvgNrNy f : (- f @ F --> -oo) <-> (f @ F --> +oo).
 Proof. by rewrite -cvgNry opprK. Qed.
 
+Lemma cvgryV f : f @ F --> +oo -> (f x)^-1 @[x --> F] --> (0 : R).
+Proof.
+move=> cvgy.
+apply: cvg_comp; first exact: cvgy.
+by rewrite pinftyV; exact: cvg_within.
+Qed.
+
+Lemma cvgrNyV f : f @ F --> -oo -> (f x)^-1 @[x --> F] --> (0 : R).
+Proof.
+move=> cvgNy.
+apply: cvg_comp; first exact: cvgNy.
+by rewrite ninftyV; exact: cvg_within.
+Qed.
+
 End cvg_infty_numField.
 
 Section cvg_infty_realField.
@@ -526,6 +587,31 @@ Proof. by move=> fy; under eq_fun do rewrite mulrC; exact: gt0_cvgMly. Qed.
 
 End gt0_cvg.
 
+Section lt0_cvg.
+Context {R : realFieldType} {F : set_system R} {FF : Filter F}.
+Variables (M : R) (f : R -> R).
+Hypothesis M0 : M < 0.
+
+Lemma lt0_cvgMlNy : (f r) @[r --> F] --> +oo -> (f r * M)%R @[r --> F] --> -oo.
+Proof.
+move=> /cvgryPge fy; apply/cvgrNyPle => A.
+by apply: filterS (fy (A / M)) => x; rewrite ler_ndivrMr.
+Qed.
+
+Lemma lt0_cvgMrNy : (f r) @[r --> F] --> +oo -> (M * f r)%R @[r --> F] --> -oo.
+Proof. by move=> fy; under eq_fun do rewrite mulrC; exact: lt0_cvgMlNy. Qed.
+
+Lemma lt0_cvgMly : f r @[r --> F] --> -oo -> (f r * M)%R @[r --> F] --> +oo.
+Proof.
+move=> /cvgrNyPle fNy; apply/cvgryPge => A.
+by apply: filterS (fNy (A / M)) => x; rewrite ler_ndivlMr.
+Qed.
+
+Lemma lt0_cvgMry : f r @[r --> F] --> -oo -> (M * f r)%R @[r --> F] --> +oo.
+Proof. by move=> fy; under eq_fun do rewrite mulrC; exact: lt0_cvgMly. Qed.
+
+End lt0_cvg.
+
 Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
     (l : set_system T) :
   f x @[x --> -oo] --> l <-> (f \o -%R) x @[x --> +oo] --> l.

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -691,6 +691,22 @@ Proof.
 by rewrite at_leftN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK.
 Qed.
 
+Lemma fmap_at_left0P {T : Type} {R : numFieldType} x (f : R -> T) : (f (x - e) @[e --> 0^'+]) = (f @ x^'-).
+Proof.
+rewrite -(subrr (-x)) at_right_shift at_rightN -fmap_comp.
+apply: near_eq_cvg_eq.
+apply: (nearW (F := x^'-)) => y /=.
+by rewrite opprB addNKr opprK.
+Qed.
+
+Lemma fmap_at_right0E {T : Type} {R : numFieldType} (x : R) (f : R -> T) : (f (x + e) @[e --> 0^'+]) = (f @ x^'+).
+Proof.
+rewrite -(subrr x) at_right_shift.
+apply: near_eq_cvg_eq.
+apply: (nearW (F := x^'+)) => y.
+by rewrite addrC subrK.
+Qed.
+
 Section at_left_right_pseudoMetricNormedZmod.
 Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R).
 

theories/normedtype_theory/tvs.v

@@ -647,6 +647,19 @@ Proof. exact/nbhsB_subproof/add_continuous. Qed.
 
 End ConvexTvs_numDomain.
 
+Lemma near_shiftE (R : numDomainType) (E : convexTvsType R) (U : set E) (x a : E) :
+  (\forall y \near x + a, U y) = (\near x, U (x + a)).
+Proof.
+eqProp; rewrite -!nbhs_nearE.
+- move/(nbhsB (-a)).
+  rewrite addrC addrK.
+  apply: filterS => _ [y Uy <-].
+  by rewrite addrC addNKr.
+- move/(nbhsB a); rewrite addrC.
+  apply: filterS => ? [y Uya <-].
+  by rewrite addrC.
+Qed.
+
 Section ConvexTvs_numField.
 
 Lemma nbhs0Z (R : numFieldType) (E : convexTvsType R) (U : set E) (r : R) :
@@ -667,6 +680,20 @@ near=> z; exists (r^-1 *: z); last by rewrite scalerA divff// scale1r.
 by apply: (BU (r^-1,z)); split; [exact: nbhs_singleton|near: z].
 Unshelve. all: by end_near. Qed.
 
+Lemma nearZE (R : numFieldType) (T : convexTvsType R) (c : R) (x : T) (P : set T) :
+  c != 0 -> (\forall y \near c *: x, P y) = (\near x, P (c *: x)).
+Proof.
+move=> c_neq0.
+have cinv_neq0 : c^-1 != 0 by apply: invr_neq0.
+eqProp.
+- move/(nbhsZ cinv_neq0).
+  rewrite scalerK//.
+  apply: filterS => ? [y Py <-].
+  by rewrite scalerKV.
+- move/(nbhsZ c_neq0).
+  by apply: filterS => ? [y Pcy <-].
+Qed.
+
 End ConvexTvs_numField.
 
 Section standard_topology.

theories/topology_theory/num_topology.v

@@ -464,6 +464,46 @@ move=> r/=; rewrite ltr_pdivlMr// -ltrBlDr; apply: le_lt_trans.
 by rewrite -lerBlDr opprK addrC (le_trans (ler_norm _))// ler_peMr// ler1n.
 Qed.
 
+Lemma near_right_in_itv (R : realFieldType) (a : R) (P : set R) : 
+  (\forall b \near a^'+, {in `]a, b[, forall x, P x}) 
+  <-> {near a^'+, forall x, P x}.
+Proof.
+split=> [[/= r r0 hr]|[/= r r0 hr]].
+- exists (r / 2) => [|x /= /ltr_distlCDr x_lt_aDr2 a_lt_x].
+    by apply: divr_gt0.
+  apply: (hr (a + r / 2)) => /=.
+  + rewrite opprD addNKr normrN gtr0_norm// ?divr_gt0//.
+    by rewrite gtr_pMr// invf_plt ?posrE// invr1 ltrDl.
+  + by rewrite ltrDl divr_gt0.
+  + by rewrite in_itv/= a_lt_x/=.
+- exists r => // x /= /ltr_distlCDr x_lt_aDr a_lt_x y.
+  rewrite in_itv/= => /andP[a_lt_y y_lt_x].
+  apply: hr => //=.
+  rewrite distrC gtr0_norm ?subr_gt0// ltrBlDl.
+  by apply: lt_trans x_lt_aDr.
+Qed.
+
+Lemma near_left_in_itv (R : realFieldType) (b : R) (P : set R) : 
+  (\forall a \near b^'-, {in `]a, b[, forall x, P x}) 
+  <-> {near b^'-, forall x, P x}.
+Proof.
+split=> [[/= r r0 hr]|[/= r r0 hr]].
+- exists (r / 2) => [|x /= /ltr_distlDr b_lt_xDr2 x_lt_b].
+    by apply: divr_gt0.
+  apply: (hr (b - r / 2)) => /=.
+  + rewrite subKr gtr0_norm ?divr_gt0//.
+    by rewrite gtr_pMr// invf_plt ?posrE// invr1 ltrDl.
+  + by rewrite gtrBl divr_gt0.
+  + by rewrite in_itv/= x_lt_b andbT ltrBlDr.
+- exists r => // x /= /ltr_distlDr b_lt_xDr x_lt_b y.
+  rewrite in_itv/= => /andP[x_lt_y y_lt_b].
+  apply: hr => //=.
+  rewrite gtr0_norm ?subr_gt0//.
+  rewrite ltrBlDl.
+  apply: (lt_trans b_lt_xDr).
+  by rewrite ltrD2r.
+Qed.
+
 Section nbhs_lt_le.
 Context {R : numFieldType}.
 Implicit Types x z : R.