Skip to content

Cleanup #1567

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

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Cleanup #1567

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
c6e00dd
Cleanup
pi8027 Apr 11, 2025
60c7f9c
cleaning in ereal.v
affeldt-aist May 19, 2025
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
2 changes: 1 addition & 1 deletion classical/unstable.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ Proof.
apply: canRL (mulfK _) _ => //; rewrite ?pnatr_eq0//.
case: lerP => _; (* TODO: ring *) rewrite [2%:R]mulr2n mulrDr mulr1.
by rewrite addrCA addrK.
by rewrite addrCA addrAC subrr add0r.
by rewrite addrC subrKA.
Qed.

Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2%:R.
Expand Down
4 changes: 2 additions & 2 deletions experimental_reals/distr.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -335,7 +335,7 @@ Definition mflip (xt : R) :=
Lemma isd_mflip xt : isdistr (mflip xt).
Proof. apply/isdistr_finP; split=> [b|].
+ by case: b; rewrite ?subr_ge0 cp01_clamp.
+ by rewrite /index_enum !unlock /= addr0 addrCA subrr addr0.
+ by rewrite /index_enum !unlock /= addr0 addrC subrK.
Qed.

Definition dflip (xt : R) := locked (mkdistr (isd_mflip xt)).
Expand Down Expand Up @@ -1133,7 +1133,7 @@ Qed.

Lemma pr_and A B mu : \P_[mu] [predI A & B] =
\P_[mu] A + \P_[mu] B - \P_[mu] [predU A & B].
Proof. by rewrite pr_or opprB addrCA subrr addr0. Qed.
Proof. by rewrite pr_or subKr. Qed.

Lemma ler_pr_or A B mu :
\P_[mu] [predU A & B] <= \P_[mu] A + \P_[mu] B.
Expand Down
9 changes: 4 additions & 5 deletions experimental_reals/realseq.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,7 @@ have gt0_e: 0 < e by rewrite subr_gt0.
move=> x y; rewrite !inE/= /eclamp pmulr_rle0 // invr_le0.
rewrite lern0 /= !ltr_distl => /andP[_ lt1] /andP[lt2 _].
apply/(lt_trans lt1)/(le_lt_trans _ lt2).
by rewrite lerBrDl addrCA -splitr /e addrCA subrr addr0.
by rewrite lerBrDl addrCA -splitr /e addrC subrK.
Qed.

Lemma separable {R : realType} (l1 l2 : \bar R) :
Expand Down Expand Up @@ -303,9 +303,8 @@ Lemma ncvgM u v lu lv : ncvg u lu%:E -> ncvg v lv%:E ->
Proof.
move=> cu cv; pose a := u \- lu%:S; pose b := v \- lv%:S.
have eq: (u \* v) =1 (lu * lv)%:S \+ ((lu%:S \* b) \+ (a \* v)).
move=> n; rewrite {}/a {}/b /= [u n+_]addrC [(_+_)*(v n)]mulrDl.
rewrite !addrA -[LHS]add0r; congr (_ + _); rewrite mulrDr.
by rewrite !(mulrN, mulNr) (addrCA (lu * lv)) subrr addr0 subrr.
move=> n; rewrite {}/a {}/b /=.
by rewrite addrC mulrBr addrAC subrK addrC mulrBl subrK.
apply/(ncvg_eq eq); rewrite -[X in X%:E]addr0; apply/ncvgD.
by apply/ncvgC. rewrite -[X in X%:E]addr0; apply/ncvgD.
+ apply/ncvgMr; first rewrite -[X in X%:E](subrr lv).
Expand Down Expand Up @@ -388,7 +387,7 @@ case: l1 l2 => [l1||] [l2||] //=; first last.
move=> lt_12; pose e := l2 - l1 => /(_ (B l2 e)).
case=> K cv; exists K => n /cv; rewrite !inE eclamp_id ?subr_gt0 //.
rewrite ltr_distl => /andP[] /(le_lt_trans _) h _; apply: h.
by rewrite {cv}/e opprB addrCA subrr addr0.
by rewrite {cv}/e subKr.
Qed.

