Skip to content

Commit

Permalink
Fix some deprecation warnings about ceil_ge
Browse files Browse the repository at this point in the history
  • Loading branch information
pi8027 committed Dec 4, 2024
1 parent 47e0e0f commit a86e8e5
Show file tree
Hide file tree
Showing 6 changed files with 29 additions and 40 deletions.
7 changes: 3 additions & 4 deletions reals/real_interval.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 -ceil_ge0 (lt_le_trans (ltrN10 R))// subr_ge0 (lteifW xy).
Qed.

Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) :
Expand All @@ -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.

Expand Down
4 changes: 2 additions & 2 deletions reals/reals.v
Original file line number Diff line number Diff line change
Expand Up @@ -116,9 +116,9 @@ End has_bound_lemmas.
(* -------------------------------------------------------------------- *)

HB.mixin Record ArchimedeanField_isReal R of Num.ArchiField R := {
sup_upper_bound_subdef : forall E : set [the archiFieldType of R],
sup_upper_bound_subdef : forall E : set R,
has_sup E -> ubound E (supremum 0 E) ;
sup_adherent_subdef : forall (E : set [the archiFieldType of R]) (eps : R),
sup_adherent_subdef : forall (E : set R) (eps : R),
0 < eps -> has_sup E -> exists2 e : R, E e & (supremum 0 E - eps) < e
}.

Expand Down
45 changes: 18 additions & 27 deletions theories/lebesgue_integral.v
Original file line number Diff line number Diff line change
Expand Up @@ -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 :
Expand Down Expand Up @@ -2350,22 +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// -ceil_ge0 (lt_le_trans (ltrN10 _))//.
by rewrite 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 _))//.
rewrite natr_absz ger0_norm ?ceil_ge// -ceil_ge0 (lt_le_trans (ltrN10 _))//.
by rewrite -mulrNN mulr_ge0// lerNr oppr0// ltW// invr_lt0.
- rewrite -fx0 mule0 /g -fx0.
under eq_fun do rewrite mule0/=. (*TODO: notation broken*)
Expand Down Expand Up @@ -2627,19 +2621,17 @@ 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.
have [muDoo|muDoo] := ltP (mu D) +oo; last first.
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.
Expand Down Expand Up @@ -3515,9 +3507,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.
Expand Down Expand Up @@ -3782,7 +3773,7 @@ move=> mf; split=> [iDf0|Df0].
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 lerD2r// le_ceil.
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.
Expand Down
4 changes: 2 additions & 2 deletions theories/lebesgue_measure.v
Original file line number Diff line number Diff line change
Expand Up @@ -718,7 +718,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.
Expand Down Expand Up @@ -2866,7 +2866,7 @@ have finite_set_F i : finite_set (F i).
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.
by rewrite -ltr_pdivrMr// -ltrBlDr (lt_le_trans _ (le_ceil _))// ltrBlDr ltrDl.
have mur2_fin_num_ : mu (ball (0:R) (r%:num + 2))%R < +oo.
by rewrite lebesgue_measure_ball// ltry.
have FE : \sum_(n <oo) \esum_(i in F n) mu (closure (B i)) =
Expand Down
2 changes: 1 addition & 1 deletion theories/normedtype.v
Original file line number Diff line number Diff line change
Expand Up @@ -642,7 +642,7 @@ Proof.
split=> [/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.

Expand Down
7 changes: 3 additions & 4 deletions theories/realfun.v
Original file line number Diff line number Diff line change
Expand Up @@ -249,10 +249,9 @@ have y_p : y_ n @[n --> \oo] --> p.
rewrite ltrBlDr => /lt_le_trans; apply.
rewrite addrC lerD2r -(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 -lez_nat abszE ger0_norm.
by rewrite -ceil_le_int//= => /le_trans; apply; rewrite ler_nat.
by rewrite -?ceil_ge0 (lt_le_trans (ltrN10 _))// invr_ge0// ltW.
have /fine_cvgP[[m _ mfy_] /= _] := h _ (conj py_ y_p).
near \oo => n.
have mn : (m <= n)%N by near: n; exists m.
Expand Down

0 comments on commit a86e8e5

Please sign in to comment.