From e72b457a4e1f0270675e7d932335f847a1e5b73c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 5 Sep 2024 23:51:34 +0900 Subject: [PATCH] upd, clean --- theories/evt.v | 271 ++++++++++++++++++++++++------------------------- 1 file changed, 130 insertions(+), 141 deletions(-) diff --git a/theories/evt.v b/theories/evt.v index 0ae623a4d8..694a629e71 100644 --- a/theories/evt.v +++ b/theories/evt.v @@ -16,8 +16,8 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -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 PointedNmodule := {M of Pointed M & GRing.Nmodule M}. +HB.structure Definition PointedZmodule := {M of Pointed M & GRing.Zmodule M}. HB.structure Definition FilteredNmodule := {M of Filtered M M & GRing.Nmodule M}. HB.structure Definition FilteredZmodule := {M of Filtered M M & GRing.Zmodule M}. HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}. @@ -25,168 +25,160 @@ HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}. HB.structure Definition TopologicalNmodule := {M of Topological M & GRing.Nmodule M}. HB.structure Definition TopologicalZmodule := {M of Uniform M & GRing.Zmodule M}. -(* TODO: put this notation in classical_sets.v - and clean in topology.v cantor.v *) -Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope. - Definition convex (R : ringType) (M : lmodType R) (A : set M) := - forall x y lambda, lambda *: x + (1 - lambda) *: y \in A. - + forall x y lambda, lambda *: x + (1 - lambda) *: y \in A. + HB.mixin Record Uniform_isEvt (R : numDomainType) E of Uniform E & GRing.Lmodule R E := { - add_continuous : continuous (fun x : E*E => x.1 + x.2); (*continuous (uncurry (@GRing.add E))*) - scale_continuous : continuous (fun z: R^o * E => z.1 *: z.2); + add_continuous : continuous (fun x : E * E => x.1 + x.2) ; + (*continuous (uncurry (@GRing.add E))*) + scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2) ; (* continuous (uncurry (@GRing.scale R E) : R^o * E -> E) *) - locally_convex : exists B : set (set E), (forall b, b \in B -> convex b) /\ (basis B) - }. + locally_convex : exists2 B : set (set E), (forall b, b \in B -> convex b) & basis B +}. #[short(type="evtType")] HB.structure Definition Evt (R : numDomainType) := - {E of Uniform_isEvt R E & Uniform E & GRing.Lmodule R E}. + {E of Uniform_isEvt R E & Uniform E & GRing.Lmodule R E}. HB.factory Record TopologicalLmod_isEvt (R : numFieldType) E - of Topological E & GRing.Lmodule R E := { - add_continuous : continuous (uncurry (@GRing.add E)); - scale_continuous : continuous (uncurry (@GRing.scale R E) : R^o * E -> E); - locally_convex : exists B : set (set E), (forall b, b \in B -> convex b) /\ (basis B) - }. + of Topological E & GRing.Lmodule R E := { + add_continuous : continuous (uncurry (@GRing.add E)); + scale_continuous : continuous (uncurry (@GRing.scale R E) : R^o * E -> E); + locally_convex : exists2 B : set (set E), (forall b, b \in B -> convex b) & basis B +}. HB.builders Context R E of TopologicalLmod_isEvt R E. - Definition entourage : set_system (E * E):= - fun P=> exists U, nbhs 0 U /\ (forall xy : E * E, (xy.1 - xy.2) \in U -> xy \in P). - - Lemma entourage_filter : Filter entourage. - Proof. - split. - exists [set: E]; split; first by apply: filter_nbhsT. - by move => xy //=. - move => P Q; rewrite /entourage nbhsE //=. - move => [U [[B B0] BU Bxy]] [V [[C C0] CV Cxy]]. - exists (U`&`V); split. - exists (B`&`C); first by apply/open_nbhsI. - by apply:setISS. - move => xy; rewrite !in_setI. - move/andP => [xyU xyV]; apply/andP;split; first by apply:Bxy. - by apply: Cxy. - move => P Q PQ; rewrite /entourage /= => [[U [HU Hxy]]]; exists U; split => //. - by move => xy /Hxy /[!inE] /PQ. - Qed. - - Lemma entourage_refl_subproof : - forall A : set (E * E), entourage A -> [set xy | xy.1 = xy.2] `<=` A. - Proof. (*why bother with \in ?*) - rewrite /entourage => A [/=U [U0 Uxy]] xy //= /eqP; rewrite -subr_eq0 => /eqP xyE. - by rewrite -in_setE; apply: Uxy; rewrite xyE in_setE; apply: nbhs_singleton. - Qed. - - Lemma nbhs0N: forall (U : set E), nbhs 0 U -> nbhs 0 (-%R @` U). - Proof. - move => U U0. move: (@scale_continuous ((-1,0)) U); rewrite /= scaler0 => /(_ U0). - move => [] //= [B] B12 [B1 B2] BU. - near=> x; move => //=; exists (-x); last by rewrite opprK. - rewrite -scaleN1r; apply: (BU (-1,x)); split => //=; last first. - by near:x; rewrite nearE. - move: B1 => [] //= ? ?; apply => [] /=; first by rewrite subrr normr0 //. - Unshelve. all: by end_near. - Qed. - - Lemma nbhs0_scaler: forall (U : set E) (r : R), (r != 0) -> nbhs 0 U -> nbhs 0 ( *:%R r @` U). - Proof. - move => U r r0 U0; move: (@scale_continuous ((r^-1,0)) U); rewrite /= scaler0 => /(_ U0). - case=>//= [B] [B1 B2] BU. - near=> x => //=; exists (r^-1*:x); last by rewrite scalerA divrr ?scale1r ?unitfE //=. - apply: (BU (r^-1,x)); split => //=; last by near: x. - by apply: nbhs_singleton. - Unshelve. all: by end_near. - Qed. - - Lemma nbhs_scaler: forall (U : set E) (r : R) (x :E), ( - r != 0) -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U). - Proof. - move => U r x r0 U0; move: (@scale_continuous ((r^-1,r *:x)) U). - rewrite /= scalerA mulrC divrr ?scale1r ?unitfE //= =>/(_ U0). - case=>//= [B] [B1 B2] BU. - near=> z => //=. - exists (r^-1*:z). - apply: (BU (r^-1,z)); split => //=; last by near: z. - by apply: nbhs_singleton. - by rewrite scalerA divrr ?scale1r ?unitfE //=. - Unshelve. all: by end_near. - Qed. - - Lemma nbhsT: forall (U : set E), forall (x : E), nbhs 0 U -> nbhs x (+%R x @`U). - Proof. - move => U x U0. - move: (@add_continuous (x,-x) U) => /=; rewrite subrr => /(_ U0) //=. - case=> //= [B] [B1 B2] BU. near=> x0. - exists (x0-x); last by rewrite //= addrCA subrr addr0. - apply: (BU (x0,-x)); split => //=; last by apply: nbhs_singleton. - by near: x0; rewrite nearE. - Unshelve. all: by end_near. - Qed. - - Lemma nbhs_add: forall (U : set E) (z :E), forall (x : E), nbhs z U -> nbhs (x + z) (+%R x @`U). - Proof. - move => U z x U0. - move: (@add_continuous ((x+z)%E,-x) U) => /=. rewrite addrAC subrr add0r. - move=> /(_ U0) //=. - case=> //= [B] [B1 B2] BU. near=> x0. - exists (x0-x); last by rewrite //= addrCA subrr addr0. - apply: (BU (x0,-x)); split => //=; last by apply: nbhs_singleton. - by near: x0; rewrite nearE. - Unshelve. all: by end_near. - Qed. - - Lemma entourage_inv_subproof : - forall A : set (E * E), entourage A -> entourage A^-1%classic. - Proof. - move => A [/=U [U0 Uxy]]; rewrite /entourage /=. - exists (-%R@`U); split; first by apply: nbhs0N. - move => xy; rewrite in_setE -opprB => [[yx] Uyx] => /oppr_inj H. - by apply: Uxy; rewrite in_setE /= -H. - Qed. - - Lemma entourage_split_ex_subproof : - forall A : set (E * E), - entourage A -> exists2 B : set (E * E), entourage B & B \; B `<=` A. - Proof. - move=> A [/= U] [U0 Uxy]; rewrite /entourage /=. - move: add_continuous. rewrite /continuous_at /==> /(_ (0,0)) /=; rewrite addr0. - move=> /(_ U U0) [] /= [W1 W2] []; rewrite nbhsE /==> [[U1 nU1 UW1] [U2 nU2 UW2]] Wadd. - exists ([set w |(W1 `&` W2) (w.1 - w.2) ]). - exists (W1 `&` W2); split; last by []. - exists (U1 `&` U2); first by apply: open_nbhsI. - move => t [U1t U2t]; split; first by apply: UW1. - by apply: UW2. - move => xy /= [z [H _] [_ H']]; rewrite -inE; apply: (Uxy xy); rewrite inE. - have -> : xy.1 - xy.2= (xy.1 - z) + (z - xy.2). - by rewrite addrA -[X in (_ = X + _)]addrA [X in (_ = (_ + X)+_)]addrC addrN addr0. - by apply: (Wadd( (xy.1 - z,z - xy.2))); split => //=. - Qed. +Definition entourage : set_system (E * E):= + fun P => exists U, nbhs 0 U /\ (forall xy : E * E, (xy.1 - xy.2) \in U -> xy \in P). + +Lemma entourage_filter : Filter entourage. +Proof. +split. +- exists [set: E]; split; first by apply: filter_nbhsT. + by move => xy //=. +- move => P Q; rewrite /entourage nbhsE //=. + move => [U [[B B0] BU Bxy]] [V [[C C0] CV Cxy]]. + exists (U`&`V); split. + exists (B`&`C); first by apply/open_nbhsI. + by apply:setISS. + move => xy; rewrite !in_setI. + move/andP => [xyU xyV]; apply/andP;split; first by apply:Bxy. + by apply: Cxy. +move => P Q PQ; rewrite /entourage /= => [[U [HU Hxy]]]; exists U; split => //. +by move => xy /Hxy /[!inE] /PQ. +Qed. + +Lemma entourage_refl_subproof (A : set (E * E)) : + entourage A -> [set xy | xy.1 = xy.2] `<=` A. +Proof. (*why bother with \in ?*) +rewrite /entourage => -[/=U [U0 Uxy]] xy //= /eqP; rewrite -subr_eq0 => /eqP xyE. +by rewrite -in_setE; apply: Uxy; rewrite xyE in_setE; apply: nbhs_singleton. +Qed. + +Lemma nbhs0N (U : set E) : nbhs 0 U -> nbhs 0 (-%R @` U). +Proof. +move => U0. move: (@scale_continuous ((-1,0)) U); rewrite /= scaler0 => /(_ U0). +move => [] //= [B] B12 [B1 B2] BU. +near=> x; move => //=; exists (-x); last by rewrite opprK. +rewrite -scaleN1r; apply: (BU (-1,x)); split => //=; last first. + by near:x; rewrite nearE. +move: B1 => [] //= ? ?; apply => [] /=; first by rewrite subrr normr0 //. +Unshelve. all: by end_near. Qed. + +Lemma nbhs0_scaler (U : set E) (r : R) : r != 0 -> nbhs 0 U -> nbhs 0 ( *:%R r @` U). +Proof. +move => r0 U0; move: (@scale_continuous ((r^-1,0)) U); rewrite /= scaler0 => /(_ U0). +case=>//= [B] [B1 B2] BU. +near=> x => //=; exists (r^-1*:x); last by rewrite scalerA divrr ?scale1r ?unitfE //=. +apply: (BU (r^-1,x)); split => //=; last by near: x. +by apply: nbhs_singleton. +Unshelve. all: by end_near. Qed. + +Lemma nbhs_scaler (U : set E) (r : R) (x :E) : + r != 0 -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U). +Proof. +move => r0 U0; move: (@scale_continuous ((r^-1,r *:x)) U). +rewrite /= scalerA mulrC divrr ?scale1r ?unitfE //= =>/(_ U0). +case=>//= [B] [B1 B2] BU. +near=> z => //=. +exists (r^-1*:z). +apply: (BU (r^-1,z)); split => //=; last by near: z. +by apply: nbhs_singleton. +by rewrite scalerA divrr ?scale1r ?unitfE //=. +Unshelve. all: by end_near. Qed. + +Lemma nbhsT: forall (U : set E), forall (x : E), nbhs 0 U -> nbhs x (+%R x @`U). +Proof. +move => U x U0. +move: (@add_continuous (x,-x) U) => /=; rewrite subrr => /(_ U0) //=. +case=> //= [B] [B1 B2] BU. near=> x0. +exists (x0-x); last by rewrite //= addrCA subrr addr0. +apply: (BU (x0,-x)); split => //=; last by apply: nbhs_singleton. +by near: x0; rewrite nearE. +Unshelve. all: by end_near. Qed. + +Lemma nbhs_add: forall (U : set E) (z :E), forall (x : E), nbhs z U -> nbhs (x + z) (+%R x @`U). +Proof. +move => U z x U0. +move: (@add_continuous ((x+z)%E,-x) U) => /=. rewrite addrAC subrr add0r. +move=> /(_ U0) //=. +case=> //= [B] [B1 B2] BU. near=> x0. +exists (x0-x); last by rewrite //= addrCA subrr addr0. +apply: (BU (x0,-x)); split => //=; last by apply: nbhs_singleton. +by near: x0; rewrite nearE. +Unshelve. all: by end_near. +Qed. + +Lemma entourage_inv_subproof : + forall A : set (E * E), entourage A -> entourage A^-1%relation. +Proof. +move => A [/=U [U0 Uxy]]; rewrite /entourage /=. +exists (-%R@`U); split; first by apply: nbhs0N. +move => xy; rewrite in_setE -opprB => [[yx] Uyx] => /oppr_inj H. +by apply: Uxy; rewrite in_setE /= -H. +Qed. +Lemma entourage_split_ex_subproof : + forall A : set (E * E), + entourage A -> exists2 B : set (E * E), entourage B & (B \; B)%relation `<=` A. +Proof. +move=> A [/= U] [U0 Uxy]; rewrite /entourage /=. +move: add_continuous. rewrite /continuous_at /==> /(_ (0,0)) /=; rewrite addr0. +move=> /(_ U U0) [] /= [W1 W2] []; rewrite nbhsE /==> [[U1 nU1 UW1] [U2 nU2 UW2]] Wadd. +exists ([set w |(W1 `&` W2) (w.1 - w.2) ]). +exists (W1 `&` W2); split; last by []. + exists (U1 `&` U2); first by apply: open_nbhsI. + move => t [U1t U2t]; split; first by apply: UW1. + by apply: UW2. +move => xy /= [z [H _] [_ H']]; rewrite -inE; apply: (Uxy xy); rewrite inE. +have -> : xy.1 - xy.2= (xy.1 - z) + (z - xy.2). + by rewrite addrA -[X in (_ = X + _)]addrA [X in (_ = (_ + X)+_)]addrC addrN addr0. +by apply: (Wadd( (xy.1 - z,z - xy.2))); split => //=. +Qed. Lemma nbhsE_subproof : nbhs = nbhs_ entourage. Proof. -have lem: (-1 != (0 : R)) by rewrite oppr_eq0 oner_eq0. +have lem : -1 != 0 :> R by rewrite oppr_eq0 oner_eq0. rewrite /nbhs_ /=; apply: funext => x; rewrite /filter_from /=. apply: funext => U; apply: propext => /=; rewrite /entourage /=; split. pose V := [set v | (x-v) \in U] : set E. - move=> nU; exists [set xy | (xy.1 - xy.2) \in V]. + move=> nU; exists [set xy | (xy.1 - xy.2) \in V]. exists V;split. move: (nbhs_add (x) (nbhs_scaler lem nU))=> /=. rewrite scaleN1r subrr /= /V. - have -> : [set (x + x0)%E | x0 in [set -1 *: x | x in U]] + have -> : [set (x + x0)%E | x0 in [set -1 *: x | x in U]] = [set v | x - v \in U]. apply: funext => /= v /=; rewrite inE; apply: propext; split. - by move => [x0 [x1]] Ux1 <- <-; rewrite scaleN1r opprB addrCA subrr addr0. + by move => [x0 [x1]] Ux1 <- <-; rewrite scaleN1r opprB addrCA subrr addr0. move=> Uxy. exists (v - x). exists (x -v) => //. by rewrite scaleN1r opprB. by rewrite addrCA subrr addr0 //. by []. by move=> xy; rewrite !inE=> Vxy; rewrite /= !inE. - by move=> y; rewrite /V /= !inE /= opprB addrCA subrr addr0 inE. + by move=> y /xsectionP; rewrite /V /= !inE /= opprB addrCA subrr addr0 inE. move=> [A [U0 [NU UA]] H]. -near=> z; apply: H => /=; rewrite -inE; apply: UA => /=. +near=> z; apply: H => /=; apply/xsectionP; rewrite -inE; apply: UA => /=. near: z; rewrite nearE. move: (nbhsT x (nbhs0_scaler lem NU))=> /=. have -> : @@ -206,26 +198,23 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E entourage_inv_subproof entourage_split_ex_subproof nbhsE_subproof. HB.end. - Definition dual {R : ringType} (E : lmodType R) : Type := {scalar E}. (* Check fun {R : ringType} (E : lmodType R) => dual E : ringType. *) - HB.mixin Record hasDual (R : ringType) (E' : lmodType R) E of GRing.Lmodule R E := { dual_pair : E -> E' -> R; dual_pair_rlinear : forall x, scalar (dual_pair x); dual_pair_llinear : forall x, scalar (dual_pair^~ x); ipair : injective ( fun x => dual_pair^~ x) -}. +}. Section bacasable. -Lemma add_continuousE (R : numDomainType) (E : evtType R): -continuous (fun (xy : E*E )=> xy.1 + xy.2). +Lemma add_continuousE (R : numDomainType) (E : evtType R) : + continuous (fun xy : E * E => xy.1 + xy.2). Proof. apply: add_continuous. Qed. End bacasable. -