Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix some deprecation warnings about ceil_ge #1415

Merged
merged 2 commits into from
Dec 9, 2024
Merged

Fix some deprecation warnings about ceil_ge #1415

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d09325c
Fix some deprecation warnings about ceil_ge
pi8027 Nov 29, 2024
6d5e8c1
Update theories/lebesgue_integral.v
pi8027 Dec 8, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions reals/real_interval.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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) :
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
54 changes: 21 additions & 33 deletions theories/lebesgue_integral.v
View file
Open in desktop
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,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.
Expand All @@ -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) ->
Expand Down Expand Up @@ -2627,19 +2619,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 +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.
Expand Down Expand Up @@ -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.
Expand Down
28 changes: 12 additions & 16 deletions theories/lebesgue_measure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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 <oo) \esum_(i in F n) mu (closure (B i)) =
Expand Down
2 changes: 1 addition & 1 deletion theories/normedtype.v
View file
Open in desktop
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
10 changes: 4 additions & 6 deletions theories/realfun.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Loading