Hahn banach 2026

CHANGELOG_UNRELEASED.md

@@ -4,21 +4,217 @@
 
 ### Added
 
+- 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)
+
+- in set_interval.v
+  + `setUitv1`, `setU1itv`, `setDitv1l`, `setDitv1r` (generalized)
+
+- in `set_interval.v`
+  + `itv_is_closed_unbounded` (fix the definition)
+
+- in `set_interval.v`
+  + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool)
+
+- in `lebesgue_Rintegrable.v`:
+  + lemma `Rintegral_cst` (does not use `cst` anymore)
+
+- split `probability.v` into directory `probability_theory` and move contents as:
+  + file `probability.v`:
+  + file `bernoulli_distribution.v`:
+    * definitions `bernoulli_pmf`, `bernoulli_prob`
+    * lemmas `bernoulli_pmf_ge0`, `bernoulli_pmf1`, `measurable_bernoulli_pmf`,
+      `eq_bernoulli`, `bernoulli_dirac`, `eq_bernoulliV2`, `bernoulli_probE`,
+      `measurable_bernoulli_prob`, `measurable_bernoulli_prob2`
+  + file `beta_distribution.v`:
+    * lemmas `continuous_onemXn`, `onemXn_derivable`, `derivable_oo_LRcontinuous_onemXnMr`,
+      `derive_onemXn`, `Rintegral_onemXn`
+    * definition `XMonemX`
+    * lemmas `XMonemX_ge0`, `XMonemX_le1`, `XMonemX0n`, `XMonemXn0`, `XMonemX00`,
+      `XMonemXC`, XMonemXM`, `continuous_XMonemX`, `within_continuous_XMonemX`,
+      `measurable_XMonemX`, `bounded_XMonemX`, `integrable_XMonemX`, `integrable_XMonemX_restrict`,
+      `integral_XMonemX_restrict`
+    * definition `beta_fun`
+    * lemmas `EFin_beta_fun`, `beta_fun_sym`, `beta_fun0n`, `beta_fun00`, `beta_fun1Sn`,
+      `beta_fun11`, `beta_funSSnSm`, `beta_funSnSm`, `beta_fun_fact`, `beta_funE`,
+      `beta_fun_gt0`, `beta_fun_ge0`
+    * definition `beta_pdf`
+    * lemmas `measurable_beta_pdf`, `beta_pdf_ge0`, `beta_pdf_le_beta_funV`, `integrable_beta_pdf`,
+      `bounded_beta_pdf_01`
+    * definition `beta_prob`
+    * lemmas integral_beta_pdf`, `beta_prob01`, `beta_prob_fin_num`, `beta_prob_dom`,
+      `beta_prob_uniform`, `integral_beta_prob_bernoulli_prob_lty`,
+      `integral_beta_prob_bernoulli_prob_onemX_lty`,
+      `integral_beta_prob_bernoulli_prob_onem_lty`, `beta_prob_integrable`,
+      `beta_prob_integrable_onem`, `beta_prob_integrable_dirac`,
+      `beta_prob_integrable_onem_dirac`, `integral_beta_prob`
+    * definition `div_beta_fun`
+    * lemmas `div_beta_fun_ge0`, `div_beta_fun_le1`
+    * definition `beta_prob_bernoulli_prob`
+    * lemmas `beta_prob_bernoulli_probE`
+  + file `binomial_distribution.v`:
+    * definition `binomial_pmf`
+    * lemmas `measurable_binomial_pmf`
+    * definition `binomial_prob`
+    * definition `bin_prob`
+    * lemmas `bin_prob0`, `bin_prob1`, `binomial_msum`, `binomial_probE`,
+      `integral_binomial`, `integral_binomial_prob`, `measurable_binomial_prob`
+  + file `exponential_distribution.v`:
+    * definition `exponential_pdf`
+    * lemmas `exponential_pdf_ge0`, `lt0_exponential_pdf`, `measurable_exponential_pdf`,
+      `exponential_pdfE`, `in_continuous_exponential_pdf`, `within_continuous_exponential_pdf`
+    * definition `exponential_prob`
+    * lemmas `derive1_exponential_pdf`, `exponential_prob_itv0c`, `integral_exponential_pdf`,
+      `integrable_exponential_pdf`
+  + file `normal_distribution.v`:
+    * definition `normal_fun`
+    * lemmas `measurable_normal_fun`, normal_fun_ge0`, `normal_fun_center`
+    * definition `normal_peak`
+    * lemmas `normal_peak_ge0`, `normal_peak_gt0`
+    * definition `normal_pdf`
+    * lemmas `normal_pdfE`, `measurable_normal_pdf`, `normal_pdf_ge0`, `continuous_normal_pdf`,
+      `normal_pdf_ub`
+    * definition `normal_prob`
+    * lemmas `integral_normal_pdf`, `integrable_normal_pdf`, `normal_prob_dominates`
+  + file `poisson_distribution.v`:
+    * definition `poisson_pmf`
+    * lemmas `poisson_pmf_ge0`, `measurable_poisson_pmf`
+    * definition `poisson_prob`
+    * lemma `measurable_poisson_prob`
+  + file `uniform_distribution.v`:
+    * definition `uniform_pdf`
+    * lemmas `uniform_pdf_ge0`, `measurable_uniform_pdf`, `integral_uniform_pdf`,
+      `integral_uniform_pdf1`
+    * definition `uniform_prob`
+    * lemmmas `integrable_uniform_pdf`, `dominates_uniform_prob`,
+      `integral_uniform`
+  + file `random_variable.v`:
+    * definition `random_variable`
+    * lemmas `notin_range_measure`, `probability_range`
+    * definition `distribution`
+    * lemmas `probability_distribution`, `ge0_integral_distribution`, `integral_distribution`
+    * definition `cdf`
+    * lemmas `cdf_ge0`, `cdf_le1`, `cdf_nondecreasing`, `cvg_cdfy1`, `cvg_cdfNy0`,
+      `cdf_right_continuous`, `cdf_lebesgue_stieltjes_id`, `lebesgue_stieltjes_cdf_id`,
+    * definition `ccdf`
+    * lemmas `cdf_ccdf_1`
+    * corollaries `ccdf_cdf_1`, `ccdf_1_cdf`, `cdf_1_ccdf`
+    * lemmas `ccdf_nonincreasing`, `cvg_ccdfy0`, `cvg_ccdfNy1`, `ccdf_right_continuous`
+    * definition `expectation`
+    * lemmas `expectation_def`, `expectation_fin_num`, `expectation_cst`,
+      `expectation_indic`, `integrable_expectation`, `expectationZl`,
+      `expectation_ge0`, `expectation_le`, `expectationD`, `expectationB`,
+      `expectation_sum`, `ge0_expectation_ccdf`
+    * definition `covariance`
+    * lemmas `covarianceE`, `covarianceC`, `covariance_fin_num`,
+      `covariance_cst_l`, `covariance_cst_r`, `covarianceZl`, `covarianceZr`,
+      `covarianceNl`, `covarianceNr`, `covarianceNN`, `covarianceDl`, `covarianceDr`,
+      `covarianceBl`, `covarianceBr`
+    * definition `variance`
+    * lemmas `varianceE`, `variance_fin_num`, `variance_ge0`, `variance_cst`,
+      `varianceZ`, `varianceN`, `varianceD`, `varianceB`, `varianceD_cst_l`, `varianceD_cst_r`,
+      `varianceB_cst_l`, `varianceB_cst_r`, `covariance_le`
+    * definition `mmt_gen_fun`
+    * lemmas `markov`, `chernoff`, `chebyshev`, `cantelli`
+    * definition `discrete_random_variable`
+    * lemmas `dRV_dom_enum`
+    * definitions `dRV_dom`, `dRV_enum`, `enum_prob`
+    * lemmas `distribution_dRV_enum`, `distribution_dRV`, `sum_enum_prob`
+    * definition `pmf`
+    * lemmas `pmf_ge0`, `pmf_gt0_countable`, `pmf_measurable`, `dRV_expectation`,
+      `expectation_pmf`
+
+- moved from `convex.v` to `realfun.v`
+  + lemma `second_derivative_convex`
+
+- in classical_sets.v
+  + lemma `in_set1` (statement changed)
+
+- in `subspace_topology.v`:
+  + lemmas `open_subspaceP` and `closed_subspaceP` (use `exists2` instead of `exists`)
+- moved from `filter.v` to `classical_sets.v`:
+  + definition `set_system`
+- moved from `measurable_structure.v` to `classical_sets.v`:
+  + definitions `setI_closed`, `setU_closed`
+
+- moved from `theories` to `theories/topology_theory`:
+  + file `function_spaces.v`
+
+- moved from `theories` to `theories/normedtype_theory`:
+  + file `tvs.v`
+
+- moved from `tvs.v` to `pseudometric_normed_Zmodule.v`:
+  + definitions `NbhsNmodule`, `NbhsZmodule`, `PreTopologicalNmodule`, `PreTopologicalZmodule`,
+    `PreUniformNmodule`, `PreUniformZmodule`
+
+- in `tvs.v`, turned into `Let`'s:
+  + local lemmas `standard_add_continuous`, `standard_scale_continuous`, `standard_locally_convex`
+
+- in `normed_module.v`, turned into `Let`'s:
+  + local lemmas `add_continuous`, `scale_continuous`, `locally_convex`
+
+- moved from `normed_module.v` to `pseudometric_normed_Zmodule.v` and
+  generalized from `normedModType` to `pseudoMetricNormedZmodType`
+  + lemma `ball_open` (`0 < r` hypothesis also not needed anymore)
+  + lemma `near_shift`
+  + lemma `cvg_comp_shift`
+  + lemma `ball_open_nbhs`
+
+- moved from `tvs.v` to `convex.v`
+  + definition `convex`, renamed to `convex_set`
+  + definition `convex`
+
 ### Renamed
 
 - in `tvs.v`:
   + definition `tvsType` -> `convexTvsType`
-  + HB class `Tvs` -> `ConvexTvs`
-  + HB mixin `Uniform_isTvs` -> `Uniform_isConvexTvs`
-  + HB factory `PreTopologicalLmod_isTvs` -> `PreTopologicalLmod_isConvexTvs`
-  + Section `Tvs_numDomain` -> `ConvexTvs_numDomain`
-  + Section `Tvs_numField` -> `ConvexTvs_numField`
-  + Section `prod_Tvs` -> `prod_ConvexTvs`
+  + class `Tvs` -> `ConvexTvs`
+  + mixin `Uniform_isTvs` -> `Uniform_isConvexTvs`
+  + factory `PreTopologicalLmod_isTvs` -> `PreTopologicalLmod_isConvexTvs`
+  + section `Tvs_numDomain` -> `ConvexTvs_numDomain`
+  + section `Tvs_numField` -> `ConvexTvs_numField`
+  + section `prod_Tvs` -> `prod_ConvexTvs`
 
 - in `normed_module.v`
-  + HB mixin ` PseudoMetricNormedZmod_Tvs_isNormedModule` ->
+  + mixin ` PseudoMetricNormedZmod_Tvs_isNormedModule` ->
     ` PseudoMetricNormedZmod_ConvexTvs_isNormedModule`
 
 ### Generalized

_CoqProject

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

classical/filter.v

@@ -946,6 +946,11 @@ Definition continuous_at (T U : nbhsType) (x : T) (f : T -> U) :=
   (f%function @ x --> f%function x).
 Notation continuous f := (forall x, continuous_at x f).
 
+Lemma continuous_comp (R S T : nbhsType) (f : R -> S) (g : S -> T) x :
+  {for x, continuous f} -> {for (f x), continuous g} ->
+  {for x, continuous (g \o f)}.
+Proof. exact: cvg_comp. Qed.
+
 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/functions.v

@@ -128,6 +128,19 @@ Add Search Blacklist "_mixin_".
 (*                   fctE == multi-rule for fct                               *)
 (* ```                                                                        *)
 (*                                                                            *)
+(* ```                                                                        *)
+(*           linfun E F s == membership predicate for linear functions of     *)
+(*                           type E -> F with scalar operator                 *)
+(*                           s : K -> F -> F                                  *)
+(*                           E and F have type lmodType K.                    *)
+(*                           This is used in particular to attach a type of   *)
+(*                           lmodType to {linear E -> F | s}.                 *)
+(*          linfun_spec f == specification for membership of the linear       *)
+(*                           function f                                       *)
+(* ```                                                                        *)
+(*                                                                            *)
+(*                                                                            *)
+(*                                                                            *)
 (******************************************************************************)
 
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
@@ -2750,3 +2763,96 @@ End function_space_lemmas.
 
 Lemma inv_funK T (R : unitRingType) (f : T -> R) : (f\^-1\^-1)%R = f.
 Proof. by apply/funeqP => x; rewrite /inv_fun/= GRing.invrK. Qed.
+
+Local Open Scope ring_scope.
+Import GRing.Theory.
+
+Section linfun_pred.
+Context {K : numDomainType} {E : lmodType K}  {F : lmodType K}
+  {s : K -> F -> F}.
+
+(**md Beware that `lfun` is reserved for vector types, hence this one has been
+ named `linfun` *)
+Definition linfun : {pred E -> F} := mem [set f | linear_for s f ].
+
+Definition linfun_key : pred_key linfun. Proof. exact. Qed.
+
+Canonical linfun_keyed := KeyedPred linfun_key.
+
+End linfun_pred.
+
+Section linfun.
+Context {R : numDomainType} {E : lmodType R}
+  {F : lmodType R} {s : GRing.Scale.law R F}.
+
+Notation T := {linear E -> F | s}.
+
+Notation linfun := (@linfun _ E F s).
+
+Section Sub.
+Context (f : E -> F) (fP : f \in linfun).
+
+#[local] Definition linfun_Sub_subproof :=
+  @GRing.isLinear.Build _ E F s f (set_mem fP).
+
+#[local] HB.instance Definition _ := linfun_Sub_subproof.
+Definition linfun_Sub : {linear _  -> _ | _ } := f.
+End Sub.
+
+Let linfun_rect (K : T -> Type) :
+  (forall f (Pf : f \in linfun), K (linfun_Sub Pf)) -> forall u : T, K u.
+Proof.
+move=> Ksub [f] [[[Pf1 Pf2]] [Pf3]].
+set G := (G in K G).
+have Pf : f \in linfun by rewrite inE /= => // x u y; rewrite Pf2 Pf3.
+suff -> : G = linfun_Sub Pf by apply: Ksub.
+rewrite {}/G.
+congr (GRing.Linear.Pack (GRing.Linear.Class _ _)).
+- by congr GRing.isNmodMorphism.Axioms_; exact: Prop_irrelevance.
+- by congr GRing.isScalable.Axioms_; exact: Prop_irrelevance.
+Qed.
+
+Let linfun_valP f (Pf : f \in linfun) : linfun_Sub Pf = f :> (_ -> _).
+Proof. by []. Qed.
+
+HB.instance Definition _ := isSub.Build _ _ T linfun_rect linfun_valP.
+
+Lemma linfun_eqP (f g : {linear E -> F | s}) : f = g <-> f =1 g.
+Proof. by split=> [->//|fg]; exact/val_inj/funext. Qed.
+
+HB.instance Definition _ := [Choice of {linear E -> F | s} by <:].
+
+Variant linfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
+| Islinfun (l : {linear E -> F | s}) : linfun_spec f l true.
+
+Lemma linfunP (f : E -> F) : f \in linfun -> linfun_spec f f (f \in linfun).
+Proof.
+move=> /[dup] f_lc ->.
+have {2}-> : f = linfun_Sub f_lc by rewrite linfun_valP.
+by constructor.
+Qed.
+
+End linfun.
+
+Section linfun_lmodtype.
+Context {R : numFieldType} {E F : lmodType R}.
+Import GRing.Theory.
+
+Let linfun_submod_closed  : submod_closed (@linfun R E F *:%R).
+Proof.
+split; first by rewrite inE; exact/linearP.
+move=> r /= _ _ /linfunP[f] /linfunP[g].
+by rewrite inE /=; exact: linearP.
+Qed.
+
+HB.instance Definition _ :=
+  @GRing.isSubmodClosed.Build _  _ linfun linfun_submod_closed.
+
+HB.instance Definition _ :=
+  [SubChoice_isSubLmodule of {linear E -> F } by <:].
+
+End linfun_lmodtype.
+
+(* TODO: we wanted to declare this instance in classical_sets.v but failed and did not understand why, also we couldn't generalize *)
+HB.instance Definition _ {R : numDomainType} (E F : lmodType R) :=
+  isPointed.Build {linear E -> F} (\0)%R.

theories/Make

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