From 9b83616fb44de27639fc8b7a0d061790cb9a24e7 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 20 Mar 2026 11:14:19 +0900 Subject: [PATCH 1/4] adding seminorms to tvs - adding also initial fam topology, gauge functions, and subbase 0basis - hahn banach initial_subctvs Co-authored-by: Reynald Affeldt Co-authored-by: Cyril Cohen --- classical/unstable.v | 20 + .../functional_analysis/hahn_banach_theorem.v | 90 +- theories/normedtype_theory/normed_module.v | 26 +- theories/normedtype_theory/tvs.v | 1347 ++++++++++++++++- theories/topology_theory/initial_topology.v | 9 +- theories/topology_theory/topology_structure.v | 8 +- 6 files changed, 1408 insertions(+), 92 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index 9d2432a9c1..4064fcda69 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -671,7 +671,27 @@ 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 -(@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. + +End realTheory. End Theory. Module Import Exports. HB.reexport. End Exports. diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 35d2c25d50..185d27dba8 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -4,7 +4,7 @@ From mathcomp Require Import interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp contra classical_sets filter. -From mathcomp Require Import topology convex reals normedtype. +From mathcomp Require Import topology convex reals normedtype unstable. (**md**************************************************************************) (* # The Hahn-Banach theorem *) @@ -358,3 +358,91 @@ by exists g'. Qed. End hahn_banach_normed. + +Section hahn_banach_extension_ctvs. +Variable (R : realType) (V : convexTvsType R) (F : pred V). +(* In contrary to the normed case, the extention thm is not true for any subtopology on F, + but only for the finest one *) + +Import Norm. + +(* A first version specifying the seminorm bounding the function *) +(* 7.1.2 Jarchow *) +Theorem hahn_banach_extension_subctvs (F' : subConvexTvsType F) + (f : {linear F' -> R}) : + (exists2 p : SemiNorm.type V, seminorm_of p & forall z : F', f z <= p (val z)) -> + exists g : {linear_continuous V -> R}, forall x : F', g (val x) = f x. +Proof. +move=> [p ps fp]. +have convp : @convex_function _ _ [set: V] p. + rewrite /convex_function /conv => l v1 v2 _ _ /=. + rewrite [in leRHS]/conv /=. + apply: le_trans; first by exact : @ler_normD _ _ p (l%:num *: v1) (l%:num.~ *: v2). + rewrite !normZ -![_ *: _]/(_ * _) (@ger0_norm _ l%:num)//. + by rewrite (@ger0_norm _ l%:num.~)// ?mulrA// onem_ge0. +have := (@hahn_banach_extension R V _ F' f p convp fp). +move=> [g majgp F_eqgf]. +have ling : linear (g : V -> R) by exact: linearP. +have contg : continuous (g : V -> R). + by apply/lcfun_seminorm; exists p; first by apply: continuous_seminorm_of. +pose lcg := isLinearContinuous.Build _ _ _ _ g ling contg. +pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg. +by exists g'. +Qed. + + +(* A second version where F is a subspace of V, meaning endowed with the initial topology wrt to val*) +(* 7.2.1 Jarchow *) +Theorem hahn_banach_extension_initialsubctvs (F' : subLmodType F) + (f : {linear_continuous (init_subctvs F') -> R^o}) : + exists g : {linear_continuous V -> R}, forall x : F', g (val x) = f x. +Proof. +have [[openBasisV BasisV] _] := has_open_nbhs_basis V. +have [p' ps' fp'] : exists2 p : SemiNorm.type V, seminorm_of p & forall z : F', f z <= p (val z). + have /linear_continuous_seminorm: continuous (f : (init_subctvs F') -> R^o) by apply: continuous_fun. + move=> [p [cp ps] /= fp]. + have [/= nF] := cp. + move=> [] onF /= pF. + have [/(_ nF onF) + _] := basis_opennbhsbasis (init_subctvs F'). + move=> [oF [[/= oV] ooV oVF] oF0 oFn]. + have /BasisV [/= bV obV boV] : nbhs 0 oV. + rewrite nbhsE; exists oV => //; split => //. + apply: (@image_preimage_subset _ _ (val : F'-> V)). + by rewrite oVF; exists 0; rewrite ?linear0. + exists (gauge_fun_basis obV). + by exists bV; exists obV => //. + move=> z. + set pVz := (X in _ <= X). + apply: le_trans; first by apply: fp. + rewrite pF; apply: inf_le. + - move=> x /= [r [r0]]; rewrite inE => -[v bVv rvalz] <-; exists (- r); split => //; exists r; split => //. + rewrite inE; exists (r^-1 *: z). + apply: oFn; rewrite -oVF /=; apply: boV. + by rewrite linearZ /= -rvalz scalerA mulrC divff ?scale1r ?lt0r_neq0. + by rewrite scalerA divff ?scale1r ?lt0r_neq0. + - have [/= s s0 szbV]:= absorbing_opennbhsbasis obV (val z). + exists s^-1; split; rewrite ?invr_gt0 // inE /=; exists (s *: val z); first by apply/set_mem. + by rewrite scalerA mulrC divff ?scale1r ?lt0r_neq0. + - split; last by exists 0 => r [? _]; rewrite ltW. + have [/= s s0 sznF]:= absorbing_opennbhsbasis onF z. + exists s^-1; split; rewrite ?invr_gt0 // inE /=; exists (s *: z); first by apply/set_mem. + by rewrite scalerA mulrC divff ?scale1r ?lt0r_neq0. +have convp : @convex_function _ _ [set: V] p'. (* or apply the previous thm but typing *) + rewrite /convex_function /conv => l v1 v2 _ _ /=. + rewrite [in leRHS]/conv /=. + apply: le_trans; first by exact : @ler_normD _ _ p' (l%:num *: v1) (l%:num.~ *: v2). + rewrite !normZ -![_ *: _]/(_ * _) (@ger0_norm _ l%:num)//. + by rewrite (@ger0_norm _ l%:num.~)// ?mulrA// onem_ge0. +have := (@hahn_banach_extension R V _ F' f p' convp fp'). +move=> [g majgp F_eqgf]. +have ling : linear (g : V -> R) by exact: linearP. +have contg : continuous (g : V -> R). + by apply/lcfun_seminorm; exists p'; first by apply: continuous_seminorm_of. +pose lcg := isLinearContinuous.Build _ _ _ _ g ling contg. +pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg. +by exists g'. +Qed. + +Section hahn_banach_separation_ctvs. +(* TODO *) +End hahn_banach_separation_ctvs. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 1252178b3f..5f7a710fe0 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -132,7 +132,7 @@ 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). +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 +145,24 @@ 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 => + <-. +by rewrite normrZ; apply: le_lt_trans; rewrite ler_piMl. +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. + (forall b, b \in B -> absolutely_convex_set b) & (nbhs_basis 0) 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]. +exists [set B | exists2 r, 0 < r & B = ball 0 r]. + move=> b; rewrite inE /= => -[r _ ->]; split; first by exact: ball_convex_set. + by exact: ball_balanced_set. +split; first by move=> /= a [r r0 ->]; apply: nbhsx_ballx. +move=> /= b; rewrite -nbhs_ballE => -[r /= r0] b0r /=. +by exists (ball 0 r)=> //; exists r. Qed. HB.instance Definition _ := @@ -2012,10 +2020,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 41126a781d..e6d681e543 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -5,7 +5,7 @@ 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,155 @@ 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. + +Lemma absolutely_convex_setX (K : numFieldType) (E F : lmodType K) + (A : set E) (B : set F) : + absolutely_convex_set A -> absolutely_convex_set B -> + absolutely_convex_set (A `*` B). +Proof. +move=> [convA balA] [convB balB]; split. +- move => [x1 y1] [x2 y2] l /[!inE] /= -[Ax1 By1] [Ax2 By2]; split. + + by apply/set_mem/convA; exact/mem_set. + + by apply/set_mem/convB; exact/mem_set. +- move=> r r1 [x1 y1] [[x2 y2]]/= [Ax2 By2] [] <- <-; split. + + by apply/balA; [exact: r1|exists x2]. + + by apply/balB; [exact: r1|exists y2]. +Qed. + +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). + +Section addsetTheory. + +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. + +End addsetTheory. + + (* 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) := *) @@ -144,6 +294,15 @@ Lemma sum_continuous (I : Type) (r : seq I) (P : pred I) (f : I -> E -> F) : continuous (fun x1 : E => \sum_(i <- r | P i) f i x1). Proof. by move=> FC0; apply: continuous_big => //; apply: add_continuous. 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. +by apply: cvg_pair => //=; exact: cvg_cst. +exact: (@add_continuous _ (x,y)). +Qed. + End TopologicalNmodule_theory. HB.mixin Record TopologicalNmodule_isTopologicalZmodule M @@ -157,7 +316,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. @@ -172,6 +331,22 @@ 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. + +Lemma addx_nbhs x (b : set M): nbhs 0 b <-> nbhs x ([set x] `+ b). +Proof. +split. + rewrite -(subrr x) => /continuous_shift. + suff -> : [set x] `+ b = +%R^~ (- x) @^-1` b by []. + apply: funext => z /=; apply: propext; split. + by move=> [? -> [y By] <-]; rewrite addrAC subrr add0r. + by move=> byx; exists x => //; exists (z - x) => //; rewrite addrCA subrr addr0. +move=> nx. +suff -> : b = +%R^~ (x) @^-1` ([set x] `+ b ) by apply: continuous_shift; rewrite add0r. +apply: funext => z /=; apply: propext; split. + by move=> bz; exists x => //; exists z => //; rewrite addrC. +by move=> [? -> [y By]]; rewrite addrC => /addIr <-. +Qed. + End TopologicalZmoduleTheory. HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M @@ -226,7 +401,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 : @@ -240,6 +415,29 @@ 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 continuousfor0_continuous (f : {linear F -> G}) : + {for 0, continuous f} -> continuous f. +Proof. +move=> cont0 x. +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 /=. + 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. +Qed. + End TopologicalLmodule_theory. HB.factory Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M @@ -327,7 +525,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. @@ -344,6 +542,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) := @@ -392,7 +592,7 @@ 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 }. #[short(type="convexTvsType")] @@ -407,11 +607,11 @@ HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) Section SubLmodule_isSubConvexTvs. Context (R : numFieldType) (V : convexTvsType R) (S : pred V) (U : subLmodType S). -Local Notation sub_init_topo := (sub_initial_topology U). -HB.instance Definition _ := Uniform.on sub_init_topo. -HB.instance Definition _ := GRing.Lmodule.on sub_init_topo. +Definition init_subctvs := (sub_initial_topology U). +HB.instance Definition _ := Uniform.on init_subctvs. +HB.instance Definition _ := GRing.Lmodule.on init_subctvs. -Let add_sub: continuous (fun x : sub_init_topo * sub_init_topo => x.1 + x.2). +Let add_sub: continuous (fun x : init_subctvs * init_subctvs => x.1 + x.2). Proof. apply: continuous_comp_initial => -[/= x y]. pose h := fun xy : U * U => (\val xy.1, \val xy.2). @@ -421,15 +621,15 @@ rewrite (_ : _ \o _ = g \o h). apply: continuous_comp; last exact: add_continuous. apply: cvg_pair => //=. - apply: (cvg_comp _ _ cvg_fst). - exact: (continuous_valE (x : sub_init_topo)). + exact: (continuous_valE (x : init_subctvs)). - apply: (cvg_comp _ _ cvg_snd). - exact: (continuous_valE (y : sub_init_topo)). + exact: (continuous_valE (y : init_subctvs)). Qed. HB.instance Definition _ := - @PreTopologicalNmodule_isTopologicalNmodule.Build sub_init_topo add_sub. + @PreTopologicalNmodule_isTopologicalNmodule.Build init_subctvs add_sub. -Let opp_sub : continuous (-%R : sub_init_topo -> sub_init_topo). +Let opp_sub : continuous (-%R : init_subctvs -> init_subctvs). Proof. apply: continuous_comp_initial => x. rewrite (_ : _ \o _ = -%R \o \val). @@ -439,9 +639,9 @@ exact: opp_continuous. Qed. HB.instance Definition _ := - TopologicalNmodule_isTopologicalZmodule.Build sub_init_topo opp_sub. + TopologicalNmodule_isTopologicalZmodule.Build init_subctvs opp_sub. -Let scale_sub : continuous (fun z : R^o * sub_init_topo => z.1 *: z.2). +Let scale_sub : continuous (fun z : R^o * init_subctvs => z.1 *: z.2). Proof. apply: continuous_comp_initial => - [] /= x /= y. pose h := fun xy : R * U => (xy.1, \val xy.2). @@ -449,7 +649,7 @@ pose g := fun xy : R * V => xy.1 *: xy.2. rewrite (_ : _ \o _ = g \o h); first by apply/funext=> i /=; rewrite GRing.valZ. apply: continuous_comp; last exact: scale_continuous. move=> /= A [/= [/= B C]] [[r/= r0 xrB]]. -move/(continuous_valE (y : sub_init_topo)) => [/= C' [woC' C'y C'C] BCA]. +move/(continuous_valE (y : init_subctvs)) => [/= C' [woC' C'y C'C] BCA]. apply: filterS; first exact: BCA. exists (ball x r, C') => /=. by split; [exact: nbhsx_ballx|exists C'; split]. @@ -457,38 +657,36 @@ by move=> su/= [xru C'u]; split; [exact: xrB|exact: C'C]. Qed. HB.instance Definition _ := - TopologicalZmodule_isTopologicalLmodule.Build R sub_init_topo scale_sub. + TopologicalZmodule_isTopologicalLmodule.Build R init_subctvs scale_sub. 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. +Let locally_convex_sub : exists2 B : set_system init_subctvs, + (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 absconvB [B0 nbhsb]] := @locally_convex R V. +rewrite /filter_from /= in nbhsb. 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. +split. + move=> ? /= [b /B0] + <-. + by rewrite -[X in nbhs X _ -> _](linear0 (\val : U -> V)); exact: initial_nbhs. +move=> /= A [a' [/= [/= b ob <-] /= b0 ba]]. +have /nbhsb [b' Bb 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 exists b'. Qed. Local Close Scope convex_scope. HB.instance Definition _ := - @Uniform_isConvexTvs.Build R sub_init_topo locally_convex_sub. -HB.instance Definition _ := GRing.SubLmodule.on sub_init_topo. + @Uniform_isConvexTvs.Build R init_subctvs locally_convex_sub. +HB.instance Definition _ := GRing.SubLmodule.on init_subctvs. End SubLmodule_isSubConvexTvs. @@ -508,7 +706,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). @@ -533,7 +731,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. @@ -548,8 +746,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. @@ -562,7 +760,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)) : @@ -611,7 +809,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. @@ -624,7 +822,6 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E entourage_inv entourage_split_ex nbhsE. - HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build E add_continuous. HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R E scale_continuous. @@ -633,18 +830,329 @@ HB.instance Definition _ := Uniform_isConvexTvs.Build R E locally_convex. HB.end. + +HB.factory Record Nbhsbasisat0_isConvexTvs (R: numFieldType) E & GRing.Lmodule 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. + +HB.builders Context R E & Nbhsbasisat0_isConvexTvs R E. + +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. +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. + by exists ([set p] `+ U) => //=; exists U. + move=> _ _ /= [U0 FU <-] [V0 FV <-]. + have [W FW WUV] := nbhsbasis_at0I FU FV. + 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. + +#[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. +rewrite /nbhs_fromfilter0/=. +move=> [B/= [C f0C <- pCA]] //=. +have [D f0D DDC] := split_nbhsbasisat0 f0C. +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))); 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. + + +#[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 [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). +rewrite inE => xV''. +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. +Proof. +exists nbhsbasis_at0; first by move=> b; rewrite inE; apply: absconvex_nbhsbasisat0. +split; first by move=> /= A nA; exists A => //; exists A => //; rewrite addset0. +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 := { + 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. + +Let 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). +Context (R : numDomainType) (E : convexTvsType R). -Lemma nbhs0N : nbhs 0 U -> nbhs 0 (-%R @` U). +Lemma nbhs0N (U : set E) : 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 nbhsD0 (U : set E) (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). +Lemma nbhsD (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U). Proof. exact/nbhsB_subproof/add_continuous. Qed. +Lemma openD (V : set E) (x : E) : open V -> open ((+%R x @` V)). +Proof. +rewrite openE /= => openV z /= [y uy <-]; rewrite /interior /=. +by apply: nbhsD; rewrite nbhsE /=; exists V => //; split => //; rewrite openE. +Qed. + +Lemma openB (U : set E) (x : E) : open ((+%R x @` U)) -> open U. +Proof. +suff : U = ((+%R (-x) @` (+%R x @` U))) by move => + H; move => ->; apply: openD. +apply/seteqP; split => z /=. + move=> Uz; exists (z + x); first by exists z => //; rewrite addrC. + by rewrite -addrCA [X in (_ + X = _)]addrC subrr addr0. +by move=> [y [y' Uy' <-] <-]; rewrite addrCA addrA subrr add0r. +Qed. + +Lemma nbhsE0 (x : E) (b : set E): nbhs x b <-> b x /\ exists2 a, nbhs 0 a & ([set x + x0 | x0 in a]) `<=` b. +Proof. +split. + move => /[dup] /(nbhsD (-x)); rewrite addNr => nb0 nb; split; first by apply: nbhs_singleton. + exists [set - x + x0 | x0 in b] => // z /=. + by move=> [y /= [y' by']] <- <-; rewrite addrA addrN add0r. +move=> [bx [a n0a xab]]; apply: filterS; first by exact: xab. +by apply: nbhsD0. +Qed. + End ConvexTvs_numDomain. Section ConvexTvs_numField. @@ -667,8 +1175,43 @@ near=> z; exists (r^-1 *: z); last by rewrite scalerA divff// scale1r. by apply: (BU (r^-1,z)); split; [exact: nbhs_singleton|near: z]. Unshelve. all: by end_near. Qed. +Lemma openZ (R : numFieldType) (E : convexTvsType R) (U : set E) (r : R) : + r != 0 -> open U -> open ( *:%R r @` U ). +Proof. +move=> r0; rewrite openE /interior /= => openU z /= [x Ux <-]; apply: nbhsZ => //. +by rewrite nbhsE => /=; exists U => //; split; rewrite // openE. +Qed. + End ConvexTvs_numField. + +Section ConvexTvs_realType. + +(*better naming ?*) +Lemma scalerx_continuous (R : realType) (E : convexTvsType R) (x : E) (s : R) : + {for s, continuous (fun t : R^o => t *: x)}. +Proof. +have -> : (fun t : R^o => t *: x) = (fun z => z.1 *: z.2) \o (fun r => (r,x)) by apply: funext. +apply: continuous_comp. +apply: (@cvg_pair _ R^o _ _ (nbhs (s : R^o))) => //=; first by exact: cvg_cst. +by exact: (scale_continuous (s : R^o,x)). +Qed. + +(* why is cvg_cst defined only on realtypes ? *) + +Lemma scalexr_continuous (R : realType) (E : convexTvsType R) (x : E) (s : R) : + {for x, continuous (fun y : E => s *: y)}. +Proof. +have -> : (fun y: E => s *: y ) = (fun z => z.1 *: z.2) \o (fun y => (s, y)). + by apply: funext. +apply: continuous_comp. +apply: (@cvg_pair _ R^o _ _ (nbhs (s : R^o))) => //=; first by exact: cvg_cst. +by exact: (scale_continuous (s: R^o, x)). +Qed. + +End ConvexTvs_realType. + + Section standard_topology. Variable R : numFieldType. @@ -693,6 +1236,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 +1250,23 @@ 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 => + <-. +by rewrite normrM; apply: le_lt_trans; rewrite ler_piMl. +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 | exists2 r, 0 < r & B = ball 0 r]. + move=> B /[!inE]/= -[r _ ->]; split. + - exact: standard_ball_convex_set. + - exact: standard_ball_balanced_set. +split; first by move=> /= ? [r r0 ->]; exact: nbhsx_ballx. +by move=> /= B [r r0 Br]; exists (ball 0 r); [exists r|exact: Br]. Qed. HB.instance Definition _ := @@ -753,28 +1306,23 @@ 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. -Proof. -have [Be Bcb Beb] := @locally_convex K E. -have [Bf Bcf Bfb] := @locally_convex K F. -pose B := [set ef : set (E * F) | open ef /\ - 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]. -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]. + exists2 B : set_system (E * F), (forall b, b \in B -> absolutely_convex_set b) + & nbhs_basis (0, 0) B. +Proof. +have [Be Bce [Be0 Beb]] := @locally_convex K E. +have [Bf Bcf [Bf0 Bfb]] := @locally_convex K F. +pose B := [set be `*` bf | be in Be & bf in Bf]. +have B00 : nbhs_basis (0, 0) B. + split. + by move=> /= b [be ?] [bf ?] <-; exists (be, bf) => //=; split => //; + [exact/Be0|exact/Bf0]. + move=> /= b [[/= be bf] [/= nbe nbf]] befb /=. + have [/= be' Beb' bbe] := Beb be nbe. + have [/= bf' Bfb' bbf] := Bfb bf nbf. + exists (be' `*` bf') => /=; first by exists be' => //; exists bf'. + by apply: subset_trans befb; exact: setSX. +exists B => // b; rewrite inE /= => -[be Bbe] [bf Bbf] <-. +by apply: absolutely_convex_setX; [exact/Bce/mem_set|exact/Bcf/mem_set]. Qed. HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build @@ -952,3 +1500,646 @@ Lemma lcfun_linear : linear f. Proof. move => *; exact: linearP. Qed. End lcfunproperties. + +Section openbasis. +Context (R : realType) (E: convexTvsType R). + +Definition nbhsbasis_ctvs := sval (cid2 (@locally_convex _ E)). + +Definition open_nbhsbasis_ctvs := [set b| exists2 b', nbhsbasis_ctvs b' & b = interior b']. + +(* TODO : convex is enough and then take balanced closure *) +Lemma has_open_nbhs_basis : + nbhs_basis 0 open_nbhsbasis_ctvs /\ ( forall b, open_nbhsbasis_ctvs b -> (open b /\ absolutely_convex_set b)). +Proof. +have [absconv [] nbhs0 basis] := (svalP (cid2 (@locally_convex _ E))). +split. + split; move=> a /=; first by move => [b /nbhs0 nbhsb ->]; apply: nbhs_interior. + move=> /basis /= [b /= nbhsb ba]; exists (interior b); first by exists b => //. + apply: subset_trans; last by exact: ba. + exact: interior_subset. +move=> ? /= [b nb ->]; split; first by exact: open_interior. +have [convb balb] := absconv b (mem_set nb). +split; rewrite /interior. + move => x y t; rewrite !inE. + move=> /nbhsE0 [bx [ax nax axb]] /nbhsE0 [by' [ay nay ayb]]; apply/nbhsE0; split. + by apply/set_mem/convb; rewrite !inE. + exists (ax `&` ay); first by apply: filterI. + move=> z /= [z' [xz xz'] <-]. + (*have -> : conv t x y + z' = conv t (x + z') (y + z').*) (*souci avec conv t (x+x0) (y+y0)*) + rewrite /conv /=. + have ->: t%:num *: x + (t%:num).~ *: y + z' = t%:num *: (x + z') + (t%:num).~ *: (y + z'). + rewrite !scalerDr -[in RHS]addrA. + rewrite [in X in (_ = _ + X)]addrCA [in X in (_ = _ + ( _ + X))]scalerBl. + by rewrite [in X in (_ = _ + ( _ + X))]addrCA addrN addr0 scale1r addrA. + apply/set_mem/convb; rewrite inE; first by apply: axb; exists z'. + by apply: ayb; exists z'. +move=> /= t. +case: (eqVneq t 0). (*disctinction overlooked in the literature*) + by move=> -> _ ? /= [?] _; rewrite scale0r => <-; apply: nbhs0 => /=; exact: nb. +move=> t0 t1 ? /= [x] /= + <-; move/nbhsE0 => [bx [a na0 ab]]. +apply/nbhsE0; split. + apply: balb; first by exact: t1. + by exists x. +exists (t `*: a). + by rewrite -(@scaler0 _ _ t); apply: nbhsZ => // ? /= [y ay] <-; apply: ab; exists y. +move => z /= [?] [y] ax <- <-; rewrite -scalerDr; apply: balb; first by exact: t1. +by exists (x + y)=> //; apply: ab; exists y. +Qed. + +Definition open_absconvex_opennbhsbasis := has_open_nbhs_basis.2. + +Definition basis_opennbhsbasis := has_open_nbhs_basis.1. + +Lemma basis_neqset0 (B : (set (set E))) (x : E): (filter_from [set U | B U] id --> x) -> B !=set0. +Proof. +by move=> /(_ [set: E]) /(_ filterT) [b ? _]; exists b. +Qed. + +Lemma absorbing_opennbhsbasis : forall b, open_nbhsbasis_ctvs b -> pabsorbing_set b. +Proof. +move=> b Bb x. +have [/(_ b Bb) n0b _] := (basis_opennbhsbasis ). +move: n0b; rewrite -(scale0r x) => n0b. +have := scalerx_continuous => /(_ _ _ x 0 b n0b) [r] /= r0 b0rb. +exists (r/2); first by apply: divr_gt0. +rewrite inE. +apply: b0rb; rewrite /ball_ /= sub0r normrN normrM !gtr0_norm //. +by rewrite gtr_pMr // invf_lt1 // ltrDl. +Qed. + +End openbasis. + +Import Norm. + +(* A should be absolutely convex and absorbing *) +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). + +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. + +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; first 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. + + +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). + +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 H) seminorm_subbasis nonempty_subbasis mem0_seminorm_subbasis expand_seminorm_subbasis absorbing_seminorm absolutely_convex_seminorm_subbasis. + +(* NB: Using init-fam (see initial_topology.v) doesn't work as we strongly need a 0 basis. With init-fam we are considering nbhs a = [ [A : set E |, exists e , A = [x | |p(x) - p(a)| 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 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. + 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 //. + 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 -> /=. + move => t /= [? ->] [y] bally <-; apply: pxrA => /=. rewrite (le_lt_trans _ bally) => //. + rewrite sub0r normrN [leRHS]ger0_norm ?norm_ge0 //. + 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 := (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). + by rewrite -(subrr x)=> A /= /continuous_shift; apply. +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. + +Section generating_seminorm. +Context (R : realType) (E : convexTvsType R). + +Definition gauge_fun_basis (b : set E) (h : (open_nbhsbasis_ctvs b)) := +gauge_fun (open_absconvex_opennbhsbasis h).2 (absorbing_opennbhsbasis h). + +Definition seminorm_of := +[set p : SemiNorm.type E | exists b, exists h : (open_nbhsbasis_ctvs b), + p = gauge_fun_basis h]. + +#[local] Lemma seminorm_ofneq0 : seminorm_of !=set0. +Proof. +have [_ /(_ [set: E] filterT)] := basis_opennbhsbasis; move=> [/= b Bb _]. +exists (gauge_fun_basis Bb). +by exists b; exists Bb. +Qed. + +#[local] Notation seminormE := (@seminorm_on R E seminorm_of seminorm_ofneq0 : convexTvsType R). + +Let ball_gauge_fun (A : set E) (r : R) (r0 : 0 < r) + (absA : absolutely_convex_set A) (pabsA: pabsorbing_set A) (_: open A): + (gauge_fun absA pabsA) @^-1` (ball (0 : R) r) = (fun y : E => r^-1 *: y) @^-1` A. +Proof. +apply/seteqP; split => y /=; rewrite /ball /= sub0r normrN ger0_norm ?gauge_ge0 //. + move/inf_lt => []. + have := pabsA y => -[r' r'0]; rewrite inE => r'yb. + exists r'^-1 => /=; split; first by rewrite invr_gt0. + rewrite inE /=; exists (r'*: y) => //. + by rewrite scalerA mulrC divff ?scale1r ?lt0r_neq0. + move=> t [t0]; rewrite inE => /= -[y' by' <-] tr. + have [_ /(_ (t/r))]:= absA; apply. + by rewrite gtr0_norm ?divr_gt0 // ler_pdivrMr // mul1r ltW. + by exists y' => //; rewrite scalerA mulrC. + move=> Ary. + have: exists2 t : R , (0 < t < 1) & (r^-1 *: y \in t `*: A). + have /scalerx_continuous : nbhs (1 *: (r^-1 *: y)) A. + by rewrite scale1r; apply: open_nbhs_nbhs; split => //. + move => [s /= s0] b1s. + exists ((1 + `|s|/2 )^-1). + rewrite ?invr_gt0 ?addr_gt0 ?mulr_gt0 ?normr_gt0 ?lt0r_neq0 ?invr_gt0 //. + apply/andP; split => //. + by rewrite invf_lt1 ?ltrDl ?addr_gt0 ?mulr_gt0 ?normr_gt0 ?lt0r_neq0 ?invr_gt0. + rewrite inE; exists ((1 + `|s| / 2) *: (r^-1 *: y)). + apply: b1s => /=. + rewrite opprD addrA subrr add0r normrN gtr0_norm ?mulr_gt0 ?normr_gt0 //. + - by rewrite lt0r_neq0. + - by rewrite gtr0_norm ?gtr_pMr ?invf_lt1 ?ltrDl //. + by rewrite scalerA mulVf ?scale1r //. +move=> [t /andP [t0 t1] rytb]. +have lepr: - (t*r) <= sup [set - x | x in [set r1 | 0 < r1 /\ y \in r1 `*: A]]. + set B := ( X in _ <= sup X). + have Br : B (- (t * r)). + exists (t * r); split => //; rewrite ?mulr_gt0 //. + rewrite inE; exists (t^-1 *: (r^-1 *: y)) => //. + have := rytb; rewrite inE => -[z bź <-]; rewrite scalerA mulVf ?lt0r_neq0 //. + by rewrite scale1r. + by rewrite !scalerA -?mulrA (mulrC r) -mulrA mulVf ?mulr1 ?gt_eqF// divff ?scale1r// gt_eqF. + have: has_ubound B by exists 0 => ? [s [s0 _]] <-; rewrite ltW // oppr_lt0. + by move/ub_le_sup/(_ _ Br). +apply: le_lt_trans; first by rewrite lerNl; exact lepr. +by rewrite gtr_pMl. +Qed. + +From mathcomp Require Import finmap. (* how to do without *) +(* TODO : uniformise the usage of `+ or (+%R~ @) withine lemmas *) +Theorem seminorm_convextvs : continuous (id : E -> seminormE) /\ (continuous (id : seminormE -> E)). +Proof. +pose B := open_nbhsbasis_ctvs. +split=> x a. + move=> [/=b [?]] [I /= Ig] /= <- <- /filterS; apply. + apply/addx_nbhs. + apply: filter_bigI => /= i /Ig /set_mem /= => -[? [b' [nb']]] -> [/= r r0 ->]. + have [/(_ b' nb') nbhsB _] := basis_opennbhsbasis. + set p := (X in nbhs 0 (X @^-1` ball 0 r)). + have -> : (p @^-1` ball (0 : R) r) = (fun y : E => r^-1 *: y) @^-1` b'. + by apply: ball_gauge_fun => //; exact: (open_absconvex_opennbhsbasis nb').1. + by apply: scalexr_continuous; rewrite scaler0. +move => /nbhsE0 /= [ax] /= [b n0b ba]. +have [_ /(_ b n0b) /= [b'/=]] := basis_opennbhsbasis. +move=> Bb' bb'. +pose p:= gauge_fun (open_absconvex_opennbhsbasis Bb').2 (absorbing_opennbhsbasis Bb'). +have /open_absconvex_opennbhsbasis [ob' absconvb'] := Bb'. +exists ([set x] `+ p @^-1` ball (0 : R) 1) => /=; last first. + rewrite ball_gauge_fun => // z /= [? ->] [y]; rewrite invr1 scale1r => b1y xyz. + by apply: ba; exists y => //; apply: bb'. +exists (p @^-1` ball (0 : R) 1) => //. +exists ([fset p @^-1` (ball (0 : R) 1)]%fset). + move=> c; rewrite !inE; move/eqP => ->; apply/mem_set => /=. + exists p; last by exists 1. + by exists b'; exists Bb'. +rewrite /bigcap; apply/seteqP; split => z /=. + by move => /(_ (p @^-1` ball (0: R) 1)); apply; rewrite inE. +by move => b1z ?; rewrite inE => /eqP ->. +Qed. + +Lemma continuous_seminorm_of q : (seminorm_of q) -> continuous q. +Proof. +have -> : (q : E -> R) = (q : seminormE -> R^o) \o (id : seminormE -> E) by []. +move=> qs x. +have contid : {for x, continuous (id : E -> seminormE)}. + by have [contid' _] := seminorm_convextvs; apply: (contid' x). +have cq : {for x, continuous (q : seminormE -> R^o)}. + by apply: (@continuous_seminorm R^o E seminorm_of _ (id x)). +by apply: (continuous_comp contid cq). +Qed. + +#[local] Definition cst0 : E -> R := fun x => 0. +#[local] Lemma cst00 : cst0 0 = 0. Proof. by []. Qed. +#[local] Lemma cst0_ge0 : forall x, 0 <= cst0 x. Proof. by []. Qed. +#[local] Lemma ler_cst0D : forall x y, cst0 (x + y) <= cst0 x + cst0 y. + Proof. by move=> x y /=; rewrite addr0. Qed. +#[local] Lemma cst0Z : forall r x, cst0 (r *: x) = `|r| * cst0 x. + Proof. by move=> r x; rewrite mulr0. Qed. + +HB.instance Definition _ := @isSemiNorm.Build R E cst0 cst00 cst0_ge0 ler_cst0D cst0Z. + +(* The litterature usually states the following lemmas using a family of seminorms p_i, a family of multiplicative constantcs Ci and bounds the abs value of l : `|l i| <= sup C_i p_i (x). +We simplify these arguments using the linearity of l to get rid of the absolute value. *) +(* 6.6.4 in Jarchow *) +Lemma linear_continuous_seminorm (l : {scalar E}): (* TODO : be more explicit in the statement *) +continuous l -> (exists2 p : SemiNorm.type E, (seminorm_of p /\ continuous p) & (forall x, l x <= p x)). +Proof. +have [Bnbhs Bbasis] := basis_opennbhsbasis. +move => /[dup] cl /(_ 0 (ball (0 : R) 1)); rewrite linear0. +move => /(_ (nbhsx_ballx (0 : R) 1 ltr01 )). +have lem : 2^-1 !=0 :>R by []. +move/(nbhsZ lem); rewrite scaler0 => /Bbasis /= [b /= Bb bl] {lem}. +have {bl} bl : b `<=` [set t | `|l (t)| < 2^-1]. + move => t /bl; rewrite /ball /= => -[x]; rewrite sub0r normrN. + move=> lx <-; rewrite linearZ /= normrM ger0_norm //. + by rewrite -[X in _ < X]mulr1 ltr_pM2l. +have [_ /(_ 0 b (Bnbhs b Bb))] := seminorm_convextvs. +move=> n0b. +pose q : SemiNorm.type E := gauge_fun_basis Bb. +exists q. + split; first by exists b; exists Bb. + by apply: continuous_seminorm_of; exists b; exists Bb. +move => x. +case : (eqVneq x 0); first by move => ->; rewrite linear0 norm0. +move=> x0. +case : (eqVneq (q x) 0). + move=> qx0. (* case forgotten in the litterature *) + suff: (l x) = 0 by move => ->; rewrite norm_ge0. + move: qx0; rewrite /q /= /gauge_fun /= => qx0. + have lxe (e : R) (e0 : 0 < e) : `|l x | < e. + have:= (bl (e^-1*:x)) => /=. + rewrite linearZ /= normrM normfV ltr_pdivrMl ?normr_gt0 ?lt0r_neq0 //. + rewrite (gtr0_norm e0) => lem; apply : lt_trans. + apply: lem. + have hasinf : has_inf [set r | 0 < r /\ x \in r `*: b]. + split; last by exists 0 => z /= [] z0 _; apply: ltW. + have [r r0] := absorbing_opennbhsbasis Bb x. + move/set_mem => bx. + exists r^-1 => /=; split; rewrite ?invr_gt0 //; apply/mem_set. + by exists (r *: x) => //; rewrite scalerA ?mulVf ?lt0r_neq0 ?scale1r. + have [eps [eps0 /set_mem /= [y by' epsyx]]] := inf_adherent e0 hasinf. + rewrite qx0 add0r -epsyx scalerA => epse; rewrite ?mulVf. + have /(_ (e^-1 * eps)):= ((open_absconvex_opennbhsbasis Bb).2).2. + apply => //=; last by exists y. + by rewrite ger0_norm ?mulr_ge0 ?invr_ge0 ?ler_pdivrMl ?ltW ?mulr1. + by rewrite gtr_pMr ?invf_lt1 ?ltrDl //. + apply: contrapT => /eqP h. + have:= lxe `|l x|. + by rewrite normr_gt0 ltxx falseE; apply. +move=> qx0. +pose y := ((2 * q x)^-1) *: x. +rewrite ltW => //. +have : `|l (y)| < 2^-1. + apply/bl. + have : (q @^-1` ball (0 : R) 1) (((2 * q x)^-1) *: x). + move => /=; rewrite sub0r normrN ger0_norm ?norm_ge0 //. + rewrite normZ /= ger0_norm ?mulr_ge0 ?invr_ge0 ?norm_ge0 //. + by rewrite mulr_ge0 ?norm_ge0 . + rewrite invfM -mulrA mulVf // ltr_pdivrMl ?mulr1 ?ltrDl //=. + by suff : 0 < 1 :> R by []. + rewrite ball_gauge_fun => //; first by have [] := open_absconvex_opennbhsbasis Bb. + by rewrite /= invr1 scale1r. +rewrite /y linearZ normrM normfV normrM ger0_norm // ltr_pdivrMl. + by rewrite mulr_gt0 ?normr_gt0. +rewrite mulrAC divff // mul1r [in X in _ < X -> _]ger0_norm ?norm_ge0 //. +move/le_lt_trans => /(_ (l x)); apply. +by rewrite ler_normr; apply/orP; left. +Qed. + +Lemma linear_seminorm_continuous (l : {scalar E}): + (exists2 p : SemiNorm.type E, continuous p & (forall x, l x <= p x)) + -> continuous (l : E -> R^o). +Proof. +move=> [p px lpxl]; apply: continuousfor0_continuous => /= a. +rewrite linear0 => -[/= e e0] balla. +have /filterS : (p @^-1` (ball_ [eta normr] (0 : R) ( e)) ) `<=` (l @^-1` a). + move=> z /=; rewrite sub0r normrN ger0_norm ?norm_ge0 // => pze. + apply: balla => /=; rewrite sub0r normrN. + apply: le_lt_trans; last by apply: pze. + case : (leP 0 (l z)) => g0; first by rewrite ger0_norm. + rewrite ltr0_norm //; have := lpxl (- z). + by rewrite linearN -[in X in _ <= X -> _]scaleN1r normZ normrN normr1 mul1r. +apply => /=; rewrite -(@norm0 _ _ p); apply: px. +by rewrite norm0 ; apply: nbhsx_ballx. +Qed. + +Proposition lcfun_seminorm (l : {scalar E}): +continuous l <-> + (exists2 p : SemiNorm.type E, continuous p & (forall x, l x <= p x)). +Proof. +split; last by apply: linear_seminorm_continuous. +by move/linear_continuous_seminorm => [p [_ cp] lpx]; exists p. +Qed. + +End generating_seminorm. diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index 943c1210cb..56c4cc5496 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. @@ -101,6 +101,13 @@ rewrite nbhs_filterE; apply: filterS FC. by apply: subset_trans sBfA; rewrite -fCeB; apply: preimage_image. Qed. +Lemma initial_nbhs (x : W) b : nbhs (f x) b -> nbhs x (f @^-1` b). +Proof. +rewrite nbhsE /= => -[b' [b0 ob]] bb'. +exists (f @^-1` b'); split => //= ; first by exists b'. +by move => z /= /bb'. +Qed. + End Initial_Topology. (*#[deprecated(since="mathcomp-analysis 1.17.0", note="renamed `initial_open`")] Notation wopen := initial_open (only parsing).*) diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index a6170e44b1..95f8addfe2 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_system T) := B `<=` open /\ forall x, filter_from [set U | B U /\ U x] id --> x. +Definition nbhs_basis (x : T) (B : set (set T)) := + (B `<=` nbhs x) /\ filter_from [set U | B U] id --> x. + Definition second_countable := exists2 B, countable B & basis B. Global Instance nbhs_pfilter (p : T) : ProperFilter (nbhs p). @@ -496,6 +499,9 @@ 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 +515,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 bd0641e65fb8f4483ed49f4186833ef3baf9c3ad Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 7 Jul 2026 12:24:57 +0900 Subject: [PATCH 2/4] fix --- .../functional_analysis/hahn_banach_theorem.v | 2 + theories/normedtype_theory/tvs.v | 53 +++++-------------- theories/topology_theory/initial_topology.v | 2 +- 3 files changed, 15 insertions(+), 42 deletions(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 185d27dba8..e50d9617b0 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -443,6 +443,8 @@ pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg. by exists g'. Qed. +End hahn_banach_extension_ctvs. + Section hahn_banach_separation_ctvs. (* TODO *) End hahn_banach_separation_ctvs. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index e6d681e543..6ed957cb54 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -97,38 +97,16 @@ 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 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 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. @@ -161,7 +139,7 @@ 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). +Lemma absolutely_convex_hull_set (A : set V) : absolutely_convex_set (absolutely_convex_hull A). Proof. apply: bigcap_closed_smallest => H Habs. split. @@ -169,17 +147,10 @@ split. - 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_convex_hull_subset (A : set V) : A `<=` absolutely_convex_hull A. +Proof. exact: sub_gen_smallest. Qed. -Lemma absolutely_convex0 (B : set V) : B !=set0 -> absolutely_convex_set B -> B 0. +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. @@ -1945,7 +1916,7 @@ Definition seminorm_of := #[local] Lemma seminorm_ofneq0 : seminorm_of !=set0. Proof. -have [_ /(_ [set: E] filterT)] := basis_opennbhsbasis; move=> [/= b Bb _]. +have [_ /(_ [set: E] filterT)] := basis_opennbhsbasis E; move=> [/= b Bb _]. exists (gauge_fun_basis Bb). by exists b; exists Bb. Qed. @@ -2005,13 +1976,13 @@ split=> x a. move=> [/=b [?]] [I /= Ig] /= <- <- /filterS; apply. apply/addx_nbhs. apply: filter_bigI => /= i /Ig /set_mem /= => -[? [b' [nb']]] -> [/= r r0 ->]. - have [/(_ b' nb') nbhsB _] := basis_opennbhsbasis. + have [/(_ b' nb') nbhsB _] := basis_opennbhsbasis E. set p := (X in nbhs 0 (X @^-1` ball 0 r)). have -> : (p @^-1` ball (0 : R) r) = (fun y : E => r^-1 *: y) @^-1` b'. by apply: ball_gauge_fun => //; exact: (open_absconvex_opennbhsbasis nb').1. by apply: scalexr_continuous; rewrite scaler0. move => /nbhsE0 /= [ax] /= [b n0b ba]. -have [_ /(_ b n0b) /= [b'/=]] := basis_opennbhsbasis. +have [_ /(_ b n0b) /= [b'/=]] := basis_opennbhsbasis E. move=> Bb' bb'. pose p:= gauge_fun (open_absconvex_opennbhsbasis Bb').2 (absorbing_opennbhsbasis Bb'). have /open_absconvex_opennbhsbasis [ob' absconvb'] := Bb'. @@ -2055,7 +2026,7 @@ We simplify these arguments using the linearity of l to get rid of the absolute Lemma linear_continuous_seminorm (l : {scalar E}): (* TODO : be more explicit in the statement *) continuous l -> (exists2 p : SemiNorm.type E, (seminorm_of p /\ continuous p) & (forall x, l x <= p x)). Proof. -have [Bnbhs Bbasis] := basis_opennbhsbasis. +have [Bnbhs Bbasis] := basis_opennbhsbasis E. move => /[dup] cl /(_ 0 (ball (0 : R) 1)); rewrite linear0. move => /(_ (nbhsx_ballx (0 : R) 1 ltr01 )). have lem : 2^-1 !=0 :>R by []. diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index 56c4cc5496..3e715715c1 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 all_algebra all_classical finmap. +From mathcomp Require Import all_ssreflect_compat algebra all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import interval_inference reals topology_structure. From 5624346f4a27c7ad0f5eeb1b01cc9ea03c0fb2fe Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 7 Jul 2026 16:05:41 +0900 Subject: [PATCH 3/4] changelog, clean (wip) --- CHANGELOG_UNRELEASED.md | 47 ++ classical/unstable.v | 5 - .../functional_analysis/hahn_banach_theorem.v | 8 +- theories/normedtype_theory/normed_module.v | 4 +- theories/normedtype_theory/tvs.v | 609 ++++++++---------- theories/topology_theory/initial_topology.v | 7 +- theories/topology_theory/topology_structure.v | 4 +- 7 files changed, 336 insertions(+), 348 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2d85fdc0a5..db5c76462b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -234,6 +234,43 @@ - in `measurable_structure.v`: + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` +- in `unstable.v`: + + lemma `seminorm_normrB` + +- in `initial_topology.v`: + + lemma `initial_nbhs_preimage` + +- in `topology_structure.v`: + + definition `nbhs_basis` + + definition `open_from` + +- in `normed_module.v`: + + lemma `ball_convex_set` (was a `Let`) + +- in `tvs.v`: + + definition `balanced_set` + + definition `absolutely_convex_set` + + lemma `absolutely_convex0` + + definition `pabsorbing_set` + + lemma `absolutely_convex_setX` + + notation `... `+ ...` + + lemmas `addsetS`, `add0set`, `addsetI`, `addsetA` + + lemma `continuous_shift` + + lemma `nbhs_add1set` + + definition `init_subconvextvs` + + factory `NbhsBasisAt0_isConvexTvs` + + definition `filter_from_basis0` + + factory `NbhsSubbasisAt0_isConvexTvs` + + definition `finI_fromsubbasis0` + + lemma `openD` + + lemma `openB` + + lemma `nbhsE0` + + lemma `openZ` + + lemma `scalerx_continuous` + + lemma `scalexr_continuous` + + definition `nbhsbasis_convextvs` + + definition `open_nbhsbasis_convextvs` + ### Changed - in `realsum.v`: @@ -354,6 +391,9 @@ - in `classical_sets.v` + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) +- from `normed_module.v` to `tvs.v`: + + lemma `continuousfor0_continuous` (moved and generalized) + ### Renamed - in `tvs.v`: @@ -407,6 +447,13 @@ - in `functions.v` + lemma `scalrfctE` -> `scalerfctE` (deprecating `scalrfctE`) +- in `tvs.v`: + + lemma `nbhsT_subproof` -> `nbhsD_subproof` + +- in `tvs.v`: + + lemma `nbhsT` -> `nbhsD0` + + lemma `nbhsB` -> `nbhsD` + ### Generalized - in `measurable_structure.v`: diff --git a/classical/unstable.v b/classical/unstable.v index 4064fcda69..c95c1c6a32 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -671,11 +671,6 @@ 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. diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index e50d9617b0..dcd7307291 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -4,7 +4,7 @@ From mathcomp Require Import interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp contra classical_sets filter. -From mathcomp Require Import topology convex reals normedtype unstable. +From mathcomp Require Import topology convex reals normedtype. (**md**************************************************************************) (* # The Hahn-Banach theorem *) @@ -394,16 +394,16 @@ Qed. (* A second version where F is a subspace of V, meaning endowed with the initial topology wrt to val*) (* 7.2.1 Jarchow *) Theorem hahn_banach_extension_initialsubctvs (F' : subLmodType F) - (f : {linear_continuous (init_subctvs F') -> R^o}) : + (f : {linear_continuous (init_subconvextvs F') -> R^o}) : exists g : {linear_continuous V -> R}, forall x : F', g (val x) = f x. Proof. have [[openBasisV BasisV] _] := has_open_nbhs_basis V. have [p' ps' fp'] : exists2 p : SemiNorm.type V, seminorm_of p & forall z : F', f z <= p (val z). - have /linear_continuous_seminorm: continuous (f : (init_subctvs F') -> R^o) by apply: continuous_fun. + have /linear_continuous_seminorm: continuous (f : (init_subconvextvs F') -> R^o) by apply: continuous_fun. move=> [p [cp ps] /= fp]. have [/= nF] := cp. move=> [] onF /= pF. - have [/(_ nF onF) + _] := basis_opennbhsbasis (init_subctvs F'). + have [/(_ nF onF) + _] := basis_opennbhsbasis (init_subconvextvs F'). move=> [oF [[/= oV] ooV oVF] oF0 oFn]. have /BasisV [/= bV obV boV] : nbhs 0 oV. rewrite nbhsE; exists oV => //; split => //. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 5f7a710fe0..0f659c83e0 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -158,8 +158,8 @@ Let locally_convex_set : (forall b, b \in B -> absolutely_convex_set b) & (nbhs_basis 0) B. Proof. exists [set B | exists2 r, 0 < 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 inE /= => -[r _ ->]; split; first exact: ball_convex_set. + exact: ball_balanced_set. split; first by move=> /= a [r r0 ->]; apply: nbhsx_ballx. move=> /= b; rewrite -nbhs_ballE => -[r /= r0] b0r /=. by exists (ball 0 r)=> //; exists r. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 6ed957cb54..fed2c9bc63 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -5,7 +5,8 @@ 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 initial_topology topology num_normedtype. +From mathcomp Require Import convex set_interval reals topology. +From mathcomp Require Import initial_topology num_normedtype. From mathcomp Require Import pseudometric_normed_Zmodule. (**md**************************************************************************) @@ -78,7 +79,6 @@ 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 }"). @@ -100,65 +100,24 @@ Local Open Scope ring_scope. 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 -> ( *:%R r) @` 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. +Lemma absolutely_convex0 (A : set V) : A !=set0 -> absolutely_convex_set A -> + A 0. 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_hull_subset (A : set V) : A `<=` absolutely_convex_hull A. -Proof. 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. +move => [] x Ax [] _ /(_ 0); rewrite normr0 ler01 // => /(_ isT) /(_ 0); apply. by exists x; rewrite //= scale0r. Qed. +Definition pabsorbing_set (A : set V) := + forall x : V, exists2 r, 0 < r & r *: x \in A. + End absolutely_convex. -Lemma absolutely_convex_setX (K : numFieldType) (E F : lmodType K) +Lemma absolutely_convex_setX (K : numDomainType) (E F : lmodType K) (A : set E) (B : set F) : absolutely_convex_set A -> absolutely_convex_set B -> absolutely_convex_set (A `*` B). @@ -173,50 +132,45 @@ move=> [convA balA] [convB balB]; split. Qed. 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). Section addsetTheory. +Context {E : zmodType}. +Implicit Types A B C D : set E. -Lemma addsubset (E : zmodType) (A B C D: set E): - A `<=` B -> C `<=` D -> (A `+ C) `<=` (B `+ D). +Lemma addsetS A B C D : 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. +Lemma add0set A : [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). +Lemma addsetI A B (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)). + by move => [r Cr] [y [Ay By] <- {z}]; split => /=; exists r => //; + exists y. +move=> /= [[r ->] [y Ay] <- {z}] [x' ->] [y' By'] /(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. +move: By'; rewrite yy' {y' yy'} => By. +by exists x => //; exists y. Qed. -Lemma addsubsetA (E : zmodType) p c (D : set E) : - [set p + c] `+ D `<=` [set p] `+ ([set c] `+ D). +Lemma addsetA p c D : [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. +exists p => //; exists (c + z) => //. + by exists c => //; exists z. by rewrite addrA. Qed. End addsetTheory. - (* 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) := *) @@ -265,13 +219,12 @@ Lemma sum_continuous (I : Type) (r : seq I) (P : pred I) (f : I -> E -> F) : continuous (fun x1 : E => \sum_(i <- r | P i) f i x1). Proof. by move=> FC0; apply: continuous_big => //; apply: add_continuous. Qed. -Lemma continuous_shift (x y: F) : - {for x, continuous (+%R^~ y)}. +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. +have -> : +%R^~ y = (fun z => z.1 + z.2) \o (fun z => (z, y)) by exact: funext. apply: continuous_comp. -by apply: cvg_pair => //=; exact: cvg_cst. -exact: (@add_continuous _ (x,y)). + by apply: cvg_pair => //=; exact: cvg_cst. +exact: (@add_continuous _ (x, y)). Qed. End TopologicalNmodule_theory. @@ -287,7 +240,7 @@ HB.structure Definition TopologicalZmodule := & TopologicalNmodule_isTopologicalZmodule M}. Section TopologicalZmoduleTheory. -Variables (M : topologicalZmodType) (E : topologicalType). +Variables (M : topologicalZmodType). Lemma sub_continuous : continuous (fun x : M * M => x.1 - x.2). Proof. @@ -302,20 +255,19 @@ 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. - -Lemma addx_nbhs x (b : set M): nbhs 0 b <-> nbhs x ([set x] `+ b). +Lemma nbhs_add1set x (A : set M) : nbhs 0 A <-> nbhs x ([set x] `+ A). Proof. -split. +split=> [|nx]. rewrite -(subrr x) => /continuous_shift. - suff -> : [set x] `+ b = +%R^~ (- x) @^-1` b by []. - apply: funext => z /=; apply: propext; split. + suff -> : [set x] `+ A = +%R^~ (- x) @^-1` A by []. + apply: funext => z /=; apply: propext; split => [|Azx]. by move=> [? -> [y By] <-]; rewrite addrAC subrr add0r. - by move=> byx; exists x => //; exists (z - x) => //; rewrite addrCA subrr addr0. -move=> nx. -suff -> : b = +%R^~ (x) @^-1` ([set x] `+ b ) by apply: continuous_shift; rewrite add0r. -apply: funext => z /=; apply: propext; split. - by move=> bz; exists x => //; exists z => //; rewrite addrC. -by move=> [? -> [y By]]; rewrite addrC => /addIr <-. + by exists x => //; exists (z - x) => //; rewrite addrCA subrr addr0. +suff -> : A = +%R^~ (x) @^-1` ([set x] `+ A). + by apply: continuous_shift; rewrite add0r. +apply: funext => z /=; apply: propext; split=> [Az|[_ -> [y By]]]. + by exists x => //; exists z => //; rewrite addrC. +by rewrite addrC => /addIr <-. Qed. End TopologicalZmoduleTheory. @@ -372,7 +324,7 @@ HB.structure Definition TopologicalLmodule (K : numDomainType) := & TopologicalZmodule_isTopologicalLmodule K M}. Section TopologicalLmodule_theory. -Variables (R : numFieldType) (E : topologicalType) (F G: 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 : @@ -387,26 +339,28 @@ 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 continuousfor0_continuous (f : {linear F -> G}) : - {for 0, continuous f} -> continuous f. + {for 0, continuous f} -> continuous f. Proof. move=> cont0 x. 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 /=. - pose B := [set z | exists2 y : G, A y & z = y - f x]. + pose B := [set y - f x | y in A]. have /fxfy : nbhs 0 B. - have -> : B = (+%R^~ (-( - (f x)))) @^-1` A. + 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. + by move=> y [/= g Ag <-]; rewrite subrK. + move=> g/= Agfx; eexists; first exact: Agfx. + by rewrite addrK. + have:= @continuous_shift _ (0 : G) (f x) A. + by rewrite opprK add0r => /(_ nA); exact. 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. + by move=> [y Ay]; rewrite linearB => /subIr <-. +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); exact: cont0. +by move => A nA /=; apply: continuous_shift; rewrite subrr. Qed. End TopologicalLmodule_theory. @@ -496,7 +450,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. @@ -513,8 +467,6 @@ 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) := @@ -578,11 +530,12 @@ HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) Section SubLmodule_isSubConvexTvs. Context (R : numFieldType) (V : convexTvsType R) (S : pred V) (U : subLmodType S). -Definition init_subctvs := (sub_initial_topology U). -HB.instance Definition _ := Uniform.on init_subctvs. -HB.instance Definition _ := GRing.Lmodule.on init_subctvs. +Definition init_subconvextvs := sub_initial_topology U. +HB.instance Definition _ := Uniform.on init_subconvextvs. +HB.instance Definition _ := GRing.Lmodule.on init_subconvextvs. -Let add_sub: continuous (fun x : init_subctvs * init_subctvs => x.1 + x.2). +Let add_sub : continuous + (fun x : init_subconvextvs * init_subconvextvs => x.1 + x.2). Proof. apply: continuous_comp_initial => -[/= x y]. pose h := fun xy : U * U => (\val xy.1, \val xy.2). @@ -591,28 +544,25 @@ rewrite (_ : _ \o _ = g \o h). by apply/funext => i /=; rewrite GRing.valD. apply: continuous_comp; last exact: add_continuous. apply: cvg_pair => //=. -- apply: (cvg_comp _ _ cvg_fst). - exact: (continuous_valE (x : init_subctvs)). -- apply: (cvg_comp _ _ cvg_snd). - exact: (continuous_valE (y : init_subctvs)). +- exact/(cvg_comp _ _ cvg_fst)/continuous_valE. +- exact/(cvg_comp _ _ cvg_snd)/continuous_valE. Qed. HB.instance Definition _ := - @PreTopologicalNmodule_isTopologicalNmodule.Build init_subctvs add_sub. + @PreTopologicalNmodule_isTopologicalNmodule.Build init_subconvextvs add_sub. -Let opp_sub : continuous (-%R : init_subctvs -> init_subctvs). +Let opp_sub : continuous (-%R : init_subconvextvs -> init_subconvextvs). Proof. apply: continuous_comp_initial => x. rewrite (_ : _ \o _ = -%R \o \val). by apply/funext=> i /=; rewrite GRing.valN. -apply: continuous_comp; first exact: continuous_valE. -exact: opp_continuous. +by apply: continuous_comp; [exact: continuous_valE|exact: opp_continuous]. Qed. HB.instance Definition _ := - TopologicalNmodule_isTopologicalZmodule.Build init_subctvs opp_sub. + TopologicalNmodule_isTopologicalZmodule.Build init_subconvextvs opp_sub. -Let scale_sub : continuous (fun z : R^o * init_subctvs => z.1 *: z.2). +Let scale_sub : continuous (fun z : R^o * init_subconvextvs => z.1 *: z.2). Proof. apply: continuous_comp_initial => - [] /= x /= y. pose h := fun xy : R * U => (xy.1, \val xy.2). @@ -620,7 +570,7 @@ pose g := fun xy : R * V => xy.1 *: xy.2. rewrite (_ : _ \o _ = g \o h); first by apply/funext=> i /=; rewrite GRing.valZ. apply: continuous_comp; last exact: scale_continuous. move=> /= A [/= [/= B C]] [[r/= r0 xrB]]. -move/(continuous_valE (y : init_subctvs)) => [/= C' [woC' C'y C'C] BCA]. +move/(continuous_valE (y : init_subconvextvs)) => [/= C' [woC' C'y C'C] BCA]. apply: filterS; first exact: BCA. exists (ball x r, C') => /=. by split; [exact: nbhsx_ballx|exists C'; split]. @@ -628,36 +578,36 @@ by move=> su/= [xru C'u]; split; [exact: xrB|exact: C'C]. Qed. HB.instance Definition _ := - TopologicalZmodule_isTopologicalLmodule.Build R init_subctvs scale_sub. + TopologicalZmodule_isTopologicalLmodule.Build R init_subconvextvs scale_sub. Local Open Scope convex_scope. -Let locally_convex_sub : exists2 B : set_system init_subctvs, +Let locally_convex_sub : exists2 B : set_system init_subconvextvs, (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B. Proof. have [B absconvB [B0 nbhsb]] := @locally_convex R V. rewrite /filter_from /= in nbhsb. -exists [set a | exists2 b, B b & \val @^-1` b = a]. +exists [set \val @^-1` b | b in B]. 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=> /= r r1 x /= [rx] ? <-; apply: balb => /=; first exact: r1. + by exists (\val rx); rewrite ?GRing.valZ. split. move=> ? /= [b /B0] + <-. - by rewrite -[X in nbhs X _ -> _](linear0 (\val : U -> V)); exact: initial_nbhs. + rewrite -[X in nbhs X _ -> _](linear0 (\val : U -> V)). + exact: initial_nbhs_preimage. move=> /= A [a' [/= [/= b ob <-] /= b0 ba]]. have /nbhsb [b' Bb 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 exists b'. +by exists (val @^-1` b') => /=; [exists b'|move => x /= /bb' /ba]. Qed. Local Close Scope convex_scope. HB.instance Definition _ := - @Uniform_isConvexTvs.Build R init_subctvs locally_convex_sub. -HB.instance Definition _ := GRing.SubLmodule.on init_subctvs. + @Uniform_isConvexTvs.Build R init_subconvextvs locally_convex_sub. +HB.instance Definition _ := GRing.SubLmodule.on init_subconvextvs. End SubLmodule_isSubConvexTvs. @@ -793,72 +743,74 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E entourage_inv entourage_split_ex nbhsE. -HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build E add_continuous. +HB.instance Definition _ := + PreTopologicalNmodule_isTopologicalNmodule.Build E add_continuous. -HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R E scale_continuous. +HB.instance Definition _ := + TopologicalNmodule_isTopologicalLmodule.Build R E scale_continuous. HB.instance Definition _ := Uniform_isConvexTvs.Build R E locally_convex. HB.end. - -HB.factory Record Nbhsbasisat0_isConvexTvs (R: numFieldType) E & GRing.Lmodule 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 ; +HB.factory Record NbhsBasisAt0_isConvexTvs (R : numFieldType) E + & GRing.Lmodule R E := { + nbhsbasis_at0 : set_system E ; + nonempty_nbhsbasisat0 : nbhsbasis_at0 !=set0 ; 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 }. + absorbing_nbhsbasisat0 : nbhsbasis_at0 `<=` @pabsorbing_set _ E ; + absconvex_nbhsbasisat0 : nbhsbasis_at0 `<=` @absolutely_convex_set _ E ; + expand_nbhsbasisat0 : forall B r, nbhsbasis_at0 B -> + exists2 U, nbhsbasis_at0 U & ( *:%R r) @` U `<=` B (* implies circled *) ; + (* *) + nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V -> + exists2 W, nbhsbasis_at0 W & W `<=` U `&` V + (* *) }. -Definition nbhs_frombasis0 (R : numFieldType) (E : zmodType) +Definition filter_from_basis0 (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. -HB.builders Context R E & Nbhsbasisat0_isConvexTvs R E. +HB.builders Context R E & NbhsBasisAt0_isConvexTvs R E. -Let nbhs_fromfilter0 := @nbhs_frombasis0 R E (nbhsbasis_at0). +Let nbhs_fromfilter0 := @filter_from_basis0 R E (nbhsbasis_at0). -Lemma split_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> - exists2 C, nbhsbasis_at0 C & C `+ C `<=` B. +#[local] 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]. +move => B /(@expand_nbhsbasisat0 _ 2)[U fU UB]. exists U => //. -move => /= x [u] Uu [v] Uv <-. +move=> /= x [u Uu] [v Uv] <-. apply: UB. -exists (2^-1 *: (u+v)); last by by rewrite scalerA mulfV // scale1r. +exists (2^-1 *: (u + v)); last 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 /=. -suff -> : (2^-1).~ = 2^-1 :> R by []. (* should be a lemma in convex *) -apply: (@mulIf _ 2%:R); rewrite /((_).~) //. -by rewrite mulrBl mulVf // mul1r // addrK. +have := convU u v r. +rewrite !inE => /(_ Uu Uv); rewrite /conv/=. +suff -> : (2^-1).~ = 2^-1 :> R by []. +by rewrite /onem [X in X - _](splitr 1) div1r addrK. Qed. -#[local] Lemma nbhs_filter : forall p : E, ProperFilter (nbhs_fromfilter0 p). +#[local] Lemma nbhs_filter (p : E) : ProperFilter (nbhs_fromfilter0 p). Proof. -rewrite /nbhs_fromfilter0 => p. apply: filter_from_proper. apply: filter_from_filter => /=. - have [U fU] := nonempty_nbhsbasisat0. - by exists ([set p] `+ U) => //=; exists U. + have [U fU] := nonempty_nbhsbasisat0. + by exists ([set p] `+ U) => //=; exists U. move=> _ _ /= [U0 FU <-] [V0 FV <-]. have [W FW WUV] := nbhsbasis_at0I FU FV. exists ([set p] `+ W); first by exists W. - rewrite -addsetI; exact: addsubset. + by rewrite -addsetI; exact: addsetS. move=> _ /= [V FV] <-. -by exists p; exists p => //; exists 0; rewrite ?addr0//; exact: mem0_nbhsbasisat0. +by exists p, 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 (p : E) (A : set E) : nbhs_fromfilter0 p A -> A p. Proof. -move=> p A [_/= [C f0C <-]]; apply; exists p => //; exists 0; rewrite ?addr0//. +move=> [_/= [C f0C <-]]; apply; exists p => //; exists 0; rewrite ?addr0//. exact: mem0_nbhsbasisat0. Qed. @@ -872,15 +824,15 @@ 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))); first by exact: addsubsetA. -apply: addsubset => //; apply: subset_trans DDC; apply: addsubset => //. +apply: (@subset_trans _ ([set p] `+ ([set c] `+ D))); first by exact: addsetA. +apply: addsetS => //; apply: subset_trans DDC; apply: addsetS => //. 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 _ := @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. @@ -893,7 +845,7 @@ 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 =>//. +apply: WV =>/=; exists y1 => //; exists y2 => //. by rewrite addrACA. Qed. @@ -901,46 +853,47 @@ Qed. 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 [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 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 [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. + by rewrite (le_trans (ltW z1s)) // /minr; case: real_ltP => //; + 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]] := absorbing_nbhsbasisat0 fV'' 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 [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). -rewrite inE => xV''. -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 //. +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)//. + 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: 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. @@ -950,13 +903,13 @@ 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. + 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 //. + 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. +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. @@ -966,162 +919,165 @@ 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. -split; first by move=> /= A nA; exists A => //; exists A => //; rewrite addset0. -move => b [a] /= [a'] fa; rewrite addset0 => <- ab /=. +exists nbhsbasis_at0. + by move=> b; rewrite inE; apply: absconvex_nbhsbasisat0. +split; first by move=> /= A nA; exists A => //; exists A => //; rewrite add0set. +move => b [a] /= [a'] fa; rewrite add0set => <- ab /=. by exists a' => //=; split => //; exact: mem0_nbhsbasisat0. Qed. -HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R E add_continuous scale_continuous locally_convex. +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 := { - 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) +HB.factory Record NbhsSubbasisAt0_isConvexTvs (R : numFieldType) E + & GRing.Lmodule R E := { + nbhssubbasis_at0 : set_system E ; + nonempty_nbhssubbasisat0 : nbhssubbasis_at0 !=set0 ; + mem0_nbhssubbasisat0 : forall B, nbhssubbasis_at0 B -> B 0 ; + absorbing_nbhssubbasisat0 : nbhssubbasis_at0 `<=` @pabsorbing_set _ E ; + absconvex_nbhssubbasisat0 : nbhssubbasis_at0 `<=` @absolutely_convex_set _ E ; + expand_nbhssubbasisat0 : forall B r, nbhssubbasis_at0 B -> + exists2 U, nbhssubbasis_at0 U & ( *:%R r) @` U `<=` B (* implies circled *) }. + +Definition finI_fromsubbasis0 (R : numFieldType) (E : zmodType) (nbhssubbasis0 : set_system E) := finI_from nbhssubbasis0 id. -HB.builders Context R E & Nbhssubbasis0_isConvexTvs R E. +HB.builders Context R E & NbhsSubbasisAt0_isConvexTvs R E. From mathcomp Require Import finmap. -Let nbhsbasis_at0 := @nbhs_fromsubbasis0 R E nbhssubbasis0. +Let nbhsbasis_at0 := @finI_fromsubbasis0 R E nbhssubbasis_at0. -#[local] Lemma nonempty_nbhsbasisat0 : exists U, nbhsbasis_at0 U. +#[local] Lemma nonempty_nbhsbasisat0 : nbhsbasis_at0 !=set0. Proof. have [U fU] := nonempty_nbhssubbasisat0; exists U. -rewrite /nbhsbasis_at0 /nbhs_fromsubbasis0 /finI_from /=. +rewrite /nbhsbasis_at0 /finI_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 ->. +by rewrite bigcap_fset big_seq_fset1. Qed. -#[local] Lemma nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V -> - exists2 W, nbhsbasis_at0 W & W `<=` U `&` V. +#[local] Lemma nbhsbasis_at0I 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. +move=> [/= I fI IV] [/=J fJ JU]. +exists (U `&` V) => //; exists (I `|` J)%fset. + move => /= W; rewrite inE => /orP [WI|WJ]; rewrite mem_set //=. + (* extremely hard to understand that asboolE is to be used here *) + by have := fI _ WI; rewrite asboolE. + by have := fJ _ WJ; rewrite asboolE. +by rewrite -IV -JU -bigcap_setU set_fsetU. Qed. -#[local] Lemma mem0_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> B 0. +#[local] Lemma mem0_nbhsbasisat0 B : nbhsbasis_at0 B -> B 0. Proof. -by move => B [/= I fI <-] U /= /fI /=; rewrite asboolE /= => /mem0_nbhssubbasisat0. +by move=> [/= 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. +#[local] Lemma expand_nbhsbasisat0 B r : nbhsbasis_at0 B -> + exists2 U, nbhsbasis_at0 U & ( *:%R 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]. +move=> [/= I fI BI]. (* Change to a type I'*) +have H i : (i \in I) -> exists2 V, nbhssubbasis_at0 V & ( *:%R r) @` V `<=` i. + move=> /(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). +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 -> nbhssubbasis_at0 (f i). by rewrite /f; case: eqP => // h _; case: cid2. -have Hr i : i \in I -> r `*: (f i) `<=` i. +have Hr i : i \in I -> ( *:%R 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 move => _ /imfsetP[/= b bi ->]; exact/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. +by exists y => //; exact: Uy. Qed. -#[local] Lemma absorbing_nbhsbasisat0 : forall B , nbhsbasis_at0 B -> pabsorbing_set B. +#[local] Lemma absorbing_nbhsbasisat0 : nbhsbasis_at0 `<=` @pabsorbing_set _ E. 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]. +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???*) +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 *) +exists r0%:num => //. rewrite -BI asboolE /= => i /= iI. -have ni : nbhssubbasis0 i by apply/set_mem/fI. -have [_ bali] := (absconvex_nbhssubbasisat0 ni). +have ni : nbhssubbasis_at0 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 //. + exact: ge_bigmin_seq. +exists ((f i)%:num *: x); first exact/set_mem/Hr. +by rewrite scalerA mulfVK. Qed. -#[local] Lemma absconvex_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> absolutely_convex_set B. +#[local] Lemma absconvex_nbhsbasisat0 : + nbhsbasis_at0 `<=` @absolutely_convex_set _ E. 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. - by apply: yb => /=. + move=> /(_ x y r); rewrite !asboolE; apply; first exact: xb. + exact: 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. +have /fI := iI; rewrite asboolE => /absconvex_nbhssubbasisat0[_ +]. +by move=> /(_ r r1 (r *: y)); apply => /=; exists y => //; exact: 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 mem0_nbhsbasisat0 absorbing_nbhsbasisat0 + absconvex_nbhsbasisat0 expand_nbhsbasisat0 nbhsbasis_at0I. HB.end. - Section ConvexTvs_numDomain. Context (R : numDomainType) (E : convexTvsType R). -Lemma nbhs0N (U : set E) : nbhs 0 U -> nbhs 0 (-%R @` U). +Lemma nbhs0N (U : set E) : nbhs 0 U -> nbhs 0 (-%R @` U). Proof. exact/nbhs0N_subproof/scale_continuous. Qed. -Lemma nbhsD0 (U : set E) (x :E) : nbhs 0 U -> nbhs x (+%R x @` U). +Lemma nbhsD0 (U : set E) (x : E) : nbhs 0 U -> nbhs x (+%R x @` U). Proof. exact/nbhsD_subproof/add_continuous. Qed. -Lemma nbhsD (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U). +Lemma nbhsD (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U). Proof. exact/nbhsB_subproof/add_continuous. Qed. -Lemma openD (V : set E) (x : E) : open V -> open ((+%R x @` V)). +Lemma openD (V : set E) (x : E) : open V -> open (+%R x @` V). Proof. rewrite openE /= => openV z /= [y uy <-]; rewrite /interior /=. by apply: nbhsD; rewrite nbhsE /=; exists V => //; split => //; rewrite openE. Qed. -Lemma openB (U : set E) (x : E) : open ((+%R x @` U)) -> open U. +Lemma openB (U : set E) (x : E) : open (+%R x @` U) -> open U. Proof. -suff : U = ((+%R (-x) @` (+%R x @` U))) by move => + H; move => ->; apply: openD. +suff : U = ((+%R (-x) @` (+%R x @` U))). + by move => + H => ->; exact: openD. apply/seteqP; split => z /=. move=> Uz; exists (z + x); first by exists z => //; rewrite addrC. by rewrite -addrCA [X in (_ + X = _)]addrC subrr addr0. by move=> [y [y' Uy' <-] <-]; rewrite addrCA addrA subrr add0r. Qed. -Lemma nbhsE0 (x : E) (b : set E): nbhs x b <-> b x /\ exists2 a, nbhs 0 a & ([set x + x0 | x0 in a]) `<=` b. +Lemma nbhsE0 (x : E) (b : set E): nbhs x b <-> b x /\ + exists2 a, nbhs 0 a & [set x + x0 | x0 in a] `<=` b. Proof. split. - move => /[dup] /(nbhsD (-x)); rewrite addNr => nb0 nb; split; first by apply: nbhs_singleton. + move => /[dup] /(nbhsD (-x)); rewrite addNr => nb0 nb; split. + exact: nbhs_singleton. exists [set - x + x0 | x0 in b] => // z /=. by move=> [y /= [y' by']] <- <-; rewrite addrA addrN add0r. -move=> [bx [a n0a xab]]; apply: filterS; first by exact: xab. -by apply: nbhsD0. +move=> [bx [a n0a xab]]; apply: filterS; first exact: xab. +exact: nbhsD0. Qed. End ConvexTvs_numDomain. @@ -1137,7 +1093,7 @@ near=> x => //=; exists (r^-1 *: x); last by rewrite scalerA divff// scale1r. by apply: (BU (r^-1, x)); split => //=;[exact: nbhs_singleton|near: x]. Unshelve. all: by end_near. Qed. -Lemma nbhsZ (R : numFieldType) (E : convexTvsType R) (U : set E) (r : R) (x :E) : +Lemma nbhsZ (R : numFieldType) (E : convexTvsType R) (U : set E) (r : R) (x :E) : r != 0 -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U ). Proof. move=> r0 U0; have /= := scale_continuous ((r^-1, r *: x)) U. @@ -1149,40 +1105,38 @@ Unshelve. all: by end_near. Qed. Lemma openZ (R : numFieldType) (E : convexTvsType R) (U : set E) (r : R) : r != 0 -> open U -> open ( *:%R r @` U ). Proof. -move=> r0; rewrite openE /interior /= => openU z /= [x Ux <-]; apply: nbhsZ => //. +move=> r0; rewrite openE /interior /= => openU z /= [x Ux <-]. +apply: nbhsZ => //. by rewrite nbhsE => /=; exists U => //; split; rewrite // openE. Qed. End ConvexTvs_numField. - Section ConvexTvs_realType. (*better naming ?*) Lemma scalerx_continuous (R : realType) (E : convexTvsType R) (x : E) (s : R) : - {for s, continuous (fun t : R^o => t *: x)}. + {for s, continuous (fun t : R^o => t *: x)}. Proof. -have -> : (fun t : R^o => t *: x) = (fun z => z.1 *: z.2) \o (fun r => (r,x)) by apply: funext. +have -> : (fun t : R^o => t *: x) = (fun z => z.1 *: z.2) \o (fun r => (r,x)). + exact: funext. apply: continuous_comp. -apply: (@cvg_pair _ R^o _ _ (nbhs (s : R^o))) => //=; first by exact: cvg_cst. -by exact: (scale_continuous (s : R^o,x)). +apply: (@cvg_pair _ _ _ _ (nbhs s)) => //=; first exact: cvg_cst. +exact: (scale_continuous (s, x)). Qed. -(* why is cvg_cst defined only on realtypes ? *) - Lemma scalexr_continuous (R : realType) (E : convexTvsType R) (x : E) (s : R) : {for x, continuous (fun y : E => s *: y)}. Proof. -have -> : (fun y: E => s *: y ) = (fun z => z.1 *: z.2) \o (fun y => (s, y)). - by apply: funext. +have -> : (fun y : E => s *: y) = (fun z => z.1 *: z.2) \o (fun y => (s, y)). + exact: funext. apply: continuous_comp. -apply: (@cvg_pair _ R^o _ _ (nbhs (s : R^o))) => //=; first by exact: cvg_cst. -by exact: (scale_continuous (s: R^o, x)). +apply: (@cvg_pair _ _ _ _ (nbhs s)) => //=; first exact: cvg_cst. +exact: (scale_continuous (s, x)). Qed. End ConvexTvs_realType. - Section standard_topology. Variable R : numFieldType. @@ -1473,23 +1427,24 @@ Proof. move => *; exact: linearP. Qed. End lcfunproperties. Section openbasis. -Context (R : realType) (E: convexTvsType R). +Context (R : realType) (E : convexTvsType R). -Definition nbhsbasis_ctvs := sval (cid2 (@locally_convex _ E)). +Definition nbhsbasis_convextvs := sval (cid2 (@locally_convex _ E)). -Definition open_nbhsbasis_ctvs := [set b| exists2 b', nbhsbasis_ctvs b' & b = interior b']. +Definition open_nbhsbasis_convextvs := [set interior b | b in nbhsbasis_convextvs]. (* TODO : convex is enough and then take balanced closure *) Lemma has_open_nbhs_basis : - nbhs_basis 0 open_nbhsbasis_ctvs /\ ( forall b, open_nbhsbasis_ctvs b -> (open b /\ absolutely_convex_set b)). + nbhs_basis 0 open_nbhsbasis_convextvs /\ + (forall b, open_nbhsbasis_convextvs b -> open b /\ absolutely_convex_set b). Proof. -have [absconv [] nbhs0 basis] := (svalP (cid2 (@locally_convex _ E))). +have [absconv [] nbhs0 basis] := svalP (cid2 (@locally_convex _ E)). split. - split; move=> a /=; first by move => [b /nbhs0 nbhsb ->]; apply: nbhs_interior. - move=> /basis /= [b /= nbhsb ba]; exists (interior b); first by exists b => //. - apply: subset_trans; last by exact: ba. + split; move=> a /=; first by move=> [b /nbhs0] nbhsb <-; exact: nbhs_interior. + move=> /basis /= [b /= nbhsb ba]; exists (interior b); first by exists b. + apply: subset_trans; last exact: ba. exact: interior_subset. -move=> ? /= [b nb ->]; split; first by exact: open_interior. +move=> ? /= [b nb <-]; split; first exact: open_interior. have [convb balb] := absconv b (mem_set nb). split; rewrite /interior. move => x y t; rewrite !inE. @@ -1512,7 +1467,7 @@ move=> t0 t1 ? /= [x] /= + <-; move/nbhsE0 => [bx [a na0 ab]]. apply/nbhsE0; split. apply: balb; first by exact: t1. by exists x. -exists (t `*: a). +exists (( *:%R t) @` a). by rewrite -(@scaler0 _ _ t); apply: nbhsZ => // ? /= [y ay] <-; apply: ab; exists y. move => z /= [?] [y] ax <- <-; rewrite -scalerDr; apply: balb; first by exact: t1. by exists (x + y)=> //; apply: ab; exists y. @@ -1527,15 +1482,15 @@ Proof. by move=> /(_ [set: E]) /(_ filterT) [b ? _]; exists b. Qed. -Lemma absorbing_opennbhsbasis : forall b, open_nbhsbasis_ctvs b -> pabsorbing_set b. +Lemma absorbing_opennbhsbasis b : open_nbhsbasis_convextvs b -> pabsorbing_set b. Proof. -move=> b Bb x. -have [/(_ b Bb) n0b _] := (basis_opennbhsbasis ). +move=> Bb x. +have [/(_ b Bb) n0b _] := basis_opennbhsbasis. move: n0b; rewrite -(scale0r x) => n0b. have := scalerx_continuous => /(_ _ _ x 0 b n0b) [r] /= r0 b0rb. -exists (r/2); first by apply: divr_gt0. +exists (r / 2); first exact: divr_gt0. rewrite inE. -apply: b0rb; rewrite /ball_ /= sub0r normrN normrM !gtr0_norm //. +apply: b0rb; rewrite /ball_ /= sub0r normrN normrM !gtr0_norm//. by rewrite gtr_pMr // invf_lt1 // ltrDl. Qed. @@ -1616,7 +1571,8 @@ Qed. 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]. +have lem (w : V) : (exists2 r, (0 < r) & A (r *: w)) -> + has_inf [set t | 0 < t /\ w \in ( *:%R t) @` A]. move => [r r0 Aw]; split => /=; rewrite /set0P; last by exists 0 => z [z0 _]; rewrite ltW. exists r^-1 => //=; split=> //. rewrite ?invr_gt0 //. @@ -1714,17 +1670,6 @@ 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). @@ -1762,7 +1707,7 @@ 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). + forall B r, seminorm_subbasis B -> exists2 U, seminorm_subbasis U & ( ( *:%R 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. @@ -1845,7 +1790,9 @@ 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 H) seminorm_subbasis nonempty_subbasis mem0_seminorm_subbasis expand_seminorm_subbasis absorbing_seminorm absolutely_convex_seminorm_subbasis. +HB.instance Definition _ := @NbhsSubbasisAt0_isConvexTvs.Build R (seminorm_on H) + seminorm_subbasis nonempty_subbasis mem0_seminorm_subbasis absorbing_seminorm + absolutely_convex_seminorm_subbasis expand_seminorm_subbasis. (* NB: Using init-fam (see initial_topology.v) doesn't work as we strongly need a 0 basis. With init-fam we are considering nbhs a = [ [A : set E |, exists e , A = [x | |p(x) - p(a)| y /=; rewrite /ball /= sub0r normrN ger0_norm ?gauge_ge0 by rewrite gtr0_norm ?divr_gt0 // ler_pdivrMr // mul1r ltW. by exists y' => //; rewrite scalerA mulrC. move=> Ary. - have: exists2 t : R , (0 < t < 1) & (r^-1 *: y \in t `*: A). + have: exists2 t : R , (0 < t < 1) & (r^-1 *: y \in ( *:%R t) @` A). have /scalerx_continuous : nbhs (1 *: (r^-1 *: y)) A. by rewrite scale1r; apply: open_nbhs_nbhs; split => //. move => [s /= s0] b1s. @@ -1953,7 +1900,7 @@ apply/seteqP; split => y /=; rewrite /ball /= sub0r normrN ger0_norm ?gauge_ge0 - by rewrite gtr0_norm ?gtr_pMr ?invf_lt1 ?ltrDl //. by rewrite scalerA mulVf ?scale1r //. move=> [t /andP [t0 t1] rytb]. -have lepr: - (t*r) <= sup [set - x | x in [set r1 | 0 < r1 /\ y \in r1 `*: A]]. +have lepr: - (t*r) <= sup [set - x | x in [set r1 | 0 < r1 /\ y \in ( *:%R r1) @` A]]. set B := ( X in _ <= sup X). have Br : B (- (t * r)). exists (t * r); split => //; rewrite ?mulr_gt0 //. @@ -1971,10 +1918,10 @@ From mathcomp Require Import finmap. (* how to do without *) (* TODO : uniformise the usage of `+ or (+%R~ @) withine lemmas *) Theorem seminorm_convextvs : continuous (id : E -> seminormE) /\ (continuous (id : seminormE -> E)). Proof. -pose B := open_nbhsbasis_ctvs. +pose B := open_nbhsbasis_convextvs. split=> x a. move=> [/=b [?]] [I /= Ig] /= <- <- /filterS; apply. - apply/addx_nbhs. + apply/nbhs_add1set. apply: filter_bigI => /= i /Ig /set_mem /= => -[? [b' [nb']]] -> [/= r r0 ->]. have [/(_ b' nb') nbhsB _] := basis_opennbhsbasis E. set p := (X in nbhs 0 (X @^-1` ball 0 r)). @@ -2053,7 +2000,7 @@ case : (eqVneq (q x) 0). rewrite linearZ /= normrM normfV ltr_pdivrMl ?normr_gt0 ?lt0r_neq0 //. rewrite (gtr0_norm e0) => lem; apply : lt_trans. apply: lem. - have hasinf : has_inf [set r | 0 < r /\ x \in r `*: b]. + have hasinf : has_inf [set r | 0 < r /\ x \in ( *:%R r) @` b]. split; last by exists 0 => z /= [] z0 _; apply: ltW. have [r r0] := absorbing_opennbhsbasis Bb x. move/set_mem => bx. diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index 3e715715c1..f0055ec949 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -101,11 +101,10 @@ rewrite nbhs_filterE; apply: filterS FC. by apply: subset_trans sBfA; rewrite -fCeB; apply: preimage_image. Qed. -Lemma initial_nbhs (x : W) b : nbhs (f x) b -> nbhs x (f @^-1` b). +Lemma initial_nbhs_preimage (w : W) A : nbhs (f w) A -> nbhs w (f @^-1` A). Proof. -rewrite nbhsE /= => -[b' [b0 ob]] bb'. -exists (f @^-1` b'); split => //= ; first by exists b'. -by move => z /= /bb'. +rewrite nbhsE /= => -[B [oB Bfx]] BA. +by exists (f @^-1` B); split => //= ; [exists B|move=> z /= /BA]. Qed. End Initial_Topology. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 95f8addfe2..59b5ea7b73 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -499,8 +499,8 @@ 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]. +Definition open_from (T I : Type) (D : set I) (f : I -> set T) := + [set \bigcup_(i in D') f i | D' in subset^~ D]. (** Topology defined by a base of open sets *) From b2609bd17cc96211b760cd1ed006354fc44d7e73 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 8 Jul 2026 12:05:48 +0900 Subject: [PATCH 4/4] changlog, clean (wip) --- CHANGELOG_UNRELEASED.md | 20 +- theories/normedtype_theory/tvs.v | 521 +++++++++++++++++-------------- 2 files changed, 300 insertions(+), 241 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index db5c76462b..ba170edd86 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -251,7 +251,7 @@ + definition `balanced_set` + definition `absolutely_convex_set` + lemma `absolutely_convex0` - + definition `pabsorbing_set` + + definition `absorbing_set` + lemma `absolutely_convex_setX` + notation `... `+ ...` + lemmas `addsetS`, `add0set`, `addsetI`, `addsetA` @@ -270,6 +270,24 @@ + lemma `scalexr_continuous` + definition `nbhsbasis_convextvs` + definition `open_nbhsbasis_convextvs` + + definition `open_absconvex_opennbhsbasis` + + definition `basis_opennbhsbasis` + + lemma `basis_neqset0` + + lemma `absorbing_opennbhsbasis` + + definition `gauge_fun` + + definition `seminorm_on` + + definition `seminorm_subbasis` + + lemmas `nonempty_subbasis`, `mem0_seminorm_subbasis`, `split_seminorm_subbasis`, + `expand_seminorm_subbasis` + + lemmas `convex_seminorm_subbasis`, `balanced_seminorm_subbasis`, + `absolutely_convex_seminorm_subbasis`, `absorbing_seminorm`, `continuous_at0_seminorm`, + `continuous_seminorm` + + definitions `gauge_fun_basis`, `seminorm_of` + + theorem `seminorm_convextvs` + + lemma `continuous_seminorm_of` + + lemma `linear_continuous_seminorm` + + lemma `linear_seminorm_continuous` + + proposition `lcfun_seminorm` ### Changed diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index fed2c9bc63..51f682454a 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -6,7 +6,7 @@ From mathcomp Require Import interval_inference. From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import convex set_interval reals topology. -From mathcomp Require Import initial_topology num_normedtype. +From mathcomp Require Import initial_topology num_normedtype. From mathcomp Require Import pseudometric_normed_Zmodule. (**md**************************************************************************) @@ -52,6 +52,7 @@ From mathcomp Require Import pseudometric_normed_Zmodule. (* The HB class is SubConvexTvs. *) (* Instance: in particular, it is shown that a *) (* sub-Lmodule is a sub-convex TVS. *) +(* init_subconvextvs == TODO *) (* PreTopologicalLmod_isConvexTvs == factory allowing the construction of a *) (* convex tvs from an Lmodule which is also a *) (* topological space *) @@ -70,6 +71,10 @@ From mathcomp Require Import pseudometric_normed_Zmodule. (* lmodType to {linear_continuous E -> F | s}. *) (* lcfun_spec f == specification for membership of the linear *) (* continuous function f *) +(* gauge_fun == TODO *) +(* seminorm_on == TODO *) +(* seminorm_subbasis == TODO *) +(* gauge_fun_basis == TODO *) (* ``` *) (* HB instances: *) (* - The type R^o (R : numFieldType) is endowed with the structure of *) @@ -112,7 +117,7 @@ move => [] x Ax [] _ /(_ 0); rewrite normr0 ler01 // => /(_ isT) /(_ 0); apply. by exists x; rewrite //= scale0r. Qed. -Definition pabsorbing_set (A : set V) := +Definition absorbing_set (A : set V) := forall x : V, exists2 r, 0 < r & r *: x \in A. End absolutely_convex. @@ -263,7 +268,7 @@ split=> [|nx]. apply: funext => z /=; apply: propext; split => [|Azx]. by move=> [? -> [y By] <-]; rewrite addrAC subrr add0r. by exists x => //; exists (z - x) => //; rewrite addrCA subrr addr0. -suff -> : A = +%R^~ (x) @^-1` ([set x] `+ A). +suff -> : A = +%R^~ x @^-1` ([set x] `+ A). by apply: continuous_shift; rewrite add0r. apply: funext => z /=; apply: propext; split=> [Az|[_ -> [y By]]]. by exists x => //; exists z => //; rewrite addrC. @@ -313,6 +318,11 @@ HB.end. HB.structure Definition PreTopologicalLmodule (K : numDomainType) := {M of Topological M & GRing.Lmodule K M}. +(* +HB.instance Definition _ (K : numDomainType) (T : preTopologicalLmodType K) : PreTopologicalLmodule K T := + ConvexSpace.copy T (convex_lmodType T). +*) + HB.mixin Record TopologicalZmodule_isTopologicalLmodule (R : numDomainType) M & Topological M & GRing.Lmodule R M := { scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ; @@ -323,6 +333,9 @@ HB.structure Definition TopologicalLmodule (K : numDomainType) := {M of TopologicalZmodule M & GRing.Lmodule K M & TopologicalZmodule_isTopologicalLmodule K M}. +(*HB.instance Definition _ (K : numDomainType) (T : topologicalLmodType K) : TopologicalLmodule K T := + ConvexSpace.copy T (convex_lmodType T).*) + Section TopologicalLmodule_theory. Variables (R : numFieldType) (E : topologicalType) (F G : topologicalLmodType R). @@ -517,20 +530,37 @@ 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 }. +(* TODO : it should be enough to ask for convex_set only and show that absolutely_convex_set can be derived from it *) #[short(type="convexTvsType")] HB.structure Definition ConvexTvs (R : numDomainType) := {E of Uniform_isConvexTvs R E & Uniform E & TopologicalLmodule R E}. +(*HB.instance Definition _ (K : numDomainType) (T : convexTvsType K) : ConvexTvs K T := + ConvexSpace.copy T (convex_lmodType T).*) + +HB.mixin Record isSubConvexSpace (R : numDomainType) (V : convType R) + (S : pred V) U & SubChoice V S U & ConvexSpace R U := { + valconv : forall (t : {i01 R}) (a b : U), val (conv t a b) = conv t (val a) (val b) +}. + +#[short(type="subConvType")] +HB.structure Definition SubConvexSpace (R : numDomainType) (V : convType R) S := + { U of SubChoice V S U & ConvexSpace R U & isSubConvexSpace R V S U }. + #[short(type="subConvexTvsType")] HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) (S : pred V) := - { U of SubTopological V S U & ConvexTvs R U & @GRing.SubLmodule R V S U }. + { U of SubTopological V S U & ConvexTvs R U & @GRing.SubLmodule R V S U}. + +(*HB.instance Definition _ (K : numDomainType) (V : convType K) (S : pred V) (T : @subConvexTvsType K V S) : @SubConvexTvs K S T := + ConvexSpace.copy T (convex_lmodType T).*) Section SubLmodule_isSubConvexTvs. Context (R : numFieldType) (V : convexTvsType R) (S : pred V) (U : subLmodType S). Definition init_subconvextvs := sub_initial_topology U. + HB.instance Definition _ := Uniform.on init_subconvextvs. HB.instance Definition _ := GRing.Lmodule.on init_subconvextvs. @@ -756,11 +786,11 @@ HB.end. HB.factory Record NbhsBasisAt0_isConvexTvs (R : numFieldType) E & GRing.Lmodule R E := { nbhsbasis_at0 : set_system E ; - nonempty_nbhsbasisat0 : nbhsbasis_at0 !=set0 ; - mem0_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> B 0 ; - absorbing_nbhsbasisat0 : nbhsbasis_at0 `<=` @pabsorbing_set _ E ; - absconvex_nbhsbasisat0 : nbhsbasis_at0 `<=` @absolutely_convex_set _ E ; - expand_nbhsbasisat0 : forall B r, nbhsbasis_at0 B -> + nonempty_nbhsbasis_at0 : nbhsbasis_at0 !=set0 ; + mem0_nbhsbasis_at0 : forall B, nbhsbasis_at0 B -> B 0 ; + absorbing_nbhsbasis_at0 : nbhsbasis_at0 `<=` @absorbing_set _ E ; + absconvex_nbhsbasis_at0 : nbhsbasis_at0 `<=` @absolutely_convex_set _ E ; + expand_nbhsbasis_at0 : forall B r, nbhsbasis_at0 B -> exists2 U, nbhsbasis_at0 U & ( *:%R r) @` U `<=` B (* implies circled *) ; (* *) nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V -> @@ -775,18 +805,18 @@ HB.builders Context R E & NbhsBasisAt0_isConvexTvs R E. Let nbhs_fromfilter0 := @filter_from_basis0 R E (nbhsbasis_at0). -#[local] Lemma split_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> +#[local] Lemma split_nbhsbasis_at0 B : nbhsbasis_at0 B -> exists2 C, nbhsbasis_at0 C & C `+ C `<=` B. Proof. -move => B /(@expand_nbhsbasisat0 _ 2)[U fU UB]. +move=> /(@expand_nbhsbasis_at0 _ 2)[U fU UB]. exists U => //. move=> /= x [u Uu] [v Uv] <-. apply: UB. exists (2^-1 *: (u + v)); last 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 [convU _] := absconvex_nbhsbasis_at0 fU. +have H : 0 <= 2^-1 :> R by []. +have G : 2^-1 <= 1 :> R by rewrite invf_le1 ?lerDl. pose r := Itv01 H G. have := convU u v r. rewrite !inE => /(_ Uu Uv); rewrite /conv/=. @@ -798,20 +828,20 @@ Qed. Proof. apply: filter_from_proper. apply: filter_from_filter => /=. - have [U fU] := nonempty_nbhsbasisat0. + have [U fU] := nonempty_nbhsbasis_at0. by exists ([set p] `+ U) => //=; exists U. move=> _ _ /= [U0 FU <-] [V0 FV <-]. have [W FW WUV] := nbhsbasis_at0I FU FV. exists ([set p] `+ W); first by exists W. by rewrite -addsetI; exact: addsetS. move=> _ /= [V FV] <-. -by exists p, p => //; exists 0; rewrite ?addr0//; exact: mem0_nbhsbasisat0. +by exists p, p => //; exists 0; rewrite ?addr0//; exact: mem0_nbhsbasis_at0. Qed. #[local] Lemma nbhs_singleton (p : E) (A : set E) : nbhs_fromfilter0 p A -> A p. Proof. move=> [_/= [C f0C <-]]; apply; exists p => //; exists 0; rewrite ?addr0//. -exact: mem0_nbhsbasisat0. +exact: mem0_nbhsbasis_at0. Qed. #[local] Lemma nbhs_nbhs (p : E) (A : set E) : nbhs_fromfilter0 p A -> @@ -819,7 +849,7 @@ Qed. Proof. rewrite /nbhs_fromfilter0/=. move=> [B/= [C f0C <- pCA]] //=. -have [D f0D DDC] := split_nbhsbasisat0 f0C. +have [D f0D DDC] := split_nbhsbasis_at0 f0C. exists ([set p] `+ D); first by exists D. move=> _ [/= _] -> [c Cc <-] /=. exists ([set p + c] `+ D) => //; first by exists D. @@ -837,7 +867,7 @@ HB.instance Definition _ := #[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. +have [W filter0W WV] := split_nbhsbasis_at0 filterV0. exists ([set x1] `+ W, [set x2] `+ W) => /=. split => //=; first by exists ([set x1] `+ W) => //; exists W. exists ([set x2] `+ W) => //; exists W => //. @@ -853,10 +883,10 @@ Qed. 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 [V0 fV0 rV0] := split_nbhsbasis_at0 fV. + have [/= s [s0]] := absorbing_nbhsbasis_at0 fV0 x. rewrite inE => xV''. - have [convV'' balV''] := absconvex_nbhsbasisat0 fV0. + have [convV'' balV''] := absconvex_nbhsbasis_at0 fV0. exists ((ball_ normr 0 (minr 1 s)), [set x] `+ V0) => //=. split. exists (minr 1 s) => //=. rewrite /minr; case: ifPn => //. @@ -876,12 +906,12 @@ have [r0|] := eqVneq r 0. apply: (balV'' z1); last by exists y. by rewrite (le_trans (ltW z1s)) // /minr; case: real_ltP => //; 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]] := absorbing_nbhsbasisat0 fV'' x. +have [V0 fV0 rV0] := split_nbhsbasis_at0 fV. +have [V' fV' rV'] := split_nbhsbasis_at0 fV0. +have [V'' fV'' rV''] := expand_nbhsbasis_at0 r fV'. +have [/= s [s0]] := absorbing_nbhsbasis_at0 fV'' x. rewrite inE => xV''. -have [convV'' balV''] := absconvex_nbhsbasisat0 fV''. +have [convV'' balV''] := absconvex_nbhsbasis_at0 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|) => //=. @@ -894,7 +924,7 @@ 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. + apply: rV'; exists 0; first by apply: mem0_nbhsbasis_at0. exists (r *: t); first by apply: rV''; exists t. by rewrite add0r. exists (y *: x + y *: t); last by rewrite addrA. @@ -904,8 +934,8 @@ apply: rV''. 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. + 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. @@ -920,7 +950,7 @@ Qed. (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B. Proof. exists nbhsbasis_at0. - by move=> b; rewrite inE; apply: absconvex_nbhsbasisat0. + by move=> b; rewrite inE; apply: absconvex_nbhsbasis_at0. split; first by move=> /= A nA; exists A => //; exists A => //; rewrite add0set. move => b [a] /= [a'] fa; rewrite add0set => <- ab /=. by exists a' => //=; split => //; exact: mem0_nbhsbasisat0. @@ -934,11 +964,11 @@ HB.end. HB.factory Record NbhsSubbasisAt0_isConvexTvs (R : numFieldType) E & GRing.Lmodule R E := { nbhssubbasis_at0 : set_system E ; - nonempty_nbhssubbasisat0 : nbhssubbasis_at0 !=set0 ; - mem0_nbhssubbasisat0 : forall B, nbhssubbasis_at0 B -> B 0 ; - absorbing_nbhssubbasisat0 : nbhssubbasis_at0 `<=` @pabsorbing_set _ E ; - absconvex_nbhssubbasisat0 : nbhssubbasis_at0 `<=` @absolutely_convex_set _ E ; - expand_nbhssubbasisat0 : forall B r, nbhssubbasis_at0 B -> + nonempty_nbhssubbasis_at0 : nbhssubbasis_at0 !=set0 ; + mem0_nbhssubbasis_at0 : forall B, nbhssubbasis_at0 B -> B 0 ; + absorbing_nbhssubbasis_at0 : nbhssubbasis_at0 `<=` @absorbing_set _ E ; + absconvex_nbhssubbasis_at0 : nbhssubbasis_at0 `<=` @absolutely_convex_set _ E ; + expand_nbhssubbasis_at0 : forall B r, nbhssubbasis_at0 B -> exists2 U, nbhssubbasis_at0 U & ( *:%R r) @` U `<=` B (* implies circled *) }. Definition finI_fromsubbasis0 (R : numFieldType) (E : zmodType) @@ -953,7 +983,7 @@ Let nbhsbasis_at0 := @finI_fromsubbasis0 R E nbhssubbasis_at0. #[local] Lemma nonempty_nbhsbasisat0 : nbhsbasis_at0 !=set0. Proof. -have [U fU] := nonempty_nbhssubbasisat0; exists U. +have [U fU] := nonempty_nbhssubbasis_at0; exists U. rewrite /nbhsbasis_at0 /finI_fromsubbasis0 /finI_from /=. exists [fset U]%fset => /=. by move=> _ /fset1P ->; rewrite mem_set //=; exists U; rewrite ?addset0. @@ -972,17 +1002,17 @@ exists (U `&` V) => //; exists (I `|` J)%fset. by rewrite -IV -JU -bigcap_setU set_fsetU. Qed. -#[local] Lemma mem0_nbhsbasisat0 B : nbhsbasis_at0 B -> B 0. +#[local] Lemma mem0_nbhsbasis_at0 B : nbhsbasis_at0 B -> B 0. Proof. -by move=> [/= I fI <-] U /= /fI /=; rewrite asboolE /= => /mem0_nbhssubbasisat0. +by move=> [/= I fI <-] U /= /fI /=; rewrite asboolE /= => /mem0_nbhssubbasis_at0. Qed. -#[local] Lemma expand_nbhsbasisat0 B r : nbhsbasis_at0 B -> +#[local] Lemma expand_nbhsbasis_at0 B r : nbhsbasis_at0 B -> exists2 U, nbhsbasis_at0 U & ( *:%R r) @` U `<=` B. Proof. move=> [/= I fI BI]. (* Change to a type I'*) have H i : (i \in I) -> exists2 V, nbhssubbasis_at0 V & ( *:%R r) @` V `<=` i. - move=> /(fI i); rewrite asboolE => /(expand_nbhssubbasisat0 r) /= [V nV rVi]. + move=> /(fI i); rewrite asboolE => /(expand_nbhssubbasis_at0 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 -> nbhssubbasis_at0 (f i). @@ -998,11 +1028,11 @@ apply: Hr => //=. by exists y => //; exact: Uy. Qed. -#[local] Lemma absorbing_nbhsbasisat0 : nbhsbasis_at0 `<=` @pabsorbing_set _ E. +#[local] Lemma absorbing_nbhsbasis_at0 : nbhsbasis_at0 `<=` @absorbing_set _ E. 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]. + move => i /(fI i); rewrite asboolE => /absorbing_nbhssubbasis_at0/(_ 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]. @@ -1013,7 +1043,7 @@ pose r0 : {posnum R} := [elaborate \big[Order.min/1%:pos]_(i <- I) f i]. exists r0%:num => //. rewrite -BI asboolE /= => i /= iI. have ni : nbhssubbasis_at0 i by apply/set_mem/fI. -have [_ bali] := absconvex_nbhssubbasisat0 ni. +have [_ bali] := absconvex_nbhssubbasis_at0 ni. apply: (bali (r0%:num / (f i)%:num)). rewrite ger0_norm // ler_pdivrMr // mul1r /r0 num_le //. exact: ge_bigmin_seq. @@ -1021,27 +1051,27 @@ exists ((f i)%:num *: x); first exact/set_mem/Hr. by rewrite scalerA mulfVK. Qed. -#[local] Lemma absconvex_nbhsbasisat0 : +#[local] Lemma absconvex_nbhsbasis_at0 : nbhsbasis_at0 `<=` @absolutely_convex_set _ E. Proof. move=> B [/= I fI <-]; split. move=> x y r; rewrite !asboolE /= => xb yb => // i /= iI. - have /fI := iI; rewrite asboolE; move/absconvex_nbhssubbasisat0 => [+ _]. + have /fI := iI; rewrite asboolE; move=> /absconvex_nbhssubbasis_at0[+ _]. move=> /(_ x y r); rewrite !asboolE; apply; first exact: xb. exact: yb. move=> r r1 x /= [y] capy <- i /= iI. -have /fI := iI; rewrite asboolE => /absconvex_nbhssubbasisat0[_ +]. +have /fI := iI; rewrite asboolE => /absconvex_nbhssubbasis_at0[_ +]. by move=> /(_ r r1 (r *: y)); apply => /=; exists y => //; exact: capy. Qed. HB.instance Definition _ := @NbhsBasisAt0_isConvexTvs.Build R E - nbhsbasis_at0 nonempty_nbhsbasisat0 mem0_nbhsbasisat0 absorbing_nbhsbasisat0 - absconvex_nbhsbasisat0 expand_nbhsbasisat0 nbhsbasis_at0I. + nbhsbasis_at0 nonempty_nbhsbasisat0 mem0_nbhsbasis_at0 absorbing_nbhsbasis_at0 + absconvex_nbhsbasis_at0 expand_nbhsbasis_at0 nbhsbasis_at0I. HB.end. Section ConvexTvs_numDomain. -Context (R : numDomainType) (E : convexTvsType R). +Context {R : numDomainType} (E : convexTvsType R). Lemma nbhs0N (U : set E) : nbhs 0 U -> nbhs 0 (-%R @` U). Proof. exact/nbhs0N_subproof/scale_continuous. Qed. @@ -1166,8 +1196,8 @@ 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. rewrite inE/=. -rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |> - (x - y : convex_lmodType _)). +rewrite [X in `|X|](_ : _ = (x - z (*: convex_lmodType _*)) <| l |> + (x - y (*: convex_lmodType _*))). by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr. rewrite (le_lt_trans (ler_normD _ _))// !normrM. rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//. @@ -1426,14 +1456,28 @@ Proof. move => *; exact: linearP. Qed. End lcfunproperties. +Local Open Scope convex_scope. + +(* TODO *) +Lemma convD (R : numDomainType) (E : lmodType R) (t : {i01 R}) (x y z' : convex_lmodType E) : + x <| t |> y + z' = (x + z' : convex_lmodType _) <| t |> (y + z'). +Proof. +rewrite /conv/=. +rewrite !scalerDr -[in RHS]addrA. +rewrite [in X in (_ = _ + X)]addrCA [in X in (_ = _ + ( _ + X))]scalerBl. +by rewrite [in X in (_ = _ + ( _ + X))]addrCA addrN addr0 scale1r addrA. +Qed. + Section openbasis. Context (R : realType) (E : convexTvsType R). Definition nbhsbasis_convextvs := sval (cid2 (@locally_convex _ E)). -Definition open_nbhsbasis_convextvs := [set interior b | b in nbhsbasis_convextvs]. +Definition open_nbhsbasis_convextvs := + [set interior b | b in nbhsbasis_convextvs]. + +Local Open Scope convex_scope. -(* TODO : convex is enough and then take balanced closure *) Lemma has_open_nbhs_basis : nbhs_basis 0 open_nbhsbasis_convextvs /\ (forall b, open_nbhsbasis_convextvs b -> open b /\ absolutely_convex_set b). @@ -1446,30 +1490,25 @@ split. exact: interior_subset. move=> ? /= [b nb <-]; split; first exact: open_interior. have [convb balb] := absconv b (mem_set nb). -split; rewrite /interior. +split. move => x y t; rewrite !inE. move=> /nbhsE0 [bx [ax nax axb]] /nbhsE0 [by' [ay nay ayb]]; apply/nbhsE0; split. - by apply/set_mem/convb; rewrite !inE. + by apply/set_mem/convb; rewrite !inE. exists (ax `&` ay); first by apply: filterI. move=> z /= [z' [xz xz'] <-]. - (*have -> : conv t x y + z' = conv t (x + z') (y + z').*) (*souci avec conv t (x+x0) (y+y0)*) - rewrite /conv /=. - have ->: t%:num *: x + (t%:num).~ *: y + z' = t%:num *: (x + z') + (t%:num).~ *: (y + z'). - rewrite !scalerDr -[in RHS]addrA. - rewrite [in X in (_ = _ + X)]addrCA [in X in (_ = _ + ( _ + X))]scalerBl. - by rewrite [in X in (_ = _ + ( _ + X))]addrCA addrN addr0 scale1r addrA. + rewrite convD. apply/set_mem/convb; rewrite inE; first by apply: axb; exists z'. by apply: ayb; exists z'. move=> /= t. -case: (eqVneq t 0). (*disctinction overlooked in the literature*) - by move=> -> _ ? /= [?] _; rewrite scale0r => <-; apply: nbhs0 => /=; exact: nb. -move=> t0 t1 ? /= [x] /= + <-; move/nbhsE0 => [bx [a na0 ab]]. +have [->|t0] := eqVneq t 0. (*disctinction overlooked in the literature*) + by move=> _ ? /= [?] _; rewrite scale0r => <-; apply: nbhs0 => /=; exact: nb. +move=> t1 ? /= [x] /= + <-; move/nbhsE0 => [bx [a na0 ab]]. apply/nbhsE0; split. - apply: balb; first by exact: t1. + apply: balb; first exact: t1. by exists x. exists (( *:%R t) @` a). - by rewrite -(@scaler0 _ _ t); apply: nbhsZ => // ? /= [y ay] <-; apply: ab; exists y. -move => z /= [?] [y] ax <- <-; rewrite -scalerDr; apply: balb; first by exact: t1. + by rewrite -(@scaler0 _ _ t); apply: nbhsZ => // ? /= [y ay] <-. +move => z /= [?] [y] ax <- <-; rewrite -scalerDr; apply: balb; first exact: t1. by exists (x + y)=> //; apply: ab; exists y. Qed. @@ -1477,14 +1516,15 @@ Definition open_absconvex_opennbhsbasis := has_open_nbhs_basis.2. Definition basis_opennbhsbasis := has_open_nbhs_basis.1. -Lemma basis_neqset0 (B : (set (set E))) (x : E): (filter_from [set U | B U] id --> x) -> B !=set0. +Lemma basis_neqset0 (B : set_system E) (x : E) : + filter_from [set U | B U] id --> x -> B !=set0. Proof. by move=> /(_ [set: E]) /(_ filterT) [b ? _]; exists b. Qed. -Lemma absorbing_opennbhsbasis b : open_nbhsbasis_convextvs b -> pabsorbing_set b. +Lemma absorbing_opennbhsbasis : open_nbhsbasis_convextvs `<=` @absorbing_set _ E. Proof. -move=> Bb x. +move=> b Bb x. have [/(_ b Bb) n0b _] := basis_opennbhsbasis. move: n0b; rewrite -(scale0r x) => n0b. have := scalerx_continuous => /(_ _ _ x 0 b n0b) [r] /= r0 b0rb. @@ -1498,54 +1538,49 @@ End openbasis. Import Norm. -(* A should be absolutely convex and absorbing *) -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]. - +Definition gauge_fun (K : realType) (V : lmodType K) (A : set V) + (absA : absolutely_convex_set A) (absorbA : absorbing_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). +Context (K : realType) (V : lmodType K) (A : set V) + (absA : absolutely_convex_set A) (absorbA : absorbing_set A). Notation gauge_fun := (gauge_fun absA absorbA). -#[local] Lemma gauge0: gauge_fun 0 = 0. +#[local] Lemma gauge0 : gauge_fun 0 = 0. Proof. -have/absolutely_convex0 := absA => A0; rewrite /gauge_fun. +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. +have infle (r : K) : 0 < r -> inf P <= r. + move=> 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. -Lemma gauge_ge0 : forall x, 0 <= gauge_fun x. +#[local] Lemma gauge_ge0 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. +rewrite /gauge_fun; set P := (X in inf X). +have [->|/set0P P0] := eqVneq P set0; first by rewrite inf0. +by apply: lb_le_inf => // z; rewrite /P /= => -[] z0 _; rewrite ltW. Qed. -(*TO BE MOVED to reals *) +(* PR #2021 in progress *) Lemma supS (B : set K) (C : set K) : B !=set0 -> has_sup C -> B `<=` C -> sup B <= sup C. Proof. move=> B0 supC BC. @@ -1562,72 +1597,70 @@ apply: supS; first by apply/nonemptyN. by apply/has_inf_supN. by apply: image_subset. Qed. -(* END TO BE MOVED *) +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. +(* PR #2021 in progress *) (* TODO : factorise*) -#[local] Lemma ler_gaugeD: - forall x y, gauge_fun (x + y) <= gauge_fun x + gauge_fun y. +#[local] Lemma ler_gaugeD 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)) -> +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 ( *:%R t) @` A]. - move => [r r0 Aw]; split => /=; rewrite /set0P; last by exists 0 => z [z0 _]; rewrite ltW. + move => [r r0 Aw]; split => /=; rewrite /set0P; last first. + 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. + by rewrite scalerA mulVf ?scale1r ?gt_eqF. +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. +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 //. + by rewrite scalerA mulVf ?scale1r ?gt_eqF. exists r'^-1 => //=. split=> //; rewrite ?invr_gt0 //. rewrite inE /=; exists (r' *: y) => //. - by rewrite scalerA mulVf ?scale1r ?lt0r_neq0 //. + by rewrite scalerA mulVf ?scale1r ?gt_eqF. 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)). +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)). +pose st := Itv01 (divDl_ge0 (ltW t0) (ltW s0)) (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. @@ -1662,91 +1695,97 @@ rewrite neq_lt -ge0_infZl// => /orP[r0|r0]; congr inf. by exists w => //; rewrite scalerA. Qed. -HB.instance Definition _ := @isSemiNorm.Build K V gauge_fun gauge0 gauge_ge0 ler_gaugeD gaugeZ. +HB.instance Definition _ := @isSemiNorm.Build K V gauge_fun gauge0 + gauge_ge0 ler_gaugeD gaugeZ. Check (gauge_fun : SemiNorm.type V). End gauge. +Definition seminorm_on {R : realFieldType} {E : lmodType R} + (P : set (SemiNorm.type E)) (Hp : P !=set0) : Type := E. -Definition seminorm_on {R : realFieldType} {E : lmodType R} {P : set (SemiNorm.type E)} (Hp : P !=set0) : Type := E. +(* TBA convex *) +Lemma lt_conv {R : realFieldType} (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 {R : realFieldType} (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. Section convex_topology_seminorm. -Context (R : realFieldType) (E : lmodType R) (P : set (SemiNorm.type E)) (H : P !=set0). +Context (R : realFieldType) (E : lmodType R) (P : set (SemiNorm.type E)) + (H : P !=set0). 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_system E := + [set A | exists2 p, P p & exists2 e, 0 < e & + A = p @^-1` ball (0 : R) e]. Lemma nonempty_subbasis : exists B, seminorm_subbasis B. Proof. move : H => [p] Pp. -exists (p @^-1` (ball (0 : R) 1)). +exists (p @^-1` ball (0 : R) 1). by exists p => //; exists 1. Qed. -Lemma mem0_seminorm_subbasis : forall B, seminorm_subbasis B -> B 0. +Lemma mem0_seminorm_subbasis B : seminorm_subbasis B -> B 0. Proof. -by move=> B; rewrite /seminorm_subbasis /= => -[p Pp [e]] e0 -> /=; rewrite norm0; exact: ballxx. +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). +Lemma split_seminorm_subbasis 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 /seminorm_subbasis /= => -[p Pp [e e0 ->]] /=. +exists (p @^-1` ball (0 : R) (e / 2)). + 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. + by apply: ltrD; [exact: ballx|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. +apply: le_trans; last exact: Num.Theory.ler_normD. +have : p (x + y) <= p x + p y by exact: 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 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. +Lemma expand_seminorm_subbasis B r : seminorm_subbasis B -> + exists2 U, seminorm_subbasis U & ( *:%R r ) @` U `<=` B. +Proof. +rewrite /seminorm_subbasis/= => -[p Pp [e e0 ->]] /=. +have [->|rneq0] := eqVneq r (0 : R). + 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 <-. +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. +Lemma convex_seminorm_subbasis : seminorm_subbasis `<=` @convex_set _ E. Proof. move=> B ; rewrite /seminorm_subbasis /= => -[p Pp [e e0 ->]] x y r. rewrite !inE /ball /= !sub0r !normrN => px py. @@ -1758,57 +1797,56 @@ have lem1: 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. +by rewrite [X in _ + X*_]ger0_norm ?onem_ge0 // lt_conv. Qed. - -Lemma balanced_seminorm_subbasis: forall B, seminorm_subbasis B -> balanced_set B. +Lemma balanced_seminorm_subbasis : seminorm_subbasis `<=` @balanced_set _ E. 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. +apply: le_lt_trans pixr. by rewrite ler_piMl ?normr_ge0. Qed. -Lemma absolutely_convex_seminorm_subbasis: forall B, seminorm_subbasis B -> absolutely_convex_set B. +Lemma absolutely_convex_seminorm_subbasis : seminorm_subbasis `<=` @absolutely_convex_set _ E. 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. +Lemma absorbing_seminorm : seminorm_subbasis `<=` @absorbing_set _ E. +Proof. +move=> B [p Pp [r r0] ->] /= y. +have [y0|y0] := eqVneq (p y) 0. by exists 1 => //; rewrite scale1r inE /ball/ball_ /= sub0r normrN y0 normr0. -exists (r/2 * (p y)^-1). +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 inE /ball/ball_ /= sub0r normrN !normZ !normrM !normr_id. rewrite !normfV -mulrA mulVf ?normr_eq0 ? mulr1//. by rewrite ltr_pdivrMr !gtr0_norm ?ltr_pMr // ltrDr. Qed. -HB.instance Definition _ := @NbhsSubbasisAt0_isConvexTvs.Build R (seminorm_on H) +HB.instance Definition _ := @NbhsSubbasisAt0_isConvexTvs.Build R (seminorm_on H) seminorm_subbasis nonempty_subbasis mem0_seminorm_subbasis absorbing_seminorm absolutely_convex_seminorm_subbasis expand_seminorm_subbasis. (* NB: Using init-fam (see initial_topology.v) doesn't work as we strongly need a 0 basis. With init-fam we are considering nbhs a = [ [A : set E |, exists e , A = [x | |p(x) - p(a)| continuous_at 0 (p : seminorm_on H -> R). +From mathcomp Require Import finmap. + +Lemma continuous_at0_seminorm 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. +move=> 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 (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. + 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 -> /=. @@ -1841,12 +1879,12 @@ have nearp : (\forall y \near (nbhs x), -p(y - x) <= p(y) - p(x) <= p (y -x)). 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). + by rewrite -(@norm0 _ _ p); exact: continuous_at0_seminorm. by rewrite -(subrr x)=> A /= /continuous_shift; apply. -apply: (@squeeze_cvgr _ (nbhs x)) => /=; first by exact: nearp. +apply: (@squeeze_cvgr _ (nbhs x)) => /=; first exact: nearp. rewrite -oppr0; apply: (@cvgN _ R^o (seminorm_on H) _ _ (p \o (fun y => y - x))). - by exact: lem. -by apply: lem. + exact: lem. +exact: lem. Qed. End convex_topology_seminorm. @@ -1854,12 +1892,11 @@ End convex_topology_seminorm. Section generating_seminorm. Context (R : realType) (E : convexTvsType R). -Definition gauge_fun_basis (b : set E) (h : (open_nbhsbasis_convextvs b)) := -gauge_fun (open_absconvex_opennbhsbasis h).2 (absorbing_opennbhsbasis h). +Definition gauge_fun_basis (b : set E) (h : open_nbhsbasis_convextvs b) := + gauge_fun (open_absconvex_opennbhsbasis h).2 (absorbing_opennbhsbasis h). -Definition seminorm_of := -[set p : SemiNorm.type E | exists b, exists h : open_nbhsbasis_convextvs b, - p = gauge_fun_basis h]. +Definition seminorm_of := [set p : SemiNorm.type E | + exists b, exists h : open_nbhsbasis_convextvs b, p = gauge_fun_basis h]. #[local] Lemma seminorm_ofneq0 : seminorm_of !=set0. Proof. @@ -1871,8 +1908,8 @@ Qed. #[local] Notation seminormE := (@seminorm_on R E seminorm_of seminorm_ofneq0 : convexTvsType R). Let ball_gauge_fun (A : set E) (r : R) (r0 : 0 < r) - (absA : absolutely_convex_set A) (pabsA: pabsorbing_set A) (_: open A): - (gauge_fun absA pabsA) @^-1` (ball (0 : R) r) = (fun y : E => r^-1 *: y) @^-1` A. + (absA : absolutely_convex_set A) (pabsA : absorbing_set A) (_ : open A): + (gauge_fun absA pabsA) @^-1` ball (0 : R) r = (fun y : E => r^-1 *: y) @^-1` A. Proof. apply/seteqP; split => y /=; rewrite /ball /= sub0r normrN ger0_norm ?gauge_ge0 //. move/inf_lt => []. @@ -1887,7 +1924,7 @@ apply/seteqP; split => y /=; rewrite /ball /= sub0r normrN ger0_norm ?gauge_ge0 move=> Ary. have: exists2 t : R , (0 < t < 1) & (r^-1 *: y \in ( *:%R t) @` A). have /scalerx_continuous : nbhs (1 *: (r^-1 *: y)) A. - by rewrite scale1r; apply: open_nbhs_nbhs; split => //. + by rewrite scale1r; exact: open_nbhs_nbhs. move => [s /= s0] b1s. exists ((1 + `|s|/2 )^-1). rewrite ?invr_gt0 ?addr_gt0 ?mulr_gt0 ?normr_gt0 ?lt0r_neq0 ?invr_gt0 //. @@ -1901,7 +1938,7 @@ apply/seteqP; split => y /=; rewrite /ball /= sub0r normrN ger0_norm ?gauge_ge0 by rewrite scalerA mulVf ?scale1r //. move=> [t /andP [t0 t1] rytb]. have lepr: - (t*r) <= sup [set - x | x in [set r1 | 0 < r1 /\ y \in ( *:%R r1) @` A]]. - set B := ( X in _ <= sup X). + set B := (X in _ <= sup X). have Br : B (- (t * r)). exists (t * r); split => //; rewrite ?mulr_gt0 //. rewrite inE; exists (t^-1 *: (r^-1 *: y)) => //. @@ -1914,7 +1951,8 @@ apply: le_lt_trans; first by rewrite lerNl; exact lepr. by rewrite gtr_pMl. Qed. -From mathcomp Require Import finmap. (* how to do without *) +From mathcomp Require Import finmap. + (* TODO : uniformise the usage of `+ or (+%R~ @) withine lemmas *) Theorem seminorm_convextvs : continuous (id : E -> seminormE) /\ (continuous (id : seminormE -> E)). Proof. @@ -1931,13 +1969,13 @@ split=> x a. move => /nbhsE0 /= [ax] /= [b n0b ba]. have [_ /(_ b n0b) /= [b'/=]] := basis_opennbhsbasis E. move=> Bb' bb'. -pose p:= gauge_fun (open_absconvex_opennbhsbasis Bb').2 (absorbing_opennbhsbasis Bb'). +pose p := gauge_fun (open_absconvex_opennbhsbasis Bb').2 (absorbing_opennbhsbasis Bb'). have /open_absconvex_opennbhsbasis [ob' absconvb'] := Bb'. exists ([set x] `+ p @^-1` ball (0 : R) 1) => /=; last first. rewrite ball_gauge_fun => // z /= [? ->] [y]; rewrite invr1 scale1r => b1y xyz. by apply: ba; exists y => //; apply: bb'. -exists (p @^-1` ball (0 : R) 1) => //. -exists ([fset p @^-1` (ball (0 : R) 1)]%fset). +exists (p @^-1` ball (0 : R) 1) => //. +exists [fset p @^-1` (ball (0 : R) 1)]%fset. move=> c; rewrite !inE; move/eqP => ->; apply/mem_set => /=. exists p; last by exists 1. by exists b'; exists Bb'. @@ -1946,7 +1984,7 @@ rewrite /bigcap; apply/seteqP; split => z /=. by move => b1z ?; rewrite inE => /eqP ->. Qed. -Lemma continuous_seminorm_of q : (seminorm_of q) -> continuous q. +Lemma continuous_seminorm_of q : seminorm_of q -> continuous q. Proof. have -> : (q : E -> R) = (q : seminormE -> R^o) \o (id : seminormE -> E) by []. move=> qs x. @@ -1967,11 +2005,15 @@ Qed. HB.instance Definition _ := @isSemiNorm.Build R E cst0 cst00 cst0_ge0 ler_cst0D cst0Z. -(* The litterature usually states the following lemmas using a family of seminorms p_i, a family of multiplicative constantcs Ci and bounds the abs value of l : `|l i| <= sup C_i p_i (x). -We simplify these arguments using the linearity of l to get rid of the absolute value. *) +(** The litterature usually states the following lemmas using a family of + seminorms p_i, a family of multiplicative constants Ci and bounds the abs + value of l : `|l i| <= sup C_i p_i (x). + We simplify these arguments using the linearity of l to get rid of the + absolute value. *) (* 6.6.4 in Jarchow *) -Lemma linear_continuous_seminorm (l : {scalar E}): (* TODO : be more explicit in the statement *) -continuous l -> (exists2 p : SemiNorm.type E, (seminorm_of p /\ continuous p) & (forall x, l x <= p x)). +Lemma linear_continuous_seminorm (l : {scalar E}) : (* TODO : be more explicit in the statement *) + continuous l -> + exists2 p : SemiNorm.type E, (seminorm_of p /\ continuous p) & (forall x, l x <= p x). Proof. have [Bnbhs Bbasis] := basis_opennbhsbasis E. move => /[dup] cl /(_ 0 (ball (0 : R) 1)); rewrite linear0. @@ -1991,8 +2033,8 @@ exists q. move => x. case : (eqVneq x 0); first by move => ->; rewrite linear0 norm0. move=> x0. -case : (eqVneq (q x) 0). - move=> qx0. (* case forgotten in the litterature *) +have [qx0|qx0] := eqVneq (q x) 0. + (* case forgotten in the litterature *) suff: (l x) = 0 by move => ->; rewrite norm_ge0. move: qx0; rewrite /q /= /gauge_fun /= => qx0. have lxe (e : R) (e0 : 0 < e) : `|l x | < e. @@ -2015,9 +2057,8 @@ case : (eqVneq (q x) 0). apply: contrapT => /eqP h. have:= lxe `|l x|. by rewrite normr_gt0 ltxx falseE; apply. -move=> qx0. pose y := ((2 * q x)^-1) *: x. -rewrite ltW => //. +apply/ltW. have : `|l (y)| < 2^-1. apply/bl. have : (q @^-1` ball (0 : R) 1) (((2 * q x)^-1) *: x). @@ -2032,16 +2073,16 @@ rewrite /y linearZ normrM normfV normrM ger0_norm // ltr_pdivrMl. by rewrite mulr_gt0 ?normr_gt0. rewrite mulrAC divff // mul1r [in X in _ < X -> _]ger0_norm ?norm_ge0 //. move/le_lt_trans => /(_ (l x)); apply. -by rewrite ler_normr; apply/orP; left. +exact: ler_norm. Qed. -Lemma linear_seminorm_continuous (l : {scalar E}): - (exists2 p : SemiNorm.type E, continuous p & (forall x, l x <= p x)) - -> continuous (l : E -> R^o). +Lemma linear_seminorm_continuous (l : {scalar E}) : + (exists2 p : SemiNorm.type E, continuous p & (forall x, l x <= p x)) -> + continuous (l : E -> R^o). Proof. move=> [p px lpxl]; apply: continuousfor0_continuous => /= a. rewrite linear0 => -[/= e e0] balla. -have /filterS : (p @^-1` (ball_ [eta normr] (0 : R) ( e)) ) `<=` (l @^-1` a). +have /filterS : p @^-1` (ball_ [eta normr] (0 : R) e) `<=` l @^-1` a. move=> z /=; rewrite sub0r normrN ger0_norm ?norm_ge0 // => pze. apply: balla => /=; rewrite sub0r normrN. apply: le_lt_trans; last by apply: pze. @@ -2052,11 +2093,11 @@ apply => /=; rewrite -(@norm0 _ _ p); apply: px. by rewrite norm0 ; apply: nbhsx_ballx. Qed. -Proposition lcfun_seminorm (l : {scalar E}): -continuous l <-> - (exists2 p : SemiNorm.type E, continuous p & (forall x, l x <= p x)). +Proposition lcfun_seminorm (l : {scalar E}) : + continuous l <-> + exists2 p : SemiNorm.type E, continuous p & (forall x, l x <= p x). Proof. -split; last by apply: linear_seminorm_continuous. +split; last exact: linear_seminorm_continuous. by move/linear_continuous_seminorm => [p [_ cp] lpx]; exists p. Qed.