From 7f06e4b498dc5a4d5dd39dec0b395db741fa21ff Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 17 Nov 2023 13:09:10 +0100 Subject: [PATCH 01/14] entourage from evt and dual pair --- theories/evt.v | 231 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 231 insertions(+) create mode 100644 theories/evt.v diff --git a/theories/evt.v b/theories/evt.v new file mode 100644 index 000000000..0ae623a4d --- /dev/null +++ b/theories/evt.v @@ -0,0 +1,231 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix. +From mathcomp Require Import rat interval zmodp vector fieldext falgebra. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality set_interval Rstruct. +Require Import ereal reals signed topology prodnormedzmodule. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +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 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}. +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. + +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); + (* 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) + }. + +#[short(type="evtType")] +HB.structure Definition Evt (R : numDomainType) := + {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) + }. + +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. + + +Lemma nbhsE_subproof : nbhs = nbhs_ entourage. +Proof. +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]. + 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]] + = [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. + 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. +move=> [A [U0 [NU UA]] H]. +near=> z; apply: H => /=; rewrite -inE; apply: UA => /=. +near: z; rewrite nearE. +move: (nbhsT x (nbhs0_scaler lem NU))=> /=. +have -> : +[set (x + x0)%E | x0 in [set -1 *: x | x in U0]] = (fun x0 : E => x - x0 \in U0). + apply:funext => /= z /=; apply: propext; split. + move=> [x0] [x1 Ux1 <-] <-. + rewrite -opprB. rewrite addrAC subrr add0r inE scaleN1r opprK //. + rewrite inE => Uxz. exists (z-x). exists (x-z) => //. + by rewrite scalerBr !scaleN1r opprK addrC. + by rewrite addrCA subrr addr0. +by []. +Unshelve. all: by end_near. +Qed. + +HB.instance Definition _ := Nbhs_isUniform_mixin.Build E + entourage_filter entourage_refl_subproof + 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). +Proof. +apply: add_continuous. +Qed. + +End bacasable. + From 385b345c3e411cd9672e89678231f97d4945a7f1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 5 Sep 2024 23:51:34 +0900 Subject: [PATCH 02/14] upd, clean --- theories/evt.v | 271 ++++++++++++++++++++++++------------------------- 1 file changed, 130 insertions(+), 141 deletions(-) diff --git a/theories/evt.v b/theories/evt.v index 0ae623a4d..694a629e7 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. - From 3f981984151857fc233dbbfdcf1f8da1c15ecfd5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 6 Sep 2024 00:40:40 +0900 Subject: [PATCH 03/14] make normedtype.v depend on evt.v --- _CoqProject | 1 + theories/Make | 1 + theories/derive.v | 10 +++++----- theories/evt.v | 14 +++++++++++++- theories/exp.v | 8 ++++---- theories/ftc.v | 4 ++-- theories/lebesgue_integral.v | 8 ++++---- theories/lebesgue_measure.v | 2 +- theories/normedtype.v | 1 + theories/realfun.v | 8 ++++---- theories/sequences.v | 20 ++++++++++---------- 11 files changed, 46 insertions(+), 31 deletions(-) diff --git a/_CoqProject b/_CoqProject index 54e246e2d..b7a78865c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -28,6 +28,7 @@ theories/topology.v theories/function_spaces.v theories/cantor.v theories/prodnormedzmodule.v +theories/evt.v theories/normedtype.v theories/realfun.v theories/sequences.v diff --git a/theories/Make b/theories/Make index f4e9346fc..a0f868e85 100644 --- a/theories/Make +++ b/theories/Make @@ -16,6 +16,7 @@ topology.v function_spaces.v cantor.v prodnormedzmodule.v +evt.v normedtype.v realfun.v sequences.v diff --git a/theories/derive.v b/theories/derive.v index 9f97fe633..8dfbc9054 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -233,13 +233,13 @@ Qed. End diff_locally_converse_tentative. Definition derive (f : V -> W) a v := - lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ 0^'). + lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ (0:R)^'). Local Notation "''D_' v f" := (derive f ^~ v). Local Notation "''D_' v f c" := (derive f c v). (* printing *) Definition derivable (f : V -> W) a v := - cvg ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ 0^'). + cvg ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ (0:R)^'). Class is_derive (a v : V) (f : V -> W) (df : W) := DeriveDef { ex_derive : derivable f a v; @@ -356,7 +356,7 @@ Lemma derivemxE m n (f : 'rV[R]_m.+1 -> 'rV[R]_n.+1) (a v : 'rV[R]_m.+1) : Proof. by move=> /deriveE->; rewrite /jacobian mul_rV_lin1. Qed. Definition derive1 V (f : R -> V) (a : R) := - lim ((fun h => h^-1 *: (f (h + a) - f a)) @ 0^'). + lim ((fun h => h^-1 *: (f (h + a) - f a)) @ (0:R)^'). Local Notation "f ^` ()" := (derive1 f). @@ -1125,7 +1125,7 @@ Implicit Types f g : V -> W. Fact der_add f g (x v : V) : derivable f x v -> derivable g x v -> (fun h => h^-1 *: (((f + g) \o shift x) (h *: v) - (f + g) x)) @ - 0^' --> 'D_v f x + 'D_v g x. + (0:R)^' --> 'D_v f x + 'D_v g x. Proof. move=> df dg. evar (fg : R -> W); rewrite [X in X @ _](_ : _ = fg) /=; last first. @@ -1177,7 +1177,7 @@ Qed. Fact der_opp f (x v : V) : derivable f x v -> (fun h => h^-1 *: (((- f) \o shift x) (h *: v) - (- f) x)) @ - 0^' --> - 'D_v f x. + (0:R)^' --> - 'D_v f x. Proof. move=> df; evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first. by rewrite funeqE => h; rewrite !scalerDr !scalerN -opprD -scalerBr /g. diff --git a/theories/evt.v b/theories/evt.v index 694a629e7..98c421438 100644 --- a/theories/evt.v +++ b/theories/evt.v @@ -18,12 +18,24 @@ 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 PointedLmodule (K : numDomainType) := + {M of Pointed M & GRing.Lmodule K 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 FilteredLmodule (K : numDomainType) := + {M of Filtered M M & GRing.Lmodule K M}. HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}. HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}. +HB.structure Definition NbhsLmodule (K : numDomainType) := + {M of Nbhs M & GRing.Lmodule K M}. HB.structure Definition TopologicalNmodule := {M of Topological M & GRing.Nmodule M}. -HB.structure Definition TopologicalZmodule := {M of Uniform M & GRing.Zmodule M}. +HB.structure Definition TopologicalZmodule := + {M of Topological M & GRing.Zmodule M}. +HB.structure Definition TopologicalLmodule (K : numDomainType) := + {M of Topological M & GRing.Lmodule K M}. +HB.structure Definition UniformZmodule := {M of Uniform M & GRing.Zmodule M}. +HB.structure Definition UniformLmodule (K : numDomainType) := + {M of Uniform M & GRing.Lmodule K M}. Definition convex (R : ringType) (M : lmodType R) (A : set M) := forall x y lambda, lambda *: x + (1 - lambda) *: y \in A. diff --git a/theories/exp.v b/theories/exp.v index de5bbfc1c..47e09ee1a 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -198,10 +198,10 @@ Lemma pseries_snd_diffs (c : R^nat) K x : Proof. move=> Ck CdK CddK xLK; rewrite /pseries. set s := (fun n : nat => _); set (f := fun x0 => _). -suff hfxs : h^-1 *: (f (h + x) - f x) @[h --> 0^'] --> limn (series s). +suff hfxs : h^-1 *: (f (h + x) - f x) @[h --> (0:R)^'] --> limn (series s). have F : f^`() x = limn (series s) by apply: cvg_lim hfxs. have Df : derivable f x 1. - move: hfxs; rewrite /derivable [X in X @ 0^'](_ : _ = + move: hfxs; rewrite /derivable [X in X @ (0:R)^'](_ : _ = (fun h => h^-1 *: (f (h%:A + x) - f x))) /=; last first. by apply/funext => i //=; rewrite [i%:A]mulr1. by move=> /(cvg_lim _) -> //. @@ -209,7 +209,7 @@ suff hfxs : h^-1 *: (f (h + x) - f x) @[h --> 0^'] --> limn (series s). pose sx := fun n : nat => c n * x ^+ n. have Csx : cvgn (pseries c x) by apply: is_cvg_pseries_inside Ck _. pose shx := fun h (n : nat) => c n * (h + x) ^+ n. -suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> limn (series s). +suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> (0:R)^'] --> limn (series s). apply: cvg_sub0 Cc. apply/cvgrPdist_lt => eps eps_gt0 /=. near=> h; rewrite sub0r normrN /=. @@ -229,7 +229,7 @@ suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> limn (series s). apply: cvg_zero => /=. suff Cc : limn (series (fun n => c n * (((h + x) ^+ n - x ^+ n) / h - n%:R * x ^+ n.-1))) - @[h --> 0^'] --> (0 : R). + @[h --> (0:R)^'] --> (0 : R). apply: cvg_sub0 Cc. apply/cvgrPdist_lt => eps eps_gt0 /=. near=> h; rewrite sub0r normrN /=. diff --git a/theories/ftc.v b/theories/ftc.v index 5d0138223..0f0854f4a 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -38,7 +38,7 @@ Implicit Types (f : R -> R) (a : itv_bound R). Let FTC0 f a : mu.-integrable setT (EFin \o f) -> let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in forall x, a < BRight x -> lebesgue_pt f x -> - h^-1 *: (F (h + x) - F x) @[h --> 0%R^'] --> f x. + h^-1 *: (F (h + x) - F x) @[h --> (0:R)%R^'] --> f x. Proof. move=> intf F x ax fx. have locf : locally_integrable setT f. @@ -294,7 +294,7 @@ Unshelve. all: by end_near. Qed. Lemma parameterized_integral_cvg_left a b (f : R -> R) : a < b -> mu.-integrable `[a, b] (EFin \o f) -> - int a x f @[x --> a] --> 0. + int a x f @[x --> a] --> (0:R). Proof. move=> ab intf; pose fab := f \_ `[a, b]. have intfab : mu.-integrable `[a, b] (EFin \o fab). diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index d2e152fb3..d9a4fb154 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -6149,7 +6149,7 @@ Hypotheses (xU : open_nbhs x U) (mU : measurable U) (mUf : measurable_fun U f) (fx : {for x, continuous f}). Let continuous_integralB_fin_num : - \forall t \near 0%R, + \forall t \near (0:R)%R, \int[mu]_(y in ball x t) `|(f y)%:E - (f x)%:E| \is a fin_num. Proof. move: fx => /cvgrPdist_le /= fx'. @@ -6172,7 +6172,7 @@ apply: ge0_le_integral => //=; first exact: measurable_ball. Unshelve. all: by end_near. Qed. Let continuous_davg_fin_num : - \forall A \near 0%R, davg f x A \is a fin_num. + \forall A \near (0:R)%R, davg f x A \is a fin_num. Proof. have [e /= e0 exf] := continuous_integralB_fin_num. move: fx => /cvgrPdist_le fx'. @@ -6183,7 +6183,7 @@ near=> t; have [t0|t0] := leP t 0%R; first by rewrite davg0. by rewrite fin_numM// exf/=. Unshelve. all: by end_near. Qed. -Lemma continuous_cvg_davg : davg f x r @[r --> 0%R] --> 0. +Lemma continuous_cvg_davg : davg f x r @[r --> (0:R)%R] --> 0. Proof. apply/fine_cvgP; split; first exact: continuous_davg_fin_num. apply/cvgrPdist_le => e e0. @@ -6795,7 +6795,7 @@ Local Notation mu := lebesgue_measure. Definition nicely_shrinking x E := (forall n, measurable (E n)) /\ exists Cr : R * {posnum R}^nat, [/\ Cr.1 > 0, - (Cr.2 n)%:num @[n --> \oo] --> 0, + (Cr.2 n)%:num @[n --> \oo] --> (0:R), (forall n, E n `<=` ball x (Cr.2 n)%:num) & (forall n, mu (ball x (Cr.2 n)%:num) <= Cr.1%:E * mu (E n))%E]. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 4208007bb..803e692ce 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1098,7 +1098,7 @@ rewrite (_ : [set~ 0] = `]-oo, 0[ `|` `]0, +oo[); last first. rewrite in_itv/= -eq_le eq_sym; [move/eqP/negbTE => ->|move/negP/eqP]. apply/measurable_funU => //; split. - apply/measurable_restrictT => //=. - rewrite (_ : _ \_ _ = cst 0)//; apply/funext => y; rewrite patchE. + rewrite (_ : _ \_ _ = cst (0:R))//; apply/funext => y; rewrite patchE. by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW. - have : {in `]0, +oo[%classic, continuous (@ln R)}. by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln. diff --git a/theories/normedtype.v b/theories/normedtype.v index 4252b849a..5d75b41bf 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -6,6 +6,7 @@ From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import archimedean. From mathcomp Require Import cardinality set_interval Rstruct. Require Import ereal reals signed topology prodnormedzmodule function_spaces. +Require Import evt. (**md**************************************************************************) (* # Norm-related Notions *) diff --git a/theories/realfun.v b/theories/realfun.v index d88ffe174..55f576959 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1511,7 +1511,7 @@ Proof. exact: (@exprn_continuous 2%N). Qed. Lemma sqrt_continuous : continuous (@Num.sqrt R). Proof. move=> x; case: (ltrgtP x 0) => [xlt0 | xgt0 | ->]. -- apply: (near_cst_continuous 0). +- apply: (near_cst_continuous (0:R)). by near do rewrite ltr0_sqrtr//; apply: (cvgr_lt x). pose I b : set R := [set` `]0 ^+ 2, b ^+ 2[]. suff main b : 0 <= b -> {in I b, continuous (@Num.sqrt R)}. @@ -1545,18 +1545,18 @@ split => [Hd|[g [fxE Cg gxE]]]. by rewrite -subr_eq0 => /divfK->. - apply/continuous_withinNshiftx; rewrite eqxx /=. pose g1 h := (h^-1 *: ((f \o shift x) h%:A - f x)). - have F1 : g1 @ 0^' --> a by case: Hd => H1 <-. + have F1 : g1 @ (0:R)^' --> a by case: Hd => H1 <-. apply: cvg_trans F1; apply: near_eq_cvg; rewrite /g1 !fctE. near=> i. rewrite ifN; first by rewrite addrK mulrC /= [_%:A]mulr1. rewrite -subr_eq0 addrK. by near: i; rewrite near_withinE /= near_simpl; near=> x1. by rewrite eqxx. -suff Hf : h^-1 *: ((f \o shift x) h%:A - f x) @[h --> 0^'] --> a. +suff Hf : h^-1 *: ((f \o shift x) h%:A - f x) @[h --> (0:R)^'] --> a. have F1 : 'D_1 f x = a by apply: cvg_lim. rewrite -F1 in Hf. by constructor. - have F1 : (g \o shift x) y @[y --> 0^'] --> a. + have F1 : (g \o shift x) y @[y --> (0:R)^'] --> a. by rewrite -gxE; apply/continuous_withinNshiftx. apply: cvg_trans F1; apply: near_eq_cvg. near=> y. diff --git a/theories/sequences.v b/theories/sequences.v index 5a54e2407..e7385ba7f 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -580,14 +580,14 @@ Notation nonincreasing_cvg_ge := nonincreasing_cvgn_ge (only parsing). Notation nondecreasing_cvg_le := nondecreasing_cvgn_le (only parsing). Lemma __deprecated__invr_cvg0 (R : realFieldType) (u : R^nat) : - (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> 0) <-> (u @ \oo --> +oo). + (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> (0:R)) <-> (u @ \oo --> +oo). Proof. by move=> ?; rewrite gtr0_cvgV0//; apply: nearW. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `gtr0_cvgV0` and generalized")] Notation invr_cvg0 := __deprecated__invr_cvg0 (only parsing). Lemma __deprecated__invr_cvg_pinfty (R : realFieldType) (u : R^nat) : - (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> +oo) <-> (u @ \oo--> 0). + (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> +oo) <-> (u @ \oo--> (0:R)). Proof. by move=> ?; rewrite cvgrVy//; apply: nearW. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgrVy` and generalized")] @@ -831,7 +831,7 @@ Proof. by rewrite /=. Qed. Lemma harmonic_ge0 {R : numFieldType} i : 0 <= harmonic i :> R. Proof. exact/ltW/harmonic_gt0. Qed. -Lemma cvg_harmonic {R : archiFieldType} : @harmonic R @ \oo --> 0. +Lemma cvg_harmonic {R : archiFieldType} : @harmonic R @ \oo --> (0:R). Proof. apply/cvgrPdist_le => _/posnumP[e]; near=> i. rewrite distrC subr0 ger0_norm//= -lef_pV2 ?qualifE//= invrK. @@ -1170,7 +1170,7 @@ Qed. Lemma cvg_to_0_linear (R : realFieldType) (f : R -> R) K (k : R) : 0 < k -> (forall r, 0 < `| r | < k -> `|f r| <= K * `| r |) -> - f x @[x --> 0^'] --> 0. + f x @[x --> (0:R)^'] --> (0:R). Proof. move=> k0 kfK; have [K0|K0] := lerP K 0. - apply/cvgrPdist_lt => _/posnumP[e]; near=> x. @@ -1179,7 +1179,7 @@ move=> k0 kfK; have [K0|K0] := lerP K 0. near: x; exists (k / 2); first by rewrite /mkset divr_gt0. move=> t /=; rewrite distrC subr0 => tk2 t0. by rewrite normr_gt0 t0 (lt_trans tk2) // -[in ltLHS](add0r k) midf_lt. -- apply/(@eqolim0 _ _ R (0^'))/eqoP => _/posnumP[e]; near=> x. +- apply/(@eqolim0 _ _ R (0:R)^')/eqoP => _/posnumP[e]; near=> x. rewrite (le_trans (kfK _ _)) //=. + near: x; exists (k / 2); first by rewrite /mkset divr_gt0. move=> t /=; rewrite distrC subr0 => tk2 t0. @@ -1192,7 +1192,7 @@ Unshelve. all: by end_near. Qed. Lemma lim_cvg_to_0_linear (R : realType) (f : nat -> R) (g : R -> nat -> R) k : 0 < k -> cvgn (series f) -> (forall r, 0 < `|r| < k -> forall n, `|g r n| <= f n * `| r |) -> - limn (series (g x)) @[x --> 0^'] --> 0. + limn (series (g x)) @[x --> (0:R)^'] --> (0:R). Proof. move=> k_gt0 Cf Hg. apply: (@cvg_to_0_linear _ _ (limn (series f)) k) => // h hLk; rewrite mulrC. @@ -2145,7 +2145,7 @@ Context {R : realFieldType}. Implicit Types (u : R^nat) (r : R). Lemma minr_cvg_0_cvg_0 u r : 0 < r -> (forall k, 0 <= u k) -> - minr (u n) r @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 0. + minr (u n) r @[n --> \oo] --> (0:R) -> u n @[n --> \oo] --> (0:R). Proof. move=> r0 u0 minr_cvg; apply/cvgrPdist_lt => _ /posnumP[e]. have : 0 < minr e%:num r by rewrite lt_min// r0 andbT. @@ -2157,7 +2157,7 @@ by rewrite le_min u0 ltW. Unshelve. all: by end_near. Qed. Lemma maxr_cvg_0_cvg_0 u r : r < 0 -> (forall k, u k <= 0) -> - maxr (u n) r @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 0. + maxr (u n) r @[n --> \oo] --> (0:R) -> u n @[n --> \oo] --> (0:R). Proof. rewrite -[in r < _]oppr0 ltrNr => r0 u0. under eq_fun do rewrite -(opprK (u _)) -[in maxr _ _](opprK r) -oppr_min. @@ -2189,7 +2189,7 @@ Unshelve. all: by end_near. Qed. Lemma mine_cvg_minr_cvg u r : (0 < r)%R -> (forall k, 0 <= u k) -> mine (u n) r%:E @[n --> \oo] --> 0 -> - minr (fine (u n)) r @[n --> \oo] --> 0%R. + minr (fine (u n)) r @[n --> \oo] --> (0:R)%R. Proof. move=> r0 u0 mine_cvg; apply: (cvg_trans _ (fine_cvg mine_cvg)). move/fine_cvgP : mine_cvg => [_ /=] /cvgrPdist_lt. @@ -2227,7 +2227,7 @@ Qed. Lemma maxe_cvg_maxr_cvg u r : (r < 0)%R -> (forall k, u k <= 0) -> maxe (u n) r%:E @[n --> \oo] --> 0 -> - maxr (fine (u n)) r @[n --> \oo] --> 0%R. + maxr (fine (u n)) r @[n --> \oo] --> (0:R)%R. Proof. rewrite -[in (r < _)%R]oppr0 ltrNr => r0 u0. under eq_fun do rewrite -(oppeK (u _)) -[in maxe _ _](oppeK r%:E) -oppe_min. From 4037a9d59f9360f1e653ddbd7996d7c7c40f53ec Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 6 Sep 2024 17:49:34 +0900 Subject: [PATCH 04/14] renaming --- _CoqProject | 2 +- theories/Make | 2 +- theories/normedtype.v | 23 ++++++++++++++++++++++- theories/{evt.v => tvs.v} | 17 +++++++++-------- 4 files changed, 33 insertions(+), 11 deletions(-) rename theories/{evt.v => tvs.v} (94%) diff --git a/_CoqProject b/_CoqProject index b7a78865c..7a09f3f43 100644 --- a/_CoqProject +++ b/_CoqProject @@ -28,7 +28,7 @@ theories/topology.v theories/function_spaces.v theories/cantor.v theories/prodnormedzmodule.v -theories/evt.v +theories/tvs.v theories/normedtype.v theories/realfun.v theories/sequences.v diff --git a/theories/Make b/theories/Make index a0f868e85..5243f4661 100644 --- a/theories/Make +++ b/theories/Make @@ -16,7 +16,7 @@ topology.v function_spaces.v cantor.v prodnormedzmodule.v -evt.v +tvs.v normedtype.v realfun.v sequences.v diff --git a/theories/normedtype.v b/theories/normedtype.v index 5d75b41bf..34eaac114 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -6,7 +6,7 @@ From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import archimedean. From mathcomp Require Import cardinality set_interval Rstruct. Require Import ereal reals signed topology prodnormedzmodule function_spaces. -Require Import evt. +Require Import tvs. (**md**************************************************************************) (* # Norm-related Notions *) @@ -791,6 +791,11 @@ HB.mixin Record PseudoMetricNormedZmod_Lmodule_isNormedModule K V normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. +(*#[short(type="normedModType")] +HB.structure Definition NormedModule (K : numDomainType) := + {T of TopologicalLmodule K T & GRing.Lmodule K T + & PseudoMetricNormedZmod_Lmodule_isNormedModule K T}.*) + #[short(type="normedModType")] HB.structure Definition NormedModule (K : numDomainType) := {T of PseudoMetricNormedZmod K T & GRing.Lmodule K T @@ -805,6 +810,22 @@ HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R R^o erefl. HB.instance Definition _ := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R R^o (@normrM _). +(*Let Ro_add_continuous : continuous (uncurry (@GRing.add R^o)). +Proof. +Admitted. + +Let Ro_scale_continuous : + continuous (uncurry (@GRing.scale R R^o) : R^o * R^o -> R^o). +Admitted. + +Let Ro_locally_convex : exists2 B : set (set R^o), + (forall b, b \in B -> convex b) & basis B. +Admitted. + +HB.instance Definition _ := + TopologicalLmod_isTvs.Build R R^o Ro_add_continuous + Ro_scale_continuous Ro_locally_convex.*) + End regular_topology. Lemma ball_itv {R : realFieldType} (x r : R) : diff --git a/theories/evt.v b/theories/tvs.v similarity index 94% rename from theories/evt.v rename to theories/tvs.v index 98c421438..f58bcb865 100644 --- a/theories/evt.v +++ b/theories/tvs.v @@ -18,8 +18,8 @@ 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 PointedLmodule (K : numDomainType) := - {M of Pointed M & GRing.Lmodule K M}. +HB.structure Definition PointedLmodule (K : numDomainType) := {M of Pointed M & GRing.Lmodule K 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 FilteredLmodule (K : numDomainType) := @@ -28,7 +28,8 @@ HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}. HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}. HB.structure Definition NbhsLmodule (K : numDomainType) := {M of Nbhs M & GRing.Lmodule K M}. -HB.structure Definition TopologicalNmodule := {M of Topological M & GRing.Nmodule M}. + +(*HB.structure Definition TopologicalNmodule := {M of Topological M & GRing.Nmodule M}.*) HB.structure Definition TopologicalZmodule := {M of Topological M & GRing.Zmodule M}. HB.structure Definition TopologicalLmodule (K : numDomainType) := @@ -40,7 +41,7 @@ HB.structure Definition UniformLmodule (K : numDomainType) := Definition convex (R : ringType) (M : lmodType R) (A : set M) := 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 := { +HB.mixin Record Uniform_isTvs (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) ; @@ -49,17 +50,17 @@ HB.mixin Record Uniform_isEvt (R : numDomainType) E of Uniform E & GRing.Lmodule }. #[short(type="evtType")] -HB.structure Definition Evt (R : numDomainType) := - {E of Uniform_isEvt R E & Uniform E & GRing.Lmodule R E}. +HB.structure Definition Tvs (R : numDomainType) := + {E of Uniform_isTvs R E & Uniform E & GRing.Lmodule R E}. -HB.factory Record TopologicalLmod_isEvt (R : numFieldType) E +HB.factory Record TopologicalLmod_isTvs (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 : exists2 B : set (set E), (forall b, b \in B -> convex b) & basis B }. -HB.builders Context R E of TopologicalLmod_isEvt R E. +HB.builders Context R E of TopologicalLmod_isTvs 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). From 041be9e8b6fa67d921fdb371f507f26660c84ca8 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 6 Sep 2024 17:03:41 +0200 Subject: [PATCH 05/14] Tvs on numDomain --- theories/tvs.v | 197 +++++++++++++++++++++++++++++++++---------------- 1 file changed, 135 insertions(+), 62 deletions(-) diff --git a/theories/tvs.v b/theories/tvs.v index f58bcb865..02ac05bcf 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -38,6 +38,7 @@ HB.structure Definition UniformZmodule := {M of Uniform M & GRing.Zmodule M}. HB.structure Definition UniformLmodule (K : numDomainType) := {M of Uniform M & GRing.Lmodule K M}. + Definition convex (R : ringType) (M : lmodType R) (A : set M) := forall x y lambda, lambda *: x + (1 - lambda) *: y \in A. @@ -49,79 +50,56 @@ HB.mixin Record Uniform_isTvs (R : numDomainType) E of Uniform E & GRing.Lmodule locally_convex : exists2 B : set (set E), (forall b, b \in B -> convex b) & basis B }. -#[short(type="evtType")] +#[short(type="tvsType")] HB.structure Definition Tvs (R : numDomainType) := {E of Uniform_isTvs R E & Uniform E & GRing.Lmodule R E}. -HB.factory Record TopologicalLmod_isTvs (R : numFieldType) E + + +HB.factory Record TopologicalLmod_isTvs (R : numDomainType) 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); + 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 : exists2 B : set (set E), (forall b, b \in B -> convex b) & basis B -}. + }. + + HB.builders Context R E of TopologicalLmod_isTvs 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 (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. +(* TODO: delete the next lemmas to better incorporate their proofs*) Lemma nbhs0N (U : set E) : nbhs 0 U -> nbhs 0 (-%R @` U). -Proof. -move => U0. move: (@scale_continuous ((-1,0)) U); rewrite /= scaler0 => /(_ U0). +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. +Unshelve. all: by end_near. Qed. -Lemma nbhs0_scaler (U : set E) (r : R) : r != 0 -> nbhs 0 U -> nbhs 0 ( *:%R r @` U). +Lemma nbhsN (U : set E) (x : E) : nbhs x U -> nbhs (-x) (-%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. +move => Ux. +move: (@scale_continuous (-1,-x) U). +rewrite /= scaleN1r opprK => /(_ Ux). +move => [] //= [B] B12 [B1 B2] BU. +near=> y; move => //=; exists (-y); last by rewrite opprK. +rewrite -scaleN1r; apply: (BU (-1,y)); split => //=; last first. + by near:y; rewrite nearE. +move: B1 => [] //= ? ?; apply => [] /=; first by rewrite subrr normr0 //. 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). +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) //=. @@ -131,7 +109,7 @@ 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). +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. @@ -143,6 +121,32 @@ by near: x0; rewrite nearE. Unshelve. all: by end_near. Qed. + +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 entourage_inv_subproof : forall A : set (E * E), entourage A -> entourage A^-1%relation. Proof. @@ -177,30 +181,29 @@ 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]. - 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]] + exists V;split. + move: (nbhs_add (x) (nbhsN nU)); rewrite /= subrr /= /V. + have -> : [set (x + x0)%E | x0 in [set - 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 opprB addrCA subrr addr0. move=> Uxy. exists (v - x). exists (x -v) => //. - by rewrite scaleN1r opprB. + by rewrite opprB. by rewrite addrCA subrr addr0 //. by []. by move=> xy; rewrite !inE=> Vxy; rewrite /= !inE. by move=> y /xsectionP; rewrite /V /= !inE /= opprB addrCA subrr addr0 inE. -move=> [A [U0 [NU UA]] H]. +move=> [A [U0 [nU UA]] H]. near=> z; apply: H => /=; apply/xsectionP; rewrite -inE; apply: UA => /=. near: z; rewrite nearE. -move: (nbhsT x (nbhs0_scaler lem NU))=> /=. +move: (nbhsT x (nbhs0N nU))=> /=. have -> : -[set (x + x0)%E | x0 in [set -1 *: x | x in U0]] = (fun x0 : E => x - x0 \in U0). +[set (x + x0)%E | x0 in [set - x | x in U0]] = (fun x0 : E => x - x0 \in U0). apply:funext => /= z /=; apply: propext; split. move=> [x0] [x1 Ux1 <-] <-. - rewrite -opprB. rewrite addrAC subrr add0r inE scaleN1r opprK //. + rewrite -opprB; rewrite addrAC subrr add0r inE opprK //. rewrite inE => Uxz. exists (z-x). exists (x-z) => //. - by rewrite scalerBr !scaleN1r opprK addrC. + by rewrite opprB. by rewrite addrCA subrr addr0. by []. Unshelve. all: by end_near. @@ -212,6 +215,72 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E nbhsE_subproof. HB.end. + +Section FirstLemmas. + + +Lemma nbhs0N (R : numDomainType) (E : tvsType R) (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 nbhsT (R : numDomainType) (E : tvsType R) : + 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 (R : numDomainType) (E : tvsType R) : + 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 nbhs0_scaler (R : numFieldType) (E : tvsType R) (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 (R : numFieldType) (E : tvsType R) (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. + + +End FirstLemmas. + Definition dual {R : ringType} (E : lmodType R) : Type := {scalar E}. (* Check fun {R : ringType} (E : lmodType R) => dual E : ringType. *) @@ -222,12 +291,16 @@ HB.mixin Record hasDual (R : ringType) (E' : lmodType R) E of GRing.Lmodule R E ipair : injective ( fun x => dual_pair^~ x) }. + + Section bacasable. -Lemma add_continuousE (R : numDomainType) (E : evtType R) : +Lemma add_continuousE (R : numDomainType) (E : tvsType R) : continuous (fun xy : E * E => xy.1 + xy.2). Proof. apply: add_continuous. Qed. End bacasable. + +About opprB. From 7b5855887f707ec6d68a1fd7c89fda595571da74 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 6 Sep 2024 17:30:47 +0200 Subject: [PATCH 06/14] normedType on tvsType --- theories/normedtype.v | 42 +++++++++++++++++++++++++++++------------- 1 file changed, 29 insertions(+), 13 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 34eaac114..b75775a69 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -791,31 +791,40 @@ HB.mixin Record PseudoMetricNormedZmod_Lmodule_isNormedModule K V normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. -(*#[short(type="normedModType")] -HB.structure Definition NormedModule (K : numDomainType) := - {T of TopologicalLmodule K T & GRing.Lmodule K T - & PseudoMetricNormedZmod_Lmodule_isNormedModule K T}.*) - #[short(type="normedModType")] HB.structure Definition NormedModule (K : numDomainType) := - {T of PseudoMetricNormedZmod K T & GRing.Lmodule K T + {T of PseudoMetricNormedZmod K T & Tvs K T & PseudoMetricNormedZmod_Lmodule_isNormedModule K T}. +(* TODO: several factories, from a norm add-continuous, +scale_continuous and locally convex can be deduced *) + Section regular_topology. Variable R : numFieldType. HB.instance Definition _ := Num.NormedZmodule.on R^o. HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R R^o erefl. -HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R R^o (@normrM _). -(*Let Ro_add_continuous : continuous (uncurry (@GRing.add R^o)). + +Let Ro_add_continuous : continuous (fun x : R^o * R^o => x.1 + x.2). Proof. +(* Ugly proof +move=> [/= x y]. +apply/cvg_ballP => e e0. +rewrite /= nearE /= -nbhs_ballE /nbhs_ball /nbhs_ball_ /=. +exists ((ball x (e/2)),(ball y (e/2))). +by move=> /=; split => /=; exists (e/2) => //=; rewrite ?divr_gt0. +move => [z1 z2]; rewrite /ball /= =>- [B1 B2]. +rewrite (le_lt_trans (ler_normD _ _)) //. +rewrite (splitr e). +rewrite ltrD //. +Qed. + *) Admitted. Let Ro_scale_continuous : - continuous (uncurry (@GRing.scale R R^o) : R^o * R^o -> R^o). + continuous (fun z : R^o * R^o => z.1 *: z.2). Admitted. Let Ro_locally_convex : exists2 B : set (set R^o), @@ -823,8 +832,11 @@ Let Ro_locally_convex : exists2 B : set (set R^o), Admitted. HB.instance Definition _ := - TopologicalLmod_isTvs.Build R R^o Ro_add_continuous - Ro_scale_continuous Ro_locally_convex.*) + Uniform_isTvs.Build R R^o Ro_add_continuous + Ro_scale_continuous Ro_locally_convex. + +HB.instance Definition _ := + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R R^o (@normrM _). End regular_topology. @@ -842,7 +854,11 @@ Variable (R : realType). #[export, non_forgetful_inheritance] HB.instance Definition _ := GRing.ComAlgebra.copy R R^o. #[export, non_forgetful_inheritance] -HB.instance Definition _ := Vector.copy R R^o. + HB.instance Definition _ := Vector.copy R R^o. +Check (R^o : evtType _ ). + +HB.howto GRing.regular normedModType. + #[export, non_forgetful_inheritance] HB.instance Definition _ := NormedModule.copy R R^o. End realType. From 3b443c347bae48ceed6cb7846d64c0d09f6dcb2d Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 6 Sep 2024 17:32:54 +0200 Subject: [PATCH 07/14] clean --- theories/normedtype.v | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index b75775a69..8e98652c4 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -854,10 +854,7 @@ Variable (R : realType). #[export, non_forgetful_inheritance] HB.instance Definition _ := GRing.ComAlgebra.copy R R^o. #[export, non_forgetful_inheritance] - HB.instance Definition _ := Vector.copy R R^o. -Check (R^o : evtType _ ). - -HB.howto GRing.regular normedModType. +HB.instance Definition _ := Vector.copy R R^o. #[export, non_forgetful_inheritance] HB.instance Definition _ := NormedModule.copy R R^o. From 681156dc5f6308845dbd3fdc136639d09b1b9e18 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Mon, 9 Sep 2024 16:15:11 +0200 Subject: [PATCH 08/14] fixing factory lmod_normed --- theories/normedtype.v | 60 +++++++++++++++++++------------------------ 1 file changed, 27 insertions(+), 33 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 8e98652c4..c6b34029b 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -786,57 +786,52 @@ Proof. by rewrite cvgeryP cvgrnyP. Qed. (** Modules with a norm *) -HB.mixin Record PseudoMetricNormedZmod_Lmodule_isNormedModule K V - of PseudoMetricNormedZmod K V & GRing.Lmodule K V := { +HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V + of PseudoMetricNormedZmod K V & Tvs K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. #[short(type="normedModType")] HB.structure Definition NormedModule (K : numDomainType) := {T of PseudoMetricNormedZmod K T & Tvs K T - & PseudoMetricNormedZmod_Lmodule_isNormedModule K T}. - -(* TODO: several factories, from a norm add-continuous, -scale_continuous and locally convex can be deduced *) - -Section regular_topology. - -Variable R : numFieldType. + & PseudoMetricNormedZmod_Tvs_isNormedModule K T}. -HB.instance Definition _ := Num.NormedZmodule.on R^o. -HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R R^o erefl. +HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numDomainType) V + of PseudoMetricNormedZmod K V & GRing.Lmodule K V := { + normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; +}. +HB.builders Context K V of PseudoMetricNormedZmod_Lmodule_isNormedModule K V. -Let Ro_add_continuous : continuous (fun x : R^o * R^o => x.1 + x.2). +Lemma add_continuous : continuous (fun x : V * V => x.1 + x.2). Proof. -(* Ugly proof -move=> [/= x y]. -apply/cvg_ballP => e e0. -rewrite /= nearE /= -nbhs_ballE /nbhs_ball /nbhs_ball_ /=. -exists ((ball x (e/2)),(ball y (e/2))). -by move=> /=; split => /=; exists (e/2) => //=; rewrite ?divr_gt0. -move => [z1 z2]; rewrite /ball /= =>- [B1 B2]. -rewrite (le_lt_trans (ler_normD _ _)) //. -rewrite (splitr e). -rewrite ltrD //. -Qed. - *) Admitted. -Let Ro_scale_continuous : - continuous (fun z : R^o * R^o => z.1 *: z.2). +Lemma scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2). +Proof. Admitted. -Let Ro_locally_convex : exists2 B : set (set R^o), - (forall b, b \in B -> convex b) & basis B. +Lemma locally_convex : exists2 B : set (set V), (forall b, b \in B -> convex b) & basis B. +Proof. Admitted. HB.instance Definition _ := - Uniform_isTvs.Build R R^o Ro_add_continuous - Ro_scale_continuous Ro_locally_convex. + Uniform_isTvs.Build K V add_continuous + scale_continuous locally_convex. HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R R^o (@normrM _). + PseudoMetricNormedZmod_Tvs_isNormedModule.Build K V normrZ. + +HB.end. + +Section regular_topology. + +Variable R : numFieldType. + +HB.instance Definition _ := Num.NormedZmodule.on R^o. +HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R R^o erefl. +HB.instance Definition _ := + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R R^o (@normrM _). End regular_topology. @@ -855,7 +850,6 @@ Variable (R : realType). HB.instance Definition _ := GRing.ComAlgebra.copy R R^o. #[export, non_forgetful_inheritance] HB.instance Definition _ := Vector.copy R R^o. - #[export, non_forgetful_inheritance] HB.instance Definition _ := NormedModule.copy R R^o. End realType. From ec83be6fd892d33513ead470858b395833783f52 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Mon, 9 Sep 2024 16:16:01 +0200 Subject: [PATCH 09/14] issue with regular --- theories/lebesgue_measure.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 803e692ce..07b555286 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -872,7 +872,7 @@ Implicit Types D : set R. Lemma oppr_measurable D : measurable_fun D -%R. Proof. apply: measurable_funTS => /=; apply: continuous_measurable_fun. -exact: opp_continuous. +exact: (@opp_continuous _ R^o). Qed. Lemma normr_measurable D : measurable_fun D (@normr _ R). From 21a47160352eb942ebb491fea07219ea7c636ec9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 12 Sep 2024 23:06:37 +0900 Subject: [PATCH 10/14] make the branch compile - move a local hint about Rhausdorff earlier in the dev - add R^o here and there --- theories/charge.v | 8 +- theories/ftc.v | 49 +++++---- theories/lebesgue_integral.v | 59 ++++++----- theories/lebesgue_measure.v | 199 ++++++++++++++++++----------------- theories/numfun.v | 2 +- theories/topology.v | 2 +- 6 files changed, 162 insertions(+), 157 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index 0e35a7dd7..60b403d79 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -700,7 +700,7 @@ have nuAoo : 0 <= nu Aoo. have A_cvg_0 : nu (A_ (v n)) @[n --> \oo] --> 0. rewrite [X in X @ _ --> _](_ : _ = (fun n => (fine (nu (A_ (v n))))%:E)); last first. by apply/funext => n/=; rewrite fineK// fin_num_measure. - apply: continuous_cvg => //; apply: cvg_series_cvg_0. + apply: continuous_cvg => //; apply: (@cvg_series_cvg_0 _ R^o). rewrite (_ : series _ = fine \o (fun n => \sum_(0 <= i < n) nu (A_ (v i)))); last first. apply/funext => n /=. by rewrite /series/= sum_fine//= => i _; rewrite fin_num_measure. @@ -831,7 +831,7 @@ have znuD n : z_ (v n) <= nu D. have max_le0 n : maxe (z_ (v n) * 2^-1%:E) (- 1%E) <= 0. by rewrite ge_max leeN10 andbT pmule_lle0. have not_s_cvg_0 : ~ (z_ \o v) n @[n --> \oo] --> 0. - move/fine_cvgP => -[zfin] /cvgrPdist_lt. + move/fine_cvgP => -[zfin] /(@cvgrPdist_lt _ R^o). have /[swap] /[apply] -[M _ hM] : (0 < `|fine (nu D)|)%R. by rewrite normr_gt0// fine_eq0// ?lt_eqF// fin_num_measure. near \oo => n. @@ -862,7 +862,7 @@ have : cvg (series (fun n => fine (maxe (z_ (v n) * 2^-1%:E) (- 1%E))) n @[n --> apply/funext => n/=; rewrite sum_fine// => m _. rewrite le0_fin_numE; first by rewrite lt_max ltNyr orbT. by rewrite /maxe; case: ifPn => // _; rewrite mule_le0_ge0. -move/cvg_series_cvg_0 => maxe_cvg_0. +move/(@cvg_series_cvg_0 _ R^o) => maxe_cvg_0. apply: not_s_cvg_0. rewrite (_ : _ \o _ = (fun n => z_ (v n) * 2^-1%:E) \* cst 2%:E); last first. by apply/funext => n/=; rewrite -muleA -EFinM mulVr ?mule1// unitfE. @@ -874,7 +874,7 @@ apply/fine_cvgP; split. rewrite sub0r normrN ltNge => maxe_lt1; rewrite fin_numE; apply/andP; split. by apply: contra maxe_lt1 => /eqP ->; rewrite max_r ?leNye//= normrN1 lexx. by rewrite lt_eqF// (@le_lt_trans _ _ 0)// mule_le0_ge0. -apply/cvgrPdist_lt => _ /posnumP[e]. +apply/(@cvgrPdist_lt _ R^o) => _ /posnumP[e]. have : (0 < minr e%:num 1)%R by rewrite lt_min// ltr01 andbT. move/cvgrPdist_lt : maxe_cvg_0 => /[apply] -[M _ hM]. near=> n; rewrite sub0r normrN. diff --git a/theories/ftc.v b/theories/ftc.v index 0f0854f4a..2911ec580 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -36,7 +36,7 @@ Local Open Scope ereal_scope. Implicit Types (f : R -> R) (a : itv_bound R). Let FTC0 f a : mu.-integrable setT (EFin \o f) -> - let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in + let F x : R^o := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in forall x, a < BRight x -> lebesgue_pt f x -> h^-1 *: (F (h + x) - F x) @[h --> (0:R)%R^'] --> f x. Proof. @@ -79,7 +79,7 @@ apply: cvg_at_right_left_dnbhs. by apply/negP; rewrite negb_and -!leNgt xz orbT. - by apply/negP; rewrite -leNgt. rewrite [f in f n @[n --> _] --> _](_ : _ = - fun n => (d n)^-1 *: fine (\int[mu]_(t in E x n) (f t)%:E)); last first. + fun n => (d n)^-1 *: (fine (\int[mu]_(t in E x n) (f t)%:E) : R^o)); last first. apply/funext => n; congr (_ *: _); rewrite -fineB/=. by rewrite /= (addrC (d n) x) ixdf. by apply: integral_fune_fin_num => //; exact: integrableS intf. @@ -106,7 +106,7 @@ apply: cvg_at_right_left_dnbhs. have nice_E y : nicely_shrinking y (E y). split=> [n|]; first exact: measurable_itv. exists (2, (fun n => PosNum (Nd_gt0 n))); split => //=. - by rewrite -oppr0; exact: cvgN. + by rewrite -oppr0; exact: (@cvgN _ R^o). move=> n z. rewrite /E/= in_itv/= /ball/= => /andP[yz zy]. by rewrite ltr_distlC opprK yz /= (le_lt_trans zy)// ltrDl. @@ -141,7 +141,7 @@ apply: cvg_at_right_left_dnbhs. rewrite /E /= !in_itv/= leNgt => xdnz. by apply/negP; rewrite negb_and xdnz. move=> b a ax. - move/cvgrPdist_le : d0. + move/(@cvgrPdist_le _ R^o) : d0. move/(_ (x - a)%R); rewrite subr_gt0 => /(_ ax)[m _ /=] h. near=> n. have mn : (m <= n)%N by near: n; exists m. @@ -170,7 +170,7 @@ apply: cvg_at_right_left_dnbhs. by apply/negP; rewrite negb_and -leNgt zxdn. suff: ((d n)^-1 * - fine (\int[mu]_(y in E x n) (f y)%:E))%R @[n --> \oo] --> f x. - apply: cvg_trans; apply: near_eq_cvg; near=> n; congr (_ *: _). + apply: cvg_trans; apply: near_eq_cvg; near=> n; congr (_ *: (_ : R^o)). rewrite /F -fineN -fineB; last 2 first. by apply: integral_fune_fin_num => //; exact: integrableS intf. by apply: integral_fune_fin_num => //; exact: integrableS intf. @@ -188,9 +188,9 @@ Unshelve. all: by end_near. Qed. (* NB: right-closed interval *) Lemma FTC1_lebesgue_pt f a : mu.-integrable setT (EFin \o f) -> - let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in + let F x : R^o := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in forall x, a < BRight x -> lebesgue_pt f x -> - derivable F x 1 /\ F^`() x = f x. + derivable (F : R^o -> R^o) x 1 /\ F^`() x = f x. Proof. move=> intf F x ax fx; split; last first. by apply/cvg_lim; [exact: Rhausdorff|exact: FTC0]. @@ -203,8 +203,8 @@ by apply/funext => y;rewrite /g /h /= [X in F (X + _)]mulr1. Qed. Corollary FTC1 f a : mu.-integrable setT (EFin \o f) -> - let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in - {ae mu, forall x, a < BRight x -> derivable F x 1 /\ F^`() x = f x}. + let F x : R^o := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in + {ae mu, forall x, a < BRight x -> derivable (F : R^o -> R^o) x 1 /\ F^`() x = f x}. Proof. move=> intf F. have /lebesgue_differentiation : locally_integrable setT f. @@ -214,8 +214,8 @@ by move=> i fi ai; apply: FTC1_lebesgue_pt => //; rewrite ltNyr. Qed. Corollary FTC1Ny f : mu.-integrable setT (EFin \o f) -> - let F x := (\int[mu]_(t in [set` `]-oo, x]]) (f t))%R in - {ae mu, forall x, derivable F x 1 /\ F^`() x = f x}. + let F x : R^o := (\int[mu]_(t in [set` `]-oo, x]]) (f t))%R in + {ae mu, forall x, derivable (F : R^o -> R^o) x 1 /\ F^`() x = f x}. Proof. move=> intf F; have := FTC1 -oo%O intf. apply: filterS; first exact: (ae_filter_ringOfSetsType mu). @@ -223,13 +223,13 @@ by move=> r /=; apply; rewrite ltNyr. Qed. Corollary continuous_FTC1 f a : mu.-integrable setT (EFin \o f) -> - let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in + let F x : R^o := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in forall x, a < BRight x -> {for x, continuous f} -> - derivable F x 1 /\ F^`() x = f x. + derivable (F : R^o -> R^o) x 1 /\ F^`() x = f x. Proof. move=> fi F x ax fx; have lfx : lebesgue_pt f x. near (0%R:R)^'+ => e; apply: (@continuous_lebesgue_pt _ _ _ (ball x e)). - - exact: ball_open_nbhs. + - exact: (@ball_open_nbhs _ R^o). - exact: measurable_ball. - by apply/measurable_funTS/EFin_measurable_fun; exact: measurable_int fi. - exact: fx. @@ -299,7 +299,7 @@ Proof. move=> ab intf; pose fab := f \_ `[a, b]. have intfab : mu.-integrable `[a, b] (EFin \o fab). by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr. -apply/cvgrPdist_le => /= e e0; rewrite near_simpl; near=> x. +apply/(@cvgrPdist_le _ R^o) => /= e e0; near=> x. rewrite {1}/int /parameterized_integral sub0r normrN. have [|xa] := leP a x. move=> ax; apply/ltW; move: ax. @@ -319,7 +319,7 @@ have /= int_normr_cont : forall e : R, 0 < e -> by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setTI. have intfab : mu.-integrable `[a, b] (EFin \o fab). by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr. -rewrite /int /parameterized_integral; apply/cvgrPdist_le => /= e e0. +rewrite /int /parameterized_integral; apply/(@cvgrPdist_le _ R^o) => /= e e0. have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0. near=> x. rewrite [in X in X - _](@itv_bndbnd_setU _ _ _ (BRight x))//; @@ -363,8 +363,7 @@ have /= int_normr_cont : forall e : R, 0 < e -> have intfab : mu.-integrable `[a, b] (EFin \o fab). by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr. rewrite /int /parameterized_integral => z; rewrite in_itv/= => /andP[az zb]. -apply/cvgrPdist_le => /= e e0. -rewrite near_simpl. +apply/(@cvgrPdist_le _ R^o) => /= e e0. have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0. near=> x. have [xz|xz|->] := ltgtP x z; last by rewrite subrr normr0 ltW. @@ -425,20 +424,20 @@ Notation mu := lebesgue_measure. Local Open Scope ereal_scope. Implicit Types (f : R -> R) (a b : R). -Corollary continuous_FTC2 f F a b : (a < b)%R -> {in `[a, b], continuous f} -> +Corollary continuous_FTC2 (f F : R^o -> R^o) a b : (a < b)%R -> {in `[a, b], continuous f} -> derivable_oo_continuous_bnd F a b -> {in `]a, b[, F^`() =1 f} -> (\int[mu]_(x in `[a, b]) (f x)%:E = (F b)%:E - (F a)%:E)%E. Proof. move=> ab cf dF F'f. pose fab := f \_ `[a, b]. -pose G x : R := (\int[mu]_(t in `[a, x]) fab t)%R. +pose G x : R^o := (\int[mu]_(t in `[a, x]) fab t)%R. have iabf : mu.-integrable `[a, b] (EFin \o f). apply: continuous_compact_integrable; first exact: segment_compact. by apply: continuous_in_subspaceT => x /[!inE] => /cf. have ifab : mu.-integrable setT (EFin \o fab). by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setTI. -have G'f : {in `]a, b[, forall x, G^`() x = fab x /\ derivable G x 1}. +have G'f : {in `]a, b[, forall x, G^`() x = fab x /\ derivable (G : R^o -> R^o) x 1}. move=> x /[!in_itv]/= /andP[ax xb]. have := @continuous_FTC1 _ _ (BLeft a) ifab x. rewrite /= lte_fin => /(_ ax). @@ -446,7 +445,7 @@ have G'f : {in `]a, b[, forall x, G^`() x = fab x /\ derivable G x 1}. have /cf xf : x \in `[a, b] by rewrite in_itv/= (ltW ax) (ltW xb). rewrite /prop_for /continuous_at {2}/fab/= patchE. rewrite mem_set ?mulr1 /=; last by rewrite in_itv/= (ltW ax) (ltW xb). - apply: cvg_trans xf; apply: near_eq_cvg; rewrite !near_simpl; near=> z. + apply: cvg_trans xf; apply: near_eq_cvg; near=> z. rewrite /fab/= patchE mem_set ?mulr1//=. near: z; have := @near_in_itv R a b x. rewrite in_itv/= ax xb => /(_ isT). @@ -469,11 +468,11 @@ have [k FGk] : exists k : R, {in `]a, b[, (F - G =1 cst k)%R}. + by move: yab; rewrite in_itv/= => /andP[_ /ltW]. have Fz1 : derivable F z 1. by case: dF => /= + _ _; apply; rewrite inE in zab. - have Gz1 : derivable G z 1 by have [|] := G'f z. + have Gz1 : derivable (G : R^o -> R^o) z 1 by have [|] := G'f z. apply: DeriveDef. + by apply: derivableB; [exact: Fz1|exact: Gz1]. + by rewrite deriveB -?derive1E; [by []|exact: Fz1|exact: Gz1]. - - apply: derivable_within_continuous => z zxy. + - apply: (@derivable_within_continuous _ R^o) => z zxy. apply: derivableB. + case: dF => /= + _ _; apply. rewrite in_itv/=; move: zxy; rewrite in_itv/= => /andP[xz zy]. @@ -519,7 +518,7 @@ have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R. have contF : {within `[a, b], continuous F}. apply/(continuous_within_itvP _ ab); split; last exact: (conj Fa Fb). move=> z zab. - apply/differentiable_continuous/derivable1_diffP. + apply/(@differentiable_continuous _ R^o R^o)/derivable1_diffP. by case: dF => /= dF _ _; apply: dF. have iabfab : mu.-integrable `[a, b] (EFin \o fab). by rewrite -restrict_EFin; apply/integrable_restrict => //; rewrite setIidr. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index d9a4fb154..cdbd7a50c 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -441,7 +441,7 @@ Qed. Section simple_bounded. Context d (T : sigmaRingType d) (R : realType). -Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun f. +Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun (f : _ -> R^o). Proof. have /finite_seqP[r fr] := fimfunP f. exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)). @@ -1671,7 +1671,6 @@ Qed. End approximation_sfun. Section lusin. -Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff ) : core. Local Open Scope ereal_scope. Context (rT : realType) (A : set rT). Let mu := [the measure _ _ of @lebesgue_measure rT]. @@ -3098,7 +3097,7 @@ case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //. - by move=> x Dx; rewrite -/((abse \o f) x) (fune_abse f) leeDl. Qed. -Lemma integrableMr (h : T -> R) g : +Lemma integrableMr (h : T -> R^o) g : measurable_fun D h -> [bounded h x | x in D] -> mu_int g -> mu_int ((EFin \o h) \* g). Proof. @@ -3118,7 +3117,7 @@ apply/le_lt_trans/ge0_le_integral => //. by rewrite (lt_le_trans _ (ler_norm _))// ltrDl. Qed. -Lemma integrableMl f (h : T -> R) : +Lemma integrableMl f (h : T -> R^o) : mu_int f -> measurable_fun D h -> [bounded h x | x in D] -> mu_int (f \* (EFin \o h)). Proof. @@ -5731,7 +5730,7 @@ Let R := [the measurableType _ of measurableTypeR rT]. Let ballE (x : R) (r : {posnum rT}) : ball x r%:num = `](x - r%:num), (x + r%:num)[%classic :> set rT. Proof. -rewrite -ball_normE /ball_ set_itvoo. +rewrite -(@ball_normE _ rT^o) /ball_ set_itvoo. by under eq_set => ? do rewrite ltr_distlC. Qed. @@ -5755,7 +5754,7 @@ have ritv r : 0 < r -> mu `[x - r, x + r]%classic = (r *+ 2)%:E. rewrite ler_ltD // ?rE // -EFinD; congr (_ _). by rewrite opprB addrAC [_ - _]addrC addrA subrr add0r. move=> oA intf ctsfx Ax. -apply: cvg_zero. +apply: (@cvg_zero _ R^o). apply/cvgrPdist_le => eps epos; apply: filter_app (@nbhs_right_gt rT 0). move/cvgrPdist_le/(_ eps epos)/at_right_in_segment : ctsfx; apply: filter_app. apply: filter_app (open_itvcc_subset oA Ax). @@ -5981,7 +5980,7 @@ move: a0; rewrite le_eqVlt => /predU1P[a0|a0]. rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW. by rewrite ltry andbT lte_fin pmulrn_lgt0// addr_gt0. exists (ball x d). - by split; [exact: ball_open|exact: ballxx]. + by split; [exact: (@ball_open _ R^o)|exact: ballxx]. move=> y; rewrite /ball/= => xyd. have ? : ball x r `<=` ball y (r + d). move=> /= z; rewrite /ball/= => xzr; rewrite -(subrK x y) -(addrA (y - x)%R). @@ -6019,7 +6018,7 @@ have axrdk : a%:E < (fine (mu (ball x (r + d))))^-1%:E * k. rewrite -mulr_natl -ltr_pdivlMl// -ltrBrDl. by near: d; exact: nbhs_right_lt. exists (ball x d). - by split; [exact: ball_open|exact: ballxx]. + by split; [exact: (@ball_open _ R^o)|exact: ballxx]. move=> y; rewrite /ball/= => xyd. have ? : ball x r `<=` ball y (r + d). move=> /= z; rewrite /ball/= => xzr; rewrite -(subrK x y) -(addrA (y - x)%R). @@ -6081,7 +6080,7 @@ have {}Kcmf : K `<=` cover [set i | HL f i > c%:E] (fun i => ball i (r_ i)). have {Kcmf}[D Dsub Kcover] : finite_subset_cover [set i | c%:E < HL f i] (fun i => ball i (r_ i)) K. move: cK; rewrite compact_cover => /(_ _ _ _ _ Kcmf); apply. - by move=> /= x cMfx; exact/ball_open/r_pos. + by move=> /= x cMfx; exact/(@ball_open _ R^o)/r_pos. have KDB : K `<=` cover [set` D] B. by apply: (subset_trans Kcover) => /= x [r Dr] rx; exists r. have is_ballB i : is_ball (B i) by exact: is_ball_ball. @@ -6152,14 +6151,16 @@ Let continuous_integralB_fin_num : \forall t \near (0:R)%R, \int[mu]_(y in ball x t) `|(f y)%:E - (f x)%:E| \is a fin_num. Proof. -move: fx => /cvgrPdist_le /= fx'. +move: fx => /(@cvgrPdist_le _ R^o) /= fx'. near (0%R:R)^'+ => e. have e0 : (0 < e)%R by near: e; exact: nbhs_right_gt. have [r /= r0 {}fx'] := fx' _ e0. -have [d/= d0 dxU] := open_subball xU.1 xU.2. +have [d/= d0 dxU] := @open_subball _ R^o _ _ xU.1 xU.2. near=> t; rewrite ge0_fin_numE ?integral_ge0//. have [t0|t0] := leP t 0%R; first by rewrite ((ball0 _ _).2 t0) integral_set0. -have xtU : ball x t `<=` U by apply: dxU => //=. +have xtU : ball x t `<=` U. + apply: dxU => //=. + by rewrite /ball_ /= sub0r normrN; near: t; exact: (@nbhs0_lt _ R^o). rewrite (@le_lt_trans _ _ (\int[mu]_(y in ball x t) e%:E))//; last first. rewrite integral_cst//=; last exact: measurable_ball. by rewrite (lebesgue_measure_ball _ (ltW t0)) ltry. @@ -6175,33 +6176,37 @@ Let continuous_davg_fin_num : \forall A \near (0:R)%R, davg f x A \is a fin_num. Proof. have [e /= e0 exf] := continuous_integralB_fin_num. -move: fx => /cvgrPdist_le fx'. +move: fx => /(@cvgrPdist_le _ R^o) fx'. near (0%R:R)^'+ => r. have r0 : (0 < r)%R by near: r; exact: nbhs_right_gt. have [d /= d0 {}fx'] := fx' _ e0. near=> t; have [t0|t0] := leP t 0%R; first by rewrite davg0. -by rewrite fin_numM// exf/=. +rewrite fin_numM// exf//=. +by rewrite /ball_ /= sub0r normrN; near: t; exact: (@nbhs0_lt _ R^o). Unshelve. all: by end_near. Qed. Lemma continuous_cvg_davg : davg f x r @[r --> (0:R)%R] --> 0. Proof. apply/fine_cvgP; split; first exact: continuous_davg_fin_num. -apply/cvgrPdist_le => e e0. -move: fx => /cvgrPdist_le /= fx'. +apply/(@cvgrPdist_le _ R^o) => e e0. +move: fx => /(@cvgrPdist_le _ R^o) /= fx'. have [r /= r0 {}fx'] := fx' _ e0. have [d /= d0 dfx] := continuous_davg_fin_num. -have [l/= l0 lxU] := open_subball xU.1 xU.2. +have [l/= l0 lxU] := @open_subball _ R^o _ _ xU.1 xU.2. near=> t. have [t0|t0] := leP t 0%R; first by rewrite /= davg0//= subrr normr0 ltW. rewrite sub0r normrN /= ger0_norm; last by rewrite fine_ge0// davg_ge0. -rewrite -lee_fin fineK//; last by rewrite dfx//= sub0r normrN gtr0_norm. +rewrite -lee_fin fineK//; last first. + rewrite dfx//=. + by rewrite /ball_ /= sub0r normrN; near: t; exact: (@nbhs0_lt _ R^o). rewrite /davg/= /iavg/= lee_pdivrMl//; last first. by rewrite fine_gt0// lebesgue_measure_ball// ?ltry ?lte_fin ?mulrn_wgt0 ?ltW. rewrite (@le_trans _ _ (\int[mu]_(y in ball x t) e%:E))//. apply: ge0_le_integral => //=. - exact: measurable_ball. - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //. - by apply: measurable_funS mUf => //; apply: lxU => //=. + apply: measurable_funS mUf => //; apply: lxU => //=. + by rewrite /ball_ /= sub0r normrN; near: t; exact: (@nbhs0_lt _ R^o). - by move=> y xty; rewrite lee_fin ltW. - move=> y xty; rewrite lee_fin distrC fx'//; apply: (lt_le_trans xty). by near: t; exact: nbhs0_ltW. @@ -6231,7 +6236,7 @@ Lemma lim_sup_davg_le f g x (U : set R) : open_nbhs x U -> measurable U -> Proof. move=> xU mY mf /= mg; apply: le_trans (lime_supD _); last first. by rewrite ge0_adde_def// inE; exact: lim_sup_davg_ge0. -have [e/= e0 exU] := open_subball xU.1 xU.2. +have [e/= e0 exU] := @open_subball _ R^o _ _ xU.1 xU.2. apply: lime_sup_le; near=> r => y; rewrite neq_lt => /orP[y0|y0 ry]. by rewrite !davg0 ?adde0// ltW. apply: davgD. @@ -6261,7 +6266,7 @@ move=> xU mU mUf cg locg; apply/eqP; rewrite eq_le; apply/andP; split. rewrite (@continuous_lim_sup_davg (- g)%R _ _ xU mU); first by rewrite adde0. - apply/(measurable_comp measurableT) => //. by case: locg => + _ _; apply: measurable_funS. - + by move=> y; exact/continuousN/cg. + + by move=> y; exact/(@continuousN _ R^o)/cg. - rewrite [leRHS](_ : _ = ((f \- g)%R^* \+ g^*) x)//. rewrite {1}(_ : f = f \- g + g)%R; last by apply/funext => y; rewrite subrK. apply: (lim_sup_davg_le xU mU). @@ -6275,7 +6280,7 @@ Qed. Local Notation mu := (@lebesgue_measure R). Let is_cvg_ereal_sup_davg f x : - cvg (ereal_sup [set davg f x y | y in ball 0%R e `\ 0%R] @[e --> 0^'+]). + cvg (ereal_sup [set davg f x y | y in @ball _ R^o 0%R e `\ 0%R] @[e --> 0^'+]). Proof. apply: nondecreasing_at_right_is_cvge; near=> e => y z. rewrite !in_itv/= => /andP[y0 ye] /andP[z0 ze] yz. @@ -6523,7 +6528,7 @@ have {ex_g_} ex_gn n : exists gn : R -> R, [/\ continuous gn, mu.-integrable (B k) (EFin \o gn) & \int[mu]_(z in B k) `|f_ k z - gn z|%:E <= n.+1%:R^-1%:E]. - case: ex_g_ => g_ [cg intg] /fine_cvgP[] [m _ fgfin] /cvgrPdist_le. + case: ex_g_ => g_ [cg intg] /fine_cvgP[] [m _ fgfin] /(@cvgrPdist_le _ R^o). move=> /(_ n.+1%:R^-1 ltac:(by []))[p _] /(_ _ (leq_addr m p)). rewrite sub0r normrN -lee_fin => /= fg0. exists (g_ (p + m)%N); split => //. @@ -6591,11 +6596,11 @@ have davgfEe : B k `&` [set x | (f_ k)^* x > e%:E] `<=` Ee. B k `&` [set x | e%:E < (f_ k \- g_B n)%R^* x]); last first. apply/seteqP; split => [x [Ex] /=|x [Ex] /=]. rewrite (@lim_sup_davgB _ _ _ _ (B k))//. - by split; [exact: ball_open|exact: Ex]. + by split; [exact: (@ball_open _ R^o)|exact: Ex]. by move/EFin_measurable_fun : mf; apply: measurable_funS. by apply: cg_B; rewrite inE. rewrite (@lim_sup_davgB _ _ _ _ (B k))//. - by split; [exact: ball_open|exact: Ex]. + by split; [exact: (@ball_open _ R^o)|exact: Ex]. by move/EFin_measurable_fun : mf; apply: measurable_funS. by apply: cg_B; rewrite inE. move=> r /= [Er] efgnr; split => //. @@ -6677,7 +6682,7 @@ suff: ~` [set x | lebesgue_pt f x] `<=` by apply: negligible_bigcup => k /=; exact: suf. move=> x /= fx; rewrite -setC_bigcap => h; apply: fx. have fE y k r : (ball 0%R k.+1%:R) y -> (r < 1)%R -> - forall t, ball y r t -> f t = fk k t. + forall t : R^o, ball y r t -> f t = fk k t. rewrite /ball/= sub0r normrN => yk1 r1 t. rewrite ltr_distlC => /andP[xrt txr]. rewrite /fk patchE mem_set// /B /ball/= sub0r normrN. @@ -6709,7 +6714,7 @@ apply/fine_cvgP; split=> [{davg_fk0}|{davg_fk_fin_num}]. - move: davg_fk_fin_num => -[M /= M0] davg_fk_fin_num. apply: filter_app f_fk_ceil; near=> t => Ht. by rewrite /davg /iavg Ht davg_fk_fin_num//= sub0r normrN gtr0_norm. -- move/cvgrPdist_le in davg_fk0; apply/cvgrPdist_le => e e0. +- move/(@cvgrPdist_le _ R^o) in davg_fk0; apply/(@cvgrPdist_le _ R^o) => e e0. have [M /= M0 {}davg_fk0] := davg_fk0 _ e0. apply: filter_app f_fk_ceil; near=> t; move=> Ht. by rewrite /davg /iavg Ht// davg_fk0//= sub0r normrN gtr0_norm. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 07b555286..04a44d656 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1063,8 +1063,8 @@ move=> mf_ f_f; have fE x : D x -> f x = limn_sup (h ^~ x). apply: (@eq_measurable_fun _ _ _ _ D (fun x => limn_sup (h ^~ x))). by move=> x; rewrite inE => Dx; rewrite -fE. apply: (@measurable_fun_limn_sup _ h) => // t Dt. -- by apply/bounded_fun_has_ubound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f. -- by apply/bounded_fun_has_lbound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f. +- by apply/bounded_fun_has_ubound/(@cvg_seq_bounded _ R^o)/cvg_ex; eexists; exact: f_f. +- by apply/bounded_fun_has_lbound/(@cvg_seq_bounded _ R^o)/cvg_ex; eexists; exact: f_f. Qed. Lemma measurable_fun_indic D (U : set T) : measurable U -> @@ -1586,100 +1586,6 @@ Qed. End open_itv_cover. -Section egorov. -Context d {R : realType} {T : measurableType d}. -Context (mu : {measure set T -> \bar R}). - -Local Open Scope ereal_scope. - -(*TODO : this generalizes to any metric space with a borel measure*) -Lemma pointwise_almost_uniform - (f : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) : - (forall n, measurable_fun A (f n)) -> - measurable A -> mu A < +oo -> (forall x, A x -> f ^~ x @ \oo --> g x) -> - (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E & - {uniform A `\` B, f @ \oo --> g}]. -Proof. -move=> mf mA finA fptwsg epspos; pose h q (z : T) : R := `|f q z - g z|%R. -have mfunh q : measurable_fun A (h q). - apply: measurableT_comp => //; apply: measurable_funB => //. - exact: measurable_fun_cvg. -pose E k n := \bigcup_(i >= n) (A `&` [set x | h i x >= k.+1%:R^-1]%R). -have Einc k : nonincreasing_seq (E k). - move=> n m nm; apply/asboolP => z [i] /= /(leq_trans _) mi [? ?]. - by exists i => //; exact: mi. -have mE k n : measurable (E k n). - apply: bigcup_measurable => q /= ?. - have -> : [set x | h q x >= k.+1%:R^-1]%R = h q @^-1` `[k.+1%:R^-1, +oo[. - by rewrite eqEsubset; split => z; rewrite /= in_itv /= andbT. - exact: mfunh. -have nEcvg x k : exists n, A x -> (~` E k n) x. - have [Ax|?] := pselect (A x); last by exists point. - have [] := fptwsg _ Ax (interior (ball (g x) k.+1%:R^-1)). - by apply: open_nbhs_nbhs; split; [exact: open_interior|exact: nbhsx_ballx]. - move=> N _ Nk; exists N.+1 => _; rewrite /E setC_bigcup => i /= /ltnW Ni. - apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC. - by case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center. -have Ek0 k : \bigcap_n (E k n) = set0. - rewrite eqEsubset; split => // z /=; suff : (~` \bigcap_n E k n) z by []. - rewrite setC_bigcap; have [Az | nAz] := pselect (A z). - by have [N /(_ Az) ?] := nEcvg z k; exists N. - by exists 0%N => //; rewrite setC_bigcup => n _ []. -have badn' k : exists n, mu (E k n) < ((eps / 2) / (2 ^ k.+1)%:R)%:E. - pose ek : R := eps / 2 / (2 ^ k.+1)%:R. - have : mu \o E k @ \oo --> mu set0. - rewrite -(Ek0 k); apply: nonincreasing_cvg_mu => //. - - by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []]. - - exact: bigcap_measurable. - rewrite measure0; case/fine_cvg/(_ (interior (ball 0%R ek))). - apply/open_nbhs_nbhs/(open_nbhs_ball _ (@PosNum _ ek _)). - by rewrite !divr_gt0. - move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN. - rewrite /ball /= distrC subr0 ger0_norm // -[x in x < _]fineK ?ge0_fin_numE//. - by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []]. -pose badn k := projT1 (cid (badn' k)); exists (\bigcup_k E k (badn k)); split. -- exact: bigcup_measurable. -- apply: (@le_lt_trans _ _ (eps / 2)%:E); first last. - by rewrite lte_fin ltr_pdivrMr // ltr_pMr // Rint_ltr_addr1 // Rint1. - apply: le_trans. - apply: (measure_sigma_subadditive _ (fun k => mE k (badn k)) _ _) => //. - exact: bigcup_measurable. - apply: le_trans; first last. - by apply: (epsilon_trick0 xpredT); rewrite divr_ge0// ltW. - by rewrite lee_nneseries // => n _; exact/ltW/(projT2 (cid (badn' _))). -apply/uniform_restrict_cvg => /= U /=; rewrite !uniform_nbhsT. -case/nbhs_ex => del /= ballU; apply: filterS; first by move=> ?; exact: ballU. -have [N _ /(_ N)/(_ (leqnn _)) Ndel] := near_infty_natSinv_lt del. -exists (badn N) => // r badNr x. -rewrite /patch; case: ifPn => // /set_mem xAB; apply: (lt_trans _ Ndel). -move: xAB; rewrite setDE => -[Ax]; rewrite setC_bigcup => /(_ N I). -rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP[]//. -by move/negP; rewrite ltNge // distrC. -Qed. - -Lemma ae_pointwise_almost_uniform - (f : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) : - (forall n, measurable_fun A (f n)) -> measurable_fun A g -> - measurable A -> mu A < +oo -> - {ae mu, (forall x, A x -> f ^~ x @ \oo --> g x)} -> - (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E & - {uniform A `\` B, f @ \oo --> g}]. -Proof. -move=> mf mg mA Afin [C [mC C0 nC] epspos]. -have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E & - {uniform (A `\` C) `\` B, f @ \oo --> g}]. - apply: pointwise_almost_uniform => //. - - by move=> n; apply : (measurable_funS mA _ (mf n)) => ? []. - - by apply: measurableI => //; exact: measurableC. - - by rewrite (le_lt_trans _ Afin)// le_measure// inE//; exact: measurableD. - - by move=> x; rewrite setDE; case => Ax /(subsetC nC); rewrite setCK; exact. -exists (B `|` C); split. -- exact: measurableU. -- by apply: (le_lt_trans _ Beps); rewrite measureU0. -- by rewrite setUC -setDDl. -Qed. - -End egorov. (* This module contains a direct construction of the Lebesgue measure that is kept here for archival purpose. The Lebesgue measure is actually defined as @@ -2700,6 +2606,101 @@ Qed. End lebesgue_regularity. +Section egorov. +Context d {R : realType} {T : measurableType d}. +Context (mu : {measure set T -> \bar R}). + +Local Open Scope ereal_scope. + +(*TODO : this generalizes to any metric space with a borel measure*) +Lemma pointwise_almost_uniform + (f : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) : + (forall n, measurable_fun A (f n)) -> + measurable A -> mu A < +oo -> (forall x, A x -> f ^~ x @ \oo --> g x) -> + (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E & + {uniform A `\` B, f @ \oo --> g}]. +Proof. +move=> mf mA finA fptwsg epspos; pose h q (z : T) : R := `|f q z - g z|%R. +have mfunh q : measurable_fun A (h q). + apply: measurableT_comp => //; apply: measurable_funB => //. + exact: measurable_fun_cvg. +pose E k n := \bigcup_(i >= n) (A `&` [set x | h i x >= k.+1%:R^-1]%R). +have Einc k : nonincreasing_seq (E k). + move=> n m nm; apply/asboolP => z [i] /= /(leq_trans _) mi [? ?]. + by exists i => //; exact: mi. +have mE k n : measurable (E k n). + apply: bigcup_measurable => q /= ?. + have -> : [set x | h q x >= k.+1%:R^-1]%R = h q @^-1` `[k.+1%:R^-1, +oo[. + by rewrite eqEsubset; split => z; rewrite /= in_itv /= andbT. + exact: mfunh. +have nEcvg x k : exists n, A x -> (~` E k n) x. + have [Ax|?] := pselect (A x); last by exists point. + have [] := fptwsg _ Ax (interior (ball (g x) k.+1%:R^-1)). + by apply: open_nbhs_nbhs; split; [exact: open_interior|exact: nbhsx_ballx]. + move=> N _ Nk; exists N.+1 => _; rewrite /E setC_bigcup => i /= /ltnW Ni. + apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC. + by case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center. +have Ek0 k : \bigcap_n (E k n) = set0. + rewrite eqEsubset; split => // z /=; suff : (~` \bigcap_n E k n) z by []. + rewrite setC_bigcap; have [Az | nAz] := pselect (A z). + by have [N /(_ Az) ?] := nEcvg z k; exists N. + by exists 0%N => //; rewrite setC_bigcup => n _ []. +have badn' k : exists n, mu (E k n) < ((eps / 2) / (2 ^ k.+1)%:R)%:E. + pose ek : R := eps / 2 / (2 ^ k.+1)%:R. + have : mu \o E k @ \oo --> mu set0. + rewrite -(Ek0 k); apply: nonincreasing_cvg_mu => //. + - by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []]. + - exact: bigcap_measurable. + rewrite measure0; case/fine_cvg/(_ (@interior R^o (ball 0%R ek))). + apply/open_nbhs_nbhs/(open_nbhs_ball _ (@PosNum _ ek _)). + by rewrite !divr_gt0. + move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN. + rewrite /ball /= distrC subr0 ger0_norm // -[x in x < _]fineK ?ge0_fin_numE//. + by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []]. +pose badn k := projT1 (cid (badn' k)); exists (\bigcup_k E k (badn k)); split. +- exact: bigcup_measurable. +- apply: (@le_lt_trans _ _ (eps / 2)%:E); first last. + by rewrite lte_fin ltr_pdivrMr // ltr_pMr // Rint_ltr_addr1 // Rint1. + apply: le_trans. + apply: (measure_sigma_subadditive _ (fun k => mE k (badn k)) _ _) => //. + exact: bigcup_measurable. + apply: le_trans; first last. + by apply: (epsilon_trick0 xpredT); rewrite divr_ge0// ltW. + by rewrite lee_nneseries // => n _; exact/ltW/(projT2 (cid (badn' _))). +apply/uniform_restrict_cvg => /= U /=; rewrite !uniform_nbhsT. +case/nbhs_ex => del /= ballU; apply: filterS; first by move=> ?; exact: ballU. +have [N _ /(_ N)/(_ (leqnn _)) Ndel] := near_infty_natSinv_lt del. +exists (badn N) => // r badNr x. +rewrite /patch; case: ifPn => // /set_mem xAB; apply: (lt_trans _ Ndel). +move: xAB; rewrite setDE => -[Ax]; rewrite setC_bigcup => /(_ N I). +rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP[]//. +by move/negP; rewrite ltNge // distrC. +Qed. + +Lemma ae_pointwise_almost_uniform + (f : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) : + (forall n, measurable_fun A (f n)) -> measurable_fun A g -> + measurable A -> mu A < +oo -> + {ae mu, (forall x, A x -> f ^~ x @ \oo --> g x)} -> + (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E & + {uniform A `\` B, f @ \oo --> g}]. +Proof. +move=> mf mg mA Afin [C [mC C0 nC] epspos]. +have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E & + {uniform (A `\` C) `\` B, f @\oo --> g}]. + apply: pointwise_almost_uniform => //. + - by move=> n; apply : (measurable_funS mA _ (mf n)) => ? []. + - by apply: measurableI => //; exact: measurableC. + - by rewrite (le_lt_trans _ Afin)// le_measure// inE//; exact: measurableD. + - by move=> x; rewrite setDE; case => Ax /(subsetC nC); rewrite setCK; exact. +exists (B `|` C); split. +- exact: measurableU. +- by apply: (le_lt_trans _ Beps); rewrite measureU0. +- by rewrite setUC -setDDl. +Qed. + +End egorov. + Definition vitali_cover {R : realType} (E : set R) I (B : I -> set R) (D : set I) := (forall i, is_ball (B i)) /\ @@ -2858,7 +2859,7 @@ have [N F5e] : exists N, \sum_(N <= n // x []. have : \sum_(N <= k \oo] --> 0. exact: nneseries_tail_cvg. - rewrite /f /= => /fine_fcvg /= /cvgrPdist_lt /=. + rewrite /f /= => /fine_fcvg /= /(@cvgrPdist_lt _ R^o) /=. have : (0 < 5%:R^-1 * e%:num)%R by rewrite mulr_gt0// invr_gt0// ltr0n. move=> /[swap] /[apply]. rewrite near_map => -[N _]/(_ _ (leqnn N)) h; exists N; move: h. @@ -2889,7 +2890,7 @@ have ZNF5 : Z r%:num `<=` case: Zz => -[Az notDBz]; rewrite /ball/= sub0r normrN => rz. have [d dzr zdK0] : exists2 d : {posnum R}, (d%:num < r%:num - `|z|)%R & closed_ball z d%:num `&` K = set0. - have [d/= d0 dzK] := closed_disjoint_closed_ball closedK Kz. + have [d/= d0 dzK] := @closed_disjoint_closed_ball _ R^o _ _ closedK Kz. have rz0 : (0 < minr ((r%:num - `|z|) / 2) (d / 2))%R. by rewrite lt_min (divr_gt0 d0)//= andbT divr_gt0// subr_gt0. exists (PosNum rz0) => /=. @@ -2914,7 +2915,7 @@ have ZNF5 : Z r%:num `<=` by rewrite (le_trans (ltW (is_ballP (is_ballB i) Biz)))// ltW. by move: dzr; rewrite -ltrBrDr. apply: subsetI_eq0 zdK0 => // y Biy. - rewrite closed_ballE//= /closed_ball_/=. + rewrite (@closed_ballE _ R^o)//= /closed_ball_/=. rewrite -(@subrK _ (cpoint (B i)) z) -(addrA (z - _)%R). rewrite (le_trans (ler_normD _ _))// [in leRHS](splitr d%:num) lerD//. by rewrite distrC (le_trans (ltW (is_ballP (is_ballB i) Biz)))// ltW. diff --git a/theories/numfun.v b/theories/numfun.v index ce6d63bab..dcea8ce52 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -620,7 +620,7 @@ exists (lim (h_ @ \oo)); split. by move=> n; rewrite mulr_ge0. rewrite (le_trans (lim_series_norm _))//; apply: le_trans. exact/(lim_series_le cvg_gt _ (g_bd ^~ t))/is_cvg_geometric_series. - rewrite (cvg_lim _ (cvg_geometric_series _))//; last exact: Rhausdorff. + rewrite (cvg_lim _ (cvg_geometric_series _))//. by rewrite onem_twothirds mulrAC divrr ?mul1r// unitfE. Unshelve. all: by end_near. Qed. diff --git a/theories/topology.v b/theories/topology.v index f0963715e..647802683 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -5602,7 +5602,7 @@ have := ball_triangle yz_he (ball_sym zx_he). by rewrite -mulr2n -(mulr_natr (_ / _) 2) divfK// => /ltW. Qed. - +Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff ) : core. Definition dense (T : topologicalType) (S : set T) := forall (O : set T), O !=set0 -> open O -> O `&` S !=set0. From e315abb1b655a5da17245d5d85922315049a0fbd Mon Sep 17 00:00:00 2001 From: mkerjean Date: Tue, 10 Sep 2024 17:11:25 +0200 Subject: [PATCH 11/14] prod tvs and convex --- theories/tvs.v | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/theories/tvs.v b/theories/tvs.v index 02ac05bcf..305e0b298 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -39,8 +39,9 @@ HB.structure Definition UniformLmodule (K : numDomainType) := {M of Uniform M & GRing.Lmodule K M}. -Definition convex (R : ringType) (M : lmodType R) (A : set M) := - forall x y lambda, lambda *: x + (1 - lambda) *: y \in A. +Definition convex (R : numDomainType) (M : lmodType R) (A : set M) := + forall x y (lambda : R), x \in A -> y \in A -> + (`|lambda| < 1) -> lambda *: x + (1 - lambda) *: y \in A. HB.mixin Record Uniform_isTvs (R : numDomainType) E of Uniform E & GRing.Lmodule R E := { add_continuous : continuous (fun x : E * E => x.1 + x.2) ; @@ -215,6 +216,27 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E nbhsE_subproof. HB.end. +Section prod_Tvs. +Context (K : numDomainType) (U V : tvsType K). + +Lemma prod_add_continuous : continuous (fun x : (U * V) * (U * V) => x.1 + x.2). +Proof. +Admitted. + +Lemma prod_scale_continuous : continuous (fun z : K^o * (U * V) => z.1 *: z.2). +Proof. +Admitted. + +Lemma prod_locally_convex : +exists2 B : set (set (U * V)), (forall b, b \in B -> convex b) & basis B. +Proof. +Admitted. + +HB.instance Definition _ := + Uniform_isTvs.Build K (U * V)%type +prod_add_continuous prod_scale_continuous prod_locally_convex. +End prod_Tvs. + Section FirstLemmas. From aad0c502bbfa26610bb2af45ad7a7e4517bde3e0 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Tue, 10 Sep 2024 17:11:43 +0200 Subject: [PATCH 12/14] Factory on numfieldtype --- theories/normedtype.v | 50 ++++++++++++++++++++++++++++++++++++++----- 1 file changed, 45 insertions(+), 5 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index c6b34029b..e90b2e3e4 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -784,7 +784,7 @@ Lemma cvgenyP {R : realType} {T} {F : set_system T} {FF : Filter F} (f : T -> na (((f n)%:R : R)%:E @[n --> F] --> +oo%E) <-> (f @ F --> \oo). Proof. by rewrite cvgeryP cvgrnyP. Qed. -(** Modules with a norm *) +(** Modules with a norm depending on a numDomain*) HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V of PseudoMetricNormedZmod K V & Tvs K V := { @@ -796,23 +796,63 @@ HB.structure Definition NormedModule (K : numDomainType) := {T of PseudoMetricNormedZmod K T & Tvs K T & PseudoMetricNormedZmod_Tvs_isNormedModule K T}. -HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numDomainType) V + + +HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldType) V of PseudoMetricNormedZmod K V & GRing.Lmodule K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. HB.builders Context K V of PseudoMetricNormedZmod_Lmodule_isNormedModule K V. - +(* These lemmas are done latter with more machinery. Move the factory ?*) Lemma add_continuous : continuous (fun x : V * V => x.1 + x.2). Proof. -Admitted. +move=> [/= x y]; apply/cvg_ballP => e e0 /=. +rewrite nearE /= -nbhs_ballE /nbhs_ball /nbhs_ball_ //=. +exists ((ball x (e/2)),(ball y (e/2))). +rewrite !nbhs_simpl /=; split; by apply: nbhsx_ballx; rewrite ?divr_gt0. +rewrite -ball_normE /= /ball_ /= => xy /= [nx ny]. +rewrite opprD addrACA (le_lt_trans (ler_normD _ _)) // (@splitr K (e)) ltrD //=. +Qed. Lemma scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2). Proof. +move=> [/= k x]; apply/cvg_ballP => e e0 /=. +rewrite nearE /= -nbhs_ballE /nbhs_ball /nbhs_ball_ //=. +near +oo_K => M. +pose r := (e/2/M). +exists ((ball k r),(ball x r)). +rewrite !nbhs_simpl /=; split; by apply: nbhsx_ballx; rewrite ?divr_gt0. +rewrite -ball_normE /= /ball_ /= => lz /= [nk nx]. +rewrite -?(scalerBr, scalerBl). +have := @ball_split _ _ (k *: lz.2) (k*: x) (lz.1 *: lz.2) e; rewrite -ball_normE /=. +move => T; apply: T; rewrite -?(scalerBr, scalerBl) normrZ. + by rewrite (@le_lt_trans _ _ (M * `|x - lz.2|)) ?ler_wpM2r -?ltr_pdivlMl// mulrC. +rewrite (@le_lt_trans _ _ (`|k - lz.1| * M)) ?ler_wpM2l -?ltr_pdivlMr//. + near: M. admit. +Unshelve. all: by end_near. Admitted. Lemma locally_convex : exists2 B : set (set V), (forall b, b \in B -> convex b) & basis B. Proof. +exists [set B | exists x, exists r, B = ball x r]. + move=> b; rewrite inE /= => [[x]] [r] -> z y l. + rewrite !inE -!ball_normE /= => zx zy l1. + rewrite opprD scalerDl opprD. + rewrite scale1r [X in (_ + X)]addrC addrA [X in (X - _)]addrA. + rewrite scaleNr opprK -addrA. admit. +split => /=. + move => B [x] [r] ->. + rewrite openE -!ball_normE /interior=> y /= bxy. + rewrite -nbhs_ballE /nbhs_ball /nbhs_ball_ /filter_from //=. + exists (r - (normr (x - y) )); first by rewrite subr_gt0. + move=> z. rewrite -ball_normE /= ltrBrDr addrC => H. + rewrite /= (le_lt_trans (ler_distD y _ _)) //. +rewrite /filter_from /= => x B. +rewrite -nbhs_ballE /nbhs_ball /nbhs_ball_ /filter_from //=. +move=> [r] r0 Bxr /=. +rewrite nbhs_simpl /=; exists (ball x r) => //; split; last by apply: ballxx. +by exists x; exists r. Admitted. HB.instance Definition _ := @@ -2380,7 +2420,7 @@ Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |. Proof. by rewrite prod_normE /= !normrZ maxr_pMr. Qed. HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K (U * V)%type + PseudoMetricNormedZmod_Tvs_isNormedModule.Build K (U * V)%type prod_norm_scale. End prod_NormedModule. From 0f185fd602317e7850548aa9c6510d808e47dccb Mon Sep 17 00:00:00 2001 From: mkerjean Date: Tue, 10 Sep 2024 23:10:25 +0200 Subject: [PATCH 13/14] proofs --- theories/normedtype.v | 71 ++++++++++++++++++++++++++++++++----------- 1 file changed, 53 insertions(+), 18 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index e90b2e3e4..110cc14ca 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -804,7 +804,9 @@ HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldTyp }. HB.builders Context K V of PseudoMetricNormedZmod_Lmodule_isNormedModule K V. -(* These lemmas are done latter with more machinery. Move the factory ?*) + + +(* These lemmas are done latter with more machinery. Can we move this factory down ?*) Lemma add_continuous : continuous (fun x : V * V => x.1 + x.2). Proof. move=> [/= x y]; apply/cvg_ballP => e e0 /=. @@ -814,33 +816,66 @@ rewrite !nbhs_simpl /=; split; by apply: nbhsx_ballx; rewrite ?divr_gt0. rewrite -ball_normE /= /ball_ /= => xy /= [nx ny]. rewrite opprD addrACA (le_lt_trans (ler_normD _ _)) // (@splitr K (e)) ltrD //=. Qed. - + Lemma scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2). Proof. -move=> [/= k x]; apply/cvg_ballP => e e0 /=. +move=> [/= k x]. +apply/cvg_ballP => e e0 /=. rewrite nearE /= -nbhs_ballE /nbhs_ball /nbhs_ball_ //=. -near +oo_K => M. -pose r := (e/2/M). +near +oo_K=> M. +pose r := (`|e|/2/M). exists ((ball k r),(ball x r)). -rewrite !nbhs_simpl /=; split; by apply: nbhsx_ballx; rewrite ?divr_gt0. -rewrite -ball_normE /= /ball_ /= => lz /= [nk nx]. -rewrite -?(scalerBr, scalerBl). -have := @ball_split _ _ (k *: lz.2) (k*: x) (lz.1 *: lz.2) e; rewrite -ball_normE /=. -move => T; apply: T; rewrite -?(scalerBr, scalerBl) normrZ. - by rewrite (@le_lt_trans _ _ (M * `|x - lz.2|)) ?ler_wpM2r -?ltr_pdivlMl// mulrC. +rewrite !nbhs_simpl /=; split; apply: nbhsx_ballx; rewrite ?divr_gt0 // ?normr_gt0 ?lt0r_neq0 //. +rewrite -ball_normE /= /ball_ /= => lz /= [nk nx]. +rewrite -?(scalerBr, scalerBl). +have := @ball_split _ _ (k *: lz.2) (k*: x) (lz.1 *: lz.2) `|e|; rewrite -ball_normE /= real_lter_normr ?gtr0_real //. +have -> : (normr (k *: x - lz.1 *: lz.2) < - e) = false by rewrite ltr_nnorml // oppr_le0 ltW. +rewrite Bool.orb_false_r => T;apply: T; rewrite -?(scalerBr, scalerBl) normrZ. +rewrite (@le_lt_trans _ _ (M * `|x - lz.2|)) ?ler_wpM2r -?ltr_pdivlMl // mulrC //. rewrite (@le_lt_trans _ _ (`|k - lz.1| * M)) ?ler_wpM2l -?ltr_pdivlMr//. - near: M. admit. +rewrite (@le_trans _ _ (normr (lz.2) + normr x)) // ?lerDl ?normr_ge0 //. +move: nx; rewrite /r => nx. +have H: normr lz.2 <= normr x + `|e|/2/M. + have -> : lz.2 = x - (x -lz.2) by rewrite opprB addrCA subrr addr0. + by rewrite (@le_trans _ _ (normr (x) + normr (x - lz.2))) // ?ler_normB // ?lerD // ltW //. +rewrite (@le_trans _ _ ((normr x + `|e| / 2 / M) + (normr x))) // ?lerD //. +rewrite addrAC. +have H0: M = M^-1 * (M * M). rewrite mulrA mulVf ?mul1r // ?lt0r_neq0 //. +rewrite [X in (_ <= X)]H0. +have -> : (normr x + normr x + `|e| / 2 / M) = M^-1 * ( M* (normr x + normr x) + `|e| / 2). + by rewrite mulrDr mulrA mulVf ?mul1r ?lt0r_neq0 // mulrC. +rewrite ler_wpM2l // ?invr_ge0 // ?ltW // -ltrBrDl -mulrBr. +apply: ltr_pM; rewrite ?ltrBrDl //. Unshelve. all: by end_near. -Admitted. +Qed. Lemma locally_convex : exists2 B : set (set V), (forall b, b \in B -> convex b) & basis B. Proof. exists [set B | exists x, exists r, B = ball x r]. move=> b; rewrite inE /= => [[x]] [r] -> z y l. - rewrite !inE -!ball_normE /= => zx zy l1. - rewrite opprD scalerDl opprD. - rewrite scale1r [X in (_ + X)]addrC addrA [X in (X - _)]addrA. - rewrite scaleNr opprK -addrA. admit. + rewrite !inE -!ball_normE /= => zx yx l1. + (* have xz : `|z| < r + `|x|. *) + (* have -> : `|z| = `|(z - x) + x| by rewrite -addrA [X in (_+X)]addrC subrr addr0. *) + (* rewrite (@lt_le_trans _ _ (r + normr x )) //. *) + (* rewrite (@le_lt_trans _ _ (normr ((x - z)%R) + normr x)) //. *) + (* rewrite -[in X in (_ <= X)]opprB normrN ler_normD // addrC. *) + (* by rewrite (@ltr_leD _ _ _ (normr x) _ zx) //. *) + (* have xy : `|y| < r + `|x|. *) + (* have -> : `|y| = `|(y - x) + x| by rewrite -addrA [X in (_+X)]addrC subrr addr0. *) + (* rewrite (@lt_le_trans _ _ (r + normr x )) //. *) + (* rewrite (@le_lt_trans _ _ (normr ((y - x)%R) + normr x)) //. *) + (* by rewrite ler_normD // addrC. *) + (* by rewrite (@ltr_leD _ _ _ (normr x) _ yx) //=. *) + have ->: x = l *: x + (1-l) *: x. admit. + have -> : + (l *: x + (1 - l) *: x) - (l *: z + (1 - l) *: y) = (l *: (x-z) + (1 - l) *: (x - y)). + rewrite opprD. rewrite addrCA. admit. + rewrite (@le_lt_trans _ _ ( `|l| * `|x - z| + `|1 - l| * `|x - y|)) //. + by rewrite -!normrZ ?ler_normD //. + rewrite (@lt_trans _ _ ( `|l| * r + `|1 - l| * r )) //. + rewrite ltrD //. rewrite le_lt_pM //. normrN. + have -> : normr (1 -l) = 1 - normr l. admit. + rewrite -mulrDl addrCA subrr addr0. split => /=. move => B [x] [r] ->. rewrite openE -!ball_normE /interior=> y /= bxy. @@ -900,7 +935,7 @@ Variable (R : rcfType). HB.instance Definition _ := GRing.ComAlgebra.copy R R^o. #[export, non_forgetful_inheritance] HB.instance Definition _ := Vector.copy R R^o. -#[export, non_forgetful_inheritance] + #[export, non_forgetful_inheritance] HB.instance Definition _ := NormedModule.copy R R^o. End rcfType. From fde7635fc21d171eb20b25c43de81890cd53bc6a Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 13 Sep 2024 22:31:18 +0200 Subject: [PATCH 14/14] convex --- theories/normedtype.v | 37 +++++++++++++++---------------------- theories/tvs.v | 2 +- 2 files changed, 16 insertions(+), 23 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 110cc14ca..a473ee7c8 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -852,30 +852,22 @@ Qed. Lemma locally_convex : exists2 B : set (set V), (forall b, b \in B -> convex b) & basis B. Proof. exists [set B | exists x, exists r, B = ball x r]. - move=> b; rewrite inE /= => [[x]] [r] -> z y l. - rewrite !inE -!ball_normE /= => zx yx l1. - (* have xz : `|z| < r + `|x|. *) - (* have -> : `|z| = `|(z - x) + x| by rewrite -addrA [X in (_+X)]addrC subrr addr0. *) - (* rewrite (@lt_le_trans _ _ (r + normr x )) //. *) - (* rewrite (@le_lt_trans _ _ (normr ((x - z)%R) + normr x)) //. *) - (* rewrite -[in X in (_ <= X)]opprB normrN ler_normD // addrC. *) - (* by rewrite (@ltr_leD _ _ _ (normr x) _ zx) //. *) - (* have xy : `|y| < r + `|x|. *) - (* have -> : `|y| = `|(y - x) + x| by rewrite -addrA [X in (_+X)]addrC subrr addr0. *) - (* rewrite (@lt_le_trans _ _ (r + normr x )) //. *) - (* rewrite (@le_lt_trans _ _ (normr ((y - x)%R) + normr x)) //. *) - (* by rewrite ler_normD // addrC. *) - (* by rewrite (@ltr_leD _ _ _ (normr x) _ yx) //=. *) - have ->: x = l *: x + (1-l) *: x. admit. - have -> : + move=> b; rewrite inE /= => [[x]] [r] -> z y l. + rewrite !inE -!ball_normE /= => zx yx l0; rewrite -subr_gt0 => l1. + have ->: x = l *: x + (1-l) *: x by rewrite scalerBl addrCA subrr addr0 scale1r. + have -> : (l *: x + (1 - l) *: x) - (l *: z + (1 - l) *: y) = (l *: (x-z) + (1 - l) *: (x - y)). - rewrite opprD. rewrite addrCA. admit. + by rewrite opprD addrCA addrA addrA -!scalerN -scalerDr [X in l*:X]addrC -addrA -scalerDr. rewrite (@le_lt_trans _ _ ( `|l| * `|x - z| + `|1 - l| * `|x - y|)) //. by rewrite -!normrZ ?ler_normD //. - rewrite (@lt_trans _ _ ( `|l| * r + `|1 - l| * r )) //. - rewrite ltrD //. rewrite le_lt_pM //. normrN. - have -> : normr (1 -l) = 1 - normr l. admit. - rewrite -mulrDl addrCA subrr addr0. + rewrite (@lt_le_trans _ _ ( `|l| * r + `|1 - l| * r )) //. + rewrite ltr_leD //. + rewrite -ltr_pdivlMl ?mulrA ?mulVf ?mul1r // ?normrE ?lt0r_neq0 //. + rewrite -ler_pdivlMl ?mulrA ?mulVf ?mul1r ?ltW // ?normrE; + by apply/eqP => H; move: l1; rewrite H // lt_def => /andP [] /eqP //=. + have -> : normr (1 -l) = 1 - normr l. + by move/ltW/normr_idP: l0 => ->; move/ltW/normr_idP: l1 => ->. + by rewrite -mulrDl addrCA subrr addr0 mul1r. split => /=. move => B [x] [r] ->. rewrite openE -!ball_normE /interior=> y /= bxy. @@ -888,7 +880,7 @@ rewrite -nbhs_ballE /nbhs_ball /nbhs_ball_ /filter_from //=. move=> [r] r0 Bxr /=. rewrite nbhs_simpl /=; exists (ball x r) => //; split; last by apply: ballxx. by exists x; exists r. -Admitted. +Qed. HB.instance Definition _ := Uniform_isTvs.Build K V add_continuous @@ -6129,3 +6121,4 @@ by have [j [Dj BiBj ij]] := maxD i Vi; move/(_ _ cBix) => ?; exists j. Qed. End vitali_lemma_infinite. + diff --git a/theories/tvs.v b/theories/tvs.v index 305e0b298..e09b1ba9f 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -41,7 +41,7 @@ HB.structure Definition UniformLmodule (K : numDomainType) := Definition convex (R : numDomainType) (M : lmodType R) (A : set M) := forall x y (lambda : R), x \in A -> y \in A -> - (`|lambda| < 1) -> lambda *: x + (1 - lambda) *: y \in A. + (0< lambda) -> (lambda < 1) -> lambda *: x + (1 - lambda) *: y \in A. HB.mixin Record Uniform_isTvs (R : numDomainType) E of Uniform E & GRing.Lmodule R E := { add_continuous : continuous (fun x : E * E => x.1 + x.2) ;