From af3797c8475b8b3fc95ff33c43a4f95c58c4c5f1 Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 12 Jan 2024 13:39:09 -0500 Subject: [PATCH] filling in admits --- theories/normedtype.v | 48 +++++++++++++++++++++++++++++++++++++++++++ theories/realfun.v | 23 ++++----------------- 2 files changed, 52 insertions(+), 19 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index d947bd320..5edd73dd5 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2904,6 +2904,54 @@ by apply: xe_A => //; rewrite eq_sym. Qed. Arguments cvg_at_leftE {R V} f x. +Lemma continuous_within_itvP {R : realType } a b (f : R -> R) : + a < b -> + {within `[a,b], continuous f} <-> + {in `]a,b[, continuous f} /\ f @ a^'+ --> f a /\ f @b^'- --> f b. +Proof. +move=> ab; split. +have [aab bab] : a \in `[a, b] /\ b \in `[a, b]. + by split; apply/andP; split => //; apply: ltW. +have [aabC babC] : `[a, b]%classic a /\ `[a, b]%classic b. + by rewrite ?inE /=; split. +move=> abf; split. + suff : {in `]a,b[%classic, continuous f}. + by move=> P ? W; by apply: P; move: W; rewrite inE /=. + rewrite -(@continuous_open_subspace); last exact: interval_open. + by move: abf; apply: continuous_subspaceW; apply: subset_itvW. + split; apply/cvgrPdist_lt => eps eps_gt0 /=; + [move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf a) + | move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf b)]; + rewrite /dnbhs /= ?near_withinE ?near_simpl /prop_near1/nbhs /=; + rewrite -nbhs_subspace_in // /within /= ?nbhs_simpl near_simpl; + apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac; + (apply => //; last by apply/eqP => CA; move: ac; rewrite CA ltxx); + apply/andP; split; apply: ltW => //; move: cba; rewrite /= ?[(`|a-c|)]distrC ger0_norm. + - by rewrite ltrBlDr -addrA [-_+_]addrC subrr addr0. + - by apply: ltW; rewrite subr_gt0. + - by rewrite ltrBlDr addrC addrA ltrBrDl -ltrBrDr -addrA subrr addr0. + - by apply: ltW; rewrite subr_gt0. +case=> ctsoo [ctsL ctsR]; apply/subspace_continuousP => x /andP []. +rewrite ?le_eqVlt => /orP + /orP; case => + []. +- by move=> /eqP [<-] /eqP [E]; move: ab; rewrite E ltxx. +- move=> /eqP [<-_]; apply/cvgrPdist_lt => eps eps_gt0 /=. + move/cvgrPdist_lt/(_ _ eps_gt0):ctsL; rewrite /at_right ?near_withinE. + apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac. + (have : a <= c by move: ac => /andP []); rewrite le_eqVlt => /orP []. + by move=> /eqP ->; rewrite subrr normr0. + by move=> ?; apply. +- move=> _ /eqP [->]; apply/cvgrPdist_lt => eps eps_gt0 /=. + move/cvgrPdist_lt/(_ _ eps_gt0):ctsR; rewrite /at_left ?near_withinE. + apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac. + (have : c <= b by move: ac => /andP []); rewrite le_eqVlt => /orP []. + by move=> /eqP ->; rewrite subrr normr0. + by move=> ?; apply. +- move=> ax xb; have aboox : x \in `]a,b[ by apply/andP; split. + rewrite within_interior; first exact: ctsoo. + suff : `]a,b[ `<=` interior `[a,b] by apply. + rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open]. +Qed. + (* TODO: generalize to R : numFieldType *) Section hausdorff. diff --git a/theories/realfun.v b/theories/realfun.v index b907b113c..f9a1bc272 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1113,6 +1113,7 @@ have : f a >= f b by rewrite (itvP xfafb). by case: ltrgtP xfafb => // ->. Qed. + Lemma segment_inc_surj_continuous a b f : {in `[a, b] &, {mono f : x y / x <= y}} -> set_surj `[a, b] `[f a, f b] f -> {within `[a, b], continuous f}. @@ -1424,12 +1425,7 @@ End is_derive_inverse. (eapply is_deriveV; first by []) : typeclass_instances. From mathcomp Require Import path. -Require Import sequences. -Notation "'nondecreasing_fun' f" := ({homo f : n m / (n <= m)%R >-> (n <= m)%R}) - (at level 10). -Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%R >-> (n >= m)%R}) - (at level 10). Lemma nondecreasing_funN {R : realType} a b (f : R -> R) : {in `[a, b] &, nondecreasing_fun f} <-> {in `[a, b] &, nonincreasing_fun (\- f)}. @@ -1457,11 +1453,6 @@ Proof. by move=> uS [y Sy] /le_trans; apply; apply: sup_ub. Qed. -(* NB: already in master? *) -Lemma ereal_sup_le {R : realType} (S : set (\bar R)) x : - (exists2 y, S y & x <= y)%E -> (x <= ereal_sup S)%E. -Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ub. Qed. - Lemma ereal_supy {R : realType} (A : set \bar R) : A +oo%E -> ereal_sup A = +oo%E. Proof. @@ -2293,7 +2284,7 @@ Lemma total_variation_opp a b f : TV a b f = TV (- b) (- a) (f \o -%R). Proof. by rewrite /total_variation variations_opp. Qed. Lemma TV_left_continuous a b x f : a < x -> x <= b -> - f @ at_left x --> f x -> + f @ x^'- --> f x -> BV a b f -> fine \o TV a ^~ f @ x^'- --> fine (TV a x f). Proof. @@ -2332,19 +2323,13 @@ apply: (TV_right_continuous _ _ _ bvNf). by apply/at_left_at_rightP; rewrite /= opprK. Unshelve. all: by end_near. Qed. -Lemma continuous_within_itvP a b (f : R -> R) : - {within `[a,b], continuous f} <-> - {in `]a,b[, continuous f} /\ f @ a^'+ --> f a /\ f @b^'- --> f b. -Proof. -Admitted. - Lemma TV_continuous a b (f : R -> R) : a < b -> {within `[a,b], continuous f} -> BV a b f -> {within `[a,b], continuous (fine \o TV a ^~ f)}. Proof. -move=> ab /continuous_within_itvP [int [l r]] bdf. -apply/continuous_within_itvP; repeat split. +move=> ab /(@continuous_within_itvP _ _ _ _ ab) [int [l r]] bdf. +apply/continuous_within_itvP; (repeat split) => //. - move=> x /[dup] xab; rewrite in_itv /= => /andP [ax xb]. apply/left_right_continuousP; split. apply: (TV_left_continuous _ (ltW xb)) => //.