Skip to content

Commit 60c7f9c

Browse files
affeldt-aistaffeldt-aist
committed
cleaning in ereal.v
1 parent c6e00dd commit 60c7f9c

2 files changed

Lines changed: 41 additions & 62 deletions

File tree

‎theories/derive.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -325,7 +325,7 @@ rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD.
325325
rewrite -(scale1r (_ _ v)); apply: cvgZl => /= X [e e0].
326326
rewrite /ball_ /= => eX.
327327
apply/nbhs_ballP.
328-
by exists e => //= x _ x0; apply eX; rewrite mulVr // ?unitfE //= subrr normr0.
328+
by exists e => //= x _ x0; apply eX; rewrite mulVf//= subrr normr0.
329329
rewrite /g2.
330330
have [->|v0] := eqVneq v 0.
331331
rewrite (_ : (fun _ => _) = cst 0); first exact: cvg_cst.
@@ -340,7 +340,7 @@ rewrite ltr_pdivlMr ?normr_gt0 // => jvi j0.
340340
rewrite add0r normrN normrZ -ltr_pdivlMl ?normr_gt0 ?invr_neq0 //.
341341
have /Hi/le_lt_trans -> // : ball 0 i (j *: v).
342342
by rewrite -ball_normE/= add0r normrN (le_lt_trans _ jvi) // normrZ.
343-
rewrite -(mulrC e) -mulrA -ltr_pdivlMl // mulrA mulVr ?unitfE ?gt_eqF //.
343+
rewrite -(mulrC e) -mulrA -ltr_pdivlMl // mulrA mulVf ?gt_eqF//.
344344
rewrite normrV ?unitfE // div1r invrK ltr_pdivrMl; last first.
345345
by rewrite pmulr_rgt0 // normr_gt0.
346346
rewrite normrZ mulrC -mulrA.

‎theories/ereal.v‎

Lines changed: 39 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -399,7 +399,7 @@ have sSoo : supremums S +oo.
399399
by move=> /= y /(_ _ Spoo); rewrite leye_eq => /eqP ->.
400400
case: xgetP.
401401
by move=> _ -> sSxget; move: (is_subset1_supremums sSoo sSxget).
402-
by move/(_ +oo) => gSoo; exfalso; exact: gSoo.
402+
by move=> /(_ +oo); exact: contra_notP.
403403
Qed.
404404

