From b74a117092059a3ffb9be9b5e56b6013fb03e477 Mon Sep 17 00:00:00 2001 From: IshYosh <103252572+IshiguroYoshihiro@users.noreply.github.com> Date: Wed, 13 Nov 2024 19:22:29 +0900 Subject: [PATCH] near_in_itv_oy/Nyo (#1375) * near_in_itv_oy/Nyo --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 4 ++++ theories/ftc.v | 2 +- theories/normedtype.v | 38 +++++++++++++++++++++++++++++++++++--- theories/realfun.v | 4 ++-- theories/trigo.v | 12 ++++++------ 5 files changed, 48 insertions(+), 12 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 260152313..a191ece6d 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_itvNyo` - in file `mathcomp_extra.v`, + new definition `sigT_fun`. @@ -147,6 +148,9 @@ ### Renamed +- in `normedtype.v`: + + `near_in_itv` -> `near_in_itvoo` + ### Generalized - in `lebesgue_integral.v`: 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 debaf7d26..8d0fc8437 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5336,10 +5336,42 @@ 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_itvoo : {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_itvNyo : + {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. + +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[ -> f @ (x : subspace `[a, b]) --> f x -> @@ -5350,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. @@ -5358,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 ebf570f54..70fae9c30 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1435,10 +1435,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).