Skip to content

Commit

Permalink
fixes #330
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Jun 17, 2024
1 parent 9c311a9 commit 880c4ec
Show file tree
Hide file tree
Showing 6 changed files with 57 additions and 41 deletions.
6 changes: 6 additions & 0 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,14 @@

### Added

- in `reals.v`:
+ lemma `mem_rg1_floor`

### Changed

- in `reals.v`:
+ definitions `Rceil`, `ceil`, `Rfloor`, `floor`

### Renamed

### Generalized
Expand Down
6 changes: 3 additions & 3 deletions theories/altreals/realsum.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.

(* -------------------------------------------------------------------- *)
Expand Down
2 changes: 1 addition & 1 deletion theories/lebesgue_integral.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 _))//.
Expand Down
8 changes: 4 additions & 4 deletions theories/lebesgue_stieltjes_measure.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
71 changes: 39 additions & 32 deletions theories/reals.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.

Expand Down
5 changes: 4 additions & 1 deletion theories/topology.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit 880c4ec

Please sign in to comment.