From 880c4ecc1c9ae177444eed6625f85b01f9d7dac0 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 17 Jun 2024 23:08:36 +0900 Subject: [PATCH] fixes #330 --- CHANGELOG_UNRELEASED.md | 6 +++ theories/altreals/realsum.v | 6 +-- theories/lebesgue_integral.v | 2 +- theories/lebesgue_stieltjes_measure.v | 8 +-- theories/reals.v | 71 +++++++++++++++------------ theories/topology.v | 5 +- 6 files changed, 57 insertions(+), 41 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 67bb43c3b6..b539a08c61 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,8 +4,14 @@ ### Added +- in `reals.v`: + + lemma `mem_rg1_floor` + ### Changed +- in `reals.v`: + + definitions `Rceil`, `ceil`, `Rfloor`, `floor` + ### Renamed ### Generalized diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v index c5eac8ae63..457c1e6298 100644 --- a/theories/altreals/realsum.v +++ b/theories/altreals/realsum.v @@ -145,8 +145,7 @@ set F := [pred x | _]; have le: {subset F <= [pred x | `[< exists p, x \in E p > pose j := `|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 -RfloorE; apply lt_succ_Rfloor. + by rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0 // 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. @@ -160,9 +159,10 @@ apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first. by have:= fsvalP m; rewrite in_fset => /le_sEi. 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_Rfloor M; rewrite RfloorE -addn1. +have /andP[_] := mem_rg1_floor M; rewrite -addn1. by rewrite natrD /= mulr1n pmulrn -{1}[floor _]gez0_abs // floor_ge0. Qed. + End SummableCountable. (* -------------------------------------------------------------------- *) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 0670dfa84d..a496506a1a 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1293,7 +1293,7 @@ rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|]. by rewrite mulr_ge0// (le_trans _ nr). apply: (@le_trans _ _ (reals.floor (n * 2 ^ n.+1)%:R)); last first. by apply: le_floor; rewrite natrM natrX ler_pM2r. - by rewrite floor_natz intz. + by rewrite -floor_ge_int. rewrite -ltz_nat gez0_abs; last first. by rewrite floor_ge0 mulr_ge0// (le_trans _ nr). rewrite -(@ltr_int R) (le_lt_trans (reals.floor_le _))//. diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 4a29cb6577..5c977eff30 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -481,11 +481,11 @@ Proof. exists (fun k => `](- k%:R), k%:R]%classic). apply/esym; rewrite -subTset => /= x _ /=. exists `|(floor `|x|%R + 1)%R|%N; rewrite //= in_itv/=. - rewrite !natr_absz intr_norm intrD -RfloorE. - suff: `|x| < `|Rfloor `|x| + 1| by rewrite ltr_norml => /andP[-> /ltW->]. + rewrite !natr_absz intr_norm intrD. + suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->]. rewrite [ltRHS]ger0_norm//. - by rewrite (le_lt_trans _ (lt_succ_Rfloor _))// ?ler_norm. - by rewrite addr_ge0// -Rfloor0 le_Rfloor. + by rewrite (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. Qed. diff --git a/theories/reals.v b/theories/reals.v index cf231eb6e7..fff38c807e 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -244,15 +244,15 @@ Variable R : realType. Implicit Types x y : R. Definition floor_set x := [set y : R | (y \is a Rint) && (y <= x)]. -Definition Rfloor x : R := sup (floor_set x). +Definition floor x : int := Num.floor x. -Definition floor x : int := Rtoint (Rfloor x). +Definition Rfloor x : R := (floor x)%:~R. Definition range1 (x : R) := [set y | x <= y < x + 1]. -Definition Rceil x := - Rfloor (- x). +Definition ceil x := Num.ceil x. -Definition ceil x := - floor (- x). +Definition Rceil x : R := (ceil x)%:~R. End RealDerivedOps. @@ -470,27 +470,29 @@ by rewrite absz_eq0 subr_eq0 eq_sym (negbTE ne_yz). Qed. Lemma isint_Rfloor x : Rfloor x \is a Rint. -Proof. by case/andP: (sup_in_floor_set x). Qed. +Proof. by rewrite inE; exists (floor x). Qed. Lemma RfloorE x : Rfloor x = (floor x)%:~R. -Proof. by rewrite /floor RtointK ?isint_Rfloor. Qed. +Proof. by []. Qed. -Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x. +Lemma mem_rg1_floor x : (range1 (floor x)%:~R) x. Proof. rewrite /range1/mkset. -have /andP[_ ->] /= := sup_in_floor_set x. -have [|] := pselect ((floor_set x) (Rfloor x + 1)); last first. - rewrite /floor_set => /negP. - by rewrite negb_and -ltNge rpredD // ?(Rint1, isint_Rfloor). -move/ubP : (sup_upper_bound (has_sup_floor_set x)) => h/h. -by rewrite gerDl ler10. +rewrite [X in _ + X](_ : 1 = 1%:~R)// -intrD lt_succ_floor ?andbT ?num_real//. +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. Lemma Rfloor_le x : Rfloor x <= x. Proof. by case/andP: (mem_rg1_Rfloor x). Qed. Lemma floor_le x : (floor x)%:~R <= x. -Proof. by rewrite -RfloorE; exact: Rfloor_le. Qed. +Proof. by rewrite ge_floor// num_real. Qed. Lemma lt_succ_Rfloor x : x < Rfloor x + 1. Proof. by case/andP: (mem_rg1_Rfloor x). Qed. @@ -547,25 +549,27 @@ Lemma Rfloor_lt0 x : x < 0 -> Rfloor x < 0. Proof. by move=> x0; rewrite (le_lt_trans _ x0) // Rfloor_le. Qed. Lemma floor_natz n : floor (n%:R : R) = n%:~R :> int. -Proof. by rewrite /floor (Rfloor_natz n) Rtointz intz. Qed. +Proof. by have /intr_inj -> := Rfloor_natz n; rewrite -pmulrn/= natz. Qed. Lemma floor0 : floor (0 : R) = 0. -Proof. by rewrite /floor Rfloor0 (_ : 0 = 0%:R) // Rtointn. Qed. +Proof. by rewrite /floor floor0. Qed. Lemma floor1 : floor (1 : R) = 1. -Proof. by rewrite /floor Rfloor1 (_ : 1 = 1%:R) // Rtointn. Qed. +Proof. by rewrite /floor floor1. Qed. Lemma floor_ge0 x : (0 <= floor x) = (0 <= x). -Proof. by rewrite -(@ler_int R) -RfloorE -Rfloor_ge_int. Qed. +Proof. by rewrite -floor_ge_int// num_real. Qed. Lemma floor_le0 x : x <= 0 -> floor x <= 0. -Proof. by move=> ?; rewrite -(@ler_int R) -RfloorE Rfloor_le0. Qed. +Proof. by move=> x0; rewrite -floor0 Num.Theory.floor_le. Qed. Lemma floor_lt0 x : x < 0 -> floor x < 0. -Proof. by move=> ?; rewrite -(@ltrz0 R) RtointK ?isint_Rfloor// Rfloor_lt0. Qed. +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}. -Proof. by move=>*; rewrite -(@ler_int R) !RtointK ?isint_Rfloor ?le_Rfloor. Qed. +Proof. by move=> a b ab; rewrite Num.Theory.floor_le. Qed. Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x >= 1). Proof. @@ -577,7 +581,9 @@ apply/idP/orP => [|[x0|/le_floor r1]]; first rewrite neq_lt => /orP[x0|x0]. Qed. Lemma lt_succ_floor x : x < (floor x)%:~R + 1. -Proof. by rewrite -RfloorE lt_succ_Rfloor. Qed. +Proof. +by rewrite [X in _ + X](_ : 1 = 1%:~R)// -intrD 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. @@ -592,7 +598,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 -RfloorE lt_succ_Rfloor. +by rewrite lt_succ_floor. Qed. End FloorTheory. @@ -603,25 +609,25 @@ Variable R : realType. Implicit Types x y : R. Lemma isint_Rceil x : Rceil x \is a Rint. -Proof. by rewrite /Rceil rpredN isint_Rfloor. Qed. +Proof. by rewrite /Rceil RintC. Qed. Lemma Rceil0 : Rceil 0 = 0 :> R. -Proof. by rewrite /Rceil oppr0 Rfloor0 oppr0. Qed. +Proof. by rewrite /Rceil /ceil ceil0. Qed. Lemma Rceil_ge x : x <= Rceil x. -Proof. by rewrite /Rceil lerNr Rfloor_le. Qed. +Proof. by rewrite /Rceil le_ceil// num_real. Qed. Lemma le_Rceil : {homo (@Rceil R) : x y / x <= y}. -Proof. by move=> x y ?; rewrite lerNl opprK le_Rfloor // lerNl opprK. Qed. +Proof. by move=> x y ?; rewrite /Rceil /ceil ler_int ceil_le. Qed. Lemma Rceil_ge0 x : 0 <= x -> 0 <= Rceil x. -Proof. by move=> ?; rewrite -Rceil0 le_Rceil. Qed. +Proof. by move=> x0; rewrite /Rceil ler0z -(ceil0 R) ceil_le. Qed. Lemma RceilE x : Rceil x = (ceil x)%:~R. -Proof. by rewrite /Rceil /ceil RfloorE mulrNz. Qed. +Proof. by []. Qed. Lemma ceil_ge x : x <= (ceil x)%:~R. -Proof. by rewrite -RceilE; exact: Rceil_ge. Qed. +Proof. by rewrite le_ceil// num_real. Qed. Lemma ceil_ge0 x : 0 <= x -> 0 <= ceil x. Proof. by move/(ge_trans (ceil_ge x)); rewrite -(ler_int R). Qed. @@ -636,12 +642,13 @@ Lemma le_ceil : {homo @ceil R : x y / x <= y}. Proof. by move=> x y xy; rewrite lerNl opprK le_floor // lerNl opprK. Qed. Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (ceil x <= z). -Proof. by rewrite /ceil lerNl -floor_ge_int// -lerNr mulrNz opprK. Qed. +Proof. by rewrite /ceil; apply: ceil_le_int; rewrite num_real. Qed. Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < ceil x). Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed. -Lemma ceilN x : ceil (- x) = - floor x. Proof. by rewrite /ceil opprK. Qed. +Lemma ceilN x : ceil (- x) = - floor x. Proof. +Proof. by rewrite /ceil /Num.ceil opprK. Qed. Lemma floorN x : floor (- x) = - ceil x. Proof. by rewrite /ceil opprK. Qed. diff --git a/theories/topology.v b/theories/topology.v index c92ca0ad37..97b02bf8bb 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -5682,7 +5682,10 @@ Proof. by rewrite /distN invr0 reals.floor0. Qed. Local Lemma distN_nat (n : nat): distN (n%:R^-1) = n. Proof. -by rewrite /distN invrK floor_natz -[RHS]distn0; congr absz; rewrite subr0 intz. +rewrite /distN invrK. +apply/eqP; rewrite -(@eqr_nat R) natr_absz ger0_norm//; last first. + by rewrite -(floor0 R) floor_le. +by rewrite -intrEfloor intrEge0. Qed. Local Lemma distN_le e1 e2 : e1 > 0 -> e1 <= e2 -> (distN e2 <= distN e1)%N.