From db04bc9bc332ea6da9866459c8f607e6b39ce549 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Mon, 9 Dec 2024 17:16:30 +0000 Subject: [PATCH] Fix some deprecation warnings about ceil_ge (#1415) * Fix some deprecation warnings about ceil_ge --- reals/real_interval.v | 9 +++--- theories/lebesgue_integral.v | 54 ++++++++++++++---------------------- theories/lebesgue_measure.v | 28 ++++++++----------- theories/normedtype.v | 2 +- theories/realfun.v | 10 +++---- 5 files changed, 42 insertions(+), 61 deletions(-) diff --git a/reals/real_interval.v b/reals/real_interval.v index 15db5ad76..a9ca280f6 100644 --- a/reals/real_interval.v +++ b/reals/real_interval.v @@ -274,7 +274,7 @@ rewrite in_itv/= => /andP[sx xs]; exists `|ceil (s - x)^-1|%N => //=. rewrite in_itv/= sx/= lerBrDl addrC -lerBrDl. rewrite -[in X in _ <= X](invrK (s - x)) ler_pV2. - rewrite -natr1 natr_absz ger0_norm; last first. - by rewrite -ceil_ge0 (lt_le_trans (ltrN10 R))// invr_ge0 subr_ge0 ltW. + by rewrite -(ceil0 R) ceil_le// invr_ge0 subr_ge0 ltW. by rewrite (@le_trans _ _ (ceil (s - x)^-1)%:~R)// ?lerDl// ceil_ge. - by rewrite inE unitfE ltr0n andbT pnatr_eq0. - by rewrite inE invr_gt0 subr_gt0 xs andbT unitfE invr_eq0 subr_eq0 gt_eqF. @@ -298,9 +298,8 @@ Proof. apply/seteqP; split=> y; rewrite /= !in_itv/= andbT; last first. by move=> [k _ /=]; move: b => [|] /=; rewrite in_itv/= => /andP[//] /ltW. move=> xy; exists `|ceil (y - x)|%N => //=; rewrite in_itv/= xy/= -lerBlDl. -rewrite !natr_absz/= ger0_norm -?ceil_ge0 ?ceil_ge//. -rewrite (lt_le_trans (ltrN10 R))// subr_ge0. -by case: b xy => //= /ltW. +rewrite natr_absz ger0_norm ?ceil_ge//. +by rewrite -(ceil0 R) ceil_le// subr_ge0 (lteifW xy). Qed. Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) : @@ -310,7 +309,7 @@ Proof. have /(congr1 (fun x => -%R @` x)) := itv_bnd_infty_bigcup (~~ b) (- x). rewrite opp_itv_bnd_infty negbK opprK => ->; rewrite image_bigcup. apply eq_bigcupr => k _; apply/seteqP; split=> [_ /= -[r rbxk <-]|y/= yxkb]. - by rewrite oppr_itv/= opprB addrC. + by rewrite oppr_itv/= opprB addrC. by exists (- y); [rewrite oppr_itv/= negbK opprD opprK|rewrite opprK]. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index dabbbcc8d..3ac62afdf 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1548,19 +1548,15 @@ move=> Dx fxoo; have approx_x n : approx n x = n%:R. by rewrite fgen_A0 // ?mulr0 // fxoo leey. case/cvg_ex => /= l; have [l0|l0] := leP 0%R l. - move=> /cvgrPdist_lt/(_ _ ltr01) -[n _]. - move=> /(_ (`|ceil l|.+1 + n)%N) /= /(_ (leq_addl _ _)). - rewrite approx_x. - apply/negP; rewrite -leNgt distrC (le_trans _ (lerB_normD _ _)) //. - rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//. - rewrite natrD lerD// ?ler1n// ger0_norm // (le_trans (ceil_ge _)) //. - by rewrite -(@gez0_abs (ceil _)) // -ceil_ge0 (lt_le_trans _ l0). + 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. - move=> /cvgrPdist_lt/(_ _ ltr01)[n _]. move=> /(_ (`|floor l|.+1 + n)%N)/(_ (leq_addl _ _)); apply/negP. - rewrite approx_x -leNgt distrC (le_trans _ (lerB_normD _ _))//. - rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//. - rewrite natrD lerD ?ler1n// ltr0_norm// (@le_trans _ _ (- floor l)%:~R)//. - by rewrite mulrNz lerNl opprK ge_floor. - by rewrite -(@lez0_abs (floor _))// -floor_le0// (lt_le_trans l0). + 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. Qed. Lemma ecvg_approx (f0 : forall x, D x -> (0 <= f x)%E) x : @@ -2350,23 +2346,20 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)). - rewrite gt0_mulye//; apply/cvgeyPgey; near=> M. have M0 : (0 <= M)%R by []. rewrite /g; case: (f x) fx0 => [r r0|_|//]; last first. - exists 1%N => // m /= m0. - by rewrite mulry gtr0_sg// ?mul1e ?leey// ltr0n. + by exists 1%N => // m /= m0; rewrite mulry gtr0_sg// ?ltr0n// mul1e leey. near=> n; rewrite lee_fin -ler_pdivrMr//. near: n; exists `|ceil (M / r)|%N => // m /=. rewrite -(ler_nat R); apply: le_trans. - rewrite natr_absz ger0_norm ?ceil_ge// -ceil_ge0// (lt_le_trans (ltrN10 _))//. - by rewrite divr_ge0// ?ltW. + rewrite natr_absz ger0_norm ?ceil_ge//. + by rewrite -(ceil0 R) ceil_le// divr_ge0// ltW. - rewrite lt0_mulye//; apply/cvgeNyPleNy; near=> M; have M0 : (M <= 0)%R by []. rewrite /g; case: (f x) fx0 => [r r0|//|_]; last first. - exists 1%N => // m /= m0. - by rewrite mulrNy gtr0_sg// ?ltr0n// mul1e ?leNye. + by exists 1%N => // m /= m0; rewrite mulrNy gtr0_sg// ?ltr0n// mul1e leNye. near=> n; rewrite lee_fin -ler_ndivrMr//. near: n; exists `|ceil (M / r)|%N => // m /=. rewrite -(ler_nat R); apply: le_trans. - rewrite natr_absz ger0_norm ?ceil_ge// -ceil_ge0// (lt_le_trans (ltrN10 _))//. - by rewrite -mulrNN mulr_ge0// lerNr oppr0// ltW// invr_lt0. + by rewrite pmulrn abszE ceil_ge_int ler_norm. - rewrite -fx0 mule0 /g -fx0. under eq_fun do rewrite mule0/=. (*TODO: notation broken*) exact: cvg_cst. @@ -2387,9 +2380,8 @@ rewrite -lee_pdivrMr//; last first. near: n. exists `|ceil (M * (fine (\int[mu]_(x in D) f x))^-1)|%N => //. move=> n /=; rewrite -(@ler_nat R) -lee_fin; apply: le_trans. -rewrite lee_fin natr_absz ger0_norm ?ceil_ge// -ceil_ge0//. -rewrite (lt_le_trans (ltrN10 _))//. -by rewrite mulr_ge0// ?invr_ge0//; exact/fine_ge0/integral_ge0. +rewrite lee_fin natr_absz ger0_norm ?ceil_ge//. +by rewrite -(ceil0 R) ceil_le// divr_ge0//; exact/fine_ge0/integral_ge0. Unshelve. all: by end_near. Qed. Lemma ge0_integralZr k : (forall x, D x -> 0 <= f x) -> @@ -2627,8 +2619,7 @@ move=> muD0; pose g : (T -> \bar R)^nat := fun n => cst n%:R%:E. have <- : (fun t => limn (g^~ t)) = cst +oo. rewrite funeqE => t; apply/cvg_lim => //=. apply/cvgeryP/cvgryPge => M; exists `|ceil M|%N => //= m. - rewrite /= -(ler_nat R); apply: le_trans. - by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm. + by rewrite /= pmulrn ceil_ge_int// -lez_nat abszE; apply/le_trans/ler_norm. rewrite monotone_convergence //. - under [in LHS]eq_fun do rewrite integral_cstr. apply/cvg_lim => //; apply/cvgeyPge => M. @@ -2636,10 +2627,9 @@ rewrite monotone_convergence //. exists 1%N => // m /= m0; move: muDoo; rewrite leye_eq => /eqP ->. by rewrite mulry gtr0_sg ?mul1e ?leey// ltr0n. exists `|ceil (M / fine (mu D))|%N => // m /=. - rewrite -(ler_nat R) => MDm; rewrite -(@fineK _ (mu D)) ?ge0_fin_numE//. + rewrite -lez_nat abszE => MDm; rewrite -(@fineK _ (mu D)) ?ge0_fin_numE//. rewrite -lee_pdivrMr; last by rewrite fine_gt0// lt0e muD0 measure_ge0. - rewrite lee_fin (le_trans _ MDm)//. - by rewrite natr_absz (le_trans (ceil_ge _))// ler_int ler_norm. + by rewrite lee_fin pmulrn ceil_ge_int// (le_trans _ MDm)// ler_norm. - by move=> n; exact: measurable_cst. - by move=> n x Dx; rewrite lee_fin. - by move=> t Dt n m nm; rewrite /g lee_fin ler_nat. @@ -3515,9 +3505,8 @@ 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 -natr1 natr_absz ger0_norm. - by rewrite (le_lt_trans (ceil_ge _))// ltrDl. - by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _))// divr_ge0. + 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. suff: E `&` D = E by move=> ->; exact/eqP. @@ -3780,9 +3769,8 @@ move=> mf; split=> [iDf0|Df0]. by rewrite lt0e abse_ge0 abse_eq0 ft0 ltey. - by rewrite inE unitfE invr_eq0 pnatr_eq0 /= invr_gt0. rewrite invrK /m -natr1 natr_absz ger0_norm; last first. - by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _)). - rewrite (@le_trans _ _ ((fine `|f t|)^-1 + 1)%R) ?lerDl//. - by rewrite lerD2r// ceil_ge. + by rewrite -(ceil0 R) ceil_le. + by rewrite intrD1 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 ecde135c1..7491d4928 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -450,19 +450,15 @@ Proof. rewrite [X in measurable X](_ : _ = \bigcup_k (D `&` ([set x | - k%:R%:E <= f x] `&` [set x | f x <= k%:R%:E]))). apply: bigcupT_measurable => k; rewrite -(setIid D) setIACA. - by apply: measurableI; [exact: emeasurable_fun_c_infty| - exact: emeasurable_fun_infty_c]. + exact/measurableI/emeasurable_fun_infty_c/emeasurable_fun_c_infty. rewrite predeqE => t; split => [/= [Dt ft]|]. - have [ft0|ft0] := leP 0%R (fine (f t)). - exists `|ceil (fine (f t))|%N => //=; split => //; split. - by rewrite -{2}(fineK ft)// lee_fin (le_trans _ ft0)// lerNl oppr0. - rewrite natr_absz ger0_norm; last first. - by rewrite -ceil_ge0 (lt_le_trans _ ft0). - by rewrite -(fineK ft) lee_fin ceil_ge. - exists `|floor (fine (f t))|%N => //=; split => //; split. - rewrite natr_absz ltr0_norm -?floor_lt0// EFinN. - by rewrite -{2}(fineK ft) lee_fin mulrNz opprK ge_floor// ?num_real. - by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)). + exists `|ceil `|fine (f t)| |%N => //=; split=> //; split. + rewrite -[leRHS](fineK ft) lee_fin lerNl pmulrn abszE ceil_ge_int ger0_norm. + by rewrite ceil_le// -normrN ler_norm. + by rewrite -(ceil0 R) ceil_le. + rewrite -[leLHS](fineK ft) lee_fin pmulrn abszE ceil_ge_int ger0_norm. + by rewrite ceil_le// ler_norm. + by rewrite -(ceil0 R) ceil_le. move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt. by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry. Qed. @@ -718,7 +714,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// ?ceil_ge// -ceil_gt0. +by rewrite natr_absz gtr0_norm// ?le_ceil// -ceil_gt0. Qed. End erealwithrays. @@ -2857,9 +2853,9 @@ have finite_set_F i : finite_set (F i). - by move=> /= x [n Fni Bnx]; exists n => //; exists i. have {CFi Fir2} := le_trans MC (le_trans CFi Fir2). apply/negP; rewrite -ltNge lebesgue_measure_ball// lte_fin. - rewrite -(@natr1 _ `| _ |%N) natr_absz ger0_norm; last first. - by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _)). - by rewrite -ltr_pdivrMr// -ltrBlDr (lt_le_trans _ (ceil_ge _))// ltrBlDr ltrDl. + rewrite -[M%:R]natr1 natr_absz ger0_norm; last first. + by rewrite -(ceil0 R) ceil_le. + by rewrite -ltr_pdivrMr// intrD1 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 [/cvgryPge|/cvgnyPge] Foo. by apply/cvgnyPge => A; near do rewrite -(@ler_nat R); apply: Foo. apply/cvgryPgey; near=> A; near=> n. -rewrite (le_trans (@ceil_ge R A))// (ler_int _ _ (f n)) [ceil _]intEsign. +rewrite pmulrn ceil_le_int// [ceil _]intEsign. by rewrite le_gtF ?expr0 ?mul1r ?lez_nat -?ceil_ge0//; near: n; apply: Foo. Unshelve. all: by end_near. Qed. diff --git a/theories/realfun.v b/theories/realfun.v index 5028c4d1b..6a741f1a3 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -246,13 +246,11 @@ have y_p : y_ n @[n --> \oo] --> p. apply/cvgrPdist_lt => e e0; near=> t. rewrite ltr0_norm// ?subr_lt0// opprB. rewrite /y_ /sval/=; case: cid2 => //= x /andP[_ + _]. - rewrite ltrBlDr => /lt_le_trans; apply. - rewrite addrC lerD2r -(invrK e) lef_pV2// ?posrE ?invr_gt0//. + rewrite -ltrBlDl => /lt_le_trans; apply. + rewrite -(invrK e) lef_pV2// ?posrE ?invr_gt0//. near: t. - exists `|ceil e^-1|%N => // k /= ek. - rewrite (le_trans (ceil_ge _))// (@le_trans _ _ `|ceil e^-1|%:~R)//. - by rewrite ger0_norm -?ceil_ge0// (lt_le_trans (ltrN10 _))// invr_ge0// ltW. - by move: ek;rewrite -(leq_add2r 1) !addn1 -(ltr_nat R) => /ltW. + exists `|ceil e^-1|%N => // k /=; rewrite pmulrn ceil_ge_int// -lez_nat abszE. + by move=> /(le_trans (ler_norm _)) /le_trans; apply; rewrite lez_nat leqnSn. have /fine_cvgP[[m _ mfy_] /= _] := h _ (conj py_ y_p). near \oo => n. have mn : (m <= n)%N by near: n; exists m.