From 3314bae3ef6cd14e3581b9f1d3275cd1fb02f03c Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 19 Mar 2025 13:24:01 +0100 Subject: [PATCH 1/3] Rename intrD1 -> intr1 and intrD1 -> int1r, like natr1 and nat1r --- CHANGELOG_UNRELEASED.md | 6 ++++++ classical/mathcomp_extra.v | 11 ++++++++--- reals/real_interval.v | 2 +- reals/reals.v | 4 ++-- theories/lebesgue_integral.v | 4 ++-- theories/lebesgue_measure.v | 2 +- theories/lebesgue_stieltjes_measure.v | 2 +- theories/realfun.v | 2 +- theories/sequences.v | 2 +- theories/topology_theory/pseudometric_structure.v | 2 +- 10 files changed, 24 insertions(+), 13 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b4d0f0a4b..aba85a7ae 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -58,6 +58,8 @@ + `min_le_min` -> `le_min2` + `max_le_max` -> `le_max2` + `real_sqrtC` -> `sqrtC_real` + + `intrD1` -> `intr1` + + `intr1D` -> `int1r` ### Generalized @@ -70,6 +72,10 @@ ### Deprecated +- in `mathcomp_extra.v` + + `intrD1` (renamed `intr1`) + + `intr1D` (renamed `int1r`) + ### Removed - file `mathcomp_extra.v` diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index d1ab19b6e..c148f970f 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -512,12 +512,17 @@ Qed. End order_min. -Lemma intrD1 {R : ringType} (i : int) : i%:~R + 1 = (i + 1)%:~R :> R. +Lemma intr1 {R : ringType} (i : int) : i%:~R + 1 = (i + 1)%:~R :> R. Proof. by rewrite intrD. Qed. -Lemma intr1D {R : ringType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R. +Lemma int1r {R : ringType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R. Proof. by rewrite intrD. Qed. +#[deprecated(since="mathcomp-analysis 1.10.0", note="use intr1 instead")] +Notation intrD1 := intr1. +#[deprecated(since="mathcomp-analysis 1.10.0", note="use int1r instead")] +Notation intr1D := int1r. + Section floor_ceil. Context {R : archiDomainType}. Implicit Type x : R. @@ -577,7 +582,7 @@ Lemma abs_ceil_ge x : `|x| <= `|Num.ceil x|.+1%:R. Proof. rewrite -natr1 natr_absz; have [x0|x0] := ltP 0 x. by rewrite !gtr0_norm// -?ceil_gt0// (le_trans (Num.Theory.le_ceil _))// lerDl. -by rewrite !ler0_norm -?ceil_le0// opprK intrD1 ltW// lt_succ_floor. +by rewrite !ler0_norm -?ceil_le0// opprK intr1 ltW// lt_succ_floor. Qed. End floor_ceil. diff --git a/reals/real_interval.v b/reals/real_interval.v index 4e44631ed..2ec9c7af7 100644 --- a/reals/real_interval.v +++ b/reals/real_interval.v @@ -343,7 +343,7 @@ Proof. rewrite -subTset => x _ /=; exists `|(floor `|x| + 1)%R|%N => //=. rewrite in_itv/= !natr_absz intr_norm intrD. have : `|x| < `|(floor `|x|)%:~R + 1|. - by rewrite [ltRHS]ger0_norm ?intrD1 ?lt_succ_floor// ler0z addr_ge0 ?floor_ge0. + 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/reals/reals.v b/reals/reals.v index 9039143d9..b3deb13bb 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -466,7 +466,7 @@ Lemma RfloorE x : Rfloor x = (floor x)%:~R. Proof. by []. Qed. Lemma mem_rg1_floor x : (range1 (floor x)%:~R) x. -Proof. by rewrite /range1 /mkset intrD1 ge_floor lt_succ_floor. Qed. +Proof. by rewrite /range1 /mkset intr1 ge_floor lt_succ_floor. Qed. Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x. Proof. exact: mem_rg1_floor. Qed. @@ -497,7 +497,7 @@ Proof. by rewrite /range1/mkset lexx /= ltrDl ltr01. Qed. Lemma range1zP (m : int) x : Rfloor x = m%:~R <-> (range1 m%:~R) x. Proof. split=> [<-|h]; first exact/mem_rg1_Rfloor. -by congr intmul; apply/floor_def; rewrite -intrD1. +by congr intmul; apply/floor_def; rewrite -intr1. Qed. Lemma Rfloor_natz (z : int) : Rfloor z%:~R = z%:~R :> R. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index c05e01060..577d77bc0 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1500,7 +1500,7 @@ have : fine (f x) < n%:R. rewrite -(@ler_nat R); apply: lt_le_trans. rewrite -natr1 (_ : `| _ |%:R = (floor (fine (f x)))%:~R); last first. by rewrite -[in RHS](@gez0_abs (floor _))// floor_ge0//; exact/fine_ge0/f0. - by rewrite intrD1 lt_succ_floor. + by rewrite intr1 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. @@ -3883,7 +3883,7 @@ move=> mf; split=> [iDf0|Df0]. - by apply/fine_gt0; rewrite lt0e abse_ge0 abse_eq0 ft0 ltey. rewrite /m -natr1 natr_absz ger0_norm; last first. by rewrite -(ceil0 R) ceil_le. - by rewrite intrD1 ceil_ge_int lerDl. + by rewrite intr1 ceil_ge_int lerDl. by split => //; apply: contraTN nft => /eqP ->; rewrite abse0 -ltNge. transitivity (limn (fun n => mu (D `&` [set x | `|f x| >= n.+1%:R^-1%:E]))). apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 2f597c922..e31680e77 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1169,7 +1169,7 @@ have finite_set_F i : finite_set (F i). apply/negP; rewrite -ltNge lebesgue_measure_ball// lte_fin. rewrite -[M%:R]natr1 natr_absz ger0_norm; last first. by rewrite -[leLHS](ceil0 R) ceil_le. - by rewrite -ltr_pdivrMr// intrD1 floor_lt_int ltzD1 ceil_floor// lerDl. + by rewrite -ltr_pdivrMr// intr1 floor_lt_int ltzD1 ceil_floor// lerDl. have mur2_fin_num_ : mu (ball (0:R) (r%:num + 2))%R < +oo. by rewrite lebesgue_measure_ball// ltry. have FE : \sum_(n `](- k%:R), k%:R]%classic). rewrite !natr_absz intr_norm intrD. suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->]. rewrite [ltRHS]ger0_norm//. - by rewrite intrD1 (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/realfun.v b/theories/realfun.v index ee793ca96..a6aa1e039 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -2800,7 +2800,7 @@ have FrBFl (x : elt_type) : exists m, m.+1%:R ^-1 < Fr (sval x) - Fl (sval x). exists (`|floor (Fr (sval x) - Fl (sval x))^-1|)%N. rewrite invf_plt ?posrE ?subr_gt0// -natr1 natr_absz ger0_norm; last first. by rewrite floor_ge0 invr_ge0// subr_ge0 ltW. - by rewrite intrD1 mathcomp_extra.lt_succ_floor// realE. + by rewrite intr1 mathcomp_extra.lt_succ_floor// realE. pose S m := [set x | x \in `]a, b[ /\ m.+1%:R ^-1 < Fr x - Fl x]. have jumpfafb m (s : seq R) : (forall i, (i < size s)%N -> nth b s i \in S m) -> path <%R a s -> diff --git a/theories/sequences.v b/theories/sequences.v index a94ac54f8..8de5404f2 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1195,7 +1195,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 `|floor x|.+1 => // m; rewrite /mkset -(@ler_nat R). move/lt_le_trans => -> //; rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor x))//. -by rewrite -intrD1 -natr1 lerD2r -(@gez0_abs (floor x)) ?floor_ge0// ltW. +by rewrite -intr1 -natr1 lerD2r -(@gez0_abs (floor x)) ?floor_ge0// ltW. Unshelve. all: by end_near. Qed. End exponential_series_cvg. diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v index 9f3a2dc1e..e8d01cbf2 100644 --- a/theories/topology_theory/pseudometric_structure.v +++ b/theories/topology_theory/pseudometric_structure.v @@ -338,7 +338,7 @@ 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; last first. by rewrite -floor_ge_int ?invr_ge0 ?num_real // ltW. -by rewrite intrD1 ltW// lt_succ_floor ?num_real. +by rewrite intr1 ltW// lt_succ_floor ?num_real. Qed. (** Specific pseudoMetric spaces *) From 10fc745b3cbbc603d03f1e9fe039d4b742fd7247 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 19 Mar 2025 13:28:51 +0100 Subject: [PATCH 2/3] Rename nat_int -> natr_int similarly to intr_int or natr_nat already in mathcomp --- CHANGELOG_UNRELEASED.md | 2 ++ classical/mathcomp_extra.v | 5 ++++- theories/pi_irrational.v | 4 ++-- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index aba85a7ae..2494614c9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -60,6 +60,7 @@ + `real_sqrtC` -> `sqrtC_real` + `intrD1` -> `intr1` + `intr1D` -> `int1r` + + `nat_int` -> `natr_int` ### Generalized @@ -75,6 +76,7 @@ - in `mathcomp_extra.v` + `intrD1` (renamed `intr1`) + `intr1D` (renamed `int1r`) + + `nat_int` (renamed `natr_int`) ### Removed diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index c148f970f..3211b8212 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -590,9 +590,12 @@ End floor_ceil. #[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to `ceil_gt_int`")] Notation ceil_lt_int := ceil_gt_int (only parsing). -Lemma nat_int {R : archiNumDomainType} n : n%:R \is a @Num.int R. +Lemma natr_int {R : archiNumDomainType} n : n%:R \is a @Num.int R. Proof. by rewrite Num.Theory.intrEge0. Qed. +#[deprecated(since="mathcomp-analysis 1.10.0", note="Use natr_int instead.")] +Notation nat_int := natr_int. + Section bijection_forall. Lemma bij_forall A B (f : A -> B) (P : B -> Prop) : diff --git a/theories/pi_irrational.v b/theories/pi_irrational.v index 0e805f3e1..4295210dd 100644 --- a/theories/pi_irrational.v +++ b/theories/pi_irrational.v @@ -86,7 +86,7 @@ Let f_int i : n`!%:R * f`_i \is a Num.int. Proof. rewrite /f coefZ mulrA divff ?mul1r ?pnatr_eq0 ?gtn_eqF ?fact_gt0//. apply/polyOverP => /=; rewrite rpredM ?rpredX ?polyOverX//=. -by rewrite rpredB ?polyOverC ?polyOverZ ?polyOverX//= nat_int. +by rewrite rpredB ?polyOverC ?polyOverZ ?polyOverX//= natr_int. Qed. Let f_small_coef0 i : (i < n)%N -> f`_i = 0. @@ -97,7 +97,7 @@ Proof. rewrite horner_coef0 coef_derivn addn0 ffactnn. have [/f_small_coef0 ->|/bin_fact <-] := ltnP i n. by rewrite mul0rn // int_Qint. -by rewrite mulnCA -mulr_natl natrM mulrAC rpredM ?f_int ?nat_int. +by rewrite mulnCA -mulr_natl natrM mulrAC rpredM ?f_int ?natr_int. Qed. Lemma F0_int : F.[0] \is a Num.int. From 6a188461b6eed77c09a0d594e388906cd0f0c939 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 19 Mar 2025 14:20:48 +0100 Subject: [PATCH 3/3] Complete lemmas about trunc/floor/ceil --- CHANGELOG_UNRELEASED.md | 21 +++ classical/mathcomp_extra.v | 278 +++++++++++++++++++++++++++++----- reals/real_interval.v | 2 +- reals/reals.v | 2 +- theories/lebesgue_integral.v | 12 +- theories/lebesgue_measure.v | 4 +- theories/measurable_realfun.v | 4 +- theories/measure.v | 2 +- theories/normedtype.v | 6 +- theories/realfun.v | 4 +- theories/sequences.v | 2 +- 11 files changed, 278 insertions(+), 59 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2494614c9..e1d484e83 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -36,6 +36,17 @@ - in `derive.v`: + lemmas `derive_shift`, `is_derive_shift` +- in `mathcomp_extra.v` + + lemmas `real_lt_succ_trunc`, `trunc_gt_nat`, `real_trunc_le_nat`, + `trunc_eq`, `trunc_le`, `natrKtrunc`, `natrEtrunc`, + `real_floor_ge_int_tmp`, `real_floor_ge_int`, `real_floor_lt_int`, + `real_floor_eq`, `real_floor_ge0`, `real_floor_le0`, `floor_gt0`, + `real_abs_floor_ge`, `real_ceil_le_int_tmp`, `real_ceil_le_int`, + `real_ceil_gt_int`, `real_ceil_eq`, `real_ceil_ge0`, `ceil_lt0`, + `real_ceil_le0`, `ceil_neq0`, `real_abs_ceil_ge`, `trunc_le_nat`, + `floor_ge_int_tmp`, `abs_floor_ge`, `ceil_le_int`, + `ceil_le_int_tmp` + ### Changed - file `nsatz_realtype.v` moved from `reals` to `reals-stdlib` package @@ -45,6 +56,10 @@ - moved, generalized, and renamed from `gauss_integral` to `trigo.v`: + `integral01_oneDsqr` -> `integral0_oneDsqr` +- in `mathcomp_extra.v`: + + `floor_lt_int`, `floor_le0`, `floor_lt0`, `ceil_gt_int`, + `ceil_ge0`, `ceil_le0`, `ceil_gt0` (equality direction) + ### Renamed - in `lebesgue_integral.v`: @@ -71,12 +86,18 @@ + lemmas `measurable_funP`, `ge0_integral_pushforward`, `integrable_pushforward`, `integral_pushforward` +- in `mathcomp_extra.v` + + lemmas `ge_trunc`, `trunc_ge_nat`, `floor_lt0`, `floor_neq0`, + `ceil_gt0` (from `archiRealDomainType` to `archiNumDomainType`) + ### Deprecated - in `mathcomp_extra.v` + `intrD1` (renamed `intr1`) + `intr1D` (renamed `int1r`) + `nat_int` (renamed `natr_int`) + + `real_floor_ge_int` (use `real_floor_ge_int_tmp` instead) + + `floor_ge_int` (use `floor_ge_int_tmp` instead) ### Removed diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 3211b8212..221769673 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -116,7 +116,40 @@ Arguments dfwith {I T} f i x. Definition idempotent_fun (U : Type) (f : U -> U) := f \o f =1 f. +Section intrN. + +Variable R : ringType. + +Implicit Types n : int. + +Lemma intrN n : (- n)%:~R = - n%:~R :> R. Proof. exact: mulrNz. Qed. + +End intrN. + From mathcomp Require Import archimedean. +Import Num.Theory. + +Section num_floor_ceil. +Context {R : archiNumDomainType}. +Implicit Type x : R. + +Lemma real_floor_itv x : x \is Num.real -> + (Num.floor x)%:~R <= x < (Num.floor x + 1)%:~R. +Proof. by case: (x \is _) (archimedean.Num.Theory.floorP x). Qed. + +Lemma real_lt_succ_floor x : x \is Num.real -> x < (Num.floor x + 1)%:~R. +Proof. by move=> /real_floor_itv /andP[]. Qed. + +Lemma real_ge_floor x : x \is Num.real -> (Num.floor x)%:~R <= x. +Proof. by move=> /real_floor_itv /andP[]. Qed. + +Lemma real_ceil_itv x : x \is Num.real -> + (Num.ceil x - 1)%:~R < x <= (Num.ceil x)%:~R. +Proof. +by move=> Rx; rewrite -opprD !mulrNz ltrNl lerNr andbC real_floor_itv ?realN. +Qed. + +End num_floor_ceil. Section floor_ceil. Context {R : archiDomainType}. @@ -125,9 +158,6 @@ Implicit Type x : R. Lemma ge_floor x : (Num.floor x)%:~R <= x. Proof. exact: Num.Theory.ge_floor. Qed. -Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x). -Proof. exact: Num.Theory.floor_ge_int. Qed. - Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R. Proof. exact: Num.Theory.lt_succ_floor. Qed. @@ -523,71 +553,239 @@ Notation intrD1 := intr1. #[deprecated(since="mathcomp-analysis 1.10.0", note="use int1r instead")] Notation intr1D := int1r. -Section floor_ceil. -Context {R : archiDomainType}. +Section num_trunc_floor_ceil. +Context {R : archiNumDomainType}. Implicit Type x : R. Lemma ge_trunc x : ((Num.trunc x)%:R <= x) = (0 <= x). Proof. -by have [/Num.Theory.trunc_itv/andP[]//|] := leP 0 x; exact/contra_ltF/le_trans. +by have := trunc_floor x; case: ifP => [/trunc_itv/andP[] | _ -> //]. +(* simplify proof when backporting: +by have := Def.truncP x; case: ifP => [+ /andP[] | + /eqP->//]. *) Qed. -Lemma lt_succ_trunc x : x < (Num.trunc x).+1%:R. -Proof. by have [/Num.Theory.trunc_itv/andP[]|/lt_le_trans->] := leP 0 x. Qed. +Lemma real_lt_succ_trunc x : x \is Num.real -> x < (Num.trunc x).+1%:R. +Proof. by move/real_ge0P => [/trunc_itv/andP[]|/lt_le_trans->]. Qed. -Lemma trunc_ge_nat x (n : nat) : 0 <= x -> (n%:R <= x) = (n <= Num.trunc x)%N. +Lemma trunc_ge_nat x n : 0 <= x -> (n <= Num.trunc x)%N = (n%:R <= x). Proof. -move=> /Num.Theory.trunc_itv /andP[letx ltxt1]; apply/idP/idP => lenx. - by rewrite -ltnS -(ltr_nat R); apply: le_lt_trans ltxt1. -by apply: le_trans letx; rewrite ler_nat. +move=> /trunc_itv /andP[letx ltxt1]; apply/idP/idP => lenx. + by apply: le_trans letx; rewrite ler_nat. +by rewrite -ltnS -(ltr_nat R); apply: le_lt_trans ltxt1. Qed. -Lemma trunc_lt_nat x (n : nat) : 0 <= x -> (x < n%:R) = (Num.trunc x < n)%N. -Proof. by rewrite ltNge ltnNge => /trunc_ge_nat ->. Qed. +Lemma trunc_gt_nat x n : (n < Num.trunc x)%N = (n.+1%:R <= x). +Proof. +have := trunc_floor x; case: ifP => [x0 _ | x0 ->]. + by rewrite trunc_ge_nat. +by rewrite ltn0; apply/esym/(contraFF _ x0)/le_trans. +(* simplify proof when backporting +have := archimedean.Num.Def.truncP x; case: ifP => [x0 _ | x0 /eqP->]. + by rewrite trunc_ge_nat. +by rewrite ltn0; apply/esym/(contraFF _ x0)/le_trans. *) +Qed. -Lemma floor_lt_int x (z : int) : (x < z%:~R) = (Num.floor x < z). -Proof. by rewrite ltNge floor_ge_int -ltNge. Qed. +Lemma trunc_lt_nat x n : 0 <= x -> (Num.trunc x < n)%N = (x < n%:R). +Proof. by move=> ?; rewrite real_ltNge ?ger0_real// ltnNge trunc_ge_nat. Qed. -Lemma floor_ge0 x : (0 <= Num.floor x) = (0 <= x). -Proof. by rewrite -floor_ge_int. Qed. +Lemma real_trunc_le_nat x n : x \is Num.real -> + (Num.trunc x <= n)%N = (x < n.+1%:R). +Proof. by move=> ?; rewrite real_ltNge// leqNgt trunc_gt_nat. Qed. + +Lemma trunc_eq x n : 0 <= x -> (Num.trunc x == n) = (n%:R <= x < n.+1%:R). +Proof. +by move=> xr; apply/eqP/idP => [<-|]; [exact: trunc_itv|exact: trunc_def]. +Qed. + +Lemma trunc_le : {homo Num.trunc : x y / x <= y :> R >-> (x <= y)%N}. +Proof. +move=> x y lexy. +move: (trunc_floor x) (trunc_floor y). +case: ifP => [x0 _ | x0->//]. +case: ifP => [y0 _ | + ->]; [|by rewrite (le_trans x0 lexy)]. +move: (trunc_itv y0) => /andP[_ /(le_lt_trans lexy)]. +move: (trunc_itv x0) => /andP[+ _] => /le_lt_trans/[apply]. +by rewrite ltr_nat ltnS. +(* simplify proof when backporting: +move: (archimedean.Num.Def.truncP x) (archimedean.Num.Def.truncP y). +case: ifP => [x0 /andP[letx _] | x0 /eqP->//]. +case: ifP => [y0 /andP[_] | + /eqP->]; [|by rewrite (le_trans x0 lexy)]. +by move=> /(le_lt_trans lexy) /(le_lt_trans letx); rewrite ltr_nat ltnS. *) +Qed. + +Lemma natrKtrunc : cancel (@GRing.natmul R 1) Num.trunc. +Proof. by move=> n; apply: trunc_def; rewrite lexx -natr1 ltrDl ltr01. Qed. + +Lemma natrEtrunc x : (x \is a Num.nat) = ((Num.trunc x)%:R == x). +Proof. +by apply/natrP/eqP => [[n ->] | <-]; [rewrite natrKtrunc | exists (Num.trunc x)]. +Qed. + +Lemma real_floor_ge_int_tmp x n : x \is Num.real -> + (n <= Num.floor x) = (n%:~R <= x). +Proof. +move=> /real_floor_itv /andP[lefx ltxf1]; apply/idP/idP => lenx. + by apply: le_trans lefx; rewrite ler_int. +by rewrite -ltzD1 -(ltr_int R); apply: le_lt_trans ltxf1. +Qed. + +#[deprecated(since="mathcomp-analysis 1.10.0", + note="Use real_floor_ge_int_tmp instead.")] +Lemma real_floor_ge_int x n : x \is Num.real -> (n%:~R <= x) = (n <= Num.floor x). +Proof. by move=> ?; rewrite real_floor_ge_int_tmp. Qed. + +Lemma real_floor_lt_int x n : x \is Num.real -> (Num.floor x < n) = (x < n%:~R). +Proof. +by move=> ?; rewrite [RHS]real_ltNge ?realz -?real_floor_ge_int_tmp -?ltNge. +Qed. + +Lemma real_floor_eq x n : x \is Num.real -> + (Num.floor x == n) = (n%:~R <= x < (n + 1)%:~R). +Proof. +by move=> xr; apply/eqP/idP => [<-|]; [exact: real_floor_itv|exact: floor_def]. +Qed. -Lemma floor_le0 x : (x < 1) = (Num.floor x <= 0). -Proof. by rewrite -ltzD1 add0r -floor_lt_int. Qed. +Lemma real_floor_ge0 x : x \is Num.real -> (0 <= Num.floor x) = (0 <= x). +Proof. by move=> ?; rewrite real_floor_ge_int_tmp. Qed. -Lemma floor_lt0 x : (x < 0) = (Num.floor x < 0). -Proof. by rewrite -floor_lt_int. Qed. +Lemma floor_lt0 x : (Num.floor x < 0) = (x < 0). +Proof. +have := archimedean.Num.Theory.floorP x; case: ifP => [xr _ | xr /eqP]. + by rewrite real_floor_lt_int. +rewrite -?[0%Z]/(@GRing.zero int) => <-. +by rewrite ltxx; apply/esym/(contraFF _ xr)/ltr0_real. +(* simpler proof when backporting: +have := archimedean.Num.Theory.floorP x; case: ifP => [xr _ | xr /eqP<-]. + by rewrite real_floor_lt_int. +by rewrite ltxx; apply/esym/(contraFF _ xr)/ltr0_real. *) +Qed. + +Lemma real_floor_le0 x : x \is Num.real -> (Num.floor x <= 0) = (x < 1). +Proof. by move=> ?; rewrite -ltzD1 add0r real_floor_lt_int. Qed. -Lemma floor_eq x m : (Num.floor x == m) = (m%:~R <= x < (m + 1)%:~R). +Lemma floor_gt0 x : (Num.floor x > 0) = (x >= 1). Proof. -apply/eqP/idP; [move=> <-|by move=> /Num.Theory.floor_def ->]. -by rewrite Num.Theory.ge_floor//= Num.Theory.lt_succ_floor. +have := archimedean.Num.Theory.floorP x; case: ifP => [xr _ | xr /eqP->]. + by rewrite gtz0_ge1 real_floor_ge_int_tmp. +by rewrite ltxx; apply/esym/(contraFF _ xr)/ger1_real. Qed. Lemma floor_neq0 x : (Num.floor x != 0) = (x < 0) || (x >= 1). -Proof. by rewrite floor_eq negb_and -ltNge -leNgt. Qed. +Proof. +have := archimedean.Num.Theory.floorP x. +case: ifP => [xr _ | xr /eqP->]; rewrite ?eqxx/=. + by rewrite neq_lt floor_lt0 floor_gt0. +by apply/esym/(contraFF _ xr) => /orP[]; [exact: ltr0_real|exact: ger1_real]. +Qed. -Lemma ceil_gt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x). -Proof. by rewrite ltNge Num.Theory.ceil_le_int// -ltNge. Qed. +Lemma real_abs_floor_ge x : x \is Num.real -> `|x| <= `|Num.floor x|.+1%:R. +Proof. +rewrite -natr1 natr_absz => rx; have [x0|x0] := real_leP (@real0 R) rx. + by rewrite !ger0_norm ?real_floor_ge0// intr1 ltW ?real_lt_succ_floor. +rewrite !ltr0_norm ?floor_lt0// lerNl opprD intrN opprK lerBlDr. +by rewrite (le_trans (real_ge_floor rx)) ?lerDl. +Qed. -Lemma ceil_ge0 x : (- 1 < x) = (0 <= Num.ceil x). -Proof. by rewrite ltrNl floor_le0 floorN lerNl oppr0. Qed. +Lemma real_ceil_le_int_tmp x n : x \is Num.real -> + (Num.ceil x <= n) = (x <= n%:~R). +Proof. +rewrite -realN; move=> /(real_floor_ge_int_tmp (- n)). +by rewrite mulrNz lerNl => ->; rewrite lerN2. +Qed. -Lemma ceil_gt0 x : (0 < x) = (0 < Num.ceil x). -Proof. by rewrite -ceil_gt_int. Qed. +#[deprecated(since="mathcomp-analyss 1.10.0", + note="Use real_ceil_le_int_tmp instead.")] +Lemma real_ceil_le_int x n : x \is Num.real -> (x <= n%:~R) = (Num.ceil x <= n). +Proof. by move=> ?; rewrite real_ceil_le_int_tmp. Qed. -Lemma ceil_le0 x : (x <= 0) = (Num.ceil x <= 0). -Proof. by rewrite -Num.Theory.ceil_le_int. Qed. +Lemma real_ceil_gt_int x n : x \is Num.real -> (n < Num.ceil x) = (n%:~R < x). +Proof. +by move=> ?; rewrite [RHS]real_ltNge ?realz -?real_ceil_le_int_tmp ?ltNge. +Qed. -Lemma abs_ceil_ge x : `|x| <= `|Num.ceil x|.+1%:R. +Lemma real_ceil_eq x n : x \is Num.real -> + (Num.ceil x == n) = ((n - 1)%:~R < x <= n%:~R). Proof. -rewrite -natr1 natr_absz; have [x0|x0] := ltP 0 x. - by rewrite !gtr0_norm// -?ceil_gt0// (le_trans (Num.Theory.le_ceil _))// lerDl. -by rewrite !ler0_norm -?ceil_le0// opprK intr1 ltW// lt_succ_floor. +by move=> xr; apply/eqP/idP => [<-|]; [exact: real_ceil_itv|exact: ceil_def]. Qed. -End floor_ceil. +Lemma real_ceil_ge0 x : x \is Num.real -> (0 <= Num.ceil x) = (-1 < x). +Proof. by move=> ?; rewrite oppr_ge0 real_floor_le0 ?realN// ltrNl. Qed. + +Lemma ceil_lt0 x : Num.ceil x < 0 = (x <= -1). +Proof. by rewrite oppr_lt0 floor_gt0 lerNr. Qed. + +Lemma real_ceil_le0 x : x \is Num.real -> (Num.ceil x <= 0) = (x <= 0). +Proof. by move=> ?; rewrite real_ceil_le_int_tmp. Qed. + +Lemma ceil_gt0 x : (Num.ceil x > 0) = (x > 0). +Proof. by rewrite oppr_gt0 floor_lt0 oppr_lt0. Qed. + +Lemma ceil_neq0 x : (Num.ceil x != 0) = (x <= -1) || (x > 0). +Proof. by rewrite oppr_eq0 floor_neq0 oppr_lt0 lerNr orbC. Qed. + +Lemma real_abs_ceil_ge x : x \is Num.real -> `|x| <= `|Num.ceil x|.+1%:R. +Proof. by move=> ?; rewrite -normrN abszN real_abs_floor_ge ?realN. Qed. + +End num_trunc_floor_ceil. + +Section trunc_floor_ceil. +Context {R : archiDomainType}. +Implicit Type x : R. + +Lemma lt_succ_trunc x : x < (Num.trunc x).+1%:R. +Proof. exact: real_lt_succ_trunc. Qed. + +Lemma trunc_le_nat x n : (Num.trunc x <= n)%N = (x < n.+1%:R). +Proof. exact: real_trunc_le_nat. Qed. + +#[deprecated(since="mathcomp-analysis 1.10.0", note="Use floor_ge_int_tmp instead.")] +Lemma floor_ge_int x n : (n%:~R <= x) = (n <= Num.floor x). +Proof. exact: real_floor_ge_int. Qed. + +Lemma floor_ge_int_tmp x n : (n <= Num.floor x) = (n%:~R <= x). +Proof. exact: real_floor_ge_int_tmp. Qed. + +Lemma floor_lt_int x n : (Num.floor x < n) = (x < n%:~R). +Proof. exact: real_floor_lt_int. Qed. + +Lemma floor_eq x n : (Num.floor x == n) = (n%:~R <= x < (n + 1)%:~R). +Proof. exact: real_floor_eq. Qed. + +Lemma floor_ge0 x : (0 <= Num.floor x) = (0 <= x). +Proof. exact: real_floor_ge0. Qed. + +Lemma floor_le0 x : (Num.floor x <= 0) = (x < 1). +Proof. exact: real_floor_le0. Qed. + +Lemma abs_floor_ge x : `|x| <= `|Num.floor x|.+1%:R. +Proof. exact: real_abs_floor_ge. Qed. + +#[deprecated(since="mathcomp-analysis 1.10.0", note="Use ceil_le_int_tmp instead.")] +Lemma ceil_le_int x n : x <= n%:~R = (Num.ceil x <= n). +Proof. exact: real_ceil_le_int. Qed. + +Lemma ceil_le_int_tmp x n : (Num.ceil x <= n) = (x <= n%:~R). +Proof. exact: real_ceil_le_int_tmp. Qed. + +Lemma ceil_gt_int x n : (n < Num.ceil x) = (n%:~R < x). +Proof. exact: real_ceil_gt_int. Qed. + +Lemma ceil_eq x n : (Num.ceil x == n) = ((n - 1)%:~R < x <= n%:~R). +Proof. exact: real_ceil_eq. Qed. + +Lemma ceil_ge0 x : (0 <= Num.ceil x) = (-1 < x). +Proof. exact: real_ceil_ge0. Qed. + +Lemma ceil_le0 x : (Num.ceil x <= 0) = (x <= 0). +Proof. exact: real_ceil_le0. Qed. + +Lemma abs_ceil_ge x : `|x| <= `|Num.ceil x|.+1%:R. +Proof. exact: real_abs_ceil_ge. Qed. + +End trunc_floor_ceil. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to `ceil_gt_int`")] +#[deprecated(since="mathcomp-analysis 1.3.0", note="Use ceil_gt_int instead.")] Notation ceil_lt_int := ceil_gt_int (only parsing). Lemma natr_int {R : archiNumDomainType} n : n%:R \is a @Num.int R. diff --git a/reals/real_interval.v b/reals/real_interval.v index 2ec9c7af7..c69f90934 100644 --- a/reals/real_interval.v +++ b/reals/real_interval.v @@ -294,7 +294,7 @@ rewrite in_itv/= xy/= natrD -natr1 natr_absz intr_norm -addrA nat1r addrA. apply: ltr_pwDr; first by rewrite ltr0n. rewrite -lterBDl (le_trans (le_ceil _)) //= le_eqVlt; apply/predU1P; left. apply/esym/normr_idP. -rewrite ler0z -ceil_ge0 (lt_le_trans (@ltrN10 R))// subr_ge0. +rewrite ler0z ceil_ge0 (lt_le_trans (@ltrN10 R))// subr_ge0. by case: b xy => //= /ltW. Qed. diff --git a/reals/reals.v b/reals/reals.v index b3deb13bb..99a7489a3 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -514,7 +514,7 @@ Lemma Rfloor_ge_int x (n : int) : (n%:~R <= x)= (n%:~R <= Rfloor x). Proof. by rewrite ler_int floor_ge_int. Qed. Lemma Rfloor_lt_int x (z : int) : (x < z%:~R) = (Rfloor x < z%:~R). -Proof. by rewrite ltr_int floor_lt_int. Qed. +Proof. by rewrite ltr_int -floor_lt_int. Qed. Lemma Rfloor_le0 x : x <= 0 -> Rfloor x <= 0. Proof. by move=> ?; rewrite -Rfloor0 le_Rfloor. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 577d77bc0..55024c968 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1273,10 +1273,10 @@ rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|]; last first. by rewrite -natrX -2!natrM 2!ler_nat. have ?: 0 <= r * 2 ^+ n.+1 by rewrite mulr_ge0// (le_trans _ nr). rewrite -bigcup_seq /=; exists (trunc (r * 2 ^+ n.+1)). - rewrite /= mem_index_iota -trunc_ge_nat// -trunc_lt_nat//. + rewrite /= mem_index_iota trunc_ge_nat// trunc_lt_nat//. by rewrite !natrM natrX ler_pM2r// ltr_pM2r// nr. rewrite /= in_itv/= ler_pdivrMr// ltr_pdivlMr//. -by rewrite trunc_ge_nat// trunc_lt_nat// !leqnn. +by rewrite -trunc_ge_nat// -trunc_lt_nat// !leqnn. Qed. Lemma dyadic_itv_image n T (f : T -> \bar R) x : @@ -1397,7 +1397,7 @@ apply/negP => /andP[/allP An0]; rewrite mulf_eq0 => /orP[|]. rewrite pnatr_eq0 eqb0 notin_setE /B => /not_andP[] // /negP. rewrite -ltNge => fxn. have K : (trunc (fine (f x) * 2 ^+ n) < n * 2 ^ n)%N. - rewrite -trunc_lt_nat; last by rewrite mulr_ge0// ltW. + rewrite trunc_lt_nat; last by rewrite mulr_ge0// ltW. by rewrite natrM natrX ltr_pM2r// -lte_fin (fineK fxfin). have /[!mem_index_enum]/(_ isT) := An0 (Ordinal K). rewrite implyTb indicE mem_set ?mulr1; last first. @@ -1539,12 +1539,12 @@ case/cvg_ex => /= l; have [l0|l0] := leP 0%R l. move=> /(_ (`|ceil l|.+1 + n)%N) /= /(_ (leq_addl _ _)); apply/negP. rewrite -leNgt approx_x distrC (le_trans _ (lerB_normD _ _))// normrN. rewrite lerBrDl addSnnS natrD [leRHS]ger0_norm// lerD ?ler1n// natr_absz. - by rewrite !ger0_norm ?le_ceil// -ceil_ge0; apply: lt_le_trans l0. + by rewrite !ger0_norm ?le_ceil// ceil_ge0; apply: lt_le_trans l0. - move=> /cvgrPdist_lt/(_ _ ltr01)[n _]. move=> /(_ (`|floor l|.+1 + n)%N)/(_ (leq_addl _ _)); apply/negP. rewrite approx_x -leNgt distrC (le_trans _ (lerB_normD _ _))// normrN. rewrite lerBrDl addSnnS natrD [leRHS]ger0_norm// lerD ?ler1n// natr_absz. - by rewrite !ltr0_norm -?floor_lt0// mulrNz lerN2 ge_floor. + by rewrite !ltr0_norm ?floor_lt0// mulrNz lerN2 ge_floor. Qed. Lemma ecvg_approx (f0 : forall x, D x -> (0 <= f x)%E) x : @@ -3608,7 +3608,7 @@ apply/negP; rewrite -ltNge. rewrite -[X in _ * X](@fineK _ (mu (E `&` D))); last first. by rewrite fin_numElt muEDoo (lt_le_trans _ (measure_ge0 _ _)). rewrite lte_fin -ltr_pdivrMr. - rewrite pmulrn floor_lt_int intS ltz1D abszE. + rewrite pmulrn -floor_lt_int intS ltz1D abszE. by apply: le_trans (ler_norm _); rewrite ceil_floor//= lerDl. rewrite -lte_fin fineK. rewrite lt0e measure_ge0 andbT. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index e31680e77..348c68ffe 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1169,7 +1169,7 @@ have finite_set_F i : finite_set (F i). apply/negP; rewrite -ltNge lebesgue_measure_ball// lte_fin. rewrite -[M%:R]natr1 natr_absz ger0_norm; last first. by rewrite -[leLHS](ceil0 R) ceil_le. - by rewrite -ltr_pdivrMr// intr1 floor_lt_int ltzD1 ceil_floor// lerDl. + by rewrite -ltr_pdivrMr// intr1 -floor_lt_int ltzD1 ceil_floor// lerDl. have mur2_fin_num_ : mu (ball (0:R) (r%:num + 2))%R < +oo. by rewrite lebesgue_measure_ball// ltry. have FE : \sum_(n ?; exact: lt_trans. rewrite -EFinM /M lte_fin (le_lt_trans (ceil_ge _))//. rewrite -natr1 natr_absz ger0_norm ?ltrDl//. - by rewrite -ceil_ge0// (@lt_le_trans _ _ 0%R)// divr_ge0// fine_ge0. + by rewrite ceil_ge0// (@lt_le_trans _ _ 0%R)// divr_ge0// fine_ge0. rewrite big_seq [in leRHS]big_seq. apply: lee_sum => //= i /G0G'r [iG rBi]. rewrite -[leRHS]fineK//; last first. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index a36e041a9..9f5f90c1a 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -693,7 +693,7 @@ move=> /(_ `|floor r|%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. - by rewrite ltrNr oppr0 -floor_lt0. + by rewrite ltrNr oppr0 floor_lt0. by rewrite mulrNz lerNl opprK ge_floor. Qed. @@ -703,7 +703,7 @@ rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry. move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=. rewrite andbT lte_fin ltNge. have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0). -by rewrite natr_absz gtr0_norm// ?le_ceil// -ceil_gt0. +by rewrite natr_absz gtr0_norm// ?le_ceil// ceil_gt0. Qed. End erealwithrays. diff --git a/theories/measure.v b/theories/measure.v index afd7b3202..08ca5e0f6 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -2330,7 +2330,7 @@ Proof. move=> infA; apply/eqyP => r r0. 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. + 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. by move=> i /[!inE] /BA /mem_set iA; rewrite diracE iA. diff --git a/theories/normedtype.v b/theories/normedtype.v index 171b7196d..d57a751fa 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -287,10 +287,10 @@ Proof. apply/seteqP; split => // x _; have [x0|x0] := ltP 0%R x. exists `|ceil x|.+1 => //. rewrite /ball /= sub0r normrN gtr0_norm// (le_lt_trans (ceil_ge _))//. - by rewrite -natr1 natr_absz -abszE gtz0_abs// -?ceil_gt0// ltr_pwDr. + by rewrite -natr1 natr_absz -abszE gtz0_abs// ?ceil_gt0// ltr_pwDr. exists `|ceil (- x)|.+1 => //. rewrite /ball /= sub0r normrN ler0_norm// (le_lt_trans (ceil_ge _))//. -rewrite -natr1 natr_absz -abszE gez0_abs ?ltr_pwDr// -ceil_ge0 ltrNl opprK. +rewrite -natr1 natr_absz -abszE gez0_abs ?ltr_pwDr// ceil_ge0 ltrNl opprK. by rewrite (le_lt_trans x0). Qed. @@ -662,7 +662,7 @@ split=> [/cvgryPge|/cvgnyPge] Foo. by apply/cvgnyPge => A; near do rewrite -(@ler_nat R); apply: Foo. apply/cvgryPgey; near=> A; near=> n. rewrite pmulrn ceil_le_int// [ceil _]intEsign. -by rewrite le_gtF ?expr0 ?mul1r ?lez_nat -?ceil_ge0//; near: n; apply: Foo. +by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo. Unshelve. all: by end_near. Qed. Section monotonic_itv_bigcup. diff --git a/theories/realfun.v b/theories/realfun.v index a6aa1e039..dec7802d5 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -202,7 +202,7 @@ exists (fun n => sval (cid (He (PosNum (invn n))))). rewrite distrC (lt_le_trans xpt)// -(@invrK _ r) lef_pV2 ?posrE ?invr_gt0//. 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. + by rewrite natr_absz gtr0_norm ?ceil_gt0 ?invr_gt0// ceil_ge. move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)). rewrite /sval/=; case: cid => // x [px xpn]. by rewrite leNgt distrC => /negP. @@ -260,7 +260,7 @@ exists (fun n => sval (cid (He (PosNum (invn n))))). rewrite distrC (lt_le_trans xpt)// -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0//. 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 ?le_ceil ?num_real. + by rewrite natr_absz gtr0_norm ?ceil_gt0 ?invr_gt0 ?le_ceil ?num_real. move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)). rewrite /sval/=; case: cid => // x [px xpn]. by rewrite ltNge distrC => /negP. diff --git a/theories/sequences.v b/theories/sequences.v index 8de5404f2..951f2c9f0 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -2771,7 +2771,7 @@ have : cvg (a @ \oo). rewrite -ltf_pV2 ?(posrE,divr_gt0)// invrK -addn1 natrD. rewrite natr_absz gtr0_norm. by rewrite (le_lt_trans (ceil_ge _)) // ltrDl. - by rewrite -ceil_gt0 invr_gt0 divr_gt0. + by rewrite ceil_gt0 invr_gt0 divr_gt0. exists n.+1; rewrite -ltr_pdivlMl //. have /lt_trans : (r n.+1)%:num < n.+1%:R^-1. have [_ ] : P n.+1 (a n, r n) (a n.+1, r n.+1) by apply: (Pf (n, ar n)).