diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index f7c05dd23..61b10a1ac 100644 --- a/classical/mathcomp_extra.v +++ b/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,9 +472,6 @@ 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 ->]. @@ -461,7 +479,7 @@ 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. diff --git a/reals/real_interval.v b/reals/real_interval.v index a9ca280f6..b9534c309 100644 --- a/reals/real_interval.v +++ b/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) : diff --git a/reals/reals.v b/reals/reals.v index 2b1fd3ad1..c6a76c5d1 100644 --- a/reals/reals.v +++ b/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. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 3ac62afdf..4e34b84d3 100644 --- a/theories/lebesgue_integral.v +++ b/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.