diff --git a/_CoqProject b/_CoqProject
index fdbf17db9..a81ecb39c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -143,6 +143,8 @@ theories/kernel.v
 theories/pi_irrational.v
 theories/gauss_integral.v
 
+theories/hahn_banach_theorem.v
+
 theories/all_analysis.v
 
 theories/showcase/summability.v
diff --git a/classical/filter.v b/classical/filter.v
index 4d4c625fd..881e098d8 100644
--- a/classical/filter.v
+++ b/classical/filter.v
@@ -245,6 +245,11 @@ HB.structure Definition Nbhs := {T of Choice T & hasNbhs T}.
 #[short(type="pnbhsType")]
 HB.structure Definition PointedNbhs := {T of Pointed T & hasNbhs T}.
 
+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 NbhsLmodule (K : numDomainType) :=
+  {M of Nbhs M & GRing.Lmodule K M}.
+
 Definition filter_from {I T : Type} (D : set I) (B : I -> set T) :
   set_system T := [set P | exists2 i, D i & B i `<=` P].
 
diff --git a/theories/Make b/theories/Make
index ea73a4022..c37944d81 100644
--- a/theories/Make
+++ b/theories/Make
@@ -104,6 +104,9 @@ probability_theory/beta_distribution.v
 probability_theory/probability.v
 
 convex.v
+
+hahn_banach_theorem.v
+
 charge.v
 kernel.v
 pi_irrational.v
diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v
new file mode 100644
index 000000000..dcf018936
--- /dev/null
+++ b/theories/hahn_banach_theorem.v
@@ -0,0 +1,733 @@
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import interval_inference.
+From mathcomp Require Import wochoice boolp classical_sets topology reals.
+From mathcomp Require Import filter reals normedtype.
+Import numFieldNormedType.Exports.
+Local Open Scope classical_set_scope.
+
+(* Marie's proposal: encode the "partial" properties by reasoning on
+  the graph of functions. The other option would be to study a partial
+  order defined on subsets of the ambiant space V, on which it is possible
+  to obtain a bounded lineEar form extending f. But this options seems much
+  less convenient, in particular when establishing that one can extend f
+  on a space with one more dimension. Indeed, exhibiting a term of type
+  V -> R requires a case ternary analysis on F, the new line, and an
+  explicit direct sum to ensure the definition is exhaustive. Working with
+  graphs allows to leave this argument completely implicit. *)
+
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+
+
+Search "choice_prop". 
+
+Definition Choice_prop := ((forall T U  (Q : T -> U -> Prop),
+                                (forall t : T, exists u : U,  Q t u) -> (exists e, forall t,  Q t (e t)))).
+
+
+ Local Open Scope ring_scope.
+ Import GRing.Theory.
+ Import Num.Theory.
+
+Section SetPredRels.
+
+ Variables T U : Type.
+ Implicit Types f g : T -> U -> Prop.
+ (* Functional (possibly empty or partial) graphs *)
+ Definition functional f :=
+   forall v r1 r2, f v r1 -> f v r2 -> r1 = r2.
+
+End SetPredRels.
+
+
+Section OrderRels.
+
+ Variable (R : numDomainType).
+
+ (* Upper bound *)
+ Definition ubd (s : set R) (a : R) := forall x, s x -> x <= a.
+
+ (* Lower bound *)
+ Definition ibd (s : set R) (a : R) := forall x, s x -> a <= x.
+
+ (* the intension is that f is the graph of a function bounded by p *)
+ Definition maj_by T p (f : T -> R -> Prop) :=
+   forall v r, f v r -> r <= p v.
+
+ End OrderRels.
+
+
+ Section LinAndCvx.
+
+ Variables (R : numDomainType) (V : lmodType R).
+
+ Definition convex_fun (p : V -> R) :=  forall v1 v2 l m,
+   ( 0 <= l /\ 0 <= m) ->  l + m = 1 -> p (l *: v1 + m *: v2) <= l * (p v1) + m * (p v2).
+
+ Definition linear_rel (f : V -> R -> Prop) :=
+   forall v1 v2 l r1 r2,  f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2).
+
+ Variable f : V -> R -> Prop.
+ Hypothesis lrf : linear_rel f.
+
+ Lemma linrel_00 x r : f x r -> f 0 0.
+ Proof.
+ suff -> : f 0 0 = f (x + (-1) *: x) (r + (-1) * r) by move=> h; apply: lrf.
+ by rewrite scaleNr mulNr mul1r scale1r !subrr.
+ Qed.
+
+ Lemma linrel_scale x r l : f x r -> f (l *: x) (l * r).
+ Proof.
+ move=> fxr.
+ have -> : f (l *: x) (l * r) = f (0 + l *: x) (0 + l * r) by rewrite !add0r.
+ by apply: lrf=> //; apply: linrel_00 fxr.
+ Qed.
+
+ Lemma linrel_add x1 x2 r1 r2 : f x1 r1 -> f x2 r2 -> f (x1 - x2)(r1 - r2).
+ Proof.
+     have -> : x1 - x2 = x1 + (-1) *: x2 by rewrite scaleNr scale1r.
+     have -> : r1 - r2 = r1 + (-1) * r2 by rewrite mulNr mul1r.
+     by apply: lrf.
+ Qed.
+
+
+ Definition add_line f w a := fun v r =>
+   exists v' : V, exists r' : R, exists lambda : R,
+         [/\ f v' r', v = v' + lambda *: w & r = r' + lambda * a].
+
+ End LinAndCvx.
+
+
+ Section HBPreparation.
+
+ Variable Choice_prop :  forall T U (P : T -> U -> Prop),
+     (forall t : T, exists u : U,  P t u) -> (exists e, forall t,  P t (e t)).
+
+ Variables (R : realFieldType) (V : lmodType R).
+
+ Variables (F G : set V) (phi : V -> R) (p : V -> R).
+
+Hypothesis linphiF : forall v1 v2 l, F v1 -> F v2 ->
+                              phi (v1 + l *: v2) = phi v1 + l * (phi v2).
+
+ Implicit Types (f g : V -> R -> Prop).
+
+ Hypothesis F0 : F 0.
+
+Fact phi0 : phi 0 = 0.
+Proof.
+have -> : 0 = 0 + (-1) *: 0 :> V by rewrite scaler0 addr0.
+by rewrite linphiF // mulN1r addrN.
+Qed.
+
+ Hypothesis p_cvx : convex_fun p.
+
+ Hypothesis sup : forall (A : set R) (a m : R),
+     A a -> ubd A m ->
+     {s : R | ubd A s /\ forall u, ubd A u -> s <= u}.
+
+ Hypothesis inf : forall (A : set R) (a m : R),
+     A a ->  ibd A m ->
+     {s : R | ibd A s /\ forall u, ibd A u -> u <= s}.
+
+ (* f is a subset of (V x R), if v is in pi_1 f, then (v, phi v) is in f.
+    Otherwise said, the graph of phi restructed to pi_1 f is included in f*)
+
+ Definition prol f := forall v, F v -> f v (phi v).
+
+ Definition spec (f : V -> R -> Prop) :=
+   [/\ functional f, linear_rel f, maj_by p f &  prol f].
+
+ Record zorn_type : Type := ZornType
+   {carrier : V -> R -> Prop; specP : spec carrier}.
+
+ Hypothesis spec_phi : spec (fun v r => F v /\ r = phi v).
+
+ Definition zphi := ZornType spec_phi.
+
+ Lemma zorn_type_eq z1 z2 : carrier z1 = carrier z2 -> z1 = z2.
+ Proof.
+ case: z1 => m1 pm1; case: z2 => m2 pm2 /= e; move: pm1 pm2; rewrite e => pm1 pm2.
+ by congr ZornType; apply: Prop_irrelevance.
+ Qed.
+
+  Definition zorn_rel (z1 z2 : zorn_type):= forall x y, (carrier z1 x y) ->  (carrier z2 x y ). 
+ 
+ (* Zorn applied to the relation of extending the graph of the first function *)
+ Lemma zorn_rel_ex : exists g : zorn_type, forall z, zorn_rel g z -> z = g.
+ Proof.
+ pose Rbool := (fun x y => `[< zorn_rel x y >]).
+ have RboolP : forall z t, Rbool z t <-> zorn_rel z t by split; move => /asboolP //=. 
+ suff [t st]:  exists t : zorn_type, forall s : zorn_type, Rbool t s -> s = t. 
+    by exists t;  move => z /RboolP tz; apply: st. 
+         apply: (@Zorn zorn_type Rbool).
+ - by move => t; apply/RboolP. 
+ - by move => r s t /RboolP  a /RboolP  b; apply/RboolP => x y /a /b. 
+ - move => r s /RboolP a /RboolP b; apply: zorn_type_eq.
+   by apply: funext => z; apply: funext => h;apply: propext; split => [/a | /b]. 
+ - move => A Amax.
+ case: (lem (exists a, A a)) => [[w Aw] | eA]; last first.
+   by exists zphi => a Aa; elim: eA; exists a.
+ (* g is the union of the graphs indexed by elements in a *)
+ pose g v r := exists a, A a /\ (carrier a v r).
+ have g_fun : functional g.
+   move=> v r1 r2 [a [Aa avr1]] [b [Ab bvr2]].
+   have [] : Rbool a b \/ Rbool b a by exact: Amax.
+      - rewrite /Rbool /RboolP /zorn_rel; case: b Ab bvr2 {Aa}.
+        move => s2 [fs2 _ _ _] /= _ s2vr2 /asboolP ecas2.
+     by move/ecas2: avr1 => /fs2 /(_ s2vr2).
+   - rewrite /Rbool /RboolP  /zorn_rel; case: a Aa avr1 {Ab} => s1 [fs1 _ _ _] /= _ s1vr1 /asboolP ecbs1.
+     by move/ecbs1: bvr2; apply: fs1.
+ have g_lin : linear_rel g.
+   move=> v1 v2 l r1 r2 [a1 [Aa1 c1]] [a2 [Aa2 c2]]. 
+   have [/RboolP sc12 | /RboolP sc21] := Amax _ _ Aa1 Aa2.
+   - have {c1 sc12 Aa1 a1} c1 :  carrier a2 v1 r1 by apply: sc12.
+     exists a2; split=> //; case: a2 {Aa2} c2 c1 => c /= [_ hl _ _] *; exact: hl.
+   - have {c2 sc21 Aa2 a2} c2 :  carrier a1 v2 r2 by apply: sc21.
+     exists a1; split=> //; case: a1 {Aa1} c2 c1 => c /= [_ hl _ _] *; exact: hl.
+ have g_majp : maj_by p g by move=> v r [[c [fs1 ls1 ms1 ps1]]] /= [_ /ms1].
+ have g_prol : prol g.
+   move=> *; exists w; split=> //; case: w Aw => [c [_ _ _ hp]] _ //=; exact: hp.
+ have spec_g : spec g by split.
+ pose zg := ZornType spec_g.
+ by  exists zg => [a Aa]; apply/RboolP; rewrite /zorn_rel  => v r cvr; exists a.
+ Qed. 
+
+ 
+ Variable g : zorn_type.
+
+ Hypothesis gP : forall z, zorn_rel g z -> z = g.
+
+ (*The next lemma proves that when z is of zorn_type, it can be extended on any
+  real line directed by an arbitrary vector v *)
+
+ Lemma domain_extend  (z : zorn_type) v :
+     exists2 ze : zorn_type, (zorn_rel z ze) & (exists r, (carrier ze)  v r).
+ Proof.
+ case: (lem (exists r, (carrier z v r))).
+   by case=> r rP; exists z => //; exists r.
+ case: z => [c [fs1 ls1 ms1 ps1]] /= nzv.
+ have c00 : c 0 0.
+   rewrite -phi0; exact: ps1.
+ have [a aP] : exists a,  forall (x : V) (r lambda : R),
+       c x r -> r + lambda * a <= p (x + lambda *: v).
+   suff [a aP] : exists a,  forall (x : V) (r lambda : R),
+       c x r -> 0 < lambda ->
+       r + lambda * a <= p (x + lambda *: v) /\
+       r - lambda * a <= p (x - lambda *: v).
+     exists a=> x r lambda cxr.
+     have {aP} aP := aP _ _ _ cxr.
+     case: (ltrgt0P lambda) ; [by case/aP | move=> ltl0 | move->]; last first.
+       by rewrite mul0r scale0r !addr0; apply: ms1.
+     rewrite -[lambda]opprK scaleNr mulNr.
+     have /aP [] : 0 < - lambda by rewrite oppr_gt0.
+     done.
+   pose b (x : V) r lambda : R := (p (x + lambda *: v) - r) / lambda.
+   pose a (x : V) r lambda : R := (r - p (x - lambda *: v)) / lambda.
+   have le_a_b x1 x2 r1 r2 s t : c x1 r1 -> c x2 r2 -> 0 < s -> 0 < t ->
+                                 a x1 r1 s <= b x2 r2 t.
+     move=> cxr1 cxr2 lt0s lt0t; rewrite /a /b.
+     rewrite ler_pdivlMr // mulrAC ler_pdivrMr // mulrC [_ * s]mulrC.
+     rewrite !mulrDr !mulrN lerBlDr addrAC lerBrDr.
+     have /ler_pM2r <- : 0 < (s + t) ^-1 by rewrite invr_gt0 addr_gt0.
+     set y1 : V := _ + _ *: _; set y2 : V :=  _ - _ *: _.
+     set rhs := (X in _ <= X).
+     have step1 : p (s  / (s + t) *: y1 + t  / (s + t) *: y2) <= rhs.
+       rewrite /rhs !mulrDl ![_  * _ / _]mulrAC; apply: p_cvx.
+       split.
+        rewrite divr_ge0 //=.
+          by apply : ltW.
+          by rewrite addr_ge0 //= ; apply: ltW.
+        rewrite divr_ge0 //=.
+          by apply : ltW.
+          by rewrite  addr_ge0 //= ;  apply: ltW.
+     by rewrite -mulrDl mulfV //; apply: lt0r_neq0; rewrite addr_gt0.
+     apply: le_trans step1 => {rhs}.
+     set u : V := (X in p X).
+     have {u y1 y2} -> : u = t  / (s + t) *: x1 + s / (s + t) *: x2.
+       rewrite /u ![_ / _]mulrC -!scalerA -!scalerDr /y1 /y2; congr (_ *: _).
+       by rewrite !scalerDr addrCA scalerN scalerA [s * t]mulrC -scalerA addrK.
+     set l := t / _; set m := s / _; set lhs := (X in X <= _).
+     have {lhs} -> : lhs = l * r1 + m * r2.
+       by rewrite /lhs mulrDl ![_  * _ / _]mulrAC.
+     apply: ms1; apply: (ls1) => //.
+     rewrite -[_ *: _]add0r -[_ * _] add0r; apply: ls1 => //.
+     pose Pa : set R := fun r =>  exists x1, exists r1, exists s1,
+       [/\ c x1 r1, 0 < s1 & r = a x1 r1 s1].
+     pose Pb : set R := fun r =>  exists x1, exists r1, exists s1,
+       [/\ c x1 r1, 0 < s1 & r = b x1 r1 s1].
+     have exPa : Pa (a 0 0 1) by exists 0; exists 0; exists 1; split.
+     have exPb : Pb (b 0 0 1) by exists 0; exists 0; exists 1; split.
+     have majPa x : Pa x -> x <= b 0 0 1.
+       move=> [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01.
+     have minPb x : Pb x -> a 0 0 1 <= x.
+       move=> [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01.
+     have [sa [ubdP saP]]:= sup exPa majPa; have [ib [ibdP ibP]]:= inf exPb minPb.
+     have le_sa_ib : sa <= ib.
+       apply: saP=> r' [y [r [l [cry lt0l -> {r'}]]]].
+       apply: ibP=> s' [z [s [m [crz lt0m -> {s'}]]]]; exact: le_a_b.
+     pose alpha := ((sa + ib) / 2%:R).
+     have le_alpha_ib : alpha <= ib by rewrite /alpha midf_le.
+     have le_sa_alpha : sa <= alpha by rewrite /alpha midf_le.
+     exists alpha => x r l cxr lt0l; split.
+     - suff : alpha <= b x r l.
+         by rewrite /b; move/ler_pdivlMr: lt0l->; rewrite lerBrDl mulrC.
+       by apply: le_trans le_alpha_ib _; apply: ibdP; exists x; exists r; exists l.
+     - suff : a x r l <= alpha.
+         rewrite /a. move/ler_pdivrMr: lt0l->.
+         by rewrite lerBlDl -lerBlDr mulrC.
+       by apply: le_trans le_sa_alpha; apply: ubdP; exists x; exists r; exists l.
+ pose z' := add_line c v a.
+ have z'_extends :  forall v r, c v r -> z' v r.
+   move=> x r cxr; exists x; exists r; exists 0; split=> //.
+   - by rewrite scale0r addr0.
+   - by rewrite mul0r addr0.
+ have z'_prol : prol z'.
+   move=> x /ps1 cxphix; exists x; exists (phi x); exists 0; split=> //.
+   - by rewrite scale0r addr0.
+   - by rewrite mul0r addr0.
+ - have z'_maj_by_p : maj_by p z'.
+   by move=> x r [w [s [l [cws -> ->]]]]; apply: aP.
+ - have z'_lin : linear_rel z'.
+   move=> x1 x2 l r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 -> ->]]]].
+   set w := (X in z' X _); set s := (X in z' _ X).
+   have {w} -> : w = w1 + l *: w2 + (m1 + l * m2) *: v.
+     by rewrite /w !scalerDr !scalerDl scalerA -!addrA [X in _ + X]addrCA.
+   have {s} -> : s = s1 + l * s2 + (m1 + l * m2) * a.
+     by rewrite /s !mulrDr !mulrDl mulrA -!addrA [X in _ + X]addrCA.
+   exists (w1 + l *: w2); exists (s1 + l * s2); exists (m1 + l * m2); split=> //.
+   exact: ls1.
+ - have z'_functional : functional z'.
+   move=> w r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 e1 ->]]]].
+   have h1 (x : V) (r l : R) : x = l *: v ->  c x r -> x = 0 /\ l = 0.
+     move=> -> cxr; case: (l =P 0) => [-> | /eqP ln0]; first by rewrite scale0r.
+     suff cvs: c v (l^-1 * r) by elim:nzv; exists (l^-1 * r).
+     suff -> : v = l ^-1 *: (l *: v) by exact: linrel_scale.
+     by rewrite scalerA mulVf ?scale1r.
+   have [rw12 erw12] : exists r,  c (w1 - w2) r.
+     exists (s1 + (-1) * s2).
+     have -> : w1 - w2 = w1 + (-1) *: w2 by rewrite scaleNr scale1r.
+     by apply: ls1.
+   have [ew12 /eqP]: w1 - w2 = 0 /\ (m2 - m1 = 0).
+     apply: h1 erw12; rewrite scalerBl; apply/eqP; rewrite subr_eq addrC addrA.
+     by rewrite -subr_eq opprK e1.
+   suff -> : s1 = s2 by rewrite subr_eq0=> /eqP->.
+   by apply: fs1 cws2; move/eqP: ew12; rewrite subr_eq0=> /eqP<-.
+ have z'_spec : spec z' by split.
+ pose zz' := ZornType z'_spec.
+ exists zz'; rewrite /zorn_rel => //=; exists a; exists 0; exists 0; exists 1.
+ by rewrite add0r mul1r scale1r add0r; split.
+ Qed.
+
+ Lemma tot_g v : exists r, carrier g v r.
+ Proof.
+ have [z /gP sgz [r zr]]:= domain_extend g v.
+ by exists r; rewrite -sgz.
+ Qed.
+
+
+Lemma hb_witness : exists h : V -> R, forall v r, carrier g v r <-> (h v = r).
+Proof.
+have [h hP] : exists h,  forall v, carrier g v (h v) by exact: Choice_prop tot_g.
+exists h => v r.
+split; last by move<-.
+case: g gP tot_g hP => c /= [fg lg mg pg] => gP' tot_g' hP cvr.
+by have -> // := fg v r (h v).
+Qed.
+
+
+ End HBPreparation.
+
+
+ Section HahnBanachold.
+(* Now we prove HahnBanach on functions*)
+(* We consider R a real (=ordered) field with supremum, and V a (left) module
+   on R. We do not make use of the 'vector' interface as the latter enforces
+   finite dimension. *)
+  
+
+Variable Choice_prop :  forall T U (P : T -> U -> Prop),
+     (forall t : T, exists u : U,  P t u) -> (exists e, forall t,  P t (e t)).
+  
+Variables (R : realFieldType) (V : lmodType R).
+
+Hypothesis sup : forall (A : set R) (a m : R),
+    A a -> ubd A m ->
+    {s : R | ubd A s /\ forall u, ubd A u -> s <= u}. 
+
+(* This could be obtained from sup but we are lazy here *)
+Hypothesis inf : forall (A : set R) (a m : R),
+    A a ->  ibd A m ->
+    {s : R | ibd A s /\ forall u, ibd A u -> u <= s}.
+
+(* F and G are of type V -> bool, as required by the Mathematical Components
+   interfaces. f is a linear application from (the entire) V to R. *)
+Variables (F G : pred V) (f : V -> R) (p : V -> R).
+
+(* MathComp seems to lack of an interface for submodules of V, so for now
+   we state "by hand" that F is closed under linear combinations. *)
+Hypothesis F0 : F 0.
+Hypothesis linF : forall v1 v2 l, F v1 -> F v2 -> F (v1 + l *: v2).
+
+Hypothesis linfF : forall v1 v2 l, F v1 -> F v2 -> 
+                              f (v1 + l *: v2) = f v1 + l * (f v2).
+
+(* In fact we do not need G to be a superset of F *)
+(* Hypothesis sFG : subpred F G. *)
+
+Hypothesis p_cvx : convex_fun p.
+
+Hypothesis f_bounded_by_p : forall x, F x -> f x <= p x.
+
+Theorem HahnBanachold : exists g : {scalar V}, 
+  (forall x,  g x <= p x) /\ (forall x, F x -> g x = f x).
+pose graphF v r := F v /\ r = f v.
+have func_graphF : functional graphF by move=> v r1 r2 [Fv ->] [_ ->].
+have lin_graphF : linear_rel graphF.
+  move=> v1 v2 l r1 r2 [Fv1 ->] [Fv2 ->]; split; first exact: linF.
+  by rewrite linfF.
+have maj_graphF : maj_by p graphF by move=> v r [Fv ->]; exact: f_bounded_by_p.
+
+have prol_graphF : prol F f graphF by move=> v Fv; split.
+have graphFP : spec F f p graphF by split.
+have [z zmax]:= zorn_rel_ex graphFP.
+pose FP v : Prop := F v.
+have FP0 : FP 0 by [].
+have [g gP]:= hb_witness Choice_prop linfF FP0 p_cvx sup inf zmax.
+have scalg : linear_for *%R g.
+  case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP.
+  have addg : additive g.
+     move=> w1 w2;  apply/gP.
+     apply: linrel_add.
+     exact ls1.
+     by apply /gP.
+     by apply /gP.
+  suff scalg : scalable_for  *%R g.
+    move=> a u v.
+    rewrite -gP.
+    rewrite (addrC _ v).
+    rewrite (addrC _ (g v)).
+    apply: ls1.
+    by apply /gP.
+    by apply /gP.
+  by move=> w l; apply/gP; apply: linrel_scale=> //; apply/gP.
+pose H := GRing.isLinear.Build _ _ _ _ g scalg.
+pose g' : {linear V -> R | *%R} := HB.pack g H.
+exists g'.
+have grxtf v : F v -> g v = f v.
+  move=> Fv; apply/gP; case: z {zmax gP} => [c [_ _ _ pf]] /=; exact: pf.
+  suff pmajg v :  g v <= p v by split.
+    by  case: z {zmax} gP => [c [_ _ bp _]] /= gP; apply/bp/gP.
+Qed.
+
+End HahnBanachold.
+
+ 
+
+Section HahnBanachnew.
+(* Now we prove HahnBanach on functions*)
+(* We consider R a real (=ordered) field with supremum, and V a (left) module
+   on R. We do not make use of the 'vector' interface as the latter enforces
+   finite dimension. *)
+
+Variable Choice_prop :  forall T U (P : T -> U -> Prop),
+     (forall t : T, exists u : U,  P t u) -> (exists e, forall t,  P t (e t)).
+
+Variables (R : realFieldType) (V : lmodType R).
+
+Hypothesis sup : forall (A : set R) (a m : R),
+    A a -> ubd A m ->
+    {s : R | ubd A s /\ forall u, ubd A u -> s <= u}.
+
+(* This could be obtained from sup but we are lazy here *)
+Hypothesis inf : forall (A : set R) (a m : R),
+    A a ->  ibd A m ->
+    {s : R | ibd A s /\ forall u, ibd A u -> u <= s}.
+
+Variables (F : subLmodType V) (f : {linear F -> R}) (p : V -> R).
+
+Hypothesis p_cvx : convex_fun p.
+
+Hypothesis f_bounded_by_p : forall x : F,  (f x) <= (p (val x)).
+
+Theorem newHahnBanach : exists g : {scalar V},
+  (forall x,  g x <= p x) /\ (forall x, F x -> g (val x) = f x).
+pose graphF v r :=  r = f v.
+have graphFP: spec [set: F] f (fun z => p (val z)) graphF. split => //=.
+ - by move=> v r1 r2  [->] [ ->]. 
+ - by move=> v1 v2 l r1 r2; rewrite /graphF => -> -> ;rewrite !linearE. 
+   by  move=> v r [->].
+(*   
+have [z zmax]:= zorn_rel_ex graphFP.
+(*   z : zorn_type (fun x : V => F x) f p
+  zmax : forall z0 : zorn_type (fun x : V => F x) f p, zorn_rel z z0 -> z0 = z
+*)
+pose FP v : Prop := F v.
+have FP0 : FP 0 by [].
+have [g gP]:= hb_witness Choice_prop linfF FP0 p_cvx sup inf zmax.
+have scalg : linear_for *%R g.
+  case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP.
+  have addg : additive g.
+     move=> w1 w2;  apply/gP.
+     apply: linrel_add.
+     exact ls1.
+     by apply /gP.
+     by apply /gP.
+  suff scalg : scalable_for  *%R g.
+    move=> a u v.
+    rewrite -gP.
+    rewrite (addrC _ v).
+    rewrite (addrC _ (g v)).
+    apply: ls1.
+    by apply /gP.
+    by apply /gP.
+  by move=> w l; apply/gP; apply: linrel_scale=> //; apply/gP.
+pose H := GRing.isLinear.Build _ _ _ _ g scalg.
+pose g' : {linear V -> R | *%R} := HB.pack g H.
+exists g'.
+have grxtf v : F v -> g v = f v.
+  move=> Fv; apply/gP; case: z {zmax gP} => [c [_ _ _ pf]] /=; exact: pf.
+  suff pmajg v :  g v <= p v by split.
+    by  case: z {zmax} gP => [c [_ _ bp _]] /= gP; apply/bp/gP.
+Qed.
+ *)
+Admitted.
+End HahnBanachnew.
+
+
+Section HBGeom.
+Variable (R : realType) (V : normedModType R) (F : pred V) (f : V -> R) (F0 : F 0).
+
+Hypothesis linF : forall (v1 v2 : V) (l : R), F v1 -> F v2 -> F (v1 + l *: v2).
+Hypothesis linfF : forall v1 v2 l, F v1 -> F v2 -> f (v1 + l *: v2) = f v1 + l * (f v2).
+
+Hypothesis (Choice_prop : ((forall T U  (Q : T -> U -> Prop),
+                      (forall t : T, exists u : U,  Q t u) -> (exists e, forall t,  Q t (e t))))).
+
+(*Looked a long time for within *)
+Definition continuousR_on ( G : set V ) (g : V -> R) :=
+  {within G, continuous g}.
+(*  (forall x, (g @ (within G (nbhs x))) --> g x).*)
+
+(*Do we need to have F x ?*)
+Definition continuousR_on_at (G : set V ) (x : V ) (g : V -> R)  :=
+  g @ (within G (nbhs x)) --> (g x).
+
+Lemma continuousR_scalar_on_bounded :
+  (continuousR_on_at F 0 f) ->
+  (exists  r , (r > 0 ) /\ (forall x : V, F x ->   (`|f x| ) <=  `|x| * r)).
+Proof.
+  rewrite /continuousR_on_at.
+  move  => /cvg_ballP  H.
+  have H':  (0 < 1) by [].
+  have : \forall x \near within (fun x : V => F x) (nbhs 0), ball (f 0) 1 (f x).
+  apply: H. by [].
+  have f0 : f 0 = 0.
+     suff -> : f 0 = f (0 + (-1)*: 0) by rewrite linfF // mulNr mul1r addrN.
+     by rewrite scaleNr scaler0 addrN.
+  rewrite /( _ @ _ ) //= nearE /(within _ ) f0 //=. rewrite near_simpl.
+  rewrite -nbhs_nearE => H0 {H} ; move : (nbhs_ex H0) => [tp H] {H0}.
+  (*pose t := tp%:num .  *)
+  exists (2*(tp%:num)^-1). split=> //.
+  move=> x. case:  (lem (x=0)).
+  - by move=> ->; rewrite f0 normr0 normr0 //= mul0r.
+  - move/eqP=> xneq0 Fx.
+  pose a : V := (`|x|^-1 * (tp%:num)/2 ) *: x.
+  have Btp : ball 0  (tp%:num) a.
+   apply : ball_sym ; rewrite -ball_normE /ball_ /=  subr0.
+   rewrite normrZ mulrC normrM.
+   rewrite !gtr0_norm //= ; last first.
+     rewrite  pmulr_lgt0 // ?invr_gt0 ?normr_gt0 //.
+   rewrite mulrC -mulrA -mulrA ltr_pdivrMl; last by rewrite normr_gt0.
+   rewrite mulrC -mulrA  gtr_pMl.
+   rewrite invf_lt1 //=.
+     by rewrite ltr1n.
+   by  rewrite pmulr_lgt0 // !normr_gt0.
+ have Fa : F a by rewrite -[a]add0r; apply: linF.
+ have :  `|f a| < 1.
+    by move: (H _ Btp Fa); rewrite /ball /ball_ //= sub0r normrN.
+  suff ->  : ( f a =  ( (`|x|^-1) * (tp%:num)/2 ) * ( f x)) .
+     rewrite normrM (gtr0_norm) //.
+     rewrite mulrC mulrC  -mulrA  -mulrA  ltr_pdivrMl //= ;
+       last by rewrite normr_gt0.
+     rewrite mulrC [(_*1)]mulrC mul1r.
+     rewrite -[X in _ * X < _ ]invf_div ltr_pdivrMr //=; apply: ltW.
+     by rewrite !mulr_gt0  ?normr_gt0  // ?invr_gt0 normr_gt0.
+ suff -> : a = 0+ (`|x|^-1 * tp%:num /2) *: x by rewrite linfF // f0 add0r.
+ by rewrite add0r.
+Qed.
+
+Lemma mymysup : forall (A : set R) (a m : R),
+     A a -> ubound A m ->
+     {s : R | ubound A s /\ forall u, ubound A u -> s <= u}.
+Proof.
+  move => A a m Aa majAm.
+  have [A0 Aub]: has_sup A. split; first by exists a.
+    by exists m => x; apply majAm.
+  exists (reals.sup A).
+split.
+  by apply: sup_upper_bound.
+  by move => x; apply: sup_le_ub.
+Qed.
+
+(*TODO: should be lb_le_inf: *)
+Lemma mymyinf : forall (A : set R) (a m : R),
+     A a ->  lbound A m ->
+     {s : R | lbound A s /\ forall u, lbound A u -> u <= s}.
+  move => A a m Aa minAm.
+  have [A0 Alb]: has_inf A. split; first by exists a.
+    by exists m => x; apply minAm.
+  exists (reals.inf A).
+  split.
+    exact: ge_inf.
+  by move => x; apply: lb_le_inf.
+Qed.
+
+Notation myHB :=
+  (HahnBanachold Choice_prop mymysup mymyinf F0 linF linfF).
+
+Theorem HB_geom_normed :
+  continuousR_on_at F 0 f ->
+  exists g: {scalar V}, (continuous (g : V -> R)) /\ (forall x, F x -> (g x = f x)).
+Proof.
+  move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}.
+  pose p:= fun x : V => `|x|*r.
+ have convp: convex_fun p.
+   move=> v1 v2 l m [lt0l lt0m] addlm1 //= ; rewrite !/( p _) !mulrA -mulrDl.
+   suff: `|l *: v1 + m *: v2|  <= (l * `|v1| + m * `|v2|).
+     move => h; apply : ler_pM; last by [].
+     by apply : normr_ge0.
+     by apply : ltW.
+       by [].
+   have labs : `|l| = l by apply/normr_idP.
+   have mabs: `|m| = m by apply/normr_idP.
+   rewrite -[in(_*_)]labs -[in(m*_)]mabs.
+   rewrite -!normrZ.
+   by apply : ler_normD.
+ have majfp : forall x, F x -> f x <= p x.
+   move => x Fx; rewrite /(p _) ; apply : le_trans ; last by [].
+   apply : le_trans.
+   apply : ler_norm.
+   by apply : (fxrx x Fx).
+ move: (myHB convp majfp) => [ g  [majgp  F_eqgf] ] {majfp}.
+ exists g;  split; last by [].
+  move=> x; rewrite /cvgP; apply: (continuousfor0_continuous).
+  apply: bounded_linear_continuous.
+  exists r.
+  split; first by rewrite realE; apply/orP; left; apply: ltW. (* r is Numreal ... *)
+  move => M m1; rewrite nbhs_ballP;  exists 1 => /=; first by [].
+  move => y; rewrite -ball_normE //= sub0r => y1.
+  rewrite ler_norml; apply/andP. split.
+  - rewrite lerNl  -linearN; apply: (le_trans (majgp (-y))).
+    by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW //=.
+  - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN.
+    apply: ler_pM; rewrite ?normr_ge0 ?ltW //=.
+Qed.
+
+
+End HBGeom.
+
+
+Section newHBGeom.
+
+  (* TODO: port to ctvsType, by porting lemmas on continuous bounded linear functions there *)
+
+Variable (R : realType) (V: normedModType R) (F : subLmodType V) (f : {linear F -> R}).
+
+(* One needs to define the topological structure on F as the one induced by V, and make it  a normedModtype, as was done for subLmodType *)
+
+Hypothesis (Choice_prop : ((forall T U  (Q : T -> U -> Prop),
+                      (forall t : T, exists u : U,  Q t u) -> (exists e, forall t,  Q t (e t))))).
+
+(*
+Lemma mymysup : forall (A : set R) (a m : R),
+     A a -> ubound A m ->
+     {s : R | ubound A s /\ forall u, ubound A u -> s <= u}.
+Proof.
+  move => A a m Aa majAm.
+  have [A0 Aub]: has_sup A. split; first by exists a.
+    by exists m => x; apply majAm.
+  exists (reals.sup A).
+split.
+  by apply: sup_upper_bound.
+  by move => x; apply: sup_le_ub.
+Qed.
+
+(*TODO: should be lb_le_inf: *)
+Lemma mymyinf : forall (A : set R) (a m : R),
+     A a ->  lbound A m ->
+     {s : R | lbound A s /\ forall u, lbound A u -> u <= s}.
+  move => A a m Aa minAm.
+  have [A0 Alb]: has_inf A. split; first by exists a.
+    by exists m => x; apply minAm.
+  exists (reals.inf A).
+  split.
+    exact: ge_inf.
+  by move => x; apply: lb_le_inf.
+Qed.
+
+
+Notation myHB :=
+  (HahnBanach (boolp.EM) Choice_prop mymysup mymyinf F0 linF linfF).
+ *)
+
+ Search "continuous" "subspace".  
+(* bounded_linear_continuous: forall [R : numFieldType] [V W : normedModType R] [f : {linear V -> W}], bounded_near f (nbhs (0 : V)) -> continuous f
+linear_bounded_continuous: forall [R : numFieldType] [V W : normedModType R] (f : {linear V -> W}), bounded_near f (nbhs 0) <-> continuous f
+continuous_linear_bounded: forall [R : numFieldType] [V W : normedModType R] (x : V) [f : {linear V -> W}], {for 0, continuous f} -> bounded_near f (nbhs x) *)
+
+ (*TODO : clean the topological structure on F. Define subctvs ? *)
+Theorem new_HB_geom_normed :
+  continuous (f : (@initial_topology (sub_type F) V val) -> R) -> 
+  exists g: {scalar V}, (continuous (g : V -> R)) /\ (forall (x : F), (g (val x) = f x)).
+Proof.
+  move /(_ 0) => /= H; rewrite /from_subspace /=.
+  have f0 : {for 0, continuous ( (f : (@initial_topology (sub_type F) V val) -> R))}.
+  admit.  
+  Check (continuous_linear_bounded).
+  (* TODO ; to apply this lemma, F needs to be given a normedmodtype structure *)
+ (*  move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}.
+  (* want :   r :
+  ltr0 : 0 < r
+  fxrx : forall x : V, F x -> `|f x| <= `|x| * r*)
+ pose p:= fun x : V => `|x|*r.
+ have convp: hahn_banach_theorem.convex p.
+   move=> v1 v2 l m [lt0l lt0m] addlm1 //= ; rewrite !/( p _) !mulrA -mulrDl.
+   suff: `|l *: v1 + m *: v2|  <= (l * `|v1| + m * `|v2|).
+     move => h; apply : ler_pM; last by [].
+     by apply : normr_ge0.
+     by apply : ltW.
+       by [].
+   have labs : `|l| = l by apply/normr_idP.
+   have mabs: `|m| = m by apply/normr_idP.
+   rewrite -[in(_*_)]labs -[in(m*_)]mabs.
+   rewrite -!normrZ.
+   by apply : ler_normD.
+ have majfp : forall x, F x -> f x <= p x.
+   move => x Fx; rewrite /(p _) ; apply : le_trans ; last by [].
+   apply : le_trans.
+   apply : ler_norm.
+   by apply : (fxrx x Fx).
+ move: (myHB convp majfp) => [ g  [majgp  F_eqgf] ] {majfp}.
+ exists g;  split; last by [].
+  move=> x; rewrite /cvgP; apply: (continuousfor0_continuous).
+  apply: bounded_linear_continuous.
+  exists r.
+  split; first by rewrite realE; apply/orP; left; apply: ltW. (* r is Numreal ... *)
+  move => M m1; rewrite nbhs_ballP;  exists 1 => /=; first by [].
+  move => y; rewrite -ball_normE //= sub0r => y1.
+  rewrite ler_norml; apply/andP. split.
+  - rewrite lerNl  -linearN; apply: (le_trans (majgp (-y))).
+    by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW //=.
+  - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN.
+    apply: ler_pM; rewrite ?normr_ge0 ?ltW //=.
+Qed.
+*)
+Admitted.  
+
+
+End newHBGeom.
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 8ebdee378..f638c820a 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -7,7 +7,7 @@ From mathcomp Require Import fieldext falgebra.
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets filter functions cardinality.
 From mathcomp Require Import set_interval interval_inference ereal reals.
-From mathcomp Require Import topology function_spaces real_interval.
+From mathcomp Require Import topology convex function_spaces real_interval.
 From mathcomp Require Import prodnormedzmodule tvs num_normedtype.
 From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule.
 
@@ -77,15 +77,15 @@ Local Open Scope ring_scope.
 
 (** Modules with a norm depending on a numDomain *)
 
-HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V
-    & PseudoMetricNormedZmod K V & Tvs K V := {
+HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule K V
+    & PseudoMetricNormedZmod K V & ConvexTvs K V := {
   normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |;
 }.
 
 #[short(type="normedModType")]
 HB.structure Definition NormedModule (K : numDomainType) :=
-  {T of PseudoMetricNormedZmod K T & Tvs K T
-   & PseudoMetricNormedZmod_Tvs_isNormedModule K T}.
+  {T of PseudoMetricNormedZmod K T & ConvexTvs K T
+   & PseudoMetricNormedZmod_ConvexTvs_isNormedModule K T}.
 
 HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldType) V
     & PseudoMetricNormedZmod K V & GRing.Lmodule K V := {
@@ -114,20 +114,26 @@ 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.
 
+Local Open Scope convex_scope.
+
 Lemma locally_convex :
-  exists2 B : set (set V), (forall b, b \in B -> convex b) & basis B.
-Proof.
-exists [set B | exists x r, B = ball x r].
-  move=> b; rewrite inE /= => [[x]] [r] -> z y l.
-  rewrite !inE -!ball_normE /= => zx yx l0; rewrite -subr_gt0 => l1.
-  have -> : x = l *: x + (1 - l) *: x by rewrite addrC scalerBl subrK scale1r.
-  rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first.
+  exists2 B : set (set (convex_lmodType V)), (forall b, b \in B -> convex b) & basis B.
+Proof.
+exists [set B | exists (x : convex_lmodType V) r, B = ball x r].
+  move=> b; rewrite inE => [[x]] [r] ->.
+  apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
+  have -> : x = x <| l |> x by rewrite convmm. (*TODO: this looks superfluous *)
+  rewrite /ball_/= inE/=.
+  rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType V) <| l |>
+                              (x - y : convex_lmodType V)); last first.
     by rewrite opprD addrACA -scalerBr -scalerBr.
-  rewrite (@le_lt_trans _ _ (`|l| * `|x - z| + `|1 - l| * `|x - y|))//.
+  rewrite (@le_lt_trans _ _ ((l%:num) * `|x - z| + l%:num.~ * `|x - y|))//.
+    rewrite -[in X in _ <= X + _](@ger0_norm _ l%:num)//.
+    rewrite -[in X in _ <= _ + X](@ger0_norm _ l%:num.~) ?subr_ge0//.
     by rewrite -!normrZ ler_normD.
-  rewrite (@lt_le_trans _ _ (`|l| * r + `|1 - l| * r ))//.
-    by rewrite ltr_leD// lter_pM2l// ?normrE ?gt_eqF// ltW.
-  by rewrite !gtr0_norm// -mulrDl addrC subrK mul1r.
+  rewrite (@lt_le_trans _ _ (l%:num * r + l%:num.~ * r ))//.
+    by rewrite ltr_leD// lter_pM2l// ?normrE ?gt_eqF ?ltW// subr_gt0.
+  by rewrite -mulrDl addrC subrK mul1r.
 split.
   move=> B [x] [r] ->.
   rewrite openE/= -ball_normE/= /interior => y /= bxy; rewrite -nbhs_ballE.
@@ -142,9 +148,9 @@ HB.instance Definition _ :=
   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 _ := Uniform_isConvexTvs.Build K V locally_convex.
 HB.instance Definition _ :=
-  PseudoMetricNormedZmod_Tvs_isNormedModule.Build K V normrZ.
+  PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build K V normrZ.
 
 HB.end.
 
@@ -154,7 +160,7 @@ Section standard_topology_normedMod.
 Variable R : numFieldType.
 
 HB.instance Definition _ :=
-  PseudoMetricNormedZmod_Tvs_isNormedModule.Build R R^o (@normrM _).
+  PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build R R^o (@normrM _).
 
 End standard_topology_normedMod.
 
@@ -1662,7 +1668,7 @@ Lemma 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_Tvs_isNormedModule.Build K (U * V)%type
+  PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build K (U * V)%type
   prod_norm_scale.
 
 End prod_NormedModule.
diff --git a/theories/tvs.v b/theories/tvs.v
index a22206fcd..c548c7dae 100644
--- a/theories/tvs.v
+++ b/theories/tvs.v
@@ -1,9 +1,11 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions cardinality.
-From mathcomp Require Import set_interval reals interval_inference.
-From mathcomp Require Import topology function_spaces.
+From mathcomp Require Import set_interval reals interval interval_inference.
+From mathcomp Require Import topology convex function_spaces.
 
 (**md**************************************************************************)
 (* # Topological vector spaces                                                *)
@@ -54,6 +56,7 @@ From mathcomp Require Import topology function_spaces.
 (******************************************************************************)
 
 Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -73,10 +76,6 @@ Local Open Scope ring_scope.
 (* 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 NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}.
-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 PreTopologicalNmodule :=
   {M of Topological M & GRing.Nmodule M}.
@@ -139,6 +138,10 @@ HB.instance Definition _ :=
 
 HB.end.
 
+(*HB.structure Definition UniformZmodule := {M of Uniform M & GRing.Zmodule M}.
+HB.structure Definition UniformLmodule (K : numDomainType) :=
+  {M of Uniform M & GRing.Lmodule K M}.*)
+
 Section TopologicalZmoduleTheory.
 Variables (M : topologicalZmodType).
 
@@ -277,6 +280,27 @@ End UniformZmoduleTheory.
 HB.structure Definition PreUniformLmodule (K : numDomainType) :=
   {M of Uniform M & GRing.Lmodule K M}.
 
+(** Due to a bug of HB.saturate, we need to define these instances
+right after the definition of the topological instances **)
+
+(* 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 NbhsLmodule (K : numDomainType) := *)
+(*   {M of Nbhs M & GRing.Lmodule K M}. *)
+
+(* HB.structure Definition TopologicalNmodule := *)
+(*   {M of Topological M & GRing.Nmodule M}. *)
+(* HB.structure Definition TopologicalZmodule := *)
+(*   {M of Topological M & GRing.Zmodule M}. *)
+
+(*#[short(type="topologicalLmodType")]
+HB.structure Definition TopologicalLmodule (K : numDomainType) :=
+  {M of Topological M & GRing.Lmodule K M}.*)
+
+(* HB.structure Definition UniformZmodule := {M of Uniform M & GRing.Zmodule M}. *)
+(* HB.structure Definition UniformLmodule (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) ;
@@ -317,19 +341,35 @@ HB.instance Definition _ :=
 
 HB.end.
 
-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.
+Local Open Scope convex_scope.
 
-HB.mixin Record Uniform_isTvs (R : numDomainType) E
+Definition convex (R : numDomainType) (M : lmodType R)
+    (A : set (convex_lmodType M))(* try to get rid of the convex_lmodType *) :=
+  forall x y lambda, x \in A -> y \in A -> x <| lambda |> y \in A.
+
+Lemma convexW (R : numDomainType) (M : lmodType R) (A : set (convex_lmodType M)) :
+  convex A <->
+  {in A &, forall x y (k : {i01 R}), 0 < k%:num -> k%:num < 1 -> x <| k |> y \in A}.
+Proof.
+split => [cA x y xA yA k k0 k1|cA x y l xA yA].
+  by have /(_ k) := cA _ _ _ xA yA.
+have [->|l0] := eqVneq l 0%:i01; first by rewrite conv0.
+have [->|l1] := eqVneq l 1%:i01; first by rewrite conv1.
+apply: cA => //.
+- by rewrite lt_neqAle eq_sym l0 ge0.
+- by rewrite lt_neqAle l1 le1.
+Qed.
+
+(*TODO : name it convexTvs*)
+HB.mixin Record Uniform_isConvexTvs (R : numDomainType) E
     & 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) :=
-  {E of Uniform_isTvs R E & Uniform E & TopologicalLmodule R E}.
+#[short(type="ctvsType")]
+HB.structure Definition ConvexTvs (R : numDomainType) :=
+  {E of Uniform_isConvexTvs R E & Uniform E & TopologicalLmodule R E}.
 
 Section properties_of_topologicalLmodule.
 Context (R : numDomainType) (E : preTopologicalLmodType R) (U : set E).
@@ -367,7 +407,7 @@ Unshelve. all: by end_near. Qed.
 
 End properties_of_topologicalLmodule.
 
-HB.factory Record PreTopologicalLmod_isTvs (R : numDomainType) E
+HB.factory Record TopologicalLmod_isConvexTvs (R : numDomainType) E
     & 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) ;
@@ -375,7 +415,7 @@ HB.factory Record PreTopologicalLmod_isTvs (R : numDomainType) E
     (forall b, b \in B -> convex b) & basis B
   }.
 
-HB.builders Context R E & PreTopologicalLmod_isTvs R E.
+HB.builders Context R E & TopologicalLmod_isConvexTvs R E.
 
 Definition entourage : set_system (E * E) :=
   fun P => exists (U : set E), nbhs (0 : E) U  /\
@@ -465,7 +505,7 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E
 HB.end.
 
 Section Tvs_numDomain.
-Context (R : numDomainType) (E : tvsType R) (U : set E).
+Context (R : numDomainType) (E : ctvsType R) (U : set E).
 
 Lemma nbhs0N : nbhs 0 U -> nbhs 0 (-%R @` U).
 Proof. exact/nbhs0N_subproof/scale_continuous. Qed.
