From b1cdc7b01b0f410bf68b001733c17e0c35cedb1f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 24 Sep 2026 10:36:06 +0900 Subject: [PATCH 1/4] fix deps between Topological/UniformNZModule and PseudoMetricNormedZmodule - mv structures from tvs.v - PseudoMetricNormedZmod inherits from TopologicalZmodule - uniform{N,Z} now depends on topological{N,Z} - structure of Uniform{N,Z}module for matrices (in `matrix_normedtype.v`) - structure of metric space over products (in `metric_structure.v`) - remove UniformLmodule - product of {Topological,Uniform}{N,Z}Module --- CHANGELOG_UNRELEASED.md | 37 ++ .../normedtype_theory/matrix_normedtype.v | 14 + theories/normedtype_theory/normed_module.v | 34 +- .../pseudometric_normed_Zmodule.v | 508 +++++++++++++++--- theories/normedtype_theory/tvs.v | 355 +++--------- theories/topology_theory/initial_topology.v | 29 +- theories/topology_theory/metric_structure.v | 38 ++ theories/topology_theory/product_topology.v | 66 ++- theories/topology_theory/uniform_structure.v | 5 +- 9 files changed, 729 insertions(+), 357 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d90a8985a4..924253533c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,6 +13,29 @@ + lemma `limn_einf_cst` - in `uniform_structure.v`: + lemma `unif_continuous_continuous` +- in `uniform_structure.v`: + + lemma `unif_continuous_comp` + +- in `initial_topology.v`: + + lemma `initial_unif_continuous` + + lemma `initial_unif_continuous_comp` + + lemma `initial_unif_continuous_comp_fst` + + lemma `initial_unif_continuous_comp_snd` + +- in `product_topology.v`: + + lemma `entourage_prod_exS` + + definition `interchange_prod` + + lemma `entourage_interchange_prod` + + lemma `pair_unif_continuous` + + lemma `fst_unif_continuous` + + lemma `snd_unif_continuous` + +- in `metric_space.v`: + + definition `prod_mdist` + +- in `pseudometric_normed_Zmodule.v`: + + lemma `PseudoMetricNormedZmod0_add_unif_continuous` + + lemma `PseudoMetricNormedZmod0_opp_unif_continuous` ### Changed @@ -38,10 +61,24 @@ ### Generalized +- in `pseudometric_normed_Zmodule.v`: + + from `pseudoMetricNormedZmodType` to `PseudoMetricNormedZmod0.type`: + * lemma `cvg_bounded` + * lemma `bounded_cst` + + from `realFieldType` to `numFieldType` + * lemma `bounded_funN` + * lemma `bounded_funD` + ### Deprecated ### Removed +- in `tvs.v`: + + structure `PreUniformLmodule` + + mixin `PreUniformLmodule_isUniformLmodule` + + structure `UniformLmodule` + + factory `UniformNmodule_isUniformLmodule` (?) + ### Infrastructure ### Misc diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index 047caece8d..008800bac1 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -286,6 +286,20 @@ elim/big_ind2 : _ => // [|a b c d bE dE]; first by rewrite mulr0. by rewrite !num_max bE dE maxr_pMr. Qed. +HB.instance Definition _ (K : numFieldType) (m n : nat) := + Uniform.on ('M[K]_(m, n)). + +Section matrix_UniformNZmodule. +Context {K : numFieldType} {m n : nat}. + +HB.instance Definition _ := PreUniformNmodule_isUniformNmodule.Build + 'M[K]_(m, n) (@PseudoMetricNormedZmod0_add_unif_continuous _ _). + +HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build + 'M[K]_(m, n) (@PseudoMetricNormedZmod0_opp_unif_continuous _ _). + +End matrix_UniformNZmodule. + HB.instance Definition _ (K : numFieldType) m n := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m, n) (@mx_normZ K m n). diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 0e97a3aca5..adeecbd08d 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -74,7 +74,6 @@ Reserved Notation "k .-lipschitz f" (at level 2, format "k .-lipschitz f"). Reserved Notation "[ 'lipschitz' E | x 'in' A ]" (at level 0, x name, format "[ 'lipschitz' E | x 'in' A ]"). -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -87,8 +86,8 @@ Local Open Scope ring_scope. (** Modules with a norm depending on a numDomain *) -HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule K V - & PseudoMetricNormedZmod K V & ConvexTvs K V := { +HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule + (K : numDomainType) V & PseudoMetricNormedZmod K V & ConvexTvs K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. @@ -111,12 +110,6 @@ HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule HB.builders Context K V & PseudoMetricNormedZmod_Lmodule_isNormedModule K V. -(**md `add_continuous` has been moved to `pseudometric_normed_Zmodule.v`, - `scale_continuous` is proved but is not proved again anymore later in this - file. *) -Let add_continuous : continuous (fun x : V * V => x.1 + x.2). -Proof. exact: add_continuous. Qed. - (** NB: we have almost the same proof in `tvs.v` *) Let scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2). Proof. @@ -157,11 +150,13 @@ move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. Qed. -HB.instance Definition _ := - PreTopologicalNmodule_isTopologicalNmodule.Build V add_continuous. +(* NB: was needed until version 1.18.0 *) +(*HB.instance Definition _ := + PreTopologicalNmodule_isTopologicalNmodule.Build V add_continuous.*) HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build K V scale_continuous. HB.instance Definition _ := Uniform_isConvexTvs.Build K V locally_convex_set. + HB.instance Definition _ := PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build K V normrZ. @@ -176,6 +171,11 @@ HB.structure Definition NormedVector (K : numDomainType) := Section standard_topology_normedMod. Variable R : numFieldType. +(* NB: was need until version 1.18.0 +HB.instance Definition _ := TopologicalZmodule_isTopologicalLmodule.Build + R^o R^o (@standard_scale_continuous R). +*) + HB.instance Definition _ := PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build R R^o (@normrM _). @@ -373,6 +373,12 @@ HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R M erefl. HB.instance Definition _ := isPseudoMetricNormedZmodule.Build R M. +HB.instance Definition _ := PreUniformNmodule_isUniformNmodule.Build + M (@PseudoMetricNormedZmod0_add_unif_continuous _ M). + +HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build + M (@PseudoMetricNormedZmod0_opp_unif_continuous _ M). + HB.instance Definition _ := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R M normrZ. @@ -2662,6 +2668,12 @@ HB.instance Definition _ (V : vectType R) := HB.instance Definition _ (V : vectType R) := isPseudoMetricNormedZmodule.Build _ (max_space V). +HB.instance Definition _ (V : vectType R) := PreUniformNmodule_isUniformNmodule.Build + (max_space V) (@PseudoMetricNormedZmod0_add_unif_continuous _ (max_space V)). + +HB.instance Definition _ (V : vectType R) := UniformNmodule_isUniformZmodule.Build + (max_space V) (@PseudoMetricNormedZmod0_opp_unif_continuous _ (max_space V)). + HB.instance Definition _ (V : vectType R) := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V) (@Norm.normZ _ _ (@max_norm V)). diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index a6c28fda15..72a9672f3d 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -141,76 +141,343 @@ HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}. HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}. HB.structure Definition PreTopologicalNmodule := {M of Topological M & GRing.Nmodule M}. + +HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M + & PreTopologicalNmodule M := { + add_continuous : continuous (fun x : M * M => x.1 + x.2) ; +}. + +HB.structure Definition TopologicalNmodule := + {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}. + +Section TopologicalNmodule_theory. +Variable (E : topologicalType) (F : TopologicalNmodule.type) (U : set_system E). + +(** TODO: + We have observed one thing: + `pseudometric_normedZmodType` is morally a `topologicalNmodule` + but `topologicalNmodule` is defined later in `tvs.v` (which imports `pseudometric_normed_zmodule.v`). + We think that it should be defined at the beginning of `pseudometric_normed_zmodule.v` and that + `pseudometric_normedZmodType` should be defined using `topologicalNmodule`. + We have realized this because of the lemmas such as `cvgD/fun_cvgD` that we needed to duplicate. *) +Lemma fun_cvgD {FF : Filter U} (f g : E -> F) a b : + f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b. +Proof. +move=> fa ga. +by apply: continuous2_cvg; [exact: (add_continuous (a, b))|by []..]. +Qed. + +Lemma cvg_sum (I : Type) (r : seq I) (P : pred I) + (Ff : I -> E -> F) (Fa : I -> F) : + Filter U -> (forall i, P i -> Ff i x @[x --> U] --> Fa i) -> + \sum_(i <- r | P i) Ff i x @[x --> U] --> \sum_(i <- r| P i) Fa i. +Proof. by move=> FF Ffa; apply: cvg_big => //; apply: add_continuous. Qed. + +Lemma sum_continuous (I : Type) (r : seq I) (P : pred I) (f : I -> E -> F) : + (forall i : I, P i -> continuous (f i)) -> + continuous (fun x1 : E => \sum_(i <- r | P i) f i x1). +Proof. by move=> FC0; apply: continuous_big => //; apply: add_continuous. Qed. + +End TopologicalNmodule_theory. + HB.structure Definition PreTopologicalZmodule := {M of Topological M & GRing.Zmodule M}. + +HB.mixin Record TopologicalNmodule_isTopologicalZmodule M + & Topological M & GRing.Zmodule M := { + opp_continuous : continuous (-%R : M -> M) ; +}. + +#[short(type="topologicalZmodType")] +HB.structure Definition TopologicalZmodule := + {M of TopologicalNmodule M & GRing.Zmodule M + & TopologicalNmodule_isTopologicalZmodule M}. + +Section TopologicalZmoduleTheory. +Variables (M : topologicalZmodType). + +Lemma sub_continuous : continuous (fun x : M * M => x.1 - x.2). +Proof. +move=> x; apply: (@continuous_comp _ _ _ (fun x => (x.1, - x.2)) + (fun x : M * M => x.1 + x.2)); last exact: add_continuous. +apply: cvg_pair; first exact: cvg_fst. +by apply: continuous_comp; [exact: cvg_snd|exact: opp_continuous]. +Qed. + +Lemma fun_cvgN (F : topologicalZmodType) (U : set_system M) {FF : Filter U} + (f : M -> F) a : + f @ U --> a -> \- f @ U --> - a. +Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed. + +End TopologicalZmoduleTheory. + +HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M + & Topological M & GRing.Zmodule M := { + sub_continuous : continuous (fun x : M * M => x.1 - x.2) ; +}. + +HB.builders Context M & PreTopologicalNmodule_isTopologicalZmodule M. + +Let opp_continuous : continuous (-%R : M -> M). +Proof. +move=> x; rewrite /continuous_at. +rewrite -(@eq_cvg _ _ _ (fun x => 0 - x)); first by move=> y; exact: add0r. +rewrite -[- x]add0r. +apply: (@continuous_comp _ _ _ (fun x => (0, x)) (fun x : M * M => x.1 - x.2)). + exact: cvg_pair. +exact: sub_continuous. +Qed. + +Let add_continuous : continuous (fun x : M * M => x.1 + x.2). +Proof. +move=> x; rewrite /continuous_at. +rewrite -(@eq_cvg _ _ _ (fun x => x.1 - (- x.2))). + by move=> y; rewrite opprK. +rewrite -[in x.1 + _](opprK x.2). +apply: (@continuous_comp _ _ _ (fun x => (x.1, - x.2)) (fun x => x.1 - x.2)). + apply: cvg_pair; first exact: cvg_fst. + by apply: continuous_comp; [exact: cvg_snd|exact: opp_continuous]. +exact: sub_continuous. +Qed. + +HB.instance Definition _ := + PreTopologicalNmodule_isTopologicalNmodule.Build M add_continuous. + +HB.instance Definition _ := + TopologicalNmodule_isTopologicalZmodule.Build M opp_continuous. + +HB.end. + HB.structure Definition PreUniformNmodule := {M of Uniform M & GRing.Nmodule M}. + +HB.mixin Record PreUniformNmodule_isUniformNmodule M & PreUniformNmodule M := { + add_unif_continuous : unif_continuous (fun x : M * M => x.1 + x.2) +}. + +HB.structure Definition UniformNmodule := + {M of PreUniformNmodule M & PreUniformNmodule_isUniformNmodule M & TopologicalNmodule M}. + +Section prod_TopologicalNmodule. +Context {E F : TopologicalNmodule.type}. + +Let prod_add_continuous : continuous (fun x : (E * F) * (E * F) => x.1 + x.2). +Proof. +move => [/= x y] /= U /= [[/= A B]] /= [xyA xyB] ABU. +have [/= A0 [A01 A02] A0A] := @add_continuous E (x.1, y.1) _ xyA. +have [/= B0 [B01 B02] B0B] := @add_continuous F (x.2, y.2) _ xyB. +exists ([set x | A0.1 x.1 /\ B0.1 x.2], [set xy | A0.2 xy.1 /\ B0.2 xy.2]). + by split; [exists (A0.1, B0.1)|exists (A0.2, B0.2)]. +move => [[x1 y1][x2 y2]] /= [[? ?] [? ?]]. +by apply: ABU; split; [exact: (A0A (x1, x2))|exact: (B0B (y1, y2))]. +Qed. + +HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build + (E * F)%type prod_add_continuous. + +End prod_TopologicalNmodule. + +Section prod_UniformNmodule. +Context {E F : UniformNmodule.type}. + +Lemma prod_add_unif_continuous : + unif_continuous (fun x : (E * F) * (E * F) => x.1 + x.2). +Proof. +move=> P /= /entourage_prod_exS[A [B [entA entB ABP]]]. +have [/= A1 [A2 [entA1 entA2 A12]]] := + entourage_prod_exS (@add_unif_continuous _ _ entA). +have [/= B1 [B2 [entB1 entB2 B12]]] := + entourage_prod_exS (@add_unif_continuous _ _ entB). +have entAB1 := prod_entP entA1 entB1. +have entAB2 := prod_entP entA2 entB2. +pose AB1 := [set xy | A1 (xy.1.1, xy.2.1) /\ B1 (xy.1.2, xy.2.2)]. +pose AB2 := [set xy | A2 (xy.1.1, xy.2.1) /\ B2 (xy.1.2, xy.2.2)]. +exists (AB1, AB2) => //=. +move=> -[[[a1 a2] [b1 b2]] [[a1' a2'] [b1' b2']]] /=. +move=> [[/= A1a B1a] [/= A2b B2b]]. +exists ((a1, a2), (a1', a2'), ((b1, b2), (b1', b2'))) =>//=. +by apply: ABP => /=; split; + [exact: (A12 (a1, a1', (b1, b1')))|exact: (B12 (a2, a2', (b2, b2')))]. +Qed. + +HB.instance Definition _ := PreUniformNmodule_isUniformNmodule.Build + (E * F)%type prod_add_unif_continuous. + +End prod_UniformNmodule. + HB.structure Definition PreUniformZmodule := {M of Uniform M & GRing.Zmodule M}. -HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T - & Num.NormedZmodule R T & PseudoPointedMetric R T := { - pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |) +HB.mixin Record UniformNmodule_isUniformZmodule M + & Uniform M & GRing.Zmodule M := { + opp_unif_continuous : unif_continuous (-%R : M -> M) }. -HB.structure Definition PseudoMetricNormedZmod0 (R : numDomainType) := - {T of Num.NormedZmodule R T & PseudoPointedMetric R T - & NormedZmod_PseudoMetric_eq R T }. +HB.structure Definition UniformZmodule := + {M of UniformNmodule M & GRing.Zmodule M & UniformNmodule_isUniformZmodule M + & TopologicalZmodule M}. -Section PseudoMetricNormedZmod0_numDomainType. -Context {K : numDomainType} {V : PseudoMetricNormedZmod0.type K}. +Section prod_TopologicalZmodule. +Context {E F : TopologicalZmodule.type}. -(**md Balls defined by the norm: *) -Local Notation ball_norm := (ball_ (@Num.norm K V)). +Let prod_opp_continuous : continuous (-%R : E * F -> E * F). +Proof. +move => [/= x y] /= U /= [[/= A B]] /= [xA yB] ABU. +have Ax := @opp_continuous E x _ xA. +have By := @opp_continuous F y _ yB. +exists (-%R @^-1` A, -%R @^-1` B) => //=. +by move=> [a b] []/= ANa BNb; exact: ABU. +Qed. -Lemma ball_normE : ball_norm = ball. -Proof. by rewrite pseudo_metric_ball_norm. Qed. +HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build + (E * F)%type prod_opp_continuous. -End PseudoMetricNormedZmod0_numDomainType. +End prod_TopologicalZmodule. -#[short(type="pseudoMetricNormedZmodType")] -HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) := - {T of PseudoMetricNormedZmod0 R T & Metric R T}. +Section prod_UniformZmodule. +Context {E F : UniformZmodule.type}. -HB.factory Record isPseudoMetricNormedZmodule - (K : numDomainType) T & PseudoMetricNormedZmod0 K T := { }. +Lemma prod_opp_unif_continuous : unif_continuous (-%R : E * F -> E * F). +Proof. +move=> P /= /entourage_prod_exS[A [B [entA entB ABP]]]. +have entAN := @opp_unif_continuous _ _ entA. +have entBN := @opp_unif_continuous _ _ entB. +apply: filterS (prod_entP entAN entBN) => -[[a1 a2] [b1 b2]] /= [A1 B2]. +exact: (ABP ((- a1, - a2), (- b1, - b2))). +Qed. -HB.builders Context K T & isPseudoMetricNormedZmodule K T. +HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build + (E * F)%type prod_opp_unif_continuous. -Let mdist (x y : T) : K := `|x - y|. +End prod_UniformZmodule. -Let mdist_ge0 x y : 0 <= mdist x y. Proof. by rewrite /mdist. Qed. +HB.factory Record PreUniformNmodule_isUniformZmodule M + & Uniform M & GRing.Zmodule M := { + sub_unif_continuous : unif_continuous (fun x : M * M => x.1 - x.2) +}. -Let mdist_positivity x y : mdist x y = 0 -> x = y. -Proof. by move=> /normr0_eq0/subr0_eq. Qed. +HB.builders Context M & PreUniformNmodule_isUniformZmodule M. -Let ballEmdist x d : ball x d = [set y | mdist x y < d]. -Proof. by rewrite -ball_normE. Qed. +Lemma opp_unif_continuous : unif_continuous (-%R : M -> M). +Proof. +have unif : unif_continuous (fun x => (0, x) : M * M). + move=> /= U [[]] /= U1 U2 [] U1e U2e /subsetP U12. + apply: filterS U2e => x xU2/=. + have /U12 : ((0, 0), x) \in U1 `*` U2. + by rewrite in_setX/= (mem_set xU2) andbT inE; exact: entourage_refl. + by rewrite inE/= => -[[[a1 a2] [b1 b2]]]/= /[swap]-[] -> -> <-. +move=> /= U /sub_unif_continuous /unif /=. +rewrite -comp_preimage/= /comp/= /nbhs/=. +congr entourage => /=; rewrite eqEsubset. +by split=> x //=; rewrite /map_pair !sub0r. +Qed. + +Lemma add_unif_continuous : unif_continuous (fun x : M * M => x.1 + x.2). +Proof. +have unif: unif_continuous (fun x => (x.1, -x.2) : M * M). + move=> /= U [[]]/= U1 U2 [] U1e /opp_unif_continuous. + rewrite /nbhs/= => U2e /subsetP U12. + apply: (@filterS _ _ entourage_filter + ((fun xy => (xy.1.1, xy.2.1, (-xy.1.2, -xy.2.2))) @^-1` (U1 `*` U2))). + move=> /= [] [] a1 a2 [] b1 b2/= [] ab1 ab2. + have /U12 : (a1, b1, (-a2, -b2)) \in U1 `*` U2 by rewrite !inE. + by rewrite /map_pair inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-. + exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split. + by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)). +move=> /= U /sub_unif_continuous/unif; rewrite /nbhs/=. +rewrite -comp_preimage/=/comp/=. +congr entourage; rewrite eqEsubset. +by split=> x /=; rewrite /map_pair !opprK. +Qed. + +Lemma add_continuous : continuous (fun x : M * M => x.1 + x.2). +Proof. by apply: unif_continuous_continuous; exact: add_unif_continuous. Qed. HB.instance Definition _ := - @PseudoMetric_isMetric.Build K T mdist mdist_ge0 mdist_positivity ballEmdist. + PreTopologicalNmodule_isTopologicalNmodule.Build M add_continuous. + +HB.instance Definition _ := + PreUniformNmodule_isUniformNmodule.Build M add_unif_continuous. + +Lemma opp_continuous : continuous (-%R : M -> M). +Proof. +apply: unif_continuous_continuous. +exact: opp_unif_continuous. +Qed. + +HB.instance Definition _ := + TopologicalNmodule_isTopologicalZmodule.Build M opp_continuous. + +HB.instance Definition _ := + UniformNmodule_isUniformZmodule.Build M opp_unif_continuous. HB.end. -(* alternative definition of a PseudoMetricNormedZmod *) -HB.factory Record NormedZmoduleMetric (R : numDomainType) T - & Num.NormedZmodule R T & Metric R T & isPointed T := { - mdist_norm : forall x y : T, mdist x y = `|y - x| +Section UniformZmoduleTheory. +Variables (M : UniformZmodule.type). + +Lemma sub_unif_continuous : unif_continuous (fun x : M * M => x.1 - x.2). +Proof. +suff unif: unif_continuous (fun x => (x.1, - x.2) : M * M). + by move=> /= U /add_unif_continuous/unif; rewrite /nbhs/= -comp_preimage. +move=> /= U [[]]/= U1 U2 [] U1e /opp_unif_continuous. +rewrite /nbhs/= => U2e /subsetP U12. +apply: (@filterS _ _ entourage_filter + ((fun xy => (xy.1.1, xy.2.1, (- xy.1.2, - xy.2.2))) @^-1` (U1 `*` U2))). + move=> /= [] [] a1 a2 [] b1 b2/= [] ab1 ab2. + have /U12 : (a1, b1, (-a2, -b2)) \in U1 `*` U2 by rewrite !inE. + by rewrite /map_pair inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-. +exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split. +by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)). +Qed. + +End UniformZmoduleTheory. + +HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T + & Num.NormedZmodule R T & PseudoPointedMetric R T := { + pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |) }. -HB.builders Context (R : numDomainType) T & NormedZmoduleMetric R T. +HB.structure Definition PseudoMetricNormedZmod0 (R : numDomainType) := + {T of Num.NormedZmodule R T & PseudoPointedMetric R T + & NormedZmod_PseudoMetric_eq R T }. -Let pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |). +Section PseudoMetricNormedZmod0_numDomainType. +Context {K : numDomainType} {V : PseudoMetricNormedZmod0.type K}. + +(**md Balls defined by the norm: *) +Local Notation ball_norm := (ball_ (@Num.norm K V)). + +Lemma ball_normE : ball_norm = ball. +Proof. by rewrite pseudo_metric_ball_norm. Qed. + +End PseudoMetricNormedZmod0_numDomainType. + +Lemma PseudoMetricNormedZmod0_add_unif_continuous {R : numFieldType} + (M : PseudoMetricNormedZmod0.type R) : unif_continuous (fun x : M * M => x.1 + x.2). Proof. -apply/funext => /= t; apply/funext => d; rewrite ballEmdist. -by apply/seteqP; split => [y|y]/=; rewrite mdist_norm distrC. +apply/unif_continuousP => /= e e0. +exists (e / 2); first by rewrite divr_gt0. +move=> [/= [a1 a2] [b1 b2]]/=. +rewrite -ball_normE/=. +rewrite /ball/= /prod_ball/= => -[]. +rewrite -ball_normE/= => ab1 ab2. +by rewrite opprD addrACA (splitr e)// (le_lt_trans (ler_normD _ _))//= ltrD. Qed. -HB.instance Definition _ := - NormedZmod_PseudoMetric_eq.Build R T pseudo_metric_ball_norm. +Lemma PseudoMetricNormedZmod0_opp_unif_continuous {R : numFieldType} + (M : PseudoMetricNormedZmod0.type R) : unif_continuous (-%R : M -> M). +Proof. +apply/unif_continuousP => /= e e0. +exists e => // -[a1 a2]/=. +by rewrite -ball_normE/= -opprD Num.normrN. +Qed. -HB.end. +#[short(type="pseudoMetricNormedZmodType")] +HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) := + {T of PseudoMetricNormedZmod0 R T & Metric R T & UniformZmodule T}. -Section pseudoMetricNormedZmod_numDomainType. -Context {K : numDomainType} {V : pseudoMetricNormedZmodType K}. +(* was Section pseudoMetricNormedZmod_numDomainType. *) +Section PseudoMetricNormedZmod0_numDomainType. +Context {K : numDomainType} {V : PseudoMetricNormedZmod0.type K}. Lemma ball_open (x : V) (r : K) : open (ball x r). Proof. @@ -380,7 +647,7 @@ rewrite funeqE => A; rewrite /= !near_simpl (near_shift (y + x)). by rewrite (_ : _ \o _ = A \o f) // funeqE=> z; rewrite /= opprD addNKr addrNK. Qed. -End pseudoMetricNormedZmod_numDomainType. +End PseudoMetricNormedZmod0_numDomainType. #[global] Hint Resolve normr_ge0 : core. Arguments cvgr_dist_lt {_ _ _ F FF}. Arguments cvgr_distC_lt {_ _ _ F FF}. @@ -402,9 +669,9 @@ Arguments cvgr0_norm_le {_ _ _ F FF}. #[global] Hint Extern 0 (is_true (`|?x| <= _)) => match goal with H : x \is_near _ |- _ => solve[near: x; now apply: cvgr0_norm_le] end : core. -Section pseudoMetricNormedZmod_realDomainType. +Section PseudoMetricNormedZmod0_realDomainType. -Lemma le0_ball0 (R : realDomainType) (V : pseudoMetricNormedZmodType R) (a : V) (r : R) : +Lemma le0_ball0 (R : realDomainType) (V : PseudoMetricNormedZmod0.type R) (a : V) (r : R) : r <= 0 -> ball a r = set0. Proof. move=> r0; rewrite -subset0 => y. @@ -412,10 +679,10 @@ rewrite -ball_normE /ball_/= ltNge => /negP; apply. by rewrite (le_trans r0). Qed. -End pseudoMetricNormedZmod_realDomainType. +End PseudoMetricNormedZmod0_realDomainType. -Section pseudoMetricNormedZmod_numFieldType. -Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R). +Section PseudoMetricNormedZmod0_numFieldType. +Variables (R : numFieldType) (V : PseudoMetricNormedZmod0.type R). Lemma norm_hausdorff : hausdorff_space V. Proof. @@ -487,10 +754,68 @@ Proof. by move=> xlt ylt; rewrite -[y]opprK (@distm_lt_split 0) ?subr0 ?opprK ?add0r. Qed. -End pseudoMetricNormedZmod_numFieldType. +End PseudoMetricNormedZmod0_numFieldType. #[global] Hint Extern 0 (hausdorff_space _) => solve[apply: norm_hausdorff] : core. +HB.factory Record isPseudoMetricNormedZmodule + (K : numFieldType) T & PseudoMetricNormedZmod0 K T := { }. + +HB.builders Context K T & isPseudoMetricNormedZmodule K T. + +Let mdist (x y : T) : K := `|x - y|. + +Let mdist_ge0 x y : 0 <= mdist x y. Proof. by rewrite /mdist. Qed. + +Let mdist_positivity x y : mdist x y = 0 -> x = y. +Proof. by move=> /normr0_eq0/subr0_eq. Qed. + +Let ballEmdist x d : ball x d = [set y | mdist x y < d]. +Proof. by rewrite -ball_normE. Qed. + +HB.instance Definition _ := + @PseudoMetric_isMetric.Build K T mdist mdist_ge0 mdist_positivity ballEmdist. + +Let add_continuous : continuous (fun x : T * T => x.1 + x.2). +Proof. +move=> [/= x y]. +apply/cvgrPdist_lt=> _/posnumP[e]; near=> a b => /=. +by rewrite opprD addrACA normm_lt_split. +Unshelve. all: by end_near. Qed. + +HB.instance Definition _ := + PreTopologicalNmodule_isTopologicalNmodule.Build T add_continuous. + +Let opp_continuous : continuous (-%R : T -> T). +Proof. +move=> x. +apply/cvgrPdist_lt=> _/posnumP[e]; near=> a => /=. +by rewrite opprK addrC. +Unshelve. all: by end_near. Qed. + +HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build T opp_continuous. + +HB.end. + +(* alternative definition of a PseudoMetricNormedZmod *) +HB.factory Record NormedZmoduleMetric (R : numDomainType) T + & 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 & 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 prod_pseudoMetricNormedZmod. Context {K : numDomainType} {U V : pseudoMetricNormedZmodType K}. @@ -507,9 +832,16 @@ Proof. by rewrite /= - ball_prod_normE. Qed. HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build K (U * V)%type prod_norm_ball. +End prod_pseudoMetricNormedZmod. + +(* +Section prod_pseudoMetricNormedZmod_new. +Context {K : numFieldType} {U V : pseudoMetricNormedZmodType K}. + HB.instance Definition _ := isPseudoMetricNormedZmodule.Build _ (U * V)%type. -End prod_pseudoMetricNormedZmod. +End prod_pseudoMetricNormedZmod_new. +*) Section prod_NormedModule_lemmas. Context {T : Type} {K : numDomainType} {U V : pseudoMetricNormedZmodType K}. @@ -543,12 +875,40 @@ Arguments cvgr2dist_ltP {_ _ _ _ _ F G FF FG}. Arguments cvgr2dist_lt {_ _ _ _ _ F G FF FG}. Section standard_topology_pseudoMetricNormedZmod. -Variable R : numFieldType. +Context {R : numFieldType}. HB.instance Definition _ := Num.NormedZmodule.on R^o. HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R R^o erefl. +Let standard_add_unif_continuous : unif_continuous (fun x : R^o * R^o => x.1 + x.2). +Proof. exact: PseudoMetricNormedZmod0_add_unif_continuous. Qed. + +Let standard_add_continuous : continuous (fun x : R^o * R^o => x.1 + x.2). +Proof. +by apply: unif_continuous_continuous; exact: standard_add_unif_continuous. +Qed. + +HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build + R^o standard_add_continuous. + +HB.instance Definition _ := PreUniformNmodule_isUniformNmodule.Build + R^o standard_add_unif_continuous. + +Let standard_opp_unif_continuous : unif_continuous (-%R : R^o -> R^o). +Proof. exact: PseudoMetricNormedZmod0_opp_unif_continuous. Qed. + +Let standard_opp_continuous : continuous (-%R : R^o -> R^o). +Proof. +by apply: unif_continuous_continuous; exact: standard_opp_unif_continuous. +Qed. + +HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build + R^o standard_opp_continuous. + +HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build + R^o standard_opp_unif_continuous. + End standard_topology_pseudoMetricNormedZmod. Lemma ball_itv {R : realFieldType} (x r : R) : @@ -569,12 +929,6 @@ move=> x; apply/cvgrPdist_lt=> e e0; near do rewrite -opprD normrN. exact: cvgr_dist_lt. Unshelve. all: by end_near. Qed. -Lemma add_continuous : continuous (fun z : V * V => z.1 + z.2). -Proof. -move=> [/= x y]; apply/cvgrPdist_lt=> _/posnumP[e]; near=> a b => /=. -by rewrite opprD addrACA normm_lt_split. -Unshelve. all: by end_near. Qed. - Lemma natmul_continuous n : continuous (fun x : V => x *+ n). Proof. case: n => [|n] x; first exact: cst_continuous. @@ -589,14 +943,14 @@ by exists e => //= y; exact/le_lt_trans/ler_dist_dist. Qed. End continuity_pseudoMetricNormedZmodType. -#[deprecated(since="mathcomp-analysis 1.11.0", note="renamed to `oppr_continuous`")] -Notation opp_continuous := oppr_continuous (only parsing). +(*#[deprecated(since="mathcomp-analysis 1.11.0", note="renamed to `oppr_continuous`")] +Notation opp_continuous := oppr_continuous (only parsing).*) -(* TODO: generalize to R : numFieldType *) +(* TODO: generalize to R : numFieldType DONE?! *) Section hausdorff. #[deprecated(since="mathcomp-analysis 1.10.0", note="use `norm_hausdorff` instead")] -Lemma pseudoMetricNormedZModType_hausdorff (R : realFieldType) +Lemma pseudoMetricNormedZModType_hausdorff (R : numFieldType) (V : pseudoMetricNormedZmodType R) : hausdorff_space V. Proof. exact: norm_hausdorff. Qed. @@ -694,7 +1048,7 @@ by rewrite at_leftN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK. Qed. Section at_left_right_pseudoMetricNormedZmod. -Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R). +Variables (R : numFieldType) (V : PseudoMetricNormedZmod0.type R). Lemma nbhsr0P (P : set V) x : (\forall y \near x, P y) <-> @@ -924,7 +1278,7 @@ by rewrite gtr_pMr// invf_lt1// ltr1n. Unshelve. all: by end_near. Qed. Section pseudoMetricNormedZmod_numFieldType. -Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R). +Variables (R : numFieldType) (V : PseudoMetricNormedZmod0.type R). Variables (I : Type) (F : set_system I) (FF : Filter F) (f : I -> V) (y : V). Lemma cvgr_norm_lty : @@ -1106,8 +1460,8 @@ Ltac near_simpl := rewrite ?near_simpl. End NearNorm. Section cvg_composition_pseudometric. -Context {K : numFieldType} {V : pseudoMetricNormedZmodType K} {T : Type}. -Context (F : set_system T) {FF : Filter F}. +Context {K : numFieldType} {V : pseudoMetricNormedZmodType K} {T : Type} + (F : set_system T) {FF : Filter F}. Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a b : V). Lemma cvgN f a : f @ F --> a -> - f @ F --> - a. @@ -1130,7 +1484,7 @@ Proof. by move=> /cvgMn /cvgP. Qed. Lemma cvgD f g a b : f @ F --> a -> g @ F --> b -> (f + g) @ F --> a + b. Proof. -by move=> *; apply: continuous2_cvg => //; exact: (@add_continuous _ _ (a, b)). +by move=> *; apply: continuous2_cvg => //; exact: (@add_continuous _ (a, b)). Qed. Lemma is_cvgD f g : cvg (f @ F) -> cvg (g @ F) -> cvg (f + g @ F). @@ -1291,7 +1645,7 @@ Qed. End limit_composition_pseudometric. Section domination. -Context {T : Type} {K : numDomainType} {V W : pseudoMetricNormedZmodType K}. +Context {T : Type} {K : numDomainType} {V W : PseudoMetricNormedZmod0.type K}. Definition dominated_by (h : T -> V) (k : K) (f : T -> W) (F : set_system T) := F [set x | `|f x| <= k * `|h x|]. @@ -1314,7 +1668,7 @@ Lemma sub_dominatedr (T : Type) (K : numDomainType) Proof. by move=> le_fg; apply: filterS2 le_fg => x; apply: le_trans. Qed. Section ex_dom_bound. -Context {T : Type} {K : numFieldType} {V W : pseudoMetricNormedZmodType K}. +Context {T : Type} {K : numFieldType} {V W : PseudoMetricNormedZmod0.type K}. Lemma ex_dom_bound (h : T -> V) (f : T -> W) (F : set_system T) {PF : ProperFilter F} : @@ -1349,7 +1703,7 @@ Qed. End ex_dom_bound. Definition bounded_near {T : Type} {K : numFieldType} - {V : pseudoMetricNormedZmodType K} + {V : PseudoMetricNormedZmod0.type K} (f : T -> V) (F : set_system T) := \forall M \near +oo, F [set x | `|f x| <= M]. @@ -1414,7 +1768,7 @@ Unshelve. all: by end_near. Qed. End bounded_near. Section cvg_bounded. -Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R). +Variables (R : numFieldType) (V : PseudoMetricNormedZmod0.type R). Lemma cvg_bounded {I} {F : set_system I} {FF : Filter F} (f : I -> V) (y : V) : f @ F --> y -> bounded_near f F. @@ -1423,7 +1777,21 @@ Proof. exact: cvgr_norm_ley. Qed. End cvg_bounded. Arguments cvg_bounded {R V I F FF}. -Lemma bounded_cst (K : numFieldType) {V : pseudoMetricNormedZmodType K} +Lemma standard_scale_continuous {R : numFieldType} : + continuous (fun z : R^o * R^o => z.1 *: z.2). +Proof. +move=> [/= k x]; apply/cvgrPdist_lt => _/posnumP[e]; near +oo_R => M. +near=> l z => /=; have M0 : 0 < M by []. +rewrite (@distm_lt_split _ _ (k *: z)) // -?(scalerBr, scalerBl) normrM. + rewrite (@le_lt_trans _ _ (M * `|x - z|)) ?ler_wpM2r -?ltr_pdivlMl//. + by near: z; apply: cvgr_dist_lt; rewrite // mulr_gt0 ?invr_gt0. +rewrite (@le_lt_trans _ _ (`|k - l| * M)) ?ler_wpM2l -?ltr_pdivlMr//. + near: z; near: M. + exact: (@cvg_bounded _ R^o _ _ _ _ _ (@cvg_refl _ _)). +by near: l; apply: cvgr_dist_lt; rewrite // divr_gt0. +Unshelve. all: by end_near. Qed. + +Lemma bounded_cst (K : numFieldType) {V : PseudoMetricNormedZmod0.type K} (k : V) T (A : set T) : [bounded k | _ in A]. Proof. rewrite /bounded_near; near=> M => t At /=. @@ -1438,7 +1806,7 @@ rewrite (le_lt_trans (ler_norm _)) ?ltrDl// => /(_ erefl) aM. by exists (`|M| + 1) => _ [n _ <-]; rewrite (le_trans (ler_norm _))// aM. Qed. -Lemma bounded_funN (T : Type) (R : realFieldType) (a : T -> R^o) : +Lemma bounded_funN (T : Type) (R : numFieldType) (a : T -> R^o) : bounded_fun a -> bounded_fun (- a). Proof. move=> [M [Mreal aM]]; rewrite /bounded_fun /bounded_near; near=> x => y /= _. @@ -1452,7 +1820,7 @@ move=> /bounded_funN/bounded_fun_has_ubound ba; apply/has_lb_ubN. by apply: subset_has_ubound ba => _ [_ [n _] <- <-]; exists n. Qed. -Lemma bounded_funD (T : Type) (R : realFieldType) (a b : T -> R^o) : +Lemma bounded_funD (T : Type) (R : numFieldType) (a b : T -> R^o) : bounded_fun a -> bounded_fun b -> bounded_fun (a \+ b). Proof. move=> [M [Mreal Ma]] [N [Nreal Nb]]. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index fbf94e28f7..cfae49fc7c 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -108,109 +108,6 @@ Local Open Scope ring_scope. HB.structure Definition NbhsLmodule (K : numDomainType) := {M of Nbhs M & GRing.Lmodule K M}. -HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M - & PreTopologicalNmodule M := { - add_continuous : continuous (fun x : M * M => x.1 + x.2) ; -}. - -HB.structure Definition TopologicalNmodule := - {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}. - -Section TopologicalNmodule_theory. -Variable (E : topologicalType) (F : TopologicalNmodule.type) (U : set_system E). - -(** TODO: - We have observed one thing: - `pseudometric_normedZmodType` is morally a `topologicalNmodule` - but `topologicalNmodule` is defined later in `tvs.v` (which imports `pseudometric_normed_zmodule.v`). - We think that it should be defined at the beginning of `pseudometric_normed_zmodule.v` and that - `pseudometric_normedZmodType` should be defined using `topologicalNmodule`. - We have realized this because of the lemmas such as `cvgD/fun_cvgD` that we needed to duplicate. *) -Lemma fun_cvgD {FF : Filter U} (f g : E -> F) a b : - f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b. -Proof. -move=> fa ga. -by apply: continuous2_cvg; [exact: (add_continuous (a, b))|by []..]. -Qed. - -Lemma cvg_sum (I : Type) (r : seq I) (P : pred I) - (Ff : I -> E -> F) (Fa : I -> F) : - Filter U -> (forall i, P i -> Ff i x @[x --> U] --> Fa i) -> - \sum_(i <- r | P i) Ff i x @[x --> U] --> \sum_(i <- r| P i) Fa i. -Proof. by move=> FF Ffa; apply: cvg_big => //; apply: add_continuous. Qed. - -Lemma sum_continuous (I : Type) (r : seq I) (P : pred I) (f : I -> E -> F) : - (forall i : I, P i -> continuous (f i)) -> - continuous (fun x1 : E => \sum_(i <- r | P i) f i x1). -Proof. by move=> FC0; apply: continuous_big => //; apply: add_continuous. Qed. - -End TopologicalNmodule_theory. - -HB.mixin Record TopologicalNmodule_isTopologicalZmodule M - & Topological M & GRing.Zmodule M := { - opp_continuous : continuous (-%R : M -> M) ; -}. - -#[short(type="topologicalZmodType")] -HB.structure Definition TopologicalZmodule := - {M of TopologicalNmodule M & GRing.Zmodule M - & TopologicalNmodule_isTopologicalZmodule M}. - -Section TopologicalZmoduleTheory. -Variables (M : topologicalZmodType). - -Lemma sub_continuous : continuous (fun x : M * M => x.1 - x.2). -Proof. -move=> x; apply: (@continuous_comp _ _ _ (fun x => (x.1, - x.2)) - (fun x : M * M => x.1 + x.2)); last exact: add_continuous. -apply: cvg_pair; first exact: cvg_fst. -by apply: continuous_comp; [exact: cvg_snd|exact: opp_continuous]. -Qed. - -Lemma fun_cvgN (F : topologicalZmodType) (U : set_system M) {FF : Filter U} - (f : M -> F) a : - f @ U --> a -> \- f @ U --> - a. -Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed. - -End TopologicalZmoduleTheory. - -HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M - & Topological M & GRing.Zmodule M := { - sub_continuous : continuous (fun x : M * M => x.1 - x.2) ; -}. - -HB.builders Context M & PreTopologicalNmodule_isTopologicalZmodule M. - -Let opp_continuous : continuous (-%R : M -> M). -Proof. -move=> x; rewrite /continuous_at. -rewrite -(@eq_cvg _ _ _ (fun x => 0 - x)); first by move=> y; exact: add0r. -rewrite -[- x]add0r. -apply: (@continuous_comp _ _ _ (fun x => (0, x)) (fun x : M * M => x.1 - x.2)). - exact: cvg_pair. -exact: sub_continuous. -Qed. - -Let add_continuous : continuous (fun x : M * M => x.1 + x.2). -Proof. -move=> x; rewrite /continuous_at. -rewrite -(@eq_cvg _ _ _ (fun x => x.1 - (- x.2))). - by move=> y; rewrite opprK. -rewrite -[in x.1 + _](opprK x.2). -apply: (@continuous_comp _ _ _ (fun x => (x.1, - x.2)) (fun x => x.1 - x.2)). - apply: cvg_pair; first exact: cvg_fst. - by apply: continuous_comp; [exact: cvg_snd|exact: opp_continuous]. -exact: sub_continuous. -Qed. - -HB.instance Definition _ := - PreTopologicalNmodule_isTopologicalNmodule.Build M add_continuous. - -HB.instance Definition _ := - TopologicalNmodule_isTopologicalZmodule.Build M opp_continuous. - -HB.end. - #[short(type="preTopologicalLmodType")] HB.structure Definition PreTopologicalLmodule (K : numDomainType) := {M of Topological M & GRing.Lmodule K M}. @@ -267,129 +164,6 @@ HB.instance Definition _ := HB.end. -HB.mixin Record PreUniformNmodule_isUniformNmodule M & PreUniformNmodule M := { - add_unif_continuous : unif_continuous (fun x : M * M => x.1 + x.2) -}. - -HB.structure Definition UniformNmodule := - {M of PreUniformNmodule M & PreUniformNmodule_isUniformNmodule M}. - -HB.mixin Record UniformNmodule_isUniformZmodule M - & Uniform M & GRing.Zmodule M := { - opp_unif_continuous : unif_continuous (-%R : M -> M) -}. - -HB.structure Definition UniformZmodule := - {M of UniformNmodule M & GRing.Zmodule M & UniformNmodule_isUniformZmodule M}. - -HB.factory Record PreUniformNmodule_isUniformZmodule M - & Uniform M & GRing.Zmodule M := { - sub_unif_continuous : unif_continuous (fun x : M * M => x.1 - x.2) -}. - -HB.builders Context M & PreUniformNmodule_isUniformZmodule M. - -Lemma opp_unif_continuous : unif_continuous (-%R : M -> M). -Proof. -have unif : unif_continuous (fun x => (0, x) : M * M). - move=> /= U [[]] /= U1 U2 [] U1e U2e /subsetP U12. - apply: filterS U2e => x xU2/=. - have /U12 : ((0, 0), x) \in U1 `*` U2. - by rewrite in_setX/= (mem_set xU2) andbT inE; exact: entourage_refl. - by rewrite inE/= => -[[[a1 a2] [b1 b2]]]/= /[swap]-[] -> -> <-. -move=> /= U /sub_unif_continuous /unif /=. -rewrite -comp_preimage/= /comp/= /nbhs/=. -congr entourage => /=; rewrite eqEsubset. -by split=> x; rewrite /map_pair/= !sub0r. -Qed. - -Lemma add_unif_continuous : unif_continuous (fun x : M * M => x.1 + x.2). -Proof. -have unif: unif_continuous (fun x => (x.1, -x.2) : M * M). - move=> /= U [[]]/= U1 U2 [] U1e /opp_unif_continuous. - rewrite /nbhs/= => U2e /subsetP U12. - apply: (@filterS _ _ entourage_filter - ((fun xy => (xy.1.1, xy.2.1, (-xy.1.2, -xy.2.2))) @^-1` (U1 `*` U2))). - move=> /= [] [] a1 a2 [] b1 b2/= [] ab1 ab2. - have /U12 : (a1, b1, (-a2, -b2)) \in U1 `*` U2 by rewrite !inE. - by rewrite /map_pair inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-. - exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split. - by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)). -move=> /= U /sub_unif_continuous/unif; rewrite /nbhs/=. -rewrite -comp_preimage/=/comp/=. -by congr entourage; rewrite eqEsubset; split=> x /=; rewrite /map_pair !opprK. -Qed. - -HB.instance Definition _ := - PreUniformNmodule_isUniformNmodule.Build M add_unif_continuous. -HB.instance Definition _ := - UniformNmodule_isUniformZmodule.Build M opp_unif_continuous. - -HB.end. - -Section UniformZmoduleTheory. -Variables (M : UniformZmodule.type). - -Lemma sub_unif_continuous : unif_continuous (fun x : M * M => x.1 - x.2). -Proof. -suff unif: unif_continuous (fun x => (x.1, - x.2) : M * M). - by move=> /= U /add_unif_continuous/unif; rewrite /nbhs/= -comp_preimage. -move=> /= U [[]]/= U1 U2 [] U1e /opp_unif_continuous. -rewrite /nbhs/= => U2e /subsetP U12. -apply: (@filterS _ _ entourage_filter - ((fun xy => (xy.1.1, xy.2.1, (- xy.1.2, - xy.2.2))) @^-1` (U1 `*` U2))). - move=> /= [] [] a1 a2 [] b1 b2/= [] ab1 ab2. - have /U12 : (a1, b1, (-a2, -b2)) \in U1 `*` U2 by rewrite !inE. - by rewrite /map_pair inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-. -exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split. -by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)). -Qed. - -End UniformZmoduleTheory. - -HB.structure Definition PreUniformLmodule (K : numDomainType) := - {M of Uniform M & GRing.Lmodule K M}. - -HB.mixin Record PreUniformLmodule_isUniformLmodule (R : numFieldType) M - & PreUniformLmodule R M := { - scale_unif_continuous : unif_continuous (fun z : R^o * M => z.1 *: z.2) ; -}. - -HB.structure Definition UniformLmodule (R : numFieldType) := - {M of UniformZmodule M & GRing.Lmodule R M - & PreUniformLmodule_isUniformLmodule R M}. - -HB.factory Record UniformNmodule_isUniformLmodule (R : numFieldType) M - & PreUniformLmodule R M := { - scale_unif_continuous : unif_continuous (fun z : R^o * M => z.1 *: z.2) ; -}. - -HB.builders Context R M & UniformNmodule_isUniformLmodule R M. - -Lemma opp_unif_continuous : unif_continuous (-%R : M -> M). -Proof. -have unif: unif_continuous (fun x => (-1, x) : R^o * M). - move=> /= U [[]] /= U1 U2 [] U1e U2e /subsetP U12. - rewrite /nbhs/=. - apply: filterS U2e => x xU2/=. - have /U12 : ((-1, -1), x) \in U1 `*` U2. - rewrite in_setX/= (mem_set xU2) andbT. - by apply/mem_set; exact: entourage_refl. - by rewrite /map_pair inE/= => [[[]]] [] a1 a2 [] b1 b2/= abU [] {2}<- <- <-/=. -move=> /= U /scale_unif_continuous/unif/=. -rewrite /nbhs/=. -rewrite -comp_preimage/=/comp/=. -by congr entourage; rewrite eqEsubset; split=> x /=; rewrite /map_pair !scaleN1r. -Qed. - -#[warning="-HB.no-new-instance"] -HB.instance Definition _ := - UniformNmodule_isUniformZmodule.Build M opp_unif_continuous. -HB.instance Definition _ := - PreUniformLmodule_isUniformLmodule.Build R M scale_unif_continuous. - -HB.end. - HB.mixin Record Uniform_isConvexTvs (R : numDomainType) E & Uniform E & GRing.Lmodule R E := { locally_convex : exists2 B : set_system E, @@ -398,7 +172,7 @@ HB.mixin Record Uniform_isConvexTvs (R : numDomainType) E #[short(type="convexTvsType")] HB.structure Definition ConvexTvs (R : numDomainType) := - {E of Uniform_isConvexTvs R E & Uniform E & TopologicalLmodule R E}. + {E of Uniform_isConvexTvs R E & Uniform E & UniformZmodule E & TopologicalLmodule R E}. #[short(type="subConvexTvsType")] HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) @@ -460,6 +234,33 @@ Qed. HB.instance Definition _ := TopologicalZmodule_isTopologicalLmodule.Build R sub_init_topo scale_sub. +Let add_unif_continuous : + unif_continuous (fun x : sub_init_topo * sub_init_topo => x.1 + x.2). +Proof. +apply/initial_unif_continuous_comp. +rewrite (_ : _ \o _ = (fun x => x.1 + x.2) \o (fun x => (val x.1, val x.2)))/=. + by apply/funext => x/=; exact: linearD. +apply: unif_continuous_comp; last exact: add_unif_continuous. +by apply: pair_unif_continuous => //=; + [exact: initial_unif_continuous_comp_fst| + exact: initial_unif_continuous_comp_snd]. +Qed. + +HB.instance Definition _ := + PreUniformNmodule_isUniformNmodule.Build sub_init_topo add_unif_continuous. + +Let opp_unif_continuous : unif_continuous (-%R : sub_init_topo -> sub_init_topo). +Proof. +apply/initial_unif_continuous_comp. +rewrite (_ : _ \o _ = (fun x => - x) \o val)/=. + by apply/funext => x/=; exact: linearN. +by apply: unif_continuous_comp; + [exact: initial_unif_continuous|exact: opp_unif_continuous]. +Qed. + +HB.instance Definition _ := + UniformNmodule_isUniformZmodule.Build sub_init_topo opp_unif_continuous. + Local Open Scope convex_scope. Let locally_convex_sub : exists2 B : set_system sub_init_topo, @@ -541,7 +342,7 @@ HB.builders Context R E & PreTopologicalLmod_isConvexTvs R E. Definition entourage : set_system (E * E) := fun P => exists (U : set E), nbhs (0 : E) U /\ - (forall xy : E * E, (xy.1 - xy.2) \in U -> xy \in P). + (forall xy : E * E, (xy.1 - xy.2) \in U -> xy \in P). Let nbhs0N (U : set E) : nbhs (0 : E) U -> nbhs (0 : E) (-%R @` U). Proof. exact/nbhs0N_subproof/scale_continuous. Qed. @@ -566,14 +367,14 @@ split; first by exists [set: E]; split; first exact: filter_nbhsT. by move=> P Q PQ [U [HU Hxy]]; exists U; split=> [|xy /Hxy /[!inE] /PQ]. Qed. -Local Lemma entourage_refl (A : set (E * E)) : +Let entourage_refl (A : set (E * E)) : entourage A -> [set xy | xy.1 = xy.2] `<=` A. Proof. move=> [U [U0 Uxy]] xy eq_xy; apply/set_mem/Uxy; rewrite eq_xy subrr. apply/mem_set; exact: nbhs_singleton. Qed. -Local Lemma entourage_inv (A : set (E * E)) : +Let entourage_inv (A : set (E * E)) : entourage A -> entourage A^-1%relation. Proof. move=> [/= U [U0 Uxy]]; exists (-%R @` U); split; first exact: nbhs0N. @@ -581,7 +382,7 @@ move=> xy /set_mem /=; rewrite -opprB => [[yx] Uyx] /oppr_inj yxE. by apply/Uxy/mem_set; rewrite /= -yxE. Qed. -Local Lemma entourage_split_ex (A : set (E * E)) : entourage A -> +Let entourage_split_ex (A : set (E * E)) : entourage A -> exists2 B : set (E * E), entourage B & (B \; B)%relation `<=` A. Proof. move=> [/= U] [U0 Uxy]; rewrite /entourage /=. @@ -596,7 +397,7 @@ rewrite [_ - _](_ : _ = (xy.1 - z) + (z - xy.2)); first by rewrite addrA subrK. exact: (Wadd (xy.1 - z,z - xy.2)). Qed. -Local Lemma nbhsE : nbhs = nbhs_ entourage. +Let nbhsE : nbhs = nbhs_ entourage. Proof. have lem : -1 != 0 :> R by rewrite oppr_eq0 oner_eq0. rewrite /nbhs_ /=; apply/funext => x; rewrite /filter_from/=. @@ -625,17 +426,59 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E entourage_inv entourage_split_ex nbhsE. - HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build E add_continuous. HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R E scale_continuous. +Let nbhs0_split (U : set E) : nbhs 0 U -> + exists2 V : set E, nbhs 0 V & forall u v, V u -> V v -> U (u + v). +Proof. +move=> U0. +have : nbhs ((0 : E, 0 : E).1 + (0 : E, 0 : E).2) U. + by rewrite /= add0r. +move/add_continuous => [[/= A B] [A0 B0] ABU]. +exists (A `&` B); first exact: filterI A0 B0. +move=> u v [Au _] [_ Bv]. +exact: (ABU (u, v)). +Qed. + +Let add_unif_continuous : unif_continuous (fun x : E * E => x.1 + x.2). +Proof. +move=> P /= [U [U0 UP]]. +have [V V0 VU] := nbhs0_split U0. +pose A := [set x | x.1 - x.2 \in V]. +have entA : @entourage A by exists V; split=> // x xV; rewrite /A inE. +exists (A, A) => //=. +move=> -[[x1 y1] [x2 y2]] /= [Ax Ay]. +exists ((x1, x2), (y1, y2)) => //=. +apply/set_mem/UP => /=. +rewrite /= opprD addrACA inE. +by apply: VU; [exact/set_mem/Ax|exact/set_mem/Ay]. +Qed. + +HB.instance Definition _ := + PreUniformNmodule_isUniformNmodule.Build E add_unif_continuous. + +Let opp_unif_continuous : unif_continuous (-%R : E -> E). +Proof. +move=> P /= [U [U0 UP]]. +exists [set z | U (- z)]; split. + have /opp_continuous : nbhs (- 0) U by rewrite oppr0. + exact. +move=> [x y] /= Uxy. +apply: UP => /=. +by rewrite -opprD. +Qed. + +HB.instance Definition _ := + UniformNmodule_isUniformZmodule.Build E opp_unif_continuous. + HB.instance Definition _ := Uniform_isConvexTvs.Build R E locally_convex. HB.end. Section ConvexTvs_numDomain. -Context (R : numDomainType) (E : convexTvsType R) (U : set E). +Context {R : numDomainType} (E : convexTvsType R) (U : set E). Lemma nbhs0N : nbhs 0 U -> nbhs 0 (-%R @` U). Proof. exact/nbhs0N_subproof/scale_continuous. Qed. @@ -671,26 +514,7 @@ Unshelve. all: by end_near. Qed. End ConvexTvs_numField. Section standard_topology. -Variable R : numFieldType. - -(** NB: we have almost the same proof in `pseudometric_normed_Zmodule.v` *) -Let standard_add_continuous : continuous (fun x : R^o * R^o => x.1 + x.2). -Proof. -move=> [/= x y]; apply/cvgrPdist_lt=> _/posnumP[e]; near=> a b => /=. -by rewrite opprD addrACA normm_lt_split. -Unshelve. all: by end_near. Qed. - -Let standard_scale_continuous : continuous (fun z : R^o * R^o => z.1 *: z.2). -Proof. -move=> [/= k x]; apply/cvgrPdist_lt => _/posnumP[e]; near +oo_R => M. -near=> l z => /=; have M0 : 0 < M by []. -rewrite (@distm_lt_split _ _ (k *: z)) // -?(scalerBr, scalerBl) normrM. - rewrite (@le_lt_trans _ _ (M * `|x - z|)) ?ler_wpM2r -?ltr_pdivlMl//. - by near: z; apply: cvgr_dist_lt; rewrite // mulr_gt0 ?invr_gt0. -rewrite (@le_lt_trans _ _ (`|k - l| * M)) ?ler_wpM2l -?ltr_pdivlMr//. - by near: z; near: M; exact: (@cvg_bounded _ R^o _ _ _ _ _ (@cvg_refl _ _)). -by near: l; apply: cvgr_dist_lt; rewrite // divr_gt0. -Unshelve. all: by end_near. Qed. +Context {R : numFieldType}. Local Open Scope convex_scope. @@ -717,10 +541,16 @@ move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. by exists (ball x r) => //=; split; [exists x, r|exact: ballxx]. Qed. +(* +Check R^o : TopologicalNmodule.type. + HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build R^o standard_add_continuous. +*) + HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R R^o standard_scale_continuous. + HB.instance Definition _ := Uniform_isConvexTvs.Build R R^o standard_locally_convex_set. @@ -729,18 +559,6 @@ End standard_topology. Section prod_ConvexTvs. Context (K : numFieldType) (E F : convexTvsType K). -Local Lemma prod_add_continuous : - continuous (fun x : (E * F) * (E * F) => x.1 + x.2). -Proof. -move => [/= xy1 xy2] /= U /= [] [A B] /= [nA nB] nU. -have [/= A0 [A01 A02] nA1] := @add_continuous E (xy1.1, xy2.1) _ nA. -have [/= B0 [B01 B02] nB1] := @add_continuous F (xy1.2, xy2.2) _ nB. -exists ([set xy | A0.1 xy.1 /\ B0.1 xy.2], [set xy | A0.2 xy.1 /\ B0.2 xy.2]). - by split; [exists (A0.1, B0.1)|exists (A0.2, B0.2)]. -move => [[x1 y1][x2 y2]] /= [] [] a1 b1 [] a2 b2. -by apply: nU; split; [exact: (nA1 (x1, x2))|exact: (nB1 (y1, y2))]. -Qed. - Local Lemma prod_scale_continuous : continuous (fun z : K^o * (E * F) => z.1 *: z.2). Proof. @@ -778,10 +596,9 @@ split. by apply/set_mem/Bcf; [exact/mem_set|exact/mem_set|exact/mem_set]. Qed. -HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build - (E * F)%type prod_add_continuous. HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build K (E * F)%type prod_scale_continuous. + HB.instance Definition _ := Uniform_isConvexTvs.Build K (E * F)%type prod_locally_convex. @@ -811,7 +628,7 @@ Context {K : numDomainType} {E : NbhsLmodule.type K} {F : NbhsZmodule.type} {s : K -> F -> F}. Definition lcfun : {pred E -> F} := - mem [set f | linear_for s f /\ continuous f ]. + mem [set f | linear_for s f /\ continuous f]. Definition lcfun_key : pred_key lcfun. Proof. exact. Qed. diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index d20977546c..ad27fb5a56 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -4,7 +4,7 @@ From mathcomp Require Import boot order algebra all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import interval_inference reals topology_structure. -From mathcomp Require Import uniform_structure order_topology. +From mathcomp Require Import uniform_structure product_topology order_topology. From mathcomp Require Import pseudometric_structure. (**md**************************************************************************) @@ -179,6 +179,33 @@ HB.instance Definition _ := @Nbhs_isUniform.Build (initial_topology f) End initial_uniform. +Section initial_unif_continuous. +Context {T : choiceType} {U : uniformType} (f : T -> U). + +Lemma initial_unif_continuous : unif_continuous (f : initial_topology f -> U). +Proof. by move=> A entA; by exists A. Qed. + +Lemma initial_unif_continuous_comp + (V : uniformType) (g : V -> initial_topology f) : + unif_continuous (f \o g : V -> U) -> unif_continuous g. +Proof. by move=> fg /= A [B entB BA]; apply: filterS _ _ BA _; exact: fg. Qed. + +Lemma initial_unif_continuous_comp_fst (V : uniformType) : + unif_continuous (fun x : initial_topology f * V => f x.1). +Proof. +by apply: unif_continuous_comp; + [exact: fst_unif_continuous|exact: initial_unif_continuous]. +Qed. + +Lemma initial_unif_continuous_comp_snd (V : uniformType) : + unif_continuous (fun x : V * initial_topology f => f x.2). +Proof. +by apply: unif_continuous_comp; + [exact: snd_unif_continuous|exact: initial_unif_continuous]. +Qed. + +End initial_unif_continuous. + HB.instance Definition _ (pS : pointedType) (U : uniformType) (f : pS -> U) := Pointed.on (initial_topology f). diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v index bcb229411d..b7b35a8d7a 100644 --- a/theories/topology_theory/metric_structure.v +++ b/theories/topology_theory/metric_structure.v @@ -92,6 +92,44 @@ Qed. End metric_lemmas. +Section prod_metric. +Context {K : numDomainType} (T U : metricType K). + +Let M := (T * U)%type. + +Let cmp (x y : M) : mdist x.1 y.1 >=< mdist x.2 y.2. +Proof. by apply: real_comparable; apply: ger0_real; exact: mdist_ge0. Qed. + +Definition prod_mdist (x y : M) := maxr (mdist x.1 y.1) (mdist x.2 y.2). + +Let prod_mdist_ge0 x y : 0 <= prod_mdist x y. +Proof. by rewrite /prod_mdist comparable_le_max// mdist_ge0. Qed. + +Let prod_mdist_positivity x y : prod_mdist x y = 0 -> x = y. +Proof. +rewrite /prod_mdist /= => m0. +have le01 : mdist x.1 y.1 <= 0 by rewrite -m0 comparable_le_max// lexx. +have le02 : mdist x.2 y.2 <= 0 by rewrite -m0 comparable_le_max// lexx orbT. +have eq01 : mdist x.1 y.1 = 0 by apply/le_anti; rewrite le01 mdist_ge0. +have eq02 : mdist x.2 y.2 = 0 by apply/le_anti; rewrite le02 mdist_ge0. +rewrite (surjective_pairing x) (surjective_pairing y). +by congr pair; exact: mdist_positivity. +Qed. + +Let ballEprod_mdist x d : ball x d = [set y | prod_mdist x y < d]. +Proof. +apply/seteqP; split => [y []|y /= xyd]. + rewrite !ballEmdist/= /prod_mdist => b1 b2. + by rewrite comparable_gt_max// b1 b2. +rewrite /ball/= /prod_ball/= !ballEmdist/=. +by apply/andP; rewrite -comparable_gt_max. +Qed. + +HB.instance Definition _ := PseudoMetric_isMetric.Build K (T * U)%type + prod_mdist_ge0 prod_mdist_positivity ballEprod_mdist. + +End prod_metric. + HB.factory Record isMetric (K : numFieldType) (M : Type) & Choice M := { mdist : M -> M -> K ; mdistxx : forall x, mdist x x = 0 ; diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v index b6493b8393..85246636b7 100644 --- a/theories/topology_theory/product_topology.v +++ b/theories/topology_theory/product_topology.v @@ -13,11 +13,11 @@ From mathcomp Require Import uniform_structure pseudometric_structure compact. (* - topology *) (* - uniform space *) (* - pseudometric space *) +(* - metric space *) (******************************************************************************) Import Order.TTheory GRing.Theory Num.Theory. -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -70,7 +70,6 @@ by exists (a, q) => //=; apply: pqA; split => //; exact: nbhs_singleton. Qed. (** product of two uniform spaces *) - Section prod_Uniform. Local Open Scope relation_scope. Context {U V : uniformType}. @@ -154,13 +153,69 @@ HB.instance Definition _ := Nbhs_isUniform.Build (U * V)%type End prod_Uniform. +Lemma entourage_prod_exS (U V : uniformType) (P : set ((U * V) * (U * V))) : + entourage P -> + exists (A : set (U * U)) (B : set (V * V)), + [/\ entourage A, entourage B & + [set x | A (x.1.1, x.2.1) /\ B (x.1.2, x.2.2)] `<=` P]. +Proof. +move=> [[A B] /= [entA entB] ABP]. +exists A, B; split => // -[[x1 y1] [x2 y2]] /= [Axx Byy]. +have /ABP [[[a b] [c d]] Pabcd]/= : (A `*` B) ((x1, x2), (y1, y2)) by []. +by case=> <- <- <- <-. +Qed. + +(**md TODO: mv to `unstable.v`? *) +Definition interchange_prod {T U} (x : (T * U) * (T * U)) : (T * T) * (U * U) := + (x.1.1, x.2.1, (x.1.2, x.2.2)). + +Lemma entourage_interchange_prod {U V : uniformType} + (B : set (U * U)) (C : set (V * V)) : +entourage B -> entourage C -> entourage (interchange_prod @^-1` (B `*` C)). +Proof. +move=> entB entC; exists (B, C) => //= -[[x1 x2] [x3 x4]] [/= HB HC]. +by exists (x1, x3, (x2, x4)). +Qed. + +Section unif_continuous_pair. +Context {U V W : uniformType}. + +Lemma pair_unif_continuous (f : U -> V) (g : U -> W) : + unif_continuous f -> unif_continuous g -> + unif_continuous (fun x => (f x, g x)). +Proof. +move=> cf cg A entA. +have [/= BC [entB entC] BCA] : exists2 BC, entourage BC.1 /\ entourage BC.2 & + interchange_prod @^-1` (BC.1 `*` BC.2) `<=` A. + move: entA => -[[B C]] entBD BCA; exists (B, C) => //=. + move=> [[x1 x2] [x3 x4]] [/=] Bx Cx. + have /= := BCA (x1, x3, _) (conj Bx Cx). + by move=> [[[a1 a2] [b1 b2]]]/= ? [<- <- <- <-]. +apply: (@filterS _ _ _ (map_pair f @^-1` BC.1 `&` (map_pair g) @^-1` BC.2)). + by move=> xy [Bxy Cxy]; exact: BCA. +by apply: filterI; [exact: cf|exact: cg]. +Qed. + +Lemma fst_unif_continuous : unif_continuous (@fst U V). +Proof. +move=> A entA; exists (A, setT) => /=; first by split => //; exact: entourageT. +by move=> [[x1 x2] [y1 y2]] [/= Ax _]; exists (x1, y1, (x2, y2)). +Qed. + +Lemma snd_unif_continuous : unif_continuous (@snd U V). +Proof. +move=> B entB; exists (setT, B) => /=; first by split => //; exact: entourageT. +by move=> [[x1 x2] [y1 y2]] [/= _ Bx]; exists (x1, y1, (x2, y2)). +Qed. + +End unif_continuous_pair. + (** product of two pseudoMetric spaces *) Section prod_PseudoMetric. Context {R : numDomainType} {U V : pseudoMetricType R}. Implicit Types (x y : U * V). -Definition prod_ball x (eps : R) y := - ball (fst x) eps (fst y) /\ ball (snd x) eps (snd y). +Definition prod_ball x (eps : R) y := ball x.1 eps y.1 /\ ball x.2 eps y.2. Lemma prod_ball_center x (eps : R) : 0 < eps -> prod_ball x eps x. Proof. by move=> /posnumP[?]. Qed. @@ -185,7 +240,8 @@ rewrite predeqE => P; split; last first. move=> [[A B]] /=; rewrite -!entourage_ballE. move=> [[_/posnumP[eA] sbA] [_/posnumP[eB] sbB] sABP]. exists (Num.min eA eB)%:num => //= -[[a b] [c d] [/= bac bbd]]. -suff /sABP [] : (A `*` B) ((a, c), (b, d)) by move=> [[??] [??]] ? [<-<-<-<-]. +suff /sABP [] : (A `*` B) ((a, c), (b, d)). + by move=> [[? ?] [? ?]] ? [<- <- <- <-]. (split; [apply: sbA|apply: sbB]) => /=. by apply: le_ball bac; rewrite num_le ge_min lexx. by apply: le_ball bbd; rewrite num_le ge_min lexx orbT. diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v index caa36a3e54..f4945b2033 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.v @@ -80,7 +80,6 @@ HB.structure Definition Uniform := HB.structure Definition PointedUniform := {T of PointedTopological T & Nbhs_isUniform_mixin T}. - HB.factory Record Nbhs_isUniform M & Nbhs M := { entourage : set_system (M * M); entourage_filter : Filter entourage; @@ -342,6 +341,10 @@ rewrite -image_sub => v [] u' /= Yfuu' <-. exact: YX. Qed. +Lemma unif_continuous_comp {U V W : uniformType} (f : U -> V) (g : V -> W) : + unif_continuous f -> unif_continuous g -> unif_continuous (g \o f). +Proof. by move=> cf cg A /cg /cf; exact. Qed. + Definition entourage_set (U : uniformType) (A : set ((set U) * (set U))) := exists2 B, entourage B & forall PQ, A PQ -> forall p q, PQ.1 p -> PQ.2 q -> B (p,q). From 3596cdaa717576a2c81585f7631dc48b58967214 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 30 Sep 2026 00:06:42 +0900 Subject: [PATCH 2/4] doc and changelog --- CHANGELOG_UNRELEASED.md | 23 +++++++++++++++- .../pseudometric_normed_Zmodule.v | 27 +++++++++++-------- theories/normedtype_theory/tvs.v | 18 ------------- 3 files changed, 38 insertions(+), 30 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 924253533c..ab6f17c925 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -36,6 +36,7 @@ - in `pseudometric_normed_Zmodule.v`: + lemma `PseudoMetricNormedZmod0_add_unif_continuous` + lemma `PseudoMetricNormedZmod0_opp_unif_continuous` + + lemma `standard_scale_continuous` ### Changed @@ -53,6 +54,24 @@ ### Changed +- moved from `tvs.v` to `pseudometric_normed_Zmodule.v` + + mixin `PreTopologicalNmodule_isTopologicalNmodule` + + structure `TopologicalNmodule` + + lemmas `fun_cvgD`, `cvg_sum`, `sum_continuous` + + mixin `TopologicalNmodule_isTopologicalZmodule` + + structure `TopologicalZmodule`, type `topologicalZmodType` + + lemmas `sub_continuous`, `fun_cvgN` + + factory `PreTopologicalNmodule_isTopologicalZmodule` + + mixin `PreUniformNmodule_isUniformNmodule` + + structure `UniformNmodule` + + mixin `UniformNmodule_isUniformZmodule` + + structure `UniformZmodule` + + factory `PreUniformNmodule_isUniformZmodule` + + lemma `sub_unif_continuous` + +- in `tvs.v`: + + structure `ConvexTvs` now inherits from `UniformZmodule` + ### Renamed - in `sequences.v`: @@ -63,6 +82,7 @@ - in `pseudometric_normed_Zmodule.v`: + from `pseudoMetricNormedZmodType` to `PseudoMetricNormedZmod0.type`: + * lemma `le0_ball0` * lemma `cvg_bounded` * lemma `bounded_cst` + from `realFieldType` to `numFieldType` @@ -77,7 +97,8 @@ + structure `PreUniformLmodule` + mixin `PreUniformLmodule_isUniformLmodule` + structure `UniformLmodule` - + factory `UniformNmodule_isUniformLmodule` (?) + + factory `UniformNmodule_isUniformLmodule` + + lemma `prod_add_continuous` (remains accessible via the generic `add_continuous` of `TopologicalNmodule.type`) ### Infrastructure diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 72a9672f3d..13cc132a4a 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -31,6 +31,21 @@ From mathcomp Require Import num_normedtype. (* *) (* ## Normed topological abelian groups *) (* ``` *) +(* PreTopologicalNmodule == HB class, join of Topological and Nmodule *) +(* TopologicalNmodule == HB class, PreTopologicalNmodule with a *) +(* continuous addition *) +(* PreTopologicalZmodule == HB class, join of Topological and Zmodule *) +(* topologicalZmodType == topological abelian group *) +(* The HB class is TopologicalZmodule, join *) +(* of TopologicalNmodule and Zmodule with a *) +(* continuous opposite operator *) +(* PreUniformNmodule == HB class, join of Uniform and Nmodule *) +(* UniformNmodule == HB class, join of Uniform and Nmodule *) +(* with a uniformly continuous addition *) +(* PreUniformZmodule == HB class, join of Uniform and Zmodule *) +(* UniformZmodule == HB class, join of UniformNmodule and *) +(* Zmodule with uniformly continuous *) +(* opposite operator *) (* PseudoMetricNormedZmod0 R == interface type for a normed topological *) (* abelian group equipped with a norm *) (* pseudoMetricNormedZmodType R == PseudoMetricNormedZmod0 R + Metric R *) @@ -279,7 +294,7 @@ End prod_TopologicalNmodule. Section prod_UniformNmodule. Context {E F : UniformNmodule.type}. -Lemma prod_add_unif_continuous : +Let prod_add_unif_continuous : unif_continuous (fun x : (E * F) * (E * F) => x.1 + x.2). Proof. move=> P /= /entourage_prod_exS[A [B [entA entB ABP]]]. @@ -834,15 +849,6 @@ HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build K (U * V)%type End prod_pseudoMetricNormedZmod. -(* -Section prod_pseudoMetricNormedZmod_new. -Context {K : numFieldType} {U V : pseudoMetricNormedZmodType K}. - -HB.instance Definition _ := isPseudoMetricNormedZmodule.Build _ (U * V)%type. - -End prod_pseudoMetricNormedZmod_new. -*) - Section prod_NormedModule_lemmas. Context {T : Type} {K : numDomainType} {U V : pseudoMetricNormedZmodType K}. @@ -946,7 +952,6 @@ End continuity_pseudoMetricNormedZmodType. (*#[deprecated(since="mathcomp-analysis 1.11.0", note="renamed to `oppr_continuous`")] Notation opp_continuous := oppr_continuous (only parsing).*) -(* TODO: generalize to R : numFieldType DONE?! *) Section hausdorff. #[deprecated(since="mathcomp-analysis 1.10.0", note="use `norm_hausdorff` instead")] diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index cfae49fc7c..dbc07cddb6 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -17,30 +17,12 @@ From mathcomp Require Import pseudometric_normed_Zmodule. (* NbhsZmodule == HB class, join of Nbhs and Zmodule *) (* NbhsLmodule K == HB class, join of Nbhs and Lmodule over K *) (* K is a numDomainType. *) -(* PreTopologicalNmodule == HB class, join of Topological and Nmodule *) -(* TopologicalNmodule == HB class, PreTopologicalNmodule with a *) -(* continuous addition *) -(* PreTopologicalZmodule == HB class, join of Topological and Zmodule *) -(* topologicalZmodType == topological abelian group *) -(* TopologicalZmodule == HB class, join of TopologicalNmodule and *) -(* Zmodule with a continuous opposite operator *) (* preTopologicalLmodType K == topological space and Lmodule over K *) (* K is a numDomainType *) (* The HB class is PreTopologicalLmodule. *) (* topologicalLmodType K == topologicalNmodule and Lmodule over K with a *) (* continuous scaling operation *) (* The HB class is TopologicalLmodule. *) -(* PreUniformNmodule == HB class, join of Uniform and Nmodule *) -(* UniformNmodule == HB class, join of Uniform and Nmodule with a *) -(* uniformly continuous addition *) -(* PreUniformZmodule == HB class, join of Uniform and Zmodule *) -(* UniformZmodule == HB class, join of UniformNmodule and Zmodule *) -(* with uniformly continuous opposite operator *) -(* PreUniformLmodule K == HB class, join of Uniform and Lmodule over K *) -(* K is a numDomainType. *) -(* UniformLmodule K == HB class, join of UniformNmodule and Lmodule *) -(* with a uniformly continuous scaling operation *) -(* K is a numFieldType. *) (* convexTvsType R == interface type for a locally convex *) (* tvs on a numDomain R *) (* A convex tvs is constructed over a uniform *) From c03c0d15c1a04f042c26a19742ce221de3927eda Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 30 Sep 2026 14:08:12 +0900 Subject: [PATCH 3/4] address comments --- CHANGELOG_UNRELEASED.md | 14 +- .../normedtype_theory/matrix_normedtype.v | 4 +- theories/normedtype_theory/normed_module.v | 58 +++-- .../pseudometric_normed_Zmodule.v | 203 +++++++++--------- theories/normedtype_theory/tvs.v | 2 +- 5 files changed, 152 insertions(+), 129 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ab6f17c925..3a3019d524 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -34,8 +34,8 @@ + definition `prod_mdist` - in `pseudometric_normed_Zmodule.v`: - + lemma `PseudoMetricNormedZmod0_add_unif_continuous` - + lemma `PseudoMetricNormedZmod0_opp_unif_continuous` + + lemma `PseudoMetricNormedZmodule_add_unif_continuous` + + lemma `PseudoMetricNormedZmodule_opp_unif_continuous` + lemma `standard_scale_continuous` ### Changed @@ -77,6 +77,13 @@ - in `sequences.v`: + `limn_einf_shift` -> `limn_einf_addl` + `series_le_cvg` -> `series_squeeze_is_cvgn` +- in `pseudometric_normed_Zmodule.v`: + + `PseudoMetricNormedZmod0` -> `PseudoMetricNormedZmodule` + + `pseudoMetricNormedZmodType` -> `metricNormedZmodType` + + `PseudoMetricNormedZmod` -> `MetricNormedZmodule` + +- in `normed_module.v`: + + `PseudoMetricNormedZmod_ConvexTvs_isNormedModule` -> `MetricNormedZmod_ConvexTvs_isNormedModule` ### Generalized @@ -100,6 +107,9 @@ + factory `UniformNmodule_isUniformLmodule` + lemma `prod_add_continuous` (remains accessible via the generic `add_continuous` of `TopologicalNmodule.type`) +- in `pseudometric_normred_Zmodule.v`: + + lemma `pseudoMetricNormedZModType_hausdorff` (deprecated since 1.10.0) + ### Infrastructure ### Misc diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index 008800bac1..fe89c0f33b 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -293,10 +293,10 @@ Section matrix_UniformNZmodule. Context {K : numFieldType} {m n : nat}. HB.instance Definition _ := PreUniformNmodule_isUniformNmodule.Build - 'M[K]_(m, n) (@PseudoMetricNormedZmod0_add_unif_continuous _ _). + 'M[K]_(m, n) (@PseudoMetricNormedZmodule_add_unif_continuous _ _). HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build - 'M[K]_(m, n) (@PseudoMetricNormedZmod0_opp_unif_continuous _ _). + 'M[K]_(m, n) (@PseudoMetricNormedZmodule_opp_unif_continuous _ _). End matrix_UniformNZmodule. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index adeecbd08d..9cbedefad5 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -86,25 +86,36 @@ Local Open Scope ring_scope. (** Modules with a norm depending on a numDomain *) -HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule - (K : numDomainType) V & PseudoMetricNormedZmod K V & ConvexTvs K V := { +HB.mixin Record MetricNormedZmod_ConvexTvs_isNormedModule + (K : numDomainType) V & MetricNormedZmodule K V & ConvexTvs K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. +#[deprecated(since="mathcomp-analysis 1.19.0", + use=MetricNormedZmod_ConvexTvs_isNormedModule)] +Notation PseudoMetricNormedZmod_ConvexTvs_isNormedModule x1 x2 := + (MetricNormedZmod_ConvexTvs_isNormedModule x1 x2). + +Module PseudoMetricNormedZmod_ConvexTvs_isNormedModule. +#[deprecated(since="mathcomp-analysis 1.19.0", + use=MetricNormedZmod_ConvexTvs_isNormedModule.Build)] +Notation Build x1 x2 x3 := + (MetricNormedZmod_ConvexTvs_isNormedModule.Build x1 x2 x3) (only parsing). +End PseudoMetricNormedZmod_ConvexTvs_isNormedModule. + #[short(type="normedModType")] HB.structure Definition NormedModule (K : numDomainType) := - {T of PseudoMetricNormedZmod K T & ConvexTvs K T - & PseudoMetricNormedZmod_ConvexTvs_isNormedModule K T}. + {T of MetricNormedZmodule K T & ConvexTvs K T + & MetricNormedZmod_ConvexTvs_isNormedModule K T}. #[short(type="subNormedModType")] HB.structure Definition SubNormedModule (R : numDomainType) - (V : normedModType R) (S : pred V) := + (V : normedModType R) (S : pred V) := { U of SubChoice V S U & NormedModule R U & @GRing.SubLmodule R V S U - & @Num.SubNormedZmodule(*Zmodule_isSubSemiNormed*) R V S U & - @SubConvexTvs R V S U}. + & @Num.SubNormedZmodule R V S U & @SubConvexTvs R V S U}. HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule - (K : numFieldType) V & PseudoMetricNormedZmod K V & GRing.Lmodule K V := { + (K : numFieldType) V & MetricNormedZmodule K V & GRing.Lmodule K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. @@ -158,7 +169,7 @@ HB.instance Definition _ := HB.instance Definition _ := Uniform_isConvexTvs.Build K V locally_convex_set. HB.instance Definition _ := - PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build K V normrZ. + MetricNormedZmod_ConvexTvs_isNormedModule.Build K V normrZ. HB.end. @@ -166,7 +177,7 @@ HB.end. HB.structure Definition NormedVector (K : numDomainType) := {T of NormedModule K T & Vector K T}. -(**md see also `Section standard_topology_pseudoMetricNormedZmod` in +(**md see also `Section standard_topology_metricNormedZmod` in `pseudometric_normed_Zmodule.v` *) Section standard_topology_normedMod. Variable R : numFieldType. @@ -177,7 +188,7 @@ HB.instance Definition _ := TopologicalZmodule_isTopologicalLmodule.Build *) HB.instance Definition _ := - PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build R R^o (@normrM _). + MetricNormedZmod_ConvexTvs_isNormedModule.Build R R^o (@normrM _). End standard_topology_normedMod. @@ -257,7 +268,7 @@ End numFieldNormedType. Import numFieldNormedType.Exports. Lemma within_continuous_compN {R : realFieldType} {K : numDomainType} - {U : pseudoMetricNormedZmodType K} (f : R -> U) (a b : R) : + {U : metricNormedZmodType K} (f : R -> U) (a b : R) : {within `[- b, - a], continuous f} -> {within `[a, b], continuous f \o -%R}. Proof. have [ab|ba _ |-> _] := ltgtP a b; last 2 first. @@ -374,10 +385,10 @@ HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R M erefl. HB.instance Definition _ := isPseudoMetricNormedZmodule.Build R M. HB.instance Definition _ := PreUniformNmodule_isUniformNmodule.Build - M (@PseudoMetricNormedZmod0_add_unif_continuous _ M). + M (@PseudoMetricNormedZmodule_add_unif_continuous _ M). HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build - M (@PseudoMetricNormedZmod0_opp_unif_continuous _ M). + M (@PseudoMetricNormedZmodule_opp_unif_continuous _ M). HB.instance Definition _ := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R M normrZ. @@ -1763,17 +1774,16 @@ apply/connected_intervalP/connected_continuous_connected => //. exact: segment_connected. Qed. -Section prod_NormedModule. +Section prod_normedModType. Context {K : numFieldType} {U V : normedModType K}. Let prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |. Proof. by rewrite prod_normE /= !normrZ maxr_pMr. Qed. -HB.instance Definition _ := - PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build K (U * V)%type - prod_norm_scale. +HB.instance Definition _ := MetricNormedZmod_ConvexTvs_isNormedModule.Build + K (U * V)%type prod_norm_scale. -End prod_NormedModule. +End prod_normedModType. (* Local properties in R *) @@ -2668,11 +2678,13 @@ HB.instance Definition _ (V : vectType R) := HB.instance Definition _ (V : vectType R) := isPseudoMetricNormedZmodule.Build _ (max_space V). -HB.instance Definition _ (V : vectType R) := PreUniformNmodule_isUniformNmodule.Build - (max_space V) (@PseudoMetricNormedZmod0_add_unif_continuous _ (max_space V)). +HB.instance Definition _ (V : vectType R) := + PreUniformNmodule_isUniformNmodule.Build (max_space V) + (@PseudoMetricNormedZmodule_add_unif_continuous _ (max_space V)). -HB.instance Definition _ (V : vectType R) := UniformNmodule_isUniformZmodule.Build - (max_space V) (@PseudoMetricNormedZmod0_opp_unif_continuous _ (max_space V)). +HB.instance Definition _ (V : vectType R) := + UniformNmodule_isUniformZmodule.Build (max_space V) + (@PseudoMetricNormedZmodule_opp_unif_continuous _ (max_space V)). HB.instance Definition _ (V : vectType R) := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V) diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 13cc132a4a..c4408fe807 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -46,10 +46,10 @@ From mathcomp Require Import num_normedtype. (* UniformZmodule == HB class, join of UniformNmodule and *) (* Zmodule with uniformly continuous *) (* opposite operator *) -(* PseudoMetricNormedZmod0 R == interface type for a normed topological *) +(* PseudoMetricNormedZmodule R == interface type for a normed topological *) (* abelian group equipped with a norm *) -(* pseudoMetricNormedZmodType R == PseudoMetricNormedZmod0 R + Metric R *) -(* The HB class is PseudoMetricNormedZmod. *) +(* metricNormedZmodType R == PseudoMetricNormedZmodule R + Metric R *) +(* The HB class is MetricNormedZmod. *) (* NormedZmoduleMetric == factory for pseudoMetricNormedZmodType *) (* based on metric structures *) (* ``` *) @@ -81,7 +81,6 @@ From mathcomp Require Import num_normedtype. Reserved Notation "[ 'bounded' E | x 'in' A ]" (at level 0, x name, format "[ 'bounded' E | x 'in' A ]"). -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -170,10 +169,10 @@ Variable (E : topologicalType) (F : TopologicalNmodule.type) (U : set_system E). (** TODO: We have observed one thing: - `pseudometric_normedZmodType` is morally a `topologicalNmodule` - but `topologicalNmodule` is defined later in `tvs.v` (which imports `pseudometric_normed_zmodule.v`). - We think that it should be defined at the beginning of `pseudometric_normed_zmodule.v` and that - `pseudometric_normedZmodType` should be defined using `topologicalNmodule`. + `metric_normedZmodType` is morally a `topologicalNmodule` + but `topologicalNmodule` was defined later in `tvs.v` (which imports `pseudometric_normed_zmodule.v`). + We now define it at the beginning of `pseudometric_normed_Zmodule.v` and that + `metric_normedZmodType` is now defined using `topologicalNmodule`. We have realized this because of the lemmas such as `cvgD/fun_cvgD` that we needed to duplicate. *) Lemma fun_cvgD {FF : Filter U} (f g : E -> F) a b : f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b. @@ -451,12 +450,22 @@ HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |) }. -HB.structure Definition PseudoMetricNormedZmod0 (R : numDomainType) := +(* TODO: introduce #[short(type="pseudoMetricNormedZmodType")] after MCA 1.20.0 *) +HB.structure Definition PseudoMetricNormedZmodule (R : numDomainType) := {T of Num.NormedZmodule R T & PseudoPointedMetric R T & NormedZmod_PseudoMetric_eq R T }. -Section PseudoMetricNormedZmod0_numDomainType. -Context {K : numDomainType} {V : PseudoMetricNormedZmod0.type K}. +#[deprecated(since="mathcomp-analysis 1.19.0", use=PseudoMetricNormedZmodule)] +Notation PseudoMetricNormedZmod0 x1 x2 := (PseudoMetricNormedZmodule x1 x2). + +Module PseudoMetricNormedZmod0. +#[deprecated(since="mathcomp-analysis 1.19.0", + use=PseudoMetricNormedZmodule.type)] +Notation type x1 := (PseudoMetricNormedZmodule.type x1) (only parsing). +End PseudoMetricNormedZmod0. + +Section PseudoMetricNormedZmodule_numDomainType. +Context {K : numDomainType} {V : PseudoMetricNormedZmodule.type K}. (**md Balls defined by the norm: *) Local Notation ball_norm := (ball_ (@Num.norm K V)). @@ -464,35 +473,10 @@ Local Notation ball_norm := (ball_ (@Num.norm K V)). Lemma ball_normE : ball_norm = ball. Proof. by rewrite pseudo_metric_ball_norm. Qed. -End PseudoMetricNormedZmod0_numDomainType. - -Lemma PseudoMetricNormedZmod0_add_unif_continuous {R : numFieldType} - (M : PseudoMetricNormedZmod0.type R) : unif_continuous (fun x : M * M => x.1 + x.2). -Proof. -apply/unif_continuousP => /= e e0. -exists (e / 2); first by rewrite divr_gt0. -move=> [/= [a1 a2] [b1 b2]]/=. -rewrite -ball_normE/=. -rewrite /ball/= /prod_ball/= => -[]. -rewrite -ball_normE/= => ab1 ab2. -by rewrite opprD addrACA (splitr e)// (le_lt_trans (ler_normD _ _))//= ltrD. -Qed. - -Lemma PseudoMetricNormedZmod0_opp_unif_continuous {R : numFieldType} - (M : PseudoMetricNormedZmod0.type R) : unif_continuous (-%R : M -> M). -Proof. -apply/unif_continuousP => /= e e0. -exists e => // -[a1 a2]/=. -by rewrite -ball_normE/= -opprD Num.normrN. -Qed. - -#[short(type="pseudoMetricNormedZmodType")] -HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) := - {T of PseudoMetricNormedZmod0 R T & Metric R T & UniformZmodule T}. +End PseudoMetricNormedZmodule_numDomainType. -(* was Section pseudoMetricNormedZmod_numDomainType. *) -Section PseudoMetricNormedZmod0_numDomainType. -Context {K : numDomainType} {V : PseudoMetricNormedZmod0.type K}. +Section PseudoMetricNormedZmodule_numDomainType. +Context {K : numDomainType} {V : PseudoMetricNormedZmodule.type K}. Lemma ball_open (x : V) (r : K) : open (ball x r). Proof. @@ -662,7 +646,7 @@ rewrite funeqE => A; rewrite /= !near_simpl (near_shift (y + x)). by rewrite (_ : _ \o _ = A \o f) // funeqE=> z; rewrite /= opprD addNKr addrNK. Qed. -End PseudoMetricNormedZmod0_numDomainType. +End PseudoMetricNormedZmodule_numDomainType. #[global] Hint Resolve normr_ge0 : core. Arguments cvgr_dist_lt {_ _ _ F FF}. Arguments cvgr_distC_lt {_ _ _ F FF}. @@ -684,9 +668,10 @@ Arguments cvgr0_norm_le {_ _ _ F FF}. #[global] Hint Extern 0 (is_true (`|?x| <= _)) => match goal with H : x \is_near _ |- _ => solve[near: x; now apply: cvgr0_norm_le] end : core. -Section PseudoMetricNormedZmod0_realDomainType. +Section PseudoMetricNormedZmodule_realDomainType. -Lemma le0_ball0 (R : realDomainType) (V : PseudoMetricNormedZmod0.type R) (a : V) (r : R) : +Lemma le0_ball0 (R : realDomainType) (V : PseudoMetricNormedZmodule.type R) + (a : V) (r : R) : r <= 0 -> ball a r = set0. Proof. move=> r0; rewrite -subset0 => y. @@ -694,10 +679,10 @@ rewrite -ball_normE /ball_/= ltNge => /negP; apply. by rewrite (le_trans r0). Qed. -End PseudoMetricNormedZmod0_realDomainType. +End PseudoMetricNormedZmodule_realDomainType. -Section PseudoMetricNormedZmod0_numFieldType. -Variables (R : numFieldType) (V : PseudoMetricNormedZmod0.type R). +Section PseudoMetricNormedZmodule_numFieldType. +Variables (R : numFieldType) (V : PseudoMetricNormedZmodule.type R). Lemma norm_hausdorff : hausdorff_space V. Proof. @@ -769,12 +754,44 @@ Proof. by move=> xlt ylt; rewrite -[y]opprK (@distm_lt_split 0) ?subr0 ?opprK ?add0r. Qed. -End PseudoMetricNormedZmod0_numFieldType. +End PseudoMetricNormedZmodule_numFieldType. #[global] Hint Extern 0 (hausdorff_space _) => solve[apply: norm_hausdorff] : core. +Lemma PseudoMetricNormedZmodule_add_unif_continuous {R : numFieldType} + (M : PseudoMetricNormedZmodule.type R) : + unif_continuous (fun x : M * M => x.1 + x.2). +Proof. +apply/unif_continuousP => /= e e0. +exists (e / 2); first by rewrite divr_gt0. +move=> [/= [a1 a2] [b1 b2]]/=. +rewrite -ball_normE/=. +rewrite /ball/= /prod_ball/= => -[]. +rewrite -ball_normE/= => ab1 ab2. +by rewrite opprD addrACA (splitr e)// (le_lt_trans (ler_normD _ _))//= ltrD. +Qed. + +Lemma PseudoMetricNormedZmodule_opp_unif_continuous {R : numFieldType} + (M : PseudoMetricNormedZmodule.type R) : + unif_continuous (-%R : M -> M). +Proof. +apply/unif_continuousP => /= e e0. +exists e => // -[a1 a2]/=. +by rewrite -ball_normE/= -opprD Num.normrN. +Qed. + +#[short(type="metricNormedZmodType")] +HB.structure Definition MetricNormedZmodule (R : numDomainType) := + {T of PseudoMetricNormedZmodule R T & Metric R T & UniformZmodule T}. + +#[deprecated(since="mathcomp-analysis 1.19.0", use=MetricNormedZmodule)] +Notation PseudoMetricNormedZmod R := (MetricNormedZmodule R) (only parsing). + +#[deprecated(since="mathcomp-analysis 1.19.0", use=metricNormedZmodType)] +Notation pseudoMetricNormedZmodType := metricNormedZmodType (only parsing). + HB.factory Record isPseudoMetricNormedZmodule - (K : numFieldType) T & PseudoMetricNormedZmod0 K T := { }. + (K : numFieldType) T & PseudoMetricNormedZmodule K T := { }. HB.builders Context K T & isPseudoMetricNormedZmodule K T. @@ -808,11 +825,12 @@ apply/cvgrPdist_lt=> _/posnumP[e]; near=> a => /=. by rewrite opprK addrC. Unshelve. all: by end_near. Qed. -HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build T opp_continuous. +HB.instance Definition _ := + TopologicalNmodule_isTopologicalZmodule.Build T opp_continuous. HB.end. -(* alternative definition of a PseudoMetricNormedZmod *) +(* alternative definition of a MetricNormedZmod *) HB.factory Record NormedZmoduleMetric (R : numDomainType) T & Num.NormedZmodule R T & Metric R T & isPointed T := { mdist_norm : forall x y : T, mdist x y = `|y - x| @@ -832,7 +850,7 @@ HB.instance Definition _ := HB.end. Section prod_pseudoMetricNormedZmod. -Context {K : numDomainType} {U V : pseudoMetricNormedZmodType K}. +Context {K : numDomainType} {U V : metricNormedZmodType K}. Lemma ball_prod_normE : ball = ball_ (fun x => `| x : U * V |). Proof. @@ -850,7 +868,7 @@ HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build K (U * V)%type End prod_pseudoMetricNormedZmod. Section prod_NormedModule_lemmas. -Context {T : Type} {K : numDomainType} {U V : pseudoMetricNormedZmodType K}. +Context {T : Type} {K : numDomainType} {U V : metricNormedZmodType K}. Lemma fcvgr2dist_ltP {F : set_system U} {G : set_system V} {FF : Filter F} {FG : Filter G} (y : U) (z : V) : @@ -887,33 +905,29 @@ HB.instance Definition _ := Num.NormedZmodule.on R^o. HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R R^o erefl. -Let standard_add_unif_continuous : unif_continuous (fun x : R^o * R^o => x.1 + x.2). -Proof. exact: PseudoMetricNormedZmod0_add_unif_continuous. Qed. - Let standard_add_continuous : continuous (fun x : R^o * R^o => x.1 + x.2). Proof. -by apply: unif_continuous_continuous; exact: standard_add_unif_continuous. +apply: unif_continuous_continuous. +exact: PseudoMetricNormedZmodule_add_unif_continuous. Qed. HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build R^o standard_add_continuous. HB.instance Definition _ := PreUniformNmodule_isUniformNmodule.Build - R^o standard_add_unif_continuous. - -Let standard_opp_unif_continuous : unif_continuous (-%R : R^o -> R^o). -Proof. exact: PseudoMetricNormedZmod0_opp_unif_continuous. Qed. + R^o (@PseudoMetricNormedZmodule_add_unif_continuous R^o R^o). Let standard_opp_continuous : continuous (-%R : R^o -> R^o). Proof. -by apply: unif_continuous_continuous; exact: standard_opp_unif_continuous. +apply: unif_continuous_continuous. +exact: PseudoMetricNormedZmodule_opp_unif_continuous. Qed. HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build R^o standard_opp_continuous. HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build - R^o standard_opp_unif_continuous. + R^o (@PseudoMetricNormedZmodule_opp_unif_continuous R^o R^o). End standard_topology_pseudoMetricNormedZmod. @@ -924,10 +938,9 @@ rewrite -(@ball_normE _ R^o) /ball_ set_itvE. by apply/seteqP; split => t/=; rewrite ltr_distlC. Qed. -(** Normed vector spaces have some continuous functions that are in fact -continuous on pseudoMetricNormedZmodType *) -Section continuity_pseudoMetricNormedZmodType. -Context {K : numFieldType} {V : pseudoMetricNormedZmodType K}. +(** Normed vector spaces have some continuous functions that are in fact continuous on metricNormedZmodType *) +Section continuity_metricNormedZmodType. +Context {K : numFieldType} {V : metricNormedZmodType K}. Lemma oppr_continuous : continuous (@GRing.opp V). Proof. @@ -948,22 +961,12 @@ move=> x; apply/(@cvgrPdist_lt K K^o) => e e0; apply/nbhs_normP. by exists e => //= y; exact/le_lt_trans/ler_dist_dist. Qed. -End continuity_pseudoMetricNormedZmodType. +End continuity_metricNormedZmodType. (*#[deprecated(since="mathcomp-analysis 1.11.0", note="renamed to `oppr_continuous`")] Notation opp_continuous := oppr_continuous (only parsing).*) -Section hausdorff. - -#[deprecated(since="mathcomp-analysis 1.10.0", note="use `norm_hausdorff` instead")] -Lemma pseudoMetricNormedZModType_hausdorff (R : numFieldType) - (V : pseudoMetricNormedZmodType R) : - hausdorff_space V. -Proof. exact: norm_hausdorff. Qed. - -End hausdorff. - Section at_left_right. -Variable R : numFieldType. +Context {R : numFieldType}. Lemma nbhs_right0P x (P : set R) : (\forall y \near x^'+, P y) <-> \forall e \near 0^'+, P (x + e). @@ -1053,7 +1056,7 @@ by rewrite at_leftN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK. Qed. Section at_left_right_pseudoMetricNormedZmod. -Variables (R : numFieldType) (V : PseudoMetricNormedZmod0.type R). +Variables (R : numFieldType) (V : PseudoMetricNormedZmodule.type R). Lemma nbhsr0P (P : set V) x : (\forall y \near x, P y) <-> @@ -1282,8 +1285,8 @@ rewrite in_itv/= !ltrD2l; apply/andP; split. by rewrite gtr_pMr// invf_lt1// ltr1n. Unshelve. all: by end_near. Qed. -Section pseudoMetricNormedZmod_numFieldType. -Variables (R : numFieldType) (V : PseudoMetricNormedZmod0.type R). +Section pseudoMetricNormedZmodule_numFieldType. +Variables (R : numFieldType) (V : PseudoMetricNormedZmodule.type R). Variables (I : Type) (F : set_system I) (FF : Filter F) (f : I -> V) (y : V). Lemma cvgr_norm_lty : @@ -1309,7 +1312,7 @@ Proof. by move=> Fy; near do exact: (cvgr_norm_ge y). Unshelve. all: by end_near. Qed. -End pseudoMetricNormedZmod_numFieldType. +End pseudoMetricNormedZmodule_numFieldType. Arguments cvgr_norm_lty {R V I F FF}. Arguments cvgr_norm_ley {R V I F FF}. Arguments cvgr_norm_gtNy {R V I F FF}. @@ -1332,8 +1335,7 @@ Definition nbhs_simpl := (nbhs_simpl,@nbhs_nbhs_norm,@filter_from_norm_nbhs). End NbhsNorm. Section continuous_within_itvP. -Context {R : realFieldType} {K : numDomainType} - {U : pseudoMetricNormedZmodType K}. +Context {R : realFieldType} {K : numDomainType} {U : metricNormedZmodType K}. Implicit Type f : R -> U. Let near_at_left (a : itv_bound R) b f eps : (a < BLeft b)%O -> 0 < eps -> @@ -1450,7 +1452,7 @@ Qed. End continuous_within_itvP. Lemma within_continuous_continuous {R : realFieldType} {K : numDomainType} - {U : pseudoMetricNormedZmodType K} a b (f : R -> U) x : (a <= b)%R -> + {U : metricNormedZmodType K} a b (f : R -> U) x : (a <= b)%R -> {within `[a, b], continuous f} -> x \in `]a, b[%R -> {for x, continuous f}. Proof. rewrite le_eqVlt => /predU1P[<- _|ab]. @@ -1464,8 +1466,8 @@ Definition near_simpl := (@near_simpl, @nbhs_normE, @filter_from_normE, Ltac near_simpl := rewrite ?near_simpl. End NearNorm. -Section cvg_composition_pseudometric. -Context {K : numFieldType} {V : pseudoMetricNormedZmodType K} {T : Type} +Section cvg_composition_metricNormedZmodType. +Context {K : numFieldType} {V : metricNormedZmodType K} {T : Type} (F : set_system T) {FF : Filter F}. Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a b : V). @@ -1555,11 +1557,11 @@ Unshelve. all: by end_near. Qed. Lemma norm_cvg0 f : `|f x| @[x --> F] --> (0:K^o) -> f @ F --> 0. Proof. by rewrite norm_cvg0P. Qed. -End cvg_composition_pseudometric. +End cvg_composition_metricNormedZmodType. Section within_continuous_lemmas. -Context {T : topologicalType} {K : numFieldType} - {V : pseudoMetricNormedZmodType K} (A : set T). +Context {T : topologicalType} {K : numFieldType} {V : metricNormedZmodType K} + (A : set T). Implicit Types f g : T -> V. Lemma within_continuousB f g : @@ -1590,7 +1592,7 @@ Lemma closure_ballE (R : numDomainType) (V : pseudoMetricType R) (c : V) (r : R) : closure (ball c r) = closed_ball c r. Proof. by []. Qed. -Lemma closed_ball0 (R : realDomainType) (V : pseudoMetricNormedZmodType R) +Lemma closed_ball0 (R : realDomainType) (V : metricNormedZmodType R) (v : V) (r : R) : r <= 0 -> closed_ball v r = set0. Proof. by move=> r0; rewrite -subset0 => w; rewrite /closed_ball le0_ball0// closure0. @@ -1624,8 +1626,8 @@ End Closed_Ball. #[deprecated(since="mathcomp-analysis 1.14.0", note="renamed to `closure_ballE`")] Notation closure_ball := closure_ballE (only parsing). -Section limit_composition_pseudometric. -Context {K : numFieldType} {V : pseudoMetricNormedZmodType K} {T : Type}. +Section limit_composition_metricNormedZmodType. +Context {K : numFieldType} {V : metricNormedZmodType K} {T : Type}. Context (F : set_system T) {FF : ProperFilter F}. Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a : V). @@ -1647,10 +1649,10 @@ move=> ?; apply: cvg_lim. exact: cvg_norm. Qed. -End limit_composition_pseudometric. +End limit_composition_metricNormedZmodType. Section domination. -Context {T : Type} {K : numDomainType} {V W : PseudoMetricNormedZmod0.type K}. +Context {T : Type} {K : numDomainType} {V W : PseudoMetricNormedZmodule.type K}. Definition dominated_by (h : T -> V) (k : K) (f : T -> W) (F : set_system T) := F [set x | `|f x| <= k * `|h x|]. @@ -1665,15 +1667,14 @@ Proof. by move=> FG f; exact: FG. Qed. End domination. -Lemma sub_dominatedr (T : Type) (K : numDomainType) - (V : pseudoMetricNormedZmodType K) +Lemma sub_dominatedr (T : Type) (K : numDomainType) (V : metricNormedZmodType K) (h : T -> V) (k : K) (f g : T -> V) (F : set_system T) (FF : Filter F) : (\forall x \near F, `|f x| <= `|g x|) -> dominated_by h k g F -> dominated_by h k f F. Proof. by move=> le_fg; apply: filterS2 le_fg => x; apply: le_trans. Qed. Section ex_dom_bound. -Context {T : Type} {K : numFieldType} {V W : PseudoMetricNormedZmod0.type K}. +Context {T : Type} {K : numFieldType} {V W : PseudoMetricNormedZmodule.type K}. Lemma ex_dom_bound (h : T -> V) (f : T -> W) (F : set_system T) {PF : ProperFilter F} : @@ -1708,7 +1709,7 @@ Qed. End ex_dom_bound. Definition bounded_near {T : Type} {K : numFieldType} - {V : PseudoMetricNormedZmod0.type K} + {V : PseudoMetricNormedZmodule.type K} (f : T -> V) (F : set_system T) := \forall M \near +oo, F [set x | `|f x| <= M]. @@ -1721,7 +1722,7 @@ Definition fun1 {T : Type} {K : numFieldType} : T -> K^o := fun=> 1. Arguments fun1 {T K} x /. Section bounded_near. -Context {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K}. +Context {T : Type} {K : numFieldType} {V : metricNormedZmodType K}. Lemma sub_boundedr (F G : set_system T) : F `=>` G -> (@bounded_near T K V)^~ G `<=` bounded_near^~ F. @@ -1773,7 +1774,7 @@ Unshelve. all: by end_near. Qed. End bounded_near. Section cvg_bounded. -Variables (R : numFieldType) (V : PseudoMetricNormedZmod0.type R). +Variables (R : numFieldType) (V : PseudoMetricNormedZmodule.type R). Lemma cvg_bounded {I} {F : set_system I} {FF : Filter F} (f : I -> V) (y : V) : f @ F --> y -> bounded_near f F. @@ -1796,7 +1797,7 @@ rewrite (@le_lt_trans _ _ (`|k - l| * M)) ?ler_wpM2l -?ltr_pdivlMr//. by near: l; apply: cvgr_dist_lt; rewrite // divr_gt0. Unshelve. all: by end_near. Qed. -Lemma bounded_cst (K : numFieldType) {V : PseudoMetricNormedZmod0.type K} +Lemma bounded_cst (K : numFieldType) {V : PseudoMetricNormedZmodule.type K} (k : V) T (A : set T) : [bounded k | _ in A]. Proof. rewrite /bounded_near; near=> M => t At /=. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index dbc07cddb6..ab87060054 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -154,7 +154,7 @@ HB.mixin Record Uniform_isConvexTvs (R : numDomainType) E #[short(type="convexTvsType")] HB.structure Definition ConvexTvs (R : numDomainType) := - {E of Uniform_isConvexTvs R E & Uniform E & UniformZmodule E & TopologicalLmodule R E}. + {E of Uniform_isConvexTvs R E & UniformZmodule E & TopologicalLmodule R E}. #[short(type="subConvexTvsType")] HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) From eb0377521263161321f4da7632723b6a4faa1944 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 1 Oct 2026 14:13:02 +0900 Subject: [PATCH 4/4] various generalizations --- CHANGELOG_UNRELEASED.md | 16 + theories/esum.v | 2 +- theories/ftc.v | 4 +- .../pseudometric_normed_Zmodule.v | 303 ++++++++---------- theories/normedtype_theory/tvs.v | 30 +- theories/numfun.v | 2 +- .../topology_theory/pseudometric_structure.v | 44 +++ 7 files changed, 200 insertions(+), 201 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3a3019d524..8e87d6262f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -37,6 +37,7 @@ + lemma `PseudoMetricNormedZmodule_add_unif_continuous` + lemma `PseudoMetricNormedZmodule_opp_unif_continuous` + lemma `standard_scale_continuous` + + notation `topologicalNmodType` ### Changed @@ -72,6 +73,11 @@ - in `tvs.v`: + structure `ConvexTvs` now inherits from `UniformZmodule` +- move to `pseudometric_structure.v`: + + definitions `closed_ball_`, `closed_ball` + + lemmas `closure_ballE`, `closed_ballxx`, `closed_ball_closed`, `subset_closed_ball`, + `subset_closure_half`, `le_closed_ball` + ### Renamed - in `sequences.v`: @@ -96,8 +102,18 @@ * lemma `bounded_funN` * lemma `bounded_funD` +- in `pseudometric_normed_Zmodule.v`: + + lemmas `cvgD`, `cvg0D`, `cvgD0`, `cvgN`, `cvgNP`, `cvgB`, `cvg0B`, `cvgB0`, `cvgN0`, + `cvg_sub0`, `cvg0`, `subr_cvg0` + + lemmas `within_continuousD`, `within_continuousB`, `within_continuousN` + + lemmas `le_closed_ball`, `closed_ball0` + ### Deprecated +- in `pseudometric_normed_Zmodule.v`: + + lemma `fun_cvgD` (use `cvgD` instead) + + lemma `fun_cvgN` (use `cvgN` instead) + ### Removed - in `tvs.v`: diff --git a/theories/esum.v b/theories/esum.v index 5faf6752e7..a6a94193b1 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -1016,7 +1016,7 @@ suff: ((fun n => C_ n - (A - B)) @ \oo --> (0 : R^o))%R. rewrite [X in X - _]esummable_nneseries_lim//; first exact/esummable_funepos. rewrite [X in _ - X]esummable_nneseries_lim//; first exact/esummable_funeneg. rewrite -EFinB; apply/cvg_lim => //; apply/fine_cvgP; split; last first. - exact: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB). + exact: (@cvg_sub0 _ _ _ _ _ (cst (A - B)%R)). apply: nearW => n; rewrite fin_num_abs; apply: le_lt_trans Pf => /=. by rewrite -nneseries_esum// (le_trans (lee_abs_sum _ _ _))// nneseries_lim_ge. have : ((fun x => A_ x - B_ x) @ \oo --> A - B)%R. diff --git a/theories/ftc.v b/theories/ftc.v index cf889b51d5..114d789dfc 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -592,7 +592,7 @@ have GacFa : G x @[x --> a^'+] --> (- c + F a)%R. apply/cvgrPdist_le => /= e e0; near=> t. rewrite opprB GFc; first by rewrite in_itv/=; apply/andP. by rewrite addNr normr0 ltW. - have := @cvgD _ _ _ _ Fap _ _ _ _ GFac Fa. + have := @cvgD _ _ _ Fap _ _ _ _ GFac Fa. rewrite (_ : (G \- F) + F = G)%R//. by apply/funext => x/=; rewrite subrK. have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R. @@ -601,7 +601,7 @@ have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R. apply/cvgrPdist_le => /= e e0; near=> t. rewrite opprB GFc; first by rewrite in_itv/=; apply/andP. by rewrite addNr normr0 ltW. - have := @cvgD _ _ _ _ Fbn _ _ _ _ GFbc Fb. + have := @cvgD _ _ _ Fbn _ _ _ _ GFbc Fb. rewrite (_ : G \- F + F = G)%R //. by apply/funext => x/=; rewrite subrK. have contF : {within `[a, b], continuous F}. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index c4408fe807..3e64d90b49 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -31,9 +31,12 @@ From mathcomp Require Import num_normedtype. (* *) (* ## Normed topological abelian groups *) (* ``` *) +(* NbhsZmodule == HB class, join of Nbhs and Zmodule *) +(* NbhsNmodule == HB class, join of Nbhs and Nmodule *) (* PreTopologicalNmodule == HB class, join of Topological and Nmodule *) -(* TopologicalNmodule == HB class, PreTopologicalNmodule with a *) -(* continuous addition *) +(* topologicalNmodType == PreTopologicalNmodule with a continuous *) +(* addition *) +(* The HB class is TopologicalNmodule. *) (* PreTopologicalZmodule == HB class, join of Topological and Zmodule *) (* topologicalZmodType == topological abelian group *) (* The HB class is TopologicalZmodule, join *) @@ -54,12 +57,6 @@ From mathcomp Require Import num_normedtype. (* based on metric structures *) (* ``` *) (* *) -(* ## Closed balls *) -(* ``` *) -(* closed_ball_ norm x e := [set y | norm (x - y) <= e] *) -(* closed_ball == closure of a ball *) -(* ``` *) -(* *) (* ## Domination *) (* ``` *) (* dominated_by h k f F == `|f| <= k * `|h|, near F *) @@ -125,7 +122,7 @@ by rewrite -(mulr_natr a) -(mulr_natr b) !mulfK. Qed. Section at_left_right_topologicalType. -Variables (R : numFieldType) (V : topologicalType) (f : R -> V) (x : R). +Context {R : numFieldType} {V : topologicalType} (f : R -> V) (x : R). Lemma cvg_at_right_filter (l : V) : f z @[z --> x] --> l -> f z @[z --> x^'+] --> l. @@ -161,44 +158,62 @@ HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M add_continuous : continuous (fun x : M * M => x.1 + x.2) ; }. +#[short(type="topologicalNmodType")] HB.structure Definition TopologicalNmodule := {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}. Section TopologicalNmodule_theory. -Variable (E : topologicalType) (F : TopologicalNmodule.type) (U : set_system E). - -(** TODO: - We have observed one thing: - `metric_normedZmodType` is morally a `topologicalNmodule` - but `topologicalNmodule` was defined later in `tvs.v` (which imports `pseudometric_normed_zmodule.v`). - We now define it at the beginning of `pseudometric_normed_Zmodule.v` and that - `metric_normedZmodType` is now defined using `topologicalNmodule`. - We have realized this because of the lemmas such as `cvgD/fun_cvgD` that we needed to duplicate. *) -Lemma fun_cvgD {FF : Filter U} (f g : E -> F) a b : - f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b. -Proof. -move=> fa ga. -by apply: continuous2_cvg; [exact: (add_continuous (a, b))|by []..]. -Qed. +Context {E : topologicalType} {F : topologicalNmodType} (U : set_system E). Lemma cvg_sum (I : Type) (r : seq I) (P : pred I) (Ff : I -> E -> F) (Fa : I -> F) : Filter U -> (forall i, P i -> Ff i x @[x --> U] --> Fa i) -> \sum_(i <- r | P i) Ff i x @[x --> U] --> \sum_(i <- r| P i) Fa i. -Proof. by move=> FF Ffa; apply: cvg_big => //; apply: add_continuous. Qed. +Proof. by move=> FF Ffa; apply: cvg_big => //; exact: add_continuous. Qed. Lemma sum_continuous (I : Type) (r : seq I) (P : pred I) (f : I -> E -> F) : (forall i : I, P i -> continuous (f i)) -> continuous (fun x1 : E => \sum_(i <- r | P i) f i x1). -Proof. by move=> FC0; apply: continuous_big => //; apply: add_continuous. Qed. +Proof. by move=> FC0; apply: continuous_big => //; exact: add_continuous. Qed. End TopologicalNmodule_theory. +Section cvg_composition_topologicalNmodType. +Context {T : Type} {V : topologicalNmodType} (F : set_system T) + {FF : Filter F}. +Implicit Types (f g : T -> V) (a b : V). + +Lemma cvgD f g a b : f @ F --> a -> g @ F --> b -> (f + g) @ F --> a + b. +Proof. +by move=> fa ga; apply: continuous2_cvg; [exact: (add_continuous (a, b))|..]. +Qed. + +Lemma cvg0D f g a : f @ F --> 0 -> g @ F --> a -> f x + g x @[x --> F] --> a. +Proof. by move=> /cvgD /[apply]; rewrite add0r. Qed. + +Lemma cvgD0 f g a : f @ F --> a -> g @ F --> 0 -> f x + g x @[x --> F] --> a. +Proof. by move=> /cvgD /[apply]; rewrite addr0. Qed. + +End cvg_composition_topologicalNmodType. +#[deprecated(since="mathcomp-analysis 1.19.0", use=cvgD)] +Notation fun_cvgD := cvgD (only parsing). + +Section within_continuous_topologicalNmodType. +Context {T : topologicalType} {V : topologicalNmodType} (A : set T). +Implicit Types f g : T -> V. + +Lemma within_continuousD f g : + {within A, continuous f} -> {within A, continuous g} -> + {within A, continuous (f + g)}. +Proof. by move=> cf cg x; apply: cvgD; [exact: cf|exact: cg]. Qed. + +End within_continuous_topologicalNmodType. + HB.structure Definition PreTopologicalZmodule := {M of Topological M & GRing.Zmodule M}. HB.mixin Record TopologicalNmodule_isTopologicalZmodule M - & Topological M & GRing.Zmodule M := { + & PreTopologicalZmodule M := { opp_continuous : continuous (-%R : M -> M) ; }. @@ -208,7 +223,7 @@ HB.structure Definition TopologicalZmodule := & TopologicalNmodule_isTopologicalZmodule M}. Section TopologicalZmoduleTheory. -Variables (M : topologicalZmodType). +Context {M : topologicalZmodType}. Lemma sub_continuous : continuous (fun x : M * M => x.1 - x.2). Proof. @@ -218,15 +233,10 @@ apply: cvg_pair; first exact: cvg_fst. by apply: continuous_comp; [exact: cvg_snd|exact: opp_continuous]. Qed. -Lemma fun_cvgN (F : topologicalZmodType) (U : set_system M) {FF : Filter U} - (f : M -> F) a : - f @ U --> a -> \- f @ U --> - a. -Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed. - End TopologicalZmoduleTheory. HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M - & Topological M & GRing.Zmodule M := { + & PreTopologicalZmodule M := { sub_continuous : continuous (fun x : M * M => x.1 - x.2) ; }. @@ -262,6 +272,62 @@ HB.instance Definition _ := HB.end. +Section cvg_composition_topologicalZmodType. +Context {T : Type} (V : topologicalZmodType) (F : set_system T) + {FF : Filter F}. +Implicit Types (f g : T -> V) (a b : V). + +Lemma cvgN f a : f @ F --> a -> - f @ F --> - a. +Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed. + +Lemma cvgNP f a : - f @ F --> - a <-> f @ F --> a. +Proof. by split=> /cvgN//; rewrite !opprK. Qed. + +Lemma cvgB f g a b : f @ F --> a -> g @ F --> b -> (f - g) @ F --> a - b. +Proof. by move=> ? ?; apply: cvgD => //; exact: cvgN. Qed. + +Lemma cvg0B f g a : f @ F --> 0 -> g @ F --> a -> f x - g x @[x --> F] --> - a. +Proof. by move=> /cvgB /[apply]; rewrite add0r. Qed. + +Lemma cvgB0 f g a : f @ F --> a -> g @ F --> 0 -> f x - g x @[x --> F] --> a. +Proof. by move=> /cvgB /[apply]; rewrite subr0. Qed. + +Lemma cvgN0 f : f @ F --> 0 -> - f @ F --> 0. +Proof. by rewrite -{2}oppr0; exact: cvgN. Qed. + +Lemma cvg_sub0 f g a : (f - g) @ F --> (0 : V) -> g @ F --> a -> f @ F --> a. +Proof. +by move=> Cfg Cg; have := cvgD Cfg Cg; rewrite subrK add0r; exact. +Qed. + +Lemma cvg_zero f a : (f - cst a) @ F --> (0 : V) -> f @ F --> a. +Proof. by move=> Cfa; exact: cvg_sub0 Cfa (cvg_cst _). Qed. + +Lemma subr_cvg0 f a : (fun x => f x - a) @ F --> 0 <-> f @ F --> a. +Proof. +split=> [?|fFk]; first exact: cvg_zero. +by rewrite -(@subrr _ a)//; exact: cvgB. +Qed. + +End cvg_composition_topologicalZmodType. +#[deprecated(since="mathcomp-analysis 1.19.0", use=cvgN)] +Notation fun_cvgN := cvgN (only parsing). + +Section within_continuous_topologicalZmodType. +Context {T : topologicalType} {V : topologicalZmodType} (A : set T). +Implicit Types f g : T -> V. + +Lemma within_continuousB f g : + {within A, continuous f} -> {within A, continuous g} -> + {within A, continuous (f - g)}. +Proof. by move=> cf cg x; apply: cvgB; [exact: cf|exact: cg]. Qed. + +Lemma within_continuousN f : + {within A, continuous f} -> {within A, continuous - f}. +Proof. move=> cf x; apply: cvgN; exact: cf. Qed. + +End within_continuous_topologicalZmodType. + HB.structure Definition PreUniformNmodule := {M of Uniform M & GRing.Nmodule M}. HB.mixin Record PreUniformNmodule_isUniformNmodule M & PreUniformNmodule M := { @@ -272,7 +338,7 @@ HB.structure Definition UniformNmodule := {M of PreUniformNmodule M & PreUniformNmodule_isUniformNmodule M & TopologicalNmodule M}. Section prod_TopologicalNmodule. -Context {E F : TopologicalNmodule.type}. +Context {E F : topologicalNmodType}. Let prod_add_continuous : continuous (fun x : (E * F) * (E * F) => x.1 + x.2). Proof. @@ -321,7 +387,7 @@ End prod_UniformNmodule. HB.structure Definition PreUniformZmodule := {M of Uniform M & GRing.Zmodule M}. HB.mixin Record UniformNmodule_isUniformZmodule M - & Uniform M & GRing.Zmodule M := { + & PreUniformZmodule M := { opp_unif_continuous : unif_continuous (-%R : M -> M) }. @@ -364,7 +430,7 @@ HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build End prod_UniformZmodule. HB.factory Record PreUniformNmodule_isUniformZmodule M - & Uniform M & GRing.Zmodule M := { + & PreUniformZmodule M := { sub_unif_continuous : unif_continuous (fun x : M * M => x.1 - x.2) }. @@ -426,7 +492,7 @@ HB.instance Definition _ := HB.end. Section UniformZmoduleTheory. -Variables (M : UniformZmodule.type). +Context {M : UniformZmodule.type}. Lemma sub_unif_continuous : unif_continuous (fun x : M * M => x.1 - x.2). Proof. @@ -456,7 +522,7 @@ HB.structure Definition PseudoMetricNormedZmodule (R : numDomainType) := & NormedZmod_PseudoMetric_eq R T }. #[deprecated(since="mathcomp-analysis 1.19.0", use=PseudoMetricNormedZmodule)] -Notation PseudoMetricNormedZmod0 x1 x2 := (PseudoMetricNormedZmodule x1 x2). +Notation PseudoMetricNormedZmod0 x1 x2 := (PseudoMetricNormedZmodule x1 x2) (only parsing). Module PseudoMetricNormedZmod0. #[deprecated(since="mathcomp-analysis 1.19.0", @@ -669,20 +735,24 @@ Arguments cvgr0_norm_le {_ _ _ F FF}. H : x \is_near _ |- _ => solve[near: x; now apply: cvgr0_norm_le] end : core. Section PseudoMetricNormedZmodule_realDomainType. +Context {R : realDomainType} {V : PseudoMetricNormedZmodule.type R}. -Lemma le0_ball0 (R : realDomainType) (V : PseudoMetricNormedZmodule.type R) - (a : V) (r : R) : - r <= 0 -> ball a r = set0. +Lemma le0_ball0 (a : V) (r : R) : r <= 0 -> ball a r = set0. Proof. move=> r0; rewrite -subset0 => y. rewrite -ball_normE /ball_/= ltNge => /negP; apply. by rewrite (le_trans r0). Qed. +Lemma closed_ball0 (v : V) (r : R) : r <= 0 -> closed_ball v r = set0. +Proof. +by move=> r0; rewrite -subset0 => w; rewrite /closed_ball le0_ball0// closure0. +Qed. + End PseudoMetricNormedZmodule_realDomainType. Section PseudoMetricNormedZmodule_numFieldType. -Variables (R : numFieldType) (V : PseudoMetricNormedZmodule.type R). +Context {R : numFieldType} {V : PseudoMetricNormedZmodule.type R}. Lemma norm_hausdorff : hausdorff_space V. Proof. @@ -754,13 +824,8 @@ Proof. by move=> xlt ylt; rewrite -[y]opprK (@distm_lt_split 0) ?subr0 ?opprK ?add0r. Qed. -End PseudoMetricNormedZmodule_numFieldType. -#[global] -Hint Extern 0 (hausdorff_space _) => solve[apply: norm_hausdorff] : core. - -Lemma PseudoMetricNormedZmodule_add_unif_continuous {R : numFieldType} - (M : PseudoMetricNormedZmodule.type R) : - unif_continuous (fun x : M * M => x.1 + x.2). +Lemma PseudoMetricNormedZmodule_add_unif_continuous : + unif_continuous (fun x : V * V => x.1 + x.2). Proof. apply/unif_continuousP => /= e e0. exists (e / 2); first by rewrite divr_gt0. @@ -771,15 +836,18 @@ rewrite -ball_normE/= => ab1 ab2. by rewrite opprD addrACA (splitr e)// (le_lt_trans (ler_normD _ _))//= ltrD. Qed. -Lemma PseudoMetricNormedZmodule_opp_unif_continuous {R : numFieldType} - (M : PseudoMetricNormedZmodule.type R) : - unif_continuous (-%R : M -> M). +Lemma PseudoMetricNormedZmodule_opp_unif_continuous : + unif_continuous (-%R : V -> V). Proof. apply/unif_continuousP => /= e e0. exists e => // -[a1 a2]/=. by rewrite -ball_normE/= -opprD Num.normrN. Qed. +End PseudoMetricNormedZmodule_numFieldType. +#[global] +Hint Extern 0 (hausdorff_space _) => solve[apply: norm_hausdorff] : core. + #[short(type="metricNormedZmodType")] HB.structure Definition MetricNormedZmodule (R : numDomainType) := {T of PseudoMetricNormedZmodule R T & Metric R T & UniformZmodule T}. @@ -1056,7 +1124,7 @@ by rewrite at_leftN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK. Qed. Section at_left_right_pseudoMetricNormedZmod. -Variables (R : numFieldType) (V : PseudoMetricNormedZmodule.type R). +Context {R : numFieldType} {V : PseudoMetricNormedZmodule.type R}. Lemma nbhsr0P (P : set V) x : (\forall y \near x, P y) <-> @@ -1215,7 +1283,7 @@ Arguments cvgr_neq0 {R V T F FF f}. (apply: at_right_proper_filter) : typeclass_instances. Section closure_left_right_open. -Variable R : realFieldType. +Context {R : realFieldType}. Implicit Types z : R. Lemma closure_gt z : closure ([set x | z < x] : set R) = [set x | z <= x]. @@ -1243,8 +1311,7 @@ Unshelve. all: by end_near. Qed. End closure_left_right_open. Section open_itv_subset. -Context {R : realFieldType}. -Variables (A : set R) (x : R). +Context {R : realFieldType} (A : set R) (x : R). Lemma open_itvoo_subset : open A -> A x -> \forall r \near 0^'+, `]x - r, x + r[ `<=` A. @@ -1286,8 +1353,8 @@ by rewrite gtr_pMr// invf_lt1// ltr1n. Unshelve. all: by end_near. Qed. Section pseudoMetricNormedZmodule_numFieldType. -Variables (R : numFieldType) (V : PseudoMetricNormedZmodule.type R). -Variables (I : Type) (F : set_system I) (FF : Filter F) (f : I -> V) (y : V). +Context {R : numFieldType} {V : PseudoMetricNormedZmodule.type R} {I : Type} + (F : set_system I) (FF : Filter F) (f : I -> V) (y : V). Lemma cvgr_norm_lty : f @ F --> y -> \forall M \near +oo, \forall y' \near F, `|f y'| < M. @@ -1319,7 +1386,7 @@ Arguments cvgr_norm_gtNy {R V I F FF}. Arguments cvgr_norm_geNy {R V I F FF}. Section realFieldType. -Context (R : realFieldType). +Context {R : realFieldType}. Lemma at_right_in_segment (x : R) (P : set R) : (\forall e \near 0^'+, {in `[x - e, x + e], forall x, P x}) <-> (\near x, P x). @@ -1471,12 +1538,6 @@ Context {K : numFieldType} {V : metricNormedZmodType K} {T : Type} (F : set_system T) {FF : Filter F}. Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a b : V). -Lemma cvgN f a : f @ F --> a -> - f @ F --> - a. -Proof. by move=> ?; apply: continuous_cvg => //; exact: oppr_continuous. Qed. - -Lemma cvgNP f a : - f @ F --> - a <-> f @ F --> a. -Proof. by split=> /cvgN//; rewrite !opprK. Qed. - Lemma is_cvgN f : cvg (f @ F) -> cvg (- f @ F). Proof. by move=> /cvgN /cvgP. Qed. @@ -1489,17 +1550,9 @@ Proof. by move=> ?; apply: continuous_cvg => //; exact: natmul_continuous. Qed. Lemma is_cvgMn f n : cvg (f @ F) -> cvg (((@GRing.natmul _)^~n \o f) @ F). Proof. by move=> /cvgMn /cvgP. Qed. -Lemma cvgD f g a b : f @ F --> a -> g @ F --> b -> (f + g) @ F --> a + b. -Proof. -by move=> *; apply: continuous2_cvg => //; exact: (@add_continuous _ (a, b)). -Qed. - Lemma is_cvgD f g : cvg (f @ F) -> cvg (g @ F) -> cvg (f + g @ F). Proof. by have := cvgP _ (cvgD _ _); apply. Qed. -Lemma cvgB f g a b : f @ F --> a -> g @ F --> b -> (f - g) @ F --> a - b. -Proof. by move=> ? ?; apply: cvgD => //; apply: cvgN. Qed. - Lemma is_cvgB f g : cvg (f @ F) -> cvg (g @ F) -> cvg (f - g @ F). Proof. by have := cvgP _ (cvgB _ _); apply. Qed. @@ -1512,35 +1565,6 @@ Qed. Lemma is_cvgDrE f g : cvg (f @ F) -> cvg ((f + g) @ F) = cvg (g @ F). Proof. by rewrite addrC; apply: is_cvgDlE. Qed. -Lemma cvg0D f g a : f @ F --> 0 -> g @ F --> a -> f x + g x @[x --> F] --> a. -Proof. by move=> /cvgD /[apply]; rewrite add0r. Qed. - -Lemma cvgD0 f g a : f @ F --> a -> g @ F --> 0 -> f x + g x @[x --> F] --> a. -Proof. by move=> /cvgD /[apply]; rewrite addr0. Qed. - -Lemma cvg0B f g a : f @ F --> 0 -> g @ F --> a -> f x - g x @[x --> F] --> -a. -Proof. by move=> /cvgB /[apply]; rewrite add0r. Qed. - -Lemma cvgB0 f g a : f @ F --> a -> g @ F --> 0 -> f x - g x @[x --> F] --> a. -Proof. by move=> /cvgB /[apply]; rewrite subr0. Qed. - -Lemma cvgN0 f : f @ F --> 0 -> - f @ F --> 0. -Proof. by rewrite -{2}oppr0; exact: cvgN. Qed. - -Lemma cvg_sub0 f g a : (f - g) @ F --> (0 : V) -> g @ F --> a -> f @ F --> a. -Proof. -by move=> Cfg Cg; have := cvgD Cfg Cg; rewrite subrK add0r; apply. -Qed. - -Lemma cvg_zero f a : (f - cst a) @ F --> (0 : V) -> f @ F --> a. -Proof. by move=> Cfa; exact: cvg_sub0 Cfa (cvg_cst _). Qed. - -Lemma subr_cvg0 f a : (fun x => f x - a) @ F --> 0 <-> f @ F --> a. -Proof. -split=> [?|fFk]; first exact: cvg_zero. -by rewrite -(@subrr _ a)//; exact: cvgB. -Qed. - Lemma cvg_norm f a : f @ F --> a -> `|f x| @[x --> F] --> (`|a| : K). Proof. by apply: continuous_cvg; exact: norm_continuous. Qed. @@ -1559,76 +1583,9 @@ Proof. by rewrite norm_cvg0P. Qed. End cvg_composition_metricNormedZmodType. -Section within_continuous_lemmas. -Context {T : topologicalType} {K : numFieldType} {V : metricNormedZmodType K} - (A : set T). -Implicit Types f g : T -> V. - -Lemma within_continuousB f g : - {within A, continuous f} -> {within A, continuous g} -> - {within A, continuous (f - g)}. -Proof. by move=> cf cg x; apply: cvgB; [exact: cf|exact: cg]. Qed. - -Lemma within_continuousD f g : - {within A, continuous f} -> {within A, continuous g} -> - {within A, continuous (f + g)}. -Proof. by move=> cf cg x; apply: cvgD; [exact: cf|exact: cg]. Qed. - -Lemma within_continuousN f : - {within A, continuous f} -> {within A, continuous - f}. -Proof. move=> cf x; apply: cvgN; exact: cf. Qed. - -End within_continuous_lemmas. - -Section Closed_Ball. - -Definition closed_ball_ (R : numDomainType) (V : zmodType) (norm : V -> R) - (x : V) (e : R) := [set y | norm (x - y) <= e]. - -Definition closed_ball (R : numDomainType) (V : pseudoMetricType R) - (x : V) (e : R) := closure (ball x e). - -Lemma closure_ballE (R : numDomainType) (V : pseudoMetricType R) - (c : V) (r : R) : closure (ball c r) = closed_ball c r. -Proof. by []. Qed. - -Lemma closed_ball0 (R : realDomainType) (V : metricNormedZmodType R) - (v : V) (r : R) : r <= 0 -> closed_ball v r = set0. -Proof. -by move=> r0; rewrite -subset0 => w; rewrite /closed_ball le0_ball0// closure0. -Qed. - -Lemma closed_ballxx (R : numDomainType) (V : pseudoMetricType R) (x : V) - (e : R) : 0 < e -> closed_ball x e x. -Proof. by move=> ?; exact/subset_closure/ballxx. Qed. - -Lemma closed_ball_closed (R : numDomainType) (V : pseudoMetricType R) (x : V) - (r : R) : closed (closed_ball x r). -Proof. exact: closed_closure. Qed. - -Lemma subset_closed_ball (R : numDomainType) (V : pseudoMetricType R) (x : V) - (r : R) : ball x r `<=` closed_ball x r. -Proof. exact: subset_closure. Qed. - -Lemma subset_closure_half (R : numFieldType) (V : pseudoMetricType R) (x : V) - (r : R) : 0 < r -> closed_ball x (r / 2) `<=` ball x r. -Proof. -move:r => _/posnumP[r] z /(_ (ball z ((r%:num/2)%:pos)%:num)) []. - exact: nbhsx_ballx. -by move=> y [+/ball_sym]; rewrite [t in ball x t z]splitr; apply: ball_triangle. -Qed. - -Lemma le_closed_ball (R : numFieldType) (M : pseudoMetricType R) - (x : M) (e1 e2 : R) : (e1 <= e2)%O -> closed_ball x e1 `<=` closed_ball x e2. -Proof. by rewrite /closed_ball => le; apply/closureS/le_ball. Qed. - -End Closed_Ball. -#[deprecated(since="mathcomp-analysis 1.14.0", note="renamed to `closure_ballE`")] -Notation closure_ball := closure_ballE (only parsing). - Section limit_composition_metricNormedZmodType. -Context {K : numFieldType} {V : metricNormedZmodType K} {T : Type}. -Context (F : set_system T) {FF : ProperFilter F}. +Context {K : numFieldType} {V : metricNormedZmodType K} {T : Type} + (F : set_system T) {FF : ProperFilter F}. Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a : V). Lemma limN f : cvg (f @ F) -> lim (- f @ F) = - lim (f @ F). @@ -1774,7 +1731,7 @@ Unshelve. all: by end_near. Qed. End bounded_near. Section cvg_bounded. -Variables (R : numFieldType) (V : PseudoMetricNormedZmodule.type R). +Context {R : numFieldType} {V : PseudoMetricNormedZmodule.type R}. Lemma cvg_bounded {I} {F : set_system I} {FF : Filter F} (f : I -> V) (y : V) : f @ F --> y -> bounded_near f F. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index ab87060054..1e91a170b7 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -13,8 +13,6 @@ From mathcomp Require Import pseudometric_normed_Zmodule. (* *) (* This file introduces locally convex topological vector spaces. *) (* ``` *) -(* NbhsNmodule == HB class, join of Nbhs and Nmodule *) -(* NbhsZmodule == HB class, join of Nbhs and Zmodule *) (* NbhsLmodule K == HB class, join of Nbhs and Lmodule over K *) (* K is a numDomainType. *) (* preTopologicalLmodType K == topological space and Lmodule over K *) @@ -78,15 +76,6 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -(* HB.structure Definition PointedNmodule := {M of Pointed M & GRing.Nmodule M}. *) -(* HB.structure Definition PointedZmodule := {M of Pointed M & GRing.Zmodule M}. *) -(* HB.structure Definition PointedLmodule (K : numDomainType) := *) -(* {M of Pointed M & GRing.Lmodule K M}. *) - -(* HB.structure Definition FilteredNmodule := {M of Filtered M M & GRing.Nmodule M}. *) -(* HB.structure Definition FilteredZmodule := {M of Filtered M M & GRing.Zmodule M}. *) -(* HB.structure Definition FilteredLmodule (K : numDomainType) := *) -(* {M of Filtered M M & GRing.Lmodule K M}. *) HB.structure Definition NbhsLmodule (K : numDomainType) := {M of Nbhs M & GRing.Lmodule K M}. @@ -95,7 +84,7 @@ HB.structure Definition PreTopologicalLmodule (K : numDomainType) := {M of Topological M & GRing.Lmodule K M}. HB.mixin Record TopologicalZmodule_isTopologicalLmodule (R : numDomainType) M - & Topological M & GRing.Lmodule R M := { + & PreTopologicalLmodule R M := { scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ; }. @@ -105,7 +94,7 @@ HB.structure Definition TopologicalLmodule (K : numDomainType) := & TopologicalZmodule_isTopologicalLmodule K M}. Section TopologicalLmodule_theory. -Variables (R : numFieldType) (E : topologicalType) (F : topologicalLmodType R). +Context {R : numFieldType} (E : topologicalType) (F : topologicalLmodType R). Lemma fun_cvgZ (U : set_system E) {FF : Filter U} (l : E -> R) (f : E -> F) (r : R) a : @@ -122,7 +111,7 @@ Proof. by apply: fun_cvgZ => //; exact: cvg_cst. Qed. End TopologicalLmodule_theory. HB.factory Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M - & Topological M & GRing.Lmodule R M := { + & PreTopologicalLmodule R M := { scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ; }. @@ -313,7 +302,7 @@ Unshelve. all: by end_near. Qed. End properties_of_topologicalLmodule. HB.factory Record PreTopologicalLmod_isConvexTvs (R : numDomainType) E - & Topological E & GRing.Lmodule R E := { + & PreTopologicalLmodule R E := { add_continuous : continuous (fun x : E * E => x.1 + x.2) ; scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2) ; locally_convex : exists2 B : set_system E, @@ -523,13 +512,6 @@ move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. by exists (ball x r) => //=; split; [exists x, r|exact: ballxx]. Qed. -(* -Check R^o : TopologicalNmodule.type. - -HB.instance Definition _ := - PreTopologicalNmodule_isTopologicalNmodule.Build R^o standard_add_continuous. -*) - HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R R^o standard_scale_continuous. @@ -707,13 +689,13 @@ Proof. by apply: cst_continuous. Qed. HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous. #[local] Lemma lcfun_continuousD f g : continuous (f \+ g). -Proof. by move=> /= x; apply: fun_cvgD; exact: continuous_fun. Qed. +Proof. by move=> /= x; apply: cvgD; exact: continuous_fun. Qed. HB.instance Definition _ f g := isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g). #[local] Lemma lcfun_continuousN f : continuous (\- f). -Proof. by move=> /= x; apply: fun_cvgN; exact: continuous_fun. Qed. +Proof. by move=> /= x; apply: cvgN; exact: continuous_fun. Qed. HB.instance Definition _ f := isContinuous.Build E F (\- f) (@lcfun_continuousN f). diff --git a/theories/numfun.v b/theories/numfun.v index 3ffff640df..b1432421d0 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -1386,7 +1386,7 @@ exists (lim (h_ @ \oo)); split. - move=> t /set_mem At; have /pointwise_cvgP/(_ t)/(cvg_lim (@Rhausdorff _)) := [elaborate pointwise_uniform_cvg _ cvgh]. rewrite -fmap_comp /comp /h_ => <-; apply/esym/(@cvg_lim _ (@Rhausdorff R)). - apply: (@cvg_zero R R^o); apply: norm_cvg0; under eq_fun => n. + apply: (@cvg_zero _ R^o); apply: norm_cvg0; under eq_fun => n. rewrite distrC /series /cst /= -mulN1r fct_sumE mulr_sumr. under [fun _ : nat => _]eq_fun => ? do rewrite mulN1r -fgE opprB. rewrite telescope_sumr //= subrKC. diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v index e1711cfd44..787516b9cc 100644 --- a/theories/topology_theory/pseudometric_structure.v +++ b/theories/topology_theory/pseudometric_structure.v @@ -41,6 +41,12 @@ From mathcomp Require Import uniform_structure. (* cauchy_ball F <-> the set of sets F is a cauchy filter *) (* (using the near notations) *) (* ``` *) +(* ## Closed balls *) +(* ``` *) +(* closed_ball_ norm x e := [set y | norm (x - y) <= e] *) +(* closed_ball == closure of a ball *) +(* ``` *) +(* *) (******************************************************************************) Import Order.TTheory GRing.Theory Num.Theory. @@ -433,3 +439,41 @@ near F => x; exists x; near: x; apply: (@nearP_dep _ _ F F). exact/Fcauchy/entourage_ball. Unshelve. all: by end_near. Qed. Arguments cauchyP {R T} F {PF}. + +Definition closed_ball_ {R : numDomainType} {V : zmodType} (norm : V -> R) + (x : V) (e : R) := [set y | norm (x - y) <= e]. + +Definition closed_ball {R : numDomainType} {V : pseudoMetricType R} + (x : V) (e : R) := closure (ball x e). + +Section closed_ball_lemmas. +Context {R : numDomainType} {V : pseudoMetricType R}. +Implicit Types (x : V) (r : R). + +Lemma closure_ballE x r : closure (ball x r) = closed_ball x r. +Proof. by []. Qed. + +Lemma closed_ballxx x r : 0 < r -> closed_ball x r x. +Proof. by move=> ?; exact/subset_closure/ballxx. Qed. + +Lemma closed_ball_closed x r : closed (closed_ball x r). +Proof. exact: closed_closure. Qed. + +Lemma subset_closed_ball x r : ball x r `<=` closed_ball x r. +Proof. exact: subset_closure. Qed. + +Lemma le_closed_ball x r1 r2 : (r1 <= r2)%O -> + closed_ball x r1 `<=` closed_ball x r2. +Proof. by rewrite /closed_ball => le; apply/closureS/le_ball. Qed. + +End closed_ball_lemmas. +#[deprecated(since="mathcomp-analysis 1.14.0", note="renamed to `closure_ballE`")] +Notation closure_ball := closure_ballE (only parsing). + +Lemma subset_closure_half {R : numFieldType} {V : pseudoMetricType R} (x : V) + (r : R) : 0 < r -> closed_ball x (r / 2) `<=` ball x r. +Proof. +move:r => _/posnumP[r] z /(_ (ball z ((r%:num/2)%:pos)%:num)) []. + exact: nbhsx_ballx. +by move=> y [+/ball_sym]; rewrite [t in ball x t z]splitr; apply: ball_triangle. +Qed.