Hahn banach 2026

CHANGELOG_UNRELEASED.md

@@ -81,12 +81,6 @@
 - in `measurable_structure.v`:
   + structure `PMeasurable`, notation `pmeasurableType`
 
-### 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 _->_ | _ }`
@@ -108,9 +102,21 @@
   + lemmas `lcfun_eqP`, `null_fun_continuous`, `fun_cvgD`,
    `fun_cvgN`, `fun_cvgZ`, `fun_cvgZr`
   + lemmas `lcfun_continuous` and `lcfun_linear`
+
+- in `mathcomp_extra.v`:
+  + lemmas `divDl_ge0`, `divDl_le1`
+  + mixin `Zmodule_isSubNormed`
+
+- 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)
 

_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/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,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