diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0023dbb5e0..320ccb093a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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`: diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 31c99d1a4f..c57a771abc 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/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. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index ae89f7d3ed..9f945624de 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/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). diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v index 01b1a30262..d9477e84cb 100644 --- a/theories/topology_theory/metric_structure.v +++ b/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}.