From c7ef0e2d692d2b919911a276c1e065172770d469 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 22 Jun 2024 01:02:00 +0900 Subject: [PATCH] try to make floor a notation (wip) --- CHANGELOG_UNRELEASED.md | 10 +++++++- classical/mathcomp_extra.v | 6 +++++ theories/altreals/realsum.v | 18 +++++++------- theories/ereal.v | 15 +++++++----- theories/lebesgue_integral.v | 35 ++++++++++++++------------- theories/lebesgue_measure.v | 4 +-- theories/lebesgue_stieltjes_measure.v | 8 +++--- theories/normedtype.v | 6 ++--- theories/real_interval.v | 22 +++++++++-------- theories/reals.v | 31 ++++++++++++------------ theories/sequences.v | 7 +++--- theories/topology.v | 14 +++++------ 12 files changed, 98 insertions(+), 78 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b539a08c6..0cde7ad5e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -7,10 +7,14 @@ - in `reals.v`: + lemma `mem_rg1_floor` +- in `mathcomp_extra.v`: + + lemmas `intr1`, `int1r` + ### Changed - in `reals.v`: - + definitions `Rceil`, `ceil`, `Rfloor`, `floor` + + definition `floor` now a notation (in `real_scope`) + + definitions `Rceil`, `ceil`, `Rfloor` ### Renamed @@ -20,6 +24,10 @@ ### Removed +- in `reals.v`: + + `lt_succ_floor` renamed to `__deprecated__lt_succ_floor` + (use `lt_succ_floor` from MathComp instead) + ### Infrastructure ### Misc diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 0e82043f4..32e15d43e 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -374,3 +374,9 @@ by elim: p => //= p <-; Qed. End positive. + +Lemma intr1 {R : ringType} (i : int) : i%:~R + 1 = (i + 1)%:~R :> R. +Proof. by rewrite intrD. Qed. + +Lemma int1r {R : ringType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R. +Proof. by rewrite intrD. Qed. diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v index 457c1e629..5c35bc01d 100644 --- a/theories/altreals/realsum.v +++ b/theories/altreals/realsum.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect all_algebra archimedean. From mathcomp.classical Require Import boolp. Require Import xfinmap ereal reals discrete realseq. From mathcomp.classical Require Import classical_sets functions mathcomp_extra. @@ -142,15 +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|)|%N; exists j; rewrite inE. + pose j := `|(floor (1 / `|f x|))%real|%N; exists j; rewrite inE. rewrite ltr_pdivrMr ?ltr0z // -ltr_pdivrMl ?normr_gt0 //. rewrite mulr1 /j div1r -addn1 /= PoszD intrD mulr1z. - by rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0 // lt_succ_floor. + rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0//. + by rewrite intr1 lt_succ_floor// num_real. 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)|.+1. -pose K := (`|floor M|.+1 * i.+1)%N; move/(_ K)/asboolP/exists_asboolP. +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=> 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. @@ -160,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 _]gez0_abs // floor_ge0. +by rewrite natrD /= mulr1n pmulrn -{1}[(floor _)%real]gez0_abs // floor_ge0. Qed. End SummableCountable. @@ -1201,9 +1202,8 @@ Qed. Lemma sum_seq1 S x : (forall y, S y != 0 -> x == y) -> sum S = S x. Proof. -move=> domS; rewrite (sum_finseq (r := [:: x])) //. - by move=> y; rewrite !inE => /domS /eqP->. -by rewrite big_seq1. +move=> domS; rewrite (sum_finseq (r := [:: x])) ?big_seq1//. +by move=> y; rewrite !inE => /domS /eqP->. Qed. End SumTheory. diff --git a/theories/ereal.v b/theories/ereal.v index 4d2fcce6f..d3d5b59c1 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -1402,21 +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) \is a Znat. + have /ZnatP[N Nfloor] : (floor (Num.max d 0%R))%real \is a Znat. 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. - by apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor natr1 ler_nat. - have /ZnatP [N Nfloor] : floor (Num.max (- d)%R 0%R) \is a Znat. + 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. 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. - by apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor natr1 ler_nat. -have /ZnatP[N Nfloor] : floor (d%:num^-1) \is a Num.nat. + 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. 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 (reals.lt_succ_floor _))// Nfloor lerD// ler_nat. +rewrite (lt_le_trans (lt_succ_floor _)) ?num_real// Nfloor. +by rewrite -intr1 lerD// ler_nat. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index a496506a1..bb0c5cfc0 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1287,11 +1287,11 @@ Lemma bigsetU_dyadic_itv n : `[n%:R, n.+1%:R[%classic = \big[setU/set0]_(n * 2 ^ n.+1 <= k < n.+1 * 2 ^ n.+1) [set` I n.+1 k]. Proof. rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|]. -- rewrite -bigcup_seq /=; exists `|reals.floor (r * 2 ^+ n.+1)|%N. +- rewrite -bigcup_seq /=; exists `|(floor (r * 2 ^+ n.+1))%real|%N. rewrite /= mem_index_iota; apply/andP; split. - rewrite -ltez_nat gez0_abs ?reals.floor_ge0; last first. + rewrite -ltez_nat gez0_abs ?floor_ge0; last first. by rewrite mulr_ge0// (le_trans _ nr). - apply: (@le_trans _ _ (reals.floor (n * 2 ^ n.+1)%:R)); last first. + apply: (@le_trans _ _ (floor (n * 2 ^ n.+1)%:R)%real); last first. by apply: le_floor; rewrite natrM natrX ler_pM2r. by rewrite -floor_ge_int. rewrite -ltz_nat gez0_abs; last first. @@ -1300,9 +1300,9 @@ rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|]. by rewrite PoszM intrM -natrX ltr_pM2r. rewrite /= in_itv /=; apply/andP; split. rewrite ler_pdivrMr// (le_trans _ (reals.floor_le _))//. - by rewrite -(@gez0_abs (reals.floor _))// floor_ge0 mulr_ge0// (le_trans _ nr). - rewrite ltr_pdivlMr// (lt_le_trans (reals.lt_succ_floor _))//. - rewrite -[in leRHS]natr1 lerD2r// -(@gez0_abs (reals.floor _))// floor_ge0. + 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. 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. @@ -1430,7 +1430,7 @@ rewrite pnatr_eq0 => /eqP. have [//|] := boolP (x \in B n). rewrite notin_setE /B /setI /= => /not_andP[] // /negP. rewrite -ltNge => fxn _. -have K : (`|reals.floor (fine (f x) * 2 ^+ n)| < n * 2 ^ n)%N. +have K : (`|(floor (fine (f x) * 2 ^+ n))%real| < n * 2 ^ n)%N. rewrite -ltz_nat gez0_abs; last by rewrite reals.floor_ge0 mulr_ge0// ltW. rewrite -(@ltr_int R); rewrite (le_lt_trans (reals.floor_le _))// PoszM intrM. by rewrite -natrX ltr_pM2r// -lte_fin (fineK fxfin). @@ -1439,9 +1439,10 @@ rewrite implyTb indicE mem_set ?mulr1; last first. rewrite /A K /= inE; split=> //=; exists (fine (f x)); last by rewrite fineK. rewrite in_itv /=; apply/andP; split. rewrite ler_pdivrMr// (le_trans _ (reals.floor_le _))//. - by rewrite -(@gez0_abs (reals.floor _))// reals.floor_ge0 mulr_ge0// ltW. - rewrite ltr_pdivlMr// (lt_le_trans (reals.lt_succ_floor _))// -[in leRHS]natr1. - by rewrite lerD2r// -{1}(@gez0_abs (reals.floor _))// reals.floor_ge0// mulr_ge0// ltW. + by rewrite -(@gez0_abs (floor _)%real)// reals.floor_ge0 mulr_ge0// ltW. + rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _)) ?num_real//. + rewrite -[in leRHS]natr1 -intr1 lerD2r// -{1}(@gez0_abs (floor _)%real)//. + by rewrite floor_ge0// mulr_ge0// ltW. rewrite mulf_eq0// -exprVn; apply/negP; rewrite negb_or expf_neq0//= andbT. rewrite pnatr_eq0 -lt0n absz_gt0 floor_neq0// -ler_pdivrMr//. apply/orP; right; apply/ltW; near: n. @@ -1538,11 +1539,11 @@ near=> n. have mn : (m <= n)%N by near: n; exists m. have : fine (f x) < n%:R. near: n. - exists `|reals.floor (fine (f x))|.+1%N => //= p /=. + exists `|(floor (fine (f x)))%real|.+1%N => //= p /=. rewrite -(@ler_nat R); apply: lt_le_trans. - rewrite -natr1 (_ : `| _ |%:R = (reals.floor (fine (f x)))%:~R); last first. - by rewrite -[in RHS](@gez0_abs (reals.floor _))// reals.floor_ge0//; exact/fine_ge0/f0. - by rewrite reals.lt_succ_floor. + 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. rewrite -lte_fin (fineK fxfin) => fxn. have [approx_nx0|[k [/andP[k0 kn2n] ? ->]]] := f_ub_approx fxn. by have := Hm _ mn; rewrite approx_nx0. @@ -1585,14 +1586,14 @@ case/cvg_ex => /= l; have [l0|l0] := leP 0%R l. rewrite natrD lerD// ?ler1n// ger0_norm // (le_trans (ceil_ge _)) //. by rewrite -(@gez0_abs (reals.ceil _)) // ceil_ge0. - move/cvgrPdist_lt => /(_ _ ltr01) -[n _]. - move=> /(_ (`|reals.floor l|.+1 + n)%N) /= /(_ (leq_addl _ _)). + move=> /(_ (`|(floor l)%real|.+1 + n)%N) /= /(_ (leq_addl _ _)). rewrite approx_x. apply/negP; rewrite -leNgt distrC (le_trans _ (lerB_normD _ _)) //. rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//. rewrite natrD lerD// ?ler1n// ler0_norm //; last by rewrite ltW. - rewrite (@le_trans _ _ (- reals.floor l)%:~R) //. + rewrite (@le_trans _ _ (- floor l)%real%:~R) //. by rewrite mulrNz lerNl opprK reals.floor_le. - by rewrite -(@lez0_abs (reals.floor _)) // reals.floor_le0 // ltW. + by rewrite -(@lez0_abs (floor _)%real)// floor_le0 // ltW. Qed. Lemma ecvg_approx (f0 : forall x, D x -> (0 <= f x)%E) x : diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 8f8c3d2d2..17a9a3d09 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -967,7 +967,7 @@ rewrite predeqE => t; split => [/= [Dt ft]|]. exists `|ceil (fine (f t))|%N => //=; split => //; split. by rewrite -{2}(fineK ft)// lee_fin (le_trans _ ft0)// lerNl oppr0. by rewrite natr_absz ger0_norm ?ceil_ge0// -(fineK ft) lee_fin ceil_ge. - exists `|floor (fine (f t))|%N => //=; split => //; split. + exists `|(floor (fine (f t)))%real|%N => //=; split => //; split. rewrite natr_absz ltr0_norm ?floor_lt0// EFinN. by rewrite -{2}(fineK ft) lee_fin mulrNz opprK floor_le. by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)). @@ -1212,7 +1212,7 @@ Lemma eset1Ny : Proof. rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr. move=> [r|/(_ O Logic.I)|]//. -move=> /(_ `|floor r|%N Logic.I); rewrite /= in_itv/= ltNge. +move=> /(_ `|(floor r)%real|%N Logic.I); rewrite /= in_itv/= ltNge. rewrite lee_fin; have [r0|r0] := leP 0%R r. by rewrite (le_trans _ r0) // lerNl oppr0 ler0n. rewrite lerNl -abszN natr_absz gtr0_norm; last first. diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 5c977eff3..6e5b6e050 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. -From mathcomp Require Import finmap fingroup perm rat. +From mathcomp Require Import finmap fingroup perm rat archimedean. From HB Require Import structures. From mathcomp.classical Require Import mathcomp_extra boolp classical_sets. From mathcomp.classical Require Import functions fsbigop cardinality. @@ -480,11 +480,11 @@ Lemma wlength_sigma_finite (f : R -> R) : Proof. exists (fun k => `](- k%:R), k%:R]%classic). apply/esym; rewrite -subTset => /= x _ /=. - exists `|(floor `|x|%R + 1)%R|%N; rewrite //= in_itv/=. + exists `|((floor `|x|%R)%real + 1)%R|%N; rewrite //= in_itv/=. rewrite !natr_absz intr_norm intrD. - suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->]. + suff: `|x| < `|(floor `|x|)%real%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->]. rewrite [ltRHS]ger0_norm//. - by rewrite (le_lt_trans _ (lt_succ_floor _))// ?ler_norm. + by rewrite intr1 (le_lt_trans _ (lt_succ_floor _))// ?ler_norm. by rewrite addr_ge0// ler0z floor_ge0. move=> k; split => //; rewrite wlength_itv /= -EFinB. by case: ifP; rewrite ltey. diff --git a/theories/normedtype.v b/theories/normedtype.v index 365b3c9fa..5e24bf0e5 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -4919,7 +4919,7 @@ Lemma compact_bounded (K : realType) (V : normedModType K) (A : set V) : Proof. rewrite compact_cover => Aco. have covA : A `<=` \bigcup_(n : int) [set p | `|p| < n%:~R]. - by move=> p _; exists (reals.floor `|p| + 1) => //; rewrite rmorphD/= reals.lt_succ_floor. + by move=> p _; exists ((floor `|p|)%real + 1) => //=; rewrite lt_succ_floor. have /Aco [] := covA. move=> n _; rewrite openE => p; rewrite /= -subr_gt0 => ltpn. apply/nbhs_ballP; exists (n%:~R - `|p|) => // q. @@ -5763,13 +5763,13 @@ Notation r_gt0 := vitali_collection_partition_ub_gt0. Lemma ex_vitali_collection_partition i : V i -> exists n, vitali_collection_partition n i. Proof. -move=> Vi; pose f := reals.floor (r / (radius (B i))%:num). +move=> Vi; pose f := (floor (r / (radius (B i))%:num))%real. have f_ge0 : 0 <= f by rewrite floor_ge0// divr_ge0// ltW// (r_gt0 Vi). have [m /andP[mf fm]] := leq_ltn_expn `|f|.-1. exists m; split => //; apply/andP; split => [{mf}|{fm}]. rewrite -(@ler_nat R) in fm. rewrite ltr_pdivrMr// mulrC -ltr_pdivrMr// (lt_le_trans _ fm)//. - rewrite (lt_le_trans (reals.lt_succ_floor _))//= -/f -natr1 lerD2r//. + rewrite (lt_le_trans (lt_succ_floor _))//= -/f intrD -natr1 lerD2r//. have [<-|f0] := eqVneq 0 f; first by rewrite /= ler0n. rewrite prednK//; last by rewrite absz_gt0 eq_sym. by rewrite natr_absz// ger0_norm. diff --git a/theories/real_interval.v b/theories/real_interval.v index cc90e5e51..9dc548a2f 100644 --- a/theories/real_interval.v +++ b/theories/real_interval.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. -From mathcomp Require Import finmap fingroup perm rat. +From mathcomp Require Import fingroup perm rat archimedean finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Export set_interval. From HB Require Import structures. @@ -173,10 +173,11 @@ Lemma itv_bnd_inftyEbigcup b x : [set` Interval (BSide b x) +oo%O] = Proof. rewrite predeqE => y; split=> /=; last first. by move=> [n _]/=; rewrite in_itv => /andP[xy yn]; rewrite in_itv /= xy. -rewrite in_itv /= andbT => xy; exists `|floor y|%N.+1 => //=. +rewrite in_itv /= andbT => xy; exists `|(floor y)%real|%N.+1 => //=. rewrite in_itv /= xy /=. have [y0|y0] := ltP 0 y; last by rewrite (le_lt_trans y0)// ltr_pwDr. -by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW// lt_succ_floor. +rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW//. +by rewrite intr1 lt_succ_floor// num_real. Qed. Lemma itv_o_inftyEbigcup x : @@ -340,10 +341,10 @@ move gxE : (g x) => gx; case: gx gxE => [gx| |gxoo fxoo]; last 2 first. - by exists 0%N => //; rewrite /E/= gxoo addey// ?leey// -ltNye. move fxE : (f x) => fx; case: fx fxE => [fx fxE gxE|fxoo gxE _|//]; last first. by exists 0%N => //; rewrite /E/= fxoo gxE// addye// leey. -rewrite lte_fin -subr_gt0 => fgx; exists `|floor (fx - gx)^-1%R|%N => //. +rewrite lte_fin -subr_gt0 => fgx; exists `|(floor (fx - gx)^-1)%real|%N => //. rewrite /E/= -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0; last exact/ltW. rewrite fxE gxE lee_fin -[leRHS]invrK lef_pV2//. -- by apply/ltW; rewrite lt_succ_floor. +- by rewrite intr1 ltW// lt_succ_floor// num_real. - by rewrite posrE// ltr_pwDr// ler0z floor_ge0 invr_ge0 ltW. - by rewrite posrE invr_gt0. Qed. @@ -363,9 +364,10 @@ apply/seteqP; split=> [x ->|]. by move=> i _/=; rewrite in_itv/= lexx ltrBlDr ltrDl invr_gt0 ltr0n. move=> x rx; apply/esym/eqP; rewrite eq_le (itvP (rx 0%N _))// andbT. apply/ler_addgt0Pl => e e_gt0; rewrite -lerBlDl ltW//. -have := rx `|floor e^-1%R|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//. +have := rx `|(floor e^-1)%real|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//. rewrite lerD2l lerN2 -lef_pV2 ?invrK//; last by rewrite posrE. -by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW// lt_succ_floor. +rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//. +by rewrite intr1 lt_succ_floor// num_real. Qed. Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) : @@ -421,10 +423,10 @@ Qed. Lemma bigcup_itvT {R : realType} b : \bigcup_i [set` Interval (BSide b (- i%:R)) (BRight i%:R)] = [set: R]. Proof. -rewrite -subTset => x _ /=; exists `|(floor `|x| + 1)%R|%N => //=. +rewrite -subTset => x _ /=; exists `|((floor `|x|)%real + 1)%R|%N => //=. rewrite in_itv/= !natr_absz intr_norm intrD. -have : `|x| < `|(floor `|x|)%:~R + 1|. - by rewrite [ltRHS]ger0_norm ?lt_succ_floor// addr_ge0// ler0z floor_ge0. +have : `|x| < `|(floor `|x|)%real%:~R + 1|. + by rewrite [ltRHS]ger0_norm ?intr1 ?lt_succ_floor// ler0z addr_ge0// floor_ge0. case: b => /=. - by move/ltW; rewrite ler_norml => /andP[-> ->]. - by rewrite ltr_norml => /andP[-> /ltW->]. diff --git a/theories/reals.v b/theories/reals.v index fff38c807..2e9142252 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -238,13 +238,17 @@ Qed. End ToInt. (* -------------------------------------------------------------------- *) +Reserved Notation "'floor' r" (at level 10). +Notation "'floor' x" := (Num.floor x) : real_scope. +Local Open Scope real_scope. + Section RealDerivedOps. Variable R : realType. Implicit Types x y : R. Definition floor_set x := [set y : R | (y \is a Rint) && (y <= x)]. -Definition floor x : int := Num.floor x. +(*Definition floor x : int := Num.floor x.*) Definition Rfloor x : R := (floor x)%:~R. @@ -477,16 +481,12 @@ Proof. by []. Qed. Lemma mem_rg1_floor x : (range1 (floor x)%:~R) x. Proof. -rewrite /range1/mkset. -rewrite [X in _ + X](_ : 1 = 1%:~R)// -intrD lt_succ_floor ?andbT ?num_real//. +rewrite /range1 /mkset intr1 lt_succ_floor ?num_real// andbT. by rewrite ge_floor// num_real. Qed. Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x. -Proof. -rewrite /range1 /mkset [X in _ + X](_ : 1 = 1%:~R)// -intrD. -by rewrite lt_succ_floor ?num_real// andbT ge_floor// num_real. -Qed. +Proof. by rewrite /Rfloor; exact: mem_rg1_floor. Qed. Lemma Rfloor_le x : Rfloor x <= x. Proof. by case/andP: (mem_rg1_Rfloor x). Qed. @@ -552,10 +552,10 @@ Lemma floor_natz n : floor (n%:R : R) = n%:~R :> int. Proof. by have /intr_inj -> := Rfloor_natz n; rewrite -pmulrn/= natz. Qed. Lemma floor0 : floor (0 : R) = 0. -Proof. by rewrite /floor floor0. Qed. +Proof. by rewrite floor0. Qed. Lemma floor1 : floor (1 : R) = 1. -Proof. by rewrite /floor floor1. Qed. +Proof. by rewrite floor1. Qed. Lemma floor_ge0 x : (0 <= floor x) = (0 <= x). Proof. by rewrite -floor_ge_int// num_real. Qed. @@ -568,7 +568,7 @@ Proof. by move=> x0; rewrite -(@ltrz0 R) (le_lt_trans (ge_floor _))// num_real. Qed. -Lemma le_floor : {homo @floor R : x y / x <= y}. +Lemma le_floor : {homo @Num.floor R : x y / x <= y}. Proof. by move=> a b ab; rewrite Num.Theory.floor_le. Qed. Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x >= 1). @@ -580,10 +580,8 @@ apply/idP/orP => [|[x0|/le_floor r1]]; first rewrite neq_lt => /orP[x0|x0]. - by rewrite gt_eqF// (lt_le_trans _ r1)// floor1. Qed. -Lemma lt_succ_floor x : x < (floor x)%:~R + 1. -Proof. -by rewrite [X in _ + X](_ : 1 = 1%:~R)// -intrD lt_succ_floor// num_real. -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. @@ -598,7 +596,7 @@ 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_ge0 invr_ge0 subr_ge0 ltW. -by rewrite lt_succ_floor. +by rewrite intr1 lt_succ_floor ?num_real. Qed. End FloorTheory. @@ -656,7 +654,8 @@ 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. -by rewrite !ler0_norm ?ceil_le0// /ceil opprK; exact/ltW/lt_succ_floor. +rewrite !ler0_norm ?ceil_le0// /ceil opprK. +by rewrite intr1; apply/ltW/lt_succ_floor; rewrite num_real. Qed. End CeilTheory. diff --git a/theories/sequences.v b/theories/sequences.v index cdd82622d..cd4885366 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1274,9 +1274,10 @@ Proof. rewrite /series; near \oo => N; have xN : x < N%:R; last first. rewrite -(@is_cvg_series_restrict N.+1). by apply: (nondecreasing_is_cvgn (incr_S1 N)); eexists; apply: S1_sup. -near: N; exists (absz (reals.floor x)).+1 => // m; rewrite /mkset -(@ler_nat R). -move/lt_le_trans => -> //; rewrite (lt_le_trans (reals.lt_succ_floor x)) // -addn1. -by rewrite natrD lerD2r -(@gez0_abs (reals.floor x)) ?reals.floor_ge0// ltW. +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//. +by rewrite -intr1 -natr1 lerD2r -(@gez0_abs (floor x)%real) ?floor_ge0// ltW. Unshelve. all: by end_near. Qed. End exponential_series_cvg. diff --git a/theories/topology.v b/theories/topology.v index 97b02bf8b..13e0b677d 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -4988,9 +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|%N; apply: subset_trans subE => xy; apply: le_ball. +exists `|(floor e^-1)%real|%N; apply: subset_trans subE => xy; apply: le_ball. rewrite /= -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0// -natr1. -by rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0// 1?ltW// reals.lt_succ_floor. +rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//. +by rewrite intr1 lt_succ_floor// num_real. Qed. (** Specific pseudoMetric spaces *) @@ -5675,16 +5676,15 @@ Qed. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Local Definition distN (e : R) : nat := `|floor e^-1|%N. +Local Definition distN (e : R) : nat := `|(floor e^-1)%real|%N. Local Lemma distN0 : distN 0 = 0%N. Proof. by rewrite /distN invr0 reals.floor0. Qed. -Local Lemma distN_nat (n : nat): distN (n%:R^-1) = n. +Local Lemma distN_nat (n : nat) : distN n%:R^-1 = n. Proof. rewrite /distN invrK. -apply/eqP; rewrite -(@eqr_nat R) natr_absz ger0_norm//; last first. - by rewrite -(floor0 R) floor_le. +apply/eqP; rewrite -(@eqr_nat R) natr_absz ger0_norm ?floor_ge0//. by rewrite -intrEfloor intrEge0. Qed. @@ -5899,7 +5899,7 @@ Lemma countable_uniform_bounded (x y : T) : in @ball _ U x 2 y. Proof. rewrite /ball; exists O%N; rewrite /n_step_ball; split; rewrite // /distN. -suff -> : @floor R 2^-1 = 0 by rewrite absz0 /=. +rewrite [X in `|X|%N](_ : _ = 0) ?absz0//. apply/eqP; rewrite -[_ == _]negbK; rewrite floor_neq0 negb_or -?ltNge -?leNgt. by apply/andP; split => //; rewrite invf_lt1 //= ltrDl. Qed.