From 0a11a30fe042fcabc70d5f9ec8adcd0c20eb0083 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 4 Dec 2021 19:17:46 +0900 Subject: [PATCH] change inequality in ereal_{d,}nbhs - from strict to large closed #122 --- CHANGELOG_UNRELEASED.md | 7 ++ theories/ereal.v | 139 +++++++++++++++++++++++----------------- theories/normedtype.v | 27 ++++---- theories/posnum.v | 14 +++- theories/sequences.v | 8 +-- 5 files changed, 118 insertions(+), 77 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1b7b917b59..4bfac1f7b5 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -8,6 +8,10 @@ + lemma `setDIr` + lemmas `setMT`, `setTM`, `setMI` + lemmas `setSM`, `setM_bigcupr`, `setM_bigcupl` +- in `posnum.v`: + + lemmas `pos_le_maxl`, `pos_le_minr` +- in `ereal.v`: + + lemmas `lee_paddl`, `lte_addl`, `lee_paddr`, `lte_paddr`, `lee_lt_add` ### Changed @@ -16,6 +20,9 @@ + `nbhs_minfty_le` renamed to `nbhs_ninfty_le_pos` and changed to not use `{posnum R}` - in `sequences.v`: + lemma `is_cvg_ereal_nneg_natsum`: remove superfluous `P` parameter +- in `ereal.v`: + + definitions `ereal_dnbhs` and `ereal_nbhs` changed to use large inequality instead + of strict inequality ### Renamed diff --git a/theories/ereal.v b/theories/ereal.v index b7a4bc1858..0a57c3ef0d 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -1160,6 +1160,10 @@ move: x y a b => [x| |] [y| |] [a| |] [b| |] _ _ //=; by rewrite !lte_fin; exact: ltr_le_add. Qed. +Lemma lee_lt_add a b x y : a \is a fin_num -> b \is a fin_num -> + a <= x -> b < y -> a + b < x + y. +Proof. by move=> afin bin xa yb; rewrite (addeC a) (addeC x) lte_le_add. Qed. + Lemma lee_sub x y z u : x <= y -> u <= z -> x - z <= y - u. Proof. move: x y z u => -[x| |] -[y| |] -[z| |] -[u| |] //=; @@ -2097,6 +2101,18 @@ exists (PosNum xy); apply/negP; rewrite -ltNge lte_fin -ltr_subr_addl. by rewrite ltr_pdivr_mulr // ltr_pmulr ?subr_gt0 // ltr1n. Qed. +Lemma lee_paddl y x z : 0 <= x -> y <= z -> y <= x + z. +Proof. by move=> *; rewrite -[y]add0e lee_add. Qed. + +Lemma lte_paddl y x z : 0 <= x -> y < z -> y < x + z. +Proof. by move=> x0 /lt_le_trans; apply; rewrite lee_paddl. Qed. + +Lemma lee_paddr y x z : 0 <= x -> y <= z -> y <= z + x. +Proof. by move=> *; rewrite addeC lee_paddl. Qed. + +Lemma lte_paddr y x z : 0 <= x -> y < z -> y < z + x. +Proof. by move=> *; rewrite addeC lte_paddl. Qed. + Lemma lte_spaddr z x y : z \is a fin_num -> 0 < y -> z <= x -> z < x + y. Proof. move: z y x => [z| |] [y| |] [x| |] _ //=; @@ -2435,14 +2451,14 @@ Local Open Scope classical_set_scope. Definition ereal_dnbhs (x : \bar R) (P : \bar R -> Prop) : Prop := match x with | r%:E => r^' (fun r => P r%:E) - | +oo => exists M, M \is Num.real /\ forall y, M%:E < y -> P y - | -oo => exists M, M \is Num.real /\ forall y, y < M%:E -> P y + | +oo => exists M, M \is Num.real /\ forall y, M%:E <= y -> P y + | -oo => exists M, M \is Num.real /\ forall y, y <= M%:E -> P y end. Definition ereal_nbhs (x : \bar R) (P : \bar R -> Prop) : Prop := match x with | x%:E => nbhs x (fun r => P r%:E) - | +oo => exists M, M \is Num.real /\ forall y, M%:E < y -> P y - | -oo => exists M, M \is Num.real /\ forall y, y < M%:E -> P y + | +oo => exists M, M \is Num.real /\ forall y, M%:E <= y -> P y + | -oo => exists M, M \is Num.real /\ forall y, y <= M%:E -> P y end. Canonical ereal_ereal_filter := FilteredType (extended R) (extended R) (ereal_nbhs). @@ -2471,63 +2487,63 @@ case=> [x||]. by move=> P Q PQ /xS; apply => y /PQ. - apply Build_ProperFilter. move=> P [x [xr xP]] //; exists (x + 1)%:E; apply xP => /=. - by rewrite lte_fin ltr_addl. - split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]]. + by rewrite lee_fin ler_addl. + split=> /= [|P Q [MP [MPr geMP]] [MQ [MQr geMQ]] |P Q sPQ [M [Mr geM]]]. + by exists 0%R; rewrite real0. + have [MP0|MP0] := eqVneq MP 0%R. have [MQ0|MQ0] := eqVneq MQ 0%R. by exists 0%R; rewrite real0; split => // x x0; split; - [apply/gtMP; rewrite MP0 | apply/gtMQ; rewrite MQ0]. + [apply/geMP; rewrite MP0 | apply/geMQ; rewrite MQ0]. exists `|MQ|%R; rewrite realE normr_ge0; split => // x MQx; split. - by apply: gtMP; rewrite (le_lt_trans _ MQx) // MP0 lee_fin. - by apply gtMQ; rewrite (le_lt_trans _ MQx)// lee_fin real_ler_normr ?lexx. + by apply: geMP; rewrite (le_trans _ MQx) // MP0 lee_fin. + by apply geMQ; rewrite (le_trans _ MQx)// lee_fin real_ler_normr ?lexx. have [MQ0|MQ0] := eqVneq MQ 0%R. exists `|MP|%R; rewrite realE normr_ge0; split => // x MPx; split. - by apply gtMP; rewrite (le_lt_trans _ MPx)// lee_fin real_ler_normr ?lexx. - by apply gtMQ; rewrite (le_lt_trans _ MPx) // lee_fin MQ0. + by apply geMP; rewrite (le_trans _ MPx)// lee_fin real_ler_normr ?lexx. + by apply geMQ; rewrite (le_trans _ MPx) // lee_fin MQ0. have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0. have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0. exists (Num.max (PosNum MP0) (PosNum MQ0))%:num. rewrite realE /= posnum_ge0 /=; split => //. case=> [r| |//]. - * rewrite lte_fin/= posnum_max pos_lt_maxl /= => /andP[MPx MQx]; split. - by apply/gtMP; rewrite lte_fin (le_lt_trans _ MPx)// real_ler_normr ?lexx. - by apply/gtMQ; rewrite lte_fin (le_lt_trans _ MQx)// real_ler_normr ?lexx. - * by move=> _; split; [apply/gtMP | apply/gtMQ]. - + by exists M; split => // ? /gtM /sPQ. + * rewrite lee_fin /= posnum_max pos_le_maxl /= => /andP[MPx MQx]; split. + by apply/geMP; rewrite lee_fin (le_trans _ MPx)// real_ler_normr ?lexx. + by apply/geMQ; rewrite lee_fin (le_trans _ MQx)// real_ler_normr ?lexx. + * by move=> _; split; [apply/geMP | apply/geMQ]. + + by exists M; split => // ? /geM /sPQ. - apply Build_ProperFilter. + move=> P [M [Mr ltMP]]; exists (M - 1)%:E. - by apply: ltMP; rewrite lte_fin gtr_addl oppr_lt0. - + split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]]. + by apply: ltMP; rewrite lee_fin ger_addl oppr_le0. + + split=> /= [|P Q [MP [MPr leMP]] [MQ [MQr leMQ]] |P Q sPQ [M [Mr leM]]]. * by exists 0%R; rewrite real0. * have [MP0|MP0] := eqVneq MP 0%R. have [MQ0|MQ0] := eqVneq MQ 0%R. by exists 0%R; rewrite real0; split => // x x0; split; - [apply/ltMP; rewrite MP0 | apply/ltMQ; rewrite MQ0]. + [apply/leMP; rewrite MP0 | apply/leMQ; rewrite MQ0]. exists (- `|MQ|)%R; rewrite realN realE normr_ge0; split => // x xMQ. split. - by apply ltMP; rewrite (lt_le_trans xMQ)// lee_fin MP0 ler_oppl oppr0. - apply ltMQ; rewrite (lt_le_trans xMQ) // lee_fin ler_oppl -normrN. + by apply leMP; rewrite (le_trans xMQ)// lee_fin MP0 ler_oppl oppr0. + apply leMQ; rewrite (le_trans xMQ) // lee_fin ler_oppl -normrN. by rewrite real_ler_normr ?realN // lexx. * have [MQ0|MQ0] := eqVneq MQ 0%R. exists (- `|MP|)%R; rewrite realN realE normr_ge0; split => // x MPx. split. - apply ltMP; rewrite (lt_le_trans MPx) // lee_fin ler_oppl -normrN. + apply leMP; rewrite (le_trans MPx) // lee_fin ler_oppl -normrN. by rewrite real_ler_normr ?realN // lexx. - by apply ltMQ; rewrite (lt_le_trans MPx) // lee_fin MQ0 ler_oppl oppr0. + by apply leMQ; rewrite (le_trans MPx) // lee_fin MQ0 ler_oppl oppr0. have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0. have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0. exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num)%R. rewrite realN realE /= posnum_ge0 /=; split => //. case=> [r|//|]. - - rewrite lte_fin ltr_oppr posnum_max pos_lt_maxl => /andP[]. - rewrite ltr_oppr => MPx; rewrite ltr_oppr => MQx; split. - apply/ltMP; rewrite lte_fin (lt_le_trans MPx) //= ler_oppl -normrN. + - rewrite lee_fin ler_oppr posnum_max pos_le_maxl => /andP[]. + rewrite ler_oppr => MPx; rewrite ler_oppr => MQx; split. + apply/leMP; rewrite lee_fin (le_trans MPx) //= ler_oppl -normrN. by rewrite real_ler_normr ?realN // lexx. - apply/ltMQ; rewrite lte_fin (lt_le_trans MQx) //= ler_oppl -normrN. + apply/leMQ; rewrite lee_fin (le_trans MQx) //= ler_oppl -normrN. by rewrite real_ler_normr ?realN // lexx. - - by move=> _; split; [apply/ltMP | apply/ltMQ]. - * by exists M; split => // x /ltM /sPQ. + - by move=> _; split; [apply/leMP | apply/leMQ]. + * by exists M; split => // x /leM /sPQ. Qed. Typeclasses Opaque ereal_dnbhs. @@ -2564,30 +2580,30 @@ move: p => -[p| [M [Mreal MA]] | [M [Mreal MA]]] //=. apply/ballA/(@ball_splitl _ _ r) => //; exact/ball_sym. - exists (M + 1)%R; split; first by rewrite realD // real1. move=> -[x| _ |] //=. - rewrite lte_fin => M'x /=. + rewrite lee_fin => M'x /=. apply/nbhs_ballP; exists 1%R => //= y x1y. - apply MA; rewrite lte_fin. - rewrite addrC -ltr_subr_addl in M'x. - rewrite (lt_le_trans M'x) // ler_subl_addl addrC -ler_subl_addl. + apply MA; rewrite lee_fin. + rewrite addrC -ler_subr_addl in M'x. + rewrite (le_trans M'x) // ler_subl_addl addrC -ler_subl_addl. rewrite (le_trans _ (ltW x1y)) // real_ler_norm // realB //. - rewrite ltr_subr_addr in M'x. + rewrite ler_subr_addr in M'x. rewrite -comparabler0 (@comparabler_trans _ (M + 1)%R) //. - by rewrite /Order.comparable (ltW M'x) orbT. + by rewrite /Order.comparable M'x orbT. by rewrite comparabler0 realD // real1. by rewrite num_real. (* where we really use realFieldType *) by exists M. - exists (M - 1)%R; split; first by rewrite realB // real1. move=> -[x| _ |] //=. - rewrite lte_fin => M'x /=. + rewrite lee_fin => M'x /=. apply/nbhs_ballP; exists 1%R => //= y x1y. - apply MA; rewrite lte_fin. - rewrite ltr_subr_addl in M'x. - rewrite (le_lt_trans _ M'x) // addrC -ler_subl_addl. + apply MA; rewrite lee_fin. + rewrite ler_subr_addl in M'x. + rewrite (le_trans _ M'x) // addrC -ler_subl_addl. rewrite (le_trans _ (ltW x1y)) // distrC real_ler_norm // realB //. by rewrite num_real. (* where we really use realFieldType *) - rewrite addrC -ltr_subr_addr in M'x. + rewrite addrC -ler_subr_addr in M'x. rewrite -comparabler0 (@comparabler_trans _ (M - 1)%R) //. - by rewrite /Order.comparable (ltW M'x). + by rewrite /Order.comparable M'x. by rewrite comparabler0 realB // real1. by exists M. Qed. @@ -2617,19 +2633,19 @@ case: x => [r /=| |]. - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]]. exists (-%E @` S). exists (- M)%R; rewrite realN Mreal; split => // x Mx. - by exists (- x); [apply MS; rewrite lte_oppl | rewrite oppeK]. + by exists (- x); [apply MS; rewrite lee_oppl | rewrite oppeK]. rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK. by exists (- x); [exists x | rewrite oppeK]. exists (- M)%R; rewrite realN; split => // y yM. - exists (- y); by [apply Mx; rewrite lte_oppr|rewrite oppeK]. + exists (- y); by [apply Mx; rewrite lee_oppr|rewrite oppeK]. - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]]. exists (-%E @` S). exists (- M)%R; rewrite realN Mreal; split => // x Mx. - by exists (- x); [apply MS; rewrite lte_oppr | rewrite oppeK]. + by exists (- x); [apply MS; rewrite lee_oppr | rewrite oppeK]. rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK. by exists (- x); [exists x | rewrite oppeK]. exists (- M)%R; rewrite realN; split => // y yM. - exists (- y); by [apply Mx; rewrite lte_oppl|rewrite oppeK]. + exists (- y); by [apply Mx; rewrite lee_oppl|rewrite oppeK]. Qed. Lemma nbhsNKe (R : realFieldType) (z : \bar R) (A : set (\bar R)) : @@ -2992,12 +3008,15 @@ Lemma nbhs_oo_up_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num <= 1)%R -> ereal_ball +oo e%:num `<=` A -> nbhs +oo A. Proof. move=> e1 ooeA. -exists (fine (expand (1 - e%:num)%R)); rewrite num_real; split => //. -case => [r | | //]. -- rewrite fine_expand; last first. - by rewrite ger0_norm ?ltr_subl_addl ?ltr_addr // subr_ge0. - by move=> ?; exact/ooeA/expand_ereal_ball_pinfty. -- by move=> _; exact/ooeA/ereal_ball_center. +exists (fine (expand (1 - e%:num / 2)%R)); rewrite num_real; split => //. +have e21 : (`|1 - e%:num / 2| < 1)%R. + rewrite ger0_norm; first by rewrite ltr_subl_addl ltr_addr. + by rewrite subr_ge0 ler_pdivr_mulr// mul1r (le_trans e1)// ler1n. +case => [r | _ | //]; last exact/ooeA/ereal_ball_center. +rewrite fine_expand // => er; apply/ooeA/expand_ereal_ball_pinfty => //. +rewrite (lt_le_trans _ er)// lt_expand ?inE; last exact/ltW. + by rewrite ler_lt_sub// ltr_pdivr_mulr// ltr_pmulr// ltr1n. +by rewrite ger0_norm ?subr_ge0// ler_subl_addl addrC -ler_subl_addl subrr. Qed. Lemma nbhs_oo_down_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num <= 1)%R -> @@ -3263,12 +3282,12 @@ rewrite predeq2E => x A; split. by rewrite subr_gt0 (le_lt_trans _ (contract_lt1 M)) // ler_norm. case=> [r| |]/=. * rewrite /ereal_ball [_ +oo]/= => rM1. - apply: MA; rewrite lte_fin. + apply: MA; rewrite lee_fin. rewrite ger0_norm in rM1; last first. by rewrite subr_ge0 // (le_trans _ (contract_le1 r%:E)) // ler_norm. rewrite ltr_subl_addr addrC addrCA addrC -ltr_subl_addr subrr in rM1. rewrite subr_gt0 in rM1. - by rewrite -lte_fin -lt_contract. + by rewrite -lee_fin -le_contract ltW. * by rewrite /ereal_ball /= subrr normr0 => h; exact: MA. * rewrite /ereal_ball /= opprK => h {MA}. exfalso. @@ -3283,12 +3302,12 @@ rewrite predeq2E => x A; split. case=> [r| |]. * rewrite /ereal_ball => /= rM1. apply MA. - rewrite lte_fin. + rewrite lee_fin. rewrite ler0_norm in rM1; last first. rewrite ler_subl_addl addr0 ltW //. by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. rewrite opprB opprK -ltr_subl_addl addrK in rM1. - by rewrite -lte_fin -lt_contract. + by rewrite -lee_fin -le_contract ltW. * rewrite /ereal_ball /= -opprD normrN => h {MA}. exfalso. move: h; apply/negP. @@ -3385,14 +3404,14 @@ case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 firs have /ZnatP [N Nfloor] : floor (Num.max d 0%R) \is a Znat. by rewrite Znat_def floor_ge0 le_maxr lexx orbC. exists N.+1 => // n ltNn; apply: dP. - have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx. - apply; apply: lt_le_trans (lt_succ_Rfloor _) _; rewrite RfloorE Nfloor. + have /le_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx. + apply; apply: le_trans (ltW (lt_succ_Rfloor _)) _; rewrite RfloorE Nfloor. by rewrite -(@natrD R N 1) ler_nat addn1. have /ZnatP [N Nfloor] : floor (Num.max (- d)%R 0%R) \is a Znat. by rewrite Znat_def floor_ge0 le_maxr lexx orbC. - exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin ltr_oppl. - have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_maxr lexx. - apply; apply: lt_le_trans (lt_succ_Rfloor _) _; rewrite RfloorE Nfloor. + exists N.+1 => // n ltNn; apply: dP; rewrite lee_fin ler_oppl. + have /le_trans : (- d <= Num.max (- d) 0)%R by rewrite le_maxr lexx. + apply; apply: le_trans (ltW (lt_succ_Rfloor _)) _; rewrite RfloorE Nfloor. by rewrite -(@natrD R N 1) ler_nat addn1. have /ZnatP [N Nfloor] : floor (d%:num^-1) \is a Znat. by rewrite Znat_def floor_ge0. diff --git a/theories/normedtype.v b/theories/normedtype.v index 0b92ed5d77..97b7636b4f 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2207,10 +2207,10 @@ move=> [x| |] /=. exact: (cvg_comp (@scaler_continuous _ _ _ _)). - rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]]. exists (r^-1 * u); split; first by rewrite realM// realV// realE (ltW r0). - by move=> x rux; apply uA; move: rux; rewrite mulEFin lte_pdivr_mull. + by move=> x rux; apply uA; move: rux; rewrite mulEFin lee_pdivr_mull. - rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]]. exists (r^-1 * u); split; first by rewrite realM// realV// realE (ltW r0). - by move=> x xru; apply uA; move: xru; rewrite mulEFin lte_pdivl_mull. + by move=> x xru; apply uA; move: xru; rewrite mulEFin lee_pdivl_mull. Grab Existential Variables. all: end_near. Qed. End mule_continuous. @@ -3597,24 +3597,28 @@ case: x => [x|//|] xy; first exact: open_ereal_lt. - case: y => [y||//] /= in xy *; last by exists 0%R. by exists y; rewrite num_real; split => //= x ?. - case: y => [y||//] /= in xy *. - + by exists y; rewrite num_real; split => //= x ?. - + exists 0%R; rewrite real0; split => // x. - by move/lt_le_trans; apply; rewrite lee_pinfty. + + exists (y - 1)%R; rewrite num_real; split => //= x /le_lt_trans; apply. + by rewrite lte_fin ltr_subl_addr ltr_addl. + + exists 0%R; rewrite real0; split => // x /le_lt_trans; apply. + by rewrite lte_pinfty. Qed. Lemma open_ereal_gt' x y : y < x -> ereal_nbhs x (fun u => y < u). Proof. case: x => [x||] //=; do ?[exact: open_ereal_gt]; case: y => [y||] //=; do ?by exists 0; rewrite real0. -- by exists y; rewrite num_real. +- exists (y + 1)%R; rewrite num_real; split => // x /lt_le_trans; apply. + by rewrite lte_fin ltr_addl. - move=> _; exists 0%R; rewrite real0; split => // x. - by apply/le_lt_trans; rewrite lee_ninfty. + by apply/lt_le_trans; rewrite lte_ninfty. Qed. Let open_ereal_lt_real r : open (fun x => x < r%:E). Proof. -case => [? | // | ?]; [rewrite lte_fin => xy | by exists r]. -by move: (@open_ereal_lt r%:E); rewrite openE; apply; rewrite /= lte_fin. +case => [? | // | ?]; [rewrite lte_fin => xy | exists (r - 1)%R]. + by move: (@open_ereal_lt r%:E); rewrite openE; apply; rewrite /= lte_fin. +rewrite num_real; split => // x /le_lt_trans; apply. +by rewrite lte_fin ltr_subl_addr ltr_addl. Qed. Lemma open_ereal_lt_ereal x : open [set y | y < x]. @@ -3631,8 +3635,9 @@ Qed. Let open_ereal_gt_real r : open (fun x => r%:E < x). Proof. -case => [? | ? | //]; [rewrite lte_fin => xy | by exists r]. -by move: (@open_ereal_gt r%:E); rewrite openE; apply; rewrite /= lte_fin. +case => [? | ? | //]; [rewrite lte_fin => xy | exists (r + 1)%R]. + by move: (@open_ereal_gt r%:E); rewrite openE; apply; rewrite /= lte_fin. +by rewrite num_real; split=> // x /lt_le_trans; apply; rewrite lte_fin ltr_addl. Qed. Lemma open_ereal_gt_ereal x : open [set y | x < y]. diff --git a/theories/posnum.v b/theories/posnum.v index ce1c075f0a..c28015526b 100644 --- a/theories/posnum.v +++ b/theories/posnum.v @@ -134,12 +134,22 @@ Proof. by rewrite lt_geF. Qed. Lemma posnum_lt0 x : (x%:num < 0 :> R) = false. Proof. by rewrite lt_gtF. Qed. -Lemma pos_lt_maxl a x y : Num.max x%:num y%:num < a = (x%:num < a) && (y%:num < a). +Lemma pos_lt_maxl a x y : + Num.max x%:num y%:num < a = (x%:num < a) && (y%:num < a). Proof. by rewrite comparable_lt_maxl ?real_comparable. Qed. -Lemma pos_lt_minr (a : R) x y : a < Num.min x%:num y%:num = (a < x%:num) && (a < y%:num). +Lemma pos_le_maxl a x y : + Num.max x%:num y%:num <= a = (x%:num <= a) && (y%:num <= a). +Proof. by rewrite comparable_le_maxl ?real_comparable. Qed. + +Lemma pos_lt_minr a x y : + a < Num.min x%:num y%:num = (a < x%:num) && (a < y%:num). Proof. by rewrite comparable_lt_minr ?real_comparable. Qed. +Lemma pos_le_minr (a : R) x y : + a <= Num.min x%:num y%:num = (a <= x%:num) && (a <= y%:num). +Proof. by rewrite comparable_le_minr ?real_comparable. Qed. + Lemma min_pos_gt0 x y : 0 < Num.min x%:num y%:num. Proof. by rewrite -posnum_min !posnum_gt0. Qed. Canonical minr_posnum x y := PosNum (@min_pos_gt0 x y). diff --git a/theories/sequences.v b/theories/sequences.v index 426f6345ba..10a2a47a84 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1317,8 +1317,8 @@ split => [u_cvg _/posnumP[A]|u_ge X [A [Ar AX]]]. by apply: u_cvg; apply: ereal_nbhs_pinfty_ge. rewrite !near_simpl [\near u_, X _](near_map u_ \oo); near=> x. apply: AX. -rewrite (@lt_le_trans _ _ (maxr 0 A + 1)%:E) //. - by rewrite addEFin lte_spaddr // ?lte_fin// lee_fin le_maxr lexx orbT. +rewrite (@le_trans _ _ (maxr 0 A + 1)%:E) //. + by rewrite addEFin lee_paddr// lee_fin// le_maxr lexx orbT. by near: x; apply: u_ge; rewrite ltr_spaddr // le_maxr lexx. Grab Existential Variables. all: end_near. Qed. @@ -1330,9 +1330,9 @@ split => [u_cvg A A0|u_le X [A [Ar AX]]]. by apply: u_cvg; apply: ereal_nbhs_ninfty_le. rewrite !near_simpl [\near u_, X _](near_map u_ \oo); near=> x. apply: AX. -rewrite (@le_lt_trans _ _ (minr 0 A - 1)%:E) //. +rewrite (@le_trans _ _ (minr 0 A - 1)%:E) //. by near: x; apply: u_le; rewrite ltr_subl_addl addr0 lt_minl ltr01. -by rewrite lte_fin ltr_subl_addl lt_minl ltr_addr ltr01 orbT. +by rewrite lee_fin ler_subl_addl le_minl ler_addr ler01 orbT. Grab Existential Variables. all: end_near. Qed. Lemma lee_lim (R : realFieldType) (u_ v_ : (\bar R)^nat) : cvg u_ -> cvg v_ ->