From b719baa6d006ae04598c284de34f27acc981909f 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 - also in {p,n}infty_{d,}nbhs closed #122 --- CHANGELOG_UNRELEASED.md | 8 ++ theories/derive.v | 4 +- theories/ereal.v | 236 +++++++++++++++---------------- theories/exp.v | 2 +- theories/landau.v | 22 +-- theories/lebesgue_integral.v | 12 +- theories/normedtype.v | 132 ++++++++++------- theories/realfun.v | 6 +- theories/sequences.v | 2 +- theories/showcase/uniform_bigO.v | 2 +- theories/topology.v | 2 +- 11 files changed, 232 insertions(+), 196 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 698794d56c..b015aeeb50 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -5,6 +5,14 @@ ### Added ### Changed + + +- in `ereal.v`: + + definitions `ereal_dnbhs` and `ereal_nbhs` changed to use large inequality instead + of strict inequality +- in `normedtype.v`: + + definitions `pinfty_dnbhs` and `ninfty_nbhs` changed to use large inequality instead + of strict inequality ### Renamed diff --git a/theories/derive.v b/theories/derive.v index 95a059ab40..f71127db02 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1337,8 +1337,8 @@ have imf_sup : has_sup imf. split; first by exists (f a); apply/imageP; rewrite /= in_itv /= lexx. have [M [Mreal imfltM]] : bounded_set (f @` `[a, b]). by apply/compact_bounded/continuous_compact => //; exact: segment_compact. - exists (M + 1) => y /imfltM yleM. - by rewrite (le_trans _ (yleM _ _)) ?ler_norm ?ltrDl. + exists (M + 1); apply/ubP => y /imfltM/= yleM. + by rewrite (le_trans _ (yleM _ _)) ?lerDl ?ler_norm. have [|imf_ltsup] := pselect (exists2 c, c \in `[a, b]%R & f c = sup imf). move=> [c cab fceqsup]; exists c => // t tab; rewrite fceqsup. by apply/sup_upper_bound => //; exact/imageP. diff --git a/theories/ereal.v b/theories/ereal.v index 51a643a27c..bfc1f0d7a1 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -662,16 +662,17 @@ Local Open Scope classical_set_scope. Definition ereal_dnbhs (x : \bar R) : set_system (\bar R) := [set P | 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) : set_system (\bar R) := [set P | 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]. HB.instance Definition _ := hasNbhs.Build (\bar R) ereal_nbhs. + End ereal_nbhs. Section ereal_nbhs_instances. @@ -680,70 +681,53 @@ Context {R : numFieldType}. Global Instance ereal_dnbhs_filter : forall x : \bar R, ProperFilter (ereal_dnbhs x). Proof. -case=> [x||]. -- case: (Proper_dnbhs_numFieldType x) => x0 [//= xT xI xS]. - apply Build_ProperFilter' => //=; apply Build_Filter => //=. - move=> P Q lP lQ; exact: xI. - 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 ltrDl. - split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]]. +move=> [r| |]. +- by apply: Build_ProperFilter' => //=; exact: filter_not_empty. +- apply: Build_ProperFilter => [P [x [_ xP]]|]. + by exists x%:E; exact: xP. + apply: Build_Filter => /= [|P Q [r +] [s +] |P Q PQ [r [rr rP]]]. + by exists 0%R. - + have [MP0|MP0] := eqVneq MP 0%R. - have [MQ0|MQ0] := eqVneq MQ 0%R. - by exists 0%R; split => // x x0; split; - [apply/gtMP; rewrite MP0 | apply/gtMQ; 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. - 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. - 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 /= ge0 /=; split => //. - case=> [r| |//]. - * rewrite lte_fin/= num_max num_gt_max /= => /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. -- apply Build_ProperFilter. - + move=> P [M [Mr ltMP]]; exists (M - 1)%:E. - by apply: ltMP; rewrite lte_fin gtrDl oppr_lt0. - + split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]]. + + have [-> [_ rP] [sr sQ]|r0 [rr rP]] := eqVneq r 0%R. + exists `|s|%R; rewrite normr_real; split => // x sx; split. + by apply/rP/(le_trans _ sx); rewrite lee_fin. + by apply/sQ/(le_trans _ sx); rewrite lee_fin real_ler_normr ?lexx. + have [-> [_ sQ]|s0 [sr sQ]] := eqVneq s 0%R. + exists `|r|%R; rewrite normr_real; split => // x rx; split. + by apply/rP/(le_trans _ rx); rewrite lee_fin real_ler_normr ?lexx. + by apply/sQ/(le_trans _ rx); rewrite lee_fin. + have /andP[{}r0 {}s0]: ((0 < `|r|) && (0 < `|s|))%R by rewrite !normr_gt0 r0. + exists (Num.max (PosNum r0) (PosNum s0))%:num. + rewrite realE /= ge0 /=; split => // -[t|_|//]. + * rewrite lee_fin /= num_max num_ge_max /= => /andP[rx sx]; split. + by apply/rP; rewrite lee_fin (le_trans _ rx)// real_ler_normr ?lexx. + by apply/sQ; rewrite lee_fin (le_trans _ sx)// real_ler_normr ?lexx. + * by split; [exact/rP|exact/sQ]. + + by exists r; split => // ? /rP /PQ. +- apply: Build_ProperFilter => [P [x [_ xP]]|]. + + by exists (x - 1)%:E; apply: xP; rewrite lee_fin gerDl. + + split=> /= [|P Q [r +] [s +] |P Q PQ [r [rr rP]]]. * by exists 0%R. - * have [MP0|MP0] := eqVneq MP 0%R. - have [MQ0|MQ0] := eqVneq MQ 0%R. - by exists 0%R; split => // x x0; split; - [apply/ltMP; rewrite MP0 | apply/ltMQ; 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 lerNl oppr0. - apply ltMQ; rewrite (lt_le_trans xMQ) // lee_fin lerNl -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 lerNl -normrN. - by rewrite real_ler_normr ?realN // lexx. - by apply ltMQ; rewrite (lt_le_trans MPx) // lee_fin MQ0 lerNl 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 /= ge0 /=; split => //. - case=> [r|//|]. - - rewrite lte_fin ltrNr num_max num_gt_max => /andP[]. - rewrite ltrNr => MPx; rewrite ltrNr => MQx; split. - apply/ltMP; rewrite lte_fin (lt_le_trans MPx) //= lerNl -normrN. + * have [-> [_ rP] [sr sQ]|r0 [rr rP]] := eqVneq r 0%R. + exists (- `|s|)%R; rewrite realN normr_real; split => // x xs; split. + by apply/rP/(le_trans xs); rewrite lee_fin lerNl oppr0. + apply/sQ/(le_trans xs); rewrite lee_fin lerNl -normrN. + by rewrite real_ler_normr ?realN ?lexx. + have [-> [_ sQ]|s0 [sr sQ]] := eqVneq s 0%R. + exists (- `|r|)%R; rewrite realN normr_real; split => // x rx; split. + apply/rP/(le_trans rx); rewrite lee_fin lerNl -normrN. by rewrite real_ler_normr ?realN // lexx. - apply/ltMQ; rewrite lte_fin (lt_le_trans MQx) //= lerNl -normrN. - by rewrite real_ler_normr ?realN // lexx. - - by move=> _; split; [apply/ltMP | apply/ltMQ]. - * by exists M; split => // x /ltM /sPQ. + by apply/sQ/(le_trans rx); rewrite lee_fin lerNl oppr0. + have /andP[{}r0 {}s0]: ((0 < `|r|) && (0 < `|s|))%R by rewrite !normr_gt0 r0. + exists (- (Num.max (PosNum r0) (PosNum s0))%:num)%R. + rewrite realN realE /= ge0 /=; split => // -[t|//|_]. + - rewrite lee_fin lerNr num_max num_ge_max => /andP[]. + rewrite lerNr => rx; rewrite lerNr => sx; split. + apply/rP; rewrite lee_fin (le_trans rx) //= lerNl -normrN. + by rewrite real_ler_normr ?realN ?lexx. + apply/sQ; rewrite lee_fin (le_trans sx) //= lerNl -normrN. + by rewrite real_ler_normr ?realN ?lexx. + - by split; [exact/rP|exact/sQ]. + * by exists r; split => // ? /rP /PQ. Qed. Typeclasses Opaque ereal_dnbhs. @@ -765,13 +749,19 @@ Context (R : numFieldType). Implicit Type (r : R). Lemma ereal_nbhs_pinfty_gt r : r \is Num.real -> \forall x \near +oo, r%:E < x. -Proof. by exists r. Qed. +Proof. +exists (r + 1)%R; split=> [|y]; first by rewrite realD. +by apply: lt_le_trans; rewrite EFinD lte_fin ltr_addl. +Qed. Lemma ereal_nbhs_pinfty_ge r : r \is Num.real -> \forall x \near +oo, r%:E <= x. Proof. by exists r; split => //; apply: ltW. Qed. Lemma ereal_nbhs_ninfty_lt r : r \is Num.real -> \forall x \near -oo, r%:E > x. -Proof. by exists r. Qed. +Proof. +exists (r - 1)%R; split=> [|y]; first by rewrite realB. +by move=> /le_lt_trans; apply; rewrite lte_fin ltr_subl_addl ltr_addr. +Qed. Lemma ereal_nbhs_ninfty_le r : r \is Num.real -> \forall x \near -oo, r%:E >= x. Proof. by exists r; split => // ?; apply: ltW. Qed. @@ -808,32 +798,34 @@ move: p => -[p| [M [Mreal MA]] | [M [Mreal MA]]] //=. apply/nbhs_ballP; exists (e%:num / 2) => //= r per. apply/nbhs_ballP; exists (e%:num / 2) => //= x rex. apply/ballA/(@ball_splitl _ _ r) => //; exact/ball_sym. -- exists (M + 1)%R; split; first by rewrite realD. - move=> -[x| _ |_] //=; last by exists M. - rewrite lte_fin => M'x /=. - apply/nbhs_ballP; exists 1%R => //= y x1y. - apply MA; rewrite lte_fin. - rewrite addrC -ltrBrDl in M'x. - rewrite (lt_le_trans M'x) // lerBlDl addrC -lerBlDl. - rewrite (le_trans _ (ltW x1y)) // real_ler_norm // realB //. - rewrite ltrBrDr in M'x. - rewrite -comparabler0 (@comparabler_trans _ (M + 1)%R) //. - by rewrite /Order.comparable (ltW M'x) orbT. - by rewrite comparabler0 realD. - by rewrite num_real. (* where we really use realFieldType *) -- exists (M - 1)%R; split; first by rewrite realB. - move=> -[x| _ |_] //=; last by exists M. - rewrite lte_fin => M'x /=. - apply/nbhs_ballP; exists 1%R => //= y x1y. - apply MA; rewrite lte_fin. - rewrite ltrBrDl in M'x. - rewrite (le_lt_trans _ M'x) // addrC -lerBlDl. - rewrite (le_trans _ (ltW x1y)) // distrC real_ler_norm // realB //. +- exists (M + 1)%R; split; first by rewrite realD // real1. + move=> -[x| _ |] //=. + rewrite lee_fin => M'x /=. + apply/nbhs_ballP; exists 1%R => //= y x1y. + apply MA; rewrite lee_fin. + rewrite addrC -lerBrDl in M'x. + rewrite (le_trans M'x) // lerBlDl addrC -lerBlDl. + rewrite (le_trans _ (ltW x1y)) // real_ler_norm // realB //. + rewrite lerBrDr in M'x. + rewrite -comparabler0 (@comparabler_trans _ (M + 1)%R) //. + by rewrite /Order.comparable M'x orbT. + by rewrite comparabler0 realD // real1. by rewrite num_real. (* where we really use realFieldType *) - rewrite addrC -ltrBrDr in M'x. - rewrite -comparabler0 (@comparabler_trans _ (M - 1)%R) //. - by rewrite /Order.comparable (ltW M'x). - by rewrite comparabler0 realB. + by exists M. +- exists (M - 1)%R; split; first by rewrite realB // real1. + move=> -[x| _ |] //=. + rewrite lee_fin => M'x /=. + apply/nbhs_ballP; exists 1%R => //= y x1y. + apply MA; rewrite lee_fin. + rewrite lerBrDl in M'x. + rewrite (le_trans _ M'x) // addrC -lerBlDl. + rewrite (le_trans _ (ltW x1y)) // distrC real_ler_norm // realB //. + by rewrite num_real. (* where we really use realFieldType *) + rewrite addrC -lerBrDr in M'x. + rewrite -comparabler0 (@comparabler_trans _ (M - 1)%R) //. + by rewrite /Order.comparable M'x. + by rewrite comparabler0 realB // real1. + by exists M. Qed. End ereal_topologicalType. @@ -857,19 +849,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 lteNl | rewrite oppeK]. + by exists (- x); [apply MS; rewrite leeNl | 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 lteNr|rewrite oppeK]. + exists (- y); by [apply Mx; rewrite leeNr|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 lteNr | rewrite oppeK]. + by exists (- x); [apply MS; rewrite leeNr | 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 lteNl|rewrite oppeK]. + exists (- y); by [apply Mx; rewrite leeNl|rewrite oppeK]. Qed. Lemma nbhsNKe (R : realFieldType) (z : \bar R) (A : set (\bar R)) : @@ -1070,12 +1062,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 ?ltrBlDl ?ltrDr // 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 ltrBlDl ltrDr. + by rewrite subr_ge0 ler_pdivrMr// 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_ltB// ltr_pdivrMr// ltr_pMr// ltr1n. +by rewrite ger0_norm ?subr_ge0// lerBlDl addrC -lerBlDl subrr. Qed. Lemma nbhs_oo_down_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num <= 1)%R -> @@ -1338,11 +1333,12 @@ rewrite predeq2E => x A; split. by rewrite subr_gt0 (le_lt_trans _ (contract_lt1 M)) // ler_norm. case=> [r| |]/= /xsectionP/=. * 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 ltrBlDr addrC addrCA addrC -ltrBlDr subrr subr_gt0 in rM1. - by rewrite -lte_fin -lt_contract. + rewrite ltrBlDr addrC addrCA addrC -ltrBlDr subrr in rM1. + rewrite subr_gt0 in rM1. + by rewrite -lee_fin -le_contract ltW. * by rewrite /ereal_ball /= subrr normr0 => h; exact: MA. * rewrite /ereal_ball /= opprK => h {MA}. exfalso. @@ -1356,12 +1352,12 @@ rewrite predeq2E => x A; split. by move: (contract_lt1 M); rewrite ltr_norml => /andP[]. case=> [r| |] /xsectionP/=. * rewrite /ereal_ball => /= rM1. - apply: MA; rewrite lte_fin. + apply MA; rewrite lee_fin. rewrite ler0_norm in rM1; last first. rewrite lerBlDl addr0 ltW //. by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. rewrite opprB opprK -ltrBlDl 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. @@ -1422,23 +1418,23 @@ Lemma cvg_ereal_loc_seq (R : realType) (x : \bar R) : Proof. move=> P; rewrite /ereal_loc_seq. case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 first. - have /natrP[N Nfloor] : Num.floor (Num.max d 0%R) \is a Num.nat. - by rewrite Znat_def floor_ge0 le_max lexx orbC. - exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin. - have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_max lexx. - apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor. - by rewrite natr1 mulrz_nat ler_nat. - have /natrP[N Nfloor] : Num.floor (Num.max (- d)%R 0%R) \is a Num.nat. + have /ZnatP [N Nfloor] : Num.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_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx. + apply; apply: le_trans (ltW (lt_succ_floor _)) _. + by rewrite Nfloor ler_nat addn1. + have /ZnatP [N Nfloor] : Num.floor (Num.max (- d)%R 0%R) \is a Znat. by rewrite Znat_def floor_ge0 le_max lexx orbC. - exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin ltrNl. - have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_max lexx. - apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor. - by rewrite natr1 mulrz_nat ler_nat. -have /natrP[N Nfloor] : Num.floor d%:num^-1 \is a Num.nat. + 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_floor _)) _. + by rewrite Nfloor ler_nat addn1. +have /ZnatP [N Nfloor] : Num.floor d%:num^-1 \is a Znat. by rewrite Znat_def floor_ge0. exists N => // n leNn; apply: dP; last first. by rewrite eq_sym addrC -subr_eq subrr eq_sym; exact/invr_neq0/lt0r_neq0. rewrite /= opprD addrA subrr distrC subr0 gtr0_norm; last by rewrite invr_gt0. rewrite -[ltLHS]mulr1 ltr_pdivrMl // -ltr_pdivrMr // div1r. -by rewrite (lt_le_trans (lt_succ_floor _))// Nfloor !natr1 mulrz_nat ler_nat. +by rewrite (lt_le_trans (lt_succ_floor _))// Nfloor -intrD1 lerD2r ler_nat. Qed. diff --git a/theories/exp.v b/theories/exp.v index de5bbfc1c3..8f1fd4eabf 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -70,7 +70,7 @@ apply: series_le_cvg Kzxn _ _ => [//=| /= n|]. rewrite !normrM normr_id mulrAC mulfK // normr_eq0 expf_eq0 andbC. by case: ltrgt0P zLx; rewrite //= normr_lt0. do! (apply: ler_pM || apply: mulr_ge0 || rewrite invr_ge0) => //. - by apply Kf => //; rewrite (lt_le_trans _ (ler_norm _))// ltrDl. + by apply Kf => //; rewrite (le_trans _ (ler_norm _))// lerDl. have F : `|z / x| < 1. by rewrite normrM normfV ltr_pdivrMr ?mul1r // (le_lt_trans _ zLx). rewrite (_ : (fun _ => _) = geometric `|K + 1| `|z / x|); last first. diff --git a/theories/landau.v b/theories/landau.v index f3cf00dfc7..6e185569d4 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -480,8 +480,8 @@ split=> [[k k0 fOg] | [k [kreal fOg]]]. exists k; rewrite realE (ltW k0) /=; split=> // l ltkl; move: fOg. by apply: filter_app; near=> x => /le_trans; apply; rewrite ler_wpM2r // ltW. exists (Num.max 1 `|k + 1|) => //. -apply: fOg; rewrite (@lt_le_trans _ _ `|k + 1|) //. - by rewrite (@lt_le_trans _ _ (k + 1)) ?ltrDl // real_ler_norm ?realD. +apply: fOg; rewrite (@le_trans _ _ `|k + 1|) //. + by rewrite (@le_trans _ _ (k + 1)) ?lerDl// real_ler_norm ?realD. by rewrite comparable_le_max ?real_comparable// lexx orbT. Unshelve. end_near. Qed. @@ -679,9 +679,11 @@ Notation "[o_ x e 'of' f ]" := (mklittleo gen_tag x f e). (*Printing*) Notation "[o '_' x e 'of' f ]" := (the_littleo _ _ (PhantomF x) f e). -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; split => // k kgt0; apply: littleoP. Qed. +Lemma eqoO (F : filter_on T) (f : T -> V) (e : T -> W) : [o_F e of f] =O_F e. +Proof. +apply/eqOP; exists 1; split => // k kge1; apply: littleoP. +by rewrite (lt_le_trans _ kge1). +Qed. Hint Resolve eqoO : core. (* NB: duplicate from Section Domination *) @@ -1116,10 +1118,10 @@ rewrite -linearB opprD addrC addrNK linearN normrN; near: y. suff flip : \forall k \near +oo, forall x, `|f x| <= k * `|x|. near +oo => k; near=> y. rewrite (le_lt_trans (near flip k _ _)) // -ltr_pdivlMl; last first. - by near: k; exists 0. + by near: k; exact: nbhs_pinfty_gt. near: y; apply/nbhs_normP. eexists; last by move=> ?; rewrite /= sub0r normrN; apply. - by rewrite /= mulr_gt0 // invr_gt0; near: k; exists 0. + by rewrite /= mulr_gt0 // invr_gt0; near: k; exact: nbhs_pinfty_gt. have /nbhs_normP [_/posnumP[d]] := Of1. rewrite /cst [X in _ * X]normr1 mulr1 => fk; near=> k => y. case: (ler0P `|y|) => [|y0]. @@ -1131,7 +1133,7 @@ rewrite -(ler_pM2l [gt0 of k0%:num]) mulr1 mulrA -[_ / _]ger0_norm //. rewrite -normm_s. rewrite -linearZ fk //= /= distrC subr0 normrZ ger0_norm //. rewrite invfM mulrA mulfVK ?lt0r_neq0 // ltr_pdivrMr //. -by rewrite -ltr_pdivrMl//. +by rewrite -ltr_pdivrMl. Unshelve. all: by end_near. Qed. End Linear3. @@ -1337,7 +1339,7 @@ rewrite (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(W1 * W2) x|)) //. rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //. rewrite ler_pdivlMl // (mulrA k1%:num) mulrCA (@normrM _ (W1 x)). by rewrite ler_pM ?mulr_ge0 //; near: x. -by rewrite ler_wpM2r // ltW //. +by rewrite ler_wpM2r // ltW. Unshelve. all: by end_near. Qed. End big_omega_in_R. @@ -1499,7 +1501,7 @@ rewrite [`|_|]normrM (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(T1 * T2) x|)) / rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //. rewrite ler_pdivlMl // (mulrA k1%:num) mulrCA (@normrM _ (T1 x)) ler_pM //; by [rewrite mulr_ge0 //|near: x]. -by rewrite ler_wpM2r // ltW //. +by rewrite ler_wpM2r // ltW. Unshelve. all: by end_near. Qed. End big_theta_in_R. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 1a4f1f28b4..dbd38bd40e 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -445,7 +445,7 @@ Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun f. Proof. have /finite_seqP[r fr] := fimfunP f. exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)). -split; rewrite ?num_real// => x mx z _; apply/ltW/(le_lt_trans _ mx). +split; rewrite ?num_real// => x mx z _; apply/(le_trans _ mx). have ? : f z \in r by have := imageT f z; rewrite fr. rewrite -[leLHS]/(fine `|f z|%:E) fine_le//. have := @bigmaxe_fin_num _ (map normr r) `|f z|. @@ -3116,7 +3116,7 @@ apply/le_lt_trans/ge0_le_integral => //. - apply/emeasurable_funM => //; apply/measurableT_comp => //. exact: measurable_int gi. - move=> x Dx; rewrite lee_wpmul2r//= lee_fin Mh//=. - by rewrite (lt_le_trans _ (ler_norm _))// ltrDl. + by rewrite (le_trans _ (ler_norm _))// lerDl. Qed. Lemma integrableMl f (h : T -> R) : @@ -4958,7 +4958,7 @@ Proof. move=> Afin mfA bdA; apply/integrableP; split; first exact/EFin_measurable_fun. have [M [_ mrt]] := bdA; apply: le_lt_trans. apply: (integral_le_bound (`|M| + 1)%:E) => //; first exact: measurableT_comp. - by apply: aeW => z Az; rewrite lee_fin mrt// ltr_pwDr// ler_norm. + by apply: aeW => z Az; rewrite lee_fin mrt// ler_wpDr// ler_norm. by rewrite lte_mul_pinfty. Qed. @@ -5052,7 +5052,7 @@ Lemma compact_finite_measure (A : set R^o) : compact A -> mu A < +oo. Proof. move=> /[dup]/compact_measurable => mA /compact_bounded[N [_ N1x]]. have AN1 : (A `<=` `[- (`|N| + 1), `|N| + 1])%R. - by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_pwDr// ler_norm. + by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ler_wpDr// ler_norm. rewrite (le_lt_trans (le_measure _ _ _ AN1)) ?inE//=. by rewrite lebesgue_measure_itv/= lte_fin gtrN// EFinD ltry. Qed. @@ -5110,7 +5110,7 @@ have mg : measurable_fun E g by exact: measurable_funTS. have [M Mpos Mbd] : (exists2 M, 0 < M & forall x, `|g x| <= M)%R. have [M [_ /= bdM]] := simple_bounded g. exists (`|M| + 1)%R; first exact: ltr_pwDr. - by move=> x; rewrite bdM// ltr_pwDr// ler_norm. + by move=> x; rewrite bdM// ler_wpDr// ler_norm. have [] // := @measurable_almost_continuous _ _ mE _ g (eps%:num / 2 / (M *+ 2)). by rewrite divr_gt0// mulrn_wgt0. move=> A [cptA AE /= muAE ctsAF]. @@ -5124,7 +5124,7 @@ move=> h [gh ctsh hbdM]; have mh : measurable_fun E h. have intg : mu.-integrable E (EFin \o h). apply: measurable_bounded_integrable => //. exists M; split; rewrite ?num_real // => x Mx y _ /=. - by rewrite (le_trans _ (ltW Mx)). + by rewrite (le_trans _ Mx). exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans. pose fgh x := `|(f x - g x)%:E| + `|(g x - h x)%:E|. apply: (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //. diff --git a/theories/normedtype.v b/theories/normedtype.v index 98739bc33c..fadb914498 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -341,13 +341,12 @@ Qed. #[global] Hint Extern 0 (ProperFilter _^') => (apply: Proper_dnbhs_numFieldType) : typeclass_instances. -(** Some Topology on extended real numbers *) - Definition pinfty_nbhs (R : numFieldType) : set_system R := - fun P => exists M, M \is Num.real /\ forall x, M < x -> P x. + fun P => exists M, M \is Num.real /\ forall x, M <= x -> P x. Arguments pinfty_nbhs R : clear implicits. + Definition ninfty_nbhs (R : numFieldType) : set_system R := - fun P => exists M, M \is Num.real /\ forall x, x < M -> P x. + fun P => exists M, M \is Num.real /\ forall x, x <= M -> P x. Arguments ninfty_nbhs R : clear implicits. Notation "+oo_ R" := (pinfty_nbhs R) @@ -365,11 +364,11 @@ Implicit Types r : R. Global Instance proper_pinfty_nbhs : ProperFilter (pinfty_nbhs R). Proof. apply Build_ProperFilter. - by move=> P [M [Mreal MP]]; exists (M + 1); apply MP; rewrite ltrDl. + by move=> P [M [Mreal MP]]; exists (M + 1); apply MP; rewrite lerDl. split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]]. - by exists 0. - exists (maxr MP MQ); split=> [|x]; first exact: max_real. - by rewrite comparable_gt_max ?real_comparable // => /andP[/gtMP ? /gtMQ]. + by rewrite comparable_ge_max ?real_comparable // => /andP[/gtMP ? /gtMQ]. - by exists M; split => // ? /gtM /sPQ. Qed. @@ -377,25 +376,31 @@ Global Instance proper_ninfty_nbhs : ProperFilter (ninfty_nbhs R). Proof. apply Build_ProperFilter. move=> P [M [Mr ltMP]]; exists (M - 1). - by apply: ltMP; rewrite gtrDl oppr_lt0. + by apply: ltMP; rewrite lerBlDl lerDr. split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]]. - by exists 0. - exists (Num.min MP MQ); split=> [|x]; first exact: min_real. - by rewrite comparable_lt_min ?real_comparable // => /andP[/ltMP ? /ltMQ]. + by rewrite comparable_le_min ?real_comparable // => /andP[/ltMP ? /ltMQ]. - by exists M; split => // x /ltM /sPQ. Qed. Lemma nbhs_pinfty_gt r : r \is Num.real -> \forall x \near +oo, r < x. -Proof. by exists r. Qed. +Proof. +move=> realr; exists (r + 1); split; first by rewrite realD. +by move=> x; apply: lt_le_trans; rewrite ltr_addl. +Qed. Lemma nbhs_pinfty_ge r : r \is Num.real -> \forall x \near +oo, r <= x. -Proof. by exists r; split => //; apply: ltW. Qed. +Proof. by exists r. Qed. Lemma nbhs_ninfty_lt r : r \is Num.real -> \forall x \near -oo, r > x. -Proof. by exists r. Qed. +Proof. +move=> r0; exists (r - 1); split; first by rewrite realB//. +by move=> x /le_lt_trans; apply; rewrite ltr_subl_addl ltr_addr. +Qed. Lemma nbhs_ninfty_le r : r \is Num.real -> \forall x \near -oo, r >= x. -Proof. by exists r; split => // ?; apply: ltW. Qed. +Proof. by exists r. Qed. Lemma nbhs_pinfty_real : \forall x \near +oo, x \is @Num.real R. Proof. by apply: filterS (nbhs_pinfty_gt (@real0 _)); apply: gtr0_real. Qed. @@ -424,8 +429,9 @@ Proof. exact: pinfty_ex_gt. Qed. Lemma near_pinfty_div2 (A : set R) : (\forall k \near +oo, A k) -> (\forall k \near +oo, A (k / 2)). Proof. -move=> [M [Mreal AM]]; exists (M * 2); split; first by rewrite realM. -by move=> x; rewrite -ltr_pdivlMr //; exact: AM. +move=> [M [Mreal AM]]; exists (M * 2); split. + by rewrite realM // realE; apply/orP; left. +by move=> x; rewrite -ler_pdivlMr //; apply: AM. Qed. End infty_nbhs_instances. @@ -472,7 +478,7 @@ tfae; first by move=> Foo A Areal; apply: Foo; apply: nbhs_pinfty_ge. - by move=> Foo; near do apply: Foo => //. - by apply: filterS => ?; apply: filterS => ?; apply: ltW. case=> [A [AR AF]] P [x [xR Px]]; near +oo_R => B. -by near do [apply: Px; apply: (@lt_le_trans _ _ B) => //]; apply: AF. +by near do [apply: Px; apply: (@le_trans _ _ B) => //]; apply: AF. Unshelve. all: by end_near. Qed. Let cvgrNyPnum {F : set_system R} {FF : Filter F} : [<-> @@ -488,7 +494,7 @@ tfae; first by move=> Foo A Areal; apply: Foo; apply: nbhs_ninfty_le. - by move=> Foo; near do apply: Foo => //. - by apply: filterS => ?; apply: filterS => ?; apply: ltW. case=> [A [AR AF]] P [x [xR Px]]; near -oo_R => B. -by near do [apply: Px; apply: (@le_lt_trans _ _ B) => //]; apply: AF. +by near do [apply: Px; apply: (@le_trans _ _ B) => //]; apply: AF. Unshelve. all: end_near. Qed. Context {T} {F : set_system T} {FF : Filter F}. @@ -619,7 +625,7 @@ tfae; first by move=> Foo A Areal; apply: Foo; apply: ereal_nbhs_pinfty_ge. - by move=> Foo; near do apply: Foo => //. - by apply: filterS => ?; apply: filterS => ?; apply: ltW. case=> [A [AR AF]] P [x [xR Px]]; near +oo_R => B. -by near do [apply: Px; rewrite (@lt_le_trans _ _ B%:E) ?lte_fin//]; apply: AF. +by near do [apply: Px; rewrite (@le_trans _ _ B%:E) ?lee_fin//]; apply: AF. Unshelve. all: end_near. Qed. Let cvgeNyPnum {F : set_system \bar R} {FF : Filter F} : [<-> @@ -635,7 +641,7 @@ tfae; first by move=> Foo A Areal; apply: Foo; apply: ereal_nbhs_ninfty_le. - by move=> Foo; near do apply: Foo => //. - by apply: filterS => ?; apply: filterS => ?; apply: ltW. case=> [A [AR AF]] P [x [xR Px]]; near -oo_R => B. -by near do [apply: Px; rewrite (@le_lt_trans _ _ B%:E) ?lte_fin//]; apply: AF. +by near do [apply: Px; rewrite (@le_trans _ _ B%:E) ?lee_fin//]; apply: AF. Unshelve. all: end_near. Qed. Context {T} {F : set_system T} {FF : Filter F}. @@ -1832,7 +1838,7 @@ Lemma bounded_fun_has_ubound (T : Type) (R : realFieldType) (a : T -> R) : bounded_fun a -> has_ubound (range a). Proof. move=> [M [Mreal]]/(_ (`|M| + 1)). -rewrite (le_lt_trans (ler_norm _)) ?ltrDl// => /(_ erefl) aM. +rewrite (le_trans (ler_norm _)) ?lerDl// => /(_ erefl) aM. by exists (`|M| + 1) => _ [n _ <-]; rewrite (le_trans (ler_norm _))// aM. Qed. @@ -1856,8 +1862,8 @@ Proof. move=> [M [Mreal Ma]] [N [Nreal Nb]]. rewrite /bounded_fun/bounded_near; near=> x => y /= _. rewrite (le_trans (ler_normD _ _))// [x]splitr. -by rewrite lerD// (Ma, Nb)// ltr_pdivlMr//; - near: x; apply: nbhs_pinfty_gt; rewrite ?rpredM ?rpred_nat. +by rewrite lerD// (Ma, Nb)// ler_pdivlMr//; + near: x; apply: nbhs_pinfty_ge; rewrite ?rpredM ?rpred_nat. Unshelve. all: by end_near. Qed. Lemma bounded_locally (T : topologicalType) @@ -2932,9 +2938,9 @@ Lemma abse_continuous : continuous (@abse R). Proof. case=> [r|A /= [r [rreal rA]]|A /= [r [rreal rA]]]/=. - exact/(cvg_comp (@norm_continuous _ [the normedModType R of R^o] r)). -- by exists r; split => // y ry; apply: rA; rewrite (lt_le_trans ry)// lee_abs. -- exists (- r)%R; rewrite realN; split => // y; rewrite EFinN -lteNr => yr. - by apply: rA; rewrite (lt_le_trans yr)// -abseN lee_abs. +- by exists r; split => // y ry; apply: rA; rewrite (le_trans ry)// lee_abs. +- exists (- r)%R; rewrite realN; split => // y; rewrite EFinN -leeNr => yr. + by apply: rA; rewrite (le_trans yr)// -abseN lee_abs. Qed. Lemma cvg_abse f (a : \bar R) : f @ F --> a -> `|f x|%E @[x --> F] --> `|a|%E. @@ -2968,10 +2974,10 @@ move=> [s||]/=. by apply: near_fun => //=; apply: continuousM => //=; apply: cvg_cst. - rewrite gt0_muley ?lte_fin// => A [u [realu uA]]. exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW. - by move=> x rux; apply: uA; move: rux; rewrite EFinM lte_pdivrMl. + by move=> x rux; apply: uA; move: rux; rewrite EFinM lee_pdivrMl. - rewrite gt0_muleNy ?lte_fin// => A [u [realu uA]]. exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW. - by move=> x xru; apply: uA; move: xru; rewrite EFinM lte_pdivlMl. + by move=> x xru; apply: uA; move: xru; rewrite EFinM lee_pdivlMl. Unshelve. all: by end_near. Qed. Lemma cvgeMl f x y : y \is a fin_num -> @@ -3882,47 +3888,71 @@ 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 ?. - + by exists 0%R; split => // x /lt_le_trans; apply; rewrite leey. + + exists (y - 1)%R; rewrite num_real; split => //= x /le_lt_trans; apply. + by rewrite lte_fin ltrBlDr ltrDl. + + by exists 0%R; split => // x /le_lt_trans; apply; rewrite ltry. 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. -- by exists y; rewrite num_real. -- by move=> _; exists 0%R; split => // x; apply/le_lt_trans; rewrite leNye. +- exists (y + 1)%R; rewrite num_real; split => // x /lt_le_trans; apply. + by rewrite lte_fin ltrDl. +- by move=> _; exists 0%R; split => // x; apply/lt_le_trans; rewrite ltNyr. Qed. -Lemma open_ereal_lt_ereal x : open [set y | y < x]. +Let open_ereal_lt_real r : open (fun x => x < r%:E). Proof. -have openr r : open [set x : \bar R | x < r%:E]. - (* BUG: why doesn't case work? *) - move=> [? | // | ?]; [rewrite /= lte_fin => xy | by exists r]. +rewrite /open /=. +case => [? | // | ?]; [rewrite lte_fin => xy | exists (r - 1)%R]. by move: (@open_ereal_lt r%:E); rewrite openE; apply; rewrite /= lte_fin. -move: x => [ // | | ]; last by move=> []. (* same BUG *) +rewrite num_real; split => // x /le_lt_trans; apply. +by rewrite lte_fin ltrBlDr ltrDl. +Qed. + +Lemma open_ereal_lt_ereal x : open [set y | y < x]. +Proof. +suff: open [set y : \bar R | y < +oo]. + move=> ?; rewrite /open/=. + by case: x => [x | | [] // ] /=; first exact: open_ereal_lt_real. suff -> : [set y | y < +oo] = \bigcup_r [set y : \bar R | y < r%:E]. - exact: bigcup_open. + by apply: bigcup_open => ? _; exact: open_ereal_lt_real. rewrite predeqE => -[r | | ]/=. -- rewrite ltry; split => // _. +- rewrite ltey; split => // _. by exists (r + 1)%R => //=; rewrite lte_fin ltrDl. -- by rewrite ltxx; split => // -[] x /=; rewrite ltNge leey. -- by split => // _; exists 0%R => //=; rewrite ltNye. +- by rewrite ltxx; split => // -[] ? /=; rewrite ltNge leey. +- by split => // _; exists 0%R => //=; rewrite ltNyr. Qed. -Lemma open_ereal_gt_ereal x : open [set y | x < y]. +Let open_ereal_gt_real r : open (fun x => r%:E < x). Proof. -have openr r : open [set x | r%:E < x]. - move=> [? | ? | //]; [rewrite /= lte_fin => xy | by exists r]. +rewrite /open /=. +case => [? | ? | //]; [rewrite lte_fin => xy | exists (r + 1)%R]. by move: (@open_ereal_gt r%:E); rewrite openE; apply; rewrite /= lte_fin. -case: x => [ // | | ]; first by move=> []. +by rewrite num_real; split=> // x /lt_le_trans; apply; rewrite lte_fin ltrDl. +Qed. + +Lemma open_ereal_gt_ereal x : open [set y | x < y]. +Proof. +suff: open [set y : \bar R | -oo < y]. + move=> ?; rewrite /open/=. + case: x => [ | | [] // ] /=; first exact: open_ereal_gt_real. + rewrite (_ : [set y | +oo < y] = set0)//. + by rewrite predeqE => -[]. + move=> r _. + rewrite /nbhs/= /nbhs/= /nbhs_ball_/=. + by exists 1%R => //= ? _; rewrite ltNyr. + move=> _. + rewrite /nbhs/= /nbhs/= /nbhs_ball_/=. + by exists 1%R => //=; split => // ?; apply: lt_le_trans; rewrite ltNyr. suff -> : [set y | -oo < y] = \bigcup_r [set y : \bar R | r%:E < y]. - exact: bigcup_open. + by apply bigcup_open => ? _; exact: open_ereal_gt_real. rewrite predeqE => -[r | | ]/=. -- rewrite ltNyr; split => // _. +- rewrite ltNye; split => // _. by exists (r - 1)%R => //=; rewrite lte_fin ltrBlDr ltrDl. -- by split => // _; exists 0%R => //=; rewrite ltey. -- by rewrite ltxx; split => // -[] x _ /=; rewrite ltNge leNye. +- by split => // _; exists 0%R => //=; rewrite ltry. +- by rewrite ltxx; split => // -[] ? _ /=; rewrite ltNge leNye. Qed. Lemma closed_ereal_le_ereal y : closed [set x | y <= x]. @@ -4953,8 +4983,8 @@ have /Aco [] := covA. move=> D _ DcovA. exists (\big[maxr/0]_(i : D) (fsval i)%:~R). rewrite bigmax_real//; last by move=> ? _; rewrite realz. -split => // x ltmaxx p /DcovA [n Dn /lt_trans /(_ _)/ltW]. -apply; apply: le_lt_trans ltmaxx. +split => // x ltmaxx p /DcovA [n Dn /lt_le_trans /(_ _)/ltW]. +apply; apply: le_trans ltmaxx. have : n \in enum_fset D by []. by rewrite enum_fsetE => /mapP[/= i iD ->]; exact/le_bigmax. Qed. @@ -5026,7 +5056,7 @@ have Mnco : compact by move=> _; apply: segment_compact. apply: subclosed_compact Acl Mnco _ => v /normAltM normvleM i. suff : `|v ord0 i : R| <= M + 1 by rewrite ler_norml. -apply: le_trans (normvleM _ _); last by rewrite ltrDl. +apply: le_trans (normvleM _ _); last by rewrite lerDl. have /mapP[j Hj ->] : `|v ord0 i| \in [seq `|v x.1 x.2| | x : 'I_1 * 'I_n.+1]. by apply/mapP; exists (ord0, i) => //=; rewrite mem_enum. by rewrite [leRHS]/normr /= mx_normrE; apply/bigmax_geP; right => /=; exists j. @@ -5471,7 +5501,7 @@ split => [/(_ 1) [M Bf]|/linear_boundedP fr y]. by rewrite sub0r normrN => x1; exact/Bf/ltW. near +oo_R => r; exists (r * y) => x xe. rewrite (@le_trans _ _ (r * `|x|)) //; first by move: {xe} x; near: r. -by rewrite ler_pM //. +by rewrite ler_pM. Unshelve. all: by end_near. Qed. End LinearContinuousBounded. diff --git a/theories/realfun.v b/theories/realfun.v index d88ffe1741..37b0e4c0e8 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -91,7 +91,7 @@ Lemma cvg_addrl (M : R) : M + r @[r --> +oo] --> +oo. Proof. move=> P [r [rreal rP]]; exists (r - M); split. by rewrite realB// num_real. -by move=> m; rewrite ltrBlDl => /rP. +by move=> m; rewrite lerBlDl => /rP. Qed. (* NB: see cvg_addnr in topology.v *) @@ -455,7 +455,7 @@ have [Spoo|Spoo] := pselect (S +oo). have -> : l = +oo by rewrite /l /ereal_sup; exact: supremum_pinfty. rewrite -(cvg_shiftr `|N|); apply: cvg_near_cst. exists N; split; first by rewrite num_real. - by move=> x /ltW Nx; rewrite Nf// ler_wpDr. + by move=> x Nx; rewrite Nf// ler_wpDr. have [lpoo|lpoo] := eqVneq l +oo. rewrite lpoo; apply/cvgeyPge => M. have /ereal_sup_gt[_ [n _] <- Mun] : M%:E < l by rewrite lpoo// ltry. @@ -482,7 +482,7 @@ have xB r : (x <= r)%R -> B r. by move: xr; rewrite urnoo leeNy_eq; exact/negP. rewrite -(@fineK _ l)//; apply/fine_cvgP; split. exists x; split; first by rewrite num_real. - by move=> r A1r; rewrite f_fin_num //; exact/xB/ltW. + by move=> r A1r; rewrite f_fin_num //; exact/xB. set g := fun n => if (n < x)%R then fine (f x) else fine (f n). have <- : sup (range g) = fine l. apply: EFin_inj; rewrite -ereal_sup_EFin//; last 2 first. diff --git a/theories/sequences.v b/theories/sequences.v index 16fcdc52eb..1fe21394d4 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -2288,7 +2288,7 @@ move=> cf; have [M [Mreal Mu]] := cvg_seq_bounded cf. apply: nonincreasing_is_cvgn. exact/nonincreasing_sups/bounded_fun_has_ubound/cvg_seq_bounded. exists (- (M + 1)) => _ [n _ <-]; rewrite (@le_trans _ _ (u n)) //. - by apply/lerNnormlW/Mu => //; rewrite ltrDl. + by apply/lerNnormlW/Mu => //; rewrite lerDl. apply: sup_ubound; last by exists n => /=. exact/has_ubound_sdrop/bounded_fun_has_ubound/cvg_seq_bounded. Qed. diff --git a/theories/showcase/uniform_bigO.v b/theories/showcase/uniform_bigO.v index 1eb7e8bf72..e8f9a2d0c1 100644 --- a/theories/showcase/uniform_bigO.v +++ b/theories/showcase/uniform_bigO.v @@ -101,7 +101,7 @@ Unshelve. all: by end_near. Qed. Lemma OuO_to_P f g : OuO f g -> OuP f g. Proof. move=> fOg; apply/Ouex_to_P; move: fOg => /eqOP [k [kreal hk]]. -have /hk [Q [->]] : k < maxr 1 (k + 1) by rewrite lt_max ltrDl orbC ltr01. +have /hk [Q [->]] : k <= maxr 1 (k + 1) by rewrite le_max lerDl orbC ler01. move=> [R [[_/posnumP[e1] Re1] [_/posnumP[e2] Re2]] sRQ] fOg. exists (minr e1%:num e2%:num) => //. exists (maxr 1 (k + 1)); first by rewrite lt_max ltr01. diff --git a/theories/topology.v b/theories/topology.v index 1130813b33..4365f45e49 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -590,7 +590,7 @@ Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). Local Notation ph := (phantom _). Definition prop_near1 {X} {fX : filteredType X} (x : fX) - P (phP : ph {all1 P}) := nbhs x P. + P (phP : ph {all1 P}) := nbhs x P. Definition prop_near2 {X X'} {fX : filteredType X} {fX' : filteredType X'} (x : fX) (x' : fX') := fun P of ph {all2 P} =>