diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5029a574c..c438ff7e7 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,8 +4,32 @@ ### Added +- new file `metric_structure.v`: + + mixin `isMetric`, structure `Metric`, type `metricType` + * with fields `mdist`, `mdist_ge0`, `mdist_positivity`, `ballEmdist` + + lemmas `metric_sym`, `mdistxx`, `mdist_gt0`, `metric_triangle`, + `metric_hausdorff` + + `R^o` declared to be an instance of `metricType` + + module `metricType_numDomainType` + + lemmas `ball_mdistE`, `nbhs_nbhs_mdist`, `nbhs_mdistP` + +- in `pseudometric_normed_Zmodule.v`: + + factory `NormedZmoduleMetric` with field `mdist_norm` + ### Changed +- moved from `pseudometric_normed_Zmodule.v` to `num_topology.v`: + + notations `^'+`, `^'-` + + definitions `at_left`, `at_right` + + instances `at_right_proper_filter`, `at_left_proper_filter` + + lemmas `nbhs_right_gt`, `nbhs_left_lt`, `nbhs_right_neq`, `nbhs_left_neq`, + `nbhs_left_neq`, `nbhs_left_le`, `nbhs_right_lt`, `nbhs_right_ltW`, + `nbhs_right_ltDr`, `nbhs_right_le`, `not_near_at_rightP` + +- moved from `realfun.v` to `metric_structure.v` and generalized: + + lemma `cvg_nbhsP` + + ### Renamed - in `lebesgue_stieltjes_measure.v`: diff --git a/_CoqProject b/_CoqProject index 4bd2a3f29..b07a5d56b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -64,6 +64,7 @@ theories/topology_theory/one_point_compactification.v theories/topology_theory/sigT_topology.v theories/topology_theory/discrete_topology.v theories/topology_theory/separation_axioms.v +theories/topology_theory/metric_structure.v theories/homotopy_theory/homotopy.v theories/homotopy_theory/wedge_sigT.v diff --git a/theories/Make b/theories/Make index c9088359b..205692dea 100644 --- a/theories/Make +++ b/theories/Make @@ -30,6 +30,7 @@ topology_theory/one_point_compactification.v topology_theory/sigT_topology.v topology_theory/discrete_topology.v topology_theory/separation_axioms.v +topology_theory/metric_structure.v homotopy_theory/homotopy.v homotopy_theory/wedge_sigT.v diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_under.v b/theories/lebesgue_integral_theory/lebesgue_integral_under.v index 2ceb1e5df..eb08f5233 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_under.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_under.v @@ -63,7 +63,7 @@ have BZ_cf x : x \in B `\` Z -> continuous (f ^~ x). by rewrite inE/= => -[Bx nZx]; exact: ncfZ. have [vu|uv] := lerP v u. by move: Ia; rewrite /I set_itv_ge// -leNgt bnd_simp. -apply/cvg_nbhsP => w wa. +apply/(@cvg_nbhsP _ R^o) => w wa. have /near_in_itvoo[e /= e0 aeuv] : a \in `]u, v[ by rewrite inE. move/cvgrPdist_lt : (wa) => /(_ _ e0)[N _ aue]. have IwnN n : I (w (n + N)) by apply: aeuv; apply: aue; exact: leq_addl. @@ -114,7 +114,7 @@ apply: (@dominated_cvg _ _ _ mu _ _ have : x \in B `\` Z. move: BZUUx; rewrite inE/= => -[Bx nZUUx]; rewrite inE/=; split => //. by apply: contra_not nZUUx; left. - by move/(BZ_cf x)/(_ a)/cvg_nbhsP; apply; rewrite (cvg_shiftn N). + by move/(BZ_cf x)/(_ a)/(@cvg_nbhsP _ R^o); apply; rewrite (cvg_shiftn N). - by apply: (integrableS mB) => //; exact: measurableD. - move=> n x [Bx ZUUx]; rewrite lee_fin. move/subsetCPl : (Ug_ub n); apply => //=. @@ -125,7 +125,8 @@ End continuity_under_integral. Section differentiation_under_integral. -Definition partial1of2 {R : realType} {T : Type} (f : R -> T -> R) : R -> T -> R := fun x y => (f ^~ y)^`() x. +Definition partial1of2 {R : realType} {T : Type} (f : R -> T -> R) : R -> T -> R := + fun x y => (f ^~ y)^`() x. Local Notation "'d1 f" := (partial1of2 f). diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 48005b39b..ed23f7808 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -32,9 +32,11 @@ From mathcomp Require Import tvs num_normedtype. (* *) (* ## Normed topological abelian groups *) (* ``` *) -(* pseudoMetricNormedZmodType R == interface type for a normed topological *) -(* abelian group equipped with a norm *) -(* The HB class is PseudoMetricNormedZmod. *) +(* pseudoMetricNormedZmodType R == interface type for a normed topological *) +(* abelian group equipped with a norm *) +(* The HB class is PseudoMetricNormedZmod. *) +(* NormedZmoduleMetric == factory for pseudoMetricNormedZmodType *) +(* based on metric structures *) (* ``` *) (* *) (* ## Closed balls *) @@ -61,8 +63,6 @@ From mathcomp Require Import tvs num_normedtype. (* *) (******************************************************************************) -Reserved Notation "x ^'+" (at level 3, left associativity, format "x ^'+"). -Reserved Notation "x ^'-" (at level 3, left associativity, format "x ^'-"). Reserved Notation "[ 'bounded' E | x 'in' A ]" (at level 0, x name, format "[ 'bounded' E | x 'in' A ]"). @@ -99,97 +99,6 @@ End Shift. Arguments shift {R} x / y. Notation center c := (shift (- c)). -Section at_left_right. -Variable R : numFieldType. - -Definition at_left (x : R) := within (fun u => u < x) (nbhs x). -Definition at_right (x : R) := within (fun u => x < u) (nbhs x). -Local Notation "x ^'-" := (at_left x) : classical_set_scope. -Local Notation "x ^'+" := (at_right x) : classical_set_scope. - -Global Instance at_right_proper_filter (x : R) : ProperFilter x^'+. -Proof. -apply: Build_ProperFilter => -[_/posnumP[d] /(_ (x + d%:num / 2))]. -apply; last by rewrite ltrDl. -by rewrite /= opprD addNKr normrN ger0_norm// gtr_pMr// invf_lt1// ltr1n. -Qed. - -Global Instance at_left_proper_filter (x : R) : ProperFilter x^'-. -Proof. -apply: Build_ProperFilter => -[_ /posnumP[d] /(_ (x - d%:num / 2))]. -apply; last by rewrite gtrBl. -by rewrite /= opprB addrC subrK ger0_norm// gtr_pMr// invf_lt1// ltr1n. -Qed. - -Lemma nbhs_right_gt x : \forall y \near x^'+, x < y. -Proof. by rewrite near_withinE; apply: nearW. Qed. - -Lemma nbhs_left_lt x : \forall y \near x^'-, y < x. -Proof. by rewrite near_withinE; apply: nearW. Qed. - -Lemma nbhs_right_neq x : \forall y \near x^'+, y != x. -Proof. by rewrite near_withinE; apply: nearW => ? /gt_eqF->. Qed. - -Lemma nbhs_left_neq x : \forall y \near x^'-, y != x. -Proof. by rewrite near_withinE; apply: nearW => ? /lt_eqF->. Qed. - -Lemma nbhs_right_ge x : \forall y \near x^'+, x <= y. -Proof. by rewrite near_withinE; apply: nearW; apply/ltW. Qed. - -Lemma nbhs_left_le x : \forall y \near x^'-, y <= x. -Proof. by rewrite near_withinE; apply: nearW => ?; apply/ltW. Qed. - -Lemma nbhs_right_lt x z : x < z -> \forall y \near x^'+, y < z. -Proof. -move=> xz; exists (z - x) => //=; first by rewrite subr_gt0. -by move=> y /= + xy; rewrite distrC ?ger0_norm ?subr_ge0 1?ltW// ltrD2r. -Qed. - -Lemma nbhs_right_ltW x z : x < z -> \forall y \near nbhs x^'+, y <= z. -Proof. -by move=> xz; near=> y; apply/ltW; near: y; exact: nbhs_right_lt. -Unshelve. all: by end_near. Qed. - -Lemma nbhs_right_ltDr x e : 0 < e -> \forall y \near x ^'+, y - x < e. -Proof. -move=> e0; near=> y; rewrite ltrBlDr; near: y. -by apply: nbhs_right_lt; rewrite ltrDr. -Unshelve. all: by end_near. Qed. - -Lemma nbhs_right_le x z : x < z -> \forall y \near x^'+, y <= z. -Proof. by move=> xz; near do apply/ltW; apply: nbhs_right_lt. -Unshelve. all: by end_near. Qed. - -(* NB: In not_near_at_rightP (and not_near_at_rightP), R has type numFieldType. - It is possible realDomainType could make the proof simpler and at least as - useful. *) -Lemma not_near_at_rightP (p : R) (P : pred R) : - ~ (\forall x \near p^'+, P x) <-> - forall e : {posnum R}, exists2 x, p < x < p + e%:num & ~ P x. -Proof. -split=> [pPf e|ex_notPx]. -- apply: contrapT => /forallPNP peP; apply: pPf; near=> t. - apply: contrapT; apply: peP; apply/andP; split. - + by near: t; exact: nbhs_right_gt. - + by near: t; apply: nbhs_right_lt; rewrite ltrDl. -- rewrite /at_right near_withinE nearE. - rewrite -filter_from_ballE /filter_from/= -forallPNP => _ /posnumP[d]. - have [x /andP[px xpd] notPx] := ex_notPx d; rewrite -existsNP; exists x => /=. - apply: contra_not notPx; apply => //. - by rewrite /ball/= ltr0_norm ?subr_lt0// opprB ltrBlDl. -Unshelve. all: by end_near. Qed. - -End at_left_right. -#[global] Typeclasses Opaque at_left at_right. -Notation "x ^'-" := (at_left x) : classical_set_scope. -Notation "x ^'+" := (at_right x) : classical_set_scope. - -#[global] Hint Extern 0 (Filter (nbhs _^'+)) => - (apply: at_right_proper_filter) : typeclass_instances. - -#[global] Hint Extern 0 (Filter (nbhs _^'-)) => - (apply: at_left_proper_filter) : typeclass_instances. - Section at_left_right_topologicalType. Variables (R : numFieldType) (V : topologicalType) (f : R -> V) (x : R). @@ -227,6 +136,25 @@ HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) := {T of Num.NormedZmodule R T & PseudoMetric R T & NormedZmod_PseudoMetric_eq R T & isPointed T}. +(* alternative definition of a PseudoMetricNormedZmod *) +HB.factory Record NormedZmoduleMetric (R : numDomainType) T + of Num.NormedZmodule R T & Metric R T & isPointed T := { + mdist_norm : forall x y : T, mdist x y = `|y - x| +}. + +HB.builders Context (R : numDomainType) T of NormedZmoduleMetric R T. + +Let pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |). +Proof. +apply/funext => /= t; apply/funext => d; rewrite ballEmdist. +by apply/seteqP; split => [y|y]/=; rewrite mdist_norm distrC. +Qed. + +HB.instance Definition _ := + NormedZmod_PseudoMetric_eq.Build R T pseudo_metric_ball_norm. + +HB.end. + Section pseudoMetricNormedZmod_numDomainType. Context {K : numDomainType} {V : pseudoMetricNormedZmodType K}. diff --git a/theories/realfun.v b/theories/realfun.v index 9051299ac..ebf350f57 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -232,37 +232,6 @@ apply: cvg_at_right_left_dnbhs. - by apply/cvg_at_leftP => u [pu ?]; apply: pfl; split => // n; rewrite lt_eqF. Unshelve. all: end_near. Qed. -Lemma cvg_nbhsP f p l : f x @[x --> p] --> l <-> - (forall u : R^nat, (u n @[n --> \oo] --> p) -> f (u n) @[n --> \oo] --> l). -Proof. -split=> [/cvgrPdist_le /= fpl u /cvgrPdist_lt /= uyp|pfl]. - apply/cvgrPdist_le => e /fpl[d d0 pdf]. - by apply: filterS (uyp d d0) => t /pdf. -apply: contrapT => fpl; move: pfl; apply/existsNP. -suff: exists2 x : R ^nat, - x n @[n --> \oo] --> p & ~ f (x n) @[n --> \oo] --> l. - by move=> [x_] hp; exists x_; exact/not_implyP. -have [e He] : exists e : {posnum R}, forall d : {posnum R}, - exists xn, `|xn - p| < d%:num /\ `|f xn - l| >= e%:num. - apply: contrapT; apply: contra_not fpl => /forallNP h. - apply/cvgrPdist_le => e e0; have /existsNP[d] := h (PosNum e0). - move/forallNP => {}h; near=> t. - have /not_andP[abs|/negP] := h t. - - exfalso; apply: abs. - by near: t; exists d%:num => //= z/=; rewrite distrC. - - by rewrite -ltNge distrC => /ltW. -have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0. -exists (fun n => sval (cid (He (PosNum (invn n))))). - apply/cvgrPdist_lt => r r0; near=> t. - rewrite /sval/=; case: cid => x [xpt _]. - rewrite distrC (lt_le_trans xpt)// -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0//. - near: t; exists (trunc r^-1) => // s /= rs. - by rewrite (le_trans (ltW (truncnS_gt _)))// ler_nat. -move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)). -rewrite /sval/=; case: cid => // x [px xpn]. -by rewrite ltNge distrC => /negP. -Unshelve. all: end_near. Qed. - End cvgr_fun_cvg_seq. Section cvge_fun_cvg_seq. diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v new file mode 100644 index 000000000..6473266ea --- /dev/null +++ b/theories/topology_theory/metric_structure.v @@ -0,0 +1,266 @@ +(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. +From mathcomp Require Import rat interval zmodp vector fieldext falgebra. +From mathcomp Require Import archimedean finmap. +From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. +From mathcomp Require Import interval_inference reals topology_structure. +From mathcomp Require Import uniform_structure pseudometric_structure. +From mathcomp Require Import num_topology product_topology separation_axioms. + +(**md**************************************************************************) +(* # Metric spaces *) +(* *) +(* ``` *) +(* metricType K == metric structure with distance mdist *) +(* The mixin is defined by extending PseudoMetric. *) +(* The HB class is Metric. *) +(* R^o with R : numFieldType is shown to be a metric space. *) +(* ``` *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +HB.mixin Record isMetric (K : numDomainType) M of PseudoMetric K M := { + mdist : M -> M -> K ; + mdist_ge0 : forall x y, 0 <= mdist x y ; + mdist_positivity : forall x y, mdist x y = 0 -> x = y; + ballEmdist : forall x d, ball x d = [set y | mdist x y < d] +}. + +#[short(type="metricType")] +HB.structure Definition Metric (K : numDomainType) := + { M of PseudoMetric K M & isMetric K M }. + +Section metric_lemmas. +Context {R : realFieldType} (T : metricType R). + +Let dist := @mdist R T. + +Lemma metric_sym x y : dist x y = dist y x. +Proof. +apply/eqP; rewrite eq_le; apply/andP; split; rewrite leNgt; apply/negP => xy. +- have := @ball_sym _ _ y x (dist x y); rewrite !ballEmdist/= => /(_ xy). + by rewrite ltxx. +- have := @ball_sym _ _ x y (dist y x); rewrite !ballEmdist/= => /(_ xy). + by rewrite ltxx. +Qed. + +Lemma mdistxx x : dist x x = 0. +Proof. +apply/eqP; rewrite eq_le mdist_ge0 andbT; apply/ler_addgt0Pl => /= e e0. +rewrite addr0 leNgt; apply/negP => exx. +by have := @ball_center _ _ x (PosNum e0); rewrite ballEmdist/= ltNge (ltW exx). +Qed. + +Lemma mdist_gt0 x y : (0 < dist x y) = (x != y). +Proof. +rewrite lt_neqAle mdist_ge0 andbT. +apply/negPn/negPn => [/eqP/esym/mdist_positivity/eqP//|/eqP ->]. +by rewrite mdistxx. +Qed. + +Lemma metric_triangle x y z : dist x z <= dist x y + dist y z. +Proof. +apply/ler_addgt0Pl => /= e e0; rewrite leNgt; apply/negP => xyz. +have := @ball_triangle _ _ y x z (dist x y + e / 2) (dist y z + e / 2). +rewrite !ballEmdist/= addrACA -splitr !ltrDl !divr_gt0// => /(_ isT isT). +by rewrite ltNge => /negP; apply; rewrite addrC ltW. +Qed. + +Lemma metric_hausdorff : hausdorff_space T. +Proof. +move=> p q pq; apply: contrapT => qp; move: pq. +pose D := dist p q / 2; have D0 : 0 < D. + by rewrite divr_gt0// mdist_gt0; exact/eqP. +have p2Dq : ~ ball p (dist p q) q by rewrite ballEmdist/= ltxx. +move=> /(_ (ball p _) (ball q _) (nbhsx_ballx _ _ D0) (nbhsx_ballx _ _ D0)). +move/set0P/eqP; apply; rewrite -subset0 => x [pDx /ball_sym qDx]. +by have := ball_triangle pDx qDx; rewrite -splitr. +Qed. + +End metric_lemmas. + +Section numFieldType_metric. +Context {R : numFieldType}. +Implicit Type x y : R. + +Let dist x y := `|y - x|. + +Let dist_ge0 x y : 0 <= dist x y. +Proof. exact: normr_ge0. Qed. + +Let dist_positivity x y : dist x y = 0 -> x = y. +Proof. by move/normr0_eq0/eqP; rewrite subr_eq0 => /eqP. Qed. + +Let ballEmdist x d : ball x d = [set y | dist x y < d]. +Proof. by apply/seteqP; split => [|]/= A; rewrite /ball/= distrC. Qed. + +HB.instance Definition _ := + @isMetric.Build R R^o dist dist_ge0 dist_positivity ballEmdist. + +End numFieldType_metric. + +Module metricType_numDomainType. +(* tentative generalization of the section +pseudoMetricNormedZmod_numDomainType +from pseudoMetricNormedZmod +to +metricType *) +Section metricType_numDomainType. +Context {K : numDomainType} {V : metricType K}. + +Local Notation ball_mdist := (fun x d => [set y : V | mdist x y < d]). + +Lemma ball_mdistE : ball_mdist = ball. +Proof. by apply/funext => x; apply/funext=> d; rewrite - ballEmdist. Qed. + +Local Notation nbhs_mdist := (nbhs_ball_ ball_mdist). + +Lemma nbhs_nbhs_mdist : nbhs_mdist = nbhs. +Proof. +apply/funext => x. +rewrite /nbhs_ball_. +rewrite -filter_from_ballE. +by rewrite -ball_mdistE. +Qed. + +Lemma nbhs_mdistP x (P : V -> Prop) : (\near x, P x) <-> nbhs_mdist x P. +Proof. by rewrite nbhs_nbhs_mdist. Qed. + +Lemma filter_from_mdist_nbhs (y : V) : + filter_from (fun i : K => 0 < i) (fun (i : K) (y' : V) => mdist y y' < i) + = nbhs y. +Proof. +rewrite -filter_from_ballE; apply/seteqP; split => [A|A]/=. + by move=> [x x0 yxA]; exists x => //; rewrite ballEmdist. +by move=> [x x0 yxA]; exists x => //; rewrite ballEmdist in yxA. +Qed. + +Let nbhs_simpl := (nbhs_simpl,@nbhs_nbhs_mdist,@filter_from_mdist_nbhs). + +Lemma fcvgrPdist_lt {F : set_system V} {FF : Filter F} (y : V) : + F --> y <-> forall eps, 0 < eps -> \forall y' \near F, mdist y y' < eps. +Proof. by rewrite -filter_fromP/= !nbhs_simpl. Qed. + +Lemma cvgrPdist_lt {T} {F : set_system T} {FF : Filter F} (f : T -> V) (y : V) : + f @ F --> y <-> forall eps, 0 < eps -> \forall t \near F, mdist y (f t) < eps. +Proof. exact: fcvgrPdist_lt. Qed. + +Lemma cvgr_dist_lt {T} {F : set_system T} {FF : Filter F} (f : T -> V) (y : V) : + f @ F --> y -> forall eps, eps > 0 -> \forall t \near F, mdist y (f t) < eps. +Proof. by move=> /cvgrPdist_lt. Qed. + +Lemma cvgr_dist_le {T} {F : set_system T} {FF : Filter F} (f : T -> V) (y : V) : + f @ F --> y -> forall eps, eps > 0 -> \forall t \near F, mdist y (f t) <= eps. +Proof. +by move=> ? ? ?; near do rewrite ltW//; apply: cvgr_dist_lt. +Unshelve. all: by end_near. Qed. + +End metricType_numDomainType. + +Section at_left_right_metricType. +(* tentative generalization of the section +at_left_right_pseudoMetricNormedZmod +from +pseudoMetricNormedZmodType +to +metricType *) +Variables (R : numFieldType) (V : metricType R). + +Lemma nbhsr0P (P : set V) x : + (\forall y \near x, P y) <-> + (\forall e \near 0^'+, forall y, mdist x y <= e -> P y). +Proof. +rewrite (*nbhs0P*)/= near_withinE !near_simpl. +split. + move => /nbhs_mdistP[/= _/posnumP[e] /(_ _) Px]. + apply/(@nbhs_mdistP R R^o). + exists e%:num => //= r /= re yr y xyr. + apply: Px => /=. + rewrite (le_lt_trans _ re)//. + rewrite (le_trans xyr)//. + by rewrite /mdist/= subr0 real_ler_norm// gtr0_real. +move => /(@nbhs_mdistP R R^o)[/= _/posnumP[e] /(_ _) Px]. +apply/(@nbhs_mdistP R V). +exists (e%:num / 2) => //= r /= re; apply: (Px (e%:num / 2)) => //=. + by rewrite /mdist/= subr0 gtr0_norm// ltr_pdivrMr// ltr_pMr// ltr1n. +by rewrite ltW. +Qed. + +Let cvgrP {F : set_system V} {FF : Filter F} (y : V) : [<-> + F --> y; + forall eps, 0 < eps -> \forall t \near F, mdist y t <= eps; + \forall eps \near 0^'+, \forall t \near F, mdist y t <= eps; + \forall eps \near 0^'+, \forall t \near F, mdist y t < eps]. +Proof. +tfae; first by move=> *; apply: cvgr_dist_le. +- by move=> Fy; near do apply: Fy; apply: nbhs_right_gt. +- move=> Fy; near=> e; near (0:R)^'+ => d; near=> x. + rewrite (@le_lt_trans _ _ d)//; first by near: x; near: d. + by near: d; apply: nbhs_right_lt; near: e; apply: nbhs_right_gt. +- move=> Fy; apply/cvgrPdist_lt => e e_gt0; near (0:R)^'+ => d. + near=> x; rewrite (@lt_le_trans _ _ d)//; first by near: x; near: d. + by near: d; apply: nbhs_right_le. +Unshelve. all: by end_near. Qed. + +Lemma cvgrPdist_le {T} {F : set_system T} {FF : Filter F} (f : T -> V) (y : V) : + f @ F --> y <-> forall eps, 0 < eps -> \forall t \near F, mdist y (f t) <= eps. +Proof. exact: (cvgrP _ 0 1)%N. Qed. + +End at_left_right_metricType. + +End metricType_numDomainType. + +Section cvg_nbhsP. +Variables (R : realType) (V : metricType R). + +Import metricType_numDomainType. + +Lemma cvg_nbhsP (f : V -> V) (p l : V) : f x @[x --> p] --> l <-> + (forall u : nat -> V, (u n @[n --> \oo] --> p) -> f (u n) @[n --> \oo] --> l). +Proof. +split=> [/cvgrPdist_le /= fpl u /cvgrPdist_lt /= uyp|pfl]. + apply/cvgrPdist_le => e /fpl. + rewrite -filter_from_mdist_nbhs. + move=> [d d0 pdf]. + by apply: filterS (uyp d d0) => t /pdf. +apply: contrapT => fpl; move: pfl; apply/existsNP. +suff: exists2 x : nat -> V, + x n @[n --> \oo] --> p & ~ f (x n) @[n --> \oo] --> l. + by move=> [x_] hp; exists x_; exact/not_implyP. +have [e He] : exists e : {posnum R}, forall d : {posnum R}, + exists xn, mdist xn p < d%:num /\ mdist (f xn) l >= e%:num. + apply: contrapT; apply: contra_not fpl => /forallNP h. + apply/cvgrPdist_le => e e0; have /existsNP[d] := h (PosNum e0). + move/forallNP => {}h; near=> t. + have /not_andP[abs|/negP] := h t. + - exfalso; apply: abs. + near: t. + rewrite !near_simpl. + rewrite /prop_near1. + rewrite -nbhs_nbhs_mdist. + exists d%:num => //= z/=. + by rewrite metric_sym. + - by rewrite -ltNge metric_sym => /ltW. +have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0. +exists (fun n => sval (cid (He (PosNum (invn n))))). + apply/cvgrPdist_lt => r r0; near=> t. + rewrite /sval/=; case: cid => x [xpt _]. + rewrite metric_sym (lt_le_trans xpt)// -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0//. + near: t; exists (trunc r^-1) => // s /= rs. + by rewrite (le_trans (ltW (truncnS_gt _)))// ler_nat. +move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)). +rewrite /sval/=; case: cid => // x [px xpn]. +by rewrite ltNge metric_sym => /negP. +Unshelve. all: end_near. Qed. + +End cvg_nbhsP. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index 28d54db18..6ba10f475 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -143,6 +143,100 @@ Module Exports. HB.reexport. End Exports. End numFieldTopology. Import numFieldTopology.Exports. +Reserved Notation "x ^'+" (at level 3, left associativity, format "x ^'+"). +Reserved Notation "x ^'-" (at level 3, left associativity, format "x ^'-"). + +Section at_left_right. +Variable R : numFieldType. + +Definition at_left (x : R) := within (fun u => u < x) (nbhs x). +Definition at_right (x : R) := within (fun u => x < u) (nbhs x). +Local Notation "x ^'-" := (at_left x) : classical_set_scope. +Local Notation "x ^'+" := (at_right x) : classical_set_scope. + +Global Instance at_right_proper_filter (x : R) : ProperFilter x^'+. +Proof. +apply: Build_ProperFilter => -[_/posnumP[d] /(_ (x + d%:num / 2))]. +apply; last by rewrite ltrDl. +by rewrite /= opprD addNKr normrN ger0_norm// gtr_pMr// invf_lt1// ltr1n. +Qed. + +Global Instance at_left_proper_filter (x : R) : ProperFilter x^'-. +Proof. +apply: Build_ProperFilter => -[_ /posnumP[d] /(_ (x - d%:num / 2))]. +apply; last by rewrite gtrBl. +by rewrite /= opprB addrC subrK ger0_norm// gtr_pMr// invf_lt1// ltr1n. +Qed. + +Lemma nbhs_right_gt x : \forall y \near x^'+, x < y. +Proof. by rewrite near_withinE; apply: nearW. Qed. + +Lemma nbhs_left_lt x : \forall y \near x^'-, y < x. +Proof. by rewrite near_withinE; apply: nearW. Qed. + +Lemma nbhs_right_neq x : \forall y \near x^'+, y != x. +Proof. by rewrite near_withinE; apply: nearW => ? /gt_eqF->. Qed. + +Lemma nbhs_left_neq x : \forall y \near x^'-, y != x. +Proof. by rewrite near_withinE; apply: nearW => ? /lt_eqF->. Qed. + +Lemma nbhs_right_ge x : \forall y \near x^'+, x <= y. +Proof. by rewrite near_withinE; apply: nearW; apply/ltW. Qed. + +Lemma nbhs_left_le x : \forall y \near x^'-, y <= x. +Proof. by rewrite near_withinE; apply: nearW => ?; apply/ltW. Qed. + +Lemma nbhs_right_lt x z : x < z -> \forall y \near x^'+, y < z. +Proof. +move=> xz; exists (z - x) => //=; first by rewrite subr_gt0. +by move=> y /= + xy; rewrite distrC ?ger0_norm ?subr_ge0 1?ltW// ltrD2r. +Qed. + +Lemma nbhs_right_ltW x z : x < z -> \forall y \near nbhs x^'+, y <= z. +Proof. +by move=> xz; near=> y; apply/ltW; near: y; exact: nbhs_right_lt. +Unshelve. all: by end_near. Qed. + +Lemma nbhs_right_ltDr x e : 0 < e -> \forall y \near x ^'+, y - x < e. +Proof. +move=> e0; near=> y; rewrite ltrBlDr; near: y. +by apply: nbhs_right_lt; rewrite ltrDr. +Unshelve. all: by end_near. Qed. + +Lemma nbhs_right_le x z : x < z -> \forall y \near x^'+, y <= z. +Proof. by move=> xz; near do apply/ltW; apply: nbhs_right_lt. +Unshelve. all: by end_near. Qed. + +(* NB: In not_near_at_rightP (and not_near_at_rightP), R has type numFieldType. + It is possible realDomainType could make the proof simpler and at least as + useful. *) +Lemma not_near_at_rightP (p : R) (P : pred R) : + ~ (\forall x \near p^'+, P x) <-> + forall e : {posnum R}, exists2 x, p < x < p + e%:num & ~ P x. +Proof. +split=> [pPf e|ex_notPx]. +- apply: contrapT => /forallPNP peP; apply: pPf; near=> t. + apply: contrapT; apply: peP; apply/andP; split. + + by near: t; exact: nbhs_right_gt. + + by near: t; apply: nbhs_right_lt; rewrite ltrDl. +- rewrite /at_right near_withinE nearE. + rewrite -filter_from_ballE /filter_from/= -forallPNP => _ /posnumP[d]. + have [x /andP[px xpd] notPx] := ex_notPx d; rewrite -existsNP; exists x => /=. + apply: contra_not notPx; apply => //. + by rewrite /ball/= ltr0_norm ?subr_lt0// opprB ltrBlDl. +Unshelve. all: by end_near. Qed. + +End at_left_right. +#[global] Typeclasses Opaque at_left at_right. +Notation "x ^'-" := (at_left x) : classical_set_scope. +Notation "x ^'+" := (at_right x) : classical_set_scope. + +#[global] Hint Extern 0 (Filter (nbhs _^'+)) => + (apply: at_right_proper_filter) : typeclass_instances. + +#[global] Hint Extern 0 (Filter (nbhs _^'-)) => + (apply: at_left_proper_filter) : typeclass_instances. + Lemma closure_sup (R : realType) (A : set R) : A !=set0 -> has_ubound A -> closure A (sup A). Proof. diff --git a/theories/topology_theory/topology.v b/theories/topology_theory/topology.v index 1211f26dd..219af7220 100644 --- a/theories/topology_theory/topology.v +++ b/theories/topology_theory/topology.v @@ -19,3 +19,4 @@ From mathcomp Require Export one_point_compactification. From mathcomp Require Export sigT_topology. From mathcomp Require Export discrete_topology. From mathcomp Require Export separation_axioms. +From mathcomp Require Export metric_structure.