@@ -480,7 +520,7 @@ End Tvs_numDomain.
 
 Section Tvs_numField.
 
-Lemma nbhs0Z (R : numFieldType) (E : tvsType R) (U : set E) (r : R) :
+Lemma nbhs0Z (R : numFieldType) (E : ctvsType R) (U : set E) (r : R) :
   r != 0 -> nbhs 0 U -> nbhs 0 ( *:%R r @` U ).
 Proof.
 move=> r0 U0; have /= := scale_continuous (r^-1, 0) U.
@@ -489,7 +529,7 @@ near=> x => //=; exists (r^-1 *: x); last by rewrite scalerA divff// scale1r.
 by apply: (BU (r^-1, x)); split => //=;[exact: nbhs_singleton|near: x].
 Unshelve. all: by end_near. Qed.
 
-Lemma nbhsZ  (R : numFieldType) (E : tvsType R) (U : set E) (r : R) (x :E) :
+Lemma nbhsZ  (R : numFieldType) (E : ctvsType R) (U : set E) (r : R) (x :E) :
   r != 0 -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U ).
 Proof.
 move=> r0 U0; have /= := scale_continuous ((r^-1, r *: x)) U.
@@ -515,8 +555,11 @@ Qed.
 
 Local Lemma standard_scale_continuous : continuous (fun z : R^o * R^o => z.1 *: z.2).
 Proof.
-(* NB: This lemma is proved once again in normedtype, in a shorter way with much more machinery *)
-(*     To be rewritten once normedtype is split and tvs can depend on these lemmas *)
+(* NB: This lemma is proved once again in normedtype, in a shorter way with
+  much more machinery *)
+(* NB2: make tvs.v depend on pseudometric_normed_Zmodule.v once PR#1544 is
+merged.  The two structures are independant and this will allow to use lemmas as
+cvgr_dist on more concrete specific instances of tvstype*)
 move=> [k x]; apply/cvg_ballP => e le0 /=.
 pose M : R := maxr (`|e| + 1) (maxr `|k| (`|x| + `|x| + 2^-1 + 1)).
 have M0l : 0 < `|e| + 1 by rewrite ltr_wpDl.
@@ -565,17 +608,24 @@ Local Lemma standard_locally_convex :
 Proof.
 (* NB(rei): almost the same code as in normedtype.v *)
 exists [set B | exists x r, B = ball x r].
-  move=> b; rewrite inE /= => [[x]] [r] -> z y l.
-  rewrite !inE /ball /= => zx yx l0; rewrite -subr_gt0 => l1.
-  have -> : x = l *: x + (1 - l) *: x by rewrite scalerBl addrC subrK scale1r.
-  rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first.
+  move=> b/= /[!inE]/= [[x]] [r] ->.
+  apply/convexW => z y; rewrite /ball/= !inE/= => zx yx l /[!inE]/= l0 l1.
+  (* conv lemma? *)
+  have -> : x = x <| l |> x by rewrite convmm. (*TODO: this looks superfluous *)
+  rewrite [X in `|X|](_ : _ = (x - z) <| l |> (x - y)); last first.
     by rewrite opprD addrACA -mulrBr -mulrBr.
-  rewrite (@le_lt_trans _ _ (`|l| * `|x - z| + `|1 - l| * `|x - y|))//.
-    by rewrite -!normrM ler_normD.
-  rewrite (@lt_le_trans _ _ (`|l| * r + `|1 - l| * r ))//.
-    by rewrite ltr_leD// -lter_pdivlMl ?mulKf// ?normrE ?gt_eqF// ltW.
-  suff-> : `|1 - l| = 1 - `|l| by rewrite -mulrDl addrC subrK mul1r.
-  by move: l0 l1 => /ltW/normr_idP -> /ltW/normr_idP ->.
+  rewrite (@le_lt_trans _ _ ((`|x - z| : R^o) <| l |> `|x - y|))//.
+    rewrite -[in X in _ <= X + _](@ger0_norm _ l%:num)//.
+    rewrite -[in X in _ <= _ + X](@ger0_norm _ l%:num.~) ?subr_ge0//.
+    rewrite [X in `|X| <= _](_ : _ = l%:num * (x - z) + l%:num.~ * (x - y))//.
+    rewrite -[X in _ <= X + _]normrM.
+    rewrite -[X in _ <= _ + X]normrM.
+    by rewrite ler_normD.
+  rewrite (@lt_le_trans _ _ ((r : R^o) <| l |> r))//.
+    rewrite ltr_leD//.
+      by rewrite ltr_pM2l// normr_gt0// gt_eqF.
+    by rewrite ler_wpM2l// ?subr_ge0// ltW.
+  by rewrite convmm.
 split.
   move=> B [x] [r] ->.
   rewrite openE/= /ball/= /interior => y /= bxy; rewrite -nbhs_ballE.
