From b60fa49c5fab66542469f49616142622fe627c14 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 22 May 2025 18:23:44 +0200 Subject: [PATCH 1/7] repair structure names in tvs.v --- theories/tvs.v | 51 ++++++++++++++++++++++++++++++++------------------ 1 file changed, 33 insertions(+), 18 deletions(-) diff --git a/theories/tvs.v b/theories/tvs.v index eb38ad196..a40d06598 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -62,18 +62,34 @@ HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}. HB.structure Definition NbhsLmodule (K : numDomainType) := {M of Nbhs M & GRing.Lmodule K M}. -HB.structure Definition TopologicalNmodule := +HB.structure Definition PreTopologicalNmodule := {M of Topological M & GRing.Nmodule M}. -HB.structure Definition TopologicalZmodule := + +HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M of PreTopologicalNmodule M := { + add_continuous : continuous (fun x : M * M => x.1 + x.2) ; +}. + +HB.structure Definition TopologicalNmodule := + {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}. +HB.structure Definition PreTopologicalZmodule := {M of Topological M & GRing.Zmodule M}. +HB.structure Definition TopologicalZmodule := + {M of TopologicalNmodule M & GRing.Zmodule M}. +HB.mixin Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M of Topological M & GRing.Lmodule R M := { + scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ; +}. + +#[short(type="preTopologicalLmodType")] +HB.structure Definition PreTopologicalLmodule (K : numDomainType) := + {M of Topological M & GRing.Lmodule K M}. #[short(type="topologicalLmodType")] HB.structure Definition TopologicalLmodule (K : numDomainType) := - {M of Topological M & GRing.Lmodule K M}. + {M of TopologicalNmodule M & TopologicalNmodule_isTopologicalLmodule K M}. -HB.structure Definition UniformZmodule := {M of Uniform M & GRing.Zmodule M}. +HB.structure Definition UniformZmodule := {M of Uniform M & TopologicalZmodule M}. HB.structure Definition UniformLmodule (K : numDomainType) := - {M of Uniform M & GRing.Lmodule K M}. + {M of Uniform M & TopologicalLmodule K M}. Definition convex (R : numDomainType) (M : lmodType R) (A : set M) := forall x y (lambda : R), x \in A -> y \in A -> @@ -81,18 +97,16 @@ Definition convex (R : numDomainType) (M : lmodType R) (A : set M) := HB.mixin Record Uniform_isTvs (R : numDomainType) E of Uniform E & GRing.Lmodule 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 (set E), (forall b, b \in B -> convex b) & basis B }. #[short(type="tvsType")] HB.structure Definition Tvs (R : numDomainType) := - {E of Uniform_isTvs R E & Uniform E & GRing.Lmodule R E}. + {E of Uniform_isTvs R E & Uniform E & TopologicalLmodule R E}. Section properties_of_topologicalLmodule. -Context (R : numDomainType) (E : topologicalLmodType R) (U : set E). +Context (R : numDomainType) (E : preTopologicalLmodType R) (U : set E). Lemma nbhsN_subproof (f : continuous (fun z : R^o * E => z.1 *: z.2)) (x : E) : nbhs x U -> nbhs (-x) (-%R @` U). @@ -127,7 +141,7 @@ Unshelve. all: by end_near. Qed. End properties_of_topologicalLmodule. -HB.factory Record TopologicalLmod_isTvs (R : numDomainType) E +HB.factory Record PreTopologicalLmod_isTvs (R : numDomainType) E of Topological E & GRing.Lmodule 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) ; @@ -135,7 +149,7 @@ HB.factory Record TopologicalLmod_isTvs (R : numDomainType) E (forall b, b \in B -> convex b) & basis B }. -HB.builders Context R E of TopologicalLmod_isTvs R E. +HB.builders Context R E of PreTopologicalLmod_isTvs R E. Definition entourage : set_system (E * E) := fun P => exists (U : set E), nbhs (0 : E) U /\ @@ -348,8 +362,9 @@ move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. Qed. -HB.instance Definition _ := Uniform_isTvs.Build R R^o - standard_add_continuous standard_scale_continuous standard_locally_convex. +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_isTvs.Build R R^o standard_locally_convex. End standard_topology. @@ -359,8 +374,8 @@ Context (K : numFieldType) (E F : tvsType 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 K E (xy1.1, xy2.1) _ nA. -have [/= B0 [B01 B02] nB1] := @add_continuous K F (xy1.2, xy2.2) _ nB. +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. @@ -401,8 +416,8 @@ move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2] l0 l1. by split; rewrite -inE; [apply: Bcb; rewrite ?inE|apply: Bcf; rewrite ?inE]. Qed. -HB.instance Definition _ := - Uniform_isTvs.Build K (E * F)%type - prod_add_continuous prod_scale_continuous prod_locally_convex. +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_isTvs.Build K (E * F)%type prod_locally_convex. End prod_Tvs. From 61a789f6988796e731a33f46878944aa2e38dc48 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 23 May 2025 11:08:35 +0200 Subject: [PATCH 2/7] doc and changelog --- CHANGELOG_UNRELEASED.md | 13 +++++++++++ theories/tvs.v | 49 ++++++++++++++++++++++++----------------- 2 files changed, 42 insertions(+), 20 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 75ff33573..3ecc6d53b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -12,6 +12,11 @@ * implemented through a module `ConvexQuasiAssoc` containing `law` and helper lemmas + lemmas `convR_itv`, `convR_line_path` +- in `tvs.v` + + HB classes `TopologicalNmodule`, `TopologicalZmodule`, `TopologicalLmodule` + + mixin `PreTopologicalNmodule_isTopologicalNmodule`, + `TopologicalNmodule_isTopologicalLmodule` + + structure `topologicalLmodule` ### Changed @@ -59,6 +64,9 @@ - in `convex.v`: + definition `convex_realDomainType` generalized and renamed accordingly `convex_numDomainType` ++ in `tvs.v` + + HB class `UniformZmodule` now contains `TopologicalZmodule` + + HB class `UniformLmodule` now contains `TopologicalLmodule` ### Renamed @@ -67,6 +75,11 @@ - in `convex.v` + lemma `conv_gt0` to `convR_gt0` +- in `tvs.v` + + HB class `TopologicalNmodule` moved to `PreTopologicalNmodule` + + HB class `TopologicalZmodule` moved to `PreTopologicalZmodule` + + HB class `TopologicalLmodule` moved to `PreTopologicalLmodule` + + structure `topologicalLmodule` moved to `preTopologicalLmodule` ### Generalized diff --git a/theories/tvs.v b/theories/tvs.v index a40d06598..33d4ffcbe 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -12,26 +12,35 @@ From mathcomp Require Import topology function_spaces. (* *) (* 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. *) -(* TopologicalNmodule == HB class, joint of Topological and Nmodule *) -(* TopologicalZmodule == HB class, joint of Topological and Zmodule *) -(* topologicalLmodType K == topological space and Lmodule over K *) -(* K is a numDomainType. *) -(* The HB class is TopologicalLmodule. *) -(* UniformZmodule == HB class, joint of Uniform and Zmodule *) -(* UniformLmodule K == HB class, joint of Uniform and Lmodule over K *) -(* K is a numDomainType. *) -(* convex A == A : set M is a convex set of elements of M *) -(* M is an Lmodule over R : numDomainType. *) -(* tvsType R == interface type for a locally convex topological *) -(* vector space on a numDomain R *) -(* A tvs is constructed over a uniform space. *) -(* The HB class is Tvs. *) -(* TopologicalLmod_isTvs == factory allowing the construction of a tvs from *) -(* an Lmodule which is also a topological space. *) +(* 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. *) +(* PreTopologicalNmodule == HB class, joint of Topological and Nmodule *) +(* TopologicalNmodule == HB class, PreTopologicalNmodule with a *) +(* continuous addition *) +(* PreTopologicalZmodule == HB class, joint of Topological and Zmodule *) +(* TopologicalZmodule == HB class, joint of TopologicalNmodule and *) +(* Zmodule *) +(*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. *) +(* UniformZmodule == HB class, joint of Uniform and *) +(* TopologicalZmodule *) +(* UniformLmodule K == HB class, joint of Uniform and *) +(* TopologicalLmodule over K *) +(* K is a numDomainType. *) +(* convex A == A : set M is a convex set of elements of M *) +(* M is an Lmodule over R : numDomainType. *) +(* tvsType R == interface type for a locally convex topological *) +(* vector space on a numDomain R *) +(* A tvs is constructed over a uniform space. *) +(* The HB class is Tvs. *) +(* TopologicalLmod_isTvs == factory allowing the construction of a tvs from *) +(* an Lmodule which is also a topological space. *) (* ``` *) (* HB instances: *) (* - The type R^o (R : numFieldType) is endowed with the structure of Tvs. *) From a8aca5dfcf852edc0bdc368da4db1124dec3ed68 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 23 May 2025 16:54:18 +0200 Subject: [PATCH 3/7] repair uniform algebraic structures --- CHANGELOG_UNRELEASED.md | 8 +++++++- theories/tvs.v | 34 ++++++++++++++++++++++++++++------ 2 files changed, 35 insertions(+), 7 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3ecc6d53b..6e93ee92b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -14,8 +14,10 @@ + lemmas `convR_itv`, `convR_line_path` - in `tvs.v` + HB classes `TopologicalNmodule`, `TopologicalZmodule`, `TopologicalLmodule` - + mixin `PreTopologicalNmodule_isTopologicalNmodule`, + `UniformNmodule`, `UniformZmodule`, `UniformLmodule` + + mixin `TopologicalNmodule_isTopologicalNmodule`, `TopologicalNmodule_isTopologicalLmodule` + `PreUniformNmodule_isUniformNmodule`, `PreUniformLmodule_isUniformLmodule` + structure `topologicalLmodule` ### Changed @@ -80,6 +82,10 @@ + HB class `TopologicalZmodule` moved to `PreTopologicalZmodule` + HB class `TopologicalLmodule` moved to `PreTopologicalLmodule` + structure `topologicalLmodule` moved to `preTopologicalLmodule` + + HB class `UniformNmodule` moved to `PreUniformNmodule` + + HB class `UniformZmodule` moved to `PreUniformZmodule` + + HB class `UniformLmodule` moved to `PreUniformLmodule` + ### Generalized diff --git a/theories/tvs.v b/theories/tvs.v index 33d4ffcbe..149033c59 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -28,18 +28,24 @@ From mathcomp Require Import topology function_spaces. (* topologicalLmodType K == topologicalNmodule and Lmodule over K with a *) (* continuous scaling operation. *) (* The HB class is TopologicalLmodule. *) -(* UniformZmodule == HB class, joint of Uniform and *) +(* UniformNmodule == HB class, joint of Uniform and Nmodule with a *) +(* uniformly continuous addition *) +(* PreUniformZmodule == HB class, joint of Uniform and *) (* TopologicalZmodule *) -(* UniformLmodule K == HB class, joint of Uniform and *) +(* UniformZmodule == HB class, joint of UniformNmodule and Zmodule *) +(* PreUniformLmodule K == HB class, joint of Uniform and *) (* TopologicalLmodule over K *) (* K is a numDomainType. *) +(* UniformLmodule K == HB class, joint of UniformNmodule and Lmodule *) +(* with a uniformly continuous scaling operation *) +(* K is a numFieldType. *) (* convex A == A : set M is a convex set of elements of M *) (* M is an Lmodule over R : numDomainType. *) (* tvsType R == interface type for a locally convex topological *) (* vector space on a numDomain R *) (* A tvs is constructed over a uniform space. *) (* The HB class is Tvs. *) -(* TopologicalLmod_isTvs == factory allowing the construction of a tvs from *) +(*PreTopologicalLmod_isTvs == factory allowing the construction of a tvs from *) (* an Lmodule which is also a topological space. *) (* ``` *) (* HB instances: *) @@ -96,10 +102,26 @@ HB.structure Definition PreTopologicalLmodule (K : numDomainType) := HB.structure Definition TopologicalLmodule (K : numDomainType) := {M of TopologicalNmodule M & TopologicalNmodule_isTopologicalLmodule K M}. -HB.structure Definition UniformZmodule := {M of Uniform M & TopologicalZmodule M}. -HB.structure Definition UniformLmodule (K : numDomainType) := +HB.structure Definition PreUniformNmodule := {M of Uniform M & TopologicalNmodule M}. + +HB.mixin Record PreUniformNmodule_isUniformNmodule M of 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.structure Definition PreUniformZmodule := {M of Uniform M & TopologicalZmodule M}. +HB.structure Definition UniformZmodule := {M of UniformNmodule M & GRing.Zmodule M}. + +HB.structure Definition PreUniformLmodule (K : numDomainType) := {M of Uniform M & TopologicalLmodule K M}. +HB.mixin Record PreUniformLmodule_isUniformLmodule (R : numFieldType) M of 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 PreUniformLmodule R M & PreUniformLmodule_isUniformLmodule R M}. + Definition convex (R : numDomainType) (M : lmodType R) (A : set M) := forall x y (lambda : R), x \in A -> y \in A -> 0 < lambda -> lambda < 1 -> lambda *: x + (1 - lambda) *: y \in A. @@ -108,7 +130,7 @@ HB.mixin Record Uniform_isTvs (R : numDomainType) E of Uniform E & GRing.Lmodule R E := { locally_convex : exists2 B : set (set E), (forall b, b \in B -> convex b) & basis B -}. +}.' #[short(type="tvsType")] HB.structure Definition Tvs (R : numDomainType) := From e6cc7fb45ec15bcee4fc459eb6d819afbd4163af Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Sat, 24 May 2025 18:22:35 +0200 Subject: [PATCH 4/7] fix Zmodules --- theories/normedtype_theory/normed_module.v | 6 +- theories/topology_theory/num_topology.v | 59 ++++++ theories/tvs.v | 198 +++++++++++++++++++-- 3 files changed, 247 insertions(+), 16 deletions(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 18bfa7713..edeccb19c 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -131,8 +131,10 @@ by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. Qed. HB.instance Definition _ := - Uniform_isTvs.Build K V add_continuous scale_continuous locally_convex. - + PreTopologicalNmodule_isTopologicalNmodule.Build V add_continuous. +HB.instance Definition _ := + TopologicalNmodule_isTopologicalLmodule.Build K V scale_continuous. +HB.instance Definition _ := Uniform_isTvs.Build K V locally_convex. HB.instance Definition _ := PseudoMetricNormedZmod_Tvs_isNormedModule.Build K V normrZ. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index df8f42623..ddd0fa8fc 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -26,10 +26,69 @@ Local Open Scope ring_scope. HB.instance Definition _ (R : numDomainType) := hasNbhs.Build R^o (nbhs_ball_ (ball_ (fun x => `|x|))). +Module TopologicalNumDomainType. +Section TopologicalNumDomainType. +Variable (R : numDomainType). + +Lemma nbhs_filter (p : R^o) : ProperFilter (nbhs p). +Proof. +split. + move=> [] e e0 /subsetP/(_ p). + by rewrite !in_setE/= subrr normr0. +split=> [|P Q|P Q]. +- exists 1; first exact: ltr01. + exact: subsetT. +- move=> [] /= e e0 /subsetP eP [] /= f f0 /subsetP fQ. + exists (Order.min e f) => /=. + rewrite [Num.min e f]/(Order.min e f). + by case: ifP. + apply/subsetP => x. + rewrite in_setE in_setI/= => pef. + apply/andP; split. + apply/eP; rewrite in_setE/=. + apply: (lt_le_trans pef). + case: (@real_ltP _ e f) => //; exact: gtr0_real. + apply/fQ; rewrite in_setE/=. + apply: (lt_le_trans pef). + case: (@real_ltP _ f e) => //; exact: gtr0_real. +- move=> PQ [] /= e e0 eP. + exists e => //. + exact: (subset_trans eP). +Qed. + +Lemma nbhs_singleton (p : R^o) (A : set R) : nbhs p A -> A p. +Proof. +move=> [] /= e e0 /subsetP /(_ p). +by rewrite !in_setE/= subrr normr0 e0 => /(_ erefl). +Qed. + +Lemma nbhs_nbhs (p : R^o) (A : set R) : nbhs p A -> nbhs p (nbhs^~ A). +Proof. +move=> [] /= e e0 /subsetP eA. +exists e => //. +apply/subsetP => x. +rewrite !inE/= => xe. +exists (e - `|p - x|); first by rewrite /= subr_gt0. +apply/subsetP => y. +rewrite inE/= -subr_gt0 -addrA -opprD subr_gt0 => ye. +apply: eA; rewrite inE/=. +have ->: p - y = (p - x) + (x - y). + by rewrite addrA; congr (_ - _); rewrite -addrA addNr addr0. +exact: (le_lt_trans (ler_normD _ _) ye). +Qed. +End TopologicalNumDomainType. +End TopologicalNumDomainType. + +HB.instance Definition _ (R : numDomainType) := Nbhs_isNbhsTopological.Build R^o (@TopologicalNumDomainType.nbhs_filter R) (@TopologicalNumDomainType.nbhs_singleton R) (@TopologicalNumDomainType.nbhs_nbhs R). + HB.instance Definition _ (R : numFieldType) := Nbhs_isPseudoMetric.Build R R^o nbhs_ball_normE ball_norm_center ball_norm_symmetric ball_norm_triangle erefl. +HB.instance Definition _ (R : numFieldType) := + Uniform_isPseudoMetric.Build R R^o + ball_norm_center ball_norm_symmetric ball_norm_triangle erefl. + Lemma real_order_nbhsE (R : realFieldType) (x : R^o) : nbhs x = filter_from (fun i => itv_open_ends i /\ x \in i) (fun i => [set` i]). Proof. diff --git a/theories/tvs.v b/theories/tvs.v index 149033c59..76b6b62d9 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -28,13 +28,12 @@ From mathcomp Require Import topology function_spaces. (* topologicalLmodType K == topologicalNmodule and Lmodule over K with a *) (* continuous scaling operation. *) (* The HB class is TopologicalLmodule. *) +(* PreUniformNmodule == HB class, joint of Uniform and Nmodule *) (* UniformNmodule == HB class, joint of Uniform and Nmodule with a *) (* uniformly continuous addition *) -(* PreUniformZmodule == HB class, joint of Uniform and *) -(* TopologicalZmodule *) +(* PreUniformZmodule == HB class, joint of Uniform and Zmodule *) (* UniformZmodule == HB class, joint of UniformNmodule and Zmodule *) -(* PreUniformLmodule K == HB class, joint of Uniform and *) -(* TopologicalLmodule over K *) +(* PreUniformLmodule K == HB class, joint of Uniform and Lmodule over K *) (* K is a numDomainType. *) (* UniformLmodule K == HB class, joint of UniformNmodule and Lmodule *) (* with a uniformly continuous scaling operation *) @@ -86,23 +85,101 @@ HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M of PreTopologicalNm HB.structure Definition TopologicalNmodule := {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}. + HB.structure Definition PreTopologicalZmodule := {M of Topological M & GRing.Zmodule M}. + +HB.mixin Record TopologicalNmodule_isTopologicalZmodule M of Topological M & GRing.Zmodule M := { + opp_continuous : continuous (-%R : M -> M) ; +}. + HB.structure Definition TopologicalZmodule := - {M of TopologicalNmodule M & GRing.Zmodule M}. + {M of TopologicalNmodule M & GRing.Zmodule M & TopologicalNmodule_isTopologicalZmodule M}. -HB.mixin Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M of Topological M & GRing.Lmodule R M := { - scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ; +HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M of Topological M & GRing.Zmodule M := { + sub_continuous : continuous (fun x : M * M => x.1 - x.2) ; }. +HB.builders Context M of PreTopologicalNmodule_isTopologicalZmodule M. + +Lemma opp_continuous : continuous (-%R : M -> M). +Proof. +move=> x; rewrite /continuous_at. +rewrite -(@eq_cvg _ _ _ (fun x : M => 0 - x)); last first. + move=> y; exact: add0r. +rewrite -[- x]add0r. +apply: (@continuous_comp _ _ _ (fun x => (0, x)) (fun x : M * M => x.1 - x.2) ); last exact: sub_continuous. +apply: cvg_pair => /=; first exact: cvg_cst. +exact: cvg_id. +Qed. + +Lemma add_continuous : continuous (fun x : M * M => x.1 + x.2). +Proof. +move=> x; rewrite /continuous_at. +rewrite -(@eq_cvg _ _ _ (fun x : M * M => x.1 - (- x.2))); last first. + by move=> y; rewrite opprK. +rewrite -[in x.1 + _](opprK x.2). +apply: (@continuous_comp _ _ _ (fun x : M * M => (x.1, - x.2)) (fun x : M * M => x.1 - x.2) ); last exact: sub_continuous. +apply: cvg_pair; first exact: cvg_fst. +apply: (@continuous_comp _ _ _ snd -%R); first exact: cvg_snd. +exact: opp_continuous. +Qed. + +HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build M add_continuous. +HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build M opp_continuous. + +HB.end. + +Section TopologicalZmoduleTheory. +Variables (M : TopologicalZmodule.type). + +Lemma sub_continuous : continuous (fun x : M * M => x.1 - x.2). +Proof. +move=> x. +apply: (@continuous_comp _ _ _ (fun x : M * M => (x.1, - x.2)) (fun x : M * M => x.1 + x.2)); last exact: add_continuous. +apply: cvg_pair; first exact: cvg_fst. +apply: (@continuous_comp _ _ _ snd -%R); first exact: cvg_snd. +exact: opp_continuous. +Qed. + +End TopologicalZmoduleTheory. + #[short(type="preTopologicalLmodType")] HB.structure Definition PreTopologicalLmodule (K : numDomainType) := {M of Topological M & GRing.Lmodule K M}. + +HB.mixin Record TopologicalZmodule_isTopologicalLmodule (R : numDomainType) M of Topological M & GRing.Lmodule R M := { + scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ; +}. + #[short(type="topologicalLmodType")] HB.structure Definition TopologicalLmodule (K : numDomainType) := - {M of TopologicalNmodule M & TopologicalNmodule_isTopologicalLmodule K M}. + {M of TopologicalZmodule M & GRing.Lmodule K M & TopologicalZmodule_isTopologicalLmodule K M}. + +HB.factory Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M of Topological M & GRing.Lmodule R M := { + scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ; +}. + +HB.builders Context R M of TopologicalNmodule_isTopologicalLmodule R M. + +Lemma opp_continuous : continuous (-%R : M -> M). +Proof. +move=> x; rewrite /continuous_at. +rewrite -(@eq_cvg _ _ _ (fun x : M => -1 *: x)); last first. + by move=> y; rewrite scaleN1r. +rewrite -[- x]scaleN1r. +apply: (@continuous_comp M (R^o * M)%type M (fun x : M => (-1, x) : R^o * M) (fun x : R^o * M => x.1 *: x.2)); last exact: scale_continuous. +apply: (@cvg_pair _ _ _ _ (nbhs (-1 : R^o))); first exact: cvg_cst. +exact: cvg_id. +Qed. -HB.structure Definition PreUniformNmodule := {M of Uniform M & TopologicalNmodule M}. +#[warning="-HB.no-new-instance"] +HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build M opp_continuous. +HB.instance Definition _ := TopologicalZmodule_isTopologicalLmodule.Build R M scale_continuous. + +HB.end. + +HB.structure Definition PreUniformNmodule := {M of Uniform M & GRing.Nmodule M}. HB.mixin Record PreUniformNmodule_isUniformNmodule M of PreUniformNmodule M := { add_unif_continuous : unif_continuous (fun x : M * M => x.1 + x.2) @@ -110,17 +187,110 @@ HB.mixin Record PreUniformNmodule_isUniformNmodule M of PreUniformNmodule M := { HB.structure Definition UniformNmodule := {M of PreUniformNmodule M & PreUniformNmodule_isUniformNmodule M}. -HB.structure Definition PreUniformZmodule := {M of Uniform M & TopologicalZmodule M}. -HB.structure Definition UniformZmodule := {M of UniformNmodule M & GRing.Zmodule M}. +HB.structure Definition PreUniformZmodule := {M of Uniform M & GRing.Zmodule M}. + +HB.mixin Record UniformNmodule_isUniformNmodule M of 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_isUniformNmodule M}. + +HB.factory Record PreUniformNmodule_isUniformZmodule M of Uniform M & GRing.Zmodule M := { + sub_unif_continuous : unif_continuous (fun x : M * M => x.1 - x.2) +}. + +HB.builders Context M of 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. + rewrite /nbhs/=. + apply: (@filterS _ _ entourage_filter U2) => // x xU2 /=. + have /U12: ((0, 0), x) \in U1 `*` U2. + rewrite in_setX/=; apply/andP; split; apply/asboolP => //. + exact: entourage_refl. + by rewrite inE/= => [[[]]] [] a1 a2 [] b1 b2/= abU [] {2}<- <- <-/=. +move=> /= U /sub_unif_continuous/unif/=. +rewrite /nbhs/=. +rewrite -comp_preimage/=/comp/=. +by congr entourage; rewrite eqEsubset; split=> x /=; rewrite !add0r. +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))); last first. + 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=> /= [] [] a1 a2 [] b1 b2/= [] ab1 ab2. + have /U12: (a1, b1, (-a2, -b2)) \in U1 `*` U2 by rewrite !inE/=. + by rewrite inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-. +move=> /= U /sub_unif_continuous/unif; rewrite /nbhs/=. +rewrite -comp_preimage/=/comp/=. +by congr entourage; rewrite eqEsubset; split=> x /=; rewrite !opprK. +Qed. + +HB.instance Definition _ := PreUniformNmodule_isUniformNmodule.Build M add_unif_continuous. +HB.instance Definition _ := UniformNmodule_isUniformNmodule.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))); last first. + 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=> /= [] [] a1 a2 [] b1 b2/= [] ab1 ab2. +have /U12: (a1, b1, (-a2, -b2)) \in U1 `*` U2 by rewrite !inE/=. +by rewrite inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-. +Qed. + +End UniformZmoduleTheory. HB.structure Definition PreUniformLmodule (K : numDomainType) := - {M of Uniform M & TopologicalLmodule K M}. + {M of Uniform M & GRing.Lmodule K M}. HB.mixin Record PreUniformLmodule_isUniformLmodule (R : numFieldType) M of 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 PreUniformLmodule R M & PreUniformLmodule_isUniformLmodule R M}. +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 of PreUniformLmodule R M := { + scale_unif_continuous : unif_continuous (fun z : R^o * M => z.1 *: z.2) ; +}. + +HB.builders Context R M of 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 _ _ entourage_filter U2) => // x xU2 /=. + have /U12: ((-1, -1), x) \in U1 `*` U2. + rewrite in_setX/=; apply/andP; split; apply/asboolP => //. + exact: entourage_refl. + by rewrite 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 !scaleN1r. +Qed. + +#[warning="-HB.no-new-instance"] +HB.instance Definition _ := UniformNmodule_isUniformNmodule.Build M opp_unif_continuous. +HB.instance Definition _ := PreUniformLmodule_isUniformLmodule.Build R M scale_unif_continuous. + +HB.end. Definition convex (R : numDomainType) (M : lmodType R) (A : set M) := forall x y (lambda : R), x \in A -> y \in A -> @@ -130,7 +300,7 @@ HB.mixin Record Uniform_isTvs (R : numDomainType) E of Uniform E & GRing.Lmodule R E := { locally_convex : exists2 B : set (set E), (forall b, b \in B -> convex b) & basis B -}.' +}. #[short(type="tvsType")] HB.structure Definition Tvs (R : numDomainType) := From 3d48758c5efbac7973034534266f747d842d4884 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Sat, 24 May 2025 19:19:15 +0200 Subject: [PATCH 5/7] doc and changelog --- CHANGELOG_UNRELEASED.md | 17 ++++++++++++++--- theories/tvs.v | 11 ++++++----- 2 files changed, 20 insertions(+), 8 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6e93ee92b..ae456e6fa 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -12,13 +12,24 @@ * implemented through a module `ConvexQuasiAssoc` containing `law` and helper lemmas + lemmas `convR_itv`, `convR_line_path` +- in `num_topology.v` + + `topologicalType` instance on `R^o` for `R : numDomainType` + - in `tvs.v` + HB classes `TopologicalNmodule`, `TopologicalZmodule`, `TopologicalLmodule` `UniformNmodule`, `UniformZmodule`, `UniformLmodule` - + mixin `TopologicalNmodule_isTopologicalNmodule`, - `TopologicalNmodule_isTopologicalLmodule` - `PreUniformNmodule_isUniformNmodule`, `PreUniformLmodule_isUniformLmodule` + + mixin `PreTopologicalNmodule_isTopologicalNmodule`, + `TopologicalNmodule_isTopologicalZmodule`, + `TopologicalZmodule_isTopologicalLmodule`, + `PreUniformNmodule_isUniformNmodule`, + `UniformNmodule_isUniformZmodule`, + `PreUniformLmodule_isUniformLmodule` + structure `topologicalLmodule` + + factories `PreTopologicalNmodule_isTopologicalZmodule`, + `TopologicalNmodule_isTopologicalLmodule`, + `PreUniformNmodule_isUniformZmodule`, + `UniformNmodule_isUniformLmodule` + + lemmas `sub_continuous`, `sub_unif_continuous` ### Changed diff --git a/theories/tvs.v b/theories/tvs.v index 76b6b62d9..0795a8b44 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -21,7 +21,7 @@ From mathcomp Require Import topology function_spaces. (* continuous addition *) (* PreTopologicalZmodule == HB class, joint of Topological and Zmodule *) (* TopologicalZmodule == HB class, joint of TopologicalNmodule and *) -(* Zmodule *) +(* Zmodule with a continuous opposite operator *) (*preTopologicalLmodType K == topological space and Lmodule over K *) (* K is a numDomainType. *) (* The HB class is PreTopologicalLmodule. *) @@ -33,6 +33,7 @@ From mathcomp Require Import topology function_spaces. (* uniformly continuous addition *) (* PreUniformZmodule == HB class, joint of Uniform and Zmodule *) (* UniformZmodule == HB class, joint of UniformNmodule and Zmodule *) +(* with uniformly continuous opposite operator *) (* PreUniformLmodule K == HB class, joint of Uniform and Lmodule over K *) (* K is a numDomainType. *) (* UniformLmodule K == HB class, joint of UniformNmodule and Lmodule *) @@ -189,11 +190,11 @@ HB.structure Definition UniformNmodule := {M of PreUniformNmodule M & PreUniform HB.structure Definition PreUniformZmodule := {M of Uniform M & GRing.Zmodule M}. -HB.mixin Record UniformNmodule_isUniformNmodule M of Uniform M & GRing.Zmodule M := { +HB.mixin Record UniformNmodule_isUniformZmodule M of 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_isUniformNmodule M}. +HB.structure Definition UniformZmodule := {M of UniformNmodule M & GRing.Zmodule M & UniformNmodule_isUniformZmodule M}. HB.factory Record PreUniformNmodule_isUniformZmodule M of Uniform M & GRing.Zmodule M := { sub_unif_continuous : unif_continuous (fun x : M * M => x.1 - x.2) @@ -233,7 +234,7 @@ by congr entourage; rewrite eqEsubset; split=> x /=; rewrite !opprK. Qed. HB.instance Definition _ := PreUniformNmodule_isUniformNmodule.Build M add_unif_continuous. -HB.instance Definition _ := UniformNmodule_isUniformNmodule.Build M opp_unif_continuous. +HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build M opp_unif_continuous. HB.end. @@ -287,7 +288,7 @@ by congr entourage; rewrite eqEsubset; split=> x /=; rewrite !scaleN1r. Qed. #[warning="-HB.no-new-instance"] -HB.instance Definition _ := UniformNmodule_isUniformNmodule.Build M opp_unif_continuous. +HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build M opp_unif_continuous. HB.instance Definition _ := PreUniformLmodule_isUniformLmodule.Build R M scale_unif_continuous. HB.end. From 89df03f5f53138275826cfbd019f70681fef5e13 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 29 May 2025 16:11:38 +0900 Subject: [PATCH 6/7] nitpicks --- CHANGELOG_UNRELEASED.md | 1 + theories/tvs.v | 254 ++++++++++++++++++++++------------------ 2 files changed, 143 insertions(+), 112 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ae456e6fa..7c65c76d1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -18,6 +18,7 @@ - in `tvs.v` + HB classes `TopologicalNmodule`, `TopologicalZmodule`, `TopologicalLmodule` `UniformNmodule`, `UniformZmodule`, `UniformLmodule` + + notation `topologicalZmodType` + mixin `PreTopologicalNmodule_isTopologicalNmodule`, `TopologicalNmodule_isTopologicalZmodule`, `TopologicalZmodule_isTopologicalLmodule`, diff --git a/theories/tvs.v b/theories/tvs.v index 0795a8b44..fe4359304 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -12,41 +12,43 @@ From mathcomp Require Import topology function_spaces. (* *) (* 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. *) -(* PreTopologicalNmodule == HB class, joint of Topological and Nmodule *) -(* TopologicalNmodule == HB class, PreTopologicalNmodule with a *) -(* continuous addition *) -(* PreTopologicalZmodule == HB class, joint of Topological and Zmodule *) -(* TopologicalZmodule == HB class, joint 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, joint of Uniform and Nmodule *) -(* UniformNmodule == HB class, joint of Uniform and Nmodule with a *) -(* uniformly continuous addition *) -(* PreUniformZmodule == HB class, joint of Uniform and Zmodule *) -(* UniformZmodule == HB class, joint of UniformNmodule and Zmodule *) -(* with uniformly continuous opposite operator *) -(* PreUniformLmodule K == HB class, joint of Uniform and Lmodule over K *) -(* K is a numDomainType. *) -(* UniformLmodule K == HB class, joint of UniformNmodule and Lmodule *) -(* with a uniformly continuous scaling operation *) -(* K is a numFieldType. *) -(* convex A == A : set M is a convex set of elements of M *) -(* M is an Lmodule over R : numDomainType. *) -(* tvsType R == interface type for a locally convex topological *) -(* vector space on a numDomain R *) -(* A tvs is constructed over a uniform space. *) -(* The HB class is Tvs. *) -(*PreTopologicalLmod_isTvs == factory allowing the construction of a tvs from *) -(* an Lmodule which is also a topological space. *) +(* 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. *) +(* 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. *) +(* convex A == A : set M is a convex set of elements of M *) +(* M is an Lmodule over R : numDomainType. *) +(* tvsType R == interface type for a locally convex *) +(* tvs on a numDomain R *) +(* A tvs is constructed over a uniform space. *) +(* The HB class is Tvs. *) +(* PreTopologicalLmod_isTvs == factory allowing the construction of a tvs *) +(* from an Lmodule which is also a topological *) +(* space *) (* ``` *) (* HB instances: *) (* - The type R^o (R : numFieldType) is endowed with the structure of Tvs. *) @@ -80,7 +82,8 @@ HB.structure Definition NbhsLmodule (K : numDomainType) := HB.structure Definition PreTopologicalNmodule := {M of Topological M & GRing.Nmodule M}. -HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M of PreTopologicalNmodule M := { +HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M + of PreTopologicalNmodule M := { add_continuous : continuous (fun x : M * M => x.1 + x.2) ; }. @@ -90,14 +93,18 @@ HB.structure Definition TopologicalNmodule := HB.structure Definition PreTopologicalZmodule := {M of Topological M & GRing.Zmodule M}. -HB.mixin Record TopologicalNmodule_isTopologicalZmodule M of Topological M & GRing.Zmodule M := { +HB.mixin Record TopologicalNmodule_isTopologicalZmodule M + of 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}. + {M of TopologicalNmodule M & GRing.Zmodule M + & TopologicalNmodule_isTopologicalZmodule M}. -HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M of Topological M & GRing.Zmodule M := { +HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M + of Topological M & GRing.Zmodule M := { sub_continuous : continuous (fun x : M * M => x.1 - x.2) ; }. @@ -106,41 +113,42 @@ HB.builders Context M of PreTopologicalNmodule_isTopologicalZmodule M. Lemma opp_continuous : continuous (-%R : M -> M). Proof. move=> x; rewrite /continuous_at. -rewrite -(@eq_cvg _ _ _ (fun x : M => 0 - x)); last first. - move=> y; exact: add0r. +rewrite -(@eq_cvg _ _ _ (fun x => 0 - x)); last by move=> y; exact: add0r. rewrite -[- x]add0r. -apply: (@continuous_comp _ _ _ (fun x => (0, x)) (fun x : M * M => x.1 - x.2) ); last exact: sub_continuous. -apply: cvg_pair => /=; first exact: cvg_cst. -exact: cvg_id. +apply: (@continuous_comp _ _ _ (fun x => (0, x)) (fun x : M * M => x.1 - x.2)). + by apply: cvg_pair => /=; [exact: cvg_cst|exact: cvg_id]. +exact: sub_continuous. Qed. Lemma add_continuous : continuous (fun x : M * M => x.1 + x.2). Proof. move=> x; rewrite /continuous_at. -rewrite -(@eq_cvg _ _ _ (fun x : M * M => x.1 - (- x.2))); last first. +rewrite -(@eq_cvg _ _ _ (fun x => x.1 - (- x.2))); last first. by move=> y; rewrite opprK. rewrite -[in x.1 + _](opprK x.2). -apply: (@continuous_comp _ _ _ (fun x : M * M => (x.1, - x.2)) (fun x : M * M => x.1 - x.2) ); last exact: sub_continuous. -apply: cvg_pair; first exact: cvg_fst. -apply: (@continuous_comp _ _ _ snd -%R); first exact: cvg_snd. -exact: opp_continuous. +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.instance Definition _ := + PreTopologicalNmodule_isTopologicalNmodule.Build M add_continuous. + +HB.instance Definition _ := + TopologicalNmodule_isTopologicalZmodule.Build M opp_continuous. HB.end. Section TopologicalZmoduleTheory. -Variables (M : TopologicalZmodule.type). +Variables (M : topologicalZmodType). Lemma sub_continuous : continuous (fun x : M * M => x.1 - x.2). Proof. -move=> x. -apply: (@continuous_comp _ _ _ (fun x : M * M => (x.1, - x.2)) (fun x : M * M => x.1 + x.2)); last exact: add_continuous. +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. -apply: (@continuous_comp _ _ _ snd -%R); first exact: cvg_snd. -exact: opp_continuous. +by apply: continuous_comp; [exact: cvg_snd|exact: opp_continuous]. Qed. End TopologicalZmoduleTheory. @@ -149,15 +157,18 @@ End TopologicalZmoduleTheory. HB.structure Definition PreTopologicalLmodule (K : numDomainType) := {M of Topological M & GRing.Lmodule K M}. -HB.mixin Record TopologicalZmodule_isTopologicalLmodule (R : numDomainType) M of Topological M & GRing.Lmodule R M := { +HB.mixin Record TopologicalZmodule_isTopologicalLmodule (R : numDomainType) M + of Topological M & GRing.Lmodule R M := { scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ; }. #[short(type="topologicalLmodType")] HB.structure Definition TopologicalLmodule (K : numDomainType) := - {M of TopologicalZmodule M & GRing.Lmodule K M & TopologicalZmodule_isTopologicalLmodule K M}. + {M of TopologicalZmodule M & GRing.Lmodule K M + & TopologicalZmodule_isTopologicalLmodule K M}. -HB.factory Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M of Topological M & GRing.Lmodule R M := { +HB.factory Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M + of Topological M & GRing.Lmodule R M := { scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ; }. @@ -166,17 +177,18 @@ HB.builders Context R M of TopologicalNmodule_isTopologicalLmodule R M. Lemma opp_continuous : continuous (-%R : M -> M). Proof. move=> x; rewrite /continuous_at. -rewrite -(@eq_cvg _ _ _ (fun x : M => -1 *: x)); last first. - by move=> y; rewrite scaleN1r. +rewrite -(@eq_cvg _ _ _ (fun x => -1 *: x)); last by move=> y; rewrite scaleN1r. rewrite -[- x]scaleN1r. -apply: (@continuous_comp M (R^o * M)%type M (fun x : M => (-1, x) : R^o * M) (fun x : R^o * M => x.1 *: x.2)); last exact: scale_continuous. -apply: (@cvg_pair _ _ _ _ (nbhs (-1 : R^o))); first exact: cvg_cst. -exact: cvg_id. +apply: (@continuous_comp M (R^o * M)%type M (fun x => (-1, x)) + (fun x => x.1 *: x.2)); last exact: scale_continuous. +by apply: (@cvg_pair _ _ _ _ (nbhs (-1 : R^o))); [exact: cvg_cst|exact: cvg_id]. Qed. #[warning="-HB.no-new-instance"] -HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build M opp_continuous. -HB.instance Definition _ := TopologicalZmodule_isTopologicalLmodule.Build R M scale_continuous. +HB.instance Definition _ := + TopologicalNmodule_isTopologicalZmodule.Build M opp_continuous. +HB.instance Definition _ := + TopologicalZmodule_isTopologicalLmodule.Build R M scale_continuous. HB.end. @@ -186,17 +198,21 @@ HB.mixin Record PreUniformNmodule_isUniformNmodule M of 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.structure Definition UniformNmodule := + {M of PreUniformNmodule M & PreUniformNmodule_isUniformNmodule M}. HB.structure Definition PreUniformZmodule := {M of Uniform M & GRing.Zmodule M}. -HB.mixin Record UniformNmodule_isUniformZmodule M of Uniform M & GRing.Zmodule M := { +HB.mixin Record UniformNmodule_isUniformZmodule M + of 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.structure Definition UniformZmodule := + {M of UniformNmodule M & GRing.Zmodule M & UniformNmodule_isUniformZmodule M}. -HB.factory Record PreUniformNmodule_isUniformZmodule M of Uniform M & GRing.Zmodule M := { +HB.factory Record PreUniformNmodule_isUniformZmodule M + of Uniform M & GRing.Zmodule M := { sub_unif_continuous : unif_continuous (fun x : M * M => x.1 - x.2) }. @@ -204,37 +220,38 @@ HB.builders Context M of PreUniformNmodule_isUniformZmodule M. Lemma opp_unif_continuous : unif_continuous (-%R : M -> M). Proof. -have unif: unif_continuous (fun x => (0, x) : M * M). +have unif : unif_continuous (fun x => (0, x) : M * M). move=> /= U [[]] /= U1 U2 [] U1e U2e /subsetP U12. - rewrite /nbhs/=. - apply: (@filterS _ _ entourage_filter U2) => // x xU2 /=. - have /U12: ((0, 0), x) \in U1 `*` U2. - rewrite in_setX/=; apply/andP; split; apply/asboolP => //. - exact: entourage_refl. - by rewrite inE/= => [[[]]] [] a1 a2 [] b1 b2/= abU [] {2}<- <- <-/=. -move=> /= U /sub_unif_continuous/unif/=. -rewrite /nbhs/=. -rewrite -comp_preimage/=/comp/=. -by congr entourage; rewrite eqEsubset; split=> x /=; rewrite !add0r. + 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/=. +by congr entourage => /=; rewrite eqEsubset; split=> x /=; rewrite !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))); last first. - 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=> /= [] [] a1 a2 [] b1 b2/= [] ab1 ab2. - have /U12: (a1, b1, (-a2, -b2)) \in U1 `*` U2 by rewrite !inE/=. - by rewrite inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-. + 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 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 !opprK. Qed. -HB.instance Definition _ := PreUniformNmodule_isUniformNmodule.Build M add_unif_continuous. -HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build M opp_unif_continuous. +HB.instance Definition _ := + PreUniformNmodule_isUniformNmodule.Build M add_unif_continuous. +HB.instance Definition _ := + UniformNmodule_isUniformZmodule.Build M opp_unif_continuous. HB.end. @@ -243,15 +260,17 @@ 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). +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))); last first. - 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=> /= [] [] a1 a2 [] b1 b2/= [] ab1 ab2. -have /U12: (a1, b1, (-a2, -b2)) \in U1 `*` U2 by rewrite !inE/=. -by rewrite inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-. +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 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. @@ -259,13 +278,17 @@ End UniformZmoduleTheory. HB.structure Definition PreUniformLmodule (K : numDomainType) := {M of Uniform M & GRing.Lmodule K M}. -HB.mixin Record PreUniformLmodule_isUniformLmodule (R : numFieldType) M of PreUniformLmodule R M := { +HB.mixin Record PreUniformLmodule_isUniformLmodule (R : numFieldType) M + of 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.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 of PreUniformLmodule R M := { +HB.factory Record UniformNmodule_isUniformLmodule (R : numFieldType) M + of PreUniformLmodule R M := { scale_unif_continuous : unif_continuous (fun z : R^o * M => z.1 *: z.2) ; }. @@ -276,10 +299,10 @@ Proof. have unif: unif_continuous (fun x => (-1, x) : R^o * M). move=> /= U [[]] /= U1 U2 [] U1e U2e /subsetP U12. rewrite /nbhs/=. - apply: (@filterS _ _ entourage_filter U2) => // x xU2 /=. - have /U12: ((-1, -1), x) \in U1 `*` U2. - rewrite in_setX/=; apply/andP; split; apply/asboolP => //. - exact: entourage_refl. + 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 inE/= => [[[]]] [] a1 a2 [] b1 b2/= abU [] {2}<- <- <-/=. move=> /= U /scale_unif_continuous/unif/=. rewrite /nbhs/=. @@ -288,8 +311,10 @@ by congr entourage; rewrite eqEsubset; split=> x /=; rewrite !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.instance Definition _ := + UniformNmodule_isUniformZmodule.Build M opp_unif_continuous. +HB.instance Definition _ := + PreUniformLmodule_isUniformLmodule.Build R M scale_unif_continuous. HB.end. @@ -564,8 +589,10 @@ 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 R^o standard_add_continuous. -HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R R^o standard_scale_continuous . +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_isTvs.Build R R^o standard_locally_convex. End standard_topology. @@ -618,8 +645,11 @@ move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2] l0 l1. by split; rewrite -inE; [apply: Bcb; rewrite ?inE|apply: Bcf; rewrite ?inE]. 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_isTvs.Build K (E * F)%type prod_locally_convex. +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_isTvs.Build K (E * F)%type prod_locally_convex. End prod_Tvs. From 7b745b4d6a1f6bcfe153ceb7c3eecf3425a60b7e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 29 May 2025 16:29:49 +0900 Subject: [PATCH 7/7] nitpicks --- theories/topology_theory/num_topology.v | 46 +++++++++++-------------- 1 file changed, 20 insertions(+), 26 deletions(-) diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index ddd0fa8fc..7a213364c 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -36,24 +36,19 @@ split. move=> [] e e0 /subsetP/(_ p). by rewrite !in_setE/= subrr normr0. split=> [|P Q|P Q]. -- exists 1; first exact: ltr01. - exact: subsetT. +- by exists 1; [exact: ltr01|exact: subsetT]. - move=> [] /= e e0 /subsetP eP [] /= f f0 /subsetP fQ. exists (Order.min e f) => /=. - rewrite [Num.min e f]/(Order.min e f). - by case: ifP. + by rewrite [Num.min e f]/(Order.min e f); case: ifP. apply/subsetP => x. rewrite in_setE in_setI/= => pef. apply/andP; split. - apply/eP; rewrite in_setE/=. - apply: (lt_le_trans pef). - case: (@real_ltP _ e f) => //; exact: gtr0_real. - apply/fQ; rewrite in_setE/=. - apply: (lt_le_trans pef). - case: (@real_ltP _ f e) => //; exact: gtr0_real. + apply/eP/mem_set/(lt_le_trans pef). + by case: (@real_ltP _ e f) => //; exact: gtr0_real. + apply/fQ/mem_set/(lt_le_trans pef). + by case: (@real_ltP _ f e) => //; exact: gtr0_real. - move=> PQ [] /= e e0 eP. - exists e => //. - exact: (subset_trans eP). + by exists e => //; exact: (subset_trans eP). Qed. Lemma nbhs_singleton (p : R^o) (A : set R) : nbhs p A -> A p. @@ -64,26 +59,25 @@ Qed. Lemma nbhs_nbhs (p : R^o) (A : set R) : nbhs p A -> nbhs p (nbhs^~ A). Proof. -move=> [] /= e e0 /subsetP eA. -exists e => //. -apply/subsetP => x. -rewrite !inE/= => xe. +move=> [] /= e e0 /subsetP eA; exists e => //. +apply/subsetP => x /[!inE]/= xe. exists (e - `|p - x|); first by rewrite /= subr_gt0. -apply/subsetP => y. -rewrite inE/= -subr_gt0 -addrA -opprD subr_gt0 => ye. -apply: eA; rewrite inE/=. -have ->: p - y = (p - x) + (x - y). - by rewrite addrA; congr (_ - _); rewrite -addrA addNr addr0. -exact: (le_lt_trans (ler_normD _ _) ye). +apply/subsetP => y; rewrite inE/= ltrBrDl => ye. +apply/eA/mem_set => /=. +by rewrite -(subrK x p) -addrA (le_lt_trans (ler_normD _ _)). Qed. + End TopologicalNumDomainType. + End TopologicalNumDomainType. -HB.instance Definition _ (R : numDomainType) := Nbhs_isNbhsTopological.Build R^o (@TopologicalNumDomainType.nbhs_filter R) (@TopologicalNumDomainType.nbhs_singleton R) (@TopologicalNumDomainType.nbhs_nbhs R). +HB.instance Definition _ (R : numDomainType) := Nbhs_isNbhsTopological.Build R^o + (@TopologicalNumDomainType.nbhs_filter R) + (@TopologicalNumDomainType.nbhs_singleton R) + (@TopologicalNumDomainType.nbhs_nbhs R). -HB.instance Definition _ (R : numFieldType) := - Nbhs_isPseudoMetric.Build R R^o - nbhs_ball_normE ball_norm_center ball_norm_symmetric ball_norm_triangle erefl. +HB.instance Definition _ (R : numFieldType) := Nbhs_isPseudoMetric.Build R R^o + nbhs_ball_normE ball_norm_center ball_norm_symmetric ball_norm_triangle erefl. HB.instance Definition _ (R : numFieldType) := Uniform_isPseudoMetric.Build R R^o