Lemma ncvg_lt (u : nat -> R) (l1 l2 : \bar R) :
Expand Down
3 changes: 1 addition & 2 deletions experimental_reals/realsum.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -465,8 +465,7 @@ apply/eqP; case: (x =P _) => // /eqP /lt_total /orP[]; last first.
move=> lt_xS; pose e := psum S - x.
have ge0_e: 0 < e by rewrite subr_gt0.
case: (sup_adherent ge0_e (summable_sup smS)) => y.
case=> /= J ->; rewrite /e /psum (asboolT smS).
rewrite opprB addrCA subrr addr0 => lt_xSJ.
case=> /= J ->; rewrite /e /psum (asboolT smS) subKr => lt_xSJ.
pose k := \max_(j : J) (val j); have lt_x_uSk: x < u k.+1.
apply/(lt_le_trans lt_xSJ); rewrite /u big_ord_mkfset.
rewrite (eq_bigr (S \o val)) => /= [j _|]; first by rewrite ger0_norm.
Expand Down
6 changes: 2 additions & 4 deletions reals/reals.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -281,8 +281,7 @@ Qed.
Lemma sup_le_ub {E} x : E !=set0 -> (ubound E) x -> sup E <= x.
Proof.
move=> hasE leEx; set y := sup E; pose z := (x + y) / 2%:R.
have Dz: 2%:R * z = x + y.
by rewrite mulrCA divff ?mulr1 // pnatr_eq0.
have Dz: 2%:R * z = x + y by rewrite mulrC divfK// pnatr_eq0.
have ubE : has_sup E by split => //; exists x.
have [/downP [t Et lezt] | leyz] := sup_total z ubE.
rewrite -(lerD2l x) -Dz -mulr2n -[leRHS]mulr_natl.
Expand Down Expand Up @@ -334,8 +333,7 @@ have e2pos : 0 < eps / 2%:R by rewrite divr_gt0// ltr0n.
have [r Ar supBr] := sup_adherent e2pos supA.
have [s Bs supAs] := sup_adherent e2pos supB.
have := ltrD supBr supAs.
rewrite -addrA [-_+_]addrC -addrA -opprD -splitr addrA /= opprD opprK addrA.
rewrite subrr add0r; apply/negP; rewrite -leNgt.
rewrite -addrACA -opprD -splitr subKr; apply/negP; rewrite -leNgt.
by apply: sup_upper_bound => //; exists r => //; exists s.
Qed.

Expand Down
4 changes: 2 additions & 2 deletions theories/derive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -325,7 +325,7 @@ rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD.
rewrite -(scale1r (_ _ v)); apply: cvgZl => /= X [e e0].
rewrite /ball_ /= => eX.
apply/nbhs_ballP.
by exists e => //= x _ x0; apply eX; rewrite mulVr // ?unitfE //= subrr normr0.
by exists e => //= x _ x0; apply eX; rewrite mulVf//= subrr normr0.
rewrite /g2.
have [->|v0] := eqVneq v 0.
rewrite (_ : (fun _ => _) = cst 0); first exact: cvg_cst.
Expand All @@ -340,7 +340,7 @@ rewrite ltr_pdivlMr ?normr_gt0 // => jvi j0.
rewrite add0r normrN normrZ -ltr_pdivlMl ?normr_gt0 ?invr_neq0 //.
have /Hi/le_lt_trans -> // : ball 0 i (j *: v).
by rewrite -ball_normE/= add0r normrN (le_lt_trans _ jvi) // normrZ.
rewrite -(mulrC e) -mulrA -ltr_pdivlMl // mulrA mulVr ?unitfE ?gt_eqF //.
rewrite -(mulrC e) -mulrA -ltr_pdivlMl // mulrA mulVf ?gt_eqF//.
rewrite normrV ?unitfE // div1r invrK ltr_pdivrMl; last first.
by rewrite pmulr_rgt0 // normr_gt0.
rewrite normrZ mulrC -mulrA.
Expand Down
99 changes: 39 additions & 60 deletions theories/ereal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -399,7 +399,7 @@ have sSoo : supremums S +oo.
by move=> /= y /(_ _ Spoo); rewrite leye_eq => /eqP ->.
case: xgetP.
by move=> _ -> sSxget; move: (is_subset1_supremums sSoo sSxget).
by move/(_ +oo) => gSoo; exfalso; exact: gSoo.
by move=> /(_ +oo); exact: contra_notP.
Qed.

