replace some `|Num.floor _| with Num.trunc _

classical/mathcomp_extra.v

@@ -433,9 +433,30 @@ Section floor_ceil.
 Context {R : archiDomainType}.
 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.
+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 trunc_ge_nat x (n : nat) : 0 <= x -> (n%:R <= x) = (n <= Num.trunc x)%N.
+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.
+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 ge_floor x : (Num.floor x)%:~R <= x.
 Proof. exact: Num.Theory.ge_floor. Qed.
 
+Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
+Proof. exact: Num.Theory.lt_succ_floor. Qed.
+
 Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x).
 Proof. exact: Num.Theory.floor_ge_int. Qed.
 
@@ -451,17 +472,14 @@ Proof. by rewrite -ltzD1 add0r -floor_lt_int. Qed.
 Lemma floor_lt0 x : (x < 0) = (Num.floor x < 0).
 Proof. by rewrite -floor_lt_int. Qed.
 
-Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
-Proof. exact: Num.Theory.lt_succ_floor. Qed.
-
 Lemma floor_eq x m : (Num.floor x == m) = (m%:~R <= x < (m + 1)%:~R).
 Proof.
 apply/eqP/idP; [move=> <-|by move=> /Num.Theory.floor_def ->].
 by rewrite Num.Theory.ge_floor//= Num.Theory.lt_succ_floor.
 Qed.
 
 Lemma floor_neq0 x : (Num.floor x != 0) = (x < 0) || (x >= 1).
-Proof. by rewrite neq_lt -floor_lt_int gtz0_ge1 -floor_ge_int. Qed.
+Proof. by rewrite floor_eq negb_and -ltNge -leNgt. Qed.
 
 #[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.le_ceil` instead")]
 Lemma ceil_ge x : x <= (Num.ceil x)%:~R.

reals/real_interval.v

@@ -150,10 +150,8 @@ 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 /= 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// intrD1 lt_succ_floor.
+rewrite in_itv /= andbT => xy; exists (trunc y).+1 => //=.
+by rewrite in_itv /= xy /= lt_succ_trunc.
 Qed.
 
 Lemma itv_o_inftyEbigcup x :
@@ -240,12 +238,8 @@ 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|%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 rewrite intrD1 ltW// lt_succ_floor.
-- by rewrite posrE// ltr_pwDr// ler0z floor_ge0 invr_ge0 ltW.
-- by rewrite posrE invr_gt0.
+rewrite lte_fin -subr_gt0 => fgx; exists (trunc (fx - gx)^-1) => //.
+by rewrite /E/= fxE gxE lee_fin invf_ple ?posrE//; apply/ltW/lt_succ_trunc.
 Qed.
 
 End set_ereal.
@@ -257,10 +251,8 @@ 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|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
-rewrite lerD2l lerN2 -lef_pV2 ?invrK//; last by rewrite posrE.
-rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//.
-by rewrite intrD1 lt_succ_floor.
+have := rx (trunc e^-1) I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
+by rewrite lerB// invf_ple ?posrE//; apply/ltW/lt_succ_trunc.
 Qed.
 
 Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) :

reals/reals.v

@@ -529,12 +529,8 @@ Proof. exact: Num.Theory.floor_le. 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// invr_ge0 subr_ge0 ltW.
-by rewrite intrD1 lt_succ_floor.
+move=> yx; exists (trunc (x - y)^-1).
+by rewrite -ltrBrDl invf_plt 1?posrE 1?subr_gt0// lt_succ_trunc.
 Qed.
 
 End FloorTheory.

theories/lebesgue_integral.v

