normed type neighborhood lemmas

CHANGELOG_UNRELEASED.md

@@ -126,6 +126,8 @@
 
 - in `filter.v`:
   + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType`
+  + new lemmas `near_eq_cvgE`, `near_eq_is_cvg`, `near_eq_lim`, 
+    `cvg_to_eq`, `cvg_to_withinP`, and `within_cvg_to_within`.
 
 - in `topology_structure.v`:
   + structure `SubTopological`, notation `subTopologicalType`
@@ -234,6 +236,22 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
+- in file `function_spaces.v`,
+  + new lemma `within_continuous_big`.
+- in file `nat_topology.v`,
+  + new lemma `near_infty_after`.
+- in file `num_topology.v`,
+  + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, 
+    `at_left_shift`, `at_right_shift`, `near_right_in_itv`, and `near_left_in_itv`.
+
+- in file `num_normedtype.v`,
+  + new lemmas `pinftyV`, `ninftyV`, `cvgryV`, `cvgrNyV`, `lt0_cvgMlNy`, 
+    `lt0_cvgMrNy`, `lt0_cvgMly`, and `lt0_cvgMry`.
+- in file `pseudometric_normed_Zmodule.v`,
+  + new lemmas `fmap_at_left0P`, and `fmap_at_right0E`.
+- in file `tvs.v`,
+  + new lemmas `near_shiftE`, and `nearZE`.
+
 ### Changed
 
 - in `realsum.v`:
@@ -354,6 +372,9 @@
 - in `classical_sets.v`
   + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`)
 
+- moved from `metric_structure.v` to `num_topology.v`: 
+  + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`.
+
 ### Renamed
 
 - in `tvs.v`:

classical/filter.v

@@ -925,10 +925,23 @@ Lemma near_eq_cvg {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) :
   {near F, f =1 g} -> g @ F `=>` f @ F.
 Proof. by move=> eq_fg P /=; apply: filterS2 eq_fg => x /= <-. Qed.
 
+Lemma near_eq_cvgE {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) :
+  {near F, f =1 g} -> f @ F = g @ F.
+Proof.
+move=> eq_fg.
+apply/seteqP; split; apply: near_eq_cvg => //.
+by near do symmetry.
+Unshelve. all: by end_near.
+Qed.
+
 Lemma eq_cvg (T T' : Type) (F : set_system T) (f g : T -> T') (x : set_system T') :
   f =1 g -> (f @ F --> x) = (g @ F --> x).
 Proof. by move=> /funext->. Qed.
 
+Lemma near_eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') : 
+  Filter F -> {near F, g =1 f} -> cvg (f x @[x --> F]) -> cvg(g x @[x --> F]).
+Proof. by move=> /@near_eq_cvgE /[apply] ->. Qed.
+
 Lemma eq_is_cvg_in (T T' : Type) (fT : pfilteredType T') (F : set_system T) (f g : T -> T') :
   f =1 g -> [cvg (f @ F) in fT] = [cvg (g @ F) in fT].
 Proof. by move=> /funext->. Qed.
@@ -937,6 +950,14 @@ Lemma eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') :
   f =1 g -> cvg (f @ F) = cvg (g @ F).
 Proof. by move=> /funext->. Qed.
 
+Lemma near_eq_lim (T : Type) (T' : pnbhsType) {F : set_system T} {FF : Filter F} (f g : T -> T') :
+  {near F, f =1 g} -> lim (f @ F) = lim (g @ F).
+Proof. by move=> /near_eq_cvgE ->. Qed.
+
+Lemma cvg_to_eq {T : nbhsType} {F : set_system T} (l l' : T) :
+  F --> l' -> l = l' -> F --> l.
+Proof. by move=> + ->. Qed.
+
 Lemma neari_eq_loc {T U} {F : set_system T} {FF : Filter F} (f g : T -> set U) :
   {near F, f =2 g} -> g `@ F `=>` f `@ F.
 Proof.
@@ -1197,6 +1218,25 @@ Qed.
 
 End within.
 
+Lemma cvg_to_withinP (T U : Type) {F : set_system T} {FF : Filter F} {G : set_system U} {FG : Filter G} 
+    (f : T -> U) (A : set U) :
+  (f @ F --> within A G) <-> (f @ F --> G /\ \forall x \near F, A (f x)).
+Proof.
+split.
+  move=> cvg_w; split.
+  - apply: (cvg_trans cvg_w).
+    exact: cvg_within.
+  - apply: cvg_w.
+    exact: withinT.
+move=> [cvgT nearfA] P. 
+rewrite !nbhs_nearE near_withinE.
+move: cvgT => /[apply].
+rewrite near_map appfilter nbhs_nearE => nearF_AP.
+near=> x.
+suff : A (f x) by near: x.
+by near: x.
+Unshelve. all: by end_near. Qed.
+
 Global Instance within_filter T D F : Filter F -> Filter (@within T D F).
 Proof.
 move=> FF; rewrite /within; constructor => /=.
@@ -1210,6 +1250,18 @@ Qed.
 Canonical within_filter_on T D (F : filter_on T) :=
   FilterType (within D F) (within_filter _ _).
 
+Lemma within_cvg_to_within (T U : Type) {F : set_system T} {FF : Filter F} {G : set_system U} {FG : Filter G}
+    (f : T -> U) (A : set T) (B : set U) :
+  (\forall x \near F, A x -> B (f x)) -> f @ F --> G -> f @ within A F --> within B G.
+Proof.
+move=> near_hom cvgT.
+apply/cvg_to_withinP; split.
+- apply: cvg_trans cvgT.
+  apply: cvg_app.
+  exact: cvg_within.
+- by rewrite near_withinE.
+Qed. 
+
 Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T)
   (F : set_system T) (P : set T) :
   Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) ->

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

@@ -628,6 +628,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_cvgE.
+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_cvgE.
+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/function_spaces.v

@@ -1600,6 +1600,11 @@ Proof.
 by move=> F_cont x; apply: cvg_big => // i /F_cont; exact.
 Qed.
 
+Lemma within_continuous_big (T : topologicalType) (A : set T) (r : seq I) (F : I -> T -> U) :
+	(forall (i : I), P i -> {within A, continuous (F i)}) ->
+	{within A, continuous (fun x : T => \big[op/x0]_(i <- r | P i) F i x)}.
+Proof. by move=> cont_F x; apply: continuous_big. Qed.
+
 End big_continuous.
 
 Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y :=

theories/topology_theory/metric_structure.v

@@ -315,33 +315,6 @@ 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.
-
 Section at_left_rightR.
 Variable (R : numFieldType).
 

theories/topology_theory/nat_topology.v

@@ -93,6 +93,18 @@ Lemma near_inftyS (P : set nat) :
   (\forall x \near \oo, P (S x)) -> (\forall x \near \oo, P x).
 Proof. case=> N _ NPS; exists (S N) => // [[]]; rewrite /= ?ltn0 //. Qed.
 
+Lemma near_infty_after (P : set nat) :
+  (\forall n \near \oo, P n) <-> (\forall N \near \oo, forall n, (n >= N)%N -> P n).
+Proof.
+split.
+- move=> [N _ afterN].
+  exists N => // n /= /[swap] n' /leq_trans /[apply].
+  exact: afterN.
+- move=> [N _ afterN].
+  exists N => // n /=.
+  by apply: afterN => /=.
+Qed.  
+
 Section infty_nat.
 Local Open Scope nat_scope.