diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 8 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 64 |
2 files changed, 59 insertions, 13 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4de3f44..6e86ad6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,9 +10,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Added -- lemmas `ltr_dist_addl`, `ler_dist_addl`, `ltr_distr_addl`, - `ler_distr_addl`, `ltr_dist_subl`, `ler_dist_subl`, - `ltr_distr_subr`, `ler_distr_subr`, `norm_lt_eqF` in `ssrnum` +- in `ssrnum.v`, new lemmas: + + `gt_norm_eqF` + + `{real_,}gtr_norm`, `{real_,}gtrNnorm`, `{real_,}ger_norm`, `{real_,}gerNnorm` + + `{real_,}ltr_dist_addl`, `{real_,}ler_dist_addl`, `{real_,}ltr_distr_addl`, `{real_,}ler_distr_addl`, + `{real_,}ltr_dist_subl`, `{real_,}ler_dist_subl`, `{real_,}ltr_distr_subr`, `{real_,}ler_distr_subr` ### Changed diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 5047868..361394a 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -2894,7 +2894,19 @@ rewrite real_ltNge ?real_ler_norml // negb_and -?real_ltNge ?realN //. by rewrite orbC ltr_oppr. Qed. -Definition real_lter_normr := (real_ler_normr, real_ltr_normr). +Definition real_lter_normr := (real_ler_normr, real_ltr_normr). + +Lemma real_gtr_norm x y : x \is real -> `|x| < y -> x < y. +Proof. by move=> ?; case/real_ltr_normlP. Qed. + +Lemma real_gtrNnorm x y : x \is real -> `|x| < y -> - y < x. +Proof. by move=> ?; case/real_ltr_normlP => //; rewrite ltr_oppl. Qed. + +Lemma real_ger_norm x y : x \is real -> `|x| <= y -> x <= y. +Proof. by move=> ?; case/real_ler_normlP. Qed. + +Lemma real_gerNnorm x y : x \is real -> `|x| <= y -> - y <= x. +Proof. by move=> ?; case/real_ler_normlP => //; rewrite ler_oppl. Qed. Lemma real_ler_distl x y e : x - y \is real -> (`|x - y| <= e) = (y - e <= x <= y + e). @@ -2906,6 +2918,30 @@ Proof. by move=> Rxy; rewrite real_lter_norml // !lter_sub_addl. Qed. Definition real_lter_distl := (real_ler_distl, real_ltr_distl). +Lemma real_ltr_dist_addl x y e : x - y \is real -> `|x - y| < e -> x < y + e. +Proof. by move=> ?; rewrite real_ltr_distl // => /andP[]. Qed. + +Lemma real_ler_dist_addl x y e : x - y \is real -> `|x - y| <= e -> x <= y + e. +Proof. by move=> ?; rewrite real_ler_distl // => /andP[]. Qed. + +Lemma real_ltr_distr_addl x y e : x - y \is real -> `|x - y| < e -> y < x + e. +Proof. by rewrite realBC (distrC x) => ? /real_ltr_dist_addl; apply. Qed. + +Lemma real_ler_distr_addl x y e : x - y \is real -> `|x - y| <= e -> y <= x + e. +Proof. by rewrite realBC distrC => ? /real_ler_dist_addl; apply. Qed. + +Lemma real_ltr_dist_subl x y e : x - y \is real -> `|x - y| < e -> x - e < y. +Proof. by move/real_ltr_dist_addl; rewrite ltr_sub_addr; apply. Qed. + +Lemma real_ler_dist_subl x y e : x - y \is real -> `|x - y| <= e -> x - e <= y. +Proof. by move/real_ler_dist_addl; rewrite ler_sub_addr; apply. Qed. + +Lemma real_ltr_distr_subr x y e : x - y \is real -> `|x - y| < e -> y - e < x. +Proof. by rewrite realBC distrC => ? /real_ltr_dist_subl; apply. Qed. + +Lemma real_ler_distr_subr x y e : x - y \is real -> `|x - y| <= e -> y - e <= x. +Proof. by rewrite realBC distrC => ? /real_ler_dist_subl; apply. Qed. + (* GG: pointless duplication }-( *) Lemma eqr_norm_id x : (`|x| == x) = (0 <= x). Proof. by rewrite ger0_def. Qed. Lemma eqr_normN x : (`|x| == - x) = (x <= 0). Proof. by rewrite ler0_def. Qed. @@ -3738,6 +3774,14 @@ Lemma ltr_normlP x y : reflect ((-x < y) * (x < y)) (`|x| < y). Proof. exact: real_ltr_normlP. Qed. Arguments ltr_normlP {x y}. +Lemma gtr_norm x y : `|x| < y -> x < y. Proof. exact: real_gtr_norm. Qed. + +Lemma gtrNnorm x y : `|x| < y -> - y < x. Proof. exact: real_gtrNnorm. Qed. + +Lemma ger_norm x y : `|x| <= y -> x <= y. Proof. exact: real_ger_norm. Qed. + +Lemma gerNnorm x y : `|x| <= y -> - y <= x. Proof. exact: real_gerNnorm. Qed. + Lemma ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y). Proof. by rewrite leNgt ltr_norml negb_and -!leNgt orbC ler_oppr. Qed. @@ -3755,30 +3799,30 @@ Proof. by rewrite lter_norml !lter_sub_addl. Qed. Definition lter_distl := (ler_distl, ltr_distl). Lemma ltr_dist_addl x y e : `|x - y| < e -> x < y + e. -Proof. by rewrite ltr_distl => /andP[]. Qed. +Proof. exact: real_ltr_dist_addl. Qed. Lemma ler_dist_addl x y e : `|x - y| <= e -> x <= y + e. -Proof. by rewrite ler_distl => /andP[]. Qed. +Proof. exact: real_ler_dist_addl. Qed. Lemma ltr_distr_addl x y e : `|x - y| < e -> y < x + e. -Proof. by rewrite distrC => /ltr_dist_addl. Qed. +Proof. exact: real_ltr_distr_addl. Qed. Lemma ler_distr_addl x y e : `|x - y| <= e -> y <= x + e. -Proof. by rewrite distrC => /ler_dist_addl. Qed. +Proof. exact: real_ler_distr_addl. Qed. Lemma ltr_dist_subl x y e : `|x - y| < e -> x - e < y. -Proof. by move/ltr_dist_addl; rewrite -ltr_subl_addr. Qed. +Proof. exact: real_ltr_dist_subl. Qed. Lemma ler_dist_subl x y e : `|x - y| <= e -> x - e <= y. -Proof. by move/ler_dist_addl; rewrite -ler_subl_addr. Qed. +Proof. exact: real_ler_dist_subl. Qed. Lemma ltr_distr_subr x y e : `|x - y| < e -> y - e < x. -Proof. by rewrite distrC => /ltr_dist_subl. Qed. +Proof. exact: real_ltr_distr_subr. Qed. Lemma ler_distr_subr x y e : `|x - y| <= e -> y - e <= x. -Proof. by rewrite distrC => /ler_dist_subl. Qed. +Proof. exact: real_ler_distr_subr. Qed. -Lemma norm_lt_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false). +Lemma gt_norm_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false). Proof. move=> x1; split; last by rewrite lt_eqF // (le_lt_trans (ler_norm _) x1). by move: x1; rewrite ltr_norml => /andP[? ?]; rewrite gt_eqF. |