From 929ac77c706ccfd31bea636c2e7c82df74ed5f7b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 1 Jul 2024 14:39:18 +0900 Subject: [PATCH] floor/ceil not notations anymore --- CHANGELOG_UNRELEASED.md | 10 +++--- classical/mathcomp_extra.v | 5 +++ theories/altreals/realsum.v | 10 +++--- theories/ereal.v | 28 ++++++++-------- theories/lebesgue_integral.v | 4 +-- theories/measure.v | 8 ++--- theories/normedtype.v | 2 +- theories/realfun.v | 14 ++++---- theories/reals.v | 62 +++++++++++++++--------------------- theories/sequences.v | 2 +- theories/topology.v | 20 +++++++----- 11 files changed, 81 insertions(+), 84 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4fb22e3961..432a61c508 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -6,16 +6,16 @@ - in `reals.v`: + lemma `mem_rg1_floor` + + lemma `ge_floor` - in `mathcomp_extra.v`: - + lemmas `intr1`, `int1r` + + lemmas `intr1`, `int1r`, `natr_def` ### Changed - in `reals.v`: - + definition `floor` now a notation (in `real_scope`) - + definition `ceil` now a notation (in `real_scope`) + definitions `Rceil`, `Rfloor` + + `lt_succ_floor`: conclusion changed to match `lt_succ_floor` in MathComp ### Renamed @@ -29,8 +29,8 @@ ### Removed - in `reals.v`: - + `lt_succ_floor` renamed to `__deprecated__lt_succ_floor` - (use `lt_succ_floor` from MathComp instead) + + definition `floor` (use `Num.floor` instead) + + definition `ceil` (use `Num.ceil` instead) ### Infrastructure diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 32e15d43e5..81c0235446 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -380,3 +380,8 @@ Proof. by rewrite intrD. Qed. Lemma int1r {R : ringType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R. Proof. by rewrite intrD. Qed. + +From mathcomp Require Import archimedean. + +Lemma natr_def (n : int) : (n \is a Num.nat) = (0 <= n)%R. +Proof. by []. Qed. diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v index 5c35bc01d7..7f8f5e86a6 100644 --- a/theories/altreals/realsum.v +++ b/theories/altreals/realsum.v @@ -142,16 +142,16 @@ Proof. case/summableP=> M ge0_M bM; pose E (p : nat) := [pred x | `|f x| > 1 / p.+1%:~R]. set F := [pred x | _]; have le: {subset F <= [pred x | `[< exists p, x \in E p >]]}. move=> x; rewrite !inE => nz_fx. - pose j := `|(floor (1 / `|f x|))%real|%N; exists j; rewrite inE. + pose j := `|Num.floor (1 / `|f x|)|%N; exists j; rewrite inE. rewrite ltr_pdivrMr ?ltr0z // -ltr_pdivrMl ?normr_gt0 //. rewrite mulr1 /j div1r -addn1 /= PoszD intrD mulr1z. rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0//. - by rewrite intr1 lt_succ_floor// num_real. + by rewrite intr1 reals.lt_succ_floor. apply/(countable_sub le)/cunion_countable=> i /=. case: (existsTP (fun s : seq T => {subset E i <= s}))=> /= [[s le_Eis]|]. by apply/finite_countable/finiteP; exists s => x /le_Eis. -move/finiteNP; pose j := `|(floor (M / i.+1%:R))%real|.+1. -pose K := (`|(floor M)%real|.+1 * i.+1)%N; move/(_ K)/asboolP/exists_asboolP. +move/finiteNP; pose j := `|Num.floor (M / i.+1%:R)|.+1. +pose K := (`|Num.floor M|.+1 * i.+1)%N; move/(_ K)/asboolP/exists_asboolP. move=> h; have /asboolP[] := xchooseP h. set s := xchoose h=> eq_si uq_s le_sEi; pose J := [fset x in s]. suff: \sum_(x : J) `|f (val x)| > M by rewrite ltNge bM. @@ -161,7 +161,7 @@ apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first. rewrite sumr_const -cardfE card_fseq undup_id // eq_si -mulr_natr -pmulrn. rewrite mul1r natrM mulrCA mulVf ?mulr1 ?pnatr_eq0 //. have /andP[_] := mem_rg1_floor M; rewrite -addn1. -by rewrite natrD /= mulr1n pmulrn -{1}[(floor _)%real]gez0_abs // floor_ge0. +by rewrite natrD /= mulr1n pmulrn -{1}[Num.floor _]gez0_abs // floor_ge0. Qed. End SummableCountable. diff --git a/theories/ereal.v b/theories/ereal.v index d3d5b59c18..cde34729e5 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -1266,7 +1266,7 @@ rewrite predeq2E => x A; split. case=> [r' /= re'r'| |]/=. * rewrite /ereal_ball in re'r'. have [r'r|rr'] := lerP (contract r'%:E) (contract r%:E). - apply: reA; rewrite /ball /= real_ltr_norml // ?num_real //. + apply: reA; rewrite /ball /= ltr_norml//. rewrite ger0_norm ?subr_ge0// in re'r'. have : (contract (r%:E - e%:num%:E) < contract r'%:E)%R. move: re'r'; rewrite /e' lt_min => /andP[+ _]. @@ -1276,7 +1276,7 @@ rewrite predeq2E => x A; split. rewrite ltrBlDr addrC -ltrBlDr => ->; rewrite andbT. rewrite (@lt_le_trans _ _ 0%R)// 1?ltrNl 1?oppr0// subr_ge0. by rewrite -lee_fin -le_contract. - apply: reA; rewrite /ball /= real_ltr_norml // ?num_real //. + apply: reA; rewrite /ball /= ltr_norml//. rewrite ltr0_norm ?subr_lt0// opprB in re'r'. apply/andP; split; last first. by rewrite (@lt_trans _ _ 0%R) // subr_lt0 -lte_fin -lt_contract. @@ -1402,24 +1402,24 @@ 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 /ZnatP[N Nfloor] : (floor (Num.max d 0%R))%real \is a Znat. - by rewrite Znat_def floor_ge0 le_max lexx orbC. + have /natrP[N Nfloor] : Num.floor (Num.max d 0%R) \is a Num.nat. + by rewrite natr_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 _)) ?num_real//. - by rewrite Nfloor ler_nat addn1. - have /ZnatP [N Nfloor] : (floor (Num.max (- d)%R 0%R))%real \is a Znat. - by rewrite Znat_def floor_ge0 le_max lexx orbC. + apply; rewrite (lt_le_trans (reals.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. + by rewrite natr_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 _)) ?num_real//. - by rewrite Nfloor ler_nat addn1. -have /ZnatP[N Nfloor] : (floor d%:num^-1)%real \is a Num.nat. - by rewrite Znat_def floor_ge0. + apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor. + by rewrite natr1 mulrz_nat ler_nat. +have /natrP[N Nfloor] : Num.floor d%:num^-1 \is a Num.nat. + by rewrite natr_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. -rewrite (lt_le_trans (lt_succ_floor _)) ?num_real// Nfloor. -by rewrite -intr1 lerD// ler_nat. +rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor. +by rewrite !natr1 mulrz_nat ler_nat. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 82643e2b43..e1a6c3c562 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1302,7 +1302,7 @@ rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|]. rewrite ler_pdivrMr// (le_trans _ (ge_floor _)) ?num_real//. by rewrite -(@gez0_abs (floor _)%real)// floor_ge0 mulr_ge0// (le_trans _ nr). rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _)) ?num_real//. - rewrite -[in leRHS]natr1 -intr1 lerD2r// -(@gez0_abs (floor _)%real) ?num_real// floor_ge0. + rewrite -[in leRHS]natr1 -intr1 lerD2r// -(@gez0_abs (floor _)%real)// floor_ge0. by rewrite mulr_ge0// (le_trans _ nr). - rewrite -bigcup_seq => -[/= k] /[!mem_index_iota] /andP[nk kn]. rewrite in_itv /= => /andP[knr rkn]; rewrite in_itv /=; apply/andP; split. @@ -1543,7 +1543,7 @@ have : fine (f x) < n%:R. rewrite -(@ler_nat R); apply: lt_le_trans. rewrite -natr1 (_ : `| _ |%:R = (floor (fine (f x)))%real%:~R); last first. by rewrite -[in RHS](@gez0_abs (floor _)%real)// floor_ge0//; exact/fine_ge0/f0. - by rewrite intr1 lt_succ_floor ?num_real. + by rewrite intr1 reals.lt_succ_floor. rewrite -lte_fin (fineK fxfin) => fxn. have [approx_nx0|[k [/andP[k0 kn2n] ? ->]]] := f_ub_approx fxn. by have := Hm _ mn; rewrite approx_nx0. diff --git a/theories/measure.v b/theories/measure.v index 11b3277292..0aac5f29c9 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect all_algebra finmap. +From mathcomp Require Import all_ssreflect all_algebra archimedean finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop. Require Import reals ereal signed topology normedtype sequences esum numfun. @@ -2198,8 +2198,8 @@ Lemma infinite_card_dirac (A : set T) : infinite_set A -> \esum_(i in A) \d_ i A = +oo :> \bar R. Proof. move=> infA; apply/eqyP => r r0. -have [B BA Br] := infinite_set_fset `|(ceil r)%real| infA. -apply: esum_ge; exists [set` B] => //; apply: (@le_trans _ _ `|(ceil r)%real|%:R%:E). +have [B BA Br] := infinite_set_fset `|ceil r| infA. +apply: esum_ge; exists [set` B] => //; apply: (@le_trans _ _ `|ceil r|%:R%:E). by rewrite lee_fin natr_absz gtr0_norm ?ceil_gt0// ceil_ge. move: Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply. rewrite (eq_fsbigr (cst 1))/=; last first. @@ -2292,7 +2292,7 @@ move=> F mF tF mUF; rewrite [X in X @ \oo --> _](_ : _ = (fun n => (r%:num)%:E * \sum_(0 <= i < n) m (F i))); last first. by apply/funext => k; rewrite ge0_sume_distrr. rewrite /mscale; have [->|r0] := eqVneq r%:num 0%R. - rewrite mul0e [X in X @ \oo --> _](_ : _ = (fun=> 0)); first exact: cvg_cst. + rewrite mul0e [X in X @ \oo --> _](_ : _ = cst 0); first exact: cvg_cst. by under eq_fun do rewrite mul0e. by apply: cvgeMl => //; exact: measure_semi_sigma_additive. Qed. diff --git a/theories/normedtype.v b/theories/normedtype.v index b8c49d1ee4..514f98887f 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5779,7 +5779,7 @@ rewrite ler_pdivlMr// mulrC -ler_pdivlMr//. have [f0|f0] := eqVneq 0 f. by move: mf; rewrite -f0 absz0 leNgt expnS ltr_nat leq_pmulr// expn_gt0. rewrite (le_trans mf)// prednK//; last by rewrite absz_gt0 eq_sym. -by rewrite natr_absz// ger0_norm// ge_floor// num_real. +by rewrite natr_absz// ger0_norm// reals.ge_floor. Qed. Lemma cover_vitali_collection_partition : diff --git a/theories/realfun.v b/theories/realfun.v index d22962658d..2e78a8ded5 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1,6 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap. +From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum archimedean. From mathcomp Require Import matrix interval zmodp vector fieldext falgebra. +From mathcomp Require Import finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality. Require Import ereal reals signed topology prodnormedzmodule normedtype derive. @@ -183,7 +184,7 @@ exists (fun n => sval (cid (He (PosNum (invn n))))). apply/cvgrPdist_lt => r r0; near=> t. rewrite /sval/=; case: cid => x [px xpt _]. rewrite distrC (lt_le_trans xpt)// -(@invrK _ r) lef_pV2 ?posrE ?invr_gt0//. - near: t; exists `|ceil (r^-1)|%real%N => // s /=. + near: t; exists `|ceil r^-1|%N => // s /=. rewrite -ltnS -(@ltr_nat R) => /ltW; apply: le_trans. by rewrite natr_absz gtr0_norm ?ceil_gt0 ?invr_gt0// ceil_ge. move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)). @@ -233,8 +234,8 @@ have y_p : y_ n @[n --> \oo] --> p. rewrite ltrBlDr => /lt_le_trans; apply. rewrite addrC lerD2r -(invrK e) lef_pV2// ?posrE ?invr_gt0//. near: t. - exists `|ceil e^-1|%real%N => // k /= ek. - rewrite (le_trans (ceil_ge _))// (@le_trans _ _ `|ceil e^-1|%real%:~R)//. + exists `|ceil e^-1|%N => // k /= ek. + rewrite (le_trans (ceil_ge _))// (@le_trans _ _ `|ceil e^-1|%:~R)//. by rewrite ger0_norm// ?ceil_ge0// ?invr_ge0// ltW. by move: ek;rewrite -(leq_add2r 1) !addn1 -(ltr_nat R) => /ltW. have /fine_cvgP[[m _ mfy_] /= _] := h _ (conj py_ y_p). @@ -1426,7 +1427,6 @@ Proof. by move=> fct fK; have [] := near_can_continuousAcan_sym fK fct. Qed. End real_inverse_functions. Section real_inverse_function_instances. - Variable R : realType. Lemma exprn_continuous n : continuous (@GRing.exp R ^~ n). @@ -2268,7 +2268,7 @@ have Nffin : TV a x (\- f) \is a fin_num. exact: (bounded_variationl ax xb). rewrite /pos_tv /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //. - rewrite addeAC oppeD //= ?fin_num_adde_defl //. - by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -Num.Theory.splitr. + by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -splitr. - by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split. - by apply: fin_num_adde_defl; rewrite fin_numN fin_numD; apply/andP; split. - by rewrite fin_numM // fin_numD; apply/andP; split. @@ -2343,7 +2343,7 @@ rewrite {1}variation_prev; last exact: itv_partition1. rewrite /= -addeA -lteBrDr; last by rewrite fin_numD; apply/andP. rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA. move/lt_trans; apply. -rewrite [x in (_ < x%:E)%E]Num.Theory.splitr EFinD addeC lteD2lE //. +rewrite [x in (_ < x%:E)%E]splitr EFinD addeC lteD2lE //. rewrite -addeA. apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E). rewrite [in leRHS]variation_prev; last exact: itv_partition1. diff --git a/theories/reals.v b/theories/reals.v index 0bd6ff6f78..c346fcab10 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -97,9 +97,7 @@ Implicit Types x : R. Lemma has_ub_image_norm E : has_ubound (normr @` E) -> has_ubound E. Proof. case => M /ubP uM; exists `|M|; apply/ubP => r rS. -rewrite (le_trans (real_ler_norm _)) ?num_real //. -rewrite (le_trans (uM _ _)) ?real_ler_norm ?num_real //. -by exists r. +by rewrite (le_trans (ler_norm _))// (le_trans (uM _ _))//; exact: ler_norm. Qed. Lemma has_inf_supN E : has_sup (-%R @` E) <-> has_inf E. @@ -238,13 +236,6 @@ Qed. End ToInt. (* -------------------------------------------------------------------- *) -Reserved Notation "'floor' r" (at level 10). -Notation "'floor' x" := (Num.floor x) : real_scope. - -Reserved Notation "'ceil' r" (at level 10). -Notation "'ceil' x" := (Num.ceil x) : real_scope. - -Local Open Scope real_scope. Section RealDerivedOps. Variable R : realType. @@ -344,14 +335,14 @@ have ABsup : has_sup [set x + y | x in A & y in B]. apply: le_anti; apply/andP; split. apply: sup_le_ub; first by case: ABsup. by move=> ? [p Ap [q Bq] <-]; apply: lerD; exact: sup_ub. -rewrite real_leNgt ?num_real// -subr_gt0; apply/negP. +rewrite leNgt -subr_gt0; apply/negP. set eps := (_ + _ - _) => epos. have e2pos : 0 < eps / 2%:R by rewrite divr_gt0// ltr0n. have [r Ar supBr] := sup_adherent e2pos supA. have [s Bs supAs] := sup_adherent e2pos supB. have := ltrD supBr supAs. rewrite -addrA [-_+_]addrC -addrA -opprD -splitr addrA /= opprD opprK addrA. -rewrite subrr add0r; apply/negP; rewrite -real_leNgt ?num_real//. +rewrite subrr add0r; apply/negP; rewrite -leNgt. by apply: sup_upper_bound => //; exists r => //; exists s. Qed. @@ -479,11 +470,14 @@ Proof. by rewrite inE; exists (floor x). Qed. Lemma RfloorE x : Rfloor x = (floor x)%:~R. Proof. by []. Qed. +Lemma lt_succ_floor x : x < (floor x + 1)%:~R. +Proof. by rewrite lt_succ_floor// num_real. Qed. + +Lemma ge_floor x : (floor x)%:~R <= x. +Proof. by rewrite ge_floor// num_real. Qed. + Lemma mem_rg1_floor x : (range1 (floor x)%:~R) x. -Proof. -rewrite /range1 /mkset intr1 lt_succ_floor ?num_real// andbT. -by rewrite ge_floor// num_real. -Qed. +Proof. by rewrite /range1 /mkset intr1 lt_succ_floor andbT ge_floor. Qed. Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x. Proof. by rewrite /Rfloor; exact: mem_rg1_floor. Qed. @@ -492,7 +486,7 @@ Lemma Rfloor_le x : Rfloor x <= x. Proof. by case/andP: (mem_rg1_Rfloor x). Qed. Lemma __deprecated__floor_le x : (floor x)%:~R <= x. -Proof. by rewrite ge_floor ?num_real. Qed. +Proof. by rewrite ge_floor. Qed. Lemma lt_succ_Rfloor x : x < Rfloor x + 1. Proof. by case/andP: (mem_rg1_Rfloor x). Qed. @@ -557,16 +551,17 @@ Proof. by rewrite floor0. Qed. Lemma floor1 : floor (1 : R) = 1. Proof. by rewrite floor1. Qed. -Lemma __deprecated__floor_ge0 x : (0 <= floor x) = (0 <= x). -Proof. by rewrite -floor_ge_int// num_real. Qed. +Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= floor x). +Proof. by rewrite Rfloor_ge_int RfloorE ler_int. Qed. + +Lemma floor_ge0 x : (0 <= floor x) = (0 <= x). +Proof. by rewrite -floor_ge_int. Qed. Lemma floor_le0 x : x <= 0 -> floor x <= 0. Proof. by move=> x0; rewrite -floor0 Num.Theory.floor_le. Qed. Lemma floor_lt0 x : x < 0 -> floor x < 0. -Proof. -by move=> x0; rewrite -(@ltrz0 R) (le_lt_trans (ge_floor _))// num_real. -Qed. +Proof. by move=> x0; rewrite -(@ltrz0 R) (le_lt_trans (ge_floor _)). Qed. Lemma le_floor : {homo @Num.floor R : x y / x <= y}. Proof. by move=> a b ab; rewrite Num.Theory.floor_le. Qed. @@ -574,34 +569,26 @@ Proof. by move=> a b ab; rewrite Num.Theory.floor_le. Qed. Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x >= 1). Proof. apply/idP/orP => [|[x0|/le_floor r1]]; first rewrite neq_lt => /orP[x0|x0]. -- by left; apply: contra_lt x0; rewrite -floor_ge_int ?num_real. -- by right; rewrite (le_trans _ (ge_floor _)) ?num_real// ler1z -gtz0_ge1. -- by rewrite lt_eqF//; apply: contra_lt x0; rewrite -floor_ge_int ?num_real. +- by left; apply: contra_lt x0; rewrite -floor_ge_int. +- by right; rewrite (le_trans _ (ge_floor _))// ler1z -gtz0_ge1. +- by rewrite lt_eqF//; apply: contra_lt x0; rewrite -floor_ge_int. - by rewrite gt_eqF// (lt_le_trans _ r1)// floor1. Qed. -Lemma __deprecated__lt_succ_floor x : x < (floor x)%:~R + 1. -Proof. by rewrite intr1 lt_succ_floor// num_real. Qed. - Lemma floor_lt_int x (z : int) : (x < z%:~R) = (floor x < z). Proof. by rewrite Rfloor_lt_int RfloorE ltr_int. Qed. -Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= floor x). -Proof. by rewrite Rfloor_ge_int RfloorE ler_int. Qed. - Lemma ltr_add_invr (y x : R) : y < x -> exists k, y + k.+1%:R^-1 < x. Proof. move=> yx; exists `|floor (x - y)^-1|%N. rewrite -ltrBrDl -{2}(invrK (x - y)%R) ltf_pV2 ?qualifE/= ?ltr0n//. by rewrite invr_gt0 subr_gt0. rewrite -natr1 natr_absz ger0_norm. - by rewrite -floor_ge_int ?num_real// invr_ge0 subr_ge0 ltW. -by rewrite intr1 lt_succ_floor ?num_real. + by rewrite -floor_ge_int// invr_ge0 subr_ge0 ltW. +by rewrite intr1 lt_succ_floor. Qed. End FloorTheory. -#[deprecated(since="mathcomp-analysis 1.3.0", note="use `floor_ge_int` instead")] -Notation floor_ge0 := __deprecated__floor_ge0 (only parsing). Section CeilTheory. Variable R : realType. @@ -638,6 +625,8 @@ Proof. by move=> ?; rewrite oppr_gt0 floor_lt0 // ltrNl oppr0. Qed. Lemma ceil_le0 x : x <= 0 -> ceil x <= 0. Proof. by move=> x0; rewrite -lerNl oppr0 floor_ge0 -lerNr oppr0. Qed. +(* TODO: rename because le_ceil means something else in archimedean, +and any should be renamed real_le_ceil *) Lemma le_ceil : {homo @Num.ceil R : x y / x <= y}. Proof. by move=> x y xy; rewrite lerNl opprK le_floor // lerNl opprK. Qed. @@ -656,8 +645,7 @@ Lemma abs_ceil_ge x : `|x| <= `|ceil x|.+1%:R. Proof. rewrite -natr1 natr_absz; have [x0|x0] := ltP 0%R x. by rewrite !gtr0_norm ?ceil_gt0// (le_trans (ceil_ge _))// lerDl. -rewrite !ler0_norm ?ceil_le0// opprK. -by rewrite intr1; apply/ltW/lt_succ_floor; rewrite num_real. +by rewrite !ler0_norm ?ceil_le0// opprK intr1 ltW// lt_succ_floor. Qed. End CeilTheory. diff --git a/theories/sequences.v b/theories/sequences.v index cd4885366a..c033a8efcb 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1276,7 +1276,7 @@ rewrite /series; near \oo => N; have xN : x < N%:R; last first. by apply: (nondecreasing_is_cvgn (incr_S1 N)); eexists; apply: S1_sup. near: N; exists (absz (floor x)%real).+1 => // m; rewrite /mkset -(@ler_nat R). move/lt_le_trans => -> //. -rewrite (lt_le_trans (@lt_succ_floor _ x _)) ?num_real//. +rewrite (lt_le_trans (@reals.lt_succ_floor _ x))//. by rewrite -intr1 -natr1 lerD2r -(@gez0_abs (floor x)%real) ?floor_ge0// ltW. Unshelve. all: by end_near. Qed. diff --git a/theories/topology.v b/theories/topology.v index 38261dfeca..138aa4b68f 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -2281,7 +2281,7 @@ Proof. by exists N. Qed. Lemma nbhs_infty_ger {R : realType} (r : R) : \forall n \near \oo, (r <= n%:R)%R. Proof. -exists (`|(ceil r)%real|)%N => // n /=; rewrite -(ler_nat R); apply: le_trans. +exists (`|Num.ceil r|)%N => // n /=; rewrite -(ler_nat R); apply: le_trans. by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm. Qed. @@ -4988,10 +4988,10 @@ apply/countable_uniformityP. exists (fun n => [set xy : T * T | ball xy.1 n.+1%:R^-1 xy.2]); last first. by move=> n; exact: (entourage_ball _ n.+1%:R^-1%:pos). move=> E; rewrite -entourage_ballE => -[e e0 subE]. -exists `|(floor e^-1)%real|%N; apply: subset_trans subE => xy; apply: le_ball. +exists `|Num.floor e^-1|%N; apply: subset_trans subE => xy; apply: le_ball. rewrite /= -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0// -natr1. -rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//. -by rewrite intr1 lt_succ_floor// num_real. +rewrite natr_absz ger0_norm; last by rewrite -reals.floor_ge_int ?invr_ge0// ltW. +by rewrite intr1 ltW// reals.lt_succ_floor. Qed. (** Specific pseudoMetric spaces *) @@ -5000,11 +5000,15 @@ Qed. Section matrix_PseudoMetric. Variables (m n : nat) (R : numDomainType) (T : pseudoMetricType R). Implicit Types x y : 'M[T]_(m, n). + Definition mx_ball x (e : R) y := forall i j, ball (x i j) e (y i j). + Lemma mx_ball_center x (e : R) : 0 < e -> mx_ball x e x. Proof. by move=> ???; apply: ballxx. Qed. + Lemma mx_ball_sym x y (e : R) : mx_ball x e y -> mx_ball y e x. Proof. by move=> xe_y ??; apply/ball_sym/xe_y. Qed. + Lemma mx_ball_triangle x y z (e1 e2 : R) : mx_ball x e1 y -> mx_ball y e2 z -> mx_ball x (e1 + e2) z. Proof. @@ -5676,10 +5680,10 @@ Qed. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Local Definition distN (e : R) : nat := `|(floor e^-1)%real|%N. +Local Definition distN (e : R) : nat := `|Num.floor e^-1|%N. Local Lemma distN0 : distN 0 = 0%N. -Proof. by rewrite /distN invr0 reals.floor0. Qed. +Proof. by rewrite /distN invr0 floor0. Qed. Local Lemma distN_nat (n : nat) : distN n%:R^-1 = n. Proof. @@ -5822,7 +5826,7 @@ move: e1 e2 x z; elim: n. rewrite -[e2]addr0 -(subrr e1) addrA -lerBlDr opprK addrC. by rewrite [e2 + _]addrC -deE; exact: lerD. - by rewrite addn0. - move=> /negP; rewrite -real_ltNge ?num_real //. + move=> /negP; rewrite -ltNge//. move=> e1d1; exists y, z, 0%N, 0%N; split. - by apply: n_step_ball_le; last (exact: Oxy); exact: ltW. - rewrite -deE; apply: (@n_step_ball_le _ _ d2) => //. @@ -5840,7 +5844,7 @@ case: (pselect (e2 <= d2)). - by rewrite addn0. have d1E' : d1 = e1 + (e2 - d2). by move: deE; rewrite addrA [e1 + _]addrC => <-; rewrite -addrA subrr addr0. -move=> /negP; rewrite -?real_ltNge // ?num_real // => d2lee2. +move=> /negP; rewrite -ltNge// => d2lee2. case: (IH e1 (e2 - d2) x y); rewrite ?subr_gt0 // -d1E' //. move=> t1 [t2] [c1] [c2] [] Oxy1 gt1t2 t2y <-. exists t1, t2, c1, c2.+1; split => //.