mv sequeeze for R earlier

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -226,6 +226,13 @@
     `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`,
     `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule`
 
+- moved from `normed_module.v` to `metric_structure.v`
+  + lemma `squeeze_cvgr`
+
+- moved from `pseudometric_normed_Zmodule.v` to `metric_structure.v`
+  + lemmas `real_cvgr_lt`, `real_cvgr_le`, `real_cvgr_le`, `real_cvgr_gt`
+  + lemmas `cvgr_lt`, `cvgr_gt`, `cvgr_ge`, `cvgr_le`
+
 ### Renamed
 
 - in `tvs.v`:

theories/normedtype_theory/normed_module.v

@@ -1307,16 +1307,6 @@ Section FilterRealType.
 Context {T : Type} {a : set_system T} {Fa : Filter a} {R : realFieldType}.
 Implicit Types f g h : T -> R.
 
-Lemma squeeze_cvgr f h g : (\near a, f a <= g a <= h a) ->
-  forall (l : R), f @ a --> l -> h @ a --> l -> g @ a --> l.
-Proof.
-move=> fgh l lfa lga; apply/cvgrPdist_lt => e e_gt0.
-near=> x; have /(_ _)/andP[//|fg gh] := near fgh x.
-rewrite distrC ltr_distl (lt_le_trans _ fg) ?(le_lt_trans gh)//=.
-  by near: x; apply: (cvgr_gt l); rewrite // gtrDl oppr_lt0.
-by near: x; apply: (cvgr_lt l); rewrite // ltrDl.
-Unshelve. all: end_near. Qed.
-
 Lemma ger_cvgy f g : (\near a, f a <= g a) ->
   f @ a --> +oo -> g @ a --> +oo.
 Proof.

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -905,49 +905,6 @@ Arguments cvgr_norm_ley {R V I F FF}.
 Arguments cvgr_norm_gtNy {R V I F FF}.
 Arguments cvgr_norm_geNy {R V I F FF}.
 
-Section at_left_rightR.
-Variable (R : numFieldType).
-
-Lemma real_cvgr_lt {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) :
-    y \is Num.real -> f @ F --> y ->
-  forall z, z > y -> \forall t \near F, f t \is Num.real -> f t < z.
-Proof.
-move=> yr Fy z zy; near=> x => fxr.
-rewrite -(ltrD2r (- y)) real_ltr_normlW// ?rpredB//.
-by near: x; apply: (@cvgr_distC_lt R R^o) => //; rewrite subr_gt0.
-Unshelve. all: by end_near. Qed.
-
-Lemma real_cvgr_le {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) :
-    y \is Num.real ->  f @ F --> y ->
-  forall z, z > y -> \forall t \near F, f t \is Num.real -> f t <= z.
-Proof.
-move=> /real_cvgr_lt/[apply] + ? z0 => /(_ _ z0).
-by apply: filterS => ? /[apply]/ltW.
-Qed.
-
-Lemma real_cvgr_gt {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) :
-    y \is Num.real -> f @ F --> y ->
-  forall z, y > z -> \forall t \near F, f t \is Num.real -> f t > z.
-Proof.
-move=> yr Fy z zy; near=> x => fxr.
-rewrite -ltrN2 -(ltrD2l y) real_ltr_normlW// ?rpredB//.
-by near: x; apply: (@cvgr_dist_lt _ R^o) => //; rewrite subr_gt0.
-Unshelve. all: by end_near. Qed.
-
-Lemma real_cvgr_ge {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) :
-    y \is Num.real -> f @ F --> y ->
-  forall z, z < y -> \forall t \near F, f t \is Num.real -> f t >= z.
-Proof.
-move=> /real_cvgr_gt/[apply] + ? z0 => /(_ _ z0).
-by apply: filterS => ? /[apply]/ltW.
-Qed.
-
-End at_left_rightR.
-Arguments real_cvgr_le {R T F FF f}.
-Arguments real_cvgr_lt {R T F FF f}.
-Arguments real_cvgr_ge {R T F FF f}.
-Arguments real_cvgr_gt {R T F FF f}.
-
 Section realFieldType.
 Context (R : realFieldType).
 
@@ -958,37 +915,7 @@ rewrite (@nbhsr0P _ R^o) -propeqE; apply: eq_near => y /=.
 by rewrite -propeqE; apply: eq_forall => z; rewrite ler_distlC.
 Qed.
 
-Lemma cvgr_lt {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) :
-  f @ F --> y -> forall z, z > y -> \forall t \near F, f t < z.
-Proof.
-move=> Fy z zy; near=> x; rewrite -(ltrD2r (- y)) ltr_normlW//.
-by near: x; apply: (@cvgr_distC_lt _ R^o) => //; rewrite subr_gt0.
-Unshelve. all: by end_near. Qed.
-
-Lemma cvgr_le {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) :
-  f @ F --> y -> forall z, z > y -> \forall t \near F, f t <= z.
-Proof.
-by move=> /cvgr_lt + ? z0 => /(_ _ z0); apply: filterS => ?; apply/ltW.
-Qed.
-
-Lemma cvgr_gt {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) :
-  f @ F --> y -> forall z, y > z -> \forall t \near F, f t > z.
-Proof.
-move=> Fy z zy; near=> x; rewrite -ltrN2 -(ltrD2l y) ltr_normlW//.
-by near: x; apply: (@cvgr_dist_lt _ R^o) => //; rewrite subr_gt0.
-Unshelve. all: by end_near. Qed.
-
-Lemma cvgr_ge {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) :
-  f @ F --> y -> forall z, z < y -> \forall t \near F, f t >= z.
-Proof.
-by move=> /cvgr_gt + ? z0 => /(_ _ z0); apply: filterS => ?; apply/ltW.
-Qed.
-
 End realFieldType.
-Arguments cvgr_le {R T F FF f}.
-Arguments cvgr_lt {R T F FF f}.
-Arguments cvgr_ge {R T F FF f}.
-Arguments cvgr_gt {R T F FF f}.
 
 Module Export NbhsNorm.
 Definition nbhs_simpl := (nbhs_simpl,@nbhs_nbhs_norm,@filter_from_norm_nbhs).

theories/topology_theory/metric_structure.v

@@ -341,3 +341,106 @@ rewrite neq_lt => /orP[tp|pt].
 Unshelve. all: by end_near. Qed.
 
 End cvg_at_right_left_dnbhs.
+
+Section at_left_rightR.
+Variable (R : numFieldType).
+
+(**md `cvgrPdistC_lt` is also defined in `pseudometric_normed_Zmodule.v` where it only needs `numDomainType` *)
+Let cvgrPdistC_lt {T} {F : set_system T} {FF : Filter F} (f : T -> R^o) (y : R) :
+  f @ F --> y <-> forall eps, 0 < eps -> \forall t \near F, mdist (f t) y < eps.
+Proof.
+rewrite metricType_numDomainType.cvgrPdist_lt.
+by under eq_forall do under eq_near do rewrite /mdist/= (@distrC _ R^o).
+Qed.
+
+(**md `cvgr_distC_lt` is also defined in `pseudometric_normed_Zmodule.v` where it only needs `numDomainType` *)
+Let cvgr_distC_lt {T} {F : set_system T} {FF : Filter F} (f : T -> R^o) (y : R) :
+  f @ F --> y -> forall eps, eps > 0 -> \forall t \near F, mdist (f t) y < eps.
+Proof. by move=> /cvgrPdistC_lt. Qed.
+
+Lemma real_cvgr_lt {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) :
+    y \is Num.real -> f @ F --> y ->
+  forall z, z > y -> \forall t \near F, f t \is Num.real -> f t < z.
+Proof.
+move=> yr Fy z zy; near=> x => fxr.
+rewrite -(ltrD2r (- y)) real_ltr_normlW// ?rpredB// distrC.
+by near: x; apply: cvgr_distC_lt => //; rewrite subr_gt0.
+Unshelve. all: by end_near. Qed.
+
+Lemma real_cvgr_le {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) :
+    y \is Num.real ->  f @ F --> y ->
+  forall z, z > y -> \forall t \near F, f t \is Num.real -> f t <= z.
+Proof.
+move=> /real_cvgr_lt/[apply] + ? z0 => /(_ _ z0).
+by apply: filterS => ? /[apply]/ltW.
+Qed.
+
+Lemma real_cvgr_gt {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) :
+    y \is Num.real -> f @ F --> y ->
+  forall z, y > z -> \forall t \near F, f t \is Num.real -> f t > z.
+Proof.
+move=> yr Fy z zy; near=> x => fxr.
+rewrite -ltrN2 -(ltrD2l y) real_ltr_normlW// ?rpredB// distrC.
+by near: x; apply: (@metricType_numDomainType.cvgr_dist_lt _ R^o) => //; rewrite subr_gt0.
+Unshelve. all: by end_near. Qed.
+
+Lemma real_cvgr_ge {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) :
+    y \is Num.real -> f @ F --> y ->
+  forall z, z < y -> \forall t \near F, f t \is Num.real -> f t >= z.
+Proof.
+move=> /real_cvgr_gt/[apply] + ? z0 => /(_ _ z0).
+by apply: filterS => ? /[apply]/ltW.
+Qed.
+
+End at_left_rightR.
+Arguments real_cvgr_le {R T F FF f}.
+Arguments real_cvgr_lt {R T F FF f}.
+Arguments real_cvgr_ge {R T F FF f}.
+Arguments real_cvgr_gt {R T F FF f}.
+
+Section squeeze_cvgr.
+Context {T : Type} {F : set_system T} {FF : Filter F} {R : realFieldType}.
+Implicit Types f g h : T -> R.
+
+Lemma cvgr_lt f (y : R) :
+  f @ F --> y -> forall z, z > y -> \forall t \near F, f t < z.
+Proof.
+move=> Fy z zy; near=> x; rewrite -(ltrD2r (- y)) ltr_normlW//.
+by near: x; apply: (@metricType_numDomainType.cvgr_dist_lt _ R^o) => //; rewrite subr_gt0.
+Unshelve. all: by end_near. Qed.
+
+Lemma cvgr_gt f (y : R) :
+  f @ F --> y -> forall z, y > z -> \forall t \near F, f t > z.
+Proof.
+move=> Fy z zy; near=> x; rewrite -ltrN2 -(ltrD2l y) ltr_normlW// distrC.
+by near: x; apply: (@metricType_numDomainType.cvgr_dist_lt _ R^o) => //; rewrite subr_gt0.
+Unshelve. all: by end_near. Qed.
+
+Lemma cvgr_le f (y : R) :
+  f @ F --> y -> forall z, z > y -> \forall t \near F, f t <= z.
+Proof.
+by move=> /cvgr_lt + ? z0 => /(_ _ z0); apply: filterS => ?; apply/ltW.
+Qed.
+
+Lemma cvgr_ge f (y : R) :
+  f @ F --> y -> forall z, z < y -> \forall t \near F, f t >= z.
+Proof.
+by move=> /cvgr_gt + ? z0 => /(_ _ z0); apply: filterS => ?; apply/ltW.
+Qed.
+
+Lemma squeeze_cvgr f h g : (\near F, f F <= g F <= h F) ->
+  forall (l : R), f @ F --> l -> h @ F --> l -> g @ F --> l.
+Proof.
+move=> fgh l lfa lga.
+apply/(@metricType_numDomainType.cvgrPdist_lt R R^o) => e e_gt0.
+near=> x; have /(_ _)/andP[//|fg gh] := near fgh x.
+rewrite ltr_distl (lt_le_trans _ fg) ?(le_lt_trans gh)//=.
+  by near: x; apply: (cvgr_gt lfa); rewrite // gtrDl oppr_lt0.
+by near: x; apply: (cvgr_lt lga); rewrite // ltrDl.
+Unshelve. all: end_near. Qed.
+
+End squeeze_cvgr.
+Arguments cvgr_lt {T F FF R f}.
+Arguments cvgr_gt {T F FF R f}.
+Arguments cvgr_le {T F FF R f}.
+Arguments cvgr_ge {T F FF R f}.