Definition ereal_sup S := supremum -oo S.
Expand Down Expand Up @@ -1175,15 +1175,13 @@ Qed.
Lemma ball_ereal_ball_fin_lt r r' (e : {posnum R}) :
let e' := (r - fine (expand (contract r%:E - e%:num)))%R in
ball r e' r' -> (r' < r)%R ->
(`|contract r%:E - (e)%:num| < 1)%R ->
(`|contract r%:E - e%:num| < 1)%R ->
ereal_ball r%:E e%:num r'%:E.
Proof.
move=> e' re'r' rr' X; rewrite /ereal_ball.
rewrite gtr0_norm ?subr_gt0// ?lt_contract ?lte_fin//.
move: re'r'.
rewrite /ball /= gtr0_norm // ?subr_gt0// /e'.
rewrite -ltrBlDl addrAC subrr add0r ltrNl opprK -lte_fin.
rewrite fine_expand // lt_expandLR ?inE ?ltW//.
move: re'r'; rewrite /ball /= gtr0_norm ?subr_gt0// /e'.
rewrite ltrD2l ltrN2 -lte_fin fine_expand// lt_expandLR ?inE ?ltW//.
by rewrite ltrBlDl addrC -ltrBlDl.
Qed.

Expand Down Expand Up @@ -1318,12 +1316,12 @@ Lemma nbhs_fin_inbound r (e : {posnum R}) (A : set (\bar R)) :
ereal_ball r%:E e%:num `<=` A -> nbhs r%:E A.
Proof.
move=> reA.
have [|reN1] := boolP (contract r%:E - e%:num == -1)%R.
have [/eqP|reN1] := eqVneq (contract r%:E - e%:num)%R (-1)%R.
rewrite subr_eq addrC => /eqP reN1.
have [re1|] := boolP (contract r%:E + e%:num == 1)%R.
move/eqP : reN1; rewrite -(eqP re1) opprD addrCA subrr addr0 -subr_eq0.
rewrite opprK -mulr2n mulrn_eq0 orFb contract_eq0 => /eqP[r0].
move: re1; rewrite r0 contract0 add0r => /eqP e1.
have [re1|] := eqVneq (contract r%:E + e%:num)%R 1%R.
move/eqP : reN1; rewrite -re1 opprD addrC subrK -subr_eq0 opprK.
rewrite -mulr2n mulrn_eq0 orFb contract_eq0 => /eqP[r0].
move: re1; rewrite r0 contract0 add0r => e1.
apply/nbhs_ballP; exists 1%R => //= r'; rewrite /ball /= sub0r normrN => r'1.
apply: reA.
by rewrite /ereal_ball r0 contract0 sub0r normrN e1 contract_lt1.
Expand All @@ -1338,10 +1336,9 @@ have [|reN1] := boolP (contract r%:E - e%:num == -1)%R.
have [rr'|r'r] := lerP (contract r%:E) (contract r'%:E).
apply: contract_ereal_ball_fin_le; last exact/ltW.
by rewrite -lee_fin -(contractK r%:E) -(contractK r'%:E) le_expand.
apply: contract_ereal_ball_fin_lt; last first.
by rewrite reN1 addrAC subrr add0r.
apply: contract_ereal_ball_fin_lt; last by rewrite reN1 lerBlDl.
rewrite -lte_fin -(contractK r%:E) -(contractK r'%:E).
by rewrite lt_expand // inE; exact: contract_le1.
by rewrite lt_expand // inE contract_le1.
exact: contract_ereal_ball_pinfty.
have : nbhs r%:E (setT `\ -oo) by apply/nbhs_ballP; exists 1%R => /=.
move=> /nbhs_ballP[_/posnumP[e']] /=; rewrite /ball /= => h.
Expand All @@ -1351,9 +1348,9 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
by apply: (@nbhs_fin_out_above _ e) => //; rewrite re1.
move: re1; rewrite neq_lt => /orP[re1|re1].
have ? : (`|contract r%:E - e%:num| < 1)%R.
rewrite ltr_norml reN1 andTb ltrBlDl.
rewrite ltr_norml reN1/= -/(contract _%:E) ltrBlDl.
rewrite (@lt_le_trans _ _ 1%R) // ?lerDr//.
by case/ltr_normlP : (contract_lt1 r).
by rewrite (le_lt_trans (ler_norm _))// contract_lt1.
have ? : (`|contract r%:E + e%:num| < 1)%R.
rewrite ltr_norml re1 andbT -(addr0 (-1)) ler_ltD //.
by move: (contract_le1 r%:E); rewrite ler_norml => /andP[].
Expand All @@ -1372,10 +1369,9 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
move=> rr'; apply: ball_ereal_ball_fin_le => //.
by apply: le_ball re'r'; rewrite ge_min lexx orbT.
move: re'r'; rewrite /ball /= lt_min => /andP[].
rewrite gtr0_norm ?subr_gt0 // -ltrBlDl addrAC subrr add0r ltrNl.
rewrite opprK -lte_fin fine_expand // => r'e'r _.
rewrite gtr0_norm ?subr_gt0// ltrD2l ltrN2 -lte_fin fine_expand// => re'r _.
exact: expand_ereal_ball_fin_lt.
by apply :(@nbhs_fin_out_above _ e) => //; rewrite ltW.
by apply: (@nbhs_fin_out_above _ e) => //; rewrite ltW.
have [re1|re1] := ltrP 1 (contract r%:E + e%:num).
exact: (@nbhs_fin_out_above_below _ e).
move: re1; rewrite le_eqVlt => /orP[re1|re1].
Expand Down Expand Up @@ -1428,11 +1424,10 @@ rewrite predeq2E => x A; split.
have : (contract (r%:E - e%:num%:E) < contract r'%:E)%R.
move: re'r'; rewrite /e' lt_min => /andP[+ _].
rewrite /e' ltrBrDl addrC -ltrBrDl => /lt_le_trans.
by apply; rewrite opprB addrCA subrr addr0.
by apply; rewrite opprB addrC subrK.
rewrite -lt_expandRL ?inE ?contract_le1 // !contractK lte_fin.
rewrite ltrBlDr addrC -ltrBlDr => ->; rewrite andbT.
rewrite (@lt_le_trans _ _ 0%R)// 1?ltrNl 1?oppr0// subr_ge0.
by rewrite -lee_fin -le_contract.
by rewrite (@lt_le_trans _ _ 0%R)// subr_ge0 -lee_fin -le_contract.
apply: reA; rewrite /ball /= ltr_norml//.
rewrite ltr0_norm ?subr_lt0// opprB in re'r'.
apply/andP; split; last first.
Expand All @@ -1449,26 +1444,20 @@ rewrite predeq2E => x A; split.
have [cr0|cr0] := lerP 0 (contract r%:E).
move: re'2; rewrite ler0_norm; last first.
by rewrite subr_le0; case/ler_normlP : (contract_le1 r%:E).
rewrite opprB ltrBrDl addrCA subrr addr0 => h.
exfalso.
move: h; apply/negP; rewrite -leNgt.
by case/ler_normlP : (contract_le1 (r%:E + e%:num%:E)).
rewrite opprB ltrBrDl addrC subrK ltNge; apply: contraNP => _.
by rewrite (le_trans (ler_norm _))// contract_le1.
move: re'2; rewrite ler0_norm; last first.
by rewrite subr_le0; case/ler_normlP : (contract_le1 r%:E).
rewrite opprB ltrBrDl addrCA subrr addr0 => h.
exfalso.
move: h; apply/negP; rewrite -leNgt.
by case/ler_normlP : (contract_le1 (r%:E + e%:num%:E)).
rewrite opprB ltrBrDl addrC subrK ltNge; apply: contraNP => _.
by rewrite (le_trans (ler_norm _))// contract_le1.
* move=> /xsectionP/=; rewrite /ereal_ball [contract -oo]/= opprK.
rewrite lt_min => /andP[re'1 _].
move: re'1.
rewrite ger0_norm; last first.
rewrite addrC -lerBlDl add0r.
by move: (contract_le1 r%:E); rewrite ler_norml => /andP[].
rewrite ltrD2l => h.
exfalso.
move: h; apply/negP; rewrite -leNgt -lerNl.
by move: (contract_le1 (r%:E - e%:num%:E)); rewrite ler_norml => /andP[].
rewrite ltrD2l ltNge; apply: contraNP => _.
by rewrite lerNl lerNnormlW// contract_le1.
+ exists (diag (1 - contract M%:E))%R; rewrite /diag.
exists (1 - contract M%:E)%R => //=.
by rewrite subr_gt0 (le_lt_trans _ (contract_lt1 M)) // ler_norm.
Expand All @@ -1480,41 +1469,31 @@ rewrite predeq2E => x A; split.
rewrite ltrBlDr addrC addrCA addrC -ltrBlDr subrr subr_gt0 in rM1.
by rewrite -lte_fin -lt_contract.
* by rewrite /ereal_ball /= subrr normr0 => h; exact: MA.
* rewrite /ereal_ball /= opprK => h {MA}.
exfalso.
move: h; apply/negP.
rewrite -leNgt [in leRHS]ger0_norm // lerBlDr.
rewrite -/(contract M%:E) addrC -lerBlDr opprD addrA subrr sub0r.
by move: (contract_le1 M%:E); rewrite ler_norml => /andP[].
* rewrite /ereal_ball /= opprK ltNge; apply: contraNP => _.
rewrite [in leRHS]ger0_norm // lerD2l.
by rewrite -/(contract M%:E) lerNl lerNnormlW// contract_le1.
+ exists (diag (1 + contract M%:E)%R); rewrite /diag.
exists (1 + contract M%:E)%R => //=.
rewrite -ltrBlDl sub0r.
by move: (contract_lt1 M); rewrite ltr_norml => /andP[].
by rewrite -/(contract M%:E) -ltrBlDl sub0r ltrNnormlW// contract_lt1.
case=> [r| |] /xsectionP/=.
* rewrite /ereal_ball => /= rM1.
apply: MA; rewrite lte_fin.
rewrite ler0_norm in rM1; last first.
rewrite lerBlDl addr0 ltW //.
by move: (contract_lt1 r); rewrite ltr_norml => /andP[].
rewrite opprB opprK -ltrBlDl addrK in rM1.
by rewrite -lte_fin -lt_contract.
* rewrite /ereal_ball /= -opprD normrN => h {MA}.
exfalso.
move: h; apply/negP.
rewrite -leNgt [in leRHS]ger0_norm// -lerBlDr addrAC.
rewrite subrr add0r -/(contract M%:E).
by rewrite (le_trans _ (ltW (contract_lt1 M))) // ler_norm.
* rewrite /ereal_ball /= => _; exact: MA.
by rewrite subr_le0 -/(contract r%:E) lerNnormlW// contract_le1.
move: rM1; rewrite opprB opprK -ltrBlDl addrK.
by rewrite -!/(contract _%:E) lt_contract lte_fin.
* rewrite /ereal_ball/= -opprD normrN ger0_norm// ltrD2l.
by rewrite -/(contract M%:E) ltNge (le_trans (ler_norm _))// contract_le1.
* by rewrite /ereal_ball /= => _; exact: MA.
- case: x => [r [E [_/posnumP[e] reA] sEA] | [E [_/posnumP[e] reA] sEA] |
[E [_/posnumP[e] reA] sEA]] //=.
+ by apply: (@nbhs_fin_inbound _ e) => ? ?; exact/sEA/xsectionP/reA.
+ have [|] := boolP (e%:num <= 1)%R.
by move/nbhs_oo_up_e1; apply => ? ?; exact/sEA/xsectionP/reA.
by rewrite -ltNge => /nbhs_oo_up_1e; apply => ? ?; exact/sEA/xsectionP/reA.
+ have [|] := boolP (e%:num <= 1)%R.
move/nbhs_oo_down_e1; apply => ? ?; apply: sEA.
by rewrite /xsection/= inE; exact: reA.
by rewrite -ltNge =>/nbhs_oo_down_1e; apply => ? ?; exact/sEA/xsectionP/reA.
+ have [|] := lerP e%:num 1%R.
* by move/nbhs_oo_up_e1; apply => x ex; exact/sEA/xsectionP/reA.
* by move/nbhs_oo_up_1e; apply => x ex; exact/sEA/xsectionP/reA.
+ have [|] := lerP e%:num 1%R.
* by move/nbhs_oo_down_e1; apply => x ex; exact/sEA/xsectionP/reA.
* by move/nbhs_oo_down_1e; apply => x ex; exact/sEA/xsectionP/reA.
Qed.

HB.instance Definition _ := Nbhs_isPseudoMetric.Build R (\bar R)
Expand Down
Loading