From d3b6809c480c0c0f5a07131bd71f2d7f72d9e16d Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Wed, 30 Oct 2024 00:03:23 +0900 Subject: [PATCH 1/2] near_in_itv_oy/yo/yy --- CHANGELOG_UNRELEASED.md | 1 + theories/normedtype.v | 39 ++++++++++++++++++++++++++++++++++++++- 2 files changed, 39 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 03c90f7b0..3eac659c3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -56,6 +56,7 @@ `nbhs_one_point_compactification_weakE`, `locally_compact_completely_regular`, and `completely_regular_regular`. + + new lemmas `near_in_itvoy`, `near_in_itvyo`, `near_in_itvyy` ### Changed diff --git a/theories/normedtype.v b/theories/normedtype.v index debaf7d26..a780b3807 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5336,10 +5336,47 @@ Lemma bound_itvE (R : numDomainType) (a b : R) : (a \in `]-oo, a]). Proof. by rewrite !(boundr_in_itv, boundl_in_itv). Qed. -Lemma near_in_itv {R : realFieldType} (a b : R) : +Section near_in_itv. +Context {R : realFieldType} (a b : R). + +Lemma near_in_itv : {in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}. Proof. exact: interval_open. Qed. +Lemma near_in_itvoy : + {in `]a, +oo[, forall y, \forall z \near y, z \in `]a, +oo[}. +Proof. +move=> x ax. +near=> z. +suff : z \in `]a, +oo[%classic by rewrite inE. +near: z. +rewrite near_nbhs. +apply: (@open_in_nearW _ _ `]a, +oo[%classic) => //. +by rewrite inE/=. +Unshelve. end_near. Qed. + +Lemma near_in_itvyo : + {in `]-oo, b[, forall y, \forall z \near y, z \in `]-oo, b[}. +Proof. +move=> x xb. +near=> z. +suff : z \in `]-oo, b[%classic by rewrite inE. +near: z. +rewrite near_nbhs. +apply: (@open_in_nearW _ _ `]-oo, b[%classic) => //. +by rewrite inE/=. +Unshelve. end_near. Qed. + +Lemma near_in_itvyy : + {in `]-oo, +oo[, forall y : R, \forall z \near y, z \in `]-oo, +oo[}. +Proof. +move=> x _. +rewrite -near_nbhs. +exact: nearW => //. +Qed. + +End near_in_itv. + Lemma cvg_patch {R : realType} (f : R -> R^o) (a b : R) (x : R) : (a < b)%R -> x \in `]a, b[ -> f @ (x : subspace `[a, b]) --> f x -> From 30e4396418826755f7ff43cdc766a6929c1c2a0d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 13 Nov 2024 17:20:16 +0900 Subject: [PATCH 2/2] rm near_in_itvyy, deprecation, renaming --- CHANGELOG_UNRELEASED.md | 5 ++++- theories/ftc.v | 2 +- theories/normedtype.v | 21 ++++++++------------- theories/realfun.v | 4 ++-- theories/trigo.v | 12 ++++++------ 5 files changed, 21 insertions(+), 23 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3eac659c3..e1a3a66ea 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -56,7 +56,7 @@ `nbhs_one_point_compactification_weakE`, `locally_compact_completely_regular`, and `completely_regular_regular`. - + new lemmas `near_in_itvoy`, `near_in_itvyo`, `near_in_itvyy` + + new lemmas `near_in_itvoy`, `near_in_itvNyo` ### Changed @@ -77,6 +77,9 @@ ### Renamed +- in `normedtype.v`: + + `near_in_itv` -> `near_in_itvoo` + ### Generalized ### Deprecated diff --git a/theories/ftc.v b/theories/ftc.v index 4f553f2c1..7be07799d 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -979,7 +979,7 @@ rewrite (@integration_by_substitution_decreasing (- F)%R); first last. rewrite -derive1E. have /cvgN := cF' _ xab; apply: cvg_trans; apply: near_eq_cvg. rewrite near_simpl; near=> y; rewrite fctE !derive1E deriveN//. - by case: Fab => + _ _; apply; near: y; exact: near_in_itv. + by case: Fab => + _ _; apply; near: y; exact: near_in_itvoo. - by move=> x y xab yab yx; rewrite ltrN2 incrF. - by []. have mGF : measurable_fun `]a, b[ (G \o F). diff --git a/theories/normedtype.v b/theories/normedtype.v index a780b3807..8d0fc8437 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5339,7 +5339,7 @@ Proof. by rewrite !(boundr_in_itv, boundl_in_itv). Qed. Section near_in_itv. Context {R : realFieldType} (a b : R). -Lemma near_in_itv : +Lemma near_in_itvoo : {in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}. Proof. exact: interval_open. Qed. @@ -5352,10 +5352,10 @@ suff : z \in `]a, +oo[%classic by rewrite inE. near: z. rewrite near_nbhs. apply: (@open_in_nearW _ _ `]a, +oo[%classic) => //. -by rewrite inE/=. +by rewrite inE. Unshelve. end_near. Qed. -Lemma near_in_itvyo : +Lemma near_in_itvNyo : {in `]-oo, b[, forall y, \forall z \near y, z \in `]-oo, b[}. Proof. move=> x xb. @@ -5367,15 +5367,10 @@ apply: (@open_in_nearW _ _ `]-oo, b[%classic) => //. by rewrite inE/=. Unshelve. end_near. Qed. -Lemma near_in_itvyy : - {in `]-oo, +oo[, forall y : R, \forall z \near y, z \in `]-oo, +oo[}. -Proof. -move=> x _. -rewrite -near_nbhs. -exact: nearW => //. -Qed. - End near_in_itv. +#[deprecated(since="mathcomp-analysis 1.7.0", + note="use `near_in_itvoo` instead")] +Notation near_in_itv := near_in_itvoo (only parsing). Lemma cvg_patch {R : realType} (f : R -> R^o) (a b : R) (x : R) : (a < b)%R -> x \in `]a, b[ -> @@ -5387,7 +5382,7 @@ move/cvgrPdist_lt : xf => /(_ e e0) xf. near=> z. rewrite patchE ifT//; last first. rewrite inE; apply: subset_itv_oo_cc. - by near: z; exact: near_in_itv. + by near: z; exact: near_in_itvoo. near: z. rewrite /prop_near1 /nbhs/= /nbhs_subspace ifT// in xf; last first. by rewrite inE/=; exact: subset_itv_oo_cc xab. @@ -5395,7 +5390,7 @@ case: xf => x0 /= x00 xf. near=> z. apply: xf => //=. rewrite inE; apply: subset_itv_oo_cc. -by near: z; exact: near_in_itv. +by near: z; exact: near_in_itvoo. Unshelve. all: by end_near. Qed. Notation "f @`[ a , b ]" := diff --git a/theories/realfun.v b/theories/realfun.v index bb902bfa2..14486a721 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1421,10 +1421,10 @@ have := xb; rewrite le_eqVlt => /orP[/eqP {}xb {ax}|{}xb]. have xoab : x \in `]a, b[ by rewrite in_itv /=; apply/andP; split. near=> y; suff: l <= f y <= u. by rewrite ge_max le_min -!andbA => /and4P[-> _ ->]. -have ? : y \in `[a, b] by apply: subset_itv_oo_cc; near: y; apply: near_in_itv. +have ? : y \in `[a, b] by apply: subset_itv_oo_cc; near: y; exact: near_in_itvoo. have fyab : f y \in `[f a, f b] by rewrite in_itv/= !fle// ?ltW. rewrite -[l <= _]gle -?[_ <= u]gle// ?fK //. -apply: subset_itv_oo_cc; near: y; apply: near_in_itv; rewrite in_itv /=. +apply: subset_itv_oo_cc; near: y; apply: near_in_itvoo; rewrite in_itv /=. rewrite -[x]fK // !glt//= lt_min gt_max ?andbT ltrBlDr ltr_pwDr //. by apply/and3P; split; rewrite // flt. Unshelve. all: by end_near. Qed. diff --git a/theories/trigo.v b/theories/trigo.v index cfcd3db86..39bebecc9 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -1003,7 +1003,7 @@ move=> /andP[x_gtN1 x_lt1]; rewrite -[x]acosK; first last. by have : -1 <= x <= 1 by rewrite !ltW //; case/andP: xB. apply: nbhs_singleton (near_can_continuous _ _); last first. by near=> z; apply: continuous_cos. -have /near_in_itv aI : acos x \in `]0, pi[. +have /near_in_itvoo aI : acos x \in `]0, pi[. suff : 0 < acos x < pi by []. by rewrite acos_gt0 ?ltW //= acos_ltpi // ltW ?andbT. near=> z; apply: cosK. @@ -1016,7 +1016,7 @@ Lemma is_derive1_acos x : Proof. move=> /andP[x_gtN1 x_lt1]; rewrite -sin_acos ?ltW // -invrN. rewrite -{1}[x]acosK; last by have : -1 <= x <= 1 by rewrite ltW // ltW. -have /near_in_itv aI : acos x \in `]0, pi[. +have /near_in_itvoo aI : acos x \in `]0, pi[. suff : 0 < acos x < pi by []. by rewrite acos_gt0 ?ltW //= acos_ltpi // ltW ?andbT. apply: (@is_derive_inverse R cos). @@ -1103,7 +1103,7 @@ move=> /andP[x_gtN1 x_lt1]; rewrite -[x]asinK; first last. by have : -1 <= x <= 1 by rewrite !ltW //; case/andP: xB. apply: nbhs_singleton (near_can_continuous _ _); last first. by near=> z; apply: continuous_sin. -have /near_in_itv aI : asin x \in `](-(pi/2)), (pi/2)[. +have /near_in_itvoo aI : asin x \in `](-(pi/2)), (pi/2)[. suff : - (pi / 2) < asin x < pi / 2 by []. by rewrite asin_gtNpi2 ?ltW ?andbT //= asin_ltpi2 // ltW. near=> z; apply: sinK. @@ -1117,7 +1117,7 @@ Lemma is_derive1_asin x : Proof. move=> /andP[x_gtN1 x_lt1]; rewrite -cos_asin ?ltW //. rewrite -{1}[x]asinK; last by have : -1 <= x <= 1 by rewrite ltW // ltW. -have /near_in_itv aI : asin x \in `](-(pi/2)), (pi/2)[. +have /near_in_itvoo aI : asin x \in `](-(pi/2)), (pi/2)[. suff : -(pi/2) < asin x < pi/2 by []. by rewrite asin_gtNpi2 ?ltW ?andbT //= asin_ltpi2 // ltW. apply: (@is_derive_inverse R sin). @@ -1219,7 +1219,7 @@ Qed. Lemma continuous_atan x : {for x, continuous (@atan R)}. Proof. rewrite -[x]atanK. -have /near_in_itv aI : atan x \in `](-(pi / 2)), (pi / 2)[. +have /near_in_itvoo aI : atan x \in `](-(pi / 2)), (pi / 2)[. suff : - (pi / 2) < atan x < pi / 2 by []. by rewrite atan_gtNpi2 atan_ltpi2. apply: nbhs_singleton (near_can_continuous _ _); last first. @@ -1244,7 +1244,7 @@ Proof. rewrite -{1}[x]atanK. have cosD0 : cos (atan x) != 0. by apply/lt0r_neq0/cos_gt0_pihalf; rewrite atan_gtNpi2 atan_ltpi2. -have /near_in_itv aI : atan x \in `](-(pi/2)), (pi/2)[. +have /near_in_itvoo aI : atan x \in `](-(pi/2)), (pi/2)[. suff : - (pi / 2) < atan x < pi / 2 by []. by rewrite atan_gtNpi2 atan_ltpi2. apply: (@is_derive_inverse R tan).