From 690d14b28b73a76c1c301f1c86d110b81be08611 Mon Sep 17 00:00:00 2001
From: mkerjean <kerjean@lipn.fr>
Date: Fri, 17 Nov 2023 13:09:10 +0100
Subject: [PATCH] initial draft definition of Evt

---
 theories/topology.v | 41 +++++++++++++++++++++++++++++++++++++++--
 1 file changed, 39 insertions(+), 2 deletions(-)

diff --git a/theories/topology.v b/theories/topology.v
index 33602e38e..50333b20e 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -4762,7 +4762,45 @@ End sup_uniform.
 HB.instance Definition _ (I : Type) (T : I -> uniformType) :=
   Uniform.copy (prod_topology T)
     (sup_topology (fun i => Uniform.class
-      [the uniformType of weak_topology (@proj _ T i)])).
+                           [the uniformType of weak_topology (@proj _ T i)])).
+
+(** Uniform of Normed Domain**)
+
+
+HB.instance Definition _ (R : zmodType) := isPointed.Build R 0.
+
+HB.instance Definition _ (R : zmodType) := Pointed.on R^o.
+
+HB.howto GRing.regular topologicalType.
+
+Definition numDomain_axiom (R : numDomainType) : Pointed_isBaseTopological R^o.
+Admitted.
+HB.instance Definition _ (R : numDomainType) := numDomain_axiom R.
+
+(** * Topological vector spaces                *)
+
+Definition convex (R : numDomainType) (M : lmodType R) (A : set M) :=
+  forall x y lambda, lambda *: x + (1 - lambda) *: y \in A. 
+
+HB.mixin Record Uniform_isTopvec (R : numDomainType) E of Uniform E & GRing.Lmodule R E := {
+    add_continuous : continuous (uncurry (@GRing.add E));
+    scale_continuous : continuous (uncurry (@GRing.scale R E) : R^o * E -> E);
+    locally_convex : exists B : set (set E), (forall b, b \in B -> convex b) /\ (basis B)     
+  }.
+
+HB.structure Definition Evt (R : numDomainType) :=
+  {E of Uniform_isTopvec R E & Uniform E & GRing.Lmodule R E}. 
+
+HB.factory Record Topological_isTopvec (R : numDomainType) E
+      of Topological E & GRing.Lmodule R E := {
+    add_continuous : continuous (uncurry (@GRing.add E));
+    scale_continuous : continuous (uncurry (@GRing.scale R E) : R^o * E -> E);
+    locally_convex : exists B : set (set E), (forall b, b \in B -> convex b) /\ (basis B)     
+  }.
+HB.builders Context R E of Topological_isTopvec R E.
+    
+HB.end.
+
 
 (** * PseudoMetric spaces defined using balls *)
 
@@ -5465,7 +5503,6 @@ HB.instance Definition _ (T : choiceType) (R : numFieldType)
     (U : completePseudoMetricType R) :=
   Uniform_isComplete.Build (T -> U) cauchy_cvg.
 
-HB.instance Definition _ (R : zmodType) := isPointed.Build R 0.
 
 Lemma compact_cauchy_cvg {T : uniformType} (U : set T) (F : set_system T) :
   ProperFilter F -> cauchy F -> F U -> compact U -> cvg F.