405405
Definition ereal_sup S := supremum -oo S.
@@ -1175,15 +1175,13 @@ Qed.
11751175
Lemma ball_ereal_ball_fin_lt r r' (e : {posnum R}) :
11761176
let e' := (r - fine (expand (contract r%:E - e%:num)))%R in
11771177
ball r e' r' -> (r' < r)%R ->
1178-
(`|contract r%:E - (e)%:num| < 1)%R ->
1178+
(`|contract r%:E - e%:num| < 1)%R ->
11791179
ereal_ball r%:E e%:num r'%:E.
11801180
Proof.
11811181
move=> e' re'r' rr' X; rewrite /ereal_ball.
11821182
rewrite gtr0_norm ?subr_gt0// ?lt_contract ?lte_fin//.
1183-
move: re'r'.
1184-
rewrite /ball /= gtr0_norm // ?subr_gt0// /e'.
1185-
rewrite -ltrBlDl addrAC subrr add0r ltrNl opprK -lte_fin.
1186-
rewrite fine_expand // lt_expandLR ?inE ?ltW//.
1183+
move: re'r'; rewrite /ball /= gtr0_norm ?subr_gt0// /e'.
1184+
rewrite ltrD2l ltrN2 -lte_fin fine_expand// lt_expandLR ?inE ?ltW//.
11871185
by rewrite ltrBlDl addrC -ltrBlDl.
11881186
Qed.
11891187

@@ -1318,12 +1316,12 @@ Lemma nbhs_fin_inbound r (e : {posnum R}) (A : set (\bar R)) :
13181316
ereal_ball r%:E e%:num `<=` A -> nbhs r%:E A.
13191317
Proof.
13201318
move=> reA.
1321-
have [|reN1] := boolP (contract r%:E - e%:num == -1)%R.
1319+
have [/eqP|reN1] := eqVneq (contract r%:E - e%:num)%R (-1)%R.
13221320
rewrite subr_eq addrC => /eqP reN1.
1323-
have [re1|] := boolP (contract r%:E + e%:num == 1)%R.
1324-
move/eqP : reN1; rewrite -(eqP re1) opprD addrCA subrr addr0 -subr_eq0.
1325-
rewrite opprK -mulr2n mulrn_eq0 orFb contract_eq0 => /eqP[r0].
1326-
move: re1; rewrite r0 contract0 add0r => /eqP e1.
1321+
have [re1|] := eqVneq (contract r%:E + e%:num)%R 1%R.
1322+
move/eqP : reN1; rewrite -re1 opprD addrC subrK -subr_eq0 opprK.
1323+
rewrite -mulr2n mulrn_eq0 orFb contract_eq0 => /eqP[r0].
1324+
move: re1; rewrite r0 contract0 add0r => e1.
13271325
apply/nbhs_ballP; exists 1%R => //= r'; rewrite /ball /= sub0r normrN => r'1.
13281326
apply: reA.
13291327
by rewrite /ereal_ball r0 contract0 sub0r normrN e1 contract_lt1.
@@ -1338,10 +1336,9 @@ have [|reN1] := boolP (contract r%:E - e%:num == -1)%R.
13381336
have [rr'|r'r] := lerP (contract r%:E) (contract r'%:E).
13391337
apply: contract_ereal_ball_fin_le; last exact/ltW.
13401338
by rewrite -lee_fin -(contractK r%:E) -(contractK r'%:E) le_expand.
1341-
apply: contract_ereal_ball_fin_lt; last first.
1342-
by rewrite reN1 addrAC subrr add0r.
1339+
apply: contract_ereal_ball_fin_lt; last by rewrite reN1 lerBlDl.
13431340
rewrite -lte_fin -(contractK r%:E) -(contractK r'%:E).
1344-
by rewrite lt_expand // inE; exact: contract_le1.
1341+
by rewrite lt_expand // inE contract_le1.
13451342
exact: contract_ereal_ball_pinfty.
13461343
have : nbhs r%:E (setT `\ -oo) by apply/nbhs_ballP; exists 1%R => /=.
13471344
move=> /nbhs_ballP[_/posnumP[e']] /=; rewrite /ball /= => h.
@@ -1351,9 +1348,9 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
13511348
by apply: (@nbhs_fin_out_above _ e) => //; rewrite re1.
13521349
move: re1; rewrite neq_lt => /orP[re1|re1].
13531350
have ? : (`|contract r%:E - e%:num| < 1)%R.
1354-
rewrite ltr_norml reN1 andTb ltrBlDl.
1351+
rewrite ltr_norml reN1/= -/(contract _%:E) ltrBlDl.
13551352
rewrite (@lt_le_trans _ _ 1%R) // ?lerDr//.
1356-
by case/ltr_normlP : (contract_lt1 r).
1353+
by rewrite (le_lt_trans (ler_norm _))// contract_lt1.
13571354
have ? : (`|contract r%:E + e%:num| < 1)%R.
13581355
rewrite ltr_norml re1 andbT -(addr0 (-1)) ler_ltD //.
13591356
by move: (contract_le1 r%:E); rewrite ler_norml => /andP[].
@@ -1372,10 +1369,9 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
13721369
move=> rr'; apply: ball_ereal_ball_fin_le => //.
13731370
by apply: le_ball re'r'; rewrite ge_min lexx orbT.
13741371
move: re'r'; rewrite /ball /= lt_min => /andP[].
1375-
rewrite gtr0_norm ?subr_gt0 // -ltrBlDl addrAC subrr add0r ltrNl.
1376-
rewrite opprK -lte_fin fine_expand // => r'e'r _.
1372+
rewrite gtr0_norm ?subr_gt0// ltrD2l ltrN2 -lte_fin fine_expand// => re'r _.
13771373
exact: expand_ereal_ball_fin_lt.
1378-
by apply :(@nbhs_fin_out_above _ e) => //; rewrite ltW.
1374+
by apply: (@nbhs_fin_out_above _ e) => //; rewrite ltW.
13791375
have [re1|re1] := ltrP 1 (contract r%:E + e%:num).
13801376
exact: (@nbhs_fin_out_above_below _ e).
13811377
move: re1; rewrite le_eqVlt => /orP[re1|re1].
@@ -1428,11 +1424,10 @@ rewrite predeq2E => x A; split.
14281424
have : (contract (r%:E - e%:num%:E) < contract r'%:E)%R.
14291425
move: re'r'; rewrite /e' lt_min => /andP[+ _].
14301426
rewrite /e' ltrBrDl addrC -ltrBrDl => /lt_le_trans.
1431-
by apply; rewrite opprB addrCA subrr addr0.
1427+
by apply; rewrite opprB addrC subrK.
14321428
rewrite -lt_expandRL ?inE ?contract_le1 // !contractK lte_fin.
14331429
rewrite ltrBlDr addrC -ltrBlDr => ->; rewrite andbT.
1434-
rewrite (@lt_le_trans _ _ 0%R)// 1?ltrNl 1?oppr0// subr_ge0.
1435-
by rewrite -lee_fin -le_contract.
1430+
by rewrite (@lt_le_trans _ _ 0%R)// subr_ge0 -lee_fin -le_contract.
14361431
apply: reA; rewrite /ball /= ltr_norml//.
14371432
rewrite ltr0_norm ?subr_lt0// opprB in re'r'.
14381433
apply/andP; split; last first.
@@ -1449,26 +1444,20 @@ rewrite predeq2E => x A; split.
14491444
have [cr0|cr0] := lerP 0 (contract r%:E).
14501445
move: re'2; rewrite ler0_norm; last first.
14511446
by rewrite subr_le0; case/ler_normlP : (contract_le1 r%:E).
1452-
rewrite opprB ltrBrDl addrCA subrr addr0 => h.
1453-
exfalso.
1454-
move: h; apply/negP; rewrite -leNgt.
1455-
by case/ler_normlP : (contract_le1 (r%:E + e%:num%:E)).
1447+
rewrite opprB ltrBrDl addrC subrK ltNge; apply: contraNP => _.
1448+
by rewrite (le_trans (ler_norm _))// contract_le1.
14561449
move: re'2; rewrite ler0_norm; last first.
14571450
by rewrite subr_le0; case/ler_normlP : (contract_le1 r%:E).
1458-
rewrite opprB ltrBrDl addrCA subrr addr0 => h.
1459-
exfalso.
1460-
move: h; apply/negP; rewrite -leNgt.
1461-
by case/ler_normlP : (contract_le1 (r%:E + e%:num%:E)).
1451+
rewrite opprB ltrBrDl addrC subrK ltNge; apply: contraNP => _.
1452+
by rewrite (le_trans (ler_norm _))// contract_le1.
14621453
* move=> /xsectionP/=; rewrite /ereal_ball [contract -oo]/= opprK.
14631454
rewrite lt_min => /andP[re'1 _].
14641455
move: re'1.
14651456
rewrite ger0_norm; last first.
14661457
rewrite addrC -lerBlDl add0r.
14671458
by move: (contract_le1 r%:E); rewrite ler_norml => /andP[].
1468-
rewrite ltrD2l => h.
1469-
exfalso.
1470-
move: h; apply/negP; rewrite -leNgt -lerNl.
1471-
by move: (contract_le1 (r%:E - e%:num%:E)); rewrite ler_norml => /andP[].
1459+
rewrite ltrD2l ltNge; apply: contraNP => _.
1460+
by rewrite lerNl lerNnormlW// contract_le1.
14721461
+ exists (diag (1 - contract M%:E))%R; rewrite /diag.
14731462
exists (1 - contract M%:E)%R => //=.
14741463
by rewrite subr_gt0 (le_lt_trans _ (contract_lt1 M)) // ler_norm.
@@ -1480,41 +1469,31 @@ rewrite predeq2E => x A; split.
14801469
rewrite ltrBlDr addrC addrCA addrC -ltrBlDr subrr subr_gt0 in rM1.
14811470
by rewrite -lte_fin -lt_contract.
14821471
* by rewrite /ereal_ball /= subrr normr0 => h; exact: MA.
1483-
* rewrite /ereal_ball /= opprK => h {MA}.
1484-
exfalso.
1485-
move: h; apply/negP.
1486-
rewrite -leNgt [in leRHS]ger0_norm // lerBlDr.
1487-
rewrite -/(contract M%:E) addrC -lerBlDr opprD addrA subrr sub0r.
1488-
by move: (contract_le1 M%:E); rewrite ler_norml => /andP[].
1472+
* rewrite /ereal_ball /= opprK ltNge; apply: contraNP => _.
1473+
rewrite [in leRHS]ger0_norm // lerD2l.
1474+
by rewrite -/(contract M%:E) lerNl lerNnormlW// contract_le1.
14891475
+ exists (diag (1 + contract M%:E)%R); rewrite /diag.
14901476
exists (1 + contract M%:E)%R => //=.
1491-
rewrite -ltrBlDl sub0r.
1492-
by move: (contract_lt1 M); rewrite ltr_norml => /andP[].
1477+
by rewrite -/(contract M%:E) -ltrBlDl sub0r ltrNnormlW// contract_lt1.
14931478
case=> [r| |] /xsectionP/=.
14941479
* rewrite /ereal_ball => /= rM1.
14951480
apply: MA; rewrite lte_fin.
14961481
rewrite ler0_norm in rM1; last first.
1497-
rewrite lerBlDl addr0 ltW //.
1498-
by move: (contract_lt1 r); rewrite ltr_norml => /andP[].
1499-
rewrite opprB opprK -ltrBlDl addrK in rM1.
1500-
by rewrite -lte_fin -lt_contract.
1501-
* rewrite /ereal_ball /= -opprD normrN => h {MA}.
1502-
exfalso.
1503-
move: h; apply/negP.
1504-
rewrite -leNgt [in leRHS]ger0_norm// -lerBlDr addrAC.
1505-
rewrite subrr add0r -/(contract M%:E).
1506-
by rewrite (le_trans _ (ltW (contract_lt1 M))) // ler_norm.
1507-
* rewrite /ereal_ball /= => _; exact: MA.
1482+
by rewrite subr_le0 -/(contract r%:E) lerNnormlW// contract_le1.
1483+
move: rM1; rewrite opprB opprK -ltrBlDl addrK.
1484+
by rewrite -!/(contract _%:E) lt_contract lte_fin.
1485+
* rewrite /ereal_ball/= -opprD normrN ger0_norm// ltrD2l.
1486+
by rewrite -/(contract M%:E) ltNge (le_trans (ler_norm _))// contract_le1.
1487+
* by rewrite /ereal_ball /= => _; exact: MA.
15081488
- case: x => [r [E [_/posnumP[e] reA] sEA] | [E [_/posnumP[e] reA] sEA] |
15091489
[E [_/posnumP[e] reA] sEA]] //=.
15101490
+ by apply: (@nbhs_fin_inbound _ e) => ? ?; exact/sEA/xsectionP/reA.
1511-
+ have [|] := boolP (e%:num <= 1)%R.
1512-
by move/nbhs_oo_up_e1; apply => ? ?; exact/sEA/xsectionP/reA.
1513-
by rewrite -ltNge => /nbhs_oo_up_1e; apply => ? ?; exact/sEA/xsectionP/reA.
1514-
+ have [|] := boolP (e%:num <= 1)%R.
1515-
move/nbhs_oo_down_e1; apply => ? ?; apply: sEA.
1516-
by rewrite /xsection/= inE; exact: reA.
1517-
by rewrite -ltNge =>/nbhs_oo_down_1e; apply => ? ?; exact/sEA/xsectionP/reA.
1491+
+ have [|] := lerP e%:num 1%R.
1492+
* by move/nbhs_oo_up_e1; apply => x ex; exact/sEA/xsectionP/reA.
1493+
* by move/nbhs_oo_up_1e; apply => x ex; exact/sEA/xsectionP/reA.
1494+
+ have [|] := lerP e%:num 1%R.
1495+
* by move/nbhs_oo_down_e1; apply => x ex; exact/sEA/xsectionP/reA.
1496+
* by move/nbhs_oo_down_1e; apply => x ex; exact/sEA/xsectionP/reA.
15181497
Qed.
15191498

15201499
HB.instance Definition _ := Nbhs_isPseudoMetric.Build R (\bar R)

0 commit comments

Comments
 (0)