From 248858dc4f51fbdadb861c8dd4930b93f8c942ea Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 11 Mar 2026 13:50:27 +0900
Subject: [PATCH 1/7] generalization

Co-authored-by: Marie Kerjean <marie.kerjean@cnrs.fr>
---
 theories/normedtype_theory/pseudometric_normed_Zmodule.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 687d6f3f6..8cfbf80bf 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -11,7 +11,7 @@ From mathcomp Require Import prodnormedzmodule num_normedtype.
 (*                                                                            *)
 (* This directory (`normed_theory`) file extends the topological hierarchy    *)
 (* with norm-related notions. Note that balls in `topology_theory` are not    *)
-(* necessarily open, here they are.                                           *)
+(* necessarily ope, here they are.                                           *)
 (*                                                                            *)
 (* ## Helper functions                                                        *)
 (* To be used in `normed_module.v`.                                           *)

From e0b189548429136f7fa5dceb0d8a25fd8e1f535b Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 11 Mar 2026 13:54:28 +0900
Subject: [PATCH 2/7] fix

---
 theories/normedtype_theory/pseudometric_normed_Zmodule.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 8cfbf80bf..687d6f3f6 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -11,7 +11,7 @@ From mathcomp Require Import prodnormedzmodule num_normedtype.
 (*                                                                            *)
 (* This directory (`normed_theory`) file extends the topological hierarchy    *)
 (* with norm-related notions. Note that balls in `topology_theory` are not    *)
-(* necessarily ope, here they are.                                           *)
+(* necessarily open, here they are.                                           *)
 (*                                                                            *)
 (* ## Helper functions                                                        *)
 (* To be used in `normed_module.v`.                                           *)

From fc8aa73fa69cd35828e8742372e20c1d92274a1f Mon Sep 17 00:00:00 2001
From: mkerjean <marie.kerjean@lipn.univ-paris13.fr>
Date: Fri, 6 Mar 2026 12:24:49 +0900
Subject: [PATCH 3/7] convex_function generalized

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
---
 CHANGELOG_UNRELEASED.md | 3 +++
 theories/convex.v       | 5 +++--
 theories/hoelder.v      | 7 ++++---
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 42aa1376b..ceef7032c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -241,6 +241,7 @@
   + lemma `cvg_comp_shift`
   + lemma `ball_open_nbhs`
 
+  
 ### Renamed
 
 - in `topology_structure.v`
@@ -291,6 +292,8 @@
 
 - in `exp.v`:
   + lemma `derivable_powR`
+- in `convex.v`:
+  + definition `convex_function` (from a realType as domain to a convex_lmodType as domain)
 
 ### Deprecated
 
diff --git a/theories/convex.v b/theories/convex.v
index 66a143d7e..c050e7834 100644
--- a/theories/convex.v
+++ b/theories/convex.v
@@ -220,7 +220,8 @@ Proof. by move=> ab; rewrite in_itv/= -lerN2 convN convC !conv_le ?lerN2. Qed.
 
 End conv_numDomainType.
 
-Definition convex_function (R : realType) (D : set R) (f : R -> R^o) :=
+
+Definition convex_function (R : numFieldType) (E : lmodType R) (E' := convex_lmodType E) (D : set E') (f : E' -> R^o) :=
   forall (t : {i01 R}),
-    {in D &, forall (x y : R^o), (f (x <| t |> y) <= f x <| t |> f y)%R}.
+    {in D &, forall (x y : E'), (f (x <| t |> y) <= f x <| t |> f y)%R}.
 (* TODO: generalize to convTypes once we have ordered convTypes (mathcomp 2) *)
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 096f55960..16cfdc741 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -532,13 +532,14 @@ End hoelder2.
 Section convex_powR.
 Context {R : realType}.
 Local Open Scope ring_scope.
+Local Open Scope convex_scope.
 
 Lemma convex_powR p : 1 <= p ->
-  convex_function `[0, +oo[%classic (@powR R ^~ p).
+  convex_function (`[0, +oo[%classic : set R) (@powR R ^~ p).
 Proof.
 move=> p1 t x y /[!inE] /= /[!in_itv] /= /[!andbT] x_ge0 y_ge0.
-have p0 : 0 < p by rewrite (lt_le_trans _ p1).
-rewrite !convRE; set w1 := t%:num; set w2 := t%:inum.~.
+have p0 : 0 < p by rewrite (lt_le_trans _ p1).  
+rewrite convRE [X in X `^ _ <= _]convRE; set w1 := t%:num; set w2 := t%:inum.~.
 have [->|w20] := eqVneq w2 0.
   rewrite !mul0r !addr0; have [->|w10] := eqVneq w1 0.
     by rewrite !mul0r powR0// gt_eqF.

From b64c7c1c5e1aa1e0c7e6d4a56a965d3c4ac818f9 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 6 Mar 2026 14:10:06 +0900
Subject: [PATCH 4/7] mv convex

---
 CHANGELOG_UNRELEASED.md                    |  4 ++
 theories/convex.v                          | 16 ++++++++
 theories/normedtype_theory/normed_module.v | 30 +++++++++------
 theories/normedtype_theory/tvs.v           | 44 +++++++++++++---------
 4 files changed, 65 insertions(+), 29 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index ceef7032c..695085675 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -83,6 +83,8 @@
 
 - in `separation_axioms.v`:
   + lemmas `limit_point_closed`
+- in `convex.v`:
+  + lemma `convexW`
 
 ### Changed
 
@@ -241,6 +243,8 @@
   + lemma `cvg_comp_shift`
   + lemma `ball_open_nbhs`
 
+- moved from `tvs.v` to `convex.v`
+  + definition `convex`
   
 ### Renamed
 
diff --git a/theories/convex.v b/theories/convex.v
index c050e7834..d44cadc1c 100644
--- a/theories/convex.v
+++ b/theories/convex.v
@@ -220,6 +220,22 @@ Proof. by move=> ab; rewrite in_itv/= -lerN2 convN convC !conv_le ?lerN2. Qed.
 
 End conv_numDomainType.
 
+Definition convex (R : numDomainType) (M : lmodType R)
+    (A : set (convex_lmodType M)) :=
+  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.
 
 Definition convex_function (R : numFieldType) (E : lmodType R) (E' := convex_lmodType E) (D : set E') (f : E' -> R^o) :=
   forall (t : {i01 R}),
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 9ccf4583a..e6bb58265 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -7,7 +7,7 @@ From mathcomp Require Import interval_inference fieldext falgebra.
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets filter functions cardinality.
 From mathcomp Require Import set_interval ereal reals topology real_interval.
-From mathcomp Require Import prodnormedzmodule tvs num_normedtype.
+From mathcomp Require Import convex prodnormedzmodule tvs num_normedtype.
 From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule.
 
 (**md**************************************************************************)
@@ -111,21 +111,27 @@ 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.
+
 (** NB: we have almost the same proof in `tvs.v` *)
 Let 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; first by move=> B [x] [r] ->; exact: ball_open.
 move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
 by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index c67224749..c96daf9db 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -2,8 +2,10 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector.
 From mathcomp Require Import interval_inference.
+#[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 topology num_normedtype.
+From mathcomp Require Import convex set_interval reals topology num_normedtype.
 From mathcomp Require Import pseudometric_normed_Zmodule.
 
 (**md**************************************************************************)
@@ -306,10 +308,6 @@ 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.
-
 HB.mixin Record Uniform_isTvs (R : numDomainType) E
     & Uniform E & GRing.Lmodule R E := {
   locally_convex : exists2 B : set (set E),
@@ -511,20 +509,30 @@ 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.
+
 Let standard_locally_convex :
   exists2 B : set (set R^o), (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.
-    by rewrite opprD addrACA -scalerBr -scalerBr.
-  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_pM2l// ?normrE ?gt_eqF// ltW.
-  by rewrite !gtr0_norm// -mulrDl addrC subrK mul1r.
+  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 _ _ ((`|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; first by move=> B [x] [r] ->; exact: ball_open.
 move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
 by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
@@ -582,8 +590,10 @@ 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.
-by split; rewrite -inE; [apply: Bcb; rewrite ?inE|apply: Bcf; rewrite ?inE].
+move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2].
+split.
+  by apply/set_mem/Bcb; [exact/mem_set|exact/mem_set|exact/mem_set].
+by apply/set_mem/Bcf; [exact/mem_set|exact/mem_set|exact/mem_set].
 Qed.
 
 HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build

From 50761e5ae5476f7a5e3792a06a3ed410d6ff7cfa Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 11 Mar 2026 13:16:20 +0900
Subject: [PATCH 5/7] simplification

---
 theories/normedtype_theory/normed_module.v | 27 +++++++++---------
 theories/normedtype_theory/tvs.v           | 33 +++++++++-------------
 2 files changed, 27 insertions(+), 33 deletions(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index e6bb58265..9e69097fa 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -113,25 +113,24 @@ Unshelve. all: by end_near. Qed.
 
 Local Open Scope convex_scope.
 
+Let ball_convex (x : convex_lmodType V) (r : K) : convex (ball x r).
+Proof.
+apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
+rewrite inE/=.
+rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |>
+                            (x - y : convex_lmodType _)); last first.
+  by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr.
+rewrite (le_lt_trans (ler_normD _ _))// !normrZ.
+rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//.
+by rewrite -[ltRHS]mul1r -(add_onemK l%:num) mulrDl ltrD// ltr_pM2l// onem_gt0.
+Qed.
+
 (** NB: we have almost the same proof in `tvs.v` *)
 Let locally_convex :
   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%: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%:num * r + l%:num.~ * r ))//.
-    by rewrite ltr_leD// lter_pM2l// ?normrE ?gt_eqF ?ltW// subr_gt0.
-  by rewrite -mulrDl addrC subrK mul1r.
+  by move=> b; rewrite inE => [[x]] [r] ->; exact: ball_convex.
 split; first by move=> B [x] [r] ->; exact: ball_open.
 move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
 by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index c96daf9db..2a1800050 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -511,31 +511,26 @@ Unshelve. all: by end_near. Qed.
 
 Local Open Scope convex_scope.
 
+Let standard_ball_convex (x : R^o) (r : R) : convex (ball x r).
+Proof.
+apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
+rewrite inE/=.
+rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |>
+                            (x - y : convex_lmodType _)); last first.
+  by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr.
+rewrite (le_lt_trans (ler_normD _ _))// !normrM.
+rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//.
+by rewrite -[ltRHS]mul1r -(add_onemK l%:num) mulrDl ltrD// ltr_pM2l// onem_gt0.
+Qed.
+
 Let standard_locally_convex :
   exists2 B : set (set R^o), (forall b, b \in B -> convex b) & basis B.
 Proof.
 exists [set B | exists x r, B = ball x r].
-  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 _ _ ((`|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.
+  by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex.
 split; first by move=> B [x] [r] ->; exact: ball_open.
 move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
-by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
+by exists (ball x r) => //=; split; [exists x, r|exact: ballxx].
 Qed.
 
 HB.instance Definition _ :=

From c3dff45460bc0cc9c88ef16dd9fa8724c2a465ca Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 11 Mar 2026 16:34:44 +0900
Subject: [PATCH 6/7] fix CI

---
 theories/normedtype_theory/normed_module.v | 3 ++-
 theories/normedtype_theory/tvs.v           | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 9e69097fa..3e1e925e9 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -122,7 +122,8 @@ rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |>
   by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr.
 rewrite (le_lt_trans (ler_normD _ _))// !normrZ.
 rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//.
-by rewrite -[ltRHS]mul1r -(add_onemK l%:num) mulrDl ltrD// ltr_pM2l// onem_gt0.
+rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl.
+by rewrite ltrD// ltr_pM2l// onem_gt0.
 Qed.
 
 (** NB: we have almost the same proof in `tvs.v` *)
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 2a1800050..8fbd1dd55 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -520,7 +520,8 @@ rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |>
   by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr.
 rewrite (le_lt_trans (ler_normD _ _))// !normrM.
 rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//.
-by rewrite -[ltRHS]mul1r -(add_onemK l%:num) mulrDl ltrD// ltr_pM2l// onem_gt0.
+rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl.
+by rewrite ltrD// ltr_pM2l// onem_gt0.
 Qed.
 
 Let standard_locally_convex :

From 9b67ad500c5e35a860de657782d6786a25af9fdc Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 12 Mar 2026 14:09:23 +0900
Subject: [PATCH 7/7] convex -> convex_set

---
 CHANGELOG_UNRELEASED.md                    |  4 +--
 theories/convex.v                          | 13 ++++++----
 theories/normedtype_theory/normed_module.v | 13 +++++-----
 theories/normedtype_theory/tvs.v           | 29 ++++++++++++----------
 4 files changed, 33 insertions(+), 26 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 695085675..81d9ba29a 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -84,7 +84,7 @@
 - in `separation_axioms.v`:
   + lemmas `limit_point_closed`
 - in `convex.v`:
-  + lemma `convexW`
+  + lemma `convex_setW`
 
 ### Changed
 
@@ -244,7 +244,7 @@
   + lemma `ball_open_nbhs`
 
 - moved from `tvs.v` to `convex.v`
-  + definition `convex`
+  + definition `convex`, renamed to `convex_set`
   
 ### Renamed
 
diff --git a/theories/convex.v b/theories/convex.v
index d44cadc1c..125e66cf4 100644
--- a/theories/convex.v
+++ b/theories/convex.v
@@ -220,13 +220,15 @@ Proof. by move=> ab; rewrite in_itv/= -lerN2 convN convC !conv_le ?lerN2. Qed.
 
 End conv_numDomainType.
 
-Definition convex (R : numDomainType) (M : lmodType R)
+Definition convex_set (R : numDomainType) (M : lmodType R)
     (A : set (convex_lmodType M)) :=
   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}.
+Lemma convex_setW (R : numDomainType) (M : lmodType R)
+    (A : set (convex_lmodType M)) :
+  convex_set 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.
@@ -237,7 +239,8 @@ apply: cA => //.
 - by rewrite lt_neqAle l1 le1.
 Qed.
 
-Definition convex_function (R : numFieldType) (E : lmodType R) (E' := convex_lmodType E) (D : set E') (f : E' -> R^o) :=
+Definition convex_function (R : numFieldType) (E : lmodType R)
+    (E' := convex_lmodType E) (D : set E') (f : E' -> R^o) :=
   forall (t : {i01 R}),
     {in D &, forall (x y : E'), (f (x <| t |> y) <= f x <| t |> f y)%R}.
 (* TODO: generalize to convTypes once we have ordered convTypes (mathcomp 2) *)
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 3e1e925e9..bcc6e52fd 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -113,9 +113,9 @@ Unshelve. all: by end_near. Qed.
 
 Local Open Scope convex_scope.
 
-Let ball_convex (x : convex_lmodType V) (r : K) : convex (ball x r).
+Let ball_convex_set (x : convex_lmodType V) (r : K) : convex_set (ball x r).
 Proof.
-apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
+apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
 rewrite inE/=.
 rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |>
                             (x - y : convex_lmodType _)); last first.
@@ -127,11 +127,12 @@ by rewrite ltrD// ltr_pM2l// onem_gt0.
 Qed.
 
 (** NB: we have almost the same proof in `tvs.v` *)
-Let locally_convex :
-  exists2 B : set (set (convex_lmodType V)), (forall b, b \in B -> convex b) & basis B.
+Let locally_convex_set :
+  exists2 B : set_system (convex_lmodType V),
+    (forall b, b \in B -> convex_set b) & basis B.
 Proof.
 exists [set B | exists (x : convex_lmodType V) r, B = ball x r].
-  by move=> b; rewrite inE => [[x]] [r] ->; exact: ball_convex.
+  by move=> b; rewrite inE => [[x]] [r] ->; exact: ball_convex_set.
 split; first by move=> B [x] [r] ->; exact: ball_open.
 move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
 by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
@@ -141,7 +142,7 @@ 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_isTvs.Build K V locally_convex_set.
 HB.instance Definition _ :=
   PseudoMetricNormedZmod_Tvs_isNormedModule.Build K V normrZ.
 
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 8fbd1dd55..26748b40f 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -310,8 +310,8 @@ HB.end.
 
 HB.mixin Record Uniform_isTvs (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
+  locally_convex : exists2 B : set_system E,
+    (forall b, b \in B -> convex_set b) & basis B
 }.
 
 #[short(type="tvsType")]
@@ -358,8 +358,8 @@ HB.factory Record PreTopologicalLmod_isTvs (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) ;
-  locally_convex : exists2 B : set (set E),
-    (forall b, b \in B -> convex b) & basis B
+  locally_convex : exists2 B : set_system E,
+    (forall b, b \in B -> convex_set b) & basis B
   }.
 
 HB.builders Context R E & PreTopologicalLmod_isTvs R E.
@@ -511,9 +511,9 @@ Unshelve. all: by end_near. Qed.
 
 Local Open Scope convex_scope.
 
-Let standard_ball_convex (x : R^o) (r : R) : convex (ball x r).
+Let standard_ball_convex_set (x : R^o) (r : R) : convex_set (ball x r).
 Proof.
-apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
+apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
 rewrite inE/=.
 rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |>
                             (x - y : convex_lmodType _)); last first.
@@ -524,11 +524,11 @@ rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl.
 by rewrite ltrD// ltr_pM2l// onem_gt0.
 Qed.
 
-Let standard_locally_convex :
-  exists2 B : set (set R^o), (forall b, b \in B -> convex b) & basis B.
+Let standard_locally_convex_set :
+  exists2 B : set_system R^o, (forall b, b \in B -> convex_set b) & basis B.
 Proof.
 exists [set B | exists x r, B = ball x r].
-  by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex.
+  by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex_set.
 split; first by move=> B [x] [r] ->; exact: ball_open.
 move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
 by exists (ball x r) => //=; split; [exists x, r|exact: ballxx].
@@ -538,14 +538,16 @@ 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_isTvs.Build R R^o standard_locally_convex_set.
 
 End standard_topology.
 
 Section prod_Tvs.
 Context (K : numFieldType) (E F : tvsType K).
 
-Local Lemma prod_add_continuous : continuous (fun x : (E * F) * (E * F) => x.1 + x.2).
+Local Lemma prod_add_continuous :
+  continuous (fun x : (E * F) * (E * F) => x.1 + x.2).
 Proof.
 move => [/= xy1 xy2] /= U /= [] [A B] /= [nA nB] nU.
 have [/= A0 [A01 A02] nA1] := @add_continuous E (xy1.1, xy2.1) _ nA.
@@ -556,7 +558,8 @@ move => [[x1 y1][x2 y2]] /= [] [] a1 b1 [] a2 b2.
 by apply: nU; split; [exact: (nA1 (x1, x2))|exact: (nB1 (y1, y2))].
 Qed.
 
-Local Lemma prod_scale_continuous : continuous (fun z : K^o * (E * F) => z.1 *: z.2).
+Local Lemma prod_scale_continuous :
+  continuous (fun z : K^o * (E * F) => z.1 *: z.2).
 Proof.
 move => [/= r [x y]] /= U /= []/= [A B] /= [nA nB] nU.
 have [/= A0 [A01 A02] nA1] := @scale_continuous K E (r, x) _ nA.
@@ -568,7 +571,7 @@ by move=> [l [e f]] /= [] [Al Bl] [] Ae Be; apply: nU; split;
 Qed.
 
 Local Lemma prod_locally_convex :
-  exists2 B : set (set (E * F)), (forall b, b \in B -> convex b) & basis B.
+  exists2 B : set_system (E * F), (forall b, b \in B -> convex_set b) & basis B.
 Proof.
 have [Be Bcb Beb] := @locally_convex K E.
 have [Bf Bcf Bfb] := @locally_convex K F.