@@ -1247,33 +1247,26 @@ Local Notation I := dyadic_itv.
 Lemma dyadic_itv_subU n k : [set` I n k] `<=`
   [set` I n.+1 k.*2] `|` [set` I n.+1 k.*2.+1].
 Proof.
-move=> r /=; rewrite in_itv /= => /andP[Ir rI].
-have [rk|rk] := ltP r (k.*2.+1%:R * (2%:R ^- n.+1)); [left|right].
-- rewrite in_itv /= rk andbT (le_trans _ Ir)// -muln2.
-  rewrite natrM exprS invrM ?unitfE// ?expf_neq0// -mulrA (mulrCA 2).
-  by rewrite divrr ?unitfE// mulr1.
-- rewrite in_itv /= rk /= (lt_le_trans rI)// -doubleS.
-  rewrite -muln2 natrM exprS invrM ?unitfE// ?expf_neq0// -mulrA (mulrCA 2).
-  by rewrite divrr ?unitfE// mulr1.
+move=> r Hr; apply/orP; rewrite -itv_splitU ?bnd_simp/=; last first.
+  by rewrite !ler_pM2r// !ler_nat leqW//=.
+move: Hr; apply/subitvP; rewrite {r}!subitvE !bnd_simp exprSr -muln2.
+rewrite ler_pdivrMr// mulrA divfK// -natrM lexx/=.
+by rewrite ler_pdivlMr// mulrA divfK// -natrM ler_nat.
 Qed.
 
 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]|]; last first.
-  rewrite -bigcup_seq => -[/= k] /[!mem_index_iota] /andP[nk kn].
-  rewrite !in_itv /= => /andP[knr rkn]; apply/andP; split.
-    by rewrite (le_trans _ knr)// ler_pdivlMr// -natrX -natrM ler_nat.
-  by rewrite (lt_le_trans rkn)// ler_pdivrMr// -natrX -natrM ler_nat.
-rewrite -bigcup_seq /=; exists `|floor (r * 2 ^+ n.+1)|%N.
-  rewrite /= mem_index_iota -ltz_nat -lez_nat gez0_abs; last first.
-    by rewrite floor_ge0 mulr_ge0// (le_trans _ nr).
-  rewrite -floor_ge_int -floor_lt_int.
-  by rewrite !PoszM -!natrXE !rmorphM !rmorphXn /= ler_wpM2r ?ltr_pM2r.
-rewrite /= in_itv /= ler_pdivrMr// ltr_pdivlMr//.
-rewrite pmulrn [(`|_|.+1%:R)]pmulrn intS addrC gez0_abs; last first.
-  by rewrite floor_ge0 mulr_ge0 ?exprn_ge0 // (le_trans _ nr).
-by rewrite ge_floor lt_succ_floor.
+  rewrite -bigcup_seq => -[/= k] /[!mem_index_iota] nkn; apply: subitvP.
+  rewrite subitvE !bnd_simp ler_pdivlMr// ler_pdivrMr//.
+  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//.
+  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.
 Qed.
 
 Lemma dyadic_itv_image n T (f : T -> \bar R) x :
@@ -1406,14 +1399,10 @@ have K : (`|floor (fine (f x) * 2 ^+ n)| < n * 2 ^ n)%N.
 have /[!mem_index_enum]/(_ isT) := An0 (Ordinal K).
 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 _ (ge_floor _))//.
-    by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// ltW.
-  rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _))//.
-  rewrite -[in leRHS]natr1 -intrD1 lerD2r// -{1}(@gez0_abs (floor _))//.
-  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//.
+  rewrite in_itv/= ler_pdivrMr// ltr_pdivlMr// [leLHS]pmulrn [ltRHS]pmulrn intS.
+  by rewrite [1 + _]addrC gez0_abs ?floor_ge0 ?pmulr_rge0// floor_itv/=.
+apply/negP; rewrite mulf_eq0 -exprVn negb_or expf_neq0//= andbT.
+rewrite pnatr_eq0 absz_eq0 floor_neq0 -ler_pdivrMr//.
 apply/orP; right; apply/ltW; near: n.
 exact: near_infty_natSinv_expn_lt (PosNum fx_gt0).
 Unshelve. all: by end_near. Qed.