Skip to content
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

near_in_itv_oy/yo/yy #1375

Merged
merged 2 commits into from
Nov 13, 2024
Merged

near_in_itv_oy/yo/yy #1375

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
d3b6809
near_in_itv_oy/yo/yy
IshiguroYoshihiro Oct 29, 2024
30e4396
rm near_in_itvyy, deprecation, renaming
affeldt-aist Nov 13, 2024
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
4 changes: 4 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`

### Changed

Expand All @@ -76,6 +77,9 @@

### Renamed

- in `normedtype.v`:
+ `near_in_itv` -> `near_in_itvoo`

### Generalized

### Deprecated
Expand Down
2 changes: 1 addition & 1 deletion theories/ftc.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down
38 changes: 35 additions & 3 deletions theories/normedtype.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand All @@ -5350,15 +5382,15 @@ 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.
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 ]" :=
Expand Down
4 changes: 2 additions & 2 deletions theories/realfun.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
12 changes: 6 additions & 6 deletions theories/trigo.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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).
Expand Down Expand Up @@ -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.
Expand All @@ -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).
Expand Down Expand Up @@ -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.
Expand All @@ -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).
Expand Down