From 6edde6a6ce84b06f1069447ebf390cbb9f5daddd Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 10 Dec 2018 18:43:24 +0100 Subject: [PATCH] replacing strict inequality by a large one in locally_Rbar --- derive.v | 6 ++-- hierarchy.v | 84 ++++++++++++++++++++++++++++++++--------------------- landau.v | 13 +++++---- 3 files changed, 61 insertions(+), 42 deletions(-) diff --git a/derive.v b/derive.v index f2e9280f8..299a91ee2 100644 --- a/derive.v +++ b/derive.v @@ -162,7 +162,7 @@ move=> /diff_locallyP [dfc]; rewrite -addrA. rewrite (littleo_bigO_eqo (cst (1 : R^o))); last first. apply/eqOP; near=> k; rewrite /cst [`|[1 : R^o]|]absr1 mulr1. near=> y; rewrite ltrW //; near: y; apply/locally_normP. - by exists k; [near: k; exists 0|move=> ? /=; rewrite sub0r normmN]. + by exists k => // ? /=; rewrite sub0r normmN. rewrite addfo; first by move=> /eqolim; rewrite flim_shift add0r. by apply/eqolim0P; apply: (flim_trans (dfc 0)); rewrite linear0. Grab Existential Variables. all: end_near. Qed. @@ -1297,7 +1297,7 @@ have imf_sup : has_sup imf. apply/compact_bounded/continuous_compact; last exact: segment_compact. by move=> ?; rewrite inE => /asboolP /fcont. exists (M + 1); apply/ubP => y; rewrite !inE => /asboolP /imfltM yltM. - apply/ltrW; apply: ler_lt_trans (yltM _ _); last by rewrite ltr_addl. + apply/ltrW; apply: ler_lt_trans (yltM _ _); last by rewrite ler_addl. by rewrite [ `|[_]| ]absRE ler_norm. case: (pselect (exists2 c, c \in `[a, b] & f c = sup imf)) => [|imf_ltsup]. move=> [c cab fceqsup]; exists c => // t tab. @@ -1324,7 +1324,7 @@ rewrite ltr_subl_addr - ltr_subl_addl. suff : sup imf - f t > k^-1 by move=> /ltrW; rewrite lerNgt => /negbTE ->. rewrite -[X in _ < X]invrK ltr_pinv. rewrite -div1r; apply: ler_lt_trans (ler_norm _) _; rewrite -absRE. - by apply: imVfltM; [rewrite ltr_maxr ltr_addl ltr01|apply: imageP]. + by apply: imVfltM; [rewrite ler_maxr ler_addl ler01|apply: imageP]. by rewrite inE kgt0 unitfE lt0r_neq0. have invsupft_gt0 : 0 < (sup imf - f t)^-1. by rewrite invr_gt0 subr_gt0 imf_ltsup. diff --git a/hierarchy.v b/hierarchy.v index c2ebe1f43..9c366ca1d 100644 --- a/hierarchy.v +++ b/hierarchy.v @@ -1198,14 +1198,14 @@ Notation "'-oo'" := m_infty : real_scope. Definition Rbar_locally' (a : Rbar) (P : R -> Prop) := match a with | Finite a => locally' a P - | +oo => exists M : R, forall x, M < x -> P x - | -oo => exists M : R, forall x, x < M -> P x + | +oo => exists M : R, forall x, M <= x -> P x + | -oo => exists M : R, forall x, x <= M -> P x end. Definition Rbar_locally (a : Rbar) (P : R -> Prop) := match a with | Finite a => locally a P - | +oo => exists M : R, forall x, M < x -> P x - | -oo => exists M : R, forall x, x < M -> P x + | +oo => exists M : R, forall x, M <= x -> P x + | -oo => exists M : R, forall x, x <= M -> P x end. Canonical Rbar_eqType := EqType Rbar gen_eqMixin. @@ -1226,19 +1226,18 @@ Global Instance Rbar_locally'_filter : forall x, ProperFilter (Rbar_locally' x). Proof. case=> [x||]; first exact: Rlocally'_proper. apply Build_ProperFilter. - by move=> P [M gtMP]; exists (M + 1); apply: gtMP; rewrite ltr_addl. - split=> /= [|P Q [MP gtMP] [MQ gtMQ] |P Q sPQ [M gtMP]]; first by exists 0. - by exists (maxr MP MQ) => ?; rewrite ltr_maxl => /andP [/gtMP ? /gtMQ]. - by exists M => ? /gtMP /sPQ. + by move=> P [M geMP]; exists M; apply: geMP. + split=> /= [|P Q [MP geMP] [MQ geMQ] |P Q sPQ [M geMP]]; first by exists 0. + by exists (maxr MP MQ) => ?; rewrite ler_maxl => /andP [/geMP ? /geMQ]. + by exists M => ? /geMP /sPQ. apply Build_ProperFilter. - by move=> P [M ltMP]; exists (M - 1); apply: ltMP; rewrite gtr_addl oppr_lt0. -split=> /= [|P Q [MP ltMP] [MQ ltMQ] |P Q sPQ [M ltMP]]; first by exists 0. - by exists (minr MP MQ) => ?; rewrite ltr_minr => /andP [/ltMP ? /ltMQ]. -by exists M => ? /ltMP /sPQ. + by move=> P [M leMP]; exists M; apply: leMP. +split=> /= [|P Q [MP leMP] [MQ leMQ] |P Q sPQ [M leMP]]; first by exists 0. + by exists (minr MP MQ) => ?; rewrite ler_minr => /andP [/leMP ? /leMQ]. +by exists M => ? /leMP /sPQ. Qed. Typeclasses Opaque Rbar_locally'. - Global Instance Rbar_locally_filter : forall x, ProperFilter (Rbar_locally x). Proof. case=> [x||]. @@ -1251,18 +1250,38 @@ Typeclasses Opaque Rbar_locally. Lemma near_pinfty_div2 (A : set R) : (\forall k \near +oo, A k) -> (\forall k \near +oo, A (k / 2)). Proof. -by move=> [M AM]; exists (M * 2) => x; rewrite -ltr_pdivl_mulr //; apply: AM. +by move=> [M AM]; exists (M * 2) => x; rewrite -ler_pdivl_mulr //; apply: AM. Qed. +Lemma locally_pinfty_ge c : \forall x \near +oo, c <= x. +Proof. by exists c. Qed. + Lemma locally_pinfty_gt c : \forall x \near +oo, c < x. +Proof. by exists (c + 1) => ? /ltr_le_trans; apply; rewrite ltr_addl. Qed. + +Hint Extern 0 (is_true (_ <= _)) => + match goal with _ : ?x \is_near (locally +oo) |- is_true (_ <= ?x) => + now (near: x; apply: locally_pinfty_ge) end : core. + +Hint Extern 0 (is_true (_ < _)) => + match goal with _ : ?x \is_near (locally +oo) |- is_true (_ < ?x) => + now (near: x; apply: locally_pinfty_gt) end : core. + +Lemma locally_minfty_le c : \forall x \near -oo, x <= c. Proof. by exists c. Qed. -Lemma locally_pinfty_ge c : \forall x \near +oo, c <= x. -Proof. by exists c; apply: ltrW. Qed. +Lemma locally_minfty_lt c : \forall x \near -oo, x < c. +Proof. +by exists (c - 1) => ? /ler_lt_trans; apply; rewrite ltr_subl_addl ltr_addr. +Qed. -Hint Extern 0 (is_true (0 < _)) => match goal with - H : ?x \is_near (locally +oo) |- _ => - solve[near: x; exists 0 => _/posnumP[x] //] end : core. +Hint Extern 0 (is_true (_ <= _)) => + match goal with _ : ?x \is_near (locally +oo) |- is_true (?x <= _) => + now (near: x; apply: locally_minfty_le) end : core. + +Hint Extern 0 (is_true (_ < _)) => + match goal with _ : ?x \is_near (locally +oo) |- is_true (?x < _) => + now (near: x; apply: locally_minfty_lt) end : core. (** ** Modules with a norm *) @@ -1616,12 +1635,11 @@ Proof. by move=> /flim_normP. Qed. Lemma flim_bounded {F : set (set V)} {FF : Filter F} (y : V) : F --> y -> \forall M \near +oo, \forall y' \near F, `|[y']|%real < M. Proof. -move=> /flim_norm Fy; exists `|[y]| => M. -rewrite -subr_gt0 => subM_gt0; have := Fy _ subM_gt0. -apply: filterS => y' yy'; rewrite -(@ltr_add2r _ (- `|[y]|)). -rewrite (ler_lt_trans _ yy') //. -by rewrite (ler_trans _ (ler_distm_dist _ _)) // absRE distrC ler_norm. -Qed. +move=> /flim_norm Fy; near=> M; have MP : M - `|[y]| > 0 by rewrite subr_gt0. +near=> y'; rewrite -(@ltr_add2r _ (- `|[y]|)) (@ler_lt_trans _ `|[y - y']|)//. + by rewrite (ler_trans (ler_norm _)) // distrC ler_distm_dist. +by apply: (near (Fy _ _) y'). +Grab Existential Variables. all: end_near. Qed. Lemma flimi_map_lim {F} {FF : ProperFilter F} (f : T -> V -> Prop) (l : V) : F (fun x : T => is_prop (f x)) -> @@ -1819,7 +1837,8 @@ rewrite (@distm_lt_split _ _ (k *: z)) // -?(scalerBr, scalerBl) normmZ. by apply: flim_norm; rewrite // mulr_gt0 // ?invr_gt0 ltr_paddl. have zM: `|[z]| < M by near: z; near: M; apply: flim_bounded; apply: flim_refl. rewrite (ler_lt_trans (ler_pmul _ _ (lerr _) (_ : _ <= M))) // ?ltrW//. -by rewrite -ltr_pdivl_mulr //; near: l; apply: (flim_norm (_ : K^o)). +rewrite -ltr_pdivl_mulr //; near: l. +by apply: (flim_norm (_ : K^o)) => //; rewrite divr_gt0. Grab Existential Variables. all: end_near. Qed. Arguments scale_continuous _ _ : clear implicits. @@ -2640,7 +2659,7 @@ have /Aco [] := covA. by rewrite -{1}(subrK p q) ler_normm_add. move=> D _ DcovA. exists (bigmaxr 0 [seq n%:~R | n <- enum_fset D]). -move=> x ltmaxx p /DcovA [n Dn /ltr_trans]; apply; apply: ler_lt_trans ltmaxx. +move=> x ltmaxx p /DcovA [n Dn /ltr_le_trans]; apply; apply: ler_trans ltmaxx. have ltin : (index n (enum_fset D) < size (enum_fset D))%N by rewrite index_mem. rewrite -(nth_index 0 Dn) -(nth_map _ 0) //; apply: bigmaxr_ler. by rewrite size_map. @@ -2713,7 +2732,7 @@ have Mnco : compact by move=> _; apply: segment_compact. apply: subclosed_compact Acl Mnco _ => v /normAltM normvltM i. suff /ltrW : `|[v ord0 i : R^o]| < M + 1 by rewrite [ `|[_]| ]absRE ler_norml. -apply: ler_lt_trans (normvltM _ _); last by rewrite ltr_addl. +apply: ler_lt_trans (normvltM _ _); last by rewrite ler_addl. have vinseq : `|v ord0 i| \in [seq `|v ij.1 ij.2| | ij : 'I_1 * 'I_n.+1]. by apply/mapP; exists (ord0, i) => //=; rewrite mem_enum. rewrite -[X in X <= _](nth_index 0 vinseq); apply: bigmaxr_ler. @@ -2741,8 +2760,7 @@ Qed. Lemma open_Rbar_lt' x y : Rbar_lt x y -> Rbar_locally x (fun u => Rbar_lt u y). Proof. case: x => [x|//|] xy; first exact: open_Rbar_lt. -case: y => [y||//] /= in xy *. -exists y => /= x ? //. +case: y => [y||//] in xy *; first exact: locally_minfty_lt. by exists 0. Qed. @@ -2750,7 +2768,7 @@ Lemma open_Rbar_gt' x y : Rbar_lt y x -> Rbar_locally x (fun u => Rbar_lt y u). Proof. case: x => [x||] //=; do ?[exact: open_Rbar_gt]; case: y => [y||] //=; do ?by exists 0. -by exists y => x yx //=. +by move=> _; exact: locally_pinfty_gt. Qed. Lemma Rbar_locally'_le x : Rbar_locally' x --> Rbar_locally x. @@ -2778,13 +2796,13 @@ move=> P; rewrite /Rbar_loc_seq. case: x => /= [x [_/posnumP[delta] Hp] |[delta Hp] |[delta Hp]]; last 2 first. have /ZnatP [N Nfloor] : ifloor (maxr delta 0) \is a Znat. by rewrite Znat_def ifloor_ge0 ler_maxr lerr orbC. - exists N.+1 => // n ltNn; apply: Hp. + exists N.+1 => // n ltNn; apply: Hp; apply: ltrW. have /ler_lt_trans : delta <= maxr delta 0 by rewrite ler_maxr lerr. apply; apply: ltr_le_trans (floorS_gtr _) _; rewrite floorE Nfloor. by rewrite -(@natrD [ringType of R] N 1) INRE ler_nat addn1. have /ZnatP [N Nfloor] : ifloor (maxr (- delta) 0) \is a Znat. by rewrite Znat_def ifloor_ge0 ler_maxr lerr orbC. - exists N.+1 => // n ltNn; apply: Hp; rewrite ltr_oppl. + exists N.+1 => // n ltNn; apply: Hp; rewrite ler_oppl; apply: ltrW. have /ler_lt_trans : - delta <= maxr (- delta) 0 by rewrite ler_maxr lerr. apply; apply: ltr_le_trans (floorS_gtr _) _; rewrite floorE Nfloor. by rewrite -(@natrD [ringType of R] N 1) INRE ler_nat addn1. diff --git a/landau.v b/landau.v index 0dc3d018c..d5242f38b 100644 --- a/landau.v +++ b/landau.v @@ -568,8 +568,8 @@ Proof. split=> [[k _ fOg] | [k fOg]]. exists k => l ltkl; move: fOg; apply: filter_app; near=> x. by move/ler_trans; apply; rewrite ler_wpmul2r // ltrW. -exists (maxr 1 (k + 1)); first by rewrite ltr_maxr ltr01. -by apply: fOg; rewrite ltr_maxr orbC ltr_addl ltr01. +exists (maxr 1 k); first by rewrite ltr_maxr ltr01. +by apply: fOg; rewrite ler_maxr orbC lerr. Unshelve. end_near. Qed. Structure bigO_type (F : set (set T)) (g : T -> W) := BigO { @@ -758,7 +758,8 @@ Proof. by have := @eqaddOE F f g h e; rewrite !funeqE. Qed. Lemma eqoO (F : filter_on T) (f : T -> V) (e : T -> W) : [o_F e of f] =O_F e. -Proof. by apply/eqOP; exists 0 => k kgt0; apply: littleoP. Qed. +Proof. by apply/eqOP; near=> M; apply: littleoP. +Grab Existential Variables. all: end_near. Qed. Hint Resolve eqoO. Lemma littleo_eqO (F : filter_on T) (e : T -> W) (f : {o_F e}) : @@ -1063,8 +1064,7 @@ Proof. rewrite [RHS]bigOE//; have [ O1 k1 Oh1] := bigO; have [ O2 k2 Oh2] := bigO. near=> k; move: Oh1 Oh2; apply: filter_app2; near=> x => leOh1 leOh2. rewrite [`|[_]|]absrM (ler_trans (ler_pmul _ _ leOh1 leOh2)) //. -rewrite mulrACA [`|[_]| in X in _ <= X]normrM ler_wpmul2r // ?mulr_ge0 //. -by near: k; apply: locally_pinfty_ge. +by rewrite mulrACA [`|[_]| in X in _ <= X]normrM ler_wpmul2r // ?mulr_ge0. Unshelve. end_near. Grab Existential Variables. end_near. Qed. End rule_of_products_in_R. @@ -1135,7 +1135,8 @@ suff flip : \forall k \near +oo, forall x, `|[f x]| <= k * `|[x]|. near +oo => k; near=> y. rewrite (ler_lt_trans (near flip k _ _)) // -ltr_pdivl_mull //. near: y; apply/locally_normP. - by eexists; last by move=> ?; rewrite /= sub0r normmN; apply. + eexists; last by move=> ?; rewrite /= sub0r normmN; apply. + by rewrite mulr_gt0// ?invr_gt0. have /locally_normP [_/posnumP[d]] := Of1. rewrite /cst [X in _ * X]absr1 mulr1 => fk; near=> k => y. case: (ler0P `|[y]|) => [|y0].