@@ -590,12 +640,13 @@ 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.
+HB.instance Definition _ := Uniform_isConvexTvs.Build R R^o
+  standard_locally_convex.
 
 End standard_topology.
 
 Section prod_Tvs.
-Context (K : numFieldType) (E F : tvsType K).
+Context (K : numFieldType) (E F : ctvsType K).
 
 Local Lemma prod_add_continuous : continuous (fun x : (E * F) * (E * F) => x.1 + x.2).
 Proof.
@@ -638,7 +689,7 @@ have : basis B.
   rewrite !nbhsE /=; split; first by exists a => //; split => //; exact: Beo.
   by exists b => //; split => // []; exact: Bfo.
 exists B => // => b; rewrite inE /= => [[]] bo [] be [] bf Bee [] Bff <-.
-move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2] l0 l1.
+move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2].
 by split; rewrite -inE; [apply: Bcb; rewrite ?inE|apply: Bcf; rewrite ?inE].
 Qed.
 
@@ -647,6 +698,473 @@ HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build
 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.
+  Uniform_isConvexTvs.Build K (E * F)%type prod_locally_convex.
 
 End prod_Tvs.
+
+
+HB.structure Definition LinearContinuous (K : numDomainType) (E : NbhsLmodule.type K)
+  (F : NbhsZmodule.type) (s : K -> F -> F) :=
+  {f of @GRing.Linear K E F s f &  @Continuous E F f }.
+
+(* https://github.com/math-comp/math-comp/issues/1536
+   we use GRing.Scale.law even though it is claimed to be internal *)
+HB.factory Structure isLinearContinuous (K : numDomainType) (E : NbhsLmodule.type K)
+  (F : NbhsZmodule.type) (s : GRing.Scale.law K F) (f : E -> F) := {
+    (* NB: why not (f : {linear E -> F | s} instead of linearP ? ) *)
+    linearP : linear_for s f ;
+    continuousP : continuous f
+  }.
+
+HB.builders Context K E F s f of @isLinearContinuous K E F s f.
+
+HB.instance Definition _ := GRing.isLinear.Build K E F s f linearP.
+HB.instance Definition _ := isContinuous.Build E F f continuousP.
+
+HB.end.
+
+Section lcfun_pred.
+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 ].
+Definition lcfun_key : pred_key lcfun. Proof. exact. Qed.
+Canonical lcfun_keyed := KeyedPred lcfun_key.
+
+End lcfun_pred.
+
+Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'"
+  (at level 0, U at level 98, V at level 99,
+   format "{ 'linear_continuous'  U  ->  V  |  s }").
+Reserved Notation "'{' 'linear_continuous' U '->' V '}'"
+  (at level 0, U at level 98, V at level 99,
+   format "{ 'linear_continuous'  U  ->  V }").
+Notation "{ 'linear_continuous' U -> V | s }" := (@LinearContinuous.type _ U%type V%type s)
+  : type_scope.
+Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type | *:%R}
+  : type_scope.
+  
+Section lcfun.
+Context {R : numDomainType} {E : NbhsLmodule.type R}
+  {F : NbhsZmodule.type} {s : GRing.Scale.law R F}.
+Notation T := {linear_continuous E -> F | s}.
+Notation lcfun := (@lcfun _ E F s).
+
+Section Sub.
+Context (f : E -> F) (fP : f \in lcfun).
+  
+Definition lcfun_Sub_subproof :=
+  @isLinearContinuous.Build _ E F s f (proj1 (set_mem fP)) (proj2 (set_mem fP)).
+#[local] HB.instance Definition _ := lcfun_Sub_subproof.
+Definition lcfun_Sub : {linear_continuous _  -> _ | _ } := f.
+End Sub.
+
+Lemma lcfun_rect (K : T -> Type) :
+  (forall f (Pf : f \in lcfun), K (lcfun_Sub Pf)) -> forall u : T, K u.
+Proof.
+move=> Ksub [f [[Pf1] [Pf2] [Pf3]]].
+set G := (G in K G).
+have Pf : f \in lcfun.
+  by rewrite inE /=; split => // x u v; rewrite Pf1 Pf2.
+suff -> : G = lcfun_Sub Pf by apply: Ksub.
+rewrite {}/G.
+congr LinearContinuous.Pack.
+congr LinearContinuous.Class.
+- by congr GRing.isNmodMorphism.Axioms_; apply: Prop_irrelevance.
+- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance.
+- by congr isContinuous.Axioms_; apply: Prop_irrelevance.
+Qed.
+
+Lemma lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _).
+Proof. by []. Qed.
+
+HB.instance Definition _ := isSub.Build _ _ T lcfun_rect lcfun_valP.
+
+Lemma lcfuneqP (f g : {linear_continuous E -> F | s}) : f = g <-> f =1 g.
+Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
+
+HB.instance Definition _ := [Choice of {linear_continuous E -> F | s} by <:].
+
+Variant lcfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
+  | Islcfun (l : {linear_continuous E -> F | s}) : lcfun_spec f l true.
+
+(*to be renamed ?*)
+Lemma lcfunE (f : E -> F) : (f \in lcfun) -> lcfun_spec f f (f \in lcfun).
+Proof.
+move=> /[dup] f_lc ->.
+have {2}-> :(f = (lcfun_Sub f_lc)) by rewrite lcfun_valP.
+constructor.
+Qed.
+
+End lcfun.
+Section lcfun_comp.
+
+Context {R : numDomainType} {E F : NbhsLmodule.type R}
+  {S : NbhsZmodule.type} {s : GRing.Scale.law R S}
+  (f : {linear_continuous E -> F}) (g : {linear_continuous F -> S | s}).
+
+Lemma lcfun_comp_subproof1 : linear_for s (g \o f). 
+Proof. by move=> *; move=> */=; rewrite !linearP. Qed.
+
+(* TODO weaken proof continuous_comp to arbitrary nbhsType *)
+Lemma lcfun_comp_subproof2 : continuous (g \o f). 
+Proof. by move=> x; move=> A /cts_fun /cts_fun. Qed.
+
+HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f)
+  lcfun_comp_subproof1 lcfun_comp_subproof2.
+
+(* TODO: do the identity? *)
+End lcfun_comp.
+
+Section lcfun_lmodtype.
+  Context {R : numFieldType} {E F G: ctvsType R}.
+    (* {s : GRing.Scale.law R F}. *)
+
+Implicit Types (r : R) (f g : {linear_continuous E -> F}) (h : {linear_continuous F -> G}).  
+
+Import GRing.Theory.
+
+Lemma null_fun_continuous : continuous (\0 : E -> F).
+Proof.
+by apply: cst_continuous.
+Qed.
+
+(*
+Lemma it_is_additive r : @Algebra.isNmodMorphism F F (s r).
+Proof.
+split.
+by apply: GRing.Scale.op_nmod_morphism.
+Qed.
+
+Fail Check (s 0 : {additive F -> F}).
+
+HB.instance Definition _ r := it_is_additive r.
+
+Check (s 0 : {additive F -> F}).
+
+Lemma null_fun_is_linear: linear_for s (\0 : E -> F).
+Proof.
+move => r x y /=.
+by rewrite raddf0 addr0.
+Qed.
+*)
+
+HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous.
+
+Lemma lcfun0 : (\0 : {linear_continuous E -> F}) =1 cst 0 :> (_ -> _). Proof. by []. Qed.
+
+(* NB TODO: move section cvg_composition_pseudometric in normedtype.v here, to
+generalize it on tvstype *)
+(* Next lemmas are duplicates  - do it more properly with appropriate conte*)
+(* TODO once PR1544 is merged *)
+
+Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} f g a b :
+  f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b.
+Proof.
+move=> fa ga.
+apply: continuous2_cvg; [|by []..].
+apply @add_continuous. (* TODO: c'est louche d'avoir besoin du @ *)
+Qed.
+
+Lemma lcfun_continuousD f g : continuous (f \+ g).
+Proof. by move=> /= x; apply: lcfun_cvgD; apply: cts_fun. Qed.
+
+Lemma lcfun_continuousN f : continuous (\- f).
+Proof.
+Admitted.
+
+HB.instance Definition _ f g := isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g).
+
+Lemma lcfun_cvgZ  (U : set_system E) {FF : Filter U} l f r a : l @ U  --> r -> f @ U --> a ->
+                     l x *: f x @[x --> U] --> r *: a.
+Proof.
+move=> ? ?; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)).
+Qed.
+
+Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k f a : f @ U --> a -> k \*: f @ U --> k *: a.
+Proof. apply: lcfun_cvgZ => //; exact: cvg_cst. Qed.
+
+Lemma lcfun_continuousM r g : continuous (r \*: g).
+Proof. by move=> /= x; apply: lcfun_cvgZr; apply: cts_fun. Qed.
+
+HB.instance Definition _ r g := isContinuous.Build E F (r \*: g)  (@lcfun_continuousM r g).
+
+Lemma lcfun_submod_closed  : submod_closed (@lcfun R E F *:%R).
+Proof.
+(*  split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous.
+  move=> r /= _ _  /lcfunE[f] /lcfunE[g].
+(*  rewrite !inE /= =>  [[lf cf] [lg cg]]; split.*)
+  (* HB pack et subst *) (* move => l u v. apply/linearP.*)
+  rewrite inE /=; split. 
+  Fail apply: (@GRing.add_fun_is_semi_additive E F ( s r f) g).
+  Fail apply: add_fun_is_linear.
+  move => l a b.
+  rewrite /= ?raddf0 ?addr0// !raddfD /=.
+  Fail rewrite (@raddfD _ _  (r \*: f \+ g) (l *: a) b).
+  rewrite addrCA -!addrA addrCA /=. Check linearZ_LR. Check (@linearZ_LR R E F _ ((r \*: f + g)) l a).
+  Fail rewrite -[s]/(GRing.scale).
+  Unset Printing Notations.
+  admit.
+  apply: continuousD.*)
+split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous.
+move=> r /= _ _  /lcfunE[f] /lcfunE[g].
+by rewrite inE /=; split; [exact: linearP | exact: lcfun_continuousD].
+Qed.
+
+(*HB.instance Definition _ f := isContinuous.Build E F (\- f)  (@continuousB f).*)
+
+Lemma add_fun_is_linear f g : linear (f \+ g).
+Proof.
+Admitted.
+
+HB.instance Definition _ f := isContinuous.Build E F (\- f) (@lcfun_continuousN f).
+
+(* Context (f g : {linear_continuous E -> F}) (r : R). *)
+(* Check (r \*: f \+ g : {linear_continuous E -> F}). *)
+
+HB.instance Definition _ :=
+  @GRing.isSubmodClosed.Build _  _ lcfun lcfun_submod_closed.
+
+HB.instance Definition _ :=
+  [SubChoice_isSubLmodule of {linear_continuous E -> F } by <:].
+
+Check ({linear_continuous E -> F} : lmodType R).
+End lcfun_lmodtype.
+
+(* make use of  {family fam, U -> V}  *)
+
+Section test.
+
+Import GRing.
+Context {F : numFieldType}.
+Check (F : Nbhs.type).
+Check (F : Zmodule.type).
+(*HB.saturate F.*)  (*numFieldType. *) (*hypothese : on a créé les
+instances de nbhs et zmodtype sur F : numFieldType avant de créer le
+join entre les deux structures *)
+Check (F : NbhsZmodule.type).
+
+(* Section ring. *)
+(* Import GRing. *)
+(* Context {R : numDomainType} {E : NbhsLmodule.type R} *)
+(*   {F : numFieldType} {s : GRing.Scale.law R F}. *)
+
+(* HB.instance Definition _ := NbhsZmodule.on F.  *)
+
+(* Lemma lcfun_submod_closed : submod_closed (@lcfun R E F s). *)
+(* Proof. *)
+(* split=> [|f g|f g]; rewrite !inE/=. *)
+(* - exact: measurable_cst. *)
+(* - exact: measurable_funB. *)
+(* - exact: measurable_funM. *)
+(* Qed. *)
+(* HB.instance Definition _ := GRing.isSubringClosed.Build _ *)
+(*   (@lcfun d default_measure_display E F) lcfun_subring_closed. *)
+(* HB.instance Definition _ := [SubChoice_isSubComRing of {linear_continuous E -> F | s} by <:]. *)
+
+(* Implicit Types (f g : {linear_continuous E -> F | s}). *)
+
+(* Lemma lcfun0 : (0 : {linear_continuous E -> F | s}) =1 cst 0 :> (_ -> _). Proof. by []. Qed. *)
+(* Lemma lcfun1 : (1 : {linear_continuous E -> F | s}) =1 cst 1 :> (_ -> _). Proof. by []. Qed. *)
+(* Lemma lcfunN f : - f = \- f :> (_ -> _). Proof. by []. Qed. *)
+(* Lemma lcfunD f g : f + g = f \+ g :> (_ -> _). Proof. by []. Qed. *)
+(* Lemma lcfunB f g : f - g = f \- g :> (_ -> _). Proof. by []. Qed. *)
+(* Lemma lcfunM f g : f * g = f \* g :> (_ -> _). Proof. by []. Qed. *)
+(* Lemma lcfun_sum I r (P : {pred I}) (f : I -> {linear_continuous E -> F | s}) (x : E) : *)
+(*   (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. *)
+(* Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. *)
+(* Lemma lcfun_prod I r (P : {pred I}) (f : I -> {linear_continuous E -> F | s}) (x : E) : *)
+(*   (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. *)
+(* Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. *)
+(* Lemma lcfunX f n : f ^+ n = (fun x => f x ^+ n) :> (_ -> _). *)
+(* Proof. by apply/funext=> x; elim: n => [|n IHn]//; rewrite !exprS lcfunM/= IHn. Qed. *)
+
+(* HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). *)
+(* HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). *)
+(* HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). *)
+(* HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). *)
+
+(* Definition mindic (D : set E) of measurable D : E -> F := \1_D. *)
+
+(* Lemma mindicE (D : set E) (mD : measurable D) : *)
+(*   mindic mD = (fun x => (x \in D)%:R). *)
+(* Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. *)
+
+(* HB.instance Definition _ D mD := @isMeasurableFun.Build _ _ E F (mindic mD) *)
+(*   (@measurable_fun_indic _ E F setT D mD). *)
+
+(* Definition indic_lcfun (D : set E) (mD : measurable D) := *)
+(*   [the {linear_continuous E -> F | s} of mindic mD]. *)
+
+(* HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k). *)
+(* Definition scale_lcfun k f := [the {linear_continuous E -> F | s} of k \o* f]. *)
+
+(* Lemma max_lcfun_subproof f g : @isMeasurableFun d _ E F (f \max g). *)
+(* Proof. by split; apply: measurable_maxr. Qed. *)
+
+(* HB.instance Definition _ f g := max_lcfun_subproof f g. *)
+
+(* Definition max_lcfun f g := [the {lcfun E >-> _} of f \max g]. *)
+
+(* End ring. *)
+
+End test.
+
+(* TODO : define bornology and topology of uniform convergence, show it's a
+tvstype *)
+(* Not used in the following *)
+
+(* (*why with typeclasses and not with HB ? *) *)
+
+(*What follows is adapted from {family fam, U -> V} in
+function_space.v. Should we copy instances from family fam to family_lcfun fam ? *)
+ Definition uniform_lcfun_family R {E : ctvsType R} (F : ctvsType R)  (fam : set E -> Prop) : Type := 
+   {linear_continuous E -> F}.
+
+(* Reserved Notation "'{' 'family_lcfun' fam , U '->' V '|' s '}'" *)
+(*   (at level 0, U at level 98, V at level 99, *)
+(*    format "{ 'family_lcfun' fam ,  U  ->  V  |  s }"). *)
+Reserved Notation "'{' 'family_lcfun' fam , U '->' V '}'"
+  (at level 0, U at level 98, V at level 99,
+    format "{ 'family_lcfun'  fam ,  U  ->  V }").
+(* Reserved Notation "'{' 'family_lcfun' fam ,  F '-->' f '|' s '}'" *)
+(*   (at level 0, F at level 98, f at level 99, *)
+(*     format  "{ 'family_lcfun' fam , F --> f | s }"). *)
+Reserved Notation "'{' 'family_lcfun' fam ,  F '-->' f  '}'"
+  (at level 0, F at level 98, f at level 99,
+   format  "{ 'family_lcfun' fam ,  F  -->  f }").
+(* Notation "{ 'family_lcfun' fam , U -> V '|' s }" :=  (@uniform_lcfun_family _ U V s fam). *)
+Notation "{ 'family_lcfun' fam , U -> V }" :=  (@uniform_lcfun_family _ U V fam).
+(* Notation "{ 'family_lcfun' fam , F --> f '|' s }" := *)
+(*   (cvg_to F (@nbhs _ {family_lcfun fam , _ -> _ | _ } f)) : type_scope. *)
+
+Notation "{ 'family_lcfun' fam , F --> f }" :=
+  (cvg_to F (@nbhs _ {family_lcfun fam,  _ -> _ } f)) : type_scope.
+
+(* we can´t use unfiorm, it is defined on E -> F and not on our space. We need to define it on {linear_continuous E -> F} , inducing its topology from uniform` E- > F *)
+
+
+(*md
+Define bounded 
+TODO generalize bounded_fun_norm in sequence.v
+Define bornology and bounded function -  prove continuous -> bounded
+Generalize bounded_near in normedtype.v
+Define uniform convergence on bornology
+Prove continuous embedding into topologies already defined on spaces of functions.
+
+Pour E_{sigma} : utiliser des tags, ie des identité annotées
+ *)
+
+
+Reserved Notation "'{' 'linear_continuous_' B , U '->' V '}'"
+  (at level 0, U at level 98, V at level 99,
+    format "{ 'linear_continuous_' B ,  U  ->  V }").
+Reserved Notation "'{' 'linear_continuous_' B , F '-->' f '}'"
+  (at level 0, F at level 98, f at level 99,
+    format "{ 'linear_continuous_'  B  ,  F  -->  f }").
+
+
+Definition bounded  (R : numFieldType) (E : ctvsType R) (b : set E) := forall (V : set E), (nbhs 0 V -> exists r, b `<=` ((fun x => r *: x )@` V)).
+
+Notation "{ 'linear_continuous_'  fam , U -> V }" :=  (@uniform_lcfun_family _ U V fam).
+Notation "{ 'linear_continuous_'  fam , F --> f }" :=
+  (cvg_to F (@nbhs _ {linear_continuous_ fam,  _ -> _ } f)) : type_scope.
+
+Definition nbhs_lineartopology  (R : numFieldType) (E : ctvsType R) (F : ctvsType R) b U :=
+  [set f : {linear_continuous E -> F}| f @` b `<=` U ]. 
+
+
+HB.mixin Record isBornology  (R : numFieldType) (E : ctvsType R) (B : set_system E) := {
+  bornoC : forall x, exists b,  (B b) /\ (b x) ;
+  bornoS : forall P Q : set E, P `<=` Q -> B Q -> B P;
+  bornoI : forall P Q : set E, B P -> B Q -> B (P `&` Q); (*wikipedia*)
+    (* bornoZ : forall r : R, forall  Q : set E, B Q -> exists P, (B P /\ (((fun x => r *: x )@`Q `<=`  P))) (*why ??*) In Jarchow*)
+  }.
+
+#[short(type="bornologyType")]
+  HB.structure Definition Bornology R E := {B of @isBornology R E B}.
+
+(*
+Pointed Type on linear_continuous, filteredtype, nbhsType, topologicaltype
+
+ *)
+
+(* Reco Cyril: copier / généraliser les defs de function_space.v, puis montrer que la prebase c ést nbhs_lineartopology. Compliqué parce que 
+Notation "{ 'uniform`' A -> V }" := (@uniform_fun _ A V) : type_scope.
+ne se généralise pas facilement en 
+Notation "{ 'linear_continuous` `' A -> V }" := (linear_continuous A ->  V) : type_scope.
+
+(* HB.instance Definition _ {R} {U V : tvsType R}  (fam : set U -> Prop) := *)
+(*   Uniform.copy {family_lcfun fam, U -> V} (sup_topology (fun k : sigT fam => *)
+(*   Uniform.class {uniform` projT1 k -> V})). *)
+
+(* HB.factory Record UniformLinCont_isTvs (R : numDomainType) (E : tvsType R) (F : tvsType R) (B : set_system  E) of Topological {family_lcfun B , E -> F} & GRing.Lmodule {linear_continuous E -> F }  := { *)
+(*   bornoC : forall x : E, exists b : set E,  (B b) /\ (b x) ; *)
+(*   bornoU : forall P Q  : set E, B P -> B Q -> B (P `|` Q) ; *)
+(*   bornoS : forall P Q : set E, P `<=` Q -> B Q -> B  P *)
+(*   }. *)
+
+(* HB.builders Context R E F B of UniformLinCont_isTvs R E F B. *)
+
+
+
+
+(*First lemmas to formalize : 
+- Prop 1 in 2.10 Jarchow  (* W is a 0-basis for a linear topology 3~aonG iff 38 consists ofG-bounded
+sets only. In that case, if F is Hausdorff and 38 covers X, then J~a is Hausdorf *)
+- Prop 2 in 8.4 Jarchow 
+
+Then define notations and prove compatibility with function_spaces.v notations*)
+
+
+(** examples **)
+(* HB.instance Definition _ (U : Type) (T : U -> topologicalType) := *)
+(*   Topological.copy (forall x : U, T x) (prod_topology T). *)
+
+(* HB.instance Definition _ (U : Type) (T : U -> uniformType) := *)
+(*   Uniform.copy (forall x : U, T x) (prod_topology T). *)
+
+(* HB.instance Definition _ (U T : topologicalType) := *)
+(*   Topological.copy  *)
+(*     (continuousType U T)  *)
+(*     (weak_topology (id : continuousType U T -> (U -> T))). *)
+
+(* HB.instance Definition _ (U : topologicalType) (T : uniformType) := *)
+(*   Uniform.copy  *)
+(*     (continuousType U T)  *)
+(*     (weak_topology (id : continuousType U T -> (U -> T))). *)
+
+(* HB.instance Definition _  R {E : tvsType R} (F : tvsType R)  (fam : set E -> Prop) := *)
+(*   Topological.copy {family_lcfun fam, E -> F} (sup_topology (fun k : sigT fam => *)
+(*        Uniform.class {uniform` projT1 k -> F})). *)
+
+(* HB.instance Definition _ {R} {U V : tvsType R}  (fam : set U -> Prop) := *)
+(*   Uniform.copy {family_lcfun fam, U -> V} (sup_topology (fun k : sigT fam => *)
+(*   Uniform.class {uniform` projT1 k -> V})). *)
+
+(* HB.factory Record UniformLinCont_isTvs (R : numDomainType) (E : tvsType R) (F : tvsType R) (B : set_system  E) of Topological {family_lcfun B , E -> F} & GRing.Lmodule {linear_continuous E -> F }  := { *)
+(*   bornoC : forall x : E, exists b : set E,  (B b) /\ (b x) ; *)
+(*   bornoU : forall P Q  : set E, B P -> B Q -> B (P `|` Q) ; *)
+(*   bornoS : forall P Q : set E, P `<=` Q -> B Q -> B  P *)
+(*   }. *)
+
+(* HB.builders Context R E F B of UniformLinCont_isTvs R E F B. *)
+
+
+(* HB.instance Definition _ := TopologicalLmod_isTvs {linearcontinuous E -> F} *)
+(*     entourage_filter entourage_refl *)
+(*     entourage_inv entourage_split_ex *)
+(*     nbhsE. *)
+(* HB.end. *)
+
+
+Section dual.
+Context {R : numDomainType} {E : ctvsType R}.
+
+(* Reserved Notation " E ''' " (at level 80, format "E ''' "). *)
+
+Notation " E ''' ":= {linear_continuous E -> R^o} (at level 80). 
+
+Check (E)'.
+Notation " E ''' ":= {linear_continuous E -> R^o} (at level 80). 
+
+End dual.
+*)