From 8af29ccbfa51bce14ee3e3b468136872d2bf13a6 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 20 Mar 2026 11:14:19 +0900 Subject: [PATCH 01/17] adding seminorms to tvs adding also initial fam topology, gauge functions, and subbase 0basis Co-authored-by: Reynald Affeldt Co-authored-by: Cyril Cohen --- CHANGELOG_UNRELEASED.md | 62 + CHANGELOG_UNRELEASED_new.md | 52 + theories/hahn_banach_theorem.v | 428 +++++++ theories/normedtype_theory/tvs.v | 1001 ++++++++++++++++- theories/topology_theory/initial_topology.v | 148 ++- theories/topology_theory/topology_structure.v | 14 +- 6 files changed, 1660 insertions(+), 45 deletions(-) create mode 100644 CHANGELOG_UNRELEASED_new.md create mode 100644 theories/hahn_banach_theorem.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0023dbb5e0..2a672e4825 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -173,6 +173,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) @@ -226,6 +263,31 @@ `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` + + structure `SubNormedZmodule`, notation `subNormedZmodType` + +- 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`: diff --git a/CHANGELOG_UNRELEASED_new.md b/CHANGELOG_UNRELEASED_new.md new file mode 100644 index 0000000000..49464d2a9a --- /dev/null +++ b/CHANGELOG_UNRELEASED_new.md @@ -0,0 +1,52 @@ +# Changelog (unreleased) + +## [Unreleased] + +### Added + +- 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` + +- in `filter.v`: + + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType` + +- in `topology_structure.v`: + + structure `SubTopological`, notation `subTopologicalType` + +- in `tvs.v`: + + structure `SubConvexTvs`, notation `subConvexTvsType` + +- in `normed_module.v`: + + structure `SubNormedModule`, notation `subNormedModType` + + instance `ent_xsection_filter` + + factory `SubLmodule_isSubNormedmodule` + +- new file `hahn_banach_theorem.v`: + + module `LinearGraph` + * definitions `graph`, `linear_graph` + * lemmas `lingraph_00`, `lingraphZ`, `lingraphD` + + module `HahnBanachZorn` + * definitions `extend_graph`, `le_graph`, `functional_graph`, `le_extend_graph` + * record `zorn_type` + * definition `zphi` + * lemma `zorn_type_eq` + * definition `zornS` + * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness` + + theorems `hahn_banach_extension`, `hahn_banach_extension_normed` + +### Deprecated + +### Renamed + +### Generalized + +### Removed + + + + 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 41126a781d..ca0a8bcc09 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -1,11 +1,11 @@ -(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From HB Require Import structures. +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector. From mathcomp Require Import interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality. -From mathcomp Require Import convex set_interval reals topology num_normedtype. +From mathcomp Require Import convex set_interval reals initial_topology topology num_normedtype. From mathcomp Require Import pseudometric_normed_Zmodule. (**md**************************************************************************) @@ -78,6 +78,7 @@ From mathcomp Require Import pseudometric_normed_Zmodule. (* and F are convexTvs. *) (******************************************************************************) + Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'" (at level 0, U at level 98, V at level 99, format "{ 'linear_continuous' U -> V | s }"). @@ -96,6 +97,99 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. + + +Module DDist. +Section dDist. +Context (R: numDomainType) (n : nat). + +Record d := { + t :> n.-tuple R ; + le1 : \sum_(a <- t) `|a| <= 1}. + +End dDist. +End DDist. +Coercion DDist.t : DDist.d >-> tuple_of. + + +Reserved Notation "{ 'ddist' n }" (at level 0, format "{ 'ddist' n }"). +Reserved Notation "R '.-ddist' n" (at level 2, format "R '.-ddist' n"). + +Notation "R '.-ddist' n" := (DDist.d R n%type). +Notation "{ 'ddist' n }" := (_.-ddist n). + + +Section absolutely_convex. +Context (K : numDomainType) (V : lmodType K). + +Definition balanced_set (A : set V) := (forall r, `|r| <= 1 -> (fun x => r *: x) @`A `<=` A). + +Definition absolutely_convex_set (A : set V) := convex_set A /\ balanced_set A. + +Definition absorbing_set (A : set V) := forall x : V, exists a, exists2 r, (a \in A) & (x = r *:a). + +Definition pabsorbing_set (A : set V) := forall x : V, exists2 r, ( 0< r) & r*: x \in A. + +Definition absolutely_convex_hull (A : set V) := smallest absolutely_convex_set A. + + + +(* TODO : move to convex.v *) +Lemma setI_convex : setI_closed (@convex_set K V). +Proof. +move=> A B cA cB x y r /[!inE] -[xA xB] [yA yB]; split; apply/set_mem. +by apply/cA; apply/mem_set. +by apply/cB; apply/mem_set. +Qed. + +Lemma bigcap_convex : bigcap_closed (@convex_set K V). +Proof. +move=> H Hconv x y r /[!inE] /= Hx Hy A /[dup] HA /Hconv /(_ _ _ _ _ _ )/set_mem; apply. +- by apply: mem_set; apply: Hx. +- by apply: mem_set; apply: Hy. +Qed. + +Lemma setI_balanced : setI_closed balanced_set. +Proof. +move=> A B bA bB x r /=; rewrite subsetI; split => z /= [t [At Bt] <-]. +- by apply: (bA _ r) => //; exists t. +- by apply: (bB _ r) => //; exists t. +Qed. + +Lemma bigcap_balanced : bigcap_closed balanced_set. +Proof. +move=> H Hconv /= r r1; apply: sub_bigcap => A HA x /= [t Ht <-]. +apply: (Hconv A HA r r1) => //. +by exists t; first by apply: Ht. +Qed. + +Lemma absolutely_convex_hull_set (A : set V) : absolutely_convex_set (absolutely_convex_hull A). +Proof. +apply: bigcap_closed_smallest => H Habs. +split. +- by apply: bigcap_convex; apply: (subset_trans Habs); apply: subIsetl. +- by apply: bigcap_balanced; apply: (subset_trans Habs); apply: subIsetr. +Qed. + +Lemma absolutely_convex_hullE (A : set V): + absolutely_convex_hull A = [set a | exists n (t: {ddist n}) (l : n.-tuple V), + [set` l] `<=` A /\ a = \sum_(i < n) t`_i *: l`_i]. +Abort. + +Lemma absolutely_convex_hull_subset (A : set V): A `<=` absolutely_convex_hull A. +Proof. +by exact: sub_gen_smallest. +Qed. + +Lemma absolutely_convex0 (B : set V) : B !=set0 -> absolutely_convex_set B -> B 0. +Proof. +move => [] x Bx [] _ /(_ 0); rewrite normr0 ler01 // => /(_ isT) /(_ 0); apply. +by exists x; rewrite //= scale0r. +Qed. + +End absolutely_convex. + + (* HB.structure Definition PointedNmodule := {M of Pointed M & GRing.Nmodule M}. *) (* HB.structure Definition PointedZmodule := {M of Pointed M & GRing.Zmodule M}. *) (* HB.structure Definition PointedLmodule (K : numDomainType) := *) @@ -392,8 +486,10 @@ HB.end. HB.mixin Record Uniform_isConvexTvs (R : numDomainType) E & Uniform E & GRing.Lmodule R E := { locally_convex : exists2 B : set_system E, - (forall b, b \in B -> convex_set b) & basis B + (forall b, b \in B -> absolutely_convex_set b) & (nbhs_basis 0) B }. +(* absolutely_convex instead of convex *) +(*filter_from [set U | B U /\ U 0] id --> 0. instead of B*) #[short(type="convexTvsType")] HB.structure Definition ConvexTvs (R : numDomainType) := @@ -533,7 +629,7 @@ HB.factory Record PreTopologicalLmod_isConvexTvs (R : numDomainType) E add_continuous : continuous (fun x : E * E => x.1 + x.2) ; scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2) ; locally_convex : exists2 B : set_system E, - (forall b, b \in B -> convex_set b) & basis B + (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B }. HB.builders Context R E & PreTopologicalLmod_isConvexTvs R E. @@ -562,7 +658,7 @@ split; first by exists [set: E]; split; first exact: filter_nbhsT. exists (U `&` V); split => [|xy]. by exists (B `&` C); [exact: open_nbhsI|exact: setISS]. by rewrite !in_setI => /andP[/Bxy-> /Cxy->]. -by move=> P Q PQ [U [HU Hxy]]; exists U; split=> [|xy /Hxy /[!inE] /PQ]. +by move=> P Q PQ [U [HU Hxy]]; exists U; split => [|xy /Hxy /[!inE] /PQ]. Qed. Local Lemma entourage_refl (A : set (E * E)) : @@ -624,15 +720,414 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E entourage_inv entourage_split_ex nbhsE. +(* TO BE DELETED once PR#1974 is merged *) HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build E add_continuous. HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R E scale_continuous. HB.instance Definition _ := Uniform_isConvexTvs.Build R E locally_convex. +(* END TO BE DELETED *) + +HB.end. + + +Notation "A `+ B" := [set x + y | x in A & y in B] (at level 54). +Notation "r `*: B" := [set r *: x | x in B] (at level 54). + +Lemma addsubset (E : zmodType) (A B C D: set E): + A `<=` B -> C `<=` D -> (A `+ C) `<=` (B `+ D). +Proof. +by move=> AB CD z [a /AB Ba [c /CD Dc <-]]; exists a => //; exists c. +Qed. + +Lemma addset0 (E : zmodType) (A: set E): + ([set 0] `+ A) = A. +Proof. +apply/seteqP; split => z /=. + by move=> [+ -> [y]]; rewrite add0r => + + <-. +by move=> Az; exists 0 => //; exists z; rewrite ?add0r. +Qed. + +Lemma addsetI (E : zmodType) (A B : set E) (x : E) : +[set x] `+ (A `&` B) = ([set x] `+ A) `&` ([set x] `+ B). +Proof. +apply/seteqP; split => z. + by move => [r Cr] [y [Ay By] <- {z}]; split => /=; exists r => //; exists y => //. +move => /= [[r ->] [y Ay] <- {z}] [x' ->] [y' By']. +move=> /(congr1 (fun h => h - x)). +rewrite addrAC subrr add0r addrAC subrr add0r => yy'. +rewrite yy' in By' *. +by exists x => //; exists y' => //; rewrite ?yy'; first by split. +Qed. + +Lemma addsubsetA (E : zmodType) p c (D : set E) : + [set p + c] `+ D `<=` [set p] `+ ([set c] `+ D). +Proof. +move=> x/= [y ->{y}] [z Dz <-{x}]. +exists p => //. +exists (c + z) => //. + exists c => //. + by exists z. +by rewrite addrA. +Qed. + +(* TODO : how to make a mixin isConvexTvssat of the following axioms, as open_at0 has to be redefined each time +{ +open_at0 : set_system E; +mem0_setsystem : forall B, open_at0 B -> B (0 : E); +split_setsystem : forall B, open_at0 B -> exists2 C, open_at0 C & ( C `+ C `<=` B); +expand_setsystem : forall B r, open_at0 B -> (0 exists2 U, open_at0 U & (r `*: U `<=` B); +convex_setsystem : forall B, open_at0 B -> convex_set B +}. + +HB.structure Definition ConvexTvsat (R : numDomainType) := {E of GRing.Lmodule R E & isConvexTvsat R E}. +*) + + +HB.factory Record Nbhsbasisat0_isConvexTvs (R: numFieldType) E & GRing.Lmodule R E (*& isConvexTvsat R E*) := { + nbhsbasis_at0 : set_system E ; (*TODO rename to filterbasis_at0*) + nonempty_nbhsbasisat0 : exists U, nbhsbasis_at0 U; + nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V -> + exists2 W, nbhsbasis_at0 W & W `<=` U `&` V ; + mem0_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> B 0 ; + expand_nbhsbasisat0 : forall B r, nbhsbasis_at0 B -> (*0 <= r ->*) + exists2 U, nbhsbasis_at0 U & r `*: U `<=` B ; (* implies circled *) + absorbing_nbhsbasisat0 : forall B , nbhsbasis_at0 B -> pabsorbing_set B; + absconvex_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> absolutely_convex_set B }. + +Definition nbhs_frombasis0 (R : numFieldType) (E : zmodType) + (nbhsbasis_at0 : set_system E) (x : E) := + filter_from [set U | exists2 V, nbhsbasis_at0 V & [set x] `+ V = U] id. +(* +Definition nbhs_fromfilter0 (R: numDomainType) (E : zmodType) (nbhsbasis_at0 : set_system E) (x : E) U := +exists2 V, ((filter_from nbhsbasis_at0 id) V) & ([set x] `+ V `<=` U). +*) + +HB.builders Context R E & Nbhsbasisat0_isConvexTvs R E. + +Local Definition nbhs_fromfilter0 := @nbhs_frombasis0 R E (nbhsbasis_at0). + +Lemma split_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> + exists2 C, nbhsbasis_at0 C & C `+ C `<=` B. +Proof. +move => B /(@expand_nbhsbasisat0 _ (2)) [U fU UB]. +exists U => //. +move => /= x [u] Uu [v] Uv <-. +apply: UB. +exists (2^-1 *: (u+v)); last by by rewrite scalerA mulfV // scale1r. +rewrite scalerDr. +have [convU _] := absconvex_nbhsbasisat0 fU. +have H : (0 : R) <= 2^-1 by []. +have G : (2^-1 : R) <= 1 by rewrite invf_le1 ?lerDl //. +pose r := Itv01 H G. +have := (convU u v r). +rewrite !inE => /(_ Uu Uv); rewrite /conv /=. +suff -> : (2^-1).~ = 2^-1 :> R by []. (* should be a lemma in convex *) +apply: (@mulIf _ 2%:R); rewrite /((_).~) //. +by rewrite mulrBl mulVf // mul1r // addrK. +Qed. + +#[local] Lemma nbhs_filter : forall p : E, ProperFilter (nbhs_fromfilter0 p). +Proof. +rewrite /nbhs_fromfilter0 => p. +apply: filter_from_proper. + apply: filter_from_filter => /=. + have [U fU] := nonempty_nbhsbasisat0. + exists ([set p] `+ U) => //=. + by exists U. + move=> _ _ /= [U0 FU <-] [V0 FV <-]. + have [W FW WUV] := nbhsbasis_at0I FU FV. + exists ([set p] `+ W). + by exists W. + rewrite -addsetI. + exact: addsubset. +move=> _ /= [V FV] <-. +by exists p; exists p => //; exists 0; rewrite ?addr0//; exact: mem0_nbhsbasisat0. +Qed. + +#[local] Lemma nbhs_singleton : forall (p : E) (A : set E), nbhs_fromfilter0 p A -> A p. +Proof. +move=> p A [_/= [C f0C <-]]; apply; exists p => //; exists 0; rewrite ?addr0//. +exact: mem0_nbhsbasisat0. +Qed. + +#[local] Lemma nbhs_nbhs (p : E) (A : set E) : nbhs_fromfilter0 p A -> + nbhs_fromfilter0 p (nbhs_fromfilter0^~ A). +Proof. (* fun x => nbhs_fromfilter0 x A est un voisinage de p *) +rewrite /nbhs_fromfilter0/=. +move=> [B/= [C f0C <- pCA]]. +red. +simpl. +have [D f0D DDC] := split_nbhsbasisat0 f0C. +exists ([set p] `+ D). + by exists D. +move=> _ [/= _] -> [c Cc <-]. +red. +simpl. +exists ([set p + c] `+ D) => //. + by exists D. +apply: (subset_trans _ pCA). +apply: (@subset_trans _ ([set p] `+ ([set c] `+ D))). + exact: addsubsetA. +apply: addsubset => //. +apply: subset_trans DDC. +apply: addsubset => //. +by move=> x ->. +Qed. + +HB.instance Definition _ := @hasNbhs.Build E (nbhs_fromfilter0). + +HB.instance Definition _ := @Nbhs_isNbhsTopological.Build E nbhs_filter nbhs_singleton nbhs_nbhs. + + +#[local] Lemma add_continuous : continuous (fun x : E * E => x.1 + x.2). +Proof. +move=> /= [x1 x2] /= A /= [V] /= [V0 filterV0 <-{V}] VA. +have [W filter0W WV] := split_nbhsbasisat0 filterV0. +exists ([set x1] `+ W, [set x2] `+ W) => /=. +split => //=; first by exists ([set x1] `+ W) => //; exists W. +exists ([set x2] `+ W) => //; exists W => //. +move => [z1 z2] /= [[x ->]] => [[y1] Vy <-{z1}]. +move => [t ->{t}] [y2 Wy2 <-]. +apply: VA => //=. +exists (x1 + x2) => //; exists (y1 + y2). +apply: WV =>/=; exists y1 => //; exists y2 =>//. +by rewrite addrACA. +Qed. + +#[local] Lemma scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2). +Proof. +move => /= [r x] /= A /= [_] /= [V fV <-] VA. +have [r0|] := eqVneq r 0. + +have [V0 fV0 rV0] := (split_nbhsbasisat0 fV). +have [/= s [s0]] := (absorbing_nbhsbasisat0 fV0 x). +rewrite inE => xV''. +have [convV'' balV''] := (absconvex_nbhsbasisat0 fV0 ). +exists ((ball_ normr 0 (minr 1 s)) (*[set t | `|t| < r]*), [set x] `+ V0) => //=. + split. + exists (minr 1 s) => //=. rewrite /minr; case: ifPn => //. + by rewrite r0. + by exists ([set x] `+ V0) => //; exists V0. +move => [z1 z2] /=. +rewrite sub0r normrN => -[z1s]. +move=> [_ ->] [y] Vy <- {z2}. +apply: VA => /=. +rewrite r0; exists 0. +rewrite scale0r //. +exists (z1 *: (x + y)); rewrite ?add0r //. +apply: rV0 => /=. +exists (z1 *: x). + apply: (balV'' (z1 * s^-1)). + rewrite normrM normfV ltW // ltr_pdivrMr ?normr_gt0 ?gt_eqF //. + rewrite mul1r. + rewrite [ltRHS]gtr0_norm //. + rewrite (lt_le_trans z1s) //. + by rewrite /minr; case: ifPn => // /ltW //. + exists (s *: x) => //. + by rewrite !scalerA divfK// gt_eqF //. +exists (z1 *: y) => //. + apply: (balV'' z1). + rewrite (le_trans (ltW z1s)) //. + rewrite /minr; case: real_ltP => //. + rewrite gtr0_real //. + by exists y. +by rewrite -scalerDr. + +have [V0 fV0 rV0] := (split_nbhsbasisat0 fV). +have [V' fV' rV'] := (split_nbhsbasisat0 fV0). +have [V'' fV'' rV''] := (expand_nbhsbasisat0 r fV'). +have [/= s [s0 (*xV'' xx'*)]] := (absorbing_nbhsbasisat0 fV'' x). +rewrite inE => xV''. +have [convV'' balV''] := (absconvex_nbhsbasisat0 fV''). +exists ([set r] `+ (ball_ normr 0 (Num.min `|r| (`|r * s|))) (*[set t | `|t| < r]*), [set x] `+ V'') => //=. + split. + exists ((Num.min `|r| (`|r * s|))) => //=. + rewrite /minr; case: ifPn. rewrite normr_gt0 //. + rewrite normr_gt0 => _. + by rewrite mulf_neq0 // gt_eqF. + move=> u/= rur. + exists r => //. + exists (u - r). + rewrite sub0r normrN distrC (lt_le_trans rur)//. + by rewrite subrKC. + by exists ([set x] `+ V'') => //; exists V''. +move => [z1 z2] /= => [] [[x0] -> {x0}] [y]. +rewrite add0r normrN => yr. +move => <- [H ->] [t] Vt <-. +apply: VA => /=. +exists (r *: x) => //. +exists (r *: t + y *: x + y *: t) => //. + apply: rV0 => /=. + exists (r *:t) => //. + apply: rV'. exists 0. apply: mem0_nbhsbasisat0 =>//. exists (r *: t). apply: rV''. exists t => //. + by rewrite add0r. + exists (y *: x + y *: t)=> //. + apply: rV'. + exists (y *: x). + apply: rV''. + exists ((r^-1 * y) *: x). + apply: (balV'' (r^-1 * y * s^-1)). + rewrite -mulrA normrM normfV // ler_pdivrMl ?normr_gt0 // mulr1. + rewrite normrM -ler_pdivlMr ?normr_gt0 // ?gt_eqF // ?invr_gt0 //. + rewrite (le_trans (ltW yr)) //; rewrite /minr. + case: ifPn => //. move/ltW. rewrite normrM normfV //. + by rewrite invrK //. + by move=> _; rewrite normfV normrM invrK. + exists (s *: x) => //. + rewrite !scalerA divfK// gt_eqF //. + by rewrite scalerA mulrA divff// mul1r. + exists (y *: t) => //. + apply: rV''. + exists ((r^-1 * y) *: t). + apply: (balV'' (r^-1 * y)). + rewrite normrM normfV// ler_pdivrMl ?normr_gt0// mulr1. + apply: (le_trans (ltW yr)). + rewrite /minr. + case : real_ltP => //. + by exists t. + by rewrite scalerA mulrA divff// mul1r. + by rewrite addrA. +rewrite !addrA. +rewrite -scalerDr. +rewrite -addrA. +rewrite -scalerDr. +by rewrite scalerDl. +Qed. + +#[local] Lemma locally_convex : exists2 B : set_system E, + (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B. +Proof. +exists nbhsbasis_at0; first by move=> b; rewrite inE; apply: absconvex_nbhsbasisat0. +move => b [a] /= [a'] fa; rewrite addset0 => <- ab /=. +by exists a' => //=; split => //; exact: mem0_nbhsbasisat0. +Qed. + +HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R E add_continuous scale_continuous locally_convex. + +HB.end. + + +HB.factory Record Nbhssubbasis0_isConvexTvs (R: numFieldType) E & GRing.Lmodule R E (*& isConvexTvsat R E*) := { + nbhssubbasis0 : set_system E ; + nonempty_nbhssubbasisat0 : exists U, nbhssubbasis0 U; + mem0_nbhssubbasisat0 : forall B, nbhssubbasis0 B -> B 0 ; + expand_nbhssubbasisat0 : forall B r, nbhssubbasis0 B -> (*0 <= r ->*) + exists2 U, nbhssubbasis0 U & r `*: U `<=` B ; (* implies circled *) + absorbing_nbhssubbasisat0 : forall B , nbhssubbasis0 B -> pabsorbing_set B; + absconvex_nbhssubbasisat0 : forall B, nbhssubbasis0 B -> absolutely_convex_set B }. + +Definition nbhs_fromsubbasis0 (R : numFieldType) (E : zmodType) + (nbhssubbasis0 : set_system E) := + finI_from nbhssubbasis0 id. + + +HB.builders Context R E & Nbhssubbasis0_isConvexTvs R E. + +From mathcomp Require Import finmap. +(*Open Scope fset_scope. *) + +Local Definition nbhsbasis_at0 := @nbhs_fromsubbasis0 R E nbhssubbasis0. + +#[local] Lemma nonempty_nbhsbasisat0 : exists U, nbhsbasis_at0 U. +Proof. +have [U fU] := nonempty_nbhssubbasisat0; exists U. +rewrite /nbhsbasis_at0 /nbhs_fromsubbasis0 /finI_from /=. +exists [fset U]%fset => /=. + by move=> _ /fset1P ->; rewrite mem_set //=; exists U; rewrite ?addset0. +rewrite /bigcap /=; apply/seteqP; split => z /=; first by apply; rewrite inE. (*bigcap_set1 not working*) by move=> Uz i /fset1P ->. +Qed. + +#[local] Lemma nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V -> + exists2 W, nbhsbasis_at0 W & W `<=` U `&` V. +Proof. +move=> U V [/= I fI IV] [/=J fJ JU]. +exists (U `&` V) => //. +exists (I `|` J)%fset. + move => /= W; rewrite inE => /orP [WI|WJ]; rewrite mem_set //=. + by have := (fI _ WI); rewrite asboolE //=. +(* extremely hard to understand that asboolE is to be used here *) + by have := (fJ _ WJ); rewrite asboolE //=. +rewrite -IV -JU /bigcap /=; apply/seteqP; split => z /=. + by move=> H; split => i iI; apply: H; rewrite inE; apply/orP; [left|right]. (*bigcapI does not work*) +move => [Iz Jz] i; rewrite inE => /orP [|]; first by apply: Iz. +by apply: Jz. +Qed. + +#[local] Lemma mem0_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> B 0. +Proof. +by move => B [/= I fI <-] U /= /fI /=; rewrite asboolE /= => /mem0_nbhssubbasisat0. +Qed. + + +#[local] Lemma expand_nbhsbasisat0 : forall B r, nbhsbasis_at0 B -> + exists2 U, nbhsbasis_at0 U & r `*: U `<=` B. +Proof. +move => B r [/= I fI BI]. (* Change to a type I'*) +have H : forall i, (i \in I) -> exists2 V, nbhssubbasis0 V & r `*: V `<=` i. + move => i /(fI i); rewrite asboolE => /(expand_nbhssubbasisat0 r) /= [V nV rVi]. + by exists V. +pose f i := if (i \in I) =P true is ReflectT h then (sval (cid2 (H _ h))) else setT. +have Hn i : i \in I -> nbhssubbasis0 (f i). + by rewrite /f; case: eqP => // h _; case: cid2. +have Hr i : i \in I -> r `*: (f i) `<=` i. + by rewrite /f; case: eqP => // h _; case: cid2. +pose U := \bigcap_(i in [set` I])(f i). +exists U. exists (f @` I)%fset => /=. + - by move => _ /imfsetP[/= b bi ->]; apply/mem_set/Hn. + - by rewrite set_imfset bigcap_image. +rewrite -BI => x /= [y]; rewrite /U /= => Uy rx i /= j. +apply: Hr => //=. +by exists y => //; apply: Uy. +Qed. + +#[local] Lemma absorbing_nbhsbasisat0 : forall B , nbhsbasis_at0 B -> pabsorbing_set B. +Proof. +move => B [/= I fI BI] /= x. +have /= H : forall i, (i \in I) -> exists r : {posnum R}, r%:num *: x \in i. + move => i /(fI i); rewrite asboolE => /absorbing_nbhssubbasisat0/(_ x) [r r0 rx]. + by exists (PosNum r0). +pose f (i : set E) : {posnum R} := [elaborate if (i \in I) =P true is ReflectT h then (sval (cid (H i h))) else 1%:pos]. (*elaborate???*) +have /= Hr i : i \in I -> (f i)%:num *: x \in i. + by rewrite /f; case: eqP => // h _; case: cid. +pose r0 : {posnum R} := [elaborate \big[Order.min/1%:pos]_(i <- I) f i]. +exists r0%:num => //. (* waouh *) +rewrite -BI asboolE /= => i /= iI. +have ni : nbhssubbasis0 i by apply/set_mem/fI. +have [_ bali] := (absconvex_nbhssubbasisat0 ni). +apply: (bali (r0%:num / (f i)%:num)). + rewrite ger0_norm // ler_pdivrMr // mul1r /r0 num_le //. + by apply: ge_bigmin_seq. +exists ((f i)%:num *: x); first apply/set_mem/Hr => //. +by rewrite scalerA mulfVK //. +Qed. + +#[local] Lemma absconvex_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> absolutely_convex_set B. +Proof. +move => B [/= I fI <-]; split. + move=> x y r; rewrite !asboolE /= => xb yb => // i /= iI. + have /fI := iI; rewrite asboolE; move/absconvex_nbhssubbasisat0 => [+ _]. + move=> /(_ x y r); rewrite !asboolE; apply; first by apply: xb. + by apply: yb => /=. +move=> r r1 x /= [y] capy <- i /= iI. +have /fI := iI; rewrite asboolE; move/absconvex_nbhssubbasisat0 => [_ +]. +by move=> /(_ r r1 (r *: y)); apply => /=; exists y => //; apply: capy. +Qed. + + +HB.instance Definition _ := @Nbhsbasisat0_isConvexTvs.Build R E + nbhsbasis_at0 + nonempty_nbhsbasisat0 + nbhsbasis_at0I + mem0_nbhsbasisat0 + expand_nbhsbasisat0 + absorbing_nbhsbasisat0 + absconvex_nbhsbasisat0. HB.end. + Section ConvexTvs_numDomain. Context (R : numDomainType) (E : convexTvsType R) (U : set E). @@ -693,6 +1188,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. @@ -706,14 +1202,28 @@ rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl. by rewrite ltrD// ltr_pM2l// onem_gt0. Qed. +Let standard_ball_balanced_set (r : R) : balanced_set (ball (0 : R^o) r). +Proof. +move => t /= t1 z /= [y]. +rewrite -ball_normE /= !sub0r !normrN => + <-. +rewrite normrM. Search ( _ * _ < _ * _). +case: (eqVneq `|t| (1 : R)). + by move=> -> ; rewrite mul1r. +move=> t11. +have : (`|t| <1) by rewrite lt_neqAle; apply/andP; split. +by move => lt1 yr; rewrite -[ltRHS]mul1r ltr_pM ?normr_ge0. +Qed. + Let standard_locally_convex_set : - exists2 B : set_system R^o, (forall b, b \in B -> convex_set b) & basis B. + exists2 B : set_system R^o, (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B. Proof. -exists [set B | exists x r, B = ball x r]. - by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex_set. -split; first by move=> B [x] [r] ->; exact: ball_open. -move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. -by exists (ball x r) => //=; split; [exists x, r|exact: ballxx]. +exists [set B | exists r, B = ball 0 r]. + move=> B/= /[!inE]/= [] [r] ->; split; first by exact: standard_ball_convex_set. + by exact: standard_ball_balanced_set. +move=> B [] r /= r0 /= Br. +exists (ball 0 r); last by exact: Br. +split; last by apply: ballxx. +by exists r. Qed. HB.instance Definition _ := @@ -753,28 +1263,32 @@ by move=> [l [e f]] /= [] [Al Bl] [] Ae Be; apply: nU; split; Qed. Local Lemma prod_locally_convex : - exists2 B : set_system (E * F), (forall b, b \in B -> convex_set b) & basis B. + exists2 B : set_system (E * F), (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis (0,0) B. Proof. -have [Be Bcb Beb] := @locally_convex K E. +have [Be Bce Beb] := @locally_convex K E. have [Bf Bcf Bfb] := @locally_convex K F. -pose B := [set ef : set (E * F) | open ef /\ +pose B := [set ef : set (E * F) | exists be, exists2 bf, Be be & Bf bf /\ be `*` bf = ef]. -have : basis B. - rewrite /basis/=; split; first by move=> b => [] []. - move=> /= [x y] ef [[ne nf]] /= [Ne Nf] Nef. - case: Beb => Beo /(_ x ne Ne) /= -[a] [] Bea ax ea. - case: Bfb => Bfo /(_ y nf Nf) /= -[b] [] Beb yb fb. - exists [set z | a z.1 /\ b z.2]; last first. - by apply: subset_trans Nef => -[zx zy] /= [] /ea + /fb. - split=> //=; split; last by exists a, b. - rewrite openE => [[z z'] /= [az bz]]; exists (a, b) => /=; last by []. - rewrite !nbhsE /=; split; first by exists a => //; split => //; exact: Beo. - by exists b => //; split => // []; exact: Bfo. -exists B => // => b; rewrite inE /= => [[]] bo [] be [] bf Bee [] Bff <-. -move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2]. +have lem : nbhs_basis (0,0) B. + move=> /= b [/= [be bf] [/= nbe nbf]] /= befb /=. + have [/= be' [Beb' be'0] bbe] := Beb be nbe. + have [/= bf' [Bfb' bf'0] bbf] := Bfb bf nbf. + exists (be' `*` bf'). + split; first by exists be'; exists bf'. + split => //=. + apply: subset_trans; last by exact: befb. + move => t /= [bet bft]; split; first by apply: bbe. + by apply: bbf. +exists B => // => b; rewrite inE /= => [[]] be [] bf Bee [] Bff <-. +have [convbe balbe] := Bce be (mem_set Bee). +have [convbf balbf] := Bcf bf (mem_set Bff). split. - by apply/set_mem/Bcb; [exact/mem_set|exact/mem_set|exact/mem_set]. -by apply/set_mem/Bcf; [exact/mem_set|exact/mem_set|exact/mem_set]. + move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2];split. + by apply/set_mem/convbe;[exact/mem_set|exact/mem_set]. + by apply/set_mem/convbf;[exact/mem_set|exact/mem_set]. +move=> r [r1 [x1 y1]] [[x2 y2]]/= [bex bfy] [] <- <-; split. + by apply/balbe; [exact: r1|exists x2]. + by apply/balbf; [exact: r1|exists y2]. Qed. HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build @@ -785,7 +1299,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 }. @@ -952,3 +1466,428 @@ Lemma lcfun_linear : linear f. Proof. move => *; exact: linearP. Qed. End lcfunproperties. + +Import Norm. + +Definition gauge_fun (K : realType) (V : lmodType K) (A : set V) + (absA : absolutely_convex_set A) (absorbA: pabsorbing_set A) + : V -> K := +fun v => inf [set r | (0 < r) /\ v \in (fun x => r *: x) @` A]. + + +(* K can be a numDomainType once #1959 is solved *) +(*Definition gauge_fun (K : realType) (V : lmodType K) (A : set V) : V -> \bar K + := fun v => ereal_inf (EFin @` [set r | 0 < r /\ v \in (fun x => r *: x) @`A]). *) + +Section gauge. +Context (K : realType) (V : lmodType K) (A : set V) (absA : absolutely_convex_set A) (absorbA: pabsorbing_set A). + +(*TBD : from PR 1964 *) + +Lemma sup_ge0 (B : set K) : (forall x, B x -> 0 <= x) -> 0 <= sup B. +Proof. +Admitted. + +Lemma has_sup_wpZl (B : set K) (a : K) : 0 <= a -> has_sup B -> has_sup [set a * x | x in B ]. +Proof. +Admitted. + +Lemma gt0_has_supZl (B : set K) (a : K) : 0 < a -> has_sup [set a * x | x in B ] -> has_sup B. +Proof. +Admitted. + +Lemma ge0_supZl (B : set K) (a : K) : + 0 <= a -> sup [set a * x | x in B ] = a * sup B . +Proof. +Admitted. + +(* END TBD *) + +Notation gauge_fun := (gauge_fun absA absorbA). + +#[local] Lemma gauge0: gauge_fun 0 = 0. +Proof. +have/absolutely_convex0 := absA => A0; rewrite /gauge_fun. +have [->|]:= eqVneq A set0. + rewrite [X in inf X]( _ : _ = set0). + by rewrite -subset0 => /= x /=; rewrite image_set0 inE => -[] //. + by rewrite inf0. +set P := (X in inf X). +move/set0P/A0 => {}A0. +apply/eqP; rewrite eq_le; apply/andP; split; last first. + apply: lb_le_inf. + by exists 1; rewrite /P /=; split => //; rewrite inE; exists 0; rewrite ?scaler0 //; apply: A0. + by move=> z; rewrite /P /= => -[z0] _; rewrite ltW. +have infle : forall (r : K), (0 < r) -> inf P <= r. + move => r r0. + have Pr : P r by split => //; rewrite inE; exists 0 => //; rewrite scaler0. + apply: ge_inf => //; exists 0 => z /= [] z0 _; rewrite ltW //. +by apply/ler_addgt0Pl => /= r r0; rewrite addr0; apply: infle. +Qed. + +#[local] Lemma gauge_ge0 : forall x, 0 <= gauge_fun x. +Proof. +move => v. rewrite /gauge_fun. +set P := (X in inf X). +case : (EM (P !=set0)). + by move=> H; apply: lb_le_inf => // z; rewrite /P /= => -[] z0 _; rewrite ltW. +move/nonemptyPn -> ; rewrite /inf /=. +have -> : [set - (x : K) | x in set0] = set0 by rewrite seteqP; split => // x [] //=. +by rewrite sup0 oppr0. +Qed. + +(*TO BE MOVED to reals *) +Lemma supS (B : set K) (C : set K) : B !=set0 -> has_sup C -> B `<=` C -> sup B <= sup C. +Proof. +move=> B0 supC BC. +apply: sup_le => //. +apply: subset_trans; first by exact: BC. +by exact: le_down. +Qed. + +Lemma infS (B : set K) (C : set K) : has_inf B -> C !=set0 -> C `<=` B -> inf B <= inf C. +Proof. +move=> infB C0 BC. +rewrite /inf lerN2. +apply: supS. by apply/nonemptyN. +by apply/has_inf_supN. +by apply: image_subset. +Qed. +(* END TO BE MOVED *) + + +(* TODO : factorise*) +#[local] Lemma ler_gaugeD: + forall x y, gauge_fun (x + y) <= gauge_fun x + gauge_fun y. +Proof. +have A0 : A 0 by move: (absorbA 0)=> [??]; rewrite scaler0 inE. +have := absA; rewrite /absolutely_convex_set => -[] convA /= balA. +have lem (w : V) : (exists2 r, (0 < r) & A (r *: w)) -> has_inf [set t | 0 < t /\ w \in t `*: A]. + move => [r r0 Aw]; split => /=; rewrite /set0P; last by exists 0 => z [z0 _]; rewrite ltW. + exists r^-1 => //=; split=> //. + rewrite ?invr_gt0 //. + rewrite inE /=; exists (r *: w) => //. + by rewrite scalerA mulVf ?scale1r ?lt0r_neq0 //. +move => x y; rewrite /gauge_fun. +have:= (absorbA x) => -[/= r r0]; rewrite inE /= => Arx. +have:= (absorbA y) => -[/= r' r0']; rewrite inE /= => Ary. +have:= (absorbA (x+y)) => -[/= r2 r20']; rewrite inE /= => Arxy. +rewrite -inf_sumE; first by apply: lem; exists r. + by apply: lem; exists r'. +apply: infS; first by apply: lem; exists r2. + exists (r^-1 + r'^-1) => /=. + exists r^-1 => //=. + split=> //; rewrite ?invr_gt0 //. + rewrite inE /=; exists (r *: x) => //. + by rewrite scalerA mulVf ?scale1r ?lt0r_neq0 //. + exists r'^-1 => //=. + split=> //; rewrite ?invr_gt0 //. + rewrite inE /=; exists (r' *: y) => //. + by rewrite scalerA mulVf ?scale1r ?lt0r_neq0 //. +move => z /= [t [t0]]; rewrite inE /= => [[v] Av rvx] [s] [s0]; rewrite inE /=. +move => [w Aw twy] <-. rewrite addr_gt0 => //; split => //; rewrite inE /=. +rewrite -twy -rvx. +exists ((t + s)^-1 *: (t *: v + s *: w)). +rewrite scalerDr !scalerA mulrC (mulrC _ s). +rewrite -divD_onem => //. +pose st := Itv01 (mathcomp_extra.divDl_ge0 (ltW t0) (ltW s0)) + (mathcomp_extra.divDl_le1 (ltW t0) (ltW s0)). +have := convA v w st. +rewrite !inE => /(_ Av Aw); rewrite /conv /=; apply. +by rewrite !scalerA divff ?scale1r //; rewrite gt_eqF // addr_gt0. +Qed. + +Lemma ge0_infZl : forall (B : set K) [a : K], 0 <= a -> inf [set a * x | x in B] = a * inf B. +Proof. +move => B a a0; rewrite /inf mulrN -(ge0_supZl (-%R @` B) a0); congr (- sup _). +by rewrite !image_comp/=; apply: eq_imagel => //= ? _; rewrite mulrN. +Qed. + +Lemma inf_ge0 (B : set K) : (forall x, B x -> 0 <= x) -> 0 <= inf B. +Proof. +move=> B0; have [->|B0'] := eqVneq B set0; first by rewrite inf0. +by apply: lb_le_inf => //; exact/set0P. +Qed. + +Lemma inf_pos : inf [set r : K | 0 < r] = 0. +Proof. +apply/eqP; rewrite eq_le; apply/andP; split; last first. + by apply: inf_ge0 => x /ltW. +apply/ler_addgt0Pr => e e0; rewrite add0r. +apply: ge_inf => //=. +by exists 0 => r /ltW. +Qed. + +(* see coq-robot/ode_common.v *) +#[local] Lemma gaugeZ r v : gauge_fun (r *: v) = `|r| * gauge_fun v. +Proof. +rewrite /gauge_fun; have [->|] := eqVneq r 0. + rewrite normr0 mul0r. + have A0 : A 0 by move: (absorbA 0)=> [??]; rewrite scaler0 inE. + rewrite [X in inf X](_ : _ = [set r0 | 0 < r0]). + apply/seteqP; split=> [s []//|s /= s0]/=; split => //. + by rewrite inE/=; exists 0 => //; rewrite scale0r scaler0. + exact: inf_pos. +rewrite neq_lt -ge0_infZl// => /orP[r0|r0]; congr inf. +- rewrite ltr0_norm//. + have balA w : A w -> A (- w). + move=> Aw; case: absA => _ /(_ (-1)); apply => /=; first by rewrite normrN1. + by exists w => //; rewrite scaleN1r. + apply/seteqP; split => [x [x0 /[!inE]-[w Aw xwry]]|_ [y [y0 /[!inE]-[w Aw <-{v} <-]]]]/=. + exists ((- r)^-1 * x); last by rewrite invrN mulrA mulrNN divff ?mul1r// lt_eqF. + rewrite mulr_gt0// ?invr_gt0 ?oppr_gt0//; split => //. + rewrite inE/=; exists (- w); first exact: balA. + rewrite scalerN invrN mulNr scaleNr opprK -scalerA xwry scalerA. + by rewrite mulVf ?scale1r ?lt_eqF. + rewrite inE/= mulr_gt0 ?oppr_gt0//; split => //. + exists (- w); first exact: balA. + by rewrite scalerN mulNr scaleNr opprK scalerA. +- rewrite gtr0_norm//. + apply/seteqP; split => [x [x0 /[!inE]-[w Aw xwry]]|_ [y [y0 /[!inE]-[w Aw <-{v} <-]]]]/=. + exists (r^-1 * x); last by rewrite mulrA divff ?mul1r// gt_eqF. + rewrite mulr_gt0 ?invr_gt0 ?gt_eqF//; split => //. + rewrite inE/=; exists w => //. + by rewrite -[LHS]scalerA xwry scalerA mulVf ?scale1r// gt_eqF. + rewrite inE/= mulr_gt0//; split => //. + by exists w => //; rewrite scalerA. +Qed. + +HB.instance Definition _ := @isSemiNorm.Build K V gauge_fun gauge0 gauge_ge0 ler_gaugeD gaugeZ. + +Check (gauge_fun : SemiNorm.type V). +End gauge. + + +(* https://www.math.uni-konstanz.de/~infusino/TVS-WS18-19/Lect9.pdf *) +(* TODO : define initial topology wrt a family of functions in initial topology *) + +Section convex_topology_seminorm. +Context (R : realFieldType) (E : lmodType R) (P : set (SemiNorm.type E)) (H : P !=set0). + +Definition seminorm_on {R : realFieldType} {E : lmodType R} {P : set (SemiNorm.type E)} {H : P !=set0} : Type := E. + +HB.instance Definition _ := GRing.Lmodule.on (@seminorm_on R E P H). + +Definition seminorm_subbasis := +[set A | exists2 p, (P p) & exists2 e, (0 < e) & (A = p @^-1` (ball (0 : R) e))] : set_system E. + +Lemma nonempty_subbasis : exists B, seminorm_subbasis B. +Proof. +move : H => [p] Pp. +exists (p @^-1` (ball (0 : R) 1)). +by exists p => //; exists 1. +Qed. + +Lemma mem0_seminorm_subbasis : forall B, seminorm_subbasis B -> B 0. +Proof. +by move=> B; rewrite /seminorm_subbasis /= => -[p Pp [e]] e0 -> /=; rewrite norm0; exact: ballxx. +Qed. + +Lemma split_seminorm_subbasis : + forall B, seminorm_subbasis B -> exists2 C, seminorm_subbasis C & ( C `+ C `<=` B). +Proof. +move=> B; rewrite /seminorm_subbasis /= => -[p Pp [e e0 ->]] /=. +exists (p @^-1` (ball (0 : R) (e/2))); first by exists p => //; exists (e/2); rewrite ?divr_gt0. +rewrite /ball /= => z /=; rewrite sub0r normrN => -[x]; rewrite sub0r normrN => ballx [y]. +rewrite sub0r normrE => bally <-; rewrite (splitr e). +apply: le_lt_trans; last first. + apply: ltrD; first by exact: ballx. + by exact: bally. +(* Beware that now that we opened the Norm module ler_normD refers to semiNorm and not to norm*) +apply: le_trans; last by apply: Num.Theory.ler_normD. +have : p (x + y) <= p x + p y by apply: ler_normD. +by rewrite ger0_le_norm ?nnegrE ?addr_ge0 ?norm_ge0. +Qed. + +Lemma expand_seminorm_subbasis : + forall B r, seminorm_subbasis B -> exists2 U, seminorm_subbasis U & (r `*: U `<=` B). +move=> B r ; rewrite /seminorm_subbasis /= => -[p Pp [e e0 ->]] /=. +case: (eqVneq r (0 : R)). + move => ->; exists (p @^-1` (ball (0 : R) (e))); first by exists p => //; exists e. + by move => z /= [x] _; rewrite scale0r => <-; rewrite norm0; exact: ballxx. +move=> rneq0. +exists (p @^-1` (ball (0 : R) (e/`|r|))). + by exists p => //; exists (e/`|r|); rewrite ?divr_gt0 // normr_gt0. +rewrite /ball /= => z /=; rewrite sub0r normrN => -[x]; rewrite sub0r normrN => ballx <-. +by rewrite normZ normrM normr_id mulrC -ltr_pdivlMr ?normr_gt0. +Qed. + +(* TBA convex *) +Lemma lt_conv (x y r e : R): (0 <= r)-> (r <= 1) -> (x < e)-> (y < e) -> r * x + r.~ * y < e. +Proof. +move => r0 r1 xe ye. +have [->|] := eqVneq r 0; first by rewrite mul0r /onem subr0 add0r mul1r. +have [->|] := eqVneq r 1; first by rewrite mul1r /onem subrr mul0r addr0. +move=> rneq0 rneq1. +have -> : e = r * e + (1 -r) * e by rewrite -mulrDl addrCA subrr addr0 mul1r. +apply: ltrD. +rewrite lter_pM2l lt_neqAle; apply/andP; split => //; first by rewrite eq_sym. +by move: xe; rewrite lt_def; move/andP => []; rewrite eq_sym //. +by apply: ltW. +rewrite lter_pM2l /onem ?subr_gt0 ?ltW //. +by rewrite lt_def; apply/andP; split => //; rewrite eq_sym. +Qed. + +Lemma le_conv (x y r e : R): +(0 <= r)-> (r <= 1) -> (0 <= x) -> (x <= e)-> (0 <= y) -> (y <= e) -> r * x + r.~ * y <= e. +Proof. +move => r0 r1 x0 xe y0 ye. +rewrite /onem. +have -> : e = r * e + (1 -r) * e by rewrite -mulrDl addrCA subrr addr0 mul1r. +apply: lerD; first by rewrite ler_pM. +by rewrite ler_pM ?subr_ge0 //. +Qed. + + +Lemma convex_seminorm_subbasis: forall B, seminorm_subbasis B -> convex_set B. +Proof. +move=> B ; rewrite /seminorm_subbasis /= => -[p Pp [e e0 ->]] x y r. +rewrite !inE /ball /= !sub0r !normrN => px py. +rewrite /conv /=. +have lem1: +`|p (r%:num *: x + (r%:num).~ *: y)| <= `|p (r%:num *: x) + p ((r%:num).~ *: y)|. + rewrite (@ger0_le_norm _ (p (r%:num *: x + (r%:num).~ *: y))) ?nnegrE ?norm_ge0 ?ler_normD //. + by rewrite ?nnegrE ?addr_ge0 ?norm_ge0 ?ler_normD//. +apply:le_lt_trans; first by exact: lem1. +apply: le_lt_trans; first by apply: Num.Theory.ler_normD. +rewrite !normZ !normrM !normr_id [X in X*_]ger0_norm //. +rewrite [X in _ + X*_]ger0_norm ?onem_ge0 //. +by apply: lt_conv. +Qed. + + +Lemma balanced_seminorm_subbasis: forall B, seminorm_subbasis B -> balanced_set B. +Proof. +move => _ [p Pp [r r0] ->] /= s s1 z /= [x]. +rewrite /ball /ball_ /= !sub0r !normrN => pixr <-. +rewrite normZ normrM normr_id. +apply: le_lt_trans; last by exact: pixr. +by rewrite ler_piMl ?normr_ge0. +Qed. + +Lemma absolutely_convex_seminorm_subbasis: forall B, seminorm_subbasis B -> absolutely_convex_set B. +Proof. +move => b Bb; split; first by apply: convex_seminorm_subbasis. +by apply: balanced_seminorm_subbasis. +Qed. + +Lemma absorbing_seminorm : forall B , seminorm_subbasis B -> pabsorbing_set B. +move => _ [p Pp [r r0] ->] /= y. +case: (eqVneq (p y) 0) => y0. + by exists 1 => //; rewrite scale1r inE /ball/ball_ /= sub0r normrN y0 normr0. +exists (r/2 * (p y)^-1). + by rewrite !divr_gt0 // lt_neqAle eq_sym norm_ge0; apply/andP. +(*normr_gt0 not available for seminorms *) +rewrite inE /ball/ball_ /= sub0r normrN !normZ !normrM !normr_id. Check normrE. +rewrite !normfV -mulrA mulVf ?normr_eq0 ? mulr1//. +by rewrite ltr_pdivrMr !gtr0_norm ?ltr_pMr // ltrDr. +Qed. + +HB.instance Definition _ := @Nbhssubbasis0_isConvexTvs.Build R (seminorm_on) seminorm_subbasis nonempty_subbasis mem0_seminorm_subbasis expand_seminorm_subbasis absorbing_seminorm absolutely_convex_seminorm_subbasis. + +Check (seminorm_on : convexTvsType R). +(* +Lemma range_seminorm: forall f : SemiNorm.type E, (exists x : E, (f x)!= 0 ) -> range f = [set r : R | 0 <= r]. +Proof. +move => f [x /eqP fx] /=. +rewrite eqEsubset; split => r; first by move => [t _] <-; apply: norm_ge0. +have f0 : 0 < (f x). + have : 0<= f(x) by apply: @norm_ge0. + by rewrite le0r; move/orP => [/eqP /fx | ]. +have /ltW := f0; rewrite -eqr_norm_id; move/eqP => normf /=. +exists ((r/ f(x) *: x))=> //. +rewrite normZ normrM normfV normf -mulrA [X in _ * X]mulrC divff ?mulr1; apply/eqP => //. +by rewrite // eqr_norm_id. +Qed. +*) + + + +(* NB: this doesn't work as we strongly need a 0 basis. Here we are considering nbhs a = [ [A : set E |, exists e , A = [x | |p(x) - p(a)| x.1 + x.2). +Proof. +apply/continuous_init_fam => i/= [a b] /= A [e /= e0] piabeA. +have lerB_seminormD v w : p i (v) - p i w <= p i (v + w). +by rewrite -{1}[v](addrK w) lterBDl (le_trans (ler_normD _ _))// addrC Norm.Theory.normN. +have ler_Bseminorm x y : p i (x) - p i (y) <= p i ( x - y). + by rewrite -[p i y]Norm.Theory.normN lerB_seminormD. +have ler_seminorm_norm x y : `|p i (x) - p i (y)| <= p i ( x - y). + have [||_|_] // := @real_leP R (p i x) (p i y) => //; rewrite ?realE ?ger0_norm ?norm_ge0 //. + by rewrite -(Norm.Theory.normN _ (x - y)) opprB; exact: ler_Bseminorm. +pose pia := p i @^-1` ball_ [eta normr] (p i a) (e / 2). +pose pib := p i @^-1` ball_ [eta normr] (p i b) (e / 2). +rewrite /nbhs /= /filter_prod /filter_from /=. +exists (pia, pib) => /=. + by split; apply: initial_fam_continuous; apply: nbhsx_ballx; rewrite divr_gt0. +move=> [c d]/= [piac piad]. rewrite /pia /= in piac. rewrite /pib /= in piad. +apply: piabeA; rewrite /ball_ /=. +Search `| `| _ | - `| _ | | . +apply: le_lt_trans. +apply: ler_seminorm_norm. +rewrite opprD addrACA. +have lem: p i (a - c + (b - d)) <= p i (a - c) + p i (b - d). + by rewrite ?ler_normD //. +apply: le_lt_trans; first by exact: lem. +rewrite (splitr e); apply: ltrD. +move : (piac); rewrite /pia /=. (* apply: ler_seminorm_norm. +*) +Admitted. + +#[local] Lemma initial_fam_scale_continuous : continuous (fun z : R^o * S => z.1 *: z.2). + + Admitted. +#[local] Lemma initial_fam_locally_convex : exists2 B : set_system S, + (forall b, b \in B -> convex_set b) & basis B. Admitted. + +HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R S initial_fam_add_continuous initial_fam_scale_continuous initial_fam_locally_convex. +*) +End convex_topology_seminorm. + +Section generating_seminorm. +Context (R : realType) (E : convexTvsType R). + +Definition nbhs_of := sval (cid2 (@locally_convex _ E)). + +Definition absconvex_nbhs_of := (svalP (cid2 (@locally_convex _ E))).1. +Definition absconvex_nbhs_of_basis := (svalP (cid2 (@locally_convex _ E))).2. + + +#[local] Lemma nbhs_ofneq0 : nbhs_of !=set0. +Proof. +Admitted. + + +Lemma absorbing_nbhs_of : forall b, nbhs_of b -> pabsorbing_set b. +Proof. +rewrite /nbhs_of. +move => b nb x . +have /(_ b) //= := (absconvex_nbhs_of_basis). +Admitted. + +Definition seminorm_of := [set p : SemiNorm.type E | exists b, exists h : (nbhs_of b), + p = gauge_fun (absconvex_nbhs_of (mem_set h)) (absorbing_nbhs_of h)]. + +#[local] Lemma seminorm_ofneq0 : seminorm_of !=set0. +Proof. +Admitted. + +#[local] Notation seminormE := (@seminorm_on R E seminorm_of seminorm_ofneq0 : convexTvsType R). + +Theorem seminorm_convextvs : continuous (id : E -> seminormE) /\ (continuous (id : seminormE -> E)). +Proof. +Admitted. + +Proposition lcfun_seminorm (l : {scalar E}): +continuous l <-> (exists2 p : SemiNorm.type E, continuous p & (forall x, `|l x| <=p x)). +Proof. +(* exists I : {fset SemiNorm.type E}, I `<=` seminorm_of & p = max_i p_i *) +Admitted. + +End generating_seminorm. + + + (* TODO : apply it to hahn banach *) + + (* TODO : define O-basis *) diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index 943c1210cb..e4f8bb096d 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import interval_inference reals topology_structure. @@ -86,21 +86,47 @@ HB.instance Definition _ := Lemma initial_continuous : continuous (f : W -> T). Proof. by apply/continuousP => A ?; exists A. Qed. -Lemma cvg_image (F : set_system S) (s : S) : - Filter F -> f @` setT = setT -> - F --> (s : W) <-> ([set f @` A | A in F] : set_system _) --> f s. +Search "image" "filter". + +(* TODO : use image_set_system to be imported from measure theory *) +Lemma cvg_initial (F : set_system S) (s : S) : + Filter F -> + ([set f @` A | A in F] : set_system _) --> f s -> F --> (s : W). Proof. -move=> FF fsurj; split=> [cvFs|cvfFfs]. - move=> A /initial_continuous [B [Bop Bs sBAf]]. - have /cvFs FB : nbhs (s : W) B by apply: open_nbhs_nbhs. - rewrite nbhs_simpl; exists (f @^-1` A); first exact: filterS FB. - exact: image_preimage. +move=> FF cvfFfs. move=> A /= [_ [[B Bop <-] Bfs sBfA]]. -have /cvfFfs [C FC fCeB] : nbhs (f s) B by rewrite nbhsE; exists B. +have /cvfFfs [C FC fCeB] : nbhs (f s) B by rewrite nbhsE; exists B. rewrite nbhs_filterE; apply: filterS FC. by apply: subset_trans sBfA; rewrite -fCeB; apply: preimage_image. Qed. +Lemma cvg_image (F : set_system S) (s : S) : + Filter F -> f @` setT = setT -> + F --> (s : W) <-> ([set f @` A | A in F] : set_system _) --> f s. +Proof. +move=> FF fsurj; split=> [cvFs|/cvg_initial //]. +move=> A /initial_continuous [B [Bop Bs sBAf]]. +have /cvFs FB : nbhs (s : W) B by apply: open_nbhs_nbhs. +rewrite nbhs_simpl; exists (f @^-1` A); first exact: filterS FB. +by exact: image_preimage. +Qed. + +(* TODO: shorten this proof*) +Lemma continuous_initial_topology (U : topologicalType) (g : U -> W): + continuous g <-> (continuous (f \o g)). +Proof. +split => cont x. + apply: continuous_comp; first by apply: cont. + by apply: initial_continuous. +move => A [B/=]; rewrite /wopen /= => -[[C] oC fBC] Bgx BA. +apply: filterS; first by exact: BA. +rewrite -fBC /nbhs /=. +rewrite -comp_preimage. +apply: cont; apply: open_nbhs_nbhs; split => //. +have : f @` B `<=` C by move => z /= [t]; rewrite -fBC //= => ? <-. +by apply => /=; exists (g x). +Qed. + End Initial_Topology. (*#[deprecated(since="mathcomp-analysis 1.17.0", note="renamed `initial_open`")] Notation wopen := initial_open (only parsing).*) @@ -131,7 +157,7 @@ Local Open Scope relation_scope. Variable (pS : choiceType) (U : uniformType) (f : pS -> U). Let S := initial_topology f. - + Definition initial_ent : set_system (S * S) := filter_from (@entourage U) (fun V => (map_pair f)@^-1` V). @@ -264,3 +290,103 @@ Proof. move=> cf z U [?/= [[W oW <-]]] /= Wsfz /filterS; apply; apply: cf. exact: open_nbhs_nbhs. Qed. + +Lemma bigsetI_open (U : topologicalType) (I: Type) (s : seq I) (P : pred I) (f : I -> set U) : + (forall i, P i -> open (f i)) -> open (\big[setI/setT]_(i<- s | P i) f i). +Proof. +move=> Pf. apply: big_ind => //. by apply: openT. exact: openI. +Qed. + +Definition initial_fam_topology {S : Type} {T : Type} {I : pointedType} + (F : I -> (S -> T)) : Type := S. + +Section initial_fam_Topology. +Variable (S : choiceType) (T : topologicalType) (I : pointedType) (F : I -> (S -> T)). +Local Notation W := (initial_fam_topology F). + +Definition init_fam_subbase := [set O | exists i, exists2 A, (O = (F i) @^-1` A) & open A ]. + +HB.instance Definition _ := Choice.on W. +HB.instance Definition _ := isSubBaseTopological.Build W init_fam_subbase id. + +Lemma initial_fam_continuous : forall i, continuous ((F i) : W -> T). +Proof. move=> i; apply/continuousP => A oA. +exists [set (F i @^-1` A)]; last by rewrite bigcup_set1. +move=> /= O /= -> /= . rewrite /finI_from /=. +exists [fset (F i @^-1` A)]%fset; last by rewrite set_fset1 bigcap_set1. +by move => ? /=; rewrite inE; move/eqP ->; rewrite /init_fam_subbase in_setE /=; exists i; exists A. +Qed. + + +(* move open_from in topology_structure away from the builder *) +Lemma cvg_init_fam (G : set_system W) (s : W) : + Filter G -> + (forall i, ([set (F i) @` A | A in G] : set_system _) --> F i s) -> G --> (s : W) . +Proof. +move=> FG cvfFfs. +move => A -[] /=. +move => _ [[]] H Hop <- [B HB Bs] sBfA/=; rewrite nbhs_filterE. +have BA : B `<=` A. + apply: subset_trans; last by exact: sBfA. + by move => y /= By; exists B =>//. +apply: (@filterS _ G _ B) => //; move /(_ B HB): Hop => /= [] /= C CO Bcap. +(* can´t apply fsubsetP or subsetP on CO to obtain the following *) +have Ci : forall (O : set S) , O \in C -> exists i : I, exists2 A : set T, O = F i @^-1` A & open A. + by move => O /CO /set_mem //=. +move => {CO} {sBfA} {BA} {A}. +have GC: forall (O : set S), O \in C -> G O. + move => O OC; move: (OC) => /Ci [i [D OD openD]]. + have : nbhs (F i s) D. + rewrite nbhsE; exists D => //; split => //. + by move: Bs; rewrite -Bcap /bigcap /= => /(_ O OC); rewrite OD. + move/(cvfFfs i D); rewrite nbhs_filterE => //= [[O']] GO' /= O'D. + apply: filterS; last by exact: GO'. + by rewrite OD -O'D; apply: preimage_image. +by rewrite -Bcap; apply: filter_bigI => /= O OC; apply: GC. +Qed. + +Lemma cvg_image_init_fam (G : set_system W) (s : W) : + Filter G -> (forall i, (F i) @` setT = setT) -> + G --> (s : W) <-> (forall i, ([set (F i) @` A | A in G] : set_system _) --> F i s). +Proof. +move=> FG fsurj; split=> [cvFs|/cvg_init_fam] //. +move=> i A /initial_fam_continuous [B [//= Bop Bs sBAf]]. +have /cvFs FB : nbhs (s : W) B by apply: open_nbhs_nbhs. +rewrite nbhs_simpl; exists ((F i) @^-1` A); first exact: filterS FB. +by exact: image_preimage. +Qed. + +(*clean*) (* document the contingency of surjective of Fi in this context *) +Lemma continuous_init_fam (V : topologicalType) (f : V -> W) : + (forall i, continuous ((F i) \o (f : V -> S))) <-> continuous f. +Proof. +split=> cont; last first. + move=> i x; apply: continuous_comp; first by apply: cont. + apply: initial_fam_continuous. +move => x A; rewrite /nbhs /= => -[/= B]. +move => [Bfrom Bfx BA] /=. +apply: filterS; first by apply: preimage_subset BA. +apply: open_nbhs_nbhs; split => //. +rewrite /open_from /= in Bfrom. +have:= Bfrom. move => -[] C CO <-. +rewrite preimage_bigcup. +apply: bigcup_open => i /CO [] /= D Dsub <-. +rewrite preimage_bigcap /=. +rewrite bigcap_fset /= big_seq. +apply: bigsetI_open => /= E /Dsub. +move/set_mem. +rewrite /init_fam_subbase /=. +move=> -[j [A0 -> oA]]. +rewrite -comp_preimage. +have /continuousP := cont j. +by apply. +Qed. + +End initial_fam_Topology. + + +HB.instance Definition _ (S : pointedType) (T : topologicalType) (I : pointedType) (F : I -> (S -> T)) := + Pointed.on (initial_fam_topology F). + + +(* TODO : uniform structure for initial fam topology *) diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 6661159148..51e01fa97b 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -125,6 +125,9 @@ Definition open_nbhs (p : T) (A : set T) := open A /\ A p. Definition basis (B : set (set T)) := B `<=` open /\ forall x, filter_from [set U | B U /\ U x] id --> x. +Definition nbhs_basis x (B : set (set T)) := + filter_from [set U | B U /\ U x] id --> x. + Definition second_countable := exists2 B, countable B & basis B. Global Instance nbhs_pfilter (p : T) : ProperFilter (nbhs p). @@ -182,8 +185,8 @@ move=> A B; rewrite openE => Aop Bop p [Ap Bp]. by apply: filterI; [apply: Aop|apply: Bop]. Qed. -Lemma bigcup_open (I : Type) (D : set I) (f : I -> set T) : - (forall i, D i -> open (f i)) -> open (\bigcup_(i in D) f i). +Lemma bigcup_open (I : Type) (D : set I) (f : I -> set T) : + (forall i, D i -> open (f i)) -> open (\bigcup_(i in D) f i). Proof. rewrite openE => fop p [i Di]. by have /fop fiop := Di; move/fiop; apply: filterS => ??; exists i. @@ -496,6 +499,11 @@ HB.instance Definition _ := Nbhs_isTopological.Build T HB.end. + +Definition open_from (T : Type) (I : Type) (D : set I) (b : I -> set T) +:= [set \bigcup_(i in D') b i | D' in subset^~ D]. + + (** Topology defined by a base of open sets *) HB.factory Record isBaseTopological T & Choice T := { @@ -509,7 +517,7 @@ HB.factory Record isBaseTopological T & Choice T := { HB.builders Context T & isBaseTopological T. -Definition open_from := [set \bigcup_(i in D') b i | D' in subset^~ D]. +Local Notation open_from := (open_from D b). Let open_fromT : open_from setT. Proof. exists D => //; exact: b_cover. Qed. From 41c0bafd0d837e4a49333c54776904369e15faaa Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 17 Jun 2026 15:24:29 +0900 Subject: [PATCH 02/17] fix loccaly_convex_sub --- theories/normedtype_theory/tvs.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index ca0a8bcc09..da5694d147 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -558,9 +558,9 @@ HB.instance Definition _ := Local Open Scope convex_scope. Let locally_convex_sub : exists2 B : set_system sub_init_topo, - (forall b, b \in B -> convex_set b) & basis B. + (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B. Proof. -have [B convexB [openB/= genB]] := @locally_convex R V. +have [B convB nbhsb] := @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. From 10bc8fbe440028ddc9d2e909d7af6ba642618247 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 17 Jun 2026 15:44:40 +0900 Subject: [PATCH 03/17] partial clean --- theories/normedtype_theory/tvs.v | 247 +++++++++++++------------------ 1 file changed, 103 insertions(+), 144 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index da5694d147..aecfe8fe4f 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -1,5 +1,5 @@ -(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From HB Require Import structures. +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector. From mathcomp Require Import interval_inference. #[warning="-warn-library-file-internal-analysis"] @@ -109,7 +109,7 @@ Record d := { End dDist. End DDist. -Coercion DDist.t : DDist.d >-> tuple_of. +Coercion DDist.t : DDist.d >-> tuple_of. Reserved Notation "{ 'ddist' n }" (at level 0, format "{ 'ddist' n }"). @@ -121,14 +121,14 @@ Notation "{ 'ddist' n }" := (_.-ddist n). Section absolutely_convex. Context (K : numDomainType) (V : lmodType K). - -Definition balanced_set (A : set V) := (forall r, `|r| <= 1 -> (fun x => r *: x) @`A `<=` A). + +Definition balanced_set (A : set V) := forall r, `|r| <= 1 -> (fun x => r *: x) @`A `<=` A. Definition absolutely_convex_set (A : set V) := convex_set A /\ balanced_set A. -Definition absorbing_set (A : set V) := forall x : V, exists a, exists2 r, (a \in A) & (x = r *:a). +Definition absorbing_set (A : set V) := forall x : V, exists a, exists2 r, a \in A & x = r *:a. -Definition pabsorbing_set (A : set V) := forall x : V, exists2 r, ( 0< r) & r*: x \in A. +Definition pabsorbing_set (A : set V) := forall x : V, exists2 r, 0 < r & r*: x \in A. Definition absolutely_convex_hull (A : set V) := smallest absolutely_convex_set A. @@ -137,53 +137,53 @@ Definition absolutely_convex_hull (A : set V) := smallest absolutely_convex_set (* TODO : move to convex.v *) Lemma setI_convex : setI_closed (@convex_set K V). Proof. -move=> A B cA cB x y r /[!inE] -[xA xB] [yA yB]; split; apply/set_mem. +move=> A B cA cB x y r /[!inE] -[xA xB] [yA yB]; split; apply/set_mem. by apply/cA; apply/mem_set. by apply/cB; apply/mem_set. Qed. Lemma bigcap_convex : bigcap_closed (@convex_set K V). Proof. -move=> H Hconv x y r /[!inE] /= Hx Hy A /[dup] HA /Hconv /(_ _ _ _ _ _ )/set_mem; apply. +move=> H Hconv x y r /[!inE] /= Hx Hy A /[dup] HA /Hconv /(_ _ _ _ _ _ )/set_mem; apply. - by apply: mem_set; apply: Hx. -- by apply: mem_set; apply: Hy. +- by apply: mem_set; apply: Hy. Qed. Lemma setI_balanced : setI_closed balanced_set. Proof. -move=> A B bA bB x r /=; rewrite subsetI; split => z /= [t [At Bt] <-]. -- by apply: (bA _ r) => //; exists t. -- by apply: (bB _ r) => //; exists t. +move=> A B bA bB x r /=; rewrite subsetI; split => z /= [t [At Bt] <-]. +- by apply: (bA _ r) => //; exists t. +- by apply: (bB _ r) => //; exists t. Qed. Lemma bigcap_balanced : bigcap_closed balanced_set. Proof. move=> H Hconv /= r r1; apply: sub_bigcap => A HA x /= [t Ht <-]. apply: (Hconv A HA r r1) => //. -by exists t; first by apply: Ht. +by exists t; first by apply: Ht. Qed. Lemma absolutely_convex_hull_set (A : set V) : absolutely_convex_set (absolutely_convex_hull A). Proof. apply: bigcap_closed_smallest => H Habs. -split. -- by apply: bigcap_convex; apply: (subset_trans Habs); apply: subIsetl. -- by apply: bigcap_balanced; apply: (subset_trans Habs); apply: subIsetr. +split. +- by apply: bigcap_convex; apply: (subset_trans Habs); apply: subIsetl. +- by apply: bigcap_balanced; apply: (subset_trans Habs); apply: subIsetr. Qed. Lemma absolutely_convex_hullE (A : set V): absolutely_convex_hull A = [set a | exists n (t: {ddist n}) (l : n.-tuple V), [set` l] `<=` A /\ a = \sum_(i < n) t`_i *: l`_i]. Abort. - + Lemma absolutely_convex_hull_subset (A : set V): A `<=` absolutely_convex_hull A. Proof. by exact: sub_gen_smallest. Qed. -Lemma absolutely_convex0 (B : set V) : B !=set0 -> absolutely_convex_set B -> B 0. -Proof. -move => [] x Bx [] _ /(_ 0); rewrite normr0 ler01 // => /(_ isT) /(_ 0); apply. +Lemma absolutely_convex0 (B : set V) : B !=set0 -> absolutely_convex_set B -> B 0. +Proof. +move => [] x Bx [] _ /(_ 0); rewrite normr0 ler01 // => /(_ isT) /(_ 0); apply. by exists x; rewrite //= scale0r. Qed. @@ -488,8 +488,6 @@ HB.mixin Record Uniform_isConvexTvs (R : numDomainType) E locally_convex : exists2 B : set_system E, (forall b, b \in B -> absolutely_convex_set b) & (nbhs_basis 0) B }. -(* absolutely_convex instead of convex *) -(*filter_from [set U | B U /\ U 0] id --> 0. instead of B*) #[short(type="convexTvsType")] HB.structure Definition ConvexTvs (R : numDomainType) := @@ -800,7 +798,7 @@ Definition nbhs_frombasis0 (R : numFieldType) (E : zmodType) (nbhsbasis_at0 : set_system E) (x : E) := filter_from [set U | exists2 V, nbhsbasis_at0 V & [set x] `+ V = U] id. (* -Definition nbhs_fromfilter0 (R: numDomainType) (E : zmodType) (nbhsbasis_at0 : set_system E) (x : E) U := +Definition nbhs_fromfilter0 (R: numDomainType) (E : zmodType) (nbhsbasis_at0 : set_system E) (x : E) U := exists2 V, ((filter_from nbhsbasis_at0 id) V) & ([set x] `+ V `<=` U). *) @@ -814,12 +812,12 @@ Proof. move => B /(@expand_nbhsbasisat0 _ (2)) [U fU UB]. exists U => //. move => /= x [u] Uu [v] Uv <-. -apply: UB. -exists (2^-1 *: (u+v)); last by by rewrite scalerA mulfV // scale1r. -rewrite scalerDr. -have [convU _] := absconvex_nbhsbasisat0 fU. +apply: UB. +exists (2^-1 *: (u+v)); last by by rewrite scalerA mulfV // scale1r. +rewrite scalerDr. +have [convU _] := absconvex_nbhsbasisat0 fU. have H : (0 : R) <= 2^-1 by []. -have G : (2^-1 : R) <= 1 by rewrite invf_le1 ?lerDl //. +have G : (2^-1 : R) <= 1 by rewrite invf_le1 ?lerDl //. pose r := Itv01 H G. have := (convU u v r). rewrite !inE => /(_ Uu Uv); rewrite /conv /=. @@ -834,14 +832,11 @@ rewrite /nbhs_fromfilter0 => p. apply: filter_from_proper. apply: filter_from_filter => /=. have [U fU] := nonempty_nbhsbasisat0. - exists ([set p] `+ U) => //=. - by exists U. + by exists ([set p] `+ U) => //=; exists U. move=> _ _ /= [U0 FU <-] [V0 FV <-]. have [W FW WUV] := nbhsbasis_at0I FU FV. - exists ([set p] `+ W). - by exists W. - rewrite -addsetI. - exact: addsubset. + exists ([set p] `+ W); first by exists W. + rewrite -addsetI; exact: addsubset. move=> _ /= [V FV] <-. by exists p; exists p => //; exists 0; rewrite ?addr0//; exact: mem0_nbhsbasisat0. Qed. @@ -854,33 +849,24 @@ Qed. #[local] Lemma nbhs_nbhs (p : E) (A : set E) : nbhs_fromfilter0 p A -> nbhs_fromfilter0 p (nbhs_fromfilter0^~ A). -Proof. (* fun x => nbhs_fromfilter0 x A est un voisinage de p *) +Proof. rewrite /nbhs_fromfilter0/=. -move=> [B/= [C f0C <- pCA]]. -red. -simpl. +move=> [B/= [C f0C <- pCA]] //=. have [D f0D DDC] := split_nbhsbasisat0 f0C. -exists ([set p] `+ D). - by exists D. -move=> _ [/= _] -> [c Cc <-]. -red. -simpl. -exists ([set p + c] `+ D) => //. - by exists D. +exists ([set p] `+ D); first by exists D. +move=> _ [/= _] -> [c Cc <-] /=. +exists ([set p + c] `+ D) => //; first by exists D. apply: (subset_trans _ pCA). -apply: (@subset_trans _ ([set p] `+ ([set c] `+ D))). - exact: addsubsetA. -apply: addsubset => //. -apply: subset_trans DDC. -apply: addsubset => //. +apply: (@subset_trans _ ([set p] `+ ([set c] `+ D))); first by exact: addsubsetA. +apply: addsubset => //; apply: subset_trans DDC; apply: addsubset => //. by move=> x ->. Qed. HB.instance Definition _ := @hasNbhs.Build E (nbhs_fromfilter0). -HB.instance Definition _ := @Nbhs_isNbhsTopological.Build E nbhs_filter nbhs_singleton nbhs_nbhs. +HB.instance Definition _ := @Nbhs_isNbhsTopological.Build E nbhs_filter nbhs_singleton nbhs_nbhs. + - #[local] Lemma add_continuous : continuous (fun x : E * E => x.1 + x.2). Proof. move=> /= [x1 x2] /= A /= [V] /= [V0 filterV0 <-{V}] VA. @@ -897,28 +883,27 @@ by rewrite addrACA. Qed. #[local] Lemma scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2). -Proof. +Proof. move => /= [r x] /= A /= [_] /= [V fV <-] VA. have [r0|] := eqVneq r 0. - have [V0 fV0 rV0] := (split_nbhsbasisat0 fV). -have [/= s [s0]] := (absorbing_nbhsbasisat0 fV0 x). +have [/= s [s0]] := (absorbing_nbhsbasisat0 fV0 x). rewrite inE => xV''. -have [convV'' balV''] := (absconvex_nbhsbasisat0 fV0 ). +have [convV'' balV''] := (absconvex_nbhsbasisat0 fV0 ). exists ((ball_ normr 0 (minr 1 s)) (*[set t | `|t| < r]*), [set x] `+ V0) => //=. - split. - exists (minr 1 s) => //=. rewrite /minr; case: ifPn => //. + split. + exists (minr 1 s) => //=. rewrite /minr; case: ifPn => //. by rewrite r0. - by exists ([set x] `+ V0) => //; exists V0. -move => [z1 z2] /=. -rewrite sub0r normrN => -[z1s]. -move=> [_ ->] [y] Vy <- {z2}. -apply: VA => /=. -rewrite r0; exists 0. + by exists ([set x] `+ V0) => //; exists V0. +move => [z1 z2] /=. +rewrite sub0r normrN => -[z1s]. +move=> [_ ->] [y] Vy <- {z2}. +apply: VA => /=. +rewrite r0; exists 0. rewrite scale0r //. -exists (z1 *: (x + y)); rewrite ?add0r //. -apply: rV0 => /=. -exists (z1 *: x). +exists (z1 *: (x + y)); rewrite ?add0r //. +apply: rV0 => /=. +exists (z1 *: x). apply: (balV'' (z1 * s^-1)). rewrite normrM normfV ltW // ltr_pdivrMr ?normr_gt0 ?gt_eqF //. rewrite mul1r. @@ -1044,11 +1029,11 @@ Qed. Proof. move=> U V [/= I fI IV] [/=J fJ JU]. exists (U `&` V) => //. -exists (I `|` J)%fset. - move => /= W; rewrite inE => /orP [WI|WJ]; rewrite mem_set //=. - by have := (fI _ WI); rewrite asboolE //=. +exists (I `|` J)%fset. + move => /= W; rewrite inE => /orP [WI|WJ]; rewrite mem_set //=. + by have := (fI _ WI); rewrite asboolE //=. (* extremely hard to understand that asboolE is to be used here *) - by have := (fJ _ WJ); rewrite asboolE //=. + by have := (fJ _ WJ); rewrite asboolE //=. rewrite -IV -JU /bigcap /=; apply/seteqP; split => z /=. by move=> H; split => i iI; apply: H; rewrite inE; apply/orP; [left|right]. (*bigcapI does not work*) move => [Iz Jz] i; rewrite inE => /orP [|]; first by apply: Iz. @@ -1063,67 +1048,62 @@ Qed. #[local] Lemma expand_nbhsbasisat0 : forall B r, nbhsbasis_at0 B -> exists2 U, nbhsbasis_at0 U & r `*: U `<=` B. -Proof. +Proof. move => B r [/= I fI BI]. (* Change to a type I'*) have H : forall i, (i \in I) -> exists2 V, nbhssubbasis0 V & r `*: V `<=` i. move => i /(fI i); rewrite asboolE => /(expand_nbhssubbasisat0 r) /= [V nV rVi]. by exists V. pose f i := if (i \in I) =P true is ReflectT h then (sval (cid2 (H _ h))) else setT. -have Hn i : i \in I -> nbhssubbasis0 (f i). +have Hn i : i \in I -> nbhssubbasis0 (f i). by rewrite /f; case: eqP => // h _; case: cid2. have Hr i : i \in I -> r `*: (f i) `<=` i. by rewrite /f; case: eqP => // h _; case: cid2. pose U := \bigcap_(i in [set` I])(f i). exists U. exists (f @` I)%fset => /=. - by move => _ /imfsetP[/= b bi ->]; apply/mem_set/Hn. - - by rewrite set_imfset bigcap_image. + - by rewrite set_imfset bigcap_image. rewrite -BI => x /= [y]; rewrite /U /= => Uy rx i /= j. -apply: Hr => //=. +apply: Hr => //=. by exists y => //; apply: Uy. -Qed. - +Qed. + #[local] Lemma absorbing_nbhsbasisat0 : forall B , nbhsbasis_at0 B -> pabsorbing_set B. Proof. move => B [/= I fI BI] /= x. -have /= H : forall i, (i \in I) -> exists r : {posnum R}, r%:num *: x \in i. +have /= H : forall i, (i \in I) -> exists r : {posnum R}, r%:num *: x \in i. move => i /(fI i); rewrite asboolE => /absorbing_nbhssubbasisat0/(_ x) [r r0 rx]. by exists (PosNum r0). pose f (i : set E) : {posnum R} := [elaborate if (i \in I) =P true is ReflectT h then (sval (cid (H i h))) else 1%:pos]. (*elaborate???*) -have /= Hr i : i \in I -> (f i)%:num *: x \in i. +have /= Hr i : i \in I -> (f i)%:num *: x \in i. by rewrite /f; case: eqP => // h _; case: cid. pose r0 : {posnum R} := [elaborate \big[Order.min/1%:pos]_(i <- I) f i]. exists r0%:num => //. (* waouh *) rewrite -BI asboolE /= => i /= iI. have ni : nbhssubbasis0 i by apply/set_mem/fI. have [_ bali] := (absconvex_nbhssubbasisat0 ni). -apply: (bali (r0%:num / (f i)%:num)). - rewrite ger0_norm // ler_pdivrMr // mul1r /r0 num_le //. +apply: (bali (r0%:num / (f i)%:num)). + rewrite ger0_norm // ler_pdivrMr // mul1r /r0 num_le //. by apply: ge_bigmin_seq. exists ((f i)%:num *: x); first apply/set_mem/Hr => //. -by rewrite scalerA mulfVK //. +by rewrite scalerA mulfVK //. Qed. #[local] Lemma absconvex_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> absolutely_convex_set B. Proof. -move => B [/= I fI <-]; split. +move => B [/= I fI <-]; split. move=> x y r; rewrite !asboolE /= => xb yb => // i /= iI. - have /fI := iI; rewrite asboolE; move/absconvex_nbhssubbasisat0 => [+ _]. - move=> /(_ x y r); rewrite !asboolE; apply; first by apply: xb. + have /fI := iI; rewrite asboolE; move/absconvex_nbhssubbasisat0 => [+ _]. + move=> /(_ x y r); rewrite !asboolE; apply; first by apply: xb. by apply: yb => /=. move=> r r1 x /= [y] capy <- i /= iI. -have /fI := iI; rewrite asboolE; move/absconvex_nbhssubbasisat0 => [_ +]. +have /fI := iI; rewrite asboolE; move/absconvex_nbhssubbasisat0 => [_ +]. by move=> /(_ r r1 (r *: y)); apply => /=; exists y => //; apply: capy. Qed. -HB.instance Definition _ := @Nbhsbasisat0_isConvexTvs.Build R E - nbhsbasis_at0 - nonempty_nbhsbasisat0 - nbhsbasis_at0I - mem0_nbhsbasisat0 - expand_nbhsbasisat0 - absorbing_nbhsbasisat0 - absconvex_nbhsbasisat0. +HB.instance Definition _ := @Nbhsbasisat0_isConvexTvs.Build R E + nbhsbasis_at0 nonempty_nbhsbasisat0 nbhsbasis_at0I mem0_nbhsbasisat0 + expand_nbhsbasisat0 absorbing_nbhsbasisat0 absconvex_nbhsbasisat0. HB.end. @@ -1204,9 +1184,9 @@ Qed. Let standard_ball_balanced_set (r : R) : balanced_set (ball (0 : R^o) r). Proof. -move => t /= t1 z /= [y]. -rewrite -ball_normE /= !sub0r !normrN => + <-. -rewrite normrM. Search ( _ * _ < _ * _). +move => t /= t1 z /= [y]. +rewrite -ball_normE /= !sub0r !normrN => + <-. +rewrite normrM. case: (eqVneq `|t| (1 : R)). by move=> -> ; rewrite mul1r. move=> t11. @@ -1223,7 +1203,7 @@ exists [set B | exists r, B = ball 0 r]. move=> B [] r /= r0 /= Br. exists (ball 0 r); last by exact: Br. split; last by apply: ballxx. -by exists r. +by exists r. Qed. HB.instance Definition _ := @@ -1299,7 +1279,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 }. @@ -1471,7 +1451,7 @@ Import Norm. Definition gauge_fun (K : realType) (V : lmodType K) (A : set V) (absA : absolutely_convex_set A) (absorbA: pabsorbing_set A) - : V -> K := + : V -> K := fun v => inf [set r | (0 < r) /\ v \in (fun x => r *: x) @` A]. @@ -1482,78 +1462,57 @@ fun v => inf [set r | (0 < r) /\ v \in (fun x => r *: x) @` A]. Section gauge. Context (K : realType) (V : lmodType K) (A : set V) (absA : absolutely_convex_set A) (absorbA: pabsorbing_set A). -(*TBD : from PR 1964 *) - -Lemma sup_ge0 (B : set K) : (forall x, B x -> 0 <= x) -> 0 <= sup B. -Proof. -Admitted. - -Lemma has_sup_wpZl (B : set K) (a : K) : 0 <= a -> has_sup B -> has_sup [set a * x | x in B ]. -Proof. -Admitted. - -Lemma gt0_has_supZl (B : set K) (a : K) : 0 < a -> has_sup [set a * x | x in B ] -> has_sup B. -Proof. -Admitted. - -Lemma ge0_supZl (B : set K) (a : K) : - 0 <= a -> sup [set a * x | x in B ] = a * sup B . -Proof. -Admitted. - -(* END TBD *) - Notation gauge_fun := (gauge_fun absA absorbA). #[local] Lemma gauge0: gauge_fun 0 = 0. -Proof. -have/absolutely_convex0 := absA => A0; rewrite /gauge_fun. -have [->|]:= eqVneq A set0. +Proof. +have/absolutely_convex0 := absA => A0; rewrite /gauge_fun. +have [->|]:= eqVneq A set0. rewrite [X in inf X]( _ : _ = set0). - by rewrite -subset0 => /= x /=; rewrite image_set0 inE => -[] //. + by rewrite -subset0 => /= x /=; rewrite image_set0 inE => -[] //. by rewrite inf0. set P := (X in inf X). move/set0P/A0 => {}A0. apply/eqP; rewrite eq_le; apply/andP; split; last first. apply: lb_le_inf. - by exists 1; rewrite /P /=; split => //; rewrite inE; exists 0; rewrite ?scaler0 //; apply: A0. + by exists 1; rewrite /P /=; split => //; rewrite inE; exists 0; rewrite ?scaler0 //; apply: A0. by move=> z; rewrite /P /= => -[z0] _; rewrite ltW. have infle : forall (r : K), (0 < r) -> inf P <= r. - move => r r0. + move => r r0. have Pr : P r by split => //; rewrite inE; exists 0 => //; rewrite scaler0. apply: ge_inf => //; exists 0 => z /= [] z0 _; rewrite ltW //. -by apply/ler_addgt0Pl => /= r r0; rewrite addr0; apply: infle. +by apply/ler_addgt0Pl => /= r r0; rewrite addr0; apply: infle. Qed. #[local] Lemma gauge_ge0 : forall x, 0 <= gauge_fun x. -Proof. +Proof. move => v. rewrite /gauge_fun. set P := (X in inf X). case : (EM (P !=set0)). - by move=> H; apply: lb_le_inf => // z; rewrite /P /= => -[] z0 _; rewrite ltW. + by move=> H; apply: lb_le_inf => // z; rewrite /P /= => -[] z0 _; rewrite ltW. move/nonemptyPn -> ; rewrite /inf /=. have -> : [set - (x : K) | x in set0] = set0 by rewrite seteqP; split => // x [] //=. -by rewrite sup0 oppr0. +by rewrite sup0 oppr0. Qed. (*TO BE MOVED to reals *) Lemma supS (B : set K) (C : set K) : B !=set0 -> has_sup C -> B `<=` C -> sup B <= sup C. -Proof. -move=> B0 supC BC. -apply: sup_le => //. -apply: subset_trans; first by exact: BC. -by exact: le_down. -Qed. +Proof. +move=> B0 supC BC. +apply: sup_le => //. +apply: subset_trans; first by exact: BC. +by exact: le_down. +Qed. Lemma infS (B : set K) (C : set K) : has_inf B -> C !=set0 -> C `<=` B -> inf B <= inf C. -Proof. -move=> infB C0 BC. -rewrite /inf lerN2. -apply: supS. by apply/nonemptyN. -by apply/has_inf_supN. +Proof. +move=> infB C0 BC. +rewrite /inf lerN2. +apply: supS; first by apply/nonemptyN. +by apply/has_inf_supN. by apply: image_subset. Qed. -(* END TO BE MOVED *) +(* END TO BE MOVED *) (* TODO : factorise*) From 46fb4753dc1afeb0691eee8d5589e282ad7297fb Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 17 Jun 2026 16:31:07 +0900 Subject: [PATCH 04/17] clean and rename nbhsT to nbhsD --- theories/normedtype_theory/tvs.v | 196 ++++++++++++------------------- 1 file changed, 74 insertions(+), 122 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index aecfe8fe4f..80ccf8af08 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -602,7 +602,7 @@ Lemma nbhs0N_subproof (f : continuous (fun z : R^o * E => z.1 *: z.2)) : nbhs 0 U -> nbhs 0 (-%R @` U). Proof. by move => Ux; rewrite -oppr0; exact: nbhsN_subproof. Qed. -Lemma nbhsT_subproof (f : continuous (fun x : E * E => x.1 + x.2)) (x : E) : +Lemma nbhsD_subproof (f : continuous (fun x : E * E => x.1 + x.2)) (x : E) : nbhs 0 U -> nbhs x (+%R x @` U). Proof. move => U0; have /= := f (x, -x) U; rewrite subrr => /(_ U0). @@ -642,8 +642,8 @@ Proof. exact/nbhs0N_subproof/scale_continuous. Qed. Lemma nbhsN (U : set E) (x : E) : nbhs x U -> nbhs (-x) (-%R @` U). Proof. exact/nbhsN_subproof/scale_continuous. Qed. -Let nbhsT (U : set E) (x : E) : nbhs (0 : E) U -> nbhs x (+%R x @`U). -Proof. exact/nbhsT_subproof/add_continuous. Qed. +Let nbhsD (U : set E) (x : E) : nbhs (0 : E) U -> nbhs x (+%R x @`U). +Proof. exact/nbhsD_subproof/add_continuous. Qed. Let nbhsB (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @`U). Proof. exact/nbhsB_subproof/add_continuous. Qed. @@ -705,7 +705,7 @@ apply/funext => U; apply/propext => /=; rewrite /entourage /=; split. move=> Uxy; exists (v - x); last by rewrite addrC subrK. by exists (x - v); rewrite ?opprB. - move=> [A [U0 [nU UA]] H]; near=> z; apply: H; apply/xsectionP/set_mem/UA. - near: z; rewrite nearE; have := nbhsT x (nbhs0N nU). + near: z; rewrite nearE; have := nbhsD x (nbhs0N nU). rewrite [X in nbhs _ X -> _](_ : _ = [set v | x - v \in U0])//. apply/funext => /= z /=; apply/propext; split. by move=> [x0] [x1 Ux1 <-] <-; rewrite opprB addrC subrK inE. @@ -1114,8 +1114,8 @@ Context (R : numDomainType) (E : convexTvsType R) (U : set E). Lemma nbhs0N : nbhs 0 U -> nbhs 0 (-%R @` U). Proof. exact/nbhs0N_subproof/scale_continuous. Qed. -Lemma nbhsT (x :E) : nbhs 0 U -> nbhs x (+%R x @` U). -Proof. exact/nbhsT_subproof/add_continuous. Qed. +Lemma nbhsD (x :E) : nbhs 0 U -> nbhs x (+%R x @` U). +Proof. exact/nbhsD_subproof/add_continuous. Qed. Lemma nbhsB (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U). Proof. exact/nbhsB_subproof/add_continuous. Qed. @@ -1524,36 +1524,36 @@ have := absA; rewrite /absolutely_convex_set => -[] convA /= balA. have lem (w : V) : (exists2 r, (0 < r) & A (r *: w)) -> has_inf [set t | 0 < t /\ w \in t `*: A]. move => [r r0 Aw]; split => /=; rewrite /set0P; last by exists 0 => z [z0 _]; rewrite ltW. exists r^-1 => //=; split=> //. - rewrite ?invr_gt0 //. + rewrite ?invr_gt0 //. rewrite inE /=; exists (r *: w) => //. by rewrite scalerA mulVf ?scale1r ?lt0r_neq0 //. move => x y; rewrite /gauge_fun. have:= (absorbA x) => -[/= r r0]; rewrite inE /= => Arx. have:= (absorbA y) => -[/= r' r0']; rewrite inE /= => Ary. -have:= (absorbA (x+y)) => -[/= r2 r20']; rewrite inE /= => Arxy. +have:= (absorbA (x+y)) => -[/= r2 r20']; rewrite inE /= => Arxy. rewrite -inf_sumE; first by apply: lem; exists r. by apply: lem; exists r'. -apply: infS; first by apply: lem; exists r2. +apply: infS; first by apply: lem; exists r2. exists (r^-1 + r'^-1) => /=. - exists r^-1 => //=. - split=> //; rewrite ?invr_gt0 //. - rewrite inE /=; exists (r *: x) => //. + exists r^-1 => //=. + split=> //; rewrite ?invr_gt0 //. + rewrite inE /=; exists (r *: x) => //. by rewrite scalerA mulVf ?scale1r ?lt0r_neq0 //. exists r'^-1 => //=. - split=> //; rewrite ?invr_gt0 //. - rewrite inE /=; exists (r' *: y) => //. + split=> //; rewrite ?invr_gt0 //. + rewrite inE /=; exists (r' *: y) => //. by rewrite scalerA mulVf ?scale1r ?lt0r_neq0 //. -move => z /= [t [t0]]; rewrite inE /= => [[v] Av rvx] [s] [s0]; rewrite inE /=. -move => [w Aw twy] <-. rewrite addr_gt0 => //; split => //; rewrite inE /=. -rewrite -twy -rvx. +move => z /= [t [t0]]; rewrite inE /= => [[v] Av rvx] [s] [s0]; rewrite inE /=. +move => [w Aw twy] <-. rewrite addr_gt0 => //; split => //; rewrite inE /=. +rewrite -twy -rvx. exists ((t + s)^-1 *: (t *: v + s *: w)). -rewrite scalerDr !scalerA mulrC (mulrC _ s). +rewrite scalerDr !scalerA mulrC (mulrC _ s). rewrite -divD_onem => //. pose st := Itv01 (mathcomp_extra.divDl_ge0 (ltW t0) (ltW s0)) - (mathcomp_extra.divDl_le1 (ltW t0) (ltW s0)). -have := convA v w st. -rewrite !inE => /(_ Av Aw); rewrite /conv /=; apply. -by rewrite !scalerA divff ?scale1r //; rewrite gt_eqF // addr_gt0. + (mathcomp_extra.divDl_le1 (ltW t0) (ltW s0)). +have := convA v w st. +rewrite !inE => /(_ Av Aw); rewrite /conv /=; apply. +by rewrite !scalerA divff ?scale1r //; rewrite gt_eqF // addr_gt0. Qed. Lemma ge0_infZl : forall (B : set K) [a : K], 0 <= a -> inf [set a * x | x in B] = a * inf B. @@ -1620,46 +1620,46 @@ End gauge. (* https://www.math.uni-konstanz.de/~infusino/TVS-WS18-19/Lect9.pdf *) (* TODO : define initial topology wrt a family of functions in initial topology *) +Definition seminorm_on {R : realFieldType} {E : lmodType R} {P : set (SemiNorm.type E)} (Hp : P !=set0) : Type := E. + Section convex_topology_seminorm. Context (R : realFieldType) (E : lmodType R) (P : set (SemiNorm.type E)) (H : P !=set0). -Definition seminorm_on {R : realFieldType} {E : lmodType R} {P : set (SemiNorm.type E)} {H : P !=set0} : Type := E. - HB.instance Definition _ := GRing.Lmodule.on (@seminorm_on R E P H). -Definition seminorm_subbasis := -[set A | exists2 p, (P p) & exists2 e, (0 < e) & (A = p @^-1` (ball (0 : R) e))] : set_system E. +Definition seminorm_subbasis := +[set A | exists2 p, (P p) & exists2 e, (0 < e) & (A = p @^-1` (ball (0 : R) e))] : set_system E. Lemma nonempty_subbasis : exists B, seminorm_subbasis B. Proof. -move : H => [p] Pp. +move : H => [p] Pp. exists (p @^-1` (ball (0 : R) 1)). by exists p => //; exists 1. Qed. Lemma mem0_seminorm_subbasis : forall B, seminorm_subbasis B -> B 0. -Proof. +Proof. by move=> B; rewrite /seminorm_subbasis /= => -[p Pp [e]] e0 -> /=; rewrite norm0; exact: ballxx. Qed. -Lemma split_seminorm_subbasis : +Lemma split_seminorm_subbasis : forall B, seminorm_subbasis B -> exists2 C, seminorm_subbasis C & ( C `+ C `<=` B). -Proof. +Proof. move=> B; rewrite /seminorm_subbasis /= => -[p Pp [e e0 ->]] /=. exists (p @^-1` (ball (0 : R) (e/2))); first by exists p => //; exists (e/2); rewrite ?divr_gt0. -rewrite /ball /= => z /=; rewrite sub0r normrN => -[x]; rewrite sub0r normrN => ballx [y]. +rewrite /ball /= => z /=; rewrite sub0r normrN => -[x]; rewrite sub0r normrN => ballx [y]. rewrite sub0r normrE => bally <-; rewrite (splitr e). -apply: le_lt_trans; last first. +apply: le_lt_trans; last first. apply: ltrD; first by exact: ballx. by exact: bally. (* Beware that now that we opened the Norm module ler_normD refers to semiNorm and not to norm*) -apply: le_trans; last by apply: Num.Theory.ler_normD. -have : p (x + y) <= p x + p y by apply: ler_normD. -by rewrite ger0_le_norm ?nnegrE ?addr_ge0 ?norm_ge0. +apply: le_trans; last by apply: Num.Theory.ler_normD. +have : p (x + y) <= p x + p y by apply: ler_normD. +by rewrite ger0_le_norm ?nnegrE ?addr_ge0 ?norm_ge0. Qed. -Lemma expand_seminorm_subbasis : - forall B r, seminorm_subbasis B -> exists2 U, seminorm_subbasis U & (r `*: U `<=` B). +Lemma expand_seminorm_subbasis : + forall B r, seminorm_subbasis B -> exists2 U, seminorm_subbasis U & (r `*: U `<=` B). move=> B r ; rewrite /seminorm_subbasis /= => -[p Pp [e e0 ->]] /=. case: (eqVneq r (0 : R)). move => ->; exists (p @^-1` (ball (0 : R) (e))); first by exists p => //; exists e. @@ -1672,52 +1672,52 @@ by rewrite normZ normrM normr_id mulrC -ltr_pdivlMr ?normr_gt0. Qed. (* TBA convex *) -Lemma lt_conv (x y r e : R): (0 <= r)-> (r <= 1) -> (x < e)-> (y < e) -> r * x + r.~ * y < e. +Lemma lt_conv (x y r e : R): 0 <= r -> r <= 1 -> x < e -> y < e -> r * x + r.~ * y < e. Proof. move => r0 r1 xe ye. have [->|] := eqVneq r 0; first by rewrite mul0r /onem subr0 add0r mul1r. have [->|] := eqVneq r 1; first by rewrite mul1r /onem subrr mul0r addr0. move=> rneq0 rneq1. have -> : e = r * e + (1 -r) * e by rewrite -mulrDl addrCA subrr addr0 mul1r. -apply: ltrD. -rewrite lter_pM2l lt_neqAle; apply/andP; split => //; first by rewrite eq_sym. +apply: ltrD. +rewrite lter_pM2l lt_neqAle; apply/andP; split => //; first by rewrite eq_sym. by move: xe; rewrite lt_def; move/andP => []; rewrite eq_sym //. by apply: ltW. rewrite lter_pM2l /onem ?subr_gt0 ?ltW //. by rewrite lt_def; apply/andP; split => //; rewrite eq_sym. -Qed. +Qed. -Lemma le_conv (x y r e : R): -(0 <= r)-> (r <= 1) -> (0 <= x) -> (x <= e)-> (0 <= y) -> (y <= e) -> r * x + r.~ * y <= e. -Proof. +Lemma le_conv (x y r e : R): +0 <= r -> r <= 1 -> 0 <= x -> x <= e -> 0 <= y -> y <= e -> r * x + r.~ * y <= e. +Proof. move => r0 r1 x0 xe y0 ye. -rewrite /onem. -have -> : e = r * e + (1 -r) * e by rewrite -mulrDl addrCA subrr addr0 mul1r. -apply: lerD; first by rewrite ler_pM. -by rewrite ler_pM ?subr_ge0 //. +rewrite /onem. +have -> : e = r * e + (1 -r) * e by rewrite -mulrDl addrCA subrr addr0 mul1r. +apply: lerD; first by rewrite ler_pM. +by rewrite ler_pM ?subr_ge0 //. Qed. Lemma convex_seminorm_subbasis: forall B, seminorm_subbasis B -> convex_set B. -Proof. +Proof. move=> B ; rewrite /seminorm_subbasis /= => -[p Pp [e e0 ->]] x y r. rewrite !inE /ball /= !sub0r !normrN => px py. -rewrite /conv /=. -have lem1: +rewrite /conv /=. +have lem1: `|p (r%:num *: x + (r%:num).~ *: y)| <= `|p (r%:num *: x) + p ((r%:num).~ *: y)|. - rewrite (@ger0_le_norm _ (p (r%:num *: x + (r%:num).~ *: y))) ?nnegrE ?norm_ge0 ?ler_normD //. - by rewrite ?nnegrE ?addr_ge0 ?norm_ge0 ?ler_normD//. + rewrite (@ger0_le_norm _ (p (r%:num *: x + (r%:num).~ *: y))) ?nnegrE ?norm_ge0 ?ler_normD //. + by rewrite ?nnegrE ?addr_ge0 ?norm_ge0 ?ler_normD//. apply:le_lt_trans; first by exact: lem1. -apply: le_lt_trans; first by apply: Num.Theory.ler_normD. +apply: le_lt_trans; first by apply: Num.Theory.ler_normD. rewrite !normZ !normrM !normr_id [X in X*_]ger0_norm //. -rewrite [X in _ + X*_]ger0_norm ?onem_ge0 //. +rewrite [X in _ + X*_]ger0_norm ?onem_ge0 //. by apply: lt_conv. Qed. - + Lemma balanced_seminorm_subbasis: forall B, seminorm_subbasis B -> balanced_set B. Proof. -move => _ [p Pp [r r0] ->] /= s s1 z /= [x]. +move => _ [p Pp [r r0] ->] /= s s1 z /= [x]. rewrite /ball /ball_ /= !sub0r !normrN => pixr <-. rewrite normZ normrM normr_id. apply: le_lt_trans; last by exact: pixr. @@ -1738,71 +1738,21 @@ exists (r/2 * (p y)^-1). by rewrite !divr_gt0 // lt_neqAle eq_sym norm_ge0; apply/andP. (*normr_gt0 not available for seminorms *) rewrite inE /ball/ball_ /= sub0r normrN !normZ !normrM !normr_id. Check normrE. -rewrite !normfV -mulrA mulVf ?normr_eq0 ? mulr1//. +rewrite !normfV -mulrA mulVf ?normr_eq0 ? mulr1//. by rewrite ltr_pdivrMr !gtr0_norm ?ltr_pMr // ltrDr. Qed. -HB.instance Definition _ := @Nbhssubbasis0_isConvexTvs.Build R (seminorm_on) seminorm_subbasis nonempty_subbasis mem0_seminorm_subbasis expand_seminorm_subbasis absorbing_seminorm absolutely_convex_seminorm_subbasis. - -Check (seminorm_on : convexTvsType R). -(* -Lemma range_seminorm: forall f : SemiNorm.type E, (exists x : E, (f x)!= 0 ) -> range f = [set r : R | 0 <= r]. -Proof. -move => f [x /eqP fx] /=. -rewrite eqEsubset; split => r; first by move => [t _] <-; apply: norm_ge0. -have f0 : 0 < (f x). - have : 0<= f(x) by apply: @norm_ge0. - by rewrite le0r; move/orP => [/eqP /fx | ]. -have /ltW := f0; rewrite -eqr_norm_id; move/eqP => normf /=. -exists ((r/ f(x) *: x))=> //. -rewrite normZ normrM normfV normf -mulrA [X in _ * X]mulrC divff ?mulr1; apply/eqP => //. -by rewrite // eqr_norm_id. -Qed. -*) +HB.instance Definition _ := @Nbhssubbasis0_isConvexTvs.Build R (seminorm_on H) seminorm_subbasis nonempty_subbasis mem0_seminorm_subbasis expand_seminorm_subbasis absorbing_seminorm absolutely_convex_seminorm_subbasis. +Check (seminorm_on H : convexTvsType R). +(* NB: Using init-fam (see initial_topology.v) doesn't work as we strongly need a 0 basis. Here we are considering nbhs a = [ [A : set E |, exists e , A = [x | |p(x) - p(a)| x.1 + x.2). -Proof. -apply/continuous_init_fam => i/= [a b] /= A [e /= e0] piabeA. -have lerB_seminormD v w : p i (v) - p i w <= p i (v + w). -by rewrite -{1}[v](addrK w) lterBDl (le_trans (ler_normD _ _))// addrC Norm.Theory.normN. -have ler_Bseminorm x y : p i (x) - p i (y) <= p i ( x - y). - by rewrite -[p i y]Norm.Theory.normN lerB_seminormD. -have ler_seminorm_norm x y : `|p i (x) - p i (y)| <= p i ( x - y). - have [||_|_] // := @real_leP R (p i x) (p i y) => //; rewrite ?realE ?ger0_norm ?norm_ge0 //. - by rewrite -(Norm.Theory.normN _ (x - y)) opprB; exact: ler_Bseminorm. -pose pia := p i @^-1` ball_ [eta normr] (p i a) (e / 2). -pose pib := p i @^-1` ball_ [eta normr] (p i b) (e / 2). -rewrite /nbhs /= /filter_prod /filter_from /=. -exists (pia, pib) => /=. - by split; apply: initial_fam_continuous; apply: nbhsx_ballx; rewrite divr_gt0. -move=> [c d]/= [piac piad]. rewrite /pia /= in piac. rewrite /pib /= in piad. -apply: piabeA; rewrite /ball_ /=. -Search `| `| _ | - `| _ | | . -apply: le_lt_trans. -apply: ler_seminorm_norm. -rewrite opprD addrACA. -have lem: p i (a - c + (b - d)) <= p i (a - c) + p i (b - d). - by rewrite ?ler_normD //. -apply: le_lt_trans; first by exact: lem. -rewrite (splitr e); apply: ltrD. -move : (piac); rewrite /pia /=. (* apply: ler_seminorm_norm. -*) +Lemma continuous_seminorm : forall p, P p -> continuous (p : seminorm_on H -> R). +Proof. Admitted. -#[local] Lemma initial_fam_scale_continuous : continuous (fun z : R^o * S => z.1 *: z.2). - - Admitted. -#[local] Lemma initial_fam_locally_convex : exists2 B : set_system S, - (forall b, b \in B -> convex_set b) & basis B. Admitted. - -HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R S initial_fam_add_continuous initial_fam_scale_continuous initial_fam_locally_convex. -*) -End convex_topology_seminorm. +End convex_topology_seminorm. Section generating_seminorm. Context (R : realType) (E : convexTvsType R). @@ -1810,20 +1760,22 @@ Context (R : realType) (E : convexTvsType R). Definition nbhs_of := sval (cid2 (@locally_convex _ E)). Definition absconvex_nbhs_of := (svalP (cid2 (@locally_convex _ E))).1. -Definition absconvex_nbhs_of_basis := (svalP (cid2 (@locally_convex _ E))).2. +Definition absconvex_nbhs_of_basis := (svalP (cid2 (@locally_convex _ E))).2. #[local] Lemma nbhs_ofneq0 : nbhs_of !=set0. Proof. +rewrite /nbhs_of. +case: cid2 => B absB; rewrite /nbhs_basis /= => /(_ [set: E]) /=. Check nbhsT. +Search (nbhs _ _) Admitted. - Lemma absorbing_nbhs_of : forall b, nbhs_of b -> pabsorbing_set b. Proof. rewrite /nbhs_of. -move => b nb x . +move => b nb x. have /(_ b) //= := (absconvex_nbhs_of_basis). -Admitted. +Admitted. Definition seminorm_of := [set p : SemiNorm.type E | exists b, exists h : (nbhs_of b), p = gauge_fun (absconvex_nbhs_of (mem_set h)) (absorbing_nbhs_of h)]. @@ -1836,11 +1788,12 @@ Admitted. Theorem seminorm_convextvs : continuous (id : E -> seminormE) /\ (continuous (id : seminormE -> E)). Proof. + Admitted. -Proposition lcfun_seminorm (l : {scalar E}): -continuous l <-> (exists2 p : SemiNorm.type E, continuous p & (forall x, `|l x| <=p x)). -Proof. +Proposition lcfun_seminorm (l : {scalar E}): +continuous l <-> (exists2 p : SemiNorm.type E, continuous p & (forall x, `|l x| <= p x)). +Proof. (* exists I : {fset SemiNorm.type E}, I `<=` seminorm_of & p = max_i p_i *) Admitted. @@ -1849,4 +1802,3 @@ End generating_seminorm. (* TODO : apply it to hahn banach *) - (* TODO : define O-basis *) From 094dcf2441afe223b1a89480ce5b4039439db639 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 17 Jun 2026 17:10:52 +0900 Subject: [PATCH 05/17] wip --- theories/normedtype_theory/tvs.v | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 80ccf8af08..2790c1cacf 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -1766,10 +1766,9 @@ Definition absconvex_nbhs_of_basis := (svalP (cid2 (@locally_convex _ E))).2. #[local] Lemma nbhs_ofneq0 : nbhs_of !=set0. Proof. rewrite /nbhs_of. -case: cid2 => B absB; rewrite /nbhs_basis /= => /(_ [set: E]) /=. Check nbhsT. -Search (nbhs _ _) -Admitted. - +case: cid2 => B absB; rewrite /nbhs_basis /= => /(_ [set: E]) /= /(_ filterT) /=. +by move=> [] /= b [Bb b0] _; exists b. +Qed. Lemma absorbing_nbhs_of : forall b, nbhs_of b -> pabsorbing_set b. Proof. rewrite /nbhs_of. From 4749fbc9c8b08c6f425847904560f3954cfe4808 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 17 Jun 2026 21:43:40 +0900 Subject: [PATCH 06/17] fix instances normed module --- theories/normedtype_theory/normed_module.v | 45 ++++++++++++++++++---- 1 file changed, 37 insertions(+), 8 deletions(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 31c99d1a4f..2277069c59 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -132,7 +132,22 @@ Unshelve. all: by end_near. Qed. Local Open Scope convex_scope. -Let ball_convex_set (x : convex_lmodType V) (r : K) : convex_set (ball x r). +(* +Let standard_locally_convex_set : + exists2 B : set_system R^o, (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B. +Proof. +exists [set B | exists r, B = ball 0 r]. + move=> B/= /[!inE]/= [] [r] ->; split; first by exact: standard_ball_convex_set. + by exact: standard_ball_balanced_set. +move=> B [] r /= r0 /= Br. +exists (ball 0 r); last by exact: Br. +split; last by apply: ballxx. +by exists r. +Qed. +*) + + +Lemma ball_convex_set (x : convex_lmodType V) (r : K) : convex_set (ball x r). Proof. apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1. rewrite inE/=. @@ -145,16 +160,30 @@ rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl. by rewrite ltrD// ltr_pM2l// onem_gt0. Qed. +#[local] Lemma ball_balanced_set (r : K) : balanced_set (ball (0 : V) r). +Proof. +move => t /= t1 z /= [y]. +rewrite -ball_normE /= !sub0r !normrN => + <-. +rewrite normrZ. +case: (eqVneq `|t| (1 : K)). + by move=> -> ; rewrite mul1r. +move=> t11. +have : (`|t| <1) by rewrite lt_neqAle; apply/andP; split. +by move => lt1 yr; rewrite -[ltRHS]mul1r ltr_pM ?normr_ge0. +Qed. + (** NB: we have almost the same proof in `tvs.v` *) Let locally_convex_set : exists2 B : set_system (convex_lmodType V), - (forall b, b \in B -> convex_set b) & basis B. -Proof. -exists [set B | exists (x : convex_lmodType V) r, B = ball x r]. - by move=> b; rewrite inE => [[x]] [r] ->; exact: ball_convex_set. -split; first by move=> B [x] [r] ->; exact: ball_open. -move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. -by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. + (forall b, b \in B -> absolutely_convex_set b) & (nbhs_basis 0) B. +Proof. +exists [set B | exists r, B = ball 0 r]. + move=> b; rewrite inE /= => -[r ->]; split; first by exact: ball_convex_set. + by exact: ball_balanced_set. +move=> /= b; rewrite -nbhs_ballE => -[r /= r0] b0r /=. +exists (ball 0 r) => //. +split; last by exact: ballxx. +by exists r. Qed. HB.instance Definition _ := From 73e80e67fc32f404ac706384f9f8b42dc230f6d6 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 17 Jun 2026 22:29:36 +0900 Subject: [PATCH 07/17] wip continuous seminorm --- theories/normedtype_theory/tvs.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 2790c1cacf..190d2cf321 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -1748,8 +1748,23 @@ Check (seminorm_on H : convexTvsType R). (* NB: Using init-fam (see initial_topology.v) doesn't work as we strongly need a 0 basis. Here we are considering nbhs a = [ [A : set E |, exists e , A = [x | |p(x) - p(a)| continuous (p : seminorm_on H -> R). Proof. +move=> p Pp /= x /= A [r /= r0] pxrA. +exists ([set x] `+ p @^-1` (ball (0 : R) r)) => /=; last first. + move=> ? /= [? ->] [z]; rewrite /ball /= sub0r normrN => brpz <-; apply: pxrA. + red => /=. + apply: le_lt_trans; last by exact: brpz. + admit. +exists (p @^-1` (ball (0 : R) r)) => //=. (*how to avoid seeing the builders explicitely ? *) +exists ([fset (p @^-1` ball (0 : R) r)]%fset) => //=. + move=> ?; rewrite inE => /eqP ->; rewrite mem_set //. + by exists p => //; exists r. +apply/seteqP; rewrite /bigcap; split => y /=. + by move => /(_ (p @^-1` ball (0 : R) r)); rewrite inE; apply. +by move => ? ?; rewrite inE; move/eqP ->. Admitted. End convex_topology_seminorm. From e1e794d0260cec8060db14c496e725dc9f2e76d4 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 19 Jun 2026 16:59:43 +0900 Subject: [PATCH 08/17] seminorms are continuous --- classical/unstable.v | 21 ++++ theories/normedtype_theory/tvs.v | 187 +++++++++++++++++++++++++++---- 2 files changed, 185 insertions(+), 23 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index cf8b4ce04a..711b8b67db 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -647,7 +647,28 @@ Proof. by elim/big_ind2 : _ => *; rewrite ?norm0// (le_trans (ler_normD _ _))// lerD. Qed. +Lemma distC (v w : L) : norm (v - w) = norm (w - v). +Proof. +by rewrite -(normN (v - w)) opprB. +Qed. + End Theory. + +Section realTheory. +Variables (K : realDomainType) (L : lmodType K) (norm : SemiNorm.type L). + +Lemma seminorm_normrB x y: `|norm x - norm y| <= norm (x - y). +Proof. +have [pxy | pyx] := leP (norm x) (norm y). +rewrite ler0_norm ?subr_le0 // opprB. +rewrite lerBlDl; rewrite -(@Theory.normN _ _ norm (x-y)) opprB. +by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK. +rewrite gtr0_norm ?subr_gt0 //. +rewrite lerBlDl. +by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK. +Qed. + +End realTheory. End Theory. Module Import Exports. HB.reexport. End Exports. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 190d2cf321..9d7271ceb4 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -251,7 +251,7 @@ HB.structure Definition TopologicalZmodule := & TopologicalNmodule_isTopologicalZmodule M}. Section TopologicalZmoduleTheory. -Variables (M : topologicalZmodType). +Variables (M : topologicalZmodType) (E : topologicalType). Lemma sub_continuous : continuous (fun x : M * M => x.1 - x.2). Proof. @@ -266,6 +266,7 @@ Lemma fun_cvgN (F : topologicalZmodType) (U : set_system M) {FF : Filter U} f @ U --> a -> \- f @ U --> - a. Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed. + End TopologicalZmoduleTheory. HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M @@ -320,7 +321,7 @@ HB.structure Definition TopologicalLmodule (K : numDomainType) := & TopologicalZmodule_isTopologicalLmodule K M}. Section TopologicalLmodule_theory. -Variables (R : numFieldType) (E : topologicalType) (F : topologicalLmodType R). +Variables (R : numFieldType) (E : topologicalType) (F G: topologicalLmodType R). Lemma fun_cvgZ (U : set_system E) {FF : Filter U} (l : E -> R) (f : E -> F) (r : R) a : @@ -334,6 +335,22 @@ Lemma fun_cvgZr (U : set_system E) {FF : Filter U} k (f : E -> F) a : f @ U --> a -> k \*: f @ U --> k *: a. Proof. by apply: fun_cvgZ => //; exact: cvg_cst. Qed. + +Lemma continuous_shift (x y: F) : {for x, continuous (+%R^~ (-y))}. +Proof. +have -> : +%R^~ (-y) = (fun z => z.1 + z.2) \o (fun z => (z,-y)) by apply: funext. +apply: continuous_comp. +red. red. +by apply: cvg_pair => //=; exact: cvg_cst. +red. red => /=. +exact: (@add_continuous _ (x,-y)). +Qed. + +Lemma contiuousat_0 (y : F) (f : {linear F -> G}) : + {for 0, continuous f} -> {for y, continuous f}. +Proof. +Abort. + End TopologicalLmodule_theory. HB.factory Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M @@ -421,7 +438,7 @@ HB.instance Definition _ := HB.end. Section UniformZmoduleTheory. -Variables (M : UniformZmodule.type). +Variables (M: UniformZmodule.type). Lemma sub_unif_continuous : unif_continuous (fun x : M * M => x.1 - x.2). Proof. @@ -438,6 +455,8 @@ exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split. by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)). Qed. + + End UniformZmoduleTheory. HB.structure Definition PreUniformLmodule (K : numDomainType) := @@ -804,7 +823,7 @@ exists2 V, ((filter_from nbhsbasis_at0 id) V) & ([set x] `+ V `<=` U). HB.builders Context R E & Nbhsbasisat0_isConvexTvs R E. -Local Definition nbhs_fromfilter0 := @nbhs_frombasis0 R E (nbhsbasis_at0). +Let nbhs_fromfilter0 := @nbhs_frombasis0 R E (nbhsbasis_at0). Lemma split_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> exists2 C, nbhsbasis_at0 C & C `+ C `<=` B. @@ -826,7 +845,7 @@ apply: (@mulIf _ 2%:R); rewrite /((_).~) //. by rewrite mulrBl mulVf // mul1r // addrK. Qed. -#[local] Lemma nbhs_filter : forall p : E, ProperFilter (nbhs_fromfilter0 p). +#[local] Lemma nbhs_filter : forall p : E, ProperFilter (nbhs_fromfilter0 p). Proof. rewrite /nbhs_fromfilter0 => p. apply: filter_from_proper. @@ -841,7 +860,7 @@ move=> _ /= [V FV] <-. by exists p; exists p => //; exists 0; rewrite ?addr0//; exact: mem0_nbhsbasisat0. Qed. -#[local] Lemma nbhs_singleton : forall (p : E) (A : set E), nbhs_fromfilter0 p A -> A p. +#[local] Lemma nbhs_singleton : forall (p : E) (A : set E), nbhs_fromfilter0 p A -> A p. Proof. move=> p A [_/= [C f0C <-]]; apply; exists p => //; exists 0; rewrite ?addr0//. exact: mem0_nbhsbasisat0. @@ -992,6 +1011,36 @@ Qed. HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R E add_continuous scale_continuous locally_convex. HB.end. +(* + nbhsbasis_at0 : set_system E ; (*TODO rename to filterbasis_at0*) + nonempty_nbhsbasisat0 : exists U, nbhsbasis_at0 U; + nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V -> + exists2 W, nbhsbasis_at0 W & W `<=` U `&` V ; + mem0_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> B 0 ; + expand_nbhsbasisat0 : forall B r, nbhsbasis_at0 B -> (*0 <= r ->*) + exists2 U, nbhsbasis_at0 U & r `*: U `<=` B ; (* implies circled *) + absorbing_nbhsbasisat0 : forall B , nbhsbasis_at0 B -> pabsorbing_set B; + absconvex_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> absolutely_convex_set B }. + +*) +(* TB renamed *) +Lemma nbhsbasisat0_filter (R : numFieldType) (E : lmodType R) + (nbhsbasis_at0 : set_system E) (x : E) +(nonempty_nbhsbasisat0 : exists U, nbhsbasis_at0 U) +( nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V -> exists2 W, nbhsbasis_at0 W & W `<=` U `&` V ) +(mem0_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> B 0) : ProperFilter (@nbhs_frombasis0 R E (nbhsbasis_at0) x). +Proof. +apply: filter_from_proper. + apply: filter_from_filter => /=. + have [U fU] := nonempty_nbhsbasisat0. + by exists ([set x] `+ U) => //=; exists U. + move=> _ _ /= [U0 FU <-] [V0 FV <-]. + have [W FW WUV] := nbhsbasis_at0I _ _ FU FV. + exists ([set x] `+ W); first by exists W. + rewrite -addsetI; exact: addsubset. +move=> _ /= [V FV] <-. +by exists x; exists x => //; exists 0; rewrite ?addr0//; exact: mem0_nbhsbasisat0. +Qed. HB.factory Record Nbhssubbasis0_isConvexTvs (R: numFieldType) E & GRing.Lmodule R E (*& isConvexTvsat R E*) := { @@ -1013,7 +1062,7 @@ HB.builders Context R E & Nbhssubbasis0_isConvexTvs R E. From mathcomp Require Import finmap. (*Open Scope fset_scope. *) -Local Definition nbhsbasis_at0 := @nbhs_fromsubbasis0 R E nbhssubbasis0. +Let nbhsbasis_at0 := @nbhs_fromsubbasis0 R E nbhssubbasis0. #[local] Lemma nonempty_nbhsbasisat0 : exists U, nbhsbasis_at0 U. Proof. @@ -1622,6 +1671,17 @@ End gauge. Definition seminorm_on {R : realFieldType} {E : lmodType R} {P : set (SemiNorm.type E)} (Hp : P !=set0) : Type := E. + +(* TBD squeeze_cvgr once available *) +Section foo. +Context {T : Type} {a : set_system T} {Fa : Filter a} {R : realFieldType}. +Implicit Types f g h : T -> R. + +Lemma squeeze_cvgr f h g : (\near a, f a <= g a <= h a) -> + forall (l : R), f @ a --> l -> h @ a --> l -> g @ a --> l. +Admitted. +End foo. + Section convex_topology_seminorm. Context (R : realFieldType) (E : lmodType R) (P : set (SemiNorm.type E)) (H : P !=set0). @@ -1746,26 +1806,104 @@ HB.instance Definition _ := @Nbhssubbasis0_isConvexTvs.Build R (seminorm_on H) Check (seminorm_on H : convexTvsType R). -(* NB: Using init-fam (see initial_topology.v) doesn't work as we strongly need a 0 basis. Here we are considering nbhs a = [ [A : set E |, exists e , A = [x | |p(x) - p(a)| continuous (p : seminorm_on H -> R). -Proof. -move=> p Pp /= x /= A [r /= r0] pxrA. -exists ([set x] `+ p @^-1` (ball (0 : R) r)) => /=; last first. - move=> ? /= [? ->] [z]; rewrite /ball /= sub0r normrN => brpz <-; apply: pxrA. - red => /=. - apply: le_lt_trans; last by exact: brpz. - admit. -exists (p @^-1` (ball (0 : R) r)) => //=. (*how to avoid seeing the builders explicitely ? *) -exists ([fset (p @^-1` ball (0 : R) r)]%fset) => //=. - move=> ?; rewrite inE => /eqP ->; rewrite mem_set //. - by exists p => //; exists r. -apply/seteqP; rewrite /bigcap; split => y /=. - by move => /(_ (p @^-1` ball (0 : R) r)); rewrite inE; apply. -by move => ? ?; rewrite inE; move/eqP ->. +Import Norm. + +Lemma continuousat0_seminorm : forall p, P p -> continuous_at 0 (p : seminorm_on H -> R). +Proof. +move=> p Pp /= /= A [r /= r0] pxrA. +exists (p @^-1` (ball (p(0) : R) r)) => /=; last first. + by move=> z /=; apply: pxrA. +exists (p @^-1` (ball (0 : R) r)) => /=. + exists ([fset (p @^-1` ball (0 : R) r)]%fset) => /=. + move => t; rewrite inE => /eqP ->. rewrite mem_set //. + by exists p => //; exists r. + apply/seteqP; rewrite /bigcap; split => y //=. + by move => /(_ (p @^-1` ball (0 : R) r)); rewrite inE; apply. + by move => bxr i; rewrite inE => /eqP -> /=. +apply/seteqP; split => z /=. + move => [? ->] [y]; rewrite /ball /= => bry <- /=; rewrite /ball /=. + by rewrite norm0 (add0r y). +by rewrite norm0 => b0rp; exists 0 => //; exists z => //; rewrite add0r. +Qed. + +(* +Lemma continuousat_seminorm x : forall p, P p -> continuous_at x (p : seminorm_on H -> R). +Proof. +move=> p Pp /= /= A [r /= r0] pxrA. +exists (p @^-1` (ball (p x : R) r)) => /=; last first. + by move=> z /=; apply: pxrA. +exists (p @^-1` (ball (0 : R) r)) => /=. + exists ([fset (p @^-1` ball (0 : R) r)]%fset) => /=. + move => t; rewrite inE => /eqP ->. rewrite mem_set //. + by exists p => //; exists r. + apply/seteqP; rewrite /bigcap; split => y //=. + by move => /(_ (p @^-1` ball (0 : R) r)); rewrite inE; apply. + by move => bxr i; rewrite inE => /eqP -> /=. +apply/seteqP; split => z /=. + move => [? ->] [y]; rewrite /ball /= => bry <- /=; rewrite /ball /=. + rewrite (le_lt_trans _ bry) //. + rewrite sub0r normrN. + rewrite [leRHS]ger0_norm ?norm_ge0 //. + rewrite (le_trans (seminorm_normrB p _ _ )) //. + by rewrite opprD addrA subrr sub0r Theory.normN. +rewrite /ball => /= bx; exists x => //; exists (z- x); last by rewrite addrC subrK. +rewrite sub0r normrN ger0_norm ?norm_ge0 //. admit. Admitted. +*) + +Lemma seminorm_normrB (norm : SemiNorm.type E) x y: `|norm x - norm y| <= norm (x - y). +Proof. +have [pxy | pyx] := leP (norm x) (norm y). +rewrite ler0_norm ?subr_le0 // opprB. +rewrite lerBlDl; rewrite -(@Theory.normN _ _ norm (x-y)) opprB. +by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK. +rewrite gtr0_norm ?subr_gt0 //. +rewrite lerBlDl. +by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK. +Qed. + + + +Lemma continuous_seminorm x : forall p, P p -> continuous_at x (p : seminorm_on H -> R). +Proof. +move=> p Pp. +suff: (p y - p x)@[y --> x] --> (0 : R). + move=> pypx A [r r0] /= pxrA. Search "nbhs" "ball". + have npA := (pypx (ball (0 : R^o) r) (nbhsx_ballx (0 : R) r r0)) => /=. + exists ([set x] `+ (p @^-1` (ball (0: R) r))) => /=. + exists (p @^-1` (ball (0: R) r)) => //. + exists ([fset p @^-1` (ball (0 : R) r)]%fset) => //=. move => y. + rewrite inE => /eqP ->; rewrite mem_set //. + exists p => //; exists r => //=. + apply/seteqP; split => t /=. + rewrite /bigcap /= => /(_ (p @^-1` (ball (0 : R) r))). + by apply; rewrite inE. + by move => h; rewrite /bigcap /= => ?; rewrite inE => /eqP -> /=. + move => t /= [? ->] [y] bally <-; apply: pxrA => /=. rewrite (le_lt_trans _ bally) => //. + rewrite sub0r normrN [leRHS]ger0_norm ?norm_ge0 //. + rewrite (le_trans (seminorm_normrB p _ _)) // opprD addrA subrr add0r Theory.normN //. +have nearp : (\forall y \near (nbhs x), -p(y - x) <= p(y) - p(x) <= p (y -x)). + apply: nearW => //= y. + by have := (seminorm_normrB p y x); rewrite ler_norml. +have lem : (p \o +%R^~ (- x)) x0 @[x0 --> nbhs x] --> (0 : R). + have := (@cvg_comp _ _ _ (fun y => y - x) p). + apply; last first. + rewrite -(@norm0 _ _ p). + have := (continuousat0_seminorm Pp). + apply. + by rewrite -(subrr x)=> A /= /(@continuous_shift _ _ _ x A ); apply. +apply: (@squeeze_cvgr _ (nbhs x)) => /=. +- exact: nearp. +- rewrite -oppr0. + simpl in *. + apply: (@cvgN _ R^o (seminorm_on H) _ _ (p \o (fun y => y - x))). + exact: lem. +- apply: lem. +Qed. End convex_topology_seminorm. @@ -1784,11 +1922,14 @@ rewrite /nbhs_of. case: cid2 => B absB; rewrite /nbhs_basis /= => /(_ [set: E]) /= /(_ filterT) /=. by move=> [] /= b [Bb b0] _; exists b. Qed. + Lemma absorbing_nbhs_of : forall b, nbhs_of b -> pabsorbing_set b. Proof. rewrite /nbhs_of. move => b nb x. have /(_ b) //= := (absconvex_nbhs_of_basis). + + Admitted. Definition seminorm_of := [set p : SemiNorm.type E | exists b, exists h : (nbhs_of b), From 569fb053bf88b83dce4b580f14bbe9a88c4ccf6b Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 19 Jun 2026 21:27:53 +0900 Subject: [PATCH 09/17] clean and wip continuous linear --- theories/normedtype_theory/tvs.v | 79 ++++++++++---------------------- 1 file changed, 25 insertions(+), 54 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 9d7271ceb4..d8da81af2e 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -346,9 +346,16 @@ red. red => /=. exact: (@add_continuous _ (x,-y)). Qed. -Lemma contiuousat_0 (y : F) (f : {linear F -> G}) : - {for 0, continuous f} -> {for y, continuous f}. -Proof. +Lemma continuousat0_linear (x : F) (f : {linear F -> G}) : + {for 0, continuous f} -> {for x, continuous f}. +Proof. +move=> cont0. +suff: (f y - f x)@[y --> x] --> (0 : G). + move=> fxfy /= A nA /=. + admit. +have -> : (fun y => f y - f x) = (fun y => f(y -x)) by apply: funext => y; rewrite linearB. +apply: cvg_comp; last by rewrite -(linear0 f); apply: cont0. +by move => A nA /=; apply: continuous_shift; rewrite subrr. Abort. End TopologicalLmodule_theory. @@ -1666,9 +1673,6 @@ Check (gauge_fun : SemiNorm.type V). End gauge. -(* https://www.math.uni-konstanz.de/~infusino/TVS-WS18-19/Lect9.pdf *) -(* TODO : define initial topology wrt a family of functions in initial topology *) - Definition seminorm_on {R : realFieldType} {E : lmodType R} {P : set (SemiNorm.type E)} (Hp : P !=set0) : Type := E. @@ -1830,31 +1834,6 @@ apply/seteqP; split => z /=. by rewrite norm0 => b0rp; exists 0 => //; exists z => //; rewrite add0r. Qed. -(* -Lemma continuousat_seminorm x : forall p, P p -> continuous_at x (p : seminorm_on H -> R). -Proof. -move=> p Pp /= /= A [r /= r0] pxrA. -exists (p @^-1` (ball (p x : R) r)) => /=; last first. - by move=> z /=; apply: pxrA. -exists (p @^-1` (ball (0 : R) r)) => /=. - exists ([fset (p @^-1` ball (0 : R) r)]%fset) => /=. - move => t; rewrite inE => /eqP ->. rewrite mem_set //. - by exists p => //; exists r. - apply/seteqP; rewrite /bigcap; split => y //=. - by move => /(_ (p @^-1` ball (0 : R) r)); rewrite inE; apply. - by move => bxr i; rewrite inE => /eqP -> /=. -apply/seteqP; split => z /=. - move => [? ->] [y]; rewrite /ball /= => bry <- /=; rewrite /ball /=. - rewrite (le_lt_trans _ bry) //. - rewrite sub0r normrN. - rewrite [leRHS]ger0_norm ?norm_ge0 //. - rewrite (le_trans (seminorm_normrB p _ _ )) //. - by rewrite opprD addrA subrr sub0r Theory.normN. -rewrite /ball => /= bx; exists x => //; exists (z- x); last by rewrite addrC subrK. -rewrite sub0r normrN ger0_norm ?norm_ge0 //. admit. -Admitted. -*) - Lemma seminorm_normrB (norm : SemiNorm.type E) x y: `|norm x - norm y| <= norm (x - y). Proof. have [pxy | pyx] := leP (norm x) (norm y). @@ -1866,43 +1845,35 @@ rewrite lerBlDl. by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK. Qed. - - Lemma continuous_seminorm x : forall p, P p -> continuous_at x (p : seminorm_on H -> R). Proof. move=> p Pp. suff: (p y - p x)@[y --> x] --> (0 : R). - move=> pypx A [r r0] /= pxrA. Search "nbhs" "ball". + move=> pypx A [r r0] /= pxrA. have npA := (pypx (ball (0 : R^o) r) (nbhsx_ballx (0 : R) r r0)) => /=. exists ([set x] `+ (p @^-1` (ball (0: R) r))) => /=. - exists (p @^-1` (ball (0: R) r)) => //. - exists ([fset p @^-1` (ball (0 : R) r)]%fset) => //=. move => y. - rewrite inE => /eqP ->; rewrite mem_set //. - exists p => //; exists r => //=. + exists (p @^-1` (ball (0: R) r)) => //. + exists ([fset p @^-1` (ball (0 : R) r)]%fset) => //. + move => y; rewrite inE => /eqP ->; rewrite mem_set //. + by exists p => //; exists r => //=. apply/seteqP; split => t /=. - rewrite /bigcap /= => /(_ (p @^-1` (ball (0 : R) r))). - by apply; rewrite inE. - by move => h; rewrite /bigcap /= => ?; rewrite inE => /eqP -> /=. + rewrite /bigcap /= => /(_ (p @^-1` (ball (0 : R) r))). + by apply; rewrite inE. + by move => h; rewrite /bigcap /= => ?; rewrite inE => /eqP -> /=. move => t /= [? ->] [y] bally <-; apply: pxrA => /=. rewrite (le_lt_trans _ bally) => //. rewrite sub0r normrN [leRHS]ger0_norm ?norm_ge0 //. - rewrite (le_trans (seminorm_normrB p _ _)) // opprD addrA subrr add0r Theory.normN //. + by rewrite (le_trans (seminorm_normrB p _ _)) // opprD addrA subrr add0r Theory.normN //. have nearp : (\forall y \near (nbhs x), -p(y - x) <= p(y) - p(x) <= p (y -x)). apply: nearW => //= y. by have := (seminorm_normrB p y x); rewrite ler_norml. have lem : (p \o +%R^~ (- x)) x0 @[x0 --> nbhs x] --> (0 : R). - have := (@cvg_comp _ _ _ (fun y => y - x) p). - apply; last first. - rewrite -(@norm0 _ _ p). - have := (continuousat0_seminorm Pp). - apply. + apply: (@cvg_comp _ _ _ (fun y => y - x) p); last first. + by rewrite -(@norm0 _ _ p); apply: (continuousat0_seminorm Pp). by rewrite -(subrr x)=> A /= /(@continuous_shift _ _ _ x A ); apply. -apply: (@squeeze_cvgr _ (nbhs x)) => /=. -- exact: nearp. -- rewrite -oppr0. - simpl in *. - apply: (@cvgN _ R^o (seminorm_on H) _ _ (p \o (fun y => y - x))). - exact: lem. -- apply: lem. +apply: (@squeeze_cvgr _ (nbhs x)) => /=; first by exact: nearp. + rewrite -oppr0; apply: (@cvgN _ R^o (seminorm_on H) _ _ (p \o (fun y => y - x))). + by exact: lem. +by apply: lem. Qed. End convex_topology_seminorm. From ecbfb1ba59c53544dc0602b1c1c1961634026bab Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 19 Jun 2026 21:39:55 +0900 Subject: [PATCH 10/17] clean --- theories/topology_theory/initial_topology.v | 56 +++++++++------------ 1 file changed, 23 insertions(+), 33 deletions(-) diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index e4f8bb096d..1fffa3fd8b 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -294,8 +294,8 @@ Qed. Lemma bigsetI_open (U : topologicalType) (I: Type) (s : seq I) (P : pred I) (f : I -> set U) : (forall i, P i -> open (f i)) -> open (\big[setI/setT]_(i<- s | P i) f i). Proof. -move=> Pf. apply: big_ind => //. by apply: openT. exact: openI. -Qed. +move=> Pf. apply: big_ind => //. by apply: openT. exact: openI. +Qed. Definition initial_fam_topology {S : Type} {T : Type} {I : pointedType} (F : I -> (S -> T)) : Type := S. @@ -311,38 +311,37 @@ HB.instance Definition _ := isSubBaseTopological.Build W init_fam_subbase id. Lemma initial_fam_continuous : forall i, continuous ((F i) : W -> T). Proof. move=> i; apply/continuousP => A oA. -exists [set (F i @^-1` A)]; last by rewrite bigcup_set1. -move=> /= O /= -> /= . rewrite /finI_from /=. +exists [set (F i @^-1` A)]; last by rewrite bigcup_set1. +move=> /= O /= -> /= . rewrite /finI_from /=. exists [fset (F i @^-1` A)]%fset; last by rewrite set_fset1 bigcap_set1. by move => ? /=; rewrite inE; move/eqP ->; rewrite /init_fam_subbase in_setE /=; exists i; exists A. Qed. - (* move open_from in topology_structure away from the builder *) Lemma cvg_init_fam (G : set_system W) (s : W) : - Filter G -> + Filter G -> (forall i, ([set (F i) @` A | A in G] : set_system _) --> F i s) -> G --> (s : W) . Proof. -move=> FG cvfFfs. -move => A -[] /=. -move => _ [[]] H Hop <- [B HB Bs] sBfA/=; rewrite nbhs_filterE. +move=> FG cvfFfs. +move => A -[] /=. +move => _ [[]] H Hop <- [B HB Bs] sBfA/=; rewrite nbhs_filterE. have BA : B `<=` A. apply: subset_trans; last by exact: sBfA. by move => y /= By; exists B =>//. apply: (@filterS _ G _ B) => //; move /(_ B HB): Hop => /= [] /= C CO Bcap. (* can´t apply fsubsetP or subsetP on CO to obtain the following *) -have Ci : forall (O : set S) , O \in C -> exists i : I, exists2 A : set T, O = F i @^-1` A & open A. - by move => O /CO /set_mem //=. +have Ci : forall (O : set S) , O \in C -> exists i : I, exists2 A : set T, O = F i @^-1` A & open A. + by move => O /CO /set_mem //=. move => {CO} {sBfA} {BA} {A}. -have GC: forall (O : set S), O \in C -> G O. +have GC: forall (O : set S), O \in C -> G O. move => O OC; move: (OC) => /Ci [i [D OD openD]]. have : nbhs (F i s) D. rewrite nbhsE; exists D => //; split => //. - by move: Bs; rewrite -Bcap /bigcap /= => /(_ O OC); rewrite OD. + by move: Bs; rewrite -Bcap /bigcap /= => /(_ O OC); rewrite OD. move/(cvfFfs i D); rewrite nbhs_filterE => //= [[O']] GO' /= O'D. apply: filterS; last by exact: GO'. by rewrite OD -O'D; apply: preimage_image. -by rewrite -Bcap; apply: filter_bigI => /= O OC; apply: GC. +by rewrite -Bcap; apply: filter_bigI => /= O OC; apply: GC. Qed. Lemma cvg_image_init_fam (G : set_system W) (s : W) : @@ -356,31 +355,22 @@ rewrite nbhs_simpl; exists ((F i) @^-1` A); first exact: filterS FB. by exact: image_preimage. Qed. -(*clean*) (* document the contingency of surjective of Fi in this context *) Lemma continuous_init_fam (V : topologicalType) (f : V -> W) : (forall i, continuous ((F i) \o (f : V -> S))) <-> continuous f. Proof. split=> cont; last first. move=> i x; apply: continuous_comp; first by apply: cont. - apply: initial_fam_continuous. -move => x A; rewrite /nbhs /= => -[/= B]. -move => [Bfrom Bfx BA] /=. + apply: initial_fam_continuous. +move => x A; rewrite /nbhs /= => -[/= B] [Bfrom Bfx BA] /=. apply: filterS; first by apply: preimage_subset BA. -apply: open_nbhs_nbhs; split => //. -rewrite /open_from /= in Bfrom. -have:= Bfrom. move => -[] C CO <-. -rewrite preimage_bigcup. -apply: bigcup_open => i /CO [] /= D Dsub <-. -rewrite preimage_bigcap /=. -rewrite bigcap_fset /= big_seq. -apply: bigsetI_open => /= E /Dsub. -move/set_mem. -rewrite /init_fam_subbase /=. -move=> -[j [A0 -> oA]]. -rewrite -comp_preimage. -have /continuousP := cont j. -by apply. -Qed. +apply: open_nbhs_nbhs; split => //. +have:= Bfrom => -[] C CO <-; rewrite preimage_bigcup. +apply: bigcup_open => i /CO [] /= D Dsub <-; rewrite preimage_bigcap /=. +rewrite bigcap_fset /= big_seq; apply: bigsetI_open => /= E /Dsub. +move/set_mem; rewrite /init_fam_subbase /= => -[j [A0 -> oA]]. +rewrite -comp_preimage. +by have /continuousP := cont j; apply. +Qed. End initial_fam_Topology. From c1fdfc983b8346e09e8416e1320c5a824f10927e Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 19 Jun 2026 21:40:22 +0900 Subject: [PATCH 11/17] clean --- classical/unstable.v | 9 ++++----- theories/normedtype_theory/tvs.v | 15 ++------------- 2 files changed, 6 insertions(+), 18 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index 711b8b67db..6c62bf02e9 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -660,11 +660,10 @@ Variables (K : realDomainType) (L : lmodType K) (norm : SemiNorm.type L). Lemma seminorm_normrB x y: `|norm x - norm y| <= norm (x - y). Proof. have [pxy | pyx] := leP (norm x) (norm y). -rewrite ler0_norm ?subr_le0 // opprB. -rewrite lerBlDl; rewrite -(@Theory.normN _ _ norm (x-y)) opprB. -by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK. -rewrite gtr0_norm ?subr_gt0 //. -rewrite lerBlDl. + rewrite ler0_norm ?subr_le0 // opprB. + rewrite lerBlDl; rewrite -(@normN _ _ norm (x-y)) opprB. + by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK. +rewrite gtr0_norm ?subr_gt0 // lerBlDl. by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK. Qed. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index d8da81af2e..b37fcfc4de 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -1834,17 +1834,6 @@ apply/seteqP; split => z /=. by rewrite norm0 => b0rp; exists 0 => //; exists z => //; rewrite add0r. Qed. -Lemma seminorm_normrB (norm : SemiNorm.type E) x y: `|norm x - norm y| <= norm (x - y). -Proof. -have [pxy | pyx] := leP (norm x) (norm y). -rewrite ler0_norm ?subr_le0 // opprB. -rewrite lerBlDl; rewrite -(@Theory.normN _ _ norm (x-y)) opprB. -by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK. -rewrite gtr0_norm ?subr_gt0 //. -rewrite lerBlDl. -by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK. -Qed. - Lemma continuous_seminorm x : forall p, P p -> continuous_at x (p : seminorm_on H -> R). Proof. move=> p Pp. @@ -1862,10 +1851,10 @@ suff: (p y - p x)@[y --> x] --> (0 : R). by move => h; rewrite /bigcap /= => ?; rewrite inE => /eqP -> /=. move => t /= [? ->] [y] bally <-; apply: pxrA => /=. rewrite (le_lt_trans _ bally) => //. rewrite sub0r normrN [leRHS]ger0_norm ?norm_ge0 //. - by rewrite (le_trans (seminorm_normrB p _ _)) // opprD addrA subrr add0r Theory.normN //. + by rewrite (le_trans (Theory.seminorm_normrB p _ _)) // opprD addrA subrr add0r Theory.normN //. have nearp : (\forall y \near (nbhs x), -p(y - x) <= p(y) - p(x) <= p (y -x)). apply: nearW => //= y. - by have := (seminorm_normrB p y x); rewrite ler_norml. + by have := (Theory.seminorm_normrB p y x); rewrite ler_norml. have lem : (p \o +%R^~ (- x)) x0 @[x0 --> nbhs x] --> (0 : R). apply: (@cvg_comp _ _ _ (fun y => y - x) p); last first. by rewrite -(@norm0 _ _ p); apply: (continuousat0_seminorm Pp). From 890b2d2a2117dad08e5c25313d2ef6f7f10d2965 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sun, 21 Jun 2026 15:04:19 +0900 Subject: [PATCH 12/17] pr2003 --- theories/topology_theory/initial_topology.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index 1fffa3fd8b..cec1297e69 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -100,6 +100,7 @@ rewrite nbhs_filterE; apply: filterS FC. by apply: subset_trans sBfA; rewrite -fCeB; apply: preimage_image. Qed. +(*IN PR#2003*) Lemma cvg_image (F : set_system S) (s : S) : Filter F -> f @` setT = setT -> F --> (s : W) <-> ([set f @` A | A in F] : set_system _) --> f s. @@ -108,10 +109,10 @@ move=> FF fsurj; split=> [cvFs|/cvg_initial //]. move=> A /initial_continuous [B [Bop Bs sBAf]]. have /cvFs FB : nbhs (s : W) B by apply: open_nbhs_nbhs. rewrite nbhs_simpl; exists (f @^-1` A); first exact: filterS FB. -by exact: image_preimage. +by exact: image_preimage. Qed. -(* TODO: shorten this proof*) +(*IN PR#2003*) Lemma continuous_initial_topology (U : topologicalType) (g : U -> W): continuous g <-> (continuous (f \o g)). Proof. @@ -291,6 +292,7 @@ move=> cf z U [?/= [[W oW <-]]] /= Wsfz /filterS; apply; apply: cf. exact: open_nbhs_nbhs. Qed. +(*until the end IN PR#2003*) Lemma bigsetI_open (U : topologicalType) (I: Type) (s : seq I) (P : pred I) (f : I -> set U) : (forall i, P i -> open (f i)) -> open (\big[setI/setT]_(i<- s | P i) f i). Proof. From 700e274cd5f757953ab0d0b6e5a0bf5100ed3bcd Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sun, 21 Jun 2026 15:31:41 +0900 Subject: [PATCH 13/17] fix --- theories/topology_theory/initial_topology.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index cec1297e69..d0642c84eb 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -119,7 +119,7 @@ Proof. split => cont x. apply: continuous_comp; first by apply: cont. by apply: initial_continuous. -move => A [B/=]; rewrite /wopen /= => -[[C] oC fBC] Bgx BA. +move => A [B/=]; rewrite /initial_open /= => -[[C] oC fBC] Bgx BA. apply: filterS; first by exact: BA. rewrite -fBC /nbhs /=. rewrite -comp_preimage. From d8b2f35bb357f766aeb057020264ee70164cc3d6 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sun, 21 Jun 2026 21:30:33 +0900 Subject: [PATCH 14/17] fix locally_convex_sub --- theories/normedtype_theory/tvs.v | 29 ++++++++++++----------------- 1 file changed, 12 insertions(+), 17 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index b37fcfc4de..8178d1cdbc 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -584,24 +584,19 @@ Local Open Scope convex_scope. Let locally_convex_sub : exists2 B : set_system sub_init_topo, (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B. Proof. -have [B convB nbhsb] := @locally_convex R V. +have [B absconvB nbhsb] := @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/= /initial_open/=; 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. + move=> a; rewrite inE /= => -[b] /mem_set/absconvB [convb balb] <-; split. + move => r s l ra sa; suff : \val (r <|l|> s) \in b by []. + by rewrite !GRing.valD !GRing.valZ convb. + move=> /= r r1 x /= [rx] ? <-; apply: balb => /=; first by exact: r1. + by exists (\val rx); last by rewrite GRing.valZ. +move=> /= A [a' [/= [/= b ob <-] /= b0 ba]]. +rewrite /nbhs_basis /= in nbhsb. +have /nbhsb [b' [Bb' b'0] bb' ] /= : nbhs 0 b. + by apply: open_nbhs_nbhs; split; rewrite -?(linear0 (\val : U -> V)). +exists (val @^-1` b') => /=; last by move => x /= /bb' /ba. +by split; rewrite ?linear0 //; exists b'. Qed. Local Close Scope convex_scope. From 52931eb3f840e0d9a1649f8ce67f13a30663f551 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sun, 21 Jun 2026 22:34:08 +0900 Subject: [PATCH 15/17] continuousat0_linear --- theories/normedtype_theory/tvs.v | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 8178d1cdbc..476ea55efb 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -336,7 +336,8 @@ Lemma fun_cvgZr (U : set_system E) {FF : Filter U} k (f : E -> F) a : Proof. by apply: fun_cvgZ => //; exact: cvg_cst. Qed. -Lemma continuous_shift (x y: F) : {for x, continuous (+%R^~ (-y))}. +Lemma continuous_shift (V : topologicalLmodType R) (x y: V) : + {for x, continuous (+%R^~ (-y))}. Proof. have -> : +%R^~ (-y) = (fun z => z.1 + z.2) \o (fun z => (z,-y)) by apply: funext. apply: continuous_comp. @@ -351,12 +352,23 @@ Lemma continuousat0_linear (x : F) (f : {linear F -> G}) : Proof. move=> cont0. suff: (f y - f x)@[y --> x] --> (0 : G). + have -> : (fun y : F => f y - f x) = (fun y : F => f (y - x) : G). + by apply: funext => y; rewrite linearB. move=> fxfy /= A nA /=. - admit. + pose B := [set z | exists2 y : G, A y & z = y - f x]. + have /fxfy : nbhs 0 B. + have -> : B = (+%R^~ (-( - (f x)))) @^-1` A. + rewrite opprK; apply/seteqP; split. + by move=> y /= [z] ? ->; rewrite subrK //; exists z. + by move=> z /= ?; exists (z + f x)=> //; rewrite addrK. + have:= (@continuous_shift _ (0 : G) (- (f x)) A). + by rewrite opprK add0r => /(_ nA); apply. + rewrite /nbhs /=; apply/filterS => z /=; rewrite /B /=. + by move => -[y] Ay; rewrite linearD linearN => /(subIr (f x)) ->. have -> : (fun y => f y - f x) = (fun y => f(y -x)) by apply: funext => y; rewrite linearB. apply: cvg_comp; last by rewrite -(linear0 f); apply: cont0. by move => A nA /=; apply: continuous_shift; rewrite subrr. -Abort. +Qed. End TopologicalLmodule_theory. From 412b781d4cd867095523af1d728bb5c43855f02e Mon Sep 17 00:00:00 2001 From: mkerjean Date: Mon, 22 Jun 2026 20:22:23 +0900 Subject: [PATCH 16/17] generalize continuousfor0_continuous --- theories/normedtype_theory/normed_module.v | 4 ---- theories/normedtype_theory/tvs.v | 6 +++--- 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 2277069c59..55cba49134 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2049,10 +2049,6 @@ rewrite (le_lt_trans (fr r _ _))// -?ltr_pdivlMl//. by near: z; apply: cvgr_dist_lt => //; rewrite mulrC divr_gt0. Unshelve. all: by end_near. Qed. -Lemma continuousfor0_continuous (f : {linear V -> W}) : - {for 0, continuous f} -> continuous f. -Proof. by move=> /continuous_linear_bounded/bounded_linear_continuous. Qed. - Lemma linear_bounded_continuous (f : {linear V -> W}) : bounded_near f (nbhs 0) <-> continuous f. Proof. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 476ea55efb..ede1a9c2d2 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -347,7 +347,8 @@ red. red => /=. exact: (@add_continuous _ (x,-y)). Qed. -Lemma continuousat0_linear (x : F) (f : {linear F -> G}) : +(* TODO : look for and factorise similar lemma in normedtype *) +Lemma continuousfor0_continuous (x : F) (f : {linear F -> G}) : {for 0, continuous f} -> {for x, continuous f}. Proof. move=> cont0. @@ -1310,7 +1311,7 @@ Local Lemma prod_locally_convex : Proof. have [Be Bce Beb] := @locally_convex K E. have [Bf Bcf Bfb] := @locally_convex K F. -pose B := [set ef : set (E * F) | +pose B := [set ef : set (E * F) | exists be, exists2 bf, Be be & Bf bf /\ be `*` bf = ef]. have lem : nbhs_basis (0,0) B. move=> /= b [/= [be bf] [/= nbe nbf]] /= befb /=. @@ -1923,4 +1924,3 @@ End generating_seminorm. (* TODO : apply it to hahn banach *) - From afc8541d7e82fadd7883a2deb7d58954123d21d1 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Mon, 22 Jun 2026 21:54:38 +0900 Subject: [PATCH 17/17] clean --- theories/normedtype_theory/tvs.v | 174 +++++++++---------------------- 1 file changed, 52 insertions(+), 122 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index ede1a9c2d2..acf7d152f3 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -752,14 +752,11 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E entourage_inv entourage_split_ex nbhsE. -(* TO BE DELETED once PR#1974 is merged *) - HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build E add_continuous. HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R E scale_continuous. HB.instance Definition _ := Uniform_isConvexTvs.Build R E locally_convex. -(* END TO BE DELETED *) HB.end. @@ -777,7 +774,7 @@ Lemma addset0 (E : zmodType) (A: set E): ([set 0] `+ A) = A. Proof. apply/seteqP; split => z /=. - by move=> [+ -> [y]]; rewrite add0r => + + <-. + by move=> [+ -> [y]]; rewrite add0r => + + <-. by move=> Az; exists 0 => //; exists z; rewrite ?add0r. Qed. @@ -927,93 +924,60 @@ have [convV'' balV''] := (absconvex_nbhsbasisat0 fV0 ). exists ((ball_ normr 0 (minr 1 s)) (*[set t | `|t| < r]*), [set x] `+ V0) => //=. split. exists (minr 1 s) => //=. rewrite /minr; case: ifPn => //. - by rewrite r0. + by rewrite r0. by exists ([set x] `+ V0) => //; exists V0. -move => [z1 z2] /=. -rewrite sub0r normrN => -[z1s]. -move=> [_ ->] [y] Vy <- {z2}. -apply: VA => /=. -rewrite r0; exists 0. -rewrite scale0r //. +move => [z1 z2] /=; rewrite sub0r normrN => -[z1s]. +move=> [_ ->] [y] Vy <- {z2}; apply: VA => /=; rewrite r0; exists 0; rewrite ?scale0r //. exists (z1 *: (x + y)); rewrite ?add0r //. -apply: rV0 => /=. -exists (z1 *: x). - apply: (balV'' (z1 * s^-1)). - rewrite normrM normfV ltW // ltr_pdivrMr ?normr_gt0 ?gt_eqF //. - rewrite mul1r. - rewrite [ltRHS]gtr0_norm //. - rewrite (lt_le_trans z1s) //. - by rewrite /minr; case: ifPn => // /ltW //. - exists (s *: x) => //. - by rewrite !scalerA divfK// gt_eqF //. -exists (z1 *: y) => //. - apply: (balV'' z1). - rewrite (le_trans (ltW z1s)) //. - rewrite /minr; case: real_ltP => //. - rewrite gtr0_real //. - by exists y. -by rewrite -scalerDr. - +apply: rV0 => /=; exists (z1 *: x). + apply: (balV'' (z1 * s^-1)). + rewrite normrM normfV ltW // ltr_pdivrMr ?normr_gt0 ?gt_eqF //. + rewrite mul1r [ltRHS]gtr0_norm // (lt_le_trans z1s) //. + by rewrite /minr; case: ifPn => // /ltW //. + by exists (s *: x) => //; rewrite !scalerA divfK// gt_eqF //. +exists (z1 *: y) => //; last by rewrite -scalerDr. +apply: (balV'' z1); last by exists y. +rewrite (le_trans (ltW z1s)) // /minr; case: real_ltP => //; +by rewrite gtr0_real. have [V0 fV0 rV0] := (split_nbhsbasisat0 fV). have [V' fV' rV'] := (split_nbhsbasisat0 fV0). -have [V'' fV'' rV''] := (expand_nbhsbasisat0 r fV'). -have [/= s [s0 (*xV'' xx'*)]] := (absorbing_nbhsbasisat0 fV'' x). +have [V'' fV'' rV''] := (expand_nbhsbasisat0 r fV'). +have [/= s [s0 (*xV'' xx'*)]] := (absorbing_nbhsbasisat0 fV'' x). rewrite inE => xV''. -have [convV'' balV''] := (absconvex_nbhsbasisat0 fV''). -exists ([set r] `+ (ball_ normr 0 (Num.min `|r| (`|r * s|))) (*[set t | `|t| < r]*), [set x] `+ V'') => //=. - split. - exists ((Num.min `|r| (`|r * s|))) => //=. - rewrite /minr; case: ifPn. rewrite normr_gt0 //. - rewrite normr_gt0 => _. - by rewrite mulf_neq0 // gt_eqF. - move=> u/= rur. - exists r => //. - exists (u - r). - rewrite sub0r normrN distrC (lt_le_trans rur)//. - by rewrite subrKC. - by exists ([set x] `+ V'') => //; exists V''. -move => [z1 z2] /= => [] [[x0] -> {x0}] [y]. -rewrite add0r normrN => yr. -move => <- [H ->] [t] Vt <-. -apply: VA => /=. -exists (r *: x) => //. -exists (r *: t + y *: x + y *: t) => //. - apply: rV0 => /=. - exists (r *:t) => //. - apply: rV'. exists 0. apply: mem0_nbhsbasisat0 =>//. exists (r *: t). apply: rV''. exists t => //. - by rewrite add0r. - exists (y *: x + y *: t)=> //. - apply: rV'. - exists (y *: x). - apply: rV''. - exists ((r^-1 * y) *: x). - apply: (balV'' (r^-1 * y * s^-1)). - rewrite -mulrA normrM normfV // ler_pdivrMl ?normr_gt0 // mulr1. - rewrite normrM -ler_pdivlMr ?normr_gt0 // ?gt_eqF // ?invr_gt0 //. - rewrite (le_trans (ltW yr)) //; rewrite /minr. - case: ifPn => //. move/ltW. rewrite normrM normfV //. - by rewrite invrK //. - by move=> _; rewrite normfV normrM invrK. - exists (s *: x) => //. - rewrite !scalerA divfK// gt_eqF //. - by rewrite scalerA mulrA divff// mul1r. - exists (y *: t) => //. - apply: rV''. - exists ((r^-1 * y) *: t). - apply: (balV'' (r^-1 * y)). - rewrite normrM normfV// ler_pdivrMl ?normr_gt0// mulr1. - apply: (le_trans (ltW yr)). - rewrite /minr. - case : real_ltP => //. - by exists t. - by rewrite scalerA mulrA divff// mul1r. - by rewrite addrA. -rewrite !addrA. -rewrite -scalerDr. -rewrite -addrA. -rewrite -scalerDr. -by rewrite scalerDl. -Qed. +have [convV'' balV''] := (absconvex_nbhsbasisat0 fV''). +exists ([set r] `+ (ball_ normr 0 (Num.min `|r| (`|r * s|))) , [set x] `+ V'') => //=. + split; last by exists ([set x] `+ V'') => //; exists V''. + exists ((Num.min `|r| (`|r * s|))) => //=. + rewrite /minr; case: ifPn; first by rewrite normr_gt0 //. + by rewrite normr_gt0 => _ ; rewrite mulf_neq0 // gt_eqF. + move=> u/= rur; exists r => //; exists (u - r); last by rewrite subrKC. + by rewrite sub0r normrN distrC (lt_le_trans rur)//. +move => [z1 z2] /= => [] [[x0] -> {x0}] [y]; rewrite add0r normrN => yr. +move => <- [H ->] [t] Vt <-; apply: VA => /=. +exists (r *: x) => //; exists (r *: t + y *: x + y *: t); last first. + by rewrite !addrA -scalerDr -addrA -scalerDr scalerDl. +apply: rV0; exists (r *:t) => //. + apply: rV'; exists 0; first by apply: mem0_nbhsbasisat0. + exists (r *: t); first by apply: rV''; exists t. + by rewrite add0r. +exists (y *: x + y *: t); last by rewrite addrA. +apply: rV'; exists (y *: x). +apply: rV''. + exists ((r^-1 * y) *: x). + apply: (balV'' (r^-1 * y * s^-1)). + rewrite -mulrA normrM normfV // ler_pdivrMl ?normr_gt0 // mulr1. + rewrite normrM -ler_pdivlMr ?normr_gt0 // ?gt_eqF // ?invr_gt0 //. + rewrite (le_trans (ltW yr)) //; rewrite /minr. + case: ifPn; last by move=> _; rewrite normfV normrM invrK. + by move/ltW; rewrite normrM normfV invrK. + exists (s *: x); rewrite // !scalerA divfK// gt_eqF //. + by rewrite scalerA mulrA divff// mul1r. +exists (y *: t) => //; apply: rV''; exists ((r^-1 * y) *: t); last first. + by rewrite scalerA mulrA divff// mul1r. +apply: (balV'' (r^-1 * y)); last by exists t. +rewrite normrM normfV// ler_pdivrMl ?normr_gt0// mulr1. +by apply: (le_trans (ltW yr)); rewrite /minr; case : real_ltP. +Qed. #[local] Lemma locally_convex : exists2 B : set_system E, (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B. @@ -1022,43 +986,12 @@ exists nbhsbasis_at0; first by move=> b; rewrite inE; apply: absconvex_nbhsbasis move => b [a] /= [a'] fa; rewrite addset0 => <- ab /=. by exists a' => //=; split => //; exact: mem0_nbhsbasisat0. Qed. - + HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R E add_continuous scale_continuous locally_convex. HB.end. -(* - nbhsbasis_at0 : set_system E ; (*TODO rename to filterbasis_at0*) - nonempty_nbhsbasisat0 : exists U, nbhsbasis_at0 U; - nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V -> - exists2 W, nbhsbasis_at0 W & W `<=` U `&` V ; - mem0_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> B 0 ; - expand_nbhsbasisat0 : forall B r, nbhsbasis_at0 B -> (*0 <= r ->*) - exists2 U, nbhsbasis_at0 U & r `*: U `<=` B ; (* implies circled *) - absorbing_nbhsbasisat0 : forall B , nbhsbasis_at0 B -> pabsorbing_set B; - absconvex_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> absolutely_convex_set B }. -*) -(* TB renamed *) -Lemma nbhsbasisat0_filter (R : numFieldType) (E : lmodType R) - (nbhsbasis_at0 : set_system E) (x : E) -(nonempty_nbhsbasisat0 : exists U, nbhsbasis_at0 U) -( nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V -> exists2 W, nbhsbasis_at0 W & W `<=` U `&` V ) -(mem0_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> B 0) : ProperFilter (@nbhs_frombasis0 R E (nbhsbasis_at0) x). -Proof. -apply: filter_from_proper. - apply: filter_from_filter => /=. - have [U fU] := nonempty_nbhsbasisat0. - by exists ([set x] `+ U) => //=; exists U. - move=> _ _ /= [U0 FU <-] [V0 FV <-]. - have [W FW WUV] := nbhsbasis_at0I _ _ FU FV. - exists ([set x] `+ W); first by exists W. - rewrite -addsetI; exact: addsubset. -move=> _ /= [V FV] <-. -by exists x; exists x => //; exists 0; rewrite ?addr0//; exact: mem0_nbhsbasisat0. -Qed. - - -HB.factory Record Nbhssubbasis0_isConvexTvs (R: numFieldType) E & GRing.Lmodule R E (*& isConvexTvsat R E*) := { +HB.factory Record Nbhssubbasis0_isConvexTvs (R: numFieldType) E & GRing.Lmodule R E := { nbhssubbasis0 : set_system E ; nonempty_nbhssubbasisat0 : exists U, nbhssubbasis0 U; mem0_nbhssubbasisat0 : forall B, nbhssubbasis0 B -> B 0 ; @@ -1071,11 +1004,9 @@ Definition nbhs_fromsubbasis0 (R : numFieldType) (E : zmodType) (nbhssubbasis0 : set_system E) := finI_from nbhssubbasis0 id. - HB.builders Context R E & Nbhssubbasis0_isConvexTvs R E. From mathcomp Require Import finmap. -(*Open Scope fset_scope. *) Let nbhsbasis_at0 := @nbhs_fromsubbasis0 R E nbhssubbasis0. @@ -1109,7 +1040,6 @@ Proof. by move => B [/= I fI <-] U /= /fI /=; rewrite asboolE /= => /mem0_nbhssubbasisat0. Qed. - #[local] Lemma expand_nbhsbasisat0 : forall B r, nbhsbasis_at0 B -> exists2 U, nbhsbasis_at0 U & r `*: U `<=` B. Proof.