Skip to content

Commit e302943

Browse files
mkerjeanaffeldt-aistCohenCyrilamahboubi
authored and
adjevahi
committed
Hahn banach 2026 (math-comp#1889)
* Hahn-Banach theorem * definition of sub normed module * subConvexTvsType --------- Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp> Co-authored-by: Cyril Cohen <cyril.cohen@inria.fr> Co-authored-by: Assia Mahboubi <Assia.Mahboubi@inria.fr>
1 parent a6bd58c commit e302943

16 files changed

Lines changed: 1256 additions & 1010 deletions

File tree

.github/workflows/nix-action-9.0-2.5.0.yml renamed to .github/workflows/nix-action-9.0-master.yml

Lines changed: 218 additions & 116 deletions
Large diffs are not rendered by default.

.github/workflows/nix-action-9.0.yml renamed to .github/workflows/nix-action-9.1-master.yml

Lines changed: 329 additions & 160 deletions
Large diffs are not rendered by default.

‎.github/workflows/nix-action-9.1.yml‎

Lines changed: 0 additions & 696 deletions
This file was deleted.

‎.nix/config.nix‎

Lines changed: 23 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -42,36 +42,45 @@ in {
4242

4343
## select an entry to build in the following `bundles` set
4444
## defaults to "default"
45-
default-bundle = "9.1";
45+
default-bundle = "9.1-master";
4646

4747
## write one `bundles.name` attribute set per
4848
## alternative configuration
4949
## When generating GitHub Action CI, one workflow file
5050
## will be created per bundle
5151

52-
bundles."9.0-2.5.0" = {
52+
bundles."9.0-master" = {
5353
rocqPackages = {
5454
rocq-core.override.version = "9.0";
55-
mathcomp.override.version = "2.5.0";
55+
mathcomp.override.version = "master";
56+
mathcomp-bigenough.override.version = "master";
57+
mathcomp-finmap.override.version = "master";
58+
micromega-plugin.override.version = "master";
5659
};
5760
coqPackages = common-bundle // {
5861
coq.override.version = "9.0";
59-
mathcomp.override.version = "2.5.0";
62+
ssprove.job = false; # not yet available for 9.1
6063
};
6164
};
6265

63-
bundles."9.0" = {
64-
rocqPackages = {
65-
rocq-core.override.version = "9.0";
66-
};
67-
coqPackages = common-bundle // {
68-
coq.override.version = "9.0";
69-
};
70-
};
66+
# bundles."9.1-2.5.0" = {
67+
# rocqPackages = {
68+
# rocq-core.override.version = "9.1";
69+
# mathcomp.override.version = "2.5.0";
70+
# };
71+
# coqPackages = common-bundle // {
72+
# coq.override.version = "9.1";
73+
# ssprove.job = false; # not yet available for 9.1
74+
# };
75+
# };
7176

72-
bundles."9.1" = {
77+
bundles."9.1-master" = {
7378
rocqPackages = {
7479
rocq-core.override.version = "9.1";
80+
mathcomp.override.version = "master";
81+
mathcomp-bigenough.override.version = "master";
82+
mathcomp-finmap.override.version = "master";
83+
micromega-plugin.override.version = "master";
7584
};
7685
coqPackages = common-bundle // {
7786
coq.override.version = "9.1";
@@ -85,11 +94,11 @@ in {
8594
stdlib.override.version = "master";
8695
rocq-elpi.override.version = "master";
8796
hierarchy-builder.override.version = "master";
88-
micromega-plugin.override.version = "master";
8997
micromega-plugin.job = false;
9098
mathcomp.override.version = "master";
9199
mathcomp-bigenough.override.version = "master";
92100
mathcomp-finmap.override.version = "master";
101+
micromega-plugin.override.version = "master";
93102
};
94103
coqPackages = common-bundle // {
95104
coq.override.version = "master";

‎.nix/coq-nix-toolbox.nix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"175e68be5dcde92457dbb949ef905e771d765a68"
1+
"6b32b8cd491ec44b75da86fb17e4353f2f102328"

‎CHANGELOG_UNRELEASED.md‎

Lines changed: 38 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,38 @@
103103

104104
- in `reals.v`:
105105
+ lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn`
106+
- in `mathcomp_extra.v`:
107+
+ lemmas `divDl_ge0`, `divDl_le1`
108+
109+
- in `unstable.v`:
110+
+ lemmas `divD_onem`
111+
112+
- in `filter.v`:
113+
+ mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType`
114+
115+
- in `topology_structure.v`:
116+
+ structure `SubTopological`, notation `subTopologicalType`
117+
118+
- in `tvs.v`:
119+
+ structure `SubConvexTvs`, notation `subConvexTvsType`
120+
121+
- in `normed_module.v`:
122+
+ structure `SubNormedModule`, notation `subNormedModType`
123+
+ instance `ent_xsection_filter`
124+
+ light-weigth factory `subLmodule_isSubNormedmodule`
125+
126+
- new file `hahn_banach_theorem.v`:
127+
+ module `LinearGraph`
128+
* definitions `graph`, `linear_graph`
129+
* lemmas `lingraph_00`, `lingraphZ`, `lingraphD`
130+
+ module `HahnBanachZorn`
131+
* definitions `extend_graph`, `le_graph`, `functional_graph`, `le_extend_graph`
132+
* record `zorn_type`
133+
* definition `zphi`
134+
* lemma `zorn_type_eq`
135+
* definition `zornS`
136+
* lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness`
137+
+ theorems `hahn_banach_extension`, `hahn_banach_extension_normed`
106138

107139
### Changed
108140

@@ -134,9 +166,14 @@
134166

135167
- new files `signed_measure.v` and `radon_nikodym.v`
136168
+ with the contents of `charge.v` (deprecated)
137-
169+
138170
### Changed
139171

172+
- moved from `measurable_structure.v` to `classical_sets.v`:
173+
+ definition `preimage_set_system`
174+
+ lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
175+
`preimage_set_system_id`
176+
140177
- moved from `measurable_structure.v` to `classical_sets.v`:
141178
+ definition `preimage_set_system`
142179
+ lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,

‎_CoqProject‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -88,6 +88,8 @@ theories/normedtype_theory/urysohn.v
8888
theories/normedtype_theory/vitali_lemma.v
8989
theories/normedtype_theory/normedtype.v
9090

91+
theories/functional_analysis/hahn_banach_theorem.v
92+
9193
theories/sequences.v
9294
theories/realfun.v
9395
theories/exp.v

‎classical/filter.v‎

Lines changed: 34 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
1+
(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *)
22
From HB Require Import structures.
33
From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
44
From mathcomp Require Import boolp classical_sets functions wochoice.
@@ -15,21 +15,31 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
1515
(* *)
1616
(* ## Structure of filter *)
1717
(* ``` *)
18-
(* filteredType U == interface type for types whose *)
19-
(* elements represent sets of sets on U *)
20-
(* These sets are intended to be filters *)
21-
(* on U but this is not enforced yet. *)
22-
(* The HB class is called Filtered. *)
23-
(* It extends Pointed. *)
24-
(* nbhs p == set of sets associated to p (in a *)
25-
(* filtered type) *)
26-
(* pfilteredType U == a pointed and filtered type *)
27-
(* hasNbhs == factory for filteredType *)
18+
(* filteredType U == interface type for types whose elements *)
19+
(* represent sets of sets on U *)
20+
(* These sets are intended to be filters on U *)
21+
(* but this is not enforced yet. *)
22+
(* The HB class is called Filtered. *)
23+
(* It extends Pointed. *)
24+
(* nbhs p == set of sets associated to p (in a filtered *)
25+
(* type) *)
26+
(* pfilteredType U == a pointed and filtered type *)
27+
(* hasNbhs == factory for filteredType *)
28+
(* nbhsType == type of a structure that has a set system *)
29+
(* of neighborhoods associated to each point *)
30+
(* pnbhsType == same has nbhsType for pointed types *)
2831
(* continuous f == f is continuous w.r.t the topology *)
29-
(* filterI_iter F n == nth stage of recursively building the *)
30-
(* filter of finite intersections of F *)
31-
(* finI_from D f == set of \bigcap_(i in E) f i where E is *)
32-
(* a finite subset of D *)
32+
(* isSubNbhs V S U == interface that states the continuity of val *)
33+
(* for U which has a subChoiceType and a *)
34+
(* nbhsType *)
35+
(* subNbhsType V S == structure that extends a *)
36+
(* subChoiceType/nbhsType with the isSubNbhs *)
37+
(* interface *)
38+
(* The HB class is SubNbhs. *)
39+
(* filterI_iter F n == nth stage of recursively building the *)
40+
(* filter of finite intersections of F *)
41+
(* finI_from D f == set of \bigcap_(i in E) f i where E is a *)
42+
(* a finite subset of D *)
3343
(* ``` *)
3444
(* *)
3545
(* 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 :
951961
{for x, continuous (g \o f)}.
952962
Proof. exact: cvg_comp. Qed.
953963

964+
HB.mixin Record isSubNbhs
965+
(V : nbhsType) (S : pred V) U & SubChoice V S U & Nbhs U := {
966+
continuous_valE : continuous (val : U -> V)
967+
}.
968+
969+
#[short(type="subNbhsType")]
970+
HB.structure Definition SubNbhs (V : nbhsType) (S : pred V) :=
971+
{ U of SubChoice V S U & Nbhs U & isSubNbhs V S U}.
972+
954973
Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) :
955974
{for x, continuous f} ->
956975
(\forall y \near f x, P y) -> (\near x, P (f x)).

‎classical/mathcomp_extra.v‎

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *)
2-
From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.
2+
From HB Require Import structures.
3+
From mathcomp Require Import all_ssreflect_compat finmap all_algebra.
34

45
(**md**************************************************************************)
56
(* # MathComp extra *)
@@ -93,10 +94,21 @@ Proof. by case: C => //= /ltW. Qed.
9394
(* MathComp 2.6 additions *)
9495
(**************************)
9596

96-
(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
9797
Lemma intrD1 {R : pzRingType} (i : int) : (i + 1)%:~R = i%:~R + 1 :> R.
9898
Proof. by rewrite intrD. Qed.
9999

100-
(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
101100
Lemma intr1D {R : pzRingType} (i : int) : (1 + i)%:~R = 1 + i%:~R :> R.
102101
Proof. by rewrite intrD. Qed.
102+
103+
Lemma divDl_ge0 (R : numDomainType) (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) :
104+
0 <= s / (s + t).
105+
Proof.
106+
by apply: divr_ge0 => //; apply: addr_ge0.
107+
Qed.
108+
109+
Lemma divDl_le1 (R : numFieldType) (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) :
110+
s / (s + t) <= 1.
111+
Proof.
112+
move: s0; rewrite le0r => /predU1P [->|s0]; first by rewrite mul0r.
113+
by rewrite ler_pdivrMr ?mul1r ?lerDl // ltr_wpDr.
114+
Qed.

‎classical/unstable.v‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -369,6 +369,13 @@ Qed.
369369
Lemma onemV (F : numFieldType) (x : F) : x != 0 -> x^-1.~ = (x - 1) / x.
370370
Proof. by move=> ?; rewrite mulrDl divff// mulN1r. Qed.
371371

372+
Lemma divD_onem (R : realFieldType) (s t : R) (s0 : 0 < s) (t0 : 0 < t) :
373+
(s / (s + t)).~ = t / (s + t).
374+
Proof.
375+
rewrite /onem.
376+
by rewrite -(@divff _ (s + t)) ?gt_eqF ?addr_gt0// -mulrBl (addrC s) addrK.
377+
Qed.
378+
372379
Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N.
373380
Proof. by case: a => //= n _; case: b. Qed.
374381

0 commit comments

Comments
 (0)