From 5bcd6e01904c5987d5685515ea5e5d269de94208 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 20 Mar 2026 11:14:19 +0900 Subject: [PATCH 01/35] Hahn-Banach theorem --- CHANGELOG_UNRELEASED.md | 194 ++++++++++++++ _CoqProject | 2 + theories/Make | 2 + theories/hahn_banach_theorem.v | 428 +++++++++++++++++++++++++++++++ theories/normedtype_theory/tvs.v | 3 +- 5 files changed, 628 insertions(+), 1 deletion(-) create mode 100644 theories/hahn_banach_theorem.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c934f4375f..e2d2938ed4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -130,6 +130,43 @@ + definition `preimage_set_system` + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, `preimage_set_system_id` +- in `functions.v`: + + lemmas `linfunP`, `linfun_eqP` + + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }` + +- 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) @@ -183,6 +220,163 @@ `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`, `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule` +- 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 8d0e2e3439..8c5f2ee371 100644 --- a/_CoqProject +++ b/_CoqProject @@ -88,6 +88,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 136692568d..d56ba42a32 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 0000000000..afd06c1516 --- /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 00b1a33851..20b20ecdb7 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -587,6 +587,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. @@ -679,7 +680,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 }. From 5eadaadc1c6314f7446e83a3951ca1f15edee465 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 15 Apr 2026 14:29:02 +0900 Subject: [PATCH 02/35] 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 afd06c1516..cc899eaf0e 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 b051952f7837ccbbea8ed53e6186a468edb1077f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 15 Apr 2026 16:10:41 +0900 Subject: [PATCH 03/35] 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 cc899eaf0e..5580a82c09 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 51977b5d56c9b8ded64ff982638dbf2bfda94a88 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 15 Apr 2026 16:26:18 +0900 Subject: [PATCH 04/35] 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 5580a82c09..3d5a23706c 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 8a7356d2a8156918e8e66bc14e987cc3d6cfa7f6 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 17 Apr 2026 11:30:43 +0900 Subject: [PATCH 05/35] 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 3d5a23706c..b2fb1c1309 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 70a8ece1bb6e056293fdc3e66ff162a18300fc73 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 17 Apr 2026 12:05:56 +0900 Subject: [PATCH 06/35] 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 b2fb1c1309..b3c4632e12 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 b8db8b19885960fcbe37608af3bfbf822b250c67 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 17 Apr 2026 15:12:10 +0900 Subject: [PATCH 07/35] 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 b3c4632e12..c4fbe2f36b 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 55fa3226518c7f7db9fca5878618e3f555c08f99 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sun, 19 Apr 2026 22:40:51 +0900 Subject: [PATCH 08/35] 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 c4fbe2f36b..decd6f5261 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 21c6e76c38c14a91db57946d231afb17f4be870f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 21 Apr 2026 12:19:15 +0900 Subject: [PATCH 09/35] 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 decd6f5261..e39aff0824 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 6206c32abc83fc8e403ddb8cda1543c2ca4de6ec Mon Sep 17 00:00:00 2001 From: mkerjean Date: Tue, 21 Apr 2026 14:26:10 +0900 Subject: [PATCH 10/35] 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 e39aff0824..b8121bd52e 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 247a8026e79a169a084e84dc990d535552703b31 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 21 Apr 2026 14:52:45 +0900 Subject: [PATCH 11/35] 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 b8121bd52e..27fddf0110 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 9c61e8d00a223e854fea51ae88f31f151c533948 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Tue, 21 Apr 2026 16:48:28 +0900 Subject: [PATCH 12/35] 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 27fddf0110..c7d0ce7c6f 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 e20aca53fce0222fb0c853089524ddfa8d297f1f Mon Sep 17 00:00:00 2001 From: mkerjean Date: Tue, 21 Apr 2026 21:26:59 +0900 Subject: [PATCH 13/35] 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 c7d0ce7c6f..459a780555 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 f6b9f40c77c574f5d316a99a6d818371d2cbce84 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 22 Apr 2026 10:06:21 +0900 Subject: [PATCH 14/35] 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 459a780555..cbd87617f0 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 23bf455f485f81a0fd02e43e711ac3e2fef42222 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 22 Apr 2026 20:53:28 +0900 Subject: [PATCH 15/35] 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 cbd87617f0..ba34571bd1 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 f597c2a76049d01f98e2fb08788f1c1fef7ec0c1 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 22 Apr 2026 21:58:34 +0900 Subject: [PATCH 16/35] 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 ba34571bd1..9e06c2429c 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 daf98b0abeab9d776d609c6895b68f84a4fc0223 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 23 Apr 2026 00:48:12 +0900 Subject: [PATCH 17/35] 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 9e06c2429c..ee419eaceb 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 5a19da86c6a3ec1088c5d17541ee1b9a1e31093a Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 24 Apr 2026 22:17:45 +0900 Subject: [PATCH 18/35] 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 ee419eaceb..80e0f45ea2 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 e65eb5ba9a8b7852ae8264f8ef78ff320ca50a65 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 24 Apr 2026 23:10:56 +0900 Subject: [PATCH 19/35] 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 80e0f45ea2..f380762acf 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 ec9437f4adc6ba6fdd8bee7b91b3790977927fc2 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 24 Apr 2026 23:22:51 +0900 Subject: [PATCH 20/35] 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 f380762acf..69077169cf 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 936bb5090afbdca32ba0d0f230576a9d082aa275 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sat, 25 Apr 2026 21:06:36 +0900 Subject: [PATCH 21/35] 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 69077169cf..0f12d3f01f 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. From bc5f750833a54e021731fadc62ad1d24733674d3 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 1 May 2026 12:05:55 +0900 Subject: [PATCH 22/35] sub locally convex --- theories/hahn_banach_theorem.v | 58 ++++++++++++++-------------------- 1 file changed, 24 insertions(+), 34 deletions(-) diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v index 0f12d3f01f..b71cdffaaf 100644 --- a/theories/hahn_banach_theorem.v +++ b/theories/hahn_banach_theorem.v @@ -206,41 +206,31 @@ 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 \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 //. +move : (@locally_convex R V) => - [] B convexB [] openB /= genB. +exists [set a | exists2 b, B(b) & (\val @^-1` b = a)]. + move=> /= a; rewrite inE /=; rewrite -inE => H /= r s l ra sa. + move: H => /=; rewrite inE => - [b] Bb ab /=. + suff : \val(r <|l|> s) \in b by rewrite !inE /= -ab. + have valr : \val r \in b by rewrite inE /=; move: ra; rewrite -ab inE //=. + have vals : \val s \in b by by rewrite inE /=; move: sa; rewrite -ab inE //=. + rewrite /conv /=; rewrite !raddf/= !GRing.valZ; apply: convexB => //. + by apply: mem_set. 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 [] /= /= 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 /= => - [] 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 + <-]. -by move=> dy /=; move: (dC y dy) => /= [] t At valt; exists t; rewrite valt. -Admitted. - +by move => /= a /= [b] Bb <-; rewrite /open /= /wopen /=; exists b => //; exact: openB. +Print basis. +move=> /= x a [] /= /= b; rewrite /wopen => -[] /= [] c openc cA bx bA. +red; simpl. +rewrite /filter_from /=. +have H: nbhs (val x) (c). + rewrite nbhsE /=; exists c => //; split => //. + have := bx; rewrite -cA //=. +have:= (genB (\val x) c H); rewrite /filter_from /= => - [] d [] Bd dx dC /=. +exists (\val @^-1` d); last first. + by move => y /= dy; apply: bA; rewrite -cA //=; apply: dC. +split; last by []. +by exists d. +Qed. + HB.instance Definition _ := @Uniform_isConvexTvs.Build R topU locally_convex_sub. (*HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R topU From 6e96471298cca0e0ff5e5c0cddf583b96c7308e1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 3 May 2026 01:02:38 +0900 Subject: [PATCH 23/35] lint --- _CoqProject | 2 +- classical/mathcomp_extra.v | 28 +- classical/unstable.v | 7 + theories/Make | 2 +- .../functional_analysis/hahn_banach_theorem.v | 739 ++++++++++++++++ theories/hahn_banach_theorem.v | 831 ------------------ 6 files changed, 774 insertions(+), 835 deletions(-) create mode 100644 theories/functional_analysis/hahn_banach_theorem.v delete mode 100644 theories/hahn_banach_theorem.v diff --git a/_CoqProject b/_CoqProject index 8c5f2ee371..f0b745c7f6 100644 --- a/_CoqProject +++ b/_CoqProject @@ -88,7 +88,7 @@ theories/normedtype_theory/urysohn.v theories/normedtype_theory/vitali_lemma.v theories/normedtype_theory/normedtype.v -theories/hahn_banach_theorem.v +theories/functional_analysis/hahn_banach_theorem.v theories/sequences.v theories/realfun.v diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 0b87d5fc7c..674ea6c198 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1,4 +1,5 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. (**md**************************************************************************) @@ -93,10 +94,33 @@ Proof. by case: C => //= /ltW. Qed. (* MathComp 2.6 additions *) (**************************) -(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *) Lemma intrD1 {R : pzRingType} (i : int) : (i + 1)%:~R = i%:~R + 1 :> R. Proof. by rewrite intrD. Qed. -(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *) Lemma intr1D {R : pzRingType} (i : int) : (1 + i)%:~R = 1 + i%:~R :> R. Proof. by rewrite intrD. Qed. + +Lemma divDl_ge0 (R : numDomainType) (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : + 0 <= s / (s + t). +Proof. +by apply: divr_ge0 => //; apply: addr_ge0. +Qed. + +Lemma divDl_le1 (R : numFieldType) (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : + s / (s + t) <= 1. +Proof. +move: s0; rewrite le0r => /predU1P [->|s0]; first by rewrite mul0r. +by rewrite ler_pdivrMr ?mul1r ?lerDl // ltr_wpDr. +Qed. + +HB.mixin Record Zmodule_isSubNormed (R : numDomainType) + (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 +}. + +#[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_isSubNormed R V S U }. diff --git a/classical/unstable.v b/classical/unstable.v index e331d2836d..cf8b4ce04a 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -369,6 +369,13 @@ Qed. Lemma onemV (F : numFieldType) (x : F) : x != 0 -> x^-1.~ = (x - 1) / x. Proof. by move=> ?; rewrite mulrDl divff// mulN1r. Qed. +Lemma divD_onem (R : realFieldType) (s t : R) (s0 : 0 < s) (t0 : 0 < t) : + (s / (s + t)).~ = t / (s + t). +Proof. +rewrite /onem. +by rewrite -(@divff _ (s + t)) ?gt_eqF ?addr_gt0// -mulrBl (addrC s) addrK. +Qed. + Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N. Proof. by case: a => //= n _; case: b. Qed. diff --git a/theories/Make b/theories/Make index d56ba42a32..17da83d2a3 100644 --- a/theories/Make +++ b/theories/Make @@ -55,7 +55,7 @@ normedtype_theory/urysohn.v normedtype_theory/vitali_lemma.v normedtype_theory/normedtype.v -hahn_banach_theorem.v +functional_analysis/hahn_banach_theorem.v realfun.v sequences.v diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v new file mode 100644 index 0000000000..eb0a1acfb7 --- /dev/null +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -0,0 +1,739 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import interval_inference. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp contra classical_sets filter. +From mathcomp Require Import topology convex reals normedtype. + +(**md**************************************************************************) +(* # The Hahn-Banach theorem *) +(* *) +(* 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 `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 HahnBanachZorn == defintion of the type Zorntype of linear *) +(* functional graphs, bounded by a convex function *) +(* and extending to the whole space a given linear *) +(* graph. *) +(* ``` *) +(* *) +(******************************************************************************) + +Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import numFieldNormedType.Exports. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope convex_scope. +Local Open Scope real_scope. + +HB.mixin Record isSubNbhs + (V : nbhsType) (S : pred V) U & SubChoice V S U & Nbhs U := { + continuous_valE : continuous (val : U -> V) +}. + +#[short(type="subNbhsType")] +HB.structure Definition SubNbhs (V : nbhsType) (S : pred V) := + { U of SubChoice V S U & Nbhs U & isSubNbhs V S U}. + +#[short(type="subTopologicalType")] +HB.structure Definition SubTopological (V : topologicalType) + (S : pred V) := {U of SubNbhs V S U & Topological U}. + +(* NB: rename to sub_init_topo? *) +Definition topU (V : Type) (S : pred V) (U : subChoiceType S) : Type + := initial_topology (\val : U -> V). + +Section SubType_isSubTopological. +Context (V : topologicalType) (S : pred V) (U : subChoiceType S). + +Local Notation topU := (topU U). +HB.instance Definition _ := SubChoice.on topU. +HB.instance Definition _ := Nbhs.on topU. +HB.instance Definition _ := Topological.on topU. + +Let 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 : 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 }. + +(* 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). + +Local Notation topU := (topU U). +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 : uniformType). +Check (topU : subLmodType S). + +Let add_sub: continuous (fun x : topU * topU => x.1 + x.2). +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). + 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. + +Check (topU : TopologicalNmodule.type). + +Let opp_sub : continuous (-%R : topU -> topU). +Proof. +apply: continuous_comp_initial => x. +rewrite (_ : _ \o _ = -%R \o \val). + 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. + +Check (topU : TopologicalZmodule.type). + +Let scale_sub : continuous (fun z : R^o * topU => z.1 *: z.2). +Proof. +apply: continuous_comp_initial => - [] /= x /= y. +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); first by apply/funext=> i /=; rewrite GRing.valZ. +apply: continuous_comp; last exact: scale_continuous. +move=> /= A [/= [/= B C]] [[r/= r0 xrB]]. +move/(continuous_valE (y : topU)) => [/= C' [woC' C'y C'C] BCA]. +apply: filterS; first exact: BCA. +exists (ball x r, C') => /=. + by split; [exact: nbhsx_ballx|exists C'; split]. +by move=> su/= [xru C'u]; split; [exact: xrB|exact: C'C]. +Qed. + +HB.instance Definition _ := + TopologicalZmodule_isTopologicalLmodule.Build R topU scale_sub. + +Check (topU : TopologicalLmodule.type R). + +Let locally_convex_sub : exists2 B : set_system topU, + (forall b, b \in B -> convex_set b) & basis B. +Proof. +have [B convexB [openB/= genB]] := @locally_convex R V. +exists [set a | exists2 b, B b & \val @^-1` b = a]. + move=> a /[!inE]/= -[b Bb ba] r s l ra sa. + suff : \val (r <|l|> s) \in b by rewrite !inE /= -ba. + rewrite !GRing.valD !GRing.valZ convexB//; first exact: mem_set. + - by move: ra; rewrite -ba !inE. + - by move: sa; rewrite -ba !inE. +split => /=. + move=> a/= [b Bb <-]; rewrite /open/= /wopen/=; exists b => //. + exact: openB. +move=> x a [/= b [[/=c openc] cb bx ba]]. +rewrite /nbhs/= /filter_from/=. +have : nbhs (val x) c. + rewrite nbhsE /=; exists c => //; split => //. + by move: bx; rewrite -cb. +move/genB => [d [Bd dx dc]]. +exists (\val @^-1` d); first by split => //; exists d. +by move=> y dy; apply: ba; rewrite -cb; exact: dc. +Qed. + +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). + +(*HB.instance Definition _ := ConvexTvs.on topU.*) +HB.instance Definition _ := GRing.SubLmodule.on topU. + +Check (topU : convexTvsType R). +Check (topU : subLmodType S). +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. + +#[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 _ := Topological.on topU. +HB.instance Definition _ := Nbhs.on topU. +HB.instance Definition _ := GRing.Lmodule.on topU. +Check (topU : SubChoice.type S). +Check (topU : pointedType). +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). +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 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 *) + +#[local] Lemma continuous_valE : continuous (val : topU -> V). +Proof. exact: initial_continuous. Qed. + +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). +Check (topU : uniformType). +HB.about subConvexTvsType. +Fail Check (topU : subConvexTvsType S). + + +Fail 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 & @SubConvexTvs R V S U}. + +Section filter_ent. + +Import pseudoMetric_from_normedZmodType. + +Lemma ent_xsection_filter {R : realFieldType} (U : normedZmodType R) x : Filter + [set P | exists2 A : set (pseudoMetric_normed U * pseudoMetric_normed U), + pseudoMetric_from_normedZmodType.ent A & xsection A x `<=` P]. +Proof. +apply: Build_Filter => /=. +- by exists setT => //; exact: (@entourageT (pseudoMetric_normed U)). +- move=> A B/= [A' entA' A'A] [B' entB' B'B]; exists (A' `&` B') => //. + rewrite entourageE. + rewrite /entourage_. + case: entA' => r/= r0 HA'. + case: entB' => d/= d0 HB'. + exists (Num.min r d); first by rewrite /= lt_min r0. + move=> z/= Hz. + split. + apply: HA' => /=. + by rewrite /ball/= (lt_le_trans Hz)// ge_min lexx. + apply: HB' => /=. + by rewrite /ball/= (lt_le_trans Hz)// ge_min lexx orbT. + by rewrite xsectionI; exact: setISS. +- move=> P Q PQ [A entA AP]; exists A => //. + exact: (subset_trans AP). +Qed. + +End filter_ent. + +HB.factory Record SubLmodule_isSubNormedmodule (R : realFieldType) + (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|. + +Let ler_normuD (x y : U) : normu (x + y) <= normu x + normu y. +Proof. by rewrite /normu GRing.valD; exact: ler_normD. Qed. + +Let normru0_eq0 x : normu x = 0 -> x = 0. +Proof. by move/eqP; rewrite normr_eq0 -(@GRing.val0 V S U) => /eqP/val_inj. Qed. + +Let normruMn x n : normu (x *+ n) = normu x *+ n. +Proof. by rewrite /normu raddfMn /=; exact: normrMn. Qed. + +Let normruN x : normu (- x) = normu x. +Proof. by rewrite /normu raddfN /=; exact: normrN. Qed. + +Let 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 @Num.Zmodule_isNormed.Build, this command check +but then we have Fail Check (U : pseudometricnormedzmodtype R) and Fail Check (U +: normedModtype R). + *) +Check (U : normedModType R). + +Let 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). + +Let continuous_valE : continuous (val : U -> V). +Proof. +move=> /= x. +rewrite /continuous_at. +set rhs := (X in _ --> X). +apply/cvgrPdist_le => //=. + exact: ent_xsection_filter. +move=> e e0; near=> t. +rewrite -GRing.valN -GRing.valD norm_valE. +by near: t; exact: cvgr_dist_le e e0. +Unshelve. all: by end_near. Qed. + +HB.instance Definition _ := isSubNbhs.Build _ _ U continuous_valE. + +Check (U : subConvexTvsType S). + +Check (U : subNormedModType S). + +HB.instance Definition _ := SubLmodule_isSubNormedmodule.Build _ _ _ U. +HB.end. + +(* TODO : use a lightweight factory to make every subLmodType a subnormedmodtype *) + +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. +exact: lrf. +Qed. + +Definition add_line f w a := fun v r => exists (v' : V) (r' lambda : R), + [/\ f v' r', v = v' + lambda *: w & r = r' + lambda * a]. + +End Lingraphsec. +End Lingraph. + +Module HahnBanachZorn. +Section HahnBanachZorn. +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}. + +Implicit Types z : zorn_type. + +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; rewrite e in pm1 pm2 *. +by congr ZornType; exact: Prop_irrelevance. +Qed. + +Definition zornS z1 z2 := 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 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. +have [[w Aw] | eA] := lem (exists a, A a); last first. + by exists zphi => a Aa; absurd: 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]. + 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; exact: 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 {sc12 Aa1 a1} {}c1 : carrier a2 v1 r1 by exact: sc12. + by exists a2 => //; case: a2 {Aa2} c2 c1 => c /= [_ hl _ _] *; exact: hl. + - have {sc21 Aa2 a2} {}c2 : carrier a1 v2 r2 by exact: 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. + 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. + +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 v : exists2 ze, zornS z ze & exists r, (carrier ze) v r. +Proof. +have [[r rP]|] := lem (exists r, carrier z v r). + by 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 have := ps1 0; rewrite GRing.val0. +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 /[dup] cxr /aP {}aP. + have [/aP[]// | ltl0 | ->] := ltrgt0P lambda. + rewrite -[lambda]opprK scaleNr mulNr. + by have /aP[] : 0 < - lambda by rewrite oppr_gt0. + by rewrite mul0r scale0r !addr0 ms1. + 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 : R) : 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// [leLHS]mulrC [leRHS]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 := _ - _ *: _. + rewrite (@le_trans _ _ (p (s / (s + t) *: y1 + t / (s + t) *: y2)))//. + 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 / _. + rewrite [leLHS](_ : _ = l * r1 + m * r2). + by rewrite mulrDl ![_ * _ / _]mulrAC. + apply: ms1; apply: (ls1) => //. + by rewrite -[_ *: _]add0r -[_ * _]add0r; exact: ls1. + rewrite !mulrDl ![_ * _ / _]mulrAC -divD_onem//. + pose st := Itv01 (divDl_ge0 (ltW lt0s) (ltW lt0t)) + (divDl_le1 (ltW lt0s) (ltW lt0t)). + exact: (p_cvx st (in_setT y1) (in_setT y2)). + pose Pa := + [set r | exists x1 r1 (s1 : R), [/\ c x1 r1, 0 < s1 & r = a x1 r1 s1]]. + pose Pb := + [set r | exists x1 r1 (s1 : R), [/\ c x1 r1, 0 < s1 & r = b x1 r1 s1]]. + pose sa := sup Pa. (* We need p with values in a *realType* *) + have Pax : Pa !=set0 by exists (a 0 0 1), 0, 0, 1. + have ubdP : ubound Pa sa. + apply: sup_upper_bound; split => //=. + by exists (b 0 0 1) =>/= x [y [r [s [cry lt0s ->]]]]; exact: le_a_b. + have saP (u : R) : ubound Pa u -> sa <= u by exact: ge_sup. + pose ib := inf Pb. (* We need P with values in a *realType* *) + have Pbx : Pb !=set0 by exists (b 0 0 1), 0, 0, 1. + have ibdP : lbound Pb ib. + apply: ge_inf; exists (a 0 0 1) => /= x [y [r [s [cry lt0s ->]]]]. + exact: le_a_b. + have ibP (u : R) : lbound Pb u -> u <= ib by exact: lb_le_inf Pbx. + have le_sa_ib : sa <= ib. + apply: saP => _ [y [r [l [cry lt0l ->]]]]. + by apply: ibP => _ [z [s [m [crz lt0m ->]]]]; exact: le_a_b. + pose alpha := (sa + ib) / 2. + exists alpha => x r l cxr lt0l; split. + - suff : alpha <= b x r l by rewrite (ler_pdivlMr _ _ lt0l) lerBrDl mulrC. + by apply: (le_trans (midf_le le_sa_ib).2); apply: ibdP; exists x, r, l. + - suff : a x r l <= alpha. + by rewrite (ler_pdivrMr _ _ lt0l) lerBlDl -lerBlDr mulrC. + by apply: (le_trans _ (midf_le le_sa_ib).1); apply: ubdP; exists x, r, l. +pose z' := fun k r => exists (v' : V) (r' lambda : R), + [/\ c v' r', k = v' + lambda *: v & r = r' + lambda * a]. +have z'_extends x r : c x r -> z' x r. + by move=> cxr; exists x, r, 0; split; rewrite // ?scale0r ?mul0r ?addr0. +have z'_prol : extend_graph z'. + move=> x. + by exists (val x), (phi x), 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 -> ->]]]]. + rewrite [X in z' X _](_ : _ = w1 + l *: w2 + (m1 + l * m2) *: v). + by rewrite !scalerDr !scalerDl scalerA -!addrA [X in _ + X]addrCA. + rewrite [X in z' _ X](_ : _ = s1 + l * s2 + (m1 + l * m2) * a). + by rewrite !mulrDr !mulrDl mulrA -!addrA [X in _ + X]addrCA. + exists (w1 + l *: w2), (s1 + l * s2), (m1 + l * m2); split => //. + exact: ls1. +have z'_functional : functional_graph z'. + move=> w r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 e1 ->]]]]. + have [rw12 erw12] : exists r, c (w1 - w2) r. + by exists (s1 + -1 * s2); rewrite -(scaleN1r w2); exact: ls1. + have h1 (x : V) (r l : R) : x = l *: v -> c x r -> x = 0 /\ l = 0. + move=> -> cxr; have [->|ln0] := eqVneq l 0; first by rewrite scale0r. + suff cvs : c v (l^-1 * r) by absurd: nzv; exists (l^-1 * r). + suff -> : v = l ^-1 *: (l *: v). + by rewrite -(add0r (_ *: _)) -(add0r (_ * _)); exact: ls1. + by rewrite scalerA mulVf ?scale1r. + have [ew12] : w1 - w2 = 0 /\ m2 - m1 = 0. + apply: h1 erw12; rewrite scalerBl. + by apply: subr0_eq; rewrite opprB addrACA e1 -opprD subrr. + suff -> : s1 = s2 by move/subr0_eq => ->. + by apply: fs1 cws2; rewrite -(subr0_eq ew12). +have z'_spec : le_extend_graph z' by []. +exists (ZornType z'_spec) => //=; exists a, 0, 0, 1. +by rewrite !add0r mul1r scale1r. +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. +have [h hP] := choice tot_g. +exists h => v r; split=> [|<-//]. +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 HahnBanachZorn. +End HahnBanachZorn. + +(* NB: could go to convex.v *) +Section hahn_banach. +Import Lingraph. +Import HahnBanachZorn. +(* 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 hahn_banach_extension : exists2 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 /(hb_witness p_cvx)[g gP]] := zornS_ex f_bounded_by_p. +have scalg : linear_for *%R g. + case: z gP => [c [_ ls1 _ _]] /= gP. + have addg : zmod_morphism 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; exact/gP. + by move=> w l; apply/gP; apply: lingraph_scale => //; exact/gP. +pose lg := GRing.isLinear.Build _ _ _ _ g scalg. +pose g' : {linear V -> R | *%R} := HB.pack g lg. +exists g'. + by case: z gP => [c [_ _ bp _]] /= gP => x; apply: bp; exact/gP. +by move=> z'; apply/gP; case: z {gP} => [c [_ _ _ pf]] /=; exact: pf. +Qed. + +End hahn_banach. + +(* 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}). + +(*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 : F', g (val x) = f x. +Proof. +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/continuous_fun. +pose p := fun x : V => `|x| * r. +have convp : @convex_function _ _ [set: V] p. + rewrite /convex_function /conv => l v1 v2 _ _ /=. + rewrite [in leRHS]/conv /= /p. + apply: le_trans. + have /ler_pM := ler_normD (l%:num *: v1) (l%:num.~ *: v2). + by apply => //; exact: ltW. + rewrite mulrDl !normrZ -![_ *: _]/(_ * _) (@ger0_norm _ l%:num)//. + by rewrite (@ger0_norm _ l%:num.~)// ?mulrA// onem_ge0. +have : forall z : F', f z <= p (\val z). + by move=> z; rewrite /p (le_trans (ler_norm _)). +move=> /(hahn_banach_extension convp)[g majgp F_eqgf]. +have ling : linear (g : V -> R) by exact: linearP. +have contg : continuous (g : V -> R). + move=> x; apply/continuousfor0_continuous/bounded_linear_continuous. + exists r; split; first exact: gtr0_real. + move=> M rM; rewrite nbhs_ballP; exists 1 => //=. + move=> y; rewrite -ball_normE//= sub0r => y1. + rewrite ler_norml; apply/andP; split. + - rewrite lerNl -linearN (le_trans (majgp (- y)))//. + by rewrite /p -(mul1r M) ltW// ltr_pM// ltW. + - by rewrite (le_trans (majgp y))// /p -(mul1r M) -normrN ltW// ltr_pM// ltW. +pose lcg := isLinearContinuous.Build _ _ _ _ g ling contg. +pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg. +by exists g'. +Qed. + +End hahn_banach_normed. diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v deleted file mode 100644 index b71cdffaaf..0000000000 --- a/theories/hahn_banach_theorem.v +++ /dev/null @@ -1,831 +0,0 @@ -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**************************************************************************) -(* # The Hahn-Banach theorem *) -(* *) -(* 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 `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 *) - -(* 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). -Proof. -rewrite /onem. -by rewrite -(@divff _ (s + t)) ?gt_eqF ?addr_gt0// -mulrBl (addrC s) addrK. -Qed. - -End pos_quotient. - -HB.mixin Record Zmodule_isSubNormed (R : numDomainType) - (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 -}. - -(* 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_isSubNormed R V S U }. - -HB.mixin Record isSubNbhs - (V : nbhsType) (S : pred V) U & SubChoice V S U & Nbhs U := { - continuous_valE : continuous (val : U -> V) -}. - -#[short(type="subNbhsType")] -HB.structure Definition SubNbhs (V : nbhsType) (S : pred V) := - { U of SubChoice V S U & Nbhs U & isSubNbhs V S U}. - -(*#[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="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 : subChoiceType 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 : 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 - }. - -(* 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). - -Notation topU := (topU U). -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 : 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 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. - -Check (topU : TopologicalNmodule.type). - -#[local] Lemma opp_sub : continuous (-%R : topU -> topU). -Proof. -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. - -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 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. - 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. -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. -Proof. -move : (@locally_convex R V) => - [] B convexB [] openB /= genB. -exists [set a | exists2 b, B(b) & (\val @^-1` b = a)]. - move=> /= a; rewrite inE /=; rewrite -inE => H /= r s l ra sa. - move: H => /=; rewrite inE => - [b] Bb ab /=. - suff : \val(r <|l|> s) \in b by rewrite !inE /= -ab. - have valr : \val r \in b by rewrite inE /=; move: ra; rewrite -ab inE //=. - have vals : \val s \in b by by rewrite inE /=; move: sa; rewrite -ab inE //=. - rewrite /conv /=; rewrite !raddf/= !GRing.valZ; apply: convexB => //. - by apply: mem_set. -split. -by move => /= a /= [b] Bb <-; rewrite /open /= /wopen /=; exists b => //; exact: openB. -Print basis. -move=> /= x a [] /= /= b; rewrite /wopen => -[] /= [] c openc cA bx bA. -red; simpl. -rewrite /filter_from /=. -have H: nbhs (val x) (c). - rewrite nbhsE /=; exists c => //; split => //. - have := bx; rewrite -cA //=. -have:= (genB (\val x) c H); rewrite /filter_from /= => - [] d [] Bd dx dC /=. -exists (\val @^-1` d); last first. - by move => y /= dy; apply: bA; rewrite -cA //=; apply: dC. -split; last by []. -by exists d. -Qed. - -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). - -HB.instance Definition _ := ConvexTvs.on topU. -HB.instance Definition _ := GRing.SubLmodule.on topU. - -Check (topU : convexTvsType R). -Check (topU : subLmodType S). -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. - -#[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 _ := Topological.on topU. -HB.instance Definition _ := Nbhs.on topU. -HB.instance Definition _ := GRing.Lmodule.on topU. -Check (topU : SubChoice.type S). -Check (topU : pointedType). -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). -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 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 *) - -#[local] Lemma continuous_valE : continuous (val : topU -> V). -Proof. exact: initial_continuous. Qed. - -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). -Check (topU : uniformType). -HB.about subConvexTvsType. -Fail Check (topU : subConvexTvsType S). - - -Fail 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 & @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 := { -}. - -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 @Num.Zmodule_isNormed.Build, this command check -but then we have Fail Check (U : pseudometricnormedzmodtype R) and Fail Check (U -: 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). - -#[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 _ := isSubNbhs.Build _ _ U continuous_valE. - -Check (U : subConvexTvsType S). - -Check (U : subNormedModType S). - -HB.instance Definition _ := SubLmodule_isSubNormedmodule.Build _ _ _ U. -HB.end. - -(* TODO : use a lightweight factory to make every subLmodType a subnormedmodtype *) - -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. -exact: lrf. -Qed. - -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. -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; 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 ). - -(* 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 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. - 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]. - 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. - 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. - 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. - -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. - -(* 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 f_bounded_by_p : forall (z : F'), (f z <= p (\val 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. -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 hahn_banach. - -(* 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}). - - -(*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. -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. - by rewrite !mulrA. -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. - apply: bounded_linear_continuous. - 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. - - 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 hahn_banach_normed. From 18f14a955054ecde483925375eaef3228b3398ff Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 3 May 2026 01:05:08 +0900 Subject: [PATCH 24/35] fix --- theories/normedtype_theory/tvs.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 20b20ecdb7..00b1a33851 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -587,7 +587,6 @@ 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. @@ -680,7 +679,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 }. From eca83672beb5a7728f7d5bf7cd0eb941b6d269ea Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 3 May 2026 01:07:21 +0900 Subject: [PATCH 25/35] upd changelog (wip) --- CHANGELOG_UNRELEASED.md | 159 ++-------------------------------------- 1 file changed, 6 insertions(+), 153 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e2d2938ed4..de330aadb7 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -222,160 +222,13 @@ - in set_interval.v + `setUitv1`, `setU1itv`, `setDitv1l`, `setDitv1r` (generalized) +- in `mathcomp_extra.v`: + + lemmas `divDl_ge0`, `divDl_le1` + + mixin `Zmodule_isSubNormed` + + structure `SubNormedZmodule`, notation `subNormedZmodType` -- 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` +- in `unstable.v`: + + lemmas `divD_onem` ### Renamed From ad937443ea3922ef76ce823f7a44a8a6c4a77100 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 3 May 2026 01:09:30 +0900 Subject: [PATCH 26/35] fix changelog --- CHANGELOG_UNRELEASED.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index de330aadb7..bf1d417258 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -230,6 +230,21 @@ - in `unstable.v`: + lemmas `divD_onem` +### Changed + +- moved from `measurable_structure.v` to `classical_sets.v`: + + definition `preimage_set_system` + + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, + `preimage_set_system_id` + +- moved from `topology_structure.v` to `filter.v`: + + lemma `continuous_comp` (and generalized) + +- in `numfun.v`: + + `fune_abse` renamed to `funeposDneg` and direction of the equality changed + + `funeposneg` renamed to `funeposBneg` and direction of the equality changed + + `funeD_posD` renamed to `funeDB` and direction of the equality changed + ### Renamed - in `tvs.v`: From 90d57af4dac494952a01e78c50225cb4f2b95475 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 3 May 2026 11:25:00 +0900 Subject: [PATCH 27/35] all_ssreflect -> all_{boot,order} --- theories/functional_analysis/hahn_banach_theorem.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index eb0a1acfb7..786b1ebad0 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -1,5 +1,5 @@ From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_boot all_order all_algebra. From mathcomp Require Import interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. @@ -32,8 +32,8 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import numFieldNormedType.Exports. Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldNormedType.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. From 11454eff31efe9826f68ae333a249608f5c35337 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 3 May 2026 12:26:11 +0900 Subject: [PATCH 28/35] trying to green CI --- CHANGELOG_UNRELEASED.md | 1 - classical/mathcomp_extra.v | 12 ----------- .../functional_analysis/hahn_banach_theorem.v | 21 +++++++++++++++++++ 3 files changed, 21 insertions(+), 13 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index bf1d417258..82b73e1f46 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -225,7 +225,6 @@ - in `mathcomp_extra.v`: + lemmas `divDl_ge0`, `divDl_le1` + mixin `Zmodule_isSubNormed` - + structure `SubNormedZmodule`, notation `subNormedZmodType` - in `unstable.v`: + lemmas `divD_onem` diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 674ea6c198..455cadd19d 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -112,15 +112,3 @@ Proof. move: s0; rewrite le0r => /predU1P [->|s0]; first by rewrite mul0r. by rewrite ler_pdivrMr ?mul1r ?lerDl // ltr_wpDr. Qed. - -HB.mixin Record Zmodule_isSubNormed (R : numDomainType) - (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 -}. - -#[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_isSubNormed R V S U }. diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 786b1ebad0..ef2ee6c2e3 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -40,6 +40,27 @@ Local Open Scope ring_scope. Local Open Scope convex_scope. Local Open Scope real_scope. +HB.mixin Record Zmodule_isSubNormed (R : numDomainType) + (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 +}. + +(* couldn't be put in mathcomp_extra.v, error: + +Error: +You must declare the hierarchy bottom-up or add a missing join. +There are two ways out: +- declare structure SubNormedZmodule before structure Num.SubNormedZmodule if Num.SubNormedZmodule inherits from it; +- declare an additional structure that inherits from both Num.SemiNormedZmodule and SubType and from which SubNormedZmodule and/or Num.SubNormedZmodule inherit. + +*) +#[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_isSubNormed R V S U }. + HB.mixin Record isSubNbhs (V : nbhsType) (S : pred V) U & SubChoice V S U & Nbhs U := { continuous_valE : continuous (val : U -> V) From 75003cbaaf0997fb2403a76491af926f6d5d6c39 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 8 May 2026 09:32:08 +0900 Subject: [PATCH 29/35] dummy structure to cheat the CI --- .../functional_analysis/hahn_banach_theorem.v | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index ef2ee6c2e3..b7e3606764 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -55,10 +55,17 @@ There are two ways out: - declare an additional structure that inherits from both Num.SemiNormedZmodule and SubType and from which SubNormedZmodule and/or Num.SubNormedZmodule inherit. *) + +HB.mixin Record isTmp (R : numDomainType) (V : normedZmodType R) (S : pred V) + (U : Type) := + { + field_tmp : True +}. + #[short(type="subNormedZmodType")] -HB.structure Definition SubNormedZmodule (R : numDomainType) +HB.structure Definition SubNormedZmodule_tmp (R : numDomainType) (V : normedZmodType R) (S : pred V) := - { U of SubChoice V S U & Num.NormedZmodule R U & GRing.SubZmodule V S U + { U of @isTmp R V S U & SubChoice V S U & Num.NormedZmodule R U & GRing.SubZmodule V S U & Zmodule_isSubNormed R V S U }. HB.mixin Record isSubNbhs @@ -321,7 +328,7 @@ Fail HB.end. 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 & @SubConvexTvs R V S U}. + & @SubNormedZmodule_tmp(*Zmodule_isSubSemiNormed*) R V S U & @SubConvexTvs R V S U}. Section filter_ent. @@ -388,6 +395,10 @@ but then we have Fail Check (U : pseudometricnormedzmodtype R) and Fail Check (U *) Check (U : normedModType R). +Let tmp_tmp : True. Proof. by []. Qed. + +HB.instance Definition _ := @isTmp.Build R V S U Logic.I. + Let normu_valE : forall x, @Num.norm _ V ((val : U -> V) x) = @Num.norm _ U x. Proof. by []. Qed. From bfce795b86b534df169c3c19ec2552c4e5bb0ebd Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 9 May 2026 18:26:39 +0900 Subject: [PATCH 30/35] add doc - more cleaning - rm unused def - rm duplicate - mv MC 2.6.0 structure to extra --- CHANGELOG_UNRELEASED.md | 1 + classical/mathcomp_extra.v | 20 ++ .../functional_analysis/hahn_banach_theorem.v | 337 ++++++------------ 3 files changed, 134 insertions(+), 224 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 82b73e1f46..059698424a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -225,6 +225,7 @@ - in `mathcomp_extra.v`: + lemmas `divDl_ge0`, `divDl_le1` + mixin `Zmodule_isSubNormed` + + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge) - in `unstable.v`: + lemmas `divD_onem` diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 455cadd19d..13d35b6540 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -112,3 +112,23 @@ Proof. move: s0; rewrite le0r => /predU1P [->|s0]; first by rewrite mul0r. by rewrite ler_pdivrMr ?mul1r ?lerDl // ltr_wpDr. Qed. + +HB.mixin Record Zmodule_isSubNormed (R : numDomainType) + (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 +}. + +(* SubNormedZmodule will appear in MC 2.6.0. + However, just duplicating it here causes an HB error in the CI with MC 2.6.0. + We therefore reproduce it with a different name and add a dummy + mixin to it to satisfy HB. + This will be removed when dropping support for MC 2.5.0 *) +HB.mixin Record isTmp (R : numDomainType) (V : normedZmodType R) (S : pred V) + (U : Type) := { field_tmp : True }. + +#[short(type="subNormedZmodType")] +HB.structure Definition SubNormedZmodule_tmp (R : numDomainType) + (V : normedZmodType R) (S : pred V) := + { U of @isTmp R V S U & SubChoice V S U & Num.NormedZmodule R U & + GRing.SubZmodule V S U & Zmodule_isSubNormed R V S U }. diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index b7e3606764..c8f03968d9 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -17,12 +17,38 @@ From mathcomp Require Import topology convex reals normedtype. (* linear continuous function on a subspace to the whole NormedModule. *) (* *) (* ``` *) -(* Module Lingraph == definitions on linear relations, thought of as *) -(* graph of functions *) -(* Module HahnBanachZorn == defintion of the type Zorntype of linear *) -(* functional graphs, bounded by a convex function *) -(* and extending to the whole space a given linear *) -(* graph. *) +(* isSubNbhs V S U == interface that states the continuity of val *) +(* for U which has a subChoiceType and a *) +(* nbhsType *) +(* subNbhsType V S == structure that extends a *) +(* subChoiceType/nbhsType with the isSubNbhs *) +(* interface *) +(* subTopologicalType V S == join of topologicalType and subNbhsType *) +(* subConvexTvsType R V S == join of subTopologicalType, convexTvsType, *) +(* and subLmoduleType *) +(* sub_initial_topology V S U == sub-initial topology generated by the *) +(* \val : U -> V *) +(* U has type subChoiceType S with S : pred V. *) +(* This is a subTopologicalType when V is *) +(* endowed with a topology. *) +(* This is a subConvexTvsType when V is *) +(* endowed with a convexTvsType (and when U is *) +(* subLmodType). *) +(* subNormedModType R V S == join of *) +(* SubChoice *) +(* NormedModule *) +(* SubLmodule *) +(* SubNormedZmodule *) +(* SubConvexTvs *) +(* SubLmodule_isSubNormedmodule R V S == factory that builds a *) +(* SubNormedmodule given a SubLmodule over a *) +(* normedModType *) +(* Module LinearGraph == definitions on linear relations, thought of *) +(* as graph of functions *) +(* Module HahnBanachZorn == defintion of the type zorn_type of linear *) +(* functional graphs, bounded by a convex *) +(* function and extending to the whole space a *) +(* given linear graph. *) (* ``` *) (* *) (******************************************************************************) @@ -40,12 +66,6 @@ Local Open Scope ring_scope. Local Open Scope convex_scope. Local Open Scope real_scope. -HB.mixin Record Zmodule_isSubNormed (R : numDomainType) - (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 -}. - (* couldn't be put in mathcomp_extra.v, error: Error: @@ -56,18 +76,6 @@ There are two ways out: *) -HB.mixin Record isTmp (R : numDomainType) (V : normedZmodType R) (S : pred V) - (U : Type) := - { - field_tmp : True -}. - -#[short(type="subNormedZmodType")] -HB.structure Definition SubNormedZmodule_tmp (R : numDomainType) - (V : normedZmodType R) (S : pred V) := - { U of @isTmp R V S U & 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 & SubChoice V S U & Nbhs U := { continuous_valE : continuous (val : U -> V) @@ -81,25 +89,24 @@ HB.structure Definition SubNbhs (V : nbhsType) (S : pred V) := HB.structure Definition SubTopological (V : topologicalType) (S : pred V) := {U of SubNbhs V S U & Topological U}. -(* NB: rename to sub_init_topo? *) -Definition topU (V : Type) (S : pred V) (U : subChoiceType S) : Type - := initial_topology (\val : U -> V). +Definition sub_initial_topology (V : Type) (S : pred V) (U : subChoiceType S) + : Type := initial_topology (\val : U -> V). Section SubType_isSubTopological. Context (V : topologicalType) (S : pred V) (U : subChoiceType S). -Local Notation topU := (topU U). -HB.instance Definition _ := SubChoice.on topU. -HB.instance Definition _ := Nbhs.on topU. -HB.instance Definition _ := Topological.on topU. +Local Notation T := (sub_initial_topology U). +HB.instance Definition _ := SubChoice.on T. +HB.instance Definition _ := Nbhs.on T. +HB.instance Definition _ := Topological.on T. -Let top_continuous_valE : continuous (val : topU -> V). +Let top_continuous_valE : continuous (val : T -> V). Proof. exact: initial_continuous. Qed. -HB.instance Definition _ := @isSubNbhs.Build V S topU top_continuous_valE. +HB.instance Definition _ := @isSubNbhs.Build V S T top_continuous_valE. -Check (topU : subNbhsType S). -Check (topU : subTopologicalType S). +Check T : subNbhsType S. +Check T : subTopologicalType S. End SubType_isSubTopological. @@ -109,28 +116,25 @@ HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) { 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) : +(*Lemma add_continuous (K : numDomainType) (E : convexTvsType K) : continuous (fun x : E * E => x.1 + x.2). -Proof. exact: add_continuous. Qed. +Proof. exact: add_continuous. Qed.*) Section lmodule_isSubTvs. -Context (R : numFieldType) (V : convexTvsType R) (S : pred V) (U: subLmodType S). +Context (R : numFieldType) (V : convexTvsType R) (S : pred V) (U : subLmodType S). -Local Notation topU := (topU U). +Local Notation topU := (sub_initial_topology U). 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 : subTopologicalType S. 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 : uniformType). -Check (topU : subLmodType S). +Check topU : uniformType. +Check topU : subLmodType S. Let add_sub: continuous (fun x : topU * topU => x.1 + x.2). Proof. @@ -150,7 +154,7 @@ Qed. HB.instance Definition _ := @PreTopologicalNmodule_isTopologicalNmodule.Build topU add_sub. -Check (topU : TopologicalNmodule.type). +Check topU : TopologicalNmodule.type. Let opp_sub : continuous (-%R : topU -> topU). Proof. @@ -164,7 +168,7 @@ Qed. HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build topU opp_sub. -Check (topU : TopologicalZmodule.type). +Check topU : TopologicalZmodule.type. Let scale_sub : continuous (fun z : R^o * topU => z.1 *: z.2). Proof. @@ -184,10 +188,10 @@ Qed. HB.instance Definition _ := TopologicalZmodule_isTopologicalLmodule.Build R topU scale_sub. -Check (topU : TopologicalLmodule.type R). +Check topU : TopologicalLmodule.type R. Let locally_convex_sub : exists2 B : set_system topU, - (forall b, b \in B -> convex_set b) & basis B. + (forall b, b \in B -> convex_set b) & basis B. Proof. have [B convexB [openB/= genB]] := @locally_convex R V. exists [set a | exists2 b, B b & \val @^-1` b = a]. @@ -225,116 +229,20 @@ Check (topU : subLmodType S). 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. - -#[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 _ := Topological.on topU. -HB.instance Definition _ := Nbhs.on topU. -HB.instance Definition _ := GRing.Lmodule.on topU. -Check (topU : SubChoice.type S). -Check (topU : pointedType). -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). -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 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 *) - -#[local] Lemma continuous_valE : continuous (val : topU -> V). -Proof. exact: initial_continuous. Qed. - -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). -Check (topU : uniformType). -HB.about subConvexTvsType. -Fail Check (topU : subConvexTvsType S). - - -Fail 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_tmp(*Zmodule_isSubSemiNormed*) R V S U & @SubConvexTvs R V S U}. + & @SubNormedZmodule_tmp(*Zmodule_isSubSemiNormed*) R V S U & + @SubConvexTvs R V S U}. Section filter_ent. Import pseudoMetric_from_normedZmodType. -Lemma ent_xsection_filter {R : realFieldType} (U : normedZmodType R) x : Filter +Global Instance ent_xsection_filter {R : realFieldType} (U : normedZmodType R) x : Filter [set P | exists2 A : set (pseudoMetric_normed U * pseudoMetric_normed U), pseudoMetric_from_normedZmodType.ent A & xsection A x `<=` P]. Proof. @@ -385,18 +293,16 @@ 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 @Num.Zmodule_isNormed.Build, this command check -but then we have Fail Check (U : pseudometricnormedzmodtype R) and Fail Check (U -: normedModtype R). +(* 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). *) -Check (U : normedModType R). - -Let tmp_tmp : True. Proof. by []. Qed. +Check U : pseudoMetricNormedZmodType R. +Check U : normedModType R. +(* hack, produces no instance with MathComp 2.5.0, + can be remove when supporting MC >= 2.6.0 *) HB.instance Definition _ := @isTmp.Build R V S U Logic.I. Let normu_valE : forall x, @Num.norm _ V ((val : U -> V) x) = @Num.norm _ U x. @@ -405,7 +311,7 @@ Proof. by []. Qed. HB.instance Definition _ := Zmodule_isSubNormed.Build _ _ _ U normu_valE. (* TODO : why is the U necessary ?*) -Check (U : subNormedZmodType S). +Check U : subNormedZmodType S. Let continuous_valE : continuous (val : U -> V). Proof. @@ -413,7 +319,6 @@ move=> /= x. rewrite /continuous_at. set rhs := (X in _ --> X). apply/cvgrPdist_le => //=. - exact: ent_xsection_filter. move=> e e0; near=> t. rewrite -GRing.valN -GRing.valD norm_valE. by near: t; exact: cvgr_dist_le e e0. @@ -421,18 +326,18 @@ Unshelve. all: by end_near. Qed. HB.instance Definition _ := isSubNbhs.Build _ _ U continuous_valE. -Check (U : subConvexTvsType S). +Check U : subConvexTvsType S. -Check (U : subNormedModType S). +Check U : subNormedModType S. HB.instance Definition _ := SubLmodule_isSubNormedmodule.Build _ _ _ U. HB.end. (* TODO : use a lightweight factory to make every subLmodType a subnormedmodtype *) -Module Lingraph. -Section Lingraphsec. -Variables (R : numDomainType) (V : lmodType R). +Module LinearGraph. +Section linear_graph. +Context (R : numDomainType) (V : lmodType R). Definition graph := V -> R -> Prop. @@ -440,38 +345,26 @@ 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. +Hypothesis lf : 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. +by move=> fxr; have := lf (-1) fxr fxr; rewrite scaleN1r mulN1r !subrr. 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. -exact: lrf. -Qed. +Lemma lingraphZ x r l : f x r -> f (l *: x) (l * r). +Proof. by move=> fxr; have := lf l (lingraph_00 fxr) fxr; rewrite !add0r. Qed. -Definition add_line f w a := fun v r => exists (v' : V) (r' lambda : R), - [/\ f v' r', v = v' + lambda *: w & r = r' + lambda * a]. +Lemma lingraphD x1 x2 r1 r2 : f x1 r1 -> f x2 r2 -> f (x1 - x2) (r1 - r2). +Proof. by move=> f1 f2; have := lf (-1) f1 f2; rewrite !scaleN1r mulN1r. Qed. -End Lingraphsec. -End Lingraph. +End linear_graph. +End LinearGraph. Module HahnBanachZorn. Section HahnBanachZorn. -Import Lingraph. -Variables (R : realType) (V : lmodType R) (F : pred V). +Import LinearGraph. +Context (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. @@ -486,22 +379,20 @@ 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]. + [/\ 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}. Implicit Types z : zorn_type. -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 -> ->]. +- 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. @@ -528,31 +419,30 @@ 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. -have [[w Aw] | eA] := lem (exists a, A a); last first. +move=> A Amax. +have [[w Aw]|eA] := lem (exists a, A a); last first. by exists zphi => a Aa; absurd: 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]. - 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. + have [|] : Rbool a b \/ Rbool b a by exact: Amax. + - rewrite /Rbool /RboolP /zornS. + case: b Ab bvr2 {Aa} => 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; exact: fs1. + - rewrite /Rbool /RboolP /zornS. + case: a Aa avr1 {Ab} => s1 [fs1 _ _ _] /= _ s1vr1 /asboolP ecbs1. + by move/ecbs1: bvr2; exact: 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 {sc12 Aa1 a1} {}c1 : carrier a2 v1 r1 by exact: sc12. - by exists a2 => //; case: a2 {Aa2} c2 c1 => c /= [_ hl _ _] *; exact: hl. + by exists a2 => //; case: a2 {Aa2} c2 c1 => c /= [_ + _ _] *; exact. - have {sc21 Aa2 a2} {}c2 : carrier a1 v2 r2 by exact: 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. + by exists a1 => //; case: a1 {Aa1} c2 c1 => c /= [_ + _ _] *; exact. +have g_majp : le_graph p g by move=> v r [[c/= [fs1 ls1 ms1 ps1]]]/= _ => /ms1. have g_prol : extend_graph g. - by move=> *; exists w => //; case: w Aw => [c [_ _ _ hp]] _ //=; exact: hp. + by move=> *; exists w => //; case: w Aw => [c [_ _ _ +]] _ //=; exact. 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. @@ -560,11 +450,8 @@ 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 +(* 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 v : exists2 ze, zornS z ze & exists r, (carrier ze) v r. Proof. have [[r rP]|] := lem (exists r, carrier z v r). @@ -596,7 +483,7 @@ have [a aP] : exists a, forall (x : V) (r lambda : R), c x r -> 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. + by rewrite !scalerDr addrCA scalerN scalerA (mulrC s) -scalerA addrK. set l := t / _; set m := s / _. rewrite [leLHS](_ : _ = l * r1 + m * r2). by rewrite mulrDl ![_ * _ / _]mulrAC. @@ -669,18 +556,21 @@ exists (ZornType z'_spec) => //=; exists a, 0, 0, 1. by rewrite !add0r mul1r scale1r. Qed. -Let tot_g v : exists r, carrier g v r. +Hypothesis gP : forall z, zornS g z -> z = g. + +Let total_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). +Lemma hahn_banach_witness : + exists h : V -> R, forall v r, carrier g v r <-> h v = r. Proof. -have [h hP] := choice tot_g. +have [h hP] := choice total_g. exists h => v r; split=> [|<-//]. -case: g gP tot_g hP => c /= [fg lg mg pg] => gP' tot_g' hP cvr. -by have -> // := fg v r (h v). +move: g gP total_g hP => [c /= [fg _ _ _]] _ _ hP cvr. +by rewrite (fg v r (h v)). Qed. End HahnBanachZorn. @@ -688,14 +578,13 @@ End HahnBanachZorn. (* NB: could go to convex.v *) Section hahn_banach. -Import Lingraph. +Import LinearGraph. Import HahnBanachZorn. -(* Now we prove HahnBanach on functions*) +(* 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). - +Context {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. @@ -706,14 +595,14 @@ Theorem hahn_banach_extension : exists2 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 /(hb_witness p_cvx)[g gP]] := zornS_ex f_bounded_by_p. +have [z /(hahn_banach_witness p_cvx)[g gP]] := zornS_ex f_bounded_by_p. have scalg : linear_for *%R g. case: z gP => [c [_ ls1 _ _]] /= gP. have addg : zmod_morphism g. - by move=> w1 w2; apply/gP; apply: lingraph_add => //; apply/gP. + by move=> w1 w2; apply/gP; apply: lingraphD => //; apply/gP. suff scalg : scalable_for *%R g. by move=> a u v; rewrite -gP -(addrC v) -(addrC (g v)); apply/ls1; exact/gP. - by move=> w l; apply/gP; apply: lingraph_scale => //; exact/gP. + by move=> w l; apply/gP; apply: lingraphZ => //; exact/gP. pose lg := GRing.isLinear.Build _ _ _ _ g scalg. pose g' : {linear V -> R | *%R} := HB.pack g lg. exists g'. @@ -723,7 +612,7 @@ Qed. End hahn_banach. -(* TODO : to define on tvs, characterize the topology of a tvs via its pseudonorms, +(* 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. From bd88ff7a2b283af5fd6eb4d33df1680b1c77e70c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 9 May 2026 18:31:49 +0900 Subject: [PATCH 31/35] fix changelog --- CHANGELOG_UNRELEASED.md | 62 ++++------------------------------------- 1 file changed, 6 insertions(+), 56 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 059698424a..2c44a19188 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -130,41 +130,14 @@ + definition `preimage_set_system` + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, `preimage_set_system_id` -- in `functions.v`: - + lemmas `linfunP`, `linfun_eqP` - + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }` -- 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 `mathcomp_extra.v`: + + lemmas `divDl_ge0`, `divDl_le1` + + mixin `Zmodule_isSubNormed` + + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge) -- in `separation_axioms.v`: - + lemmas `limit_point_closed` -- in `convex.v`: - + lemma `convex_setW` -- in `convex.v`: - + lemma `convexW` +- in `unstable.v`: + + lemmas `divD_onem` ### Changed @@ -219,32 +192,9 @@ + lemmas `Radon_NikodymE`, `Radon_Nikodym_fin_num`, `Radon_Nikodym_integrable`, `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`, `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule` - -- in set_interval.v - + `setUitv1`, `setU1itv`, `setDitv1l`, `setDitv1r` (generalized) -- in `mathcomp_extra.v`: - + lemmas `divDl_ge0`, `divDl_le1` - + mixin `Zmodule_isSubNormed` - + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge) - -- in `unstable.v`: - + lemmas `divD_onem` ### Changed -- moved from `measurable_structure.v` to `classical_sets.v`: - + definition `preimage_set_system` - + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, - `preimage_set_system_id` - -- moved from `topology_structure.v` to `filter.v`: - + lemma `continuous_comp` (and generalized) - -- in `numfun.v`: - + `fune_abse` renamed to `funeposDneg` and direction of the equality changed - + `funeposneg` renamed to `funeposBneg` and direction of the equality changed - + `funeD_posD` renamed to `funeDB` and direction of the equality changed - ### Renamed - in `tvs.v`: From c5fdd94e206ef07e2ce83e449ca0a4fde3527326 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 9 May 2026 18:32:37 +0900 Subject: [PATCH 32/35] fix changelog --- CHANGELOG_UNRELEASED.md | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2c44a19188..cf3ec3e84e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -93,6 +93,14 @@ + lemma `is_diff_mx` + instance `is_diff_mx` +- in `mathcomp_extra.v`: + + lemmas `divDl_ge0`, `divDl_le1` + + mixin `Zmodule_isSubNormed` + + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge) + +- in `unstable.v`: + + lemmas `divD_onem` + ### Changed - moved from `measurable_structure.v` to `classical_sets.v`: @@ -131,16 +139,6 @@ + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, `preimage_set_system_id` -- in `mathcomp_extra.v`: - + lemmas `divDl_ge0`, `divDl_le1` - + mixin `Zmodule_isSubNormed` - + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge) - -- in `unstable.v`: - + lemmas `divD_onem` - -### Changed - - moved from `topology_structure.v` to `filter.v`: + lemma `continuous_comp` (and generalized) From ccc86e8a7ab6dc6de05721eaebf3d3b86f02b30b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 9 May 2026 18:33:51 +0900 Subject: [PATCH 33/35] fix changelog --- CHANGELOG_UNRELEASED.md | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index cf3ec3e84e..e935b4f277 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -93,20 +93,6 @@ + lemma `is_diff_mx` + instance `is_diff_mx` -- in `mathcomp_extra.v`: - + lemmas `divDl_ge0`, `divDl_le1` - + mixin `Zmodule_isSubNormed` - + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge) - -- in `unstable.v`: - + lemmas `divD_onem` - -### Changed - -- moved from `measurable_structure.v` to `classical_sets.v`: - + definition `preimage_set_system` - + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, - `preimage_set_system_id` - in `functions.v`: + lemmas `linfunP`, `linfun_eqP` + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }` @@ -131,9 +117,22 @@ - new files `signed_measure.v` and `radon_nikodym.v` + with the contents of `charge.v` (deprecated) - + +- in `mathcomp_extra.v`: + + lemmas `divDl_ge0`, `divDl_le1` + + mixin `Zmodule_isSubNormed` + + mixin `isTmp` and structure `SubNormedZmodule_tmp` (temporary kludge) + +- in `unstable.v`: + + lemmas `divD_onem` + ### Changed +- moved from `measurable_structure.v` to `classical_sets.v`: + + definition `preimage_set_system` + + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, + `preimage_set_system_id` + - moved from `measurable_structure.v` to `classical_sets.v`: + definition `preimage_set_system` + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, From 5adf446d8556c0614e0246352ebfe2a95646d884 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 9 May 2026 18:34:26 +0900 Subject: [PATCH 34/35] fix changelog --- CHANGELOG_UNRELEASED.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e935b4f277..59912dcdcc 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -189,8 +189,6 @@ + lemmas `Radon_NikodymE`, `Radon_Nikodym_fin_num`, `Radon_Nikodym_integrable`, `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`, `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule` - -### Changed ### Renamed From d0eebda87b678ffb1419a3b224b8dffa5db76ddd Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sat, 9 May 2026 20:58:33 +0900 Subject: [PATCH 35/35] deleting comments --- .../functional_analysis/hahn_banach_theorem.v | 52 ------------------- 1 file changed, 52 deletions(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index c8f03968d9..ac87f6dd00 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -105,9 +105,6 @@ Proof. exact: initial_continuous. Qed. HB.instance Definition _ := @isSubNbhs.Build V S T top_continuous_valE. -Check T : subNbhsType S. -Check T : subTopologicalType S. - End SubType_isSubTopological. #[short(type="subConvexTvsType")] @@ -115,26 +112,12 @@ 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). Local Notation topU := (sub_initial_topology U). -Check topU : nbhsType. -Check topU : subChoiceType S. -Check topU : topologicalType. -Check topU : subTopologicalType S. -Check topU : subNbhsType S. -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. Let add_sub: continuous (fun x : topU * topU => x.1 + x.2). Proof. @@ -154,7 +137,6 @@ Qed. HB.instance Definition _ := @PreTopologicalNmodule_isTopologicalNmodule.Build topU add_sub. -Check topU : TopologicalNmodule.type. Let opp_sub : continuous (-%R : topU -> topU). Proof. @@ -168,8 +150,6 @@ Qed. HB.instance Definition _ := TopologicalNmodule_isTopologicalZmodule.Build topU opp_sub. -Check topU : TopologicalZmodule.type. - Let scale_sub : continuous (fun z : R^o * topU => z.1 *: z.2). Proof. apply: continuous_comp_initial => - [] /= x /= y. @@ -188,8 +168,6 @@ Qed. HB.instance Definition _ := TopologicalZmodule_isTopologicalLmodule.Build R topU scale_sub. -Check topU : TopologicalLmodule.type R. - Let locally_convex_sub : exists2 B : set_system topU, (forall b, b \in B -> convex_set b) & basis B. Proof. @@ -214,20 +192,8 @@ by move=> y dy; apply: ba; rewrite -cb; exact: dc. Qed. 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). - -(*HB.instance Definition _ := ConvexTvs.on topU.*) HB.instance Definition _ := GRing.SubLmodule.on topU. -Check (topU : convexTvsType R). -Check (topU : subLmodType S). -Check (topU : subConvexTvsType S). - End lmodule_isSubTvs. (* TODO: moved to normed_module.v *) @@ -293,13 +259,6 @@ Proof. by rewrite /normu GRing.valZ; exact: normrZ. Qed. HB.instance Definition _ := @Lmodule_isNormed.Build R U normu ler_normuD normruZ normru0_eq0. -(* 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). - *) -Check U : pseudoMetricNormedZmodType R. -Check U : normedModType R. (* hack, produces no instance with MathComp 2.5.0, can be remove when supporting MC >= 2.6.0 *) @@ -309,9 +268,6 @@ Let 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. Let continuous_valE : continuous (val : U -> V). Proof. @@ -326,10 +282,6 @@ Unshelve. all: by end_near. Qed. HB.instance Definition _ := isSubNbhs.Build _ _ U continuous_valE. -Check U : subConvexTvsType S. - -Check U : subNormedModType S. - HB.instance Definition _ := SubLmodule_isSubNormedmodule.Build _ _ _ U. HB.end. @@ -612,15 +564,11 @@ Qed. End hahn_banach. -(* 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}). -(*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 : F', g (val x) = f x. Proof.