adding seminorms to tvs

adding also initial fam topology, gauge functions, and subbase 0basis

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

Co-authored-by: Cyril Cohen <cyril.cohen@inria.fr>

Author: mkerjean

CHANGELOG_UNRELEASED.md

@@ -93,12 +93,6 @@
   + lemma `is_diff_mx`
   + instance `is_diff_mx`
 
-### Changed
-
-- moved from `measurable_structure.v` to `classical_sets.v`:
-  + definition `preimage_set_system`
-  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
-    `preimage_set_system_id`
 - in `functions.v`:
   + lemmas `linfunP`, `linfun_eqP`
   + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }`
@@ -123,13 +117,55 @@
 
 - new files `signed_measure.v` and `radon_nikodym.v`
   + with the contents of `charge.v` (deprecated)
-  
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:
   + definition `preimage_set_system`
   + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
     `preimage_set_system_id`
+  
+- moved from `measurable_structure.v` to `classical_sets.v`:
+  + definition `preimage_set_system`
+  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
+    `preimage_set_system_id`
+- in `functions.v`:
+  + lemmas `linfunP`, `linfun_eqP`
+  + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }`
+
+- in `tvs.v`:
+  + structure `LinearContinuous`
+  + factory `isLinearContinuous`
+  + instance of `ChoiceType` on `{linear_continuous _ -> _ }`
+  + instance of `LinearContinuous` with the composition of two functions of type `LinearContinuous`
+  + instance of `LinearContinuous` with the sum of two functions of type `LinearContinuous`
+  + instance of `LinearContinuous` with the scalar multiplication of a function of type
+    `LinearContinuous`
+  + instance of `Continuous` on \-f when f is of type `LinearContinuous`
+  + instance of `SubModClosed` on `{linear_continuous _ -> _}`
+  + instance of `SubLModule` on  `{linear_continuous _ -> _ }`
+  + instance of `LinearContinuous` on the null function
+  + notations `{linear_continuous _ -> _ | _ }` and `{linear_continuous _ -> _ }`
+  + definitions `lcfun`, `lcfun_key, `lcfunP`
+  + lemmas `lcfun_eqP`, `null_fun_continuous`, `fun_cvgD`,
+   `fun_cvgN`, `fun_cvgZ`, `fun_cvgZr`
+  + lemmas `lcfun_continuous` and `lcfun_linear`
+  
+  + ...
+- in `derive.v`:
+  + lemmas `derivable_max`, `derive_maxl`, `derive_maxr` `derivable_min`, `derive_minl`, `derive_minr`
+  + lemmas `derivable0`, `derive0`, `is_derive0`
+- in `topology_structure.v`:
+  + lemma `not_limit_pointE`
+
+- in `separation_axioms.v`:
+  + lemmas `limit_point_closed`
+- in `convex.v`:
+  + lemma `convex_setW`
+- in `convex.v`:
+  + lemma `convexW`
+
+### Changed
 
 - moved from `topology_structure.v` to `filter.v`:
   + lemma `continuous_comp` (and generalized)
@@ -183,6 +219,31 @@
     `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`,
     `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule`
 
+- in set_interval.v
+  + `setUitv1`, `setU1itv`, `setDitv1l`, `setDitv1r` (generalized)
+- in `mathcomp_extra.v`:
+  + lemmas `divDl_ge0`, `divDl_le1`
+  + mixin `Zmodule_isSubNormed`
+  + structure `SubNormedZmodule`, notation `subNormedZmodType`
+
+- in `unstable.v`:
+  + lemmas `divD_onem`
+  
+### Changed
+
+- moved from `measurable_structure.v` to `classical_sets.v`:
+  + definition `preimage_set_system`
+  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
+    `preimage_set_system_id`
+
+- moved from `topology_structure.v` to `filter.v`:
+  + lemma `continuous_comp` (and generalized)
+
+- in `numfun.v`:
+  + `fune_abse` renamed to `funeposDneg` and direction of the equality changed
+  + `funeposneg` renamed to `funeposBneg` and direction of the equality changed
+  + `funeD_posD` renamed to `funeDB` and direction of the equality changed
+
 ### Renamed
 
 - in `tvs.v`:

CHANGELOG_UNRELEASED_new.md

@@ -0,0 +1,52 @@
+# Changelog (unreleased)
+
+## [Unreleased]
+
+### Added
+
+- in `mathcomp_extra.v`:
+  + lemmas `divDl_ge0`, `divDl_le1`
+  + mixin `Zmodule_isSubNormed`
+  + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge)
+
+- in `unstable.v`:
+  + lemmas `divD_onem`
+
+- in `filter.v`:
+  + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType`
+
+- in `topology_structure.v`:
+  + structure `SubTopological`, notation `subTopologicalType`
+
+- in `tvs.v`:
+  + structure `SubConvexTvs`, notation `subConvexTvsType`
+
+- in `normed_module.v`:
+  + structure `SubNormedModule`, notation `subNormedModType`
+  + instance `ent_xsection_filter`
+  + factory `SubLmodule_isSubNormedmodule`
+
+- new file `hahn_banach_theorem.v`:
+  + module `LinearGraph`
+    * definitions `graph`, `linear_graph`
+    * lemmas `lingraph_00`, `lingraphZ`, `lingraphD`
+  + module `HahnBanachZorn`
+    * definitions `extend_graph`, `le_graph`, `functional_graph`, `le_extend_graph`
+    * record `zorn_type`
+    * definition `zphi`
+    * lemma `zorn_type_eq`
+    * definition `zornS`
+    * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness`
+  + theorems `hahn_banach_extension`, `hahn_banach_extension_normed`
+
+### Deprecated
+
+### Renamed
+
+### Generalized
+
+### Removed
+
+
+
+

_CoqProject

@@ -88,6 +88,8 @@ theories/normedtype_theory/urysohn.v
 theories/normedtype_theory/vitali_lemma.v
 theories/normedtype_theory/normedtype.v
 
+theories/functional_analysis/hahn_banach_theorem.v
+
 theories/sequences.v
 theories/realfun.v
 theories/exp.v

classical/filter.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
 From mathcomp Require Import boolp classical_sets functions wochoice.
@@ -15,21 +15,31 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
 (*                                                                            *)
 (* ## Structure of filter                                                     *)
 (* ```                                                                        *)
-(*                   filteredType U == interface type for types whose         *)
-(*                                     elements represent sets of sets on U   *)
-(*                                     These sets are intended to be filters  *)
-(*                                     on U but this is not enforced yet.     *)
-(*                                     The HB class is called Filtered.       *)
-(*                                     It extends Pointed.                    *)
-(*                           nbhs p == set of sets associated to p (in a      *)
-(*                                     filtered type)                         *)
-(*                  pfilteredType U == a pointed and filtered type            *)
-(*                          hasNbhs == factory for filteredType               *)
+(*              filteredType U == interface type for types whose elements     *)
+(*                                represent sets of sets on U                 *)
+(*                                These sets are intended to be filters on U  *)
+(*                                but this is not enforced yet.               *)
+(*                                The HB class is called Filtered.            *)
+(*                                It extends Pointed.                         *)
+(*                      nbhs p == set of sets associated to p (in a filtered  *)
+(*                                type)                                       *)
+(*             pfilteredType U == a pointed and filtered type                 *)
+(*                     hasNbhs == factory for filteredType                    *)
+(*                    nbhsType == type of a structure that has a set system   *)
+(*                                of neighborhoods associated to each point   *)
+(*                   pnbhsType == same has nbhsType for pointed types         *)
 (*                     continuous f == f is continuous w.r.t the topology     *)
-(*                 filterI_iter F n == nth stage of recursively building the  *)
-(*                                     filter of finite intersections of F    *)
-(*                    finI_from D f == set of \bigcap_(i in E) f i where E is *)
-(*                                     a finite subset of D                   *)
+(*             isSubNbhs V S U == interface that states the continuity of val *)
+(*                                for U which has a subChoiceType and a       *)
+(*                                nbhsType                                    *)
+(*             subNbhsType V S == structure that extends a                    *)
+(*                                subChoiceType/nbhsType with the isSubNbhs   *)
+(*                                interface                                   *)
+(*                                The HB class is SubNbhs.                    *)
+(*            filterI_iter F n == nth stage of recursively building the       *)
+(*                                filter of finite intersections of F         *)
+(*               finI_from D f == set of \bigcap_(i in E) f i where E is a    *)
+(*                                a finite subset of D                        *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* We endow several standard types with the structure of filter, e.g.:        *)
@@ -951,6 +961,15 @@ Lemma continuous_comp (R S T : nbhsType) (f : R -> S) (g : S -> T) x :
   {for x, continuous (g \o f)}.
 Proof. exact: cvg_comp. Qed.
 
+HB.mixin Record isSubNbhs
+  (V : nbhsType) (S : pred V) U & SubChoice V S U & Nbhs U := {
+  continuous_valE : continuous (val : U -> V)
+}.
+
+#[short(type="subNbhsType")]
+HB.structure Definition SubNbhs (V : nbhsType) (S : pred V) :=
+  { U of SubChoice V S U & Nbhs U & isSubNbhs V S U}.
+
 Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) :
     {for x, continuous f} ->
   (\forall y \near f x, P y) -> (\near x, P (f x)).

classical/mathcomp_extra.v

@@ -1,4 +1,5 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.
 
 (**md**************************************************************************)
@@ -93,10 +94,41 @@ Proof. by case: C => //= /ltW. Qed.
 (* MathComp 2.6 additions *)
 (**************************)
 
-(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
 Lemma intrD1 {R : pzRingType} (i : int) : (i + 1)%:~R = i%:~R + 1 :> R.
 Proof. by rewrite intrD. Qed.
 
-(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
 Lemma intr1D {R : pzRingType} (i : int) : (1 + i)%:~R = 1 + i%:~R :> R.
 Proof. by rewrite intrD. Qed.
+
+Lemma divDl_ge0 (R : numDomainType) (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) :
+  0 <= s / (s + t).
+Proof.
+by apply: divr_ge0 => //; apply: addr_ge0.
+Qed.
+
+Lemma divDl_le1 (R : numFieldType) (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) :
+  s / (s + t) <= 1.
+Proof.
+move: s0; rewrite le0r => /predU1P [->|s0]; first by rewrite mul0r.
+by rewrite ler_pdivrMr ?mul1r ?lerDl // ltr_wpDr.
+Qed.
+
+HB.mixin Record Zmodule_isSubNormed (R : numDomainType)
+    (M : normedZmodType R) (S : pred M) T & SubChoice M S T
+    & Num.NormedZmodule R T := {
+  norm_valE : forall x , @Num.norm _ M ((val : T -> M) x) = @Num.norm _ T x
+}.
+
+(* SubNormedZmodule will appear in MC 2.6.0.
+   However, just duplicating it here causes an HB error in the CI with MC 2.6.0.
+   We therefore reproduce it with a different name and add a dummy
+   mixin to it to satisfy HB.
+   This will be removed when dropping support for MC 2.5.0 *)
+HB.mixin Record isTmp (R : numDomainType) (V : normedZmodType R) (S : pred V)
+    (U : Type) := { field_tmp : True }.
+
+#[short(type="subNormedZmodType")]
+HB.structure Definition SubNormedZmodule_tmp (R : numDomainType)
+    (V : normedZmodType R) (S : pred V) :=
+  { U of @isTmp R V S U & SubChoice V S U & Num.NormedZmodule R U &
+    GRing.SubZmodule V S U & Zmodule_isSubNormed R V S U }.

classical/unstable.v

@@ -369,6 +369,13 @@ Qed.
 Lemma onemV (F : numFieldType) (x : F) : x != 0 -> x^-1.~ = (x - 1) / x.
 Proof. by move=> ?; rewrite mulrDl divff// mulN1r. Qed.
 
+Lemma divD_onem (R : realFieldType) (s t : R) (s0 : 0 < s) (t0 : 0 < t) :
+  (s / (s + t)).~ = t / (s + t).
+Proof.
+rewrite /onem.
+by rewrite -(@divff _ (s + t)) ?gt_eqF ?addr_gt0// -mulrBl (addrC s) addrK.
+Qed.
+
 Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N.
 Proof. by case: a => //= n _; case: b. Qed.
 

theories/Make

@@ -55,6 +55,9 @@ normedtype_theory/urysohn.v
 normedtype_theory/vitali_lemma.v
 normedtype_theory/normedtype.v
 
+functional_analysis/hahn_banach_theorem.v
+
+
 realfun.v
 sequences.v
 exp.v