From f7460af18ebd76d13daf396a15727da9293b1628 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 20 Mar 2026 11:14:19 +0900 Subject: [PATCH 01/21] Hahn-Banach theorem --- CHANGELOG_UNRELEASED.md | 195 ++++++++++++++ _CoqProject | 2 + theories/Make | 2 + theories/hahn_banach_theorem.v | 428 +++++++++++++++++++++++++++++++ theories/normedtype_theory/tvs.v | 5 +- 5 files changed, 630 insertions(+), 2 deletions(-) create mode 100644 theories/hahn_banach_theorem.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 18411b030..c67a6695a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -49,9 +49,204 @@ ### Changed +- 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`: diff --git a/_CoqProject b/_CoqProject index 456b4f83f..7b8e7ba4f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -89,6 +89,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 diff --git a/theories/Make b/theories/Make index acde6dc9a..580669249 100644 --- a/theories/Make +++ b/theories/Make @@ -55,6 +55,8 @@ normedtype_theory/urysohn.v normedtype_theory/vitali_lemma.v normedtype_theory/normedtype.v +hahn_banach_theorem.v + realfun.v sequences.v exp.v diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v new file mode 100644 index 000000000..afd06c151 --- /dev/null +++ b/theories/hahn_banach_theorem.v @@ -0,0 +1,428 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import interval_inference. +From mathcomp Require Import unstable wochoice boolp classical_sets topology reals. +From mathcomp Require Import filter reals normedtype convex. +Import numFieldNormedType.Exports. +Local Open Scope classical_set_scope. + + + + +(**md**************************************************************************) +(* *) +(* *) +(* This files proves the Hahn-Banach theorem thanks to Zorn's lemma. Theorem *) +(* `Hahnbanach` states that, considering `V` a Lmodtype on a realtype, a *) +(* linear function on a subLmotdype of V, that is bounded by a convex *) +(* function, can be extended to a linear map on V boundeby the same convex *) +(* function. Theorem `HBgeom` specifies this to the extention of a linear *) +(* continuous function on a subspace to the whole NormedModule. *) +(* *) +(* Module Lingraph == definitions on linear relations, thought of as *) +(* graph of functions *) +(* Module HBPreparation == defintion of the type Zorntype of linear *) +(* functional graphs, bounded by a convex function *) +(* and extending to the whole space a given linear *) +(* graph. *) +(******************************************************************************) + + + + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. + + +Local Open Scope ring_scope. +Local Open Scope convex_scope. +Local Open Scope real_scope. +Import GRing.Theory. +Import Num.Theory. + + +Section pos_quotient. + +(* auxiliary lemmas that could be moved elsewhere *) +(* TBD once merged in mathcomp *) + +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. + +Lemma divD_onem (R: realType) (s t : R) (s0 : 0 < s) (t0 : 0 < t): (s / (s + t)).~ = t / (s + t). +Proof. +rewrite /(_).~. +suff -> : 1 = (s + t)/(s + t) by rewrite -mulrBl -addrAC subrr add0r. +rewrite divff // /eqP addr_eq0; apply/negbT/eqP => H. +by move: s0; rewrite H oppr_gt0 ltNge; move/negP; apply; rewrite ltW. +Qed. + +End pos_quotient. + + +Module Lingraph. +Section Lingraphsec. + +Variables (R : numDomainType) (V : lmodType R). + +Definition graph := V -> R -> Prop. + +Definition linear_graph (f : graph) := + forall v1 v2 l r1 r2, f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2). + +Variable f : graph. +Hypothesis lrf : linear_graph f. + +Lemma lingraph_00 x r : f x r -> f 0 0. +Proof. +suff -> : f 0 0 = f (x + (-1) *: x) (r + (-1) * r) by move=> h; apply: lrf. +by rewrite scaleNr mulNr mul1r scale1r !subrr. +Qed. + +Lemma lingraph_scale x r l : f x r -> f (l *: x) (l * r). +Proof. +move=> fxr. +have -> : f (l *: x) (l * r) = f (0 + l *: x) (0 + l * r) by rewrite !add0r. +by apply: lrf=> //; exact: lingraph_00 fxr. +Qed. + +Lemma lingraph_add x1 x2 r1 r2 : f x1 r1 -> f x2 r2 -> f (x1 - x2)(r1 - r2). +Proof. +have -> : x1 - x2 = x1 + (-1) *: x2 by rewrite scaleNr scale1r. +have -> : r1 - r2 = r1 + (-1) * r2 by rewrite mulNr mul1r. +by exact: lrf. +Qed. + + +Definition add_line f w a := fun v r => exists v' : V, exists r' : R, exists lambda : R, + [/\ f v' r', v = v' + lambda *: w & r = r' + lambda * a]. + +End Lingraphsec. +End Lingraph. + + +Module HBPreparation. +Section HBPreparation. +Import Lingraph. +Variables (R : realType) (V : lmodType R) (F : pred V). +Variables (F' : subLmodType F) (phi : {linear F' -> R}) (p : V -> R). + +Implicit Types (f g : graph V). + +Hypothesis phi_le_p : forall v, (phi v) <= (p (val v)). + +Hypothesis p_cvx : (@convex_function R V [set: V] p). + +Definition extend_graph f := forall (v : F'), f (\val v) (phi v). + +Definition le_graph p f := forall v r, f v r -> r <= p v. + +Definition functional_graph f := forall v r1 r2, f v r1 -> f v r2 -> r1 = r2. + +Definition linear_graph f := + forall v1 v2 l r1 r2, f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2). + +Definition le_extend_graph f := + [/\ functional_graph f, linear_graph f, le_graph p f & extend_graph f]. + +Record zorn_type : Type := ZornType + {carrier : graph V; specP : le_extend_graph carrier}. + +Let spec_phi : le_extend_graph (fun v r => exists2 y : F', v = val y & r = phi y). +Proof. +split. +- by move=> v r1 r2 [y1 -> ->] [y2 + ->] => /val_inj ->. +- move => v1 v2 l r1 r2 [y1 -> ->] [y2 -> ->]. + by exists (y1 + l *: y2); rewrite !linearD !linearZ //. +- by move => r v [y -> ->]. +- by move => v; exists v. +Qed. + +Definition zphi := ZornType spec_phi. + +Lemma zorn_type_eq z1 z2 : carrier z1 = carrier z2 -> z1 = z2. +Proof. +case: z1 => m1 pm1; case: z2 => m2 pm2 /= e; move: pm1 pm2; rewrite e => pm1 pm2. +by congr ZornType; apply: Prop_irrelevance. +Qed. + +Definition zornS (z1 z2 : zorn_type):= + forall x y, (carrier z1 x y) -> (carrier z2 x y ). + +(* Zorn applied to the relation of extending the graph of the first function *) +Lemma zornS_ex : exists g : zorn_type, forall z, zornS g z -> z = g. +Proof. +pose Rbool := (fun x y => `[< zornS x y >]). +have RboolP : forall z t, Rbool z t <-> zornS z t by split; move => /asboolP //=. +suff [t st]: exists t : zorn_type, forall s : zorn_type, Rbool t s -> s = t. + by exists t; move => z /RboolP tz; apply: st. +apply: (@Zorn zorn_type Rbool); first by move => t; apply/RboolP. +- by move => r s t /RboolP a /RboolP b; apply/RboolP => x y /a /b. +- move => r s /RboolP a /RboolP b; apply: zorn_type_eq. + by apply: funext => z; apply: funext => h;apply: propext; split => [/a | /b]. +- move => A Amax. + case: (lem (exists a, A a)) => [[w Aw] | eA]; last by exists zphi => a Aa; elim: eA; exists a. + (* g is the union of the graphs indexed by elements in a *) + pose g v r := exists a, A a /\ (carrier a v r). + have g_fun : functional_graph g. + move=> v r1 r2 [a [Aa avr1]] [b [Ab bvr2]]. + have [] : Rbool a b \/ Rbool b a by exact: Amax. + rewrite /Rbool /RboolP /zornS; case: b Ab bvr2 {Aa}. + move => s2 [fs2 _ _ _] /= _ s2vr2 /asboolP ecas2. + by move/ecas2: avr1 => /fs2 /(_ s2vr2). + rewrite /Rbool /RboolP /zornS; case: a Aa avr1 {Ab} => s1 [fs1 _ _ _] /= _ s1vr1 /asboolP ecbs1. + by move/ecbs1: bvr2; apply: fs1. +have g_lin : linear_graph g. + move=> v1 v2 l r1 r2 [a1 [Aa1 c1]] [a2 [Aa2 c2]]. + have [/RboolP sc12 | /RboolP sc21] := Amax _ _ Aa1 Aa2. + - have {c1 sc12 Aa1 a1} c1 : carrier a2 v1 r1 by apply: sc12. + exists a2; split=> //; case: a2 {Aa2} c2 c1 => c /= [_ hl _ _] *; exact: hl. + - have {c2 sc21 Aa2 a2} c2 : carrier a1 v2 r2 by apply: sc21. + exists a1; split=> //; case: a1 {Aa1} c2 c1 => c /= [_ hl _ _] *; exact: hl. +have g_majp : le_graph p g by move=> v r [[c [fs1 ls1 ms1 ps1]]] /= [_ /ms1]. +have g_prol : extend_graph g. + move=> *; exists w; split=> //; case: w Aw => [c [_ _ _ hp]] _ //=; exact: hp. + have spec_g : le_extend_graph g by split. +pose zg := ZornType spec_g. +by exists zg => [a Aa]; apply/RboolP; rewrite /zornS => v r cvr; exists a. +Qed. + +Variable g : zorn_type. + +Hypothesis gP : forall z, zornS g z -> z = g. + +(*The next lemma proves that when z is of zorn_type, it can be extended on any +real line directed by an arbitrary vector v *) + +Lemma domain_extend (z : zorn_type) v : + exists2 ze : zorn_type, (zornS z ze) & (exists r, (carrier ze) v r). +Proof. +case: (lem (exists r, (carrier z v r))). + by case=> r rP; exists z => //; exists r. +case: z => [c [fs1 ls1 ms1 ps1]] /= nzv. +have c00 : c 0 0. + have <- : phi 0 = 0 by rewrite linear0. + by move: ps1; rewrite /extend_graph /= => /(_ 0) /=; rewrite GRing.val0; apply. +have [a aP] : exists a, forall (x : V) (r lambda : R), c x r -> r + lambda * a <= p (x + lambda *: v). + suff [a aP] : exists a, forall (x : V) (r lambda : R), c x r -> 0 < lambda -> + r + lambda * a <= p (x + lambda *: v) /\ r - lambda * a <= p (x - lambda *: v). + exists a=> x r lambda cxr. + have {aP} aP := aP _ _ _ cxr. + case: (ltrgt0P lambda) ; [by case/aP | move=> ltl0 | move->]; last first. + by rewrite mul0r scale0r !addr0; apply: ms1. + rewrite -[lambda]opprK scaleNr mulNr. + have /aP [] : 0 < - lambda by rewrite oppr_gt0. + done. + pose b (x : V) r lambda : R := (p (x + lambda *: v) - r) / lambda. + pose a (x : V) r lambda : R := (r - p (x - lambda *: v)) / lambda. + have le_a_b x1 x2 r1 r2 s t : c x1 r1 -> c x2 r2 -> 0 < s -> 0 < t -> a x1 r1 s <= b x2 r2 t. + move=> cxr1 cxr2 lt0s lt0t; rewrite /a /b. + rewrite ler_pdivlMr // mulrAC ler_pdivrMr // mulrC [_ * s]mulrC. + rewrite !mulrDr !mulrN lerBlDr addrAC lerBrDr. + have /ler_pM2r <- : 0 < (s + t) ^-1 by rewrite invr_gt0 addr_gt0. + set y1 : V := _ + _ *: _; set y2 : V := _ - _ *: _. + set rhs := (X in _ <= X). + have step1 : p (s / (s + t) *: y1 + t / (s + t) *: y2) <= rhs. + rewrite /rhs !mulrDl ![_ * _ / _]mulrAC. + pose st := Itv01 (divDl_ge0 (ltW lt0s) (ltW lt0t)) ((divDl_le1 (ltW lt0s) (ltW lt0t))). + move: (p_cvx st (in_setT y1) (in_setT y2)). + by rewrite /conv /= [X in ((_ <= X)-> _)]/conv /= divD_onem /=. + apply: le_trans step1 => {rhs}. + set u : V := (X in p X). + have {u y1 y2} -> : u = t / (s + t) *: x1 + s / (s + t) *: x2. + rewrite /u ![_ / _]mulrC -!scalerA -!scalerDr /y1 /y2; congr (_ *: _). + by rewrite !scalerDr addrCA scalerN scalerA [s * t]mulrC -scalerA addrK. + set l := t / _; set m := s / _; set lhs := (X in X <= _). + have {lhs} -> : lhs = l * r1 + m * r2. + by rewrite /lhs mulrDl ![_ * _ / _]mulrAC. + apply: ms1; apply: (ls1) => //. + rewrite -[_ *: _]add0r -[_ * _] add0r; apply: ls1 => //. + pose Pa : set R := fun r => exists x1, exists r1, exists s1, + [/\ c x1 r1, 0 < s1 & r = a x1 r1 s1]. + pose Pb : set R := fun r => exists x1, exists r1, exists s1, + [/\ c x1 r1, 0 < s1 & r = b x1 r1 s1]. + pose sa := reals.sup Pa. (* This is why we need realTypes, we need p with values in a realType *) + have Pax : Pa !=set0 by exists (a 0 0 1); exists 0; exists 0; exists 1; split. + have ubdP : ubound Pa sa. + apply: sup_upper_bound; split => //=. + exists (b 0 0 1) =>/= x [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01. + have saP: forall u : R, ubound Pa u -> sa <= u by move=> u; apply: ge_sup. + pose ib := reals.inf Pb. (* This is why we need realTypes, we need P with values in a realType *) + have Pbx : Pb !=set0 by exists (b 0 0 1); exists 0; exists 0; exists 1; split. + have ibdP : lbound Pb ib. + by apply: ge_inf; exists (a 0 0 1) =>/= x [y [r [s [cry lt0s ->]]]]; apply: le_a_b => //; exact: ltr01. + have ibP: forall u : R, lbound Pb u -> u <= ib by move=> u; apply: lb_le_inf Pbx. + have le_sa_ib : sa <= ib. + apply: saP=> r' [y [r [l [cry lt0l -> {r'}]]]]. + apply: ibP=> s' [z [s [m [crz lt0m -> {s'}]]]]; exact: le_a_b. + pose alpha := ((sa + ib) / 2%:R). + have le_alpha_ib : alpha <= ib by rewrite /alpha midf_le. + have le_sa_alpha : sa <= alpha by rewrite /alpha midf_le. + exists alpha => x r l cxr lt0l; split. + - suff : alpha <= b x r l. + by rewrite /b; move/ler_pdivlMr: lt0l->; rewrite lerBrDl mulrC. + by apply: le_trans le_alpha_ib _; apply: ibdP; exists x; exists r; exists l. + - suff : a x r l <= alpha. + by rewrite /a; move/ler_pdivrMr: lt0l-> ; rewrite lerBlDl -lerBlDr mulrC. + by apply: le_trans le_sa_alpha; apply: ubdP; exists x; exists r; exists l. +pose z' := fun k r => exists v' : V, exists r' : R, exists lambda : R, + [/\ c v' r', k = v' + lambda *: v & r = r' + lambda * a]. +have z'_extends : forall v r, c v r -> z' v r. + by move=> x r cxr; exists x; exists r; exists 0; split; rewrite // ?scale0r ?mul0r !addr0. +have z'_prol : extend_graph z'. + by move=> x; exists (val x); exists (phi x); exists 0; split; rewrite // ?scale0r ?mul0r !addr0. +have z'_maj_by_p : le_graph p z' by move=> x r [w [s [l [cws -> ->]]]]; apply: aP. +have z'_lin : linear_graph z'. + move=> x1 x2 l r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 -> ->]]]]. + set w := (X in z' X _); set s := (X in z' _ X). + have {w} -> : w = w1 + l *: w2 + (m1 + l * m2) *: v. + by rewrite /w !scalerDr !scalerDl scalerA -!addrA [X in _ + X]addrCA. + have {s} -> : s = s1 + l * s2 + (m1 + l * m2) * a. + by rewrite /s !mulrDr !mulrDl mulrA -!addrA [X in _ + X]addrCA. + exists (w1 + l *: w2); exists (s1 + l * s2); exists (m1 + l * m2); split=> //. + by exact: ls1. +have z'_functional : functional_graph z'. + move=> w r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 e1 ->]]]]. + have h1 (x : V) (r l : R) : x = l *: v -> c x r -> x = 0 /\ l = 0. + move=> -> cxr; case: (l =P 0) => [-> | /eqP ln0]; first by rewrite scale0r. + suff cvs: c v (l^-1 * r) by elim:nzv; exists (l^-1 * r). + suff -> : v = l ^-1 *: (l *: v). + have -> : c(l^-1*:(l*:v))(l^-1*r) = c(0 + l^-1*:(l*:v))(0+l^-1*r) by rewrite !add0r. + by apply: ls1=> //; apply: linrel_00 fxr. + by rewrite scalerA mulVf ?scale1r. + have [rw12 erw12] : exists r, c (w1 - w2) r. + exists (s1+(-1)*s2). + have -> : w1 - w2 = w1 + (-1) *: w2 by rewrite scaleNr scale1r. + by apply: ls1. + have [ew12 /eqP]: w1 - w2 = 0 /\ (m2 - m1 = 0). + apply: h1 erw12; rewrite scalerBl; apply/eqP; rewrite subr_eq addrC addrA. + by rewrite -subr_eq opprK e1. + suff -> : s1 = s2 by rewrite subr_eq0=> /eqP->. + by apply: fs1 cws2; move/eqP: ew12; rewrite subr_eq0=> /eqP<-. +have z'_spec : le_extend_graph z' by split. +pose zz' := ZornType z'_spec. +exists zz'; rewrite /zornS => //=; exists a; exists 0; exists 0; exists 1. +by rewrite add0r mul1r scale1r add0r; split. +Qed. + +Let tot_g v : exists r, carrier g v r. +Proof. +have [z /gP sgz [r zr]]:= domain_extend g v. +by exists r; rewrite -sgz. +Qed. + + +Lemma hb_witness : exists h : V -> R, forall v r, carrier g v r <-> (h v = r). +Proof. +move: (choice tot_g) => [h hP]; exists h => v r; split; last by move<-. +case: g gP tot_g hP => c /= [fg lg mg pg] => gP' tot_g' hP cvr. +by have -> // := fg v r (h v). +Qed. + + +End HBPreparation. +End HBPreparation. + +Section HahnBanach. +Import Lingraph. +Import HBPreparation. +(* Now we prove HahnBanach on functions*) +(* We consider R a real (=ordered) field with supremum, and V a (left) module + on R. We do not make use of the 'vector' interface as the latter enforces + finite dimension. *) + +Variables (R : realType) (V : lmodType R) (F : pred V). + +Variables (F' : subLmodType F) (f : {linear F' -> R}) (p : V -> R). + +Hypothesis p_cvx : (@convex_function R V [set: V] p). + +Hypothesis f_bounded_by_p : forall (z : F'), (f z <= p (\val z)). + +Theorem HahnBanach : exists g : {scalar V}, +(forall x, g x <= p x) /\ (forall (z : F'), g (\val z) = f z). +Proof. +pose graphF (v : V) r := exists2 z : F', v = \val z & r = f z. +have [z zmax]:= zornS_ex f_bounded_by_p. +have [g gP]:= (hb_witness p_cvx zmax). +have scalg : linear_for *%R g. + case: z {zmax} gP=> [c [_ ls1 _ _]] /= gP. + have addg : additive g. + by move=> w1 w2; apply/gP; apply: lingraph_add =>//; apply/gP. + suff scalg : scalable_for *%R g. + by move=> a u v; rewrite -gP (addrC _ v) (addrC _ (g v)); apply: ls1; apply /gP. + by move=> w l; apply/gP; apply: lingraph_scale=> //; apply/gP. +pose H := GRing.isLinear.Build _ _ _ _ g scalg. +pose g' : {linear V -> R | *%R} := HB.pack g H. +exists g'. +split; last first. + by move => z'; apply/gP; case: z {zmax gP} => [c [_ _ _ pf]] /=; exact: pf. +by case: z {zmax} gP => [c [_ _ bp _]] /= gP => x; apply: bp; apply/gP. +Qed. + +End HahnBanach. + +Section HBGeom. +(*TODO : define on convextvstype once issue #1927 solved*) + +Variable (R : realType) (V : normedModType R) (F : pred V) +(F' : subLmodType F) (f : {linear F' -> R}). + +(* once subnormedspaces are correctly defined replace by +Variable (R : realType) (V : normedModType R) (F : pred V) +(f : {linear_continuous F' -> R}). +*) + +Let setF := [set x : V | exists (z : F'), val z = x]. + +Theorem HB_geom_normed : + (exists r , (r > 0 ) /\ (forall (z : F'), (`|f z| ) <= `|(val z)| * r)) -> +(* hypothesis to delete once f is of type {linear_continuous _ -> _ } + and obtain through continuous_linear_bounded *) + exists g: {linear_continuous V -> R}, (forall x, (g (val x) = f x)). +Proof. + move=> [r [ltr0 fxrx]]. + pose p:= fun x : V => `|x|*r. + have convp: (@convex_function _ _ [set: V] p). + rewrite /convex_function /conv => l v1 v2 _ _ /=. + rewrite [X in (_ <= X)]/conv /= /p. + apply: le_trans. + have H : `|l%:num *: v1 + (l%:num).~ *: v2| <= `|l%:num *: v1| + `|(l%:num).~ *: v2|. + by apply: ler_normD. + by apply: (@ler_pM _ _ _ r r _ _ H) => //; apply: ltW. + rewrite mulrDl !normrZ -![_ *: _]/(_ * _). + have -> : `|l%:num| = l%:num by apply/normr_idP. + have -> : `|(l%:num).~| = (l%:num).~ by apply/normr_idP; apply: onem_ge0. + by rewrite !mulrA. + have majfp : forall z : F', f z <= p (\val z). + move => z; rewrite /(p _) ; apply : le_trans; last by []. + by apply : ler_norm. + move: (HahnBanach convp majfp) => [g] [majgp F_eqgf] {majfp}. +have ling :(linear (g : V -> R)) by exact:linearP. +have contg: (continuous (g : V -> R)). + move=> x; rewrite /cvgP; apply: (continuousfor0_continuous). + apply: bounded_linear_continuous. + exists r; split; first by exact: gtr0_real. + move => M m1; rewrite nbhs_ballP; exists 1 => /=; first by []. + move => y; rewrite -ball_normE //= sub0r => y1. + rewrite ler_norml; apply/andP. split. + - rewrite lerNl -linearN; apply: (le_trans (majgp (-y))). + by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. + - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN. + apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. +pose Hg := isLinearContinuous.Build _ _ _ _ g ling contg. +pose g': {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) Hg. +by exists g'. +Qed. + +End HBGeom. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 1f8d3dcd7..4063e2e56 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -576,6 +576,7 @@ Unshelve. all: by end_near. Qed. Local Open Scope convex_scope. + Let standard_ball_convex_set (x : R^o) (r : R) : convex_set (ball x r). Proof. apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1. @@ -668,7 +669,7 @@ HB.instance Definition _ := Uniform_isConvexTvs.Build K (E * F)%type prod_locally_convex. End prod_ConvexTvs. - + HB.structure Definition LinearContinuous (K : numDomainType) (E : NbhsLmodule.type K) (F : NbhsZmodule.type) (s : K -> F -> F) := {f of @GRing.Linear K E F s f & @Continuous E F f }. @@ -771,7 +772,7 @@ Context {R : numDomainType} {E F : NbhsLmodule.type R} Let lcfun_comp_subproof1 : linear_for s (g \o f). Proof. by move=> *; move=> *; rewrite !linearP. Qed. -Let lcfun_comp_subproof2 : continuous (g \o f). +Let lcfun_comp_subproof2 : continuous (g \o f). Proof. by move=> x; apply: continuous_comp; exact/cts_fun. Qed. HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f) From 6cd072818eaa91440d346d079a588ee17c31af8d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 15 Apr 2026 14:29:02 +0900 Subject: [PATCH 02/21] minor linting --- theories/hahn_banach_theorem.v | 153 ++++++++++++++++----------------- 1 file changed, 73 insertions(+), 80 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index afd06c151..cc899eaf0 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -6,79 +6,72 @@ From mathcomp Require Import filter reals normedtype convex. Import numFieldNormedType.Exports. Local Open Scope classical_set_scope. - - - (**md**************************************************************************) +(* # The Hahn-Banach theorem *) (* *) -(* *) -(* This files proves the Hahn-Banach theorem thanks to Zorn's lemma. Theorem *) -(* `Hahnbanach` states that, considering `V` a Lmodtype on a realtype, a *) -(* linear function on a subLmotdype of V, that is bounded by a convex *) +(* This files proves the Hahn-Banach theorem thanks to Zorn's lemma. Theorem *) +(* `Hahnbanach` states that, considering `V` an lmodtype on a realtype, a *) +(* linear function on a subLmodype of V, that is bounded by a convex *) (* function, can be extended to a linear map on V boundeby the same convex *) -(* function. Theorem `HBgeom` specifies this to the extention of a linear *) -(* continuous function on a subspace to the whole NormedModule. *) +(* function. Theorem `HB_geom_normed` specifies this to the extention of a *) +(* linear continuous function on a subspace to the whole NormedModule. *) (* *) +(* ``` *) (* Module Lingraph == definitions on linear relations, thought of as *) (* graph of functions *) (* Module HBPreparation == defintion of the type Zorntype of linear *) (* functional graphs, bounded by a convex function *) (* and extending to the whole space a given linear *) (* graph. *) +(* ``` *) +(* *) (******************************************************************************) - - - Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. - Local Open Scope ring_scope. Local Open Scope convex_scope. Local Open Scope real_scope. Import GRing.Theory. Import Num.Theory. - Section pos_quotient. (* auxiliary lemmas that could be moved elsewhere *) -(* TBD once merged in mathcomp *) +(* NB: to appear in MathComp 2.6.0 *) 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. +(* NB: to appear in MathComp 2.6.0 *) 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. -Lemma divD_onem (R: realType) (s t : R) (s0 : 0 < s) (t0 : 0 < t): (s / (s + t)).~ = t / (s + t). +Lemma divD_onem (R: realType) (s t : R) (s0 : 0 < s) (t0 : 0 < t) : + (s / (s + t)).~ = t / (s + t). Proof. -rewrite /(_).~. -suff -> : 1 = (s + t)/(s + t) by rewrite -mulrBl -addrAC subrr add0r. -rewrite divff // /eqP addr_eq0; apply/negbT/eqP => H. -by move: s0; rewrite H oppr_gt0 ltNge; move/negP; apply; rewrite ltW. +rewrite /onem. +by rewrite -(@divff _ (s + t)) ?gt_eqF ?addr_gt0// -mulrBl (addrC s) addrK. Qed. End pos_quotient. - Module Lingraph. Section Lingraphsec. - Variables (R : numDomainType) (V : lmodType R). Definition graph := V -> R -> Prop. Definition linear_graph (f : graph) := - forall v1 v2 l r1 r2, f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2). + forall v1 v2 l r1 r2, f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2). Variable f : graph. Hypothesis lrf : linear_graph f. @@ -96,21 +89,19 @@ have -> : f (l *: x) (l * r) = f (0 + l *: x) (0 + l * r) by rewrite !add0r. by apply: lrf=> //; exact: lingraph_00 fxr. Qed. -Lemma lingraph_add x1 x2 r1 r2 : f x1 r1 -> f x2 r2 -> f (x1 - x2)(r1 - r2). +Lemma lingraph_add x1 x2 r1 r2 : f x1 r1 -> f x2 r2 -> f (x1 - x2) (r1 - r2). Proof. have -> : x1 - x2 = x1 + (-1) *: x2 by rewrite scaleNr scale1r. have -> : r1 - r2 = r1 + (-1) * r2 by rewrite mulNr mul1r. -by exact: lrf. +exact: lrf. Qed. - -Definition add_line f w a := fun v r => exists v' : V, exists r' : R, exists lambda : R, - [/\ f v' r', v = v' + lambda *: w & r = r' + lambda * a]. +Definition add_line f w a := fun v r => exists (v' : V) (r' : R) (lambda : R), + [/\ f v' r', v = v' + lambda *: w & r = r' + lambda * a]. End Lingraphsec. End Lingraph. - Module HBPreparation. Section HBPreparation. Import Lingraph. @@ -133,66 +124,69 @@ Definition linear_graph f := forall v1 v2 l r1 r2, f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2). Definition le_extend_graph f := - [/\ functional_graph f, linear_graph f, le_graph p f & extend_graph f]. + [/\ functional_graph f, linear_graph f, le_graph p f & extend_graph f]. Record zorn_type : Type := ZornType - {carrier : graph V; specP : le_extend_graph carrier}. + {carrier : graph V; specP : le_extend_graph carrier}. -Let spec_phi : le_extend_graph (fun v r => exists2 y : F', v = val y & r = phi y). +Let spec_phi : le_extend_graph (fun v r => exists2 y : F', v = val y & r = phi y). Proof. split. - by move=> v r1 r2 [y1 -> ->] [y2 + ->] => /val_inj ->. - move => v1 v2 l r1 r2 [y1 -> ->] [y2 -> ->]. - by exists (y1 + l *: y2); rewrite !linearD !linearZ //. -- by move => r v [y -> ->]. -- by move => v; exists v. + by exists (y1 + l *: y2); rewrite !linearD !linearZ. +- by move=> r v [y -> ->]. +- by move=> v; exists v. Qed. Definition zphi := ZornType spec_phi. Lemma zorn_type_eq z1 z2 : carrier z1 = carrier z2 -> z1 = z2. Proof. -case: z1 => m1 pm1; case: z2 => m2 pm2 /= e; move: pm1 pm2; rewrite e => pm1 pm2. -by congr ZornType; apply: Prop_irrelevance. +case: z1 => m1 pm1; case: z2 => m2 pm2 /= e; rewrite e in pm1 pm2 *. +by congr ZornType; exact: Prop_irrelevance. Qed. Definition zornS (z1 z2 : zorn_type):= - forall x y, (carrier z1 x y) -> (carrier z2 x y ). + forall x y, (carrier z1 x y) -> (carrier z2 x y ). -(* Zorn applied to the relation of extending the graph of the first function *) +(* Zorn applied to the relation of extending the graph of the first function: *) Lemma zornS_ex : exists g : zorn_type, forall z, zornS g z -> z = g. Proof. -pose Rbool := (fun x y => `[< zornS x y >]). -have RboolP : forall z t, Rbool z t <-> zornS z t by split; move => /asboolP //=. -suff [t st]: exists t : zorn_type, forall s : zorn_type, Rbool t s -> s = t. - by exists t; move => z /RboolP tz; apply: st. -apply: (@Zorn zorn_type Rbool); first by move => t; apply/RboolP. -- by move => r s t /RboolP a /RboolP b; apply/RboolP => x y /a /b. -- move => r s /RboolP a /RboolP b; apply: zorn_type_eq. - by apply: funext => z; apply: funext => h;apply: propext; split => [/a | /b]. +pose Rbool x y := `[< zornS x y >]. +have RboolP z t : Rbool z t <-> zornS z t by split => /asboolP. +suff [t st] : exists t : zorn_type, forall s : zorn_type, Rbool t s -> s = t. + by exists t; move => z /RboolP tz; exact: st. +apply: (@Zorn zorn_type Rbool); first by move=> t; exact/RboolP. +- by move=> r s t /RboolP a /RboolP b; apply/RboolP => x y /a /b. +- move=> r s /RboolP a /RboolP b; apply: zorn_type_eq. + by apply: funext => z; apply: funext => h; apply: propext; split => [/a | /b]. - move => A Amax. - case: (lem (exists a, A a)) => [[w Aw] | eA]; last by exists zphi => a Aa; elim: eA; exists a. - (* g is the union of the graphs indexed by elements in a *) - pose g v r := exists a, A a /\ (carrier a v r). + have [[w Aw] | eA] := lem (exists a, A a); last first. + by exists zphi => a Aa; elim: eA; exists a. + (* g is the union of the graphs indexed by elements in a *) + pose g v r := exists2 a, A a & (carrier a v r). have g_fun : functional_graph g. - move=> v r1 r2 [a [Aa avr1]] [b [Ab bvr2]]. + move=> v r1 r2 [a Aa avr1] [b Ab bvr2]. have [] : Rbool a b \/ Rbool b a by exact: Amax. rewrite /Rbool /RboolP /zornS; case: b Ab bvr2 {Aa}. move => s2 [fs2 _ _ _] /= _ s2vr2 /asboolP ecas2. - by move/ecas2: avr1 => /fs2 /(_ s2vr2). - rewrite /Rbool /RboolP /zornS; case: a Aa avr1 {Ab} => s1 [fs1 _ _ _] /= _ s1vr1 /asboolP ecbs1. - by move/ecbs1: bvr2; apply: fs1. + by move/ecas2: avr1 => /fs2 /(_ s2vr2). + rewrite /Rbool /RboolP /zornS. + case: a Aa avr1 {Ab} => s1 [fs1 _ _ _] /= _ s1vr1 /asboolP ecbs1. + by move/ecbs1: bvr2; apply: fs1. have g_lin : linear_graph g. - move=> v1 v2 l r1 r2 [a1 [Aa1 c1]] [a2 [Aa2 c2]]. - have [/RboolP sc12 | /RboolP sc21] := Amax _ _ Aa1 Aa2. - - have {c1 sc12 Aa1 a1} c1 : carrier a2 v1 r1 by apply: sc12. - exists a2; split=> //; case: a2 {Aa2} c2 c1 => c /= [_ hl _ _] *; exact: hl. - - have {c2 sc21 Aa2 a2} c2 : carrier a1 v2 r2 by apply: sc21. - exists a1; split=> //; case: a1 {Aa1} c2 c1 => c /= [_ hl _ _] *; exact: hl. -have g_majp : le_graph p g by move=> v r [[c [fs1 ls1 ms1 ps1]]] /= [_ /ms1]. + move=> v1 v2 l r1 r2 [a1 Aa1 c1] [a2 Aa2 c2]. + have [/RboolP sc12 | /RboolP sc21] := Amax _ _ Aa1 Aa2. + - have {c1 sc12 Aa1 a1} c1 : carrier a2 v1 r1 by apply: sc12. + by exists a2 => //; case: a2 {Aa2} c2 c1 => c /= [_ hl _ _] *; exact: hl. + - have {c2 sc21 Aa2 a2} c2 : carrier a1 v2 r2 by apply: sc21. + by exists a1 => //; case: a1 {Aa1} c2 c1 => c /= [_ hl _ _] *; exact: hl. +have g_majp : le_graph p g. + by move=> v r [[c/= [fs1 ls1 ms1 ps1]]]/= _ => /ms1. have g_prol : extend_graph g. - move=> *; exists w; split=> //; case: w Aw => [c [_ _ _ hp]] _ //=; exact: hp. - have spec_g : le_extend_graph g by split. + by move=> *; exists w=> //; case: w Aw => [c [_ _ _ hp]] _ //=; exact: hp. +have spec_g : le_extend_graph g by split. pose zg := ZornType spec_g. by exists zg => [a Aa]; apply/RboolP; rewrite /zornS => v r cvr; exists a. Qed. @@ -205,7 +199,7 @@ Hypothesis gP : forall z, zornS g z -> z = g. real line directed by an arbitrary vector v *) Lemma domain_extend (z : zorn_type) v : - exists2 ze : zorn_type, (zornS z ze) & (exists r, (carrier ze) v r). + exists2 ze : zorn_type, zornS z ze & exists r, (carrier ze) v r. Proof. case: (lem (exists r, (carrier z v r))). by case=> r rP; exists z => //; exists r. @@ -213,8 +207,9 @@ case: z => [c [fs1 ls1 ms1 ps1]] /= nzv. have c00 : c 0 0. have <- : phi 0 = 0 by rewrite linear0. by move: ps1; rewrite /extend_graph /= => /(_ 0) /=; rewrite GRing.val0; apply. -have [a aP] : exists a, forall (x : V) (r lambda : R), c x r -> r + lambda * a <= p (x + lambda *: v). - suff [a aP] : exists a, forall (x : V) (r lambda : R), c x r -> 0 < lambda -> +have [a aP] : exists a, forall (x : V) (r lambda : R), c x r -> + r + lambda * a <= p (x + lambda *: v). + suff [a aP] : exists a, forall (x : V) (r lambda : R), c x r -> 0 < lambda -> r + lambda * a <= p (x + lambda *: v) /\ r - lambda * a <= p (x - lambda *: v). exists a=> x r lambda cxr. have {aP} aP := aP _ _ _ cxr. @@ -321,7 +316,6 @@ have [z /gP sgz [r zr]]:= domain_extend g v. by exists r; rewrite -sgz. Qed. - Lemma hb_witness : exists h : V -> R, forall v r, carrier g v r <-> (h v = r). Proof. move: (choice tot_g) => [h hP]; exists h => v r; split; last by move<-. @@ -329,13 +323,12 @@ case: g gP tot_g hP => c /= [fg lg mg pg] => gP' tot_g' hP cvr. by have -> // := fg v r (h v). Qed. - End HBPreparation. End HBPreparation. Section HahnBanach. Import Lingraph. -Import HBPreparation. +Import HBPreparation. (* Now we prove HahnBanach on functions*) (* We consider R a real (=ordered) field with supremum, and V a (left) module on R. We do not make use of the 'vector' interface as the latter enforces @@ -350,7 +343,7 @@ Hypothesis p_cvx : (@convex_function R V [set: V] p). Hypothesis f_bounded_by_p : forall (z : F'), (f z <= p (\val z)). Theorem HahnBanach : exists g : {scalar V}, -(forall x, g x <= p x) /\ (forall (z : F'), g (\val z) = f z). + (forall x, g x <= p x) /\ (forall (z : F'), g (\val z) = f z). Proof. pose graphF (v : V) r := exists2 z : F', v = \val z & r = f z. have [z zmax]:= zornS_ex f_bounded_by_p. @@ -397,7 +390,7 @@ Proof. rewrite /convex_function /conv => l v1 v2 _ _ /=. rewrite [X in (_ <= X)]/conv /= /p. apply: le_trans. - have H : `|l%:num *: v1 + (l%:num).~ *: v2| <= `|l%:num *: v1| + `|(l%:num).~ *: v2|. + have H : `|l%:num *: v1 + (l%:num).~ *: v2| <= `|l%:num *: v1| + `|(l%:num).~ *: v2|. by apply: ler_normD. by apply: (@ler_pM _ _ _ r r _ _ H) => //; apply: ltW. rewrite mulrDl !normrZ -![_ *: _]/(_ * _). @@ -407,19 +400,19 @@ Proof. have majfp : forall z : F', f z <= p (\val z). move => z; rewrite /(p _) ; apply : le_trans; last by []. by apply : ler_norm. - move: (HahnBanach convp majfp) => [g] [majgp F_eqgf] {majfp}. -have ling :(linear (g : V -> R)) by exact:linearP. -have contg: (continuous (g : V -> R)). - move=> x; rewrite /cvgP; apply: (continuousfor0_continuous). +move: (HahnBanach convp majfp) => [g] [majgp F_eqgf] {majfp}. +have ling : linear (g : V -> R) by exact: linearP. +have contg : (continuous (g : V -> R)). + move=> x; rewrite /cvgP; apply: continuousfor0_continuous. apply: bounded_linear_continuous. - exists r; split; first by exact: gtr0_real. + exists r; split; first exact: gtr0_real. move => M m1; rewrite nbhs_ballP; exists 1 => /=; first by []. move => y; rewrite -ball_normE //= sub0r => y1. - rewrite ler_norml; apply/andP. split. - - rewrite lerNl -linearN; apply: (le_trans (majgp (-y))). - by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. + rewrite ler_norml; apply/andP; split. + - rewrite lerNl -linearN; apply: (le_trans (majgp (- y))). + by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW. - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN. - apply: ler_pM; rewrite ?normr_ge0 ?ltW //=. + by apply: ler_pM; rewrite ?normr_ge0 ?ltW. pose Hg := isLinearContinuous.Build _ _ _ _ g ling contg. pose g': {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) Hg. by exists g'. From de8f1638dac4116df129b2b66144d366f2ca0c31 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 15 Apr 2026 16:10:41 +0900 Subject: [PATCH 03/21] definition of sub normed module --- theories/hahn_banach_theorem.v | 103 +++++++++++++++++++++------------ 1 file changed, 66 insertions(+), 37 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index cc899eaf0..5580a82c0 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -64,6 +64,41 @@ Qed. End pos_quotient. +HB.mixin Record Zmodule_isSubSemiNormed (R : numDomainType) + (M : semiNormedZmodType R) (S : pred M) T & SubType M S T + & Num.NormedZmodule R T := { + norm_valE : forall x, @Num.norm _ M ((val : T -> M) x) = @Num.norm _ T x +}. + +(* TODO: should go to MathComp in numdomain.v *) +#[short(type="subNormedZmodType")] +HB.structure Definition SubNormedZmodule (R : numDomainType) + (V : normedZmodType R) (S : pred V) := + { U of SubChoice V S U & Num.NormedZmodule R U & GRing.SubZmodule V S U + & Zmodule_isSubSemiNormed R V S U & Num.SemiNormedZmodule R U + & Num.SemiNormedZmodule_isPositiveDefinite R U }. + +(* TODO: moved to normed_module.v *) +#[short(type="subNormedModType")] +HB.structure Definition SubNormedModule (R : numDomainType) + (V : normedModType R) (S : pred V) := + { U of SubChoice V S U & NormedModule R U & @GRing.SubLmodule R V S U + & @SubNormedZmodule(*Zmodule_isSubSemiNormed*) R V S U}. + +Section test. +Context {R : numDomainType} {V : normedModType R} {F : pred V} + {S' : subNormedModType F}. + +Check S' : normedModType R. +Check S' : subLmodType F. +Check S' : subNormedZmodType F. +Check S' : normedZmodType R. + +End test. + +(* TODO: defined a factory that takes a sub vector space S of a normed module V + and construct a sub normed module with the induced norm *) + Module Lingraph. Section Lingraphsec. Variables (R : numDomainType) (V : lmodType R). @@ -326,24 +361,24 @@ Qed. End HBPreparation. End HBPreparation. -Section HahnBanach. +(* NB: could go to convex.v *) +Section hahn_banach. Import Lingraph. Import HBPreparation. (* Now we prove HahnBanach on functions*) (* We consider R a real (=ordered) field with supremum, and V a (left) module on R. We do not make use of the 'vector' interface as the latter enforces finite dimension. *) - Variables (R : realType) (V : lmodType R) (F : pred V). Variables (F' : subLmodType F) (f : {linear F' -> R}) (p : V -> R). -Hypothesis p_cvx : (@convex_function R V [set: V] p). +Hypothesis p_cvx : @convex_function R V [set: V] p. Hypothesis f_bounded_by_p : forall (z : F'), (f z <= p (\val z)). -Theorem HahnBanach : exists g : {scalar V}, - (forall x, g x <= p x) /\ (forall (z : F'), g (\val z) = f z). +Theorem hahn_banach_extension : exists g : {scalar V}, + (forall x, g x <= p x) /\ (forall z : F', g (\val z) = f z). Proof. pose graphF (v : V) r := exists2 z : F', v = \val z & r = f z. have [z zmax]:= zornS_ex f_bounded_by_p. @@ -363,44 +398,38 @@ split; last first. by case: z {zmax} gP => [c [_ _ bp _]] /= gP => x; apply: bp; apply/gP. Qed. -End HahnBanach. +End hahn_banach. -Section HBGeom. (*TODO : define on convextvstype once issue #1927 solved*) - +Section hahn_banach_normed. Variable (R : realType) (V : normedModType R) (F : pred V) -(F' : subLmodType F) (f : {linear F' -> R}). - -(* once subnormedspaces are correctly defined replace by -Variable (R : realType) (V : normedModType R) (F : pred V) -(f : {linear_continuous F' -> R}). -*) - -Let setF := [set x : V | exists (z : F'), val z = x]. + (F' : subNormedModType F) (f : {linear_continuous F' -> R}). -Theorem HB_geom_normed : - (exists r , (r > 0 ) /\ (forall (z : F'), (`|f z| ) <= `|(val z)| * r)) -> -(* hypothesis to delete once f is of type {linear_continuous _ -> _ } - and obtain through continuous_linear_bounded *) - exists g: {linear_continuous V -> R}, (forall x, (g (val x) = f x)). +Theorem hahn_banach_extension_normed : + exists g : {linear_continuous V -> R}, (forall x, (g (val x) = f x)). Proof. - move=> [r [ltr0 fxrx]]. - pose p:= fun x : V => `|x|*r. - have convp: (@convex_function _ _ [set: V] p). - rewrite /convex_function /conv => l v1 v2 _ _ /=. - rewrite [X in (_ <= X)]/conv /= /p. - apply: le_trans. - have H : `|l%:num *: v1 + (l%:num).~ *: v2| <= `|l%:num *: v1| + `|(l%:num).~ *: v2|. - by apply: ler_normD. - by apply: (@ler_pM _ _ _ r r _ _ H) => //; apply: ltW. +have [r [ltr0 fxrx]] : exists2 r, r > 0 & forall (z : F'), `|f z| <= `|val z| * r. + suff: \forall r \near +oo, forall x : F', `|f x| <= r * `|x|. + move=> [t [_ tf]]. + exists (`|t| + 1); first by rewrite ltr_wpDl. + by move=> z; rewrite mulrC norm_valE tf// (le_lt_trans (ler_norm _))// ltrDl. + exact/linear_boundedP/continuous_linear_bounded/cts_fun. +pose p := fun x : V => `|x| * r. +have convp : @convex_function _ _ [set: V] p. + rewrite /convex_function /conv => l v1 v2 _ _ /=. + rewrite [X in (_ <= X)]/conv /= /p. + apply: le_trans. + have H : `|l%:num *: v1 + (l%:num).~ *: v2| <= `|l%:num *: v1| + `|l%:num.~ *: v2|. + exact: ler_normD. + by apply: (@ler_pM _ _ _ r r _ _ H) => //; apply: ltW. rewrite mulrDl !normrZ -![_ *: _]/(_ * _). have -> : `|l%:num| = l%:num by apply/normr_idP. - have -> : `|(l%:num).~| = (l%:num).~ by apply/normr_idP; apply: onem_ge0. + have -> : `|l%:num.~| = l%:num.~ by apply/normr_idP; apply: onem_ge0. by rewrite !mulrA. - have majfp : forall z : F', f z <= p (\val z). - move => z; rewrite /(p _) ; apply : le_trans; last by []. - by apply : ler_norm. -move: (HahnBanach convp majfp) => [g] [majgp F_eqgf] {majfp}. +have majfp : forall z : F', f z <= p (\val z). + move => z; rewrite /(p _) ; apply : le_trans; last by []. + exact: ler_norm. +have [g [majgp F_eqgf {majfp}]] := hahn_banach_extension convp majfp. have ling : linear (g : V -> R) by exact: linearP. have contg : (continuous (g : V -> R)). move=> x; rewrite /cvgP; apply: continuousfor0_continuous. @@ -411,11 +440,11 @@ have contg : (continuous (g : V -> R)). rewrite ler_norml; apply/andP; split. - rewrite lerNl -linearN; apply: (le_trans (majgp (- y))). by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW. - - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN. + - apply: (le_trans (majgp y)); rewrite /p -[X in _ <= X]mul1r -normrN. by apply: ler_pM; rewrite ?normr_ge0 ?ltW. pose Hg := isLinearContinuous.Build _ _ _ _ g ling contg. pose g': {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) Hg. by exists g'. Qed. -End HBGeom. +End hahn_banach_normed. From 6176e3e51a45c0c9a06c100b59c22704fdbfd497 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 15 Apr 2026 16:26:18 +0900 Subject: [PATCH 04/21] todo todo --- theories/hahn_banach_theorem.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 5580a82c0..3d5a23706 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -401,6 +401,10 @@ Qed. End hahn_banach. (*TODO : define on convextvstype once issue #1927 solved*) +(* OR *) +(* TODO : to define on tvs, characterize the topology of a tvs via its pseudonorms, +and the continuity of linear continuous functions via the pseudonorms. *) + Section hahn_banach_normed. Variable (R : realType) (V : normedModType R) (F : pred V) (F' : subNormedModType F) (f : {linear_continuous F' -> R}). From 72019151dcadc96272233d824104a66811d38a0a Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 17 Apr 2026 11:30:43 +0900 Subject: [PATCH 05/21] subNormedModType factory --- theories/hahn_banach_theorem.v | 58 ++++++++++++++++++++++++++++++---- 1 file changed, 51 insertions(+), 7 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 3d5a23706..b2fb1c130 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -64,10 +64,10 @@ Qed. End pos_quotient. -HB.mixin Record Zmodule_isSubSemiNormed (R : numDomainType) - (M : semiNormedZmodType R) (S : pred M) T & SubType M S T +HB.mixin Record Zmodule_isSubNormed (R : numDomainType) + (M : normedZmodType R) (S : pred M) T & SubType M S T & Num.NormedZmodule R T := { - norm_valE : forall x, @Num.norm _ M ((val : T -> M) x) = @Num.norm _ T x + norm_valE : forall x , @Num.norm _ M ((val : T -> M) x) = @Num.norm _ T x }. (* TODO: should go to MathComp in numdomain.v *) @@ -75,8 +75,7 @@ HB.mixin Record Zmodule_isSubSemiNormed (R : numDomainType) HB.structure Definition SubNormedZmodule (R : numDomainType) (V : normedZmodType R) (S : pred V) := { U of SubChoice V S U & Num.NormedZmodule R U & GRing.SubZmodule V S U - & Zmodule_isSubSemiNormed R V S U & Num.SemiNormedZmodule R U - & Num.SemiNormedZmodule_isPositiveDefinite R U }. + & Zmodule_isSubNormed R V S U }. (* TODO: moved to normed_module.v *) #[short(type="subNormedModType")] @@ -96,8 +95,53 @@ Check S' : normedZmodType R. End test. -(* TODO: defined a factory that takes a sub vector space S of a normed module V - and construct a sub normed module with the induced norm *) +HB.factory Record SubLmodule_isSubNormedmodule (R : numFieldType) + (V : normedModType R) (S : pred V) U & SubChoice V S U & @GRing.SubLmodule R V S U := { +}. + +HB.builders Context R V S U & SubLmodule_isSubNormedmodule R V S U. + +Local Definition normu := fun (u : U)=> `|\val u|. + +#[local] Lemma ler_normuD (x y :U): normu (x + y) <= normu x + normu y. +Proof. +by rewrite /normu GRing.valD; exact: ler_normD. +Qed. + +#[local] Lemma normru0_eq0 x: normu x = 0 -> x = 0. +Proof. +move/eqP; rewrite normr_eq0 /normu -(@GRing.val0 V S U) =>/eqP. +by exact: val_inj. +Qed. + +#[local] Lemma normruMn x n: normu (x *+ n) = normu x *+ n. +Proof. +by rewrite /normu raddfMn /=; exact: normrMn. +Qed. + +#[local] Lemma normruN x: normu (- x) = normu x. +Proof. +by rewrite /normu raddfN /=; exact: normrN. +Qed. + +#[local] Lemma normruZ (l : R) (x : U): normu (l *: x) = `|l| * normu x. +Proof. +by rewrite /normu GRing.valZ; exact: normrZ. +Qed. + +HB.instance Definition _ := + @Lmodule_isNormed.Build R U normu ler_normuD normruZ normru0_eq0. + +HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R U erefl. + + +HB.instance Definition _ := + @Lmodule_isNormed.Build R U normu ler_normuD normruZ normru0_eq0. +(* NB : when defining intermediate instances first, via +Zmodule_isSubNormed.Build and @Num.Zmodule_isNormed.Build, this command check +but then we have Fail Check (U : pseudometricnormedzmodtype R) and Fail Check (U +: normedModtype R) *). +HB.end. Module Lingraph. Section Lingraphsec. From 6828184bdb0a30c669b170db8ecfb497f1ce33e4 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 17 Apr 2026 12:05:56 +0900 Subject: [PATCH 06/21] subNormedModType --- theories/hahn_banach_theorem.v | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index b2fb1c130..b3c4632e1 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -134,15 +134,26 @@ HB.instance Definition _ := HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R U erefl. - HB.instance Definition _ := @Lmodule_isNormed.Build R U normu ler_normuD normruZ normru0_eq0. -(* NB : when defining intermediate instances first, via -Zmodule_isSubNormed.Build and @Num.Zmodule_isNormed.Build, this command check +(* NB : when defining intermediate instances first, via @Num.Zmodule_isNormed.Build, this command check but then we have Fail Check (U : pseudometricnormedzmodtype R) and Fail Check (U -: normedModtype R) *). +: normedModtype R). + *) +Check (U : normedModType R). + +#[local] Lemma normu_valE : forall x, @Num.norm _ V ((val : U -> V) x) = @Num.norm _ U x. +Proof. by []. Qed. + +HB.instance Definition _ := Zmodule_isSubNormed.Build _ _ _ U normu_valE. +(* TODO : why is the U necessary ?*) + +Check (U : subNormedZmodType S). +Check (U : subNormedModType S). + HB.end. + Module Lingraph. Section Lingraphsec. Variables (R : numDomainType) (V : lmodType R). @@ -444,8 +455,6 @@ Qed. End hahn_banach. -(*TODO : define on convextvstype once issue #1927 solved*) -(* OR *) (* TODO : to define on tvs, characterize the topology of a tvs via its pseudonorms, and the continuity of linear continuous functions via the pseudonorms. *) @@ -453,6 +462,9 @@ Section hahn_banach_normed. Variable (R : realType) (V : normedModType R) (F : pred V) (F' : subNormedModType F) (f : {linear_continuous F' -> R}). + +(*To use the thm on a F': subLmodType F, use @SubLmodule_isSubNormedmodule.Build. +TODO : a lightweight factory *) Theorem hahn_banach_extension_normed : exists g : {linear_continuous V -> R}, (forall x, (g (val x) = f x)). Proof. From dc4c7fc3d96a2d9ccbfcf781584930be9e0eb6db Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 17 Apr 2026 15:12:10 +0900 Subject: [PATCH 07/21] fail subconvextvs --- theories/hahn_banach_theorem.v | 124 ++++++++++++++++++++++++++++----- 1 file changed, 108 insertions(+), 16 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index b3c4632e1..c4fbe2f36 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -1,4 +1,4 @@ -From HB Require Import structures. +From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. From mathcomp Require Import interval_inference. From mathcomp Require Import unstable wochoice boolp classical_sets topology reals. @@ -75,25 +75,117 @@ HB.mixin Record Zmodule_isSubNormed (R : numDomainType) HB.structure Definition SubNormedZmodule (R : numDomainType) (V : normedZmodType R) (S : pred V) := { U of SubChoice V S U & Num.NormedZmodule R U & GRing.SubZmodule V S U - & Zmodule_isSubNormed R V S U }. + & Zmodule_isSubNormed R V S U }. + + + +HB.mixin Record isSubConvexTvs (R : numDomainType) + (V : convexTvsType R) (S : pred V) U & SubType V S U +& @GRing.SubLmodule R V S U + & ConvexTvs R U := { + continuous_valE : continuous (val : U -> V) +}. + +#[short(type="subConvexTvsType")] +HB.structure Definition SubConvexTvs (R : numDomainType) + (V : convexTvsType R) (S : pred V) := + { U of SubChoice V S U & ConvexTvs R U & @GRing.SubLmodule R V S U + & isSubConvexTvs R V S U}. + +HB.factory Record SubLmodule_isSubConvexTvs (R : numFieldType) + (V : convexTvsType R) (S : pred V) U & SubChoice V S U & @GRing.SubLmodule R V S U := { +}. + +HB.builders Context (R : numFieldType) (V : convexTvsType R) (S : pred V) U + & SubLmodule_isSubConvexTvs R V S U. + +#[local] Definition topU : Type := (initial_topology (\val : U -> V)). + +(*Because there is a new identificator, we need to redefine Topological. +When unifying, if it does not work immedialty, initial_topology will be unfolded *) +(*HB.instance Definition _ := Topological.on topU.*) +HB.instance Definition _ := SubChoice.on topU. +HB.instance Definition _ := Uniform.on topU. +HB.instance Definition _ := GRing.Lmodule.on topU. +Check (topU : SubChoice.type S). +Check (topU : uniformType). +Check (topU : topologicalType). +Check (topU : lmodType R). +Check (topU : preTopologicalLmodType R). +Check (topU : subLmodType S). + +#[local] Lemma add_sub: continuous (fun x : topU * topU => x.1 + x.2). Admitted. + +HB.instance Definition _ := @PreTopologicalNmodule_isTopologicalNmodule.Build topU add_sub. + +Check (topU : TopologicalNmodule.type). + +#[local] Lemma opp_sub : continuous (-%R : topU -> topU). Admitted. + +HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build topU opp_sub. + +Check (topU : TopologicalZmodule.type). + +#[local] Lemma scale_sub : continuous (fun z : R^o * topU => z.1 *: z.2). Admitted. + +HB.instance Definition _ := TopologicalZmodule_isTopologicalLmodule.Build R topU scale_sub. + +Check (topU : TopologicalLmodule.type R). + +#[local] Lemma add_unif_sub: unif_continuous (fun x : topU * topU => x.1 + x.2). Admitted. + +HB.instance Definition _ := @PreUniformNmodule_isUniformNmodule.Build topU add_unif_sub. + +Check (topU : UniformNmodule.type). + +#[local] Lemma opp_unif_sub : unif_continuous (-%R : topU -> topU). Admitted. + +HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build topU opp_unif_sub. + +Check (topU : UniformZmodule.type). + +#[local] Lemma scale_unif_sub : unif_continuous (fun z : R^o * topU => z.1 *: z.2). Admitted. + +HB.instance Definition _ := @UniformNmodule_isUniformLmodule.Build R topU scale_unif_sub. + +Check (topU : UniformLmodule.type R). + +#[local] Lemma locally_convex_sub : exists2 B : set_system topU, + (forall b, b \in B -> convex_set b) & basis B. Admitted. + +HB.instance Definition _ := @Uniform_isConvexTvs.Build R topU locally_convex_sub. + + +(*Can't use that ? Maybe because we already have a uniform structure defined by initial_topology *) +(*HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R topU + add_sub scale_sub locally_convex_sub. + + *) +(* Maybe this is enough instead of all the Top/Unif N/Z/Mlomd *) + +#[loca] Lemma continuous_valE : continuous (val : topU -> V). Admitted. + +HB.instance Definition _ := isSubConvexTvs.Build R V S topU continuous_valE. + +Check (topU : SubType.type S). +Check (topU : @GRing.SubLmodule.type R V S). +Check (topU : NbhsZmodule.type). +Check (topU : ConvexTvs.type R). +Check (topU : SubChoice.type S). +Check (topU : PreUniformLmodule.type R). +Check (topU : UniformLmodule.type R). +Check (topU : topologicalZmodType). +HB.about subConvexTvsType. + +Fail Check (topU : subConvexTvsType S). +HB.end. (* TODO: moved to normed_module.v *) #[short(type="subNormedModType")] HB.structure Definition SubNormedModule (R : numDomainType) (V : normedModType R) (S : pred V) := { U of SubChoice V S U & NormedModule R U & @GRing.SubLmodule R V S U - & @SubNormedZmodule(*Zmodule_isSubSemiNormed*) R V S U}. - -Section test. -Context {R : numDomainType} {V : normedModType R} {F : pred V} - {S' : subNormedModType F}. - -Check S' : normedModType R. -Check S' : subLmodType F. -Check S' : subNormedZmodType F. -Check S' : normedZmodType R. - -End test. + & @SubNormedZmodule(*Zmodule_isSubSemiNormed*) R V S U & @SubConvexTvs R V S U}. HB.factory Record SubLmodule_isSubNormedmodule (R : numFieldType) (V : normedModType R) (S : pred V) U & SubChoice V S U & @GRing.SubLmodule R V S U := { @@ -144,13 +236,13 @@ Check (U : normedModType R). #[local] Lemma normu_valE : forall x, @Num.norm _ V ((val : U -> V) x) = @Num.norm _ U x. Proof. by []. Qed. - + HB.instance Definition _ := Zmodule_isSubNormed.Build _ _ _ U normu_valE. (* TODO : why is the U necessary ?*) Check (U : subNormedZmodType S). Check (U : subNormedModType S). - +(* TODO : to a lightweight factory to put an instanec of subNormedModType on every subLmodtype *) HB.end. From 853f6d6897c72ae125b7ab4e26cb979dc9ac5475 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sun, 19 Apr 2026 22:40:51 +0900 Subject: [PATCH 08/21] clean --- theories/hahn_banach_theorem.v | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index c4fbe2f36..decd6f526 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -91,7 +91,7 @@ HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) (S : pred V) := { U of SubChoice V S U & ConvexTvs R U & @GRing.SubLmodule R V S U & isSubConvexTvs R V S U}. - +(* HB.factory Record SubLmodule_isSubConvexTvs (R : numFieldType) (V : convexTvsType R) (S : pred V) U & SubChoice V S U & @GRing.SubLmodule R V S U := { }. @@ -153,7 +153,7 @@ Check (topU : UniformLmodule.type R). #[local] Lemma locally_convex_sub : exists2 B : set_system topU, (forall b, b \in B -> convex_set b) & basis B. Admitted. -HB.instance Definition _ := @Uniform_isConvexTvs.Build R topU locally_convex_sub. +HB.instance Definition _ := @Uniform_isConvexTvs.Build R topU locally_convex_sub. (*Can't use that ? Maybe because we already have a uniform structure defined by initial_topology *) @@ -176,9 +176,8 @@ Check (topU : PreUniformLmodule.type R). Check (topU : UniformLmodule.type R). Check (topU : topologicalZmodType). HB.about subConvexTvsType. - Fail Check (topU : subConvexTvsType S). -HB.end. +HB.end.*) (* TODO: moved to normed_module.v *) #[short(type="subNormedModType")] @@ -236,15 +235,24 @@ Check (U : normedModType R). #[local] Lemma normu_valE : forall x, @Num.norm _ V ((val : U -> V) x) = @Num.norm _ U x. Proof. by []. Qed. - + HB.instance Definition _ := Zmodule_isSubNormed.Build _ _ _ U normu_valE. (* TODO : why is the U necessary ?*) Check (U : subNormedZmodType S). + +#[local] Lemma continuous_valE : continuous (val : U -> V). Admitted. + +HB.instance Definition _ := isSubConvexTvs.Build _ _ _ U continuous_valE. + +Check (U : subConvexTvsType S). + Check (U : subNormedModType S). -(* TODO : to a lightweight factory to put an instanec of subNormedModType on every subLmodtype *) + +HB.instance Definition _ := SubLmodule_isSubNormedmodule.Build _ _ _ U. HB.end. +(* TODO : use a lightweight factory to make every subLmodType a subnormedmodtype *) Module Lingraph. Section Lingraphsec. From 6d5419ef7143403d9b08e2ad85f444b5f71eebcb Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 21 Apr 2026 12:19:15 +0900 Subject: [PATCH 09/21] filter by hand (still broken) --- theories/hahn_banach_theorem.v | 76 ++++++++++++++++++++++++++++++---- 1 file changed, 68 insertions(+), 8 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index decd6f526..e39aff082 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -91,12 +91,47 @@ HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) (S : pred V) := { U of SubChoice V S U & ConvexTvs R U & @GRing.SubLmodule R V S U & isSubConvexTvs R V S U}. -(* -HB.factory Record SubLmodule_isSubConvexTvs (R : numFieldType) + +Lemma myfilter {R : realFieldType} (U : normedZmodType R) x : Filter + [set P | (exists2 i : set (pseudoMetric_normed U * pseudoMetric_normed U), + pseudoMetric_from_normedZmodType.ent i & xsection i x `<=` P)]. +Proof. +apply: Build_Filter => /=. +- exists setT. + have := @entourageT (pseudoMetric_normed U). + exact. + by []. +- move=> A B/= [A' entA' A'A] [B' entB' B'B]. + exists (A' `&` B') => //. + Import pseudoMetric_from_normedZmodType. + rewrite entourageE. + rewrite /entourage_. + case: entA' => r/= r0 HA'. + case: entB' => d/= d0 HB'. + exists (Num.min r d) => /=. + by rewrite lt_min r0. + move=> z/= Hz. + split. + apply: HA' => /=. + do 3 red. + rewrite (lt_le_trans Hz)//. + by rewrite ge_min lexx. + apply: HB' => /=. + do 3 red. + rewrite (lt_le_trans Hz)//. + by rewrite ge_min lexx orbT. + by rewrite xsectionI; apply: setISS. +- move=> P Q PQ [A entA AP]. + exists A => //. + exact: (subset_trans AP). +Qed. + +HB.factory Record SubLmodule_isSubConvexTvs (R : realFieldType) (V : convexTvsType R) (S : pred V) U & SubChoice V S U & @GRing.SubLmodule R V S U := { }. -HB.builders Context (R : numFieldType) (V : convexTvsType R) (S : pred V) U +(* +HB.builders Context (R : realFieldType) (V : convexTvsType R) (S : pred V) U & SubLmodule_isSubConvexTvs R V S U. #[local] Definition topU : Type := (initial_topology (\val : U -> V)). @@ -106,6 +141,8 @@ When unifying, if it does not work immedialty, initial_topology will be unfolded (*HB.instance Definition _ := Topological.on topU.*) HB.instance Definition _ := SubChoice.on topU. HB.instance Definition _ := Uniform.on topU. +HB.instance Definition _ := Topological.on topU. +HB.instance Definition _ := Nbhs.on topU. HB.instance Definition _ := GRing.Lmodule.on topU. Check (topU : SubChoice.type S). Check (topU : uniformType). @@ -114,7 +151,8 @@ Check (topU : lmodType R). Check (topU : preTopologicalLmodType R). Check (topU : subLmodType S). -#[local] Lemma add_sub: continuous (fun x : topU * topU => x.1 + x.2). Admitted. +#[local] Lemma add_sub: continuous (fun x : topU * topU => x.1 + x.2). +Proof. Admitted. HB.instance Definition _ := @PreTopologicalNmodule_isTopologicalNmodule.Build topU add_sub. @@ -163,7 +201,8 @@ HB.instance Definition _ := @Uniform_isConvexTvs.Build R topU locally_convex_sub *) (* Maybe this is enough instead of all the Top/Unif N/Z/Mlomd *) -#[loca] Lemma continuous_valE : continuous (val : topU -> V). Admitted. +#[local] Lemma continuous_valE : continuous (val : topU -> V). +Proof. exact: initial_continuous. Qed. HB.instance Definition _ := isSubConvexTvs.Build R V S topU continuous_valE. @@ -175,9 +214,15 @@ Check (topU : SubChoice.type S). Check (topU : PreUniformLmodule.type R). Check (topU : UniformLmodule.type R). Check (topU : topologicalZmodType). +Check (topU : uniformType). HB.about subConvexTvsType. Fail Check (topU : subConvexTvsType S). -HB.end.*) + + +Fail HB.end. +*) + + (* TODO: moved to normed_module.v *) #[short(type="subNormedModType")] @@ -186,7 +231,7 @@ HB.structure Definition SubNormedModule (R : numDomainType) { U of SubChoice V S U & NormedModule R U & @GRing.SubLmodule R V S U & @SubNormedZmodule(*Zmodule_isSubSemiNormed*) R V S U & @SubConvexTvs R V S U}. -HB.factory Record SubLmodule_isSubNormedmodule (R : numFieldType) +HB.factory Record SubLmodule_isSubNormedmodule (R : realFieldType) (V : normedModType R) (S : pred V) U & SubChoice V S U & @GRing.SubLmodule R V S U := { }. @@ -241,7 +286,22 @@ HB.instance Definition _ := Zmodule_isSubNormed.Build _ _ _ U normu_valE. Check (U : subNormedZmodType S). -#[local] Lemma continuous_valE : continuous (val : U -> V). Admitted. +#[local] Lemma continuous_valE : continuous (val : U -> V). +Proof. +move=> /= x. +red. +set rhs := (X in _ --> X). +apply/cvgrPdist_le => //=. + by apply: myfilter. +move=> e e0. +near=> t. +rewrite -GRing.valN. +rewrite -GRing.valD. +rewrite norm_valE. +near: t. +move: e e0. +by apply/cvgrPdist_le. +Unshelve. all: by end_near. Qed. HB.instance Definition _ := isSubConvexTvs.Build _ _ _ U continuous_valE. From 55ba0cb1e54d595adc41c3b6826d61c9fd53d6df Mon Sep 17 00:00:00 2001 From: mkerjean Date: Tue, 21 Apr 2026 14:26:10 +0900 Subject: [PATCH 10/21] instances instead of factories --- theories/hahn_banach_theorem.v | 172 ++++++++++++++++++++++++--------- 1 file changed, 129 insertions(+), 43 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index e39aff082..b8121bd52 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -78,59 +78,106 @@ HB.structure Definition SubNormedZmodule (R : numDomainType) & Zmodule_isSubNormed R V S U }. - -HB.mixin Record isSubConvexTvs (R : numDomainType) - (V : convexTvsType R) (S : pred V) U & SubType V S U -& @GRing.SubLmodule R V S U - & ConvexTvs R U := { +HB.mixin Record isSubNbhs + (V : nbhsType) (S : pred V) U & SubType 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}. + + + +#[short(type="subTopologicalType")] +HB.structure Definition SubTopological + (V : topologicalType) (S : pred V) := + { U of SubNbhs V S U & Topological U}. + + +Definition topU (V : Type) (S : pred V) (U : subType S) : Type + := (initial_topology (\val : U -> V)). + +Section SubType_isSubTopological. +Context (V : topologicalType) (S : pred V) (U : subChoiceType S). + +Notation topU := (topU U). +HB.instance Definition _ := SubChoice.on topU. +HB.instance Definition _ := Nbhs.on topU. +HB.instance Definition _ := Topological.on topU. + +#[local] Lemma top_continuous_valE : continuous (val : topU -> V). +Proof. exact: initial_continuous. Qed. + +HB.instance Definition _ := @isSubNbhs.Build V S topU top_continuous_valE. + +Check (topU : topologicalType). +Check (topU : subNbhsType S). +Check (topU : subTopologicalType S). + +End SubType_isSubTopological. + #[short(type="subConvexTvsType")] HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) (S : pred V) := - { U of SubChoice V S U & ConvexTvs R U & @GRing.SubLmodule R V S U - & isSubConvexTvs R V S U}. + { U of SubTopological V S U & ConvexTvs R U & @GRing.SubLmodule R V S U + }. -Lemma myfilter {R : realFieldType} (U : normedZmodType R) x : Filter - [set P | (exists2 i : set (pseudoMetric_normed U * pseudoMetric_normed U), - pseudoMetric_from_normedZmodType.ent i & xsection i x `<=` P)]. -Proof. -apply: Build_Filter => /=. -- exists setT. - have := @entourageT (pseudoMetric_normed U). - exact. - by []. -- move=> A B/= [A' entA' A'A] [B' entB' B'B]. - exists (A' `&` B') => //. - Import pseudoMetric_from_normedZmodType. - rewrite entourageE. - rewrite /entourage_. - case: entA' => r/= r0 HA'. - case: entB' => d/= d0 HB'. - exists (Num.min r d) => /=. - by rewrite lt_min r0. - move=> z/= Hz. - split. - apply: HA' => /=. - do 3 red. - rewrite (lt_le_trans Hz)//. - by rewrite ge_min lexx. - apply: HB' => /=. - do 3 red. - rewrite (lt_le_trans Hz)//. - by rewrite ge_min lexx orbT. - by rewrite xsectionI; apply: setISS. -- move=> P Q PQ [A entA AP]. - exists A => //. - exact: (subset_trans AP). -Qed. +Section lmodule_isSubTvs. +Context (R : numFieldType) (V : convexTvsType R) (S : pred V) (U: subLmodType S). + +Notation topU := (topU U). +HB.instance Definition _ := SubChoice.on topU. +HB.instance Definition _ := Nbhs.on topU. +HB.instance Definition _ := Topological.on topU. +HB.instance Definition _ := Uniform.on topU. +HB.instance Definition _ := GRing.Lmodule.on topU. + +Check (topU : subLmodType S). + +#[local] Lemma add_sub: continuous (fun x : topU * topU => x.1 + x.2). +Proof. Admitted. + +HB.instance Definition _ := @PreTopologicalNmodule_isTopologicalNmodule.Build topU add_sub. + +Check (topU : TopologicalNmodule.type). + +#[local] Lemma opp_sub : continuous (-%R : topU -> topU). Admitted. + +HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build topU opp_sub. + +Check (topU : TopologicalZmodule.type). + +#[local] Lemma scale_sub : continuous (fun z : R^o * topU => z.1 *: z.2). Admitted. + +HB.instance Definition _ := TopologicalZmodule_isTopologicalLmodule.Build R topU scale_sub. + +Check (topU : TopologicalLmodule.type R). + +#[local] Lemma locally_convex_sub : exists2 B : set_system topU, + (forall b, b \in B -> convex_set b) & basis B. Admitted. + +HB.instance Definition _ := @Uniform_isConvexTvs.Build R topU locally_convex_sub. + + +(*HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R topU + add_sub scale_sub locally_convex_sub. *) +(* Does not work. why ?*) + +Check (topU : convexTvsType R). +Check (topU : subTopologicalType S). +Check (topU : subLmodType S). +Fail Check (topU : subConvexTvsType S). +End lmodule_isSubTvs. +(* HB.factory Record SubLmodule_isSubConvexTvs (R : realFieldType) (V : convexTvsType R) (S : pred V) U & SubChoice V S U & @GRing.SubLmodule R V S U := { }. -(* + HB.builders Context (R : realFieldType) (V : convexTvsType R) (S : pred V) U & SubLmodule_isSubConvexTvs R V S U. @@ -144,7 +191,8 @@ HB.instance Definition _ := Uniform.on topU. HB.instance Definition _ := Topological.on topU. HB.instance Definition _ := Nbhs.on topU. HB.instance Definition _ := GRing.Lmodule.on topU. -Check (topU : SubChoice.type S). +Check (topU : SubChoice.type S). +Check (topU : pointedType). Check (topU : uniformType). Check (topU : topologicalType). Check (topU : lmodType R). @@ -231,6 +279,44 @@ HB.structure Definition SubNormedModule (R : numDomainType) { U of SubChoice V S U & NormedModule R U & @GRing.SubLmodule R V S U & @SubNormedZmodule(*Zmodule_isSubSemiNormed*) R V S U & @SubConvexTvs R V S U}. + + +Lemma myfilter {R : realFieldType} (U : normedZmodType R) x : Filter + [set P | (exists2 i : set (pseudoMetric_normed U * pseudoMetric_normed U), + pseudoMetric_from_normedZmodType.ent i & xsection i x `<=` P)]. +Proof. +apply: Build_Filter => /=. +- exists setT. + have := @entourageT (pseudoMetric_normed U). + exact. + by []. +- move=> A B/= [A' entA' A'A] [B' entB' B'B]. + exists (A' `&` B') => //. + Import pseudoMetric_from_normedZmodType. + rewrite entourageE. + rewrite /entourage_. + case: entA' => r/= r0 HA'. + case: entB' => d/= d0 HB'. + exists (Num.min r d) => /=. + by rewrite lt_min r0. + move=> z/= Hz. + split. + apply: HA' => /=. + do 3 red. + rewrite (lt_le_trans Hz)//. + by rewrite ge_min lexx. + apply: HB' => /=. + do 3 red. + rewrite (lt_le_trans Hz)//. + by rewrite ge_min lexx orbT. + by rewrite xsectionI; apply: setISS. +- move=> P Q PQ [A entA AP]. + exists A => //. + exact: (subset_trans AP). +Qed. + + + HB.factory Record SubLmodule_isSubNormedmodule (R : realFieldType) (V : normedModType R) (S : pred V) U & SubChoice V S U & @GRing.SubLmodule R V S U := { }. @@ -303,7 +389,7 @@ move: e e0. by apply/cvgrPdist_le. Unshelve. all: by end_near. Qed. -HB.instance Definition _ := isSubConvexTvs.Build _ _ _ U continuous_valE. +HB.instance Definition _ := isSubNbhs.Build _ _ U continuous_valE. Check (U : subConvexTvsType S). From 47bde9d77603b8d12ae91a1f4436bb7726f29b58 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 21 Apr 2026 14:52:45 +0900 Subject: [PATCH 11/21] subConvexTvsType at last --- theories/hahn_banach_theorem.v | 66 ++++++++++++++++++---------------- 1 file changed, 36 insertions(+), 30 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index b8121bd52..27fddf011 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -65,7 +65,7 @@ Qed. End pos_quotient. HB.mixin Record Zmodule_isSubNormed (R : numDomainType) - (M : normedZmodType R) (S : pred M) T & SubType M S T + (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 }. @@ -77,27 +77,30 @@ HB.structure Definition SubNormedZmodule (R : numDomainType) { U of SubChoice V S U & Num.NormedZmodule R U & GRing.SubZmodule V S U & Zmodule_isSubNormed R V S U }. - HB.mixin Record isSubNbhs - (V : nbhsType) (S : pred V) U & SubType V S U & Nbhs U := { + (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}. - - +HB.structure Definition SubNbhs (V : nbhsType) (S : pred V) := + { U of SubChoice V S U & Nbhs U & isSubNbhs V S U}. -#[short(type="subTopologicalType")] -HB.structure Definition SubTopological - (V : topologicalType) (S : pred V) := +(*#[short(type="subTopologicalType")] +HB.structure Definition SubTopological (V : topologicalType) (S : pred V) := { U of SubNbhs V S U & Topological U}. +#[short(type="subUniformType")] +HB.structure Definition SubUniform (V : uniformType) (S : pred V) := + { U of SubTopological V S U & Uniform U}.*) + +#[short(type="subConvexTvsType")] +HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) + (S : pred V) := { + U of SubNbhs V S U & ConvexTvs R U & @GRing.SubLmodule R V S U + }. -Definition topU (V : Type) (S : pred V) (U : subType S) : Type +Definition topU (V : Type) (S : pred V) (U : subChoiceType S) : Type := (initial_topology (\val : U -> V)). Section SubType_isSubTopological. @@ -106,7 +109,6 @@ Context (V : topologicalType) (S : pred V) (U : subChoiceType S). Notation topU := (topU U). HB.instance Definition _ := SubChoice.on topU. HB.instance Definition _ := Nbhs.on topU. -HB.instance Definition _ := Topological.on topU. #[local] Lemma top_continuous_valE : continuous (val : topU -> V). Proof. exact: initial_continuous. Qed. @@ -115,28 +117,28 @@ HB.instance Definition _ := @isSubNbhs.Build V S topU top_continuous_valE. Check (topU : topologicalType). Check (topU : subNbhsType S). -Check (topU : subTopologicalType S). End SubType_isSubTopological. -#[short(type="subConvexTvsType")] -HB.structure Definition SubConvexTvs (R : numDomainType) - (V : convexTvsType R) (S : pred V) := - { U of SubTopological V S U & ConvexTvs R U & @GRing.SubLmodule R V S U - }. - - Section lmodule_isSubTvs. Context (R : numFieldType) (V : convexTvsType R) (S : pred V) (U: subLmodType S). Notation topU := (topU U). -HB.instance Definition _ := SubChoice.on topU. +Check topU : nbhsType. HB.instance Definition _ := Nbhs.on topU. +Check topU : subChoiceType S. +HB.instance Definition _ := SubChoice.on topU. +Check topU : topologicalType. HB.instance Definition _ := Topological.on topU. +Check topU : subNbhsType S. +HB.instance Definition _ := SubNbhs.on topU. +Check topU : uniformType. HB.instance Definition _ := Uniform.on topU. +Check topU : lmodType R. HB.instance Definition _ := GRing.Lmodule.on topU. -Check (topU : subLmodType S). +Check (topU : uniformType). +Check (topU : subLmodType S). #[local] Lemma add_sub: continuous (fun x : topU * topU => x.1 + x.2). Proof. Admitted. @@ -147,7 +149,7 @@ Check (topU : TopologicalNmodule.type). #[local] Lemma opp_sub : continuous (-%R : topU -> topU). Admitted. -HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build topU opp_sub. +HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build topU opp_sub. Check (topU : TopologicalZmodule.type). @@ -162,15 +164,19 @@ Check (topU : TopologicalLmodule.type R). HB.instance Definition _ := @Uniform_isConvexTvs.Build R topU locally_convex_sub. - -(*HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R topU - add_sub scale_sub locally_convex_sub. *) +HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R topU + add_sub scale_sub locally_convex_sub. (* Does not work. why ?*) Check (topU : convexTvsType R). -Check (topU : subTopologicalType S). + +HB.instance Definition _ := ConvexTvs.on topU. +HB.instance Definition _ := GRing.SubLmodule.on topU. + +Check (topU : convexTvsType R). Check (topU : subLmodType S). -Fail Check (topU : subConvexTvsType S). +Check (topU : subConvexTvsType S). + End lmodule_isSubTvs. (* HB.factory Record SubLmodule_isSubConvexTvs (R : realFieldType) From 9e5316254d97cbf386217bf2e7991f2dda339773 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Tue, 21 Apr 2026 16:48:28 +0900 Subject: [PATCH 12/21] proofs --- theories/hahn_banach_theorem.v | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 27fddf011..c7d0ce7c6 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -120,6 +120,16 @@ Check (topU : subNbhsType S). End SubType_isSubTopological. +#[short(type="subConvexTvsType")] +HB.structure Definition SubConvexTvs (R : numDomainType) + (V : convexTvsType R) (S : pred V) := + { U of SubTopological V S U & ConvexTvs R U & @GRing.SubLmodule R V S U + }. + +(* For lisibility, to be added to tvs.v *) +Lemma add_continuous (K : numDomainType) (E : convexTvsType K) : continuous (fun x : E * E => x.1 + x.2). +Proof. exact: add_continuous. Qed. + Section lmodule_isSubTvs. Context (R : numFieldType) (V : convexTvsType R) (S : pred V) (U: subLmodType S). @@ -136,12 +146,20 @@ Check topU : uniformType. HB.instance Definition _ := Uniform.on topU. Check topU : lmodType R. HB.instance Definition _ := GRing.Lmodule.on topU. - Check (topU : uniformType). Check (topU : subLmodType S). #[local] Lemma add_sub: continuous (fun x : topU * topU => x.1 + x.2). -Proof. Admitted. +Proof. +apply: continuous_comp_initial => xy. +pose h := fun x1x2 : U * U => (\val x1x2.1, \val x1x2.2). +pose g := fun xy : V * V => xy.1 + xy.2. +rewrite (_ : _ \o _ = g \o h)//. +apply: continuous_comp; last by exact: add_continuous. +Check cvg_prod. +admit. +by apply/funext => i/=; rewrite /g /h /= GRing.valD. +Admitted. HB.instance Definition _ := @PreTopologicalNmodule_isTopologicalNmodule.Build topU add_sub. From 4c582a83bfeb5e35595736096f3c898726283c83 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Tue, 21 Apr 2026 21:26:59 +0900 Subject: [PATCH 13/21] proofs --- theories/hahn_banach_theorem.v | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index c7d0ce7c6..459a78055 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -94,10 +94,10 @@ HB.structure Definition SubTopological (V : topologicalType) (S : pred V) := HB.structure Definition SubUniform (V : uniformType) (S : pred V) := { U of SubTopological V S U & Uniform U}.*) -#[short(type="subConvexTvsType")] -HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) +#[short(type="subTopologicalType")] +HB.structure Definition SubTopological (V : topologicalType) (S : pred V) := { - U of SubNbhs V S U & ConvexTvs R U & @GRing.SubLmodule R V S U + U of SubNbhs V S U & Topological U }. Definition topU (V : Type) (S : pred V) (U : subChoiceType S) : Type @@ -109,14 +109,15 @@ Context (V : topologicalType) (S : pred V) (U : subChoiceType S). Notation topU := (topU U). HB.instance Definition _ := SubChoice.on topU. HB.instance Definition _ := Nbhs.on topU. +HB.instance Definition _ := Topological.on topU. #[local] Lemma top_continuous_valE : continuous (val : topU -> V). Proof. exact: initial_continuous. Qed. HB.instance Definition _ := @isSubNbhs.Build V S topU top_continuous_valE. -Check (topU : topologicalType). Check (topU : subNbhsType S). +Check (topU : subTopologicalType S). End SubType_isSubTopological. @@ -156,7 +157,7 @@ pose h := fun x1x2 : U * U => (\val x1x2.1, \val x1x2.2). pose g := fun xy : V * V => xy.1 + xy.2. rewrite (_ : _ \o _ = g \o h)//. apply: continuous_comp; last by exact: add_continuous. -Check cvg_prod. +Check cvg_prod. move => /= A [] /= [] a1 a2 [ /= na1 na2]. admit. by apply/funext => i/=; rewrite /g /h /= GRing.valD. Admitted. From cd5e3af87db3a69d5ccff8ef7cf38ee89a9caa14 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 22 Apr 2026 10:06:21 +0900 Subject: [PATCH 14/21] proofs --- theories/hahn_banach_theorem.v | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 459a78055..cbd87617f 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -152,12 +152,16 @@ Check (topU : subLmodType S). #[local] Lemma add_sub: continuous (fun x : topU * topU => x.1 + x.2). Proof. -apply: continuous_comp_initial => xy. +apply: continuous_comp_initial => - [] /= x /= y. pose h := fun x1x2 : U * U => (\val x1x2.1, \val x1x2.2). pose g := fun xy : V * V => xy.1 + xy.2. rewrite (_ : _ \o _ = g \o h)//. apply: continuous_comp; last by exact: add_continuous. -Check cvg_prod. move => /= A [] /= [] a1 a2 [ /= na1 na2]. +move => /= A [] /= [] a1 a2 [/=]. +move/(continuous_valE (x : topU)) => [na1 /= [] wo1 nax1 val1]. +move/(continuous_valE (y : topU)) => [na2 /= [] wo2 nay2 val2] A12. +apply: filterS; first by exact: A12. +exists (na1, na2); split => //=; admit. by apply/funext => i/=; rewrite /g /h /= GRing.valD. Admitted. From ac1379693bb458bc779b1c840d9f8f07888e92e2 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 22 Apr 2026 20:53:28 +0900 Subject: [PATCH 15/21] proofs --- theories/hahn_banach_theorem.v | 58 ++++++++++++++++++++++++---------- 1 file changed, 42 insertions(+), 16 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index cbd87617f..ba34571bd 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -4,7 +4,7 @@ From mathcomp Require Import interval_inference. From mathcomp Require Import unstable wochoice boolp classical_sets topology reals. From mathcomp Require Import filter reals normedtype convex. Import numFieldNormedType.Exports. -Local Open Scope classical_set_scope. +Local Open Scope classical_set_scope. (**md**************************************************************************) (* # The Hahn-Banach theorem *) @@ -149,46 +149,72 @@ Check topU : lmodType R. HB.instance Definition _ := GRing.Lmodule.on topU. Check (topU : uniformType). Check (topU : subLmodType S). - + #[local] Lemma add_sub: continuous (fun x : topU * topU => x.1 + x.2). Proof. apply: continuous_comp_initial => - [] /= x /= y. pose h := fun x1x2 : U * U => (\val x1x2.1, \val x1x2.2). -pose g := fun xy : V * V => xy.1 + xy.2. +pose g := fun xy : V * V => xy.1 + xy.2. rewrite (_ : _ \o _ = g \o h)//. -apply: continuous_comp; last by exact: add_continuous. -move => /= A [] /= [] a1 a2 [/=]. -move/(continuous_valE (x : topU)) => [na1 /= [] wo1 nax1 val1]. -move/(continuous_valE (y : topU)) => [na2 /= [] wo2 nay2 val2] A12. -apply: filterS; first by exact: A12. -exists (na1, na2); split => //=; -admit. +apply: continuous_comp; last by exact: add_continuous. + move => /= A [] /= [] a1 a2 [/=]. + move/(continuous_valE (x : topU)) => /= [na1 /= [] wo1 nax1 val1]. + move/(continuous_valE (y : topU)) => /= [na2 /= [] wo2 nay2 val2] A12. + apply: filterS; first by exact: A12. + exists (na1, na2); split => //=; first by exists na1; split => //=. + exists na2; split => //=. + - by move: H => /= [H _]; apply: val1. + - by move: H => /= [_ H]; apply: val2. by apply/funext => i/=; rewrite /g /h /= GRing.valD. -Admitted. +Qed. HB.instance Definition _ := @PreTopologicalNmodule_isTopologicalNmodule.Build topU add_sub. Check (topU : TopologicalNmodule.type). -#[local] Lemma opp_sub : continuous (-%R : topU -> topU). Admitted. +#[local] Lemma opp_sub : continuous (-%R : topU -> topU). +Proof. +apply: continuous_comp_initial => x. +rewrite (_ : _ \o _ = (-%R \o \val))//. +apply: continuous_comp; first by exact: continuous_valE. +by exact: opp_continuous. +by apply/funext => i/=; rewrite GRing.valN. +Qed. HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build topU opp_sub. Check (topU : TopologicalZmodule.type). -#[local] Lemma scale_sub : continuous (fun z : R^o * topU => z.1 *: z.2). Admitted. +#[local] Lemma scale_sub : continuous (fun z : R^o * topU => z.1 *: z.2). +Proof. +apply: continuous_comp_initial => - [] /= x /= y. +pose h := fun x1x2 : R * U => (x1x2.1, \val x1x2.2). +pose g := fun xy : R * V => xy.1 *: xy.2. +rewrite (_ : _ \o _ = g \o h)//. +apply: continuous_comp; last by exact: scale_continuous. + move => /= A [] /= [] a1 a2 [/=]. + move=> - [] /= r /= - [] r0 /= br1. + move/(continuous_valE (y : topU)) => /= [na2 /= [] wo2 nay2 val2] A12. + apply: filterS; first by exact: A12. + exists ( ball_ [eta normr] x r ,na2) => //=; split; first by exists r. + exists na2; split => //. + - by apply: br1; move: H => /= [H _]. + - by move: H => /= [_ H]; apply: val2. +by apply/funext => i/=; rewrite /g /h /= GRing.valZ. +Qed. HB.instance Definition _ := TopologicalZmodule_isTopologicalLmodule.Build R topU scale_sub. Check (topU : TopologicalLmodule.type R). #[local] Lemma locally_convex_sub : exists2 B : set_system topU, - (forall b, b \in B -> convex_set b) & basis B. Admitted. + (forall b, b \in B -> convex_set b) & basis B. +Admitted. HB.instance Definition _ := @Uniform_isConvexTvs.Build R topU locally_convex_sub. -HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R topU - add_sub scale_sub locally_convex_sub. +(*HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R topU + add_sub scale_sub locally_convex_sub.*) (* Does not work. why ?*) Check (topU : convexTvsType R). From 5a37d93cd3fc1d7f7396fd4cf1411d1ad867bb96 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 22 Apr 2026 21:58:34 +0900 Subject: [PATCH 16/21] proofs --- theories/hahn_banach_theorem.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index ba34571bd..9e06c2429 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -209,6 +209,18 @@ Check (topU : TopologicalLmodule.type R). #[local] Lemma locally_convex_sub : exists2 B : set_system topU, (forall b, b \in B -> convex_set b) & basis B. +Proof. +move : (@locally_convex R V) => - [] B convexB [] openB /= genB. +exists [set a | B(\val @` a)]. + move=> /= a; rewrite inE /=; rewrite -inE => H /= r s l ra sa. + suff : \val(r <|l|> s) \in \val @` a by rewrite !inE /= => -[] x ax /val_inj <-. + have valr : \val r \in [set \val x | x in a] by rewrite inE => /=; exists r; first by rewrite -inE. + have vals : \val s \in [set \val x | x in a] by rewrite inE => /=; exists s; first by rewrite -inE. + move: (convexB ( [set \val x | x in a] ) H (\val r) (\val s) l valr vals) => /=. + by rewrite !GRing.valD !GRing.valZ //. +split. + move=> /= a. admit. +move => /=. Admitted. HB.instance Definition _ := @Uniform_isConvexTvs.Build R topU locally_convex_sub. From 9e3addfb13ee67a8060c837f66d189e347b4ee7e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 23 Apr 2026 00:48:12 +0900 Subject: [PATCH 17/21] simplification of add_sub --- theories/hahn_banach_theorem.v | 58 ++++++++++++++++------------------ 1 file changed, 27 insertions(+), 31 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 9e06c2429..ee419eace 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -149,36 +149,33 @@ Check topU : lmodType R. HB.instance Definition _ := GRing.Lmodule.on topU. Check (topU : uniformType). Check (topU : subLmodType S). - + #[local] Lemma add_sub: continuous (fun x : topU * topU => x.1 + x.2). -Proof. -apply: continuous_comp_initial => - [] /= x /= y. -pose h := fun x1x2 : U * U => (\val x1x2.1, \val x1x2.2). -pose g := fun xy : V * V => xy.1 + xy.2. -rewrite (_ : _ \o _ = g \o h)//. -apply: continuous_comp; last by exact: add_continuous. - move => /= A [] /= [] a1 a2 [/=]. - move/(continuous_valE (x : topU)) => /= [na1 /= [] wo1 nax1 val1]. - move/(continuous_valE (y : topU)) => /= [na2 /= [] wo2 nay2 val2] A12. - apply: filterS; first by exact: A12. - exists (na1, na2); split => //=; first by exists na1; split => //=. - exists na2; split => //=. - - by move: H => /= [H _]; apply: val1. - - by move: H => /= [_ H]; apply: val2. -by apply/funext => i/=; rewrite /g /h /= GRing.valD. +Proof. +apply: continuous_comp_initial => -[/= x y]. +pose h := fun xy : U * U => (\val xy.1, \val xy.2). +pose g := fun xy : V * V => xy.1 + xy.2. +rewrite (_ : _ \o _ = g \o h); last first. + by apply/funext => i /=; rewrite GRing.valD. +apply: continuous_comp; last exact: add_continuous. +apply: cvg_pair => //=. +- apply: (cvg_comp _ _ cvg_fst). + exact: (continuous_valE (x : topU)). +- apply: (cvg_comp _ _ cvg_snd). + exact: (continuous_valE (y : topU)). Qed. -HB.instance Definition _ := @PreTopologicalNmodule_isTopologicalNmodule.Build topU add_sub. +HB.instance Definition _ := @PreTopologicalNmodule_isTopologicalNmodule.Build topU add_sub. -Check (topU : TopologicalNmodule.type). +Check (topU : TopologicalNmodule.type). #[local] Lemma opp_sub : continuous (-%R : topU -> topU). Proof. -apply: continuous_comp_initial => x. -rewrite (_ : _ \o _ = (-%R \o \val))//. -apply: continuous_comp; first by exact: continuous_valE. -by exact: opp_continuous. -by apply/funext => i/=; rewrite GRing.valN. +apply: continuous_comp_initial => x. +rewrite (_ : _ \o _ = -%R \o \val); last first. + by apply/funext=> i /=; rewrite GRing.valN. +apply: continuous_comp; first exact: continuous_valE. +exact: opp_continuous. Qed. HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build topU opp_sub. @@ -188,10 +185,10 @@ Check (topU : TopologicalZmodule.type). #[local] Lemma scale_sub : continuous (fun z : R^o * topU => z.1 *: z.2). Proof. apply: continuous_comp_initial => - [] /= x /= y. -pose h := fun x1x2 : R * U => (x1x2.1, \val x1x2.2). -pose g := fun xy : R * V => xy.1 *: xy.2. -rewrite (_ : _ \o _ = g \o h)//. -apply: continuous_comp; last by exact: scale_continuous. +pose h := fun xy : R * U => (xy.1, \val xy.2). +pose g := fun xy : R * V => xy.1 *: xy.2. +rewrite (_ : _ \o _ = g \o h); last by apply/funext=> i /=; rewrite GRing.valZ. +apply: continuous_comp; last exact: scale_continuous. move => /= A [] /= [] a1 a2 [/=]. move=> - [] /= r /= - [] r0 /= br1. move/(continuous_valE (y : topU)) => /= [na2 /= [] wo2 nay2 val2] A12. @@ -200,7 +197,6 @@ apply: continuous_comp; last by exact: scale_continuous. exists na2; split => //. - by apply: br1; move: H => /= [H _]. - by move: H => /= [_ H]; apply: val2. -by apply/funext => i/=; rewrite /g /h /= GRing.valZ. Qed. HB.instance Definition _ := TopologicalZmodule_isTopologicalLmodule.Build R topU scale_sub. @@ -214,9 +210,9 @@ move : (@locally_convex R V) => - [] B convexB [] openB /= genB. exists [set a | B(\val @` a)]. move=> /= a; rewrite inE /=; rewrite -inE => H /= r s l ra sa. suff : \val(r <|l|> s) \in \val @` a by rewrite !inE /= => -[] x ax /val_inj <-. - have valr : \val r \in [set \val x | x in a] by rewrite inE => /=; exists r; first by rewrite -inE. - have vals : \val s \in [set \val x | x in a] by rewrite inE => /=; exists s; first by rewrite -inE. - move: (convexB ( [set \val x | x in a] ) H (\val r) (\val s) l valr vals) => /=. + have valr : \val r \in \val @` a by rewrite inE => /=; exists r; first by rewrite -inE. + have vals : \val s \in \val @` a by rewrite inE => /=; exists s; first by rewrite -inE. + move: (convexB (\val @` a) H (\val r) (\val s) l valr vals) => /=. by rewrite !GRing.valD !GRing.valZ //. split. move=> /= a. admit. From a0f882a9a7c1938543c8f0fe3861a9152e5897aa Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 24 Apr 2026 22:17:45 +0900 Subject: [PATCH 18/21] base convexe wip --- theories/hahn_banach_theorem.v | 25 ++++++++++++++++++++----- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index ee419eace..80e0f45ea 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -157,7 +157,7 @@ pose h := fun xy : U * U => (\val xy.1, \val xy.2). pose g := fun xy : V * V => xy.1 + xy.2. rewrite (_ : _ \o _ = g \o h); last first. by apply/funext => i /=; rewrite GRing.valD. -apply: continuous_comp; last exact: add_continuous. +apply: continuous_comp; last exact: add_continuous. apply: cvg_pair => //=. - apply: (cvg_comp _ _ cvg_fst). exact: (continuous_valE (x : topU)). @@ -190,7 +190,7 @@ pose g := fun xy : R * V => xy.1 *: xy.2. rewrite (_ : _ \o _ = g \o h); last by apply/funext=> i /=; rewrite GRing.valZ. apply: continuous_comp; last exact: scale_continuous. move => /= A [] /= [] a1 a2 [/=]. - move=> - [] /= r /= - [] r0 /= br1. + move=> - [] /= r /= - [] r0 /= br1. move/(continuous_valE (y : topU)) => /= [na2 /= [] wo2 nay2 val2] A12. apply: filterS; first by exact: A12. exists ( ball_ [eta normr] x r ,na2) => //=; split; first by exists r. @@ -215,8 +215,23 @@ exists [set a | B(\val @` a)]. move: (convexB (\val @` a) H (\val r) (\val s) l valr vals) => /=. by rewrite !GRing.valD !GRing.valZ //. split. - move=> /= a. admit. -move => /=. + move => A /= H. + have -> : A = \val @^-1`(\val @` A ). + apply/seteqP; split => x /=; first by exists x. + by move => -[y Ay] /val_inj <-. + apply: open_comp; first by move => x _ ;apply: continuous_valE. + by apply: openB. +(* the following should be simpler *) +move=> /= x A [] A' []; rewrite /wopen => -[]/= C openC CA Ax AA'. +have H : nbhs (\val x) C by rewrite nbhsE /=; exists C =>//; split => //=; move: Ax; rewrite -CA /=. +move: (genB (\val x) C H); rewrite /filter_from /=. +move => [] c [] Bc cx cC /=. +exists (\val @^-1` c); last by move => y Cy; apply: AA'; rewrite -CA /=; apply:cC. +split => //=. +suff -> : [set \val x | x in \val @^-1` c] = c by []. +move=> P T /=; rewrite eqEsubset; split => y; first by move=> [z + <-]. +move=> cy /=. +(*nope*) Admitted. HB.instance Definition _ := @Uniform_isConvexTvs.Build R topU locally_convex_sub. @@ -234,7 +249,7 @@ Check (topU : convexTvsType R). Check (topU : subLmodType S). Check (topU : subConvexTvsType S). -End lmodule_isSubTvs. +End lmodule_isSubTvs. (* HB.factory Record SubLmodule_isSubConvexTvs (R : realFieldType) (V : convexTvsType R) (S : pred V) U & SubChoice V S U & @GRing.SubLmodule R V S U := { From 1cea0c450c06f092a6579e736dd4d01e2b3f0eae Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 24 Apr 2026 23:10:56 +0900 Subject: [PATCH 19/21] base convexe wip --- theories/hahn_banach_theorem.v | 36 ++++++++++++++++++++++++++++++++-- 1 file changed, 34 insertions(+), 2 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 80e0f45ea..f380762ac 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -207,7 +207,39 @@ Check (topU : TopologicalLmodule.type R). (forall b, b \in B -> convex_set b) & basis B. Proof. move : (@locally_convex R V) => - [] B convexB [] openB /= genB. -exists [set a | B(\val @` a)]. +exists [set a | B(\val @` a)]. + move=> /= a; rewrite inE /=; rewrite -inE => H /= r s l ra sa. + suff : \val(r <|l|> s) \in \val @` a by rewrite !inE /= => -[] x ax /val_inj <-. + have valr : \val r \in \val @` a by rewrite inE => /=; exists r; first by rewrite -inE. + have vals : \val s \in \val @` a by rewrite inE => /=; exists s; first by rewrite -inE. + move: (convexB (\val @` a) H (\val r) (\val s) l valr vals) => /=. + by rewrite !GRing.valD !GRing.valZ //. +split. + move => A /= H. + have -> : A = \val @^-1`(\val @` A ). + apply/seteqP; split => x /=; first by exists x. + by move => -[y Ay] /val_inj <-. + apply: open_comp; first by move => x _ ;apply: continuous_valE. + by apply: openB. +(* the following should be simpler *) +move=> /= x A nxA. +pose t:= nxA. +move: t => -[] /= /= b; rewrite /wopen => -[] /= [] c openc cA bx bA. +have H: nbhs (val x) (val @` A). rewrite nbhsE /=. +exists (val @` b); last by move => z //= [] z0 bz valz; exists z0; first by apply: bA. +split => //=; last by exists x. +Print wopen. admit. (*maybe ?*) +move: (genB (\val x) _ H). +rewrite /filter_from /=. +move => [] d [] Bd dx dC /=. +exists (\val @^-1` d); last by move => y /= Cy; move: (dC (\val y) Cy) => /= [] t + /val_inj <-. +split => //=. +suff -> : [set \val (x : topU) | x in \val @^-1` d] = d by []. +rewrite eqEsubset; split => y; first by move=> [z + <-]. +move=> dy /=. +by move: (dC y dy) => /= [] t At valt; exists t; rewrite valt. + +(*exists [set a | B(\val @` a)]. move=> /= a; rewrite inE /=; rewrite -inE => H /= r s l ra sa. suff : \val(r <|l|> s) \in \val @` a by rewrite !inE /= => -[] x ax /val_inj <-. have valr : \val r \in \val @` a by rewrite inE => /=; exists r; first by rewrite -inE. @@ -230,7 +262,7 @@ exists (\val @^-1` c); last by move => y Cy; apply: AA'; rewrite -CA /=; apply: split => //=. suff -> : [set \val x | x in \val @^-1` c] = c by []. move=> P T /=; rewrite eqEsubset; split => y; first by move=> [z + <-]. -move=> cy /=. +move=> cy /=.*) (*nope*) Admitted. From f235a1a6782340dfbd9f54a350bd2aa8a025ae60 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 24 Apr 2026 23:22:51 +0900 Subject: [PATCH 20/21] base convexe wip --- theories/hahn_banach_theorem.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index f380762ac..69077169c 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -226,9 +226,9 @@ move=> /= x A nxA. pose t:= nxA. move: t => -[] /= /= b; rewrite /wopen => -[] /= [] c openc cA bx bA. have H: nbhs (val x) (val @` A). rewrite nbhsE /=. -exists (val @` b); last by move => z //= [] z0 bz valz; exists z0; first by apply: bA. -split => //=; last by exists x. -Print wopen. admit. (*maybe ?*) +exists (val @` (b: set topU)); last by move => z //= [] z0 bz valz; exists z0; first by apply: bA. +split => //=; last by exists x. have ob: open (b : set topU). (*should be true as val_continuous*) admit. +Fail apply: (@initial_subspace_open V ( (initial_topology \val)) (\val) b ob). (*why ??*) admit. move: (genB (\val x) _ H). rewrite /filter_from /=. move => [] d [] Bd dx dC /=. From cad6d8a62cd67fa167b1d25fd37c7347a19e9031 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sat, 25 Apr 2026 21:06:36 +0900 Subject: [PATCH 21/21] missing join ? --- theories/hahn_banach_theorem.v | 53 +++++++++------------------------- 1 file changed, 14 insertions(+), 39 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 69077169c..0f12d3f01 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -222,48 +222,23 @@ split. apply: open_comp; first by move => x _ ;apply: continuous_valE. by apply: openB. (* the following should be simpler *) -move=> /= x A nxA. -pose t:= nxA. -move: t => -[] /= /= b; rewrite /wopen => -[] /= [] c openc cA bx bA. -have H: nbhs (val x) (val @` A). rewrite nbhsE /=. -exists (val @` (b: set topU)); last by move => z //= [] z0 bz valz; exists z0; first by apply: bA. -split => //=; last by exists x. have ob: open (b : set topU). (*should be true as val_continuous*) admit. -Fail apply: (@initial_subspace_open V ( (initial_topology \val)) (\val) b ob). (*why ??*) admit. +move=> /= x A [] /= /= b; rewrite /wopen => -[] /= [] c openc cA bx bA. +have H: nbhs (val x) (val @` A). + rewrite nbhsE /=; exists (val @` (b: set topU)); last first. + by move => z //= [] z0 bz valz; exists z0; first by apply: bA. + split => //=; last by exists x. + have ob: open (b : set topU) by rewrite /open /= /wopen; exists c. + move: (@initial_subspace_open V ( (initial_topology \val)) (\val) b ob). + Fail exact. + Set Printing Implicit. + (*why ?? Set Printing Implicit shows that intermediate instances might be missing *) + admit. move: (genB (\val x) _ H). -rewrite /filter_from /=. -move => [] d [] Bd dx dC /=. +rewrite /filter_from /= => - [] d [] Bd dx dC /=. exists (\val @^-1` d); last by move => y /= Cy; move: (dC (\val y) Cy) => /= [] t + /val_inj <-. -split => //=. -suff -> : [set \val (x : topU) | x in \val @^-1` d] = d by []. +split => //=;suff -> : [set \val (x : topU) | x in \val @^-1` d] = d by []. rewrite eqEsubset; split => y; first by move=> [z + <-]. -move=> dy /=. -by move: (dC y dy) => /= [] t At valt; exists t; rewrite valt. - -(*exists [set a | B(\val @` a)]. - move=> /= a; rewrite inE /=; rewrite -inE => H /= r s l ra sa. - suff : \val(r <|l|> s) \in \val @` a by rewrite !inE /= => -[] x ax /val_inj <-. - have valr : \val r \in \val @` a by rewrite inE => /=; exists r; first by rewrite -inE. - have vals : \val s \in \val @` a by rewrite inE => /=; exists s; first by rewrite -inE. - move: (convexB (\val @` a) H (\val r) (\val s) l valr vals) => /=. - by rewrite !GRing.valD !GRing.valZ //. -split. - move => A /= H. - have -> : A = \val @^-1`(\val @` A ). - apply/seteqP; split => x /=; first by exists x. - by move => -[y Ay] /val_inj <-. - apply: open_comp; first by move => x _ ;apply: continuous_valE. - by apply: openB. -(* the following should be simpler *) -move=> /= x A [] A' []; rewrite /wopen => -[]/= C openC CA Ax AA'. -have H : nbhs (\val x) C by rewrite nbhsE /=; exists C =>//; split => //=; move: Ax; rewrite -CA /=. -move: (genB (\val x) C H); rewrite /filter_from /=. -move => [] c [] Bc cx cC /=. -exists (\val @^-1` c); last by move => y Cy; apply: AA'; rewrite -CA /=; apply:cC. -split => //=. -suff -> : [set \val x | x in \val @^-1` c] = c by []. -move=> P T /=; rewrite eqEsubset; split => y; first by move=> [z + <-]. -move=> cy /=.*) -(*nope*) +by move=> dy /=; move: (dC y dy) => /= [] t At valt; exists t; rewrite valt. Admitted. HB.instance Definition _ := @Uniform_isConvexTvs.Build R topU locally_convex_sub.