Hahn banach 2026

.nix/config.nix

@@ -42,36 +42,45 @@ in {
 
   ## select an entry to build in the following `bundles` set
   ## defaults to "default"
-  default-bundle = "9.1";
+  default-bundle = "9.1-master";
 
   ## write one `bundles.name` attribute set per
   ## alternative configuration
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
 
-  bundles."9.0-2.5.0" = {
+  bundles."9.0-master" = {
     rocqPackages = {
       rocq-core.override.version = "9.0";
-      mathcomp.override.version = "2.5.0";
+      mathcomp.override.version = "master";
+      mathcomp-bigenough.override.version = "master";
+      mathcomp-finmap.override.version = "master";
+      micromega-plugin.override.version = "master";
     };
     coqPackages = common-bundle // {
       coq.override.version = "9.0";
-      mathcomp.override.version = "2.5.0";
+      ssprove.job = false;  # not yet available for 9.1
     };
   };
 
-  bundles."9.0" = {
-    rocqPackages = {
-      rocq-core.override.version = "9.0";
-    };
-    coqPackages = common-bundle // {
-      coq.override.version = "9.0";
-    };
-  };
+  # bundles."9.1-2.5.0" = {
+  #   rocqPackages = {
+  #     rocq-core.override.version = "9.1";
+  #     mathcomp.override.version = "2.5.0";
+  #   };
+  #   coqPackages = common-bundle // {
+  #     coq.override.version = "9.1";
+  #     ssprove.job = false;  # not yet available for 9.1
+  #   };
+  # };
 
-  bundles."9.1" = {
+  bundles."9.1-master" = {
     rocqPackages = {
       rocq-core.override.version = "9.1";
+      mathcomp.override.version = "master";
+      mathcomp-bigenough.override.version = "master";
+      mathcomp-finmap.override.version = "master";
+      micromega-plugin.override.version = "master";
     };
     coqPackages = common-bundle // {
       coq.override.version = "9.1";
@@ -90,6 +99,7 @@ in {
       mathcomp.override.version = "master";
       mathcomp-bigenough.override.version = "master";
       mathcomp-finmap.override.version = "master";
+      micromega-plugin.override.version = "master";
     };
     coqPackages = common-bundle // {
       coq.override.version = "master";

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"175e68be5dcde92457dbb949ef905e771d765a68"
+"6b32b8cd491ec44b75da86fb17e4353f2f102328"

CHANGELOG_UNRELEASED.md

@@ -95,6 +95,38 @@
 
 - in `reals.v`:
   + lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn`
+- in `mathcomp_extra.v`:
+  + lemmas `divDl_ge0`, `divDl_le1`
+
+- 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`
 
 ### Changed
 
@@ -126,9 +158,14 @@
 
 - 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`,

_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,5 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
-From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect_compat finmap all_algebra.
 
 (**md**************************************************************************)
 (* # MathComp extra                                                           *)
@@ -93,10 +94,21 @@ 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.

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,8 @@ 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