tentative proof factorization

CHANGELOG_UNRELEASED.md

@@ -67,8 +67,9 @@
 - in file `separation_axioms.v`,
   + new lemma `sigT_hausdorff`.
 
-- in file `normedtype.v`,
-  + new lemmas `continuous_within_itvcyP`, `continuous_within_itvycP`
+- in `normedtype.v`:
+  + lemma `in_continuous_mksetP`
+  + lemmas `continuous_within_itvcyP`, `continuous_within_itvycP`
 
 ### Changed
 

theories/normedtype.v

@@ -2080,31 +2080,66 @@ 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 ->
+(* TODO: move earlier *)
+Lemma in_continuous_mksetP {T : realFieldType} {U : realFieldType}
+    (i : interval T) (f : T -> U) :
+  {in i, continuous f} <-> {in [set` i], continuous f}.
+Proof.
+by split => [fi x /set_mem/=|fi x xi]; [exact: fi|apply: fi; rewrite inE].
+Qed.
+
+Section continuous_within_itvP.
+Context {R : realType}.
+Implicit Type f : R -> R.
+
+Let near_at_left (a : itv_bound R) b f eps : (a < BLeft b)%O -> 0 < eps ->
+  {within [set` Interval a (BRight b)], continuous f} ->
+  \forall t \near b^'-, normr (f b - f t) < eps.
+Proof.
+move=> ab eps_gt0 cf.
+move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (cf b).
+rewrite /dnbhs/= near_withinE !near_simpl /prop_near1 /nbhs/=.
+rewrite -nbhs_subspace_in//; last first.
+  rewrite /= in_itv/= lexx andbT.
+  by move: a ab {cf} => [[a|a]/=|[|]//]; rewrite bnd_simp// => /ltW.
+rewrite /within/= near_simpl; apply: filter_app.
+move: a ab {cf} => [a0 a/= /[!bnd_simp] ab|[_|//]].
+- exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
+  apply=> //; rewrite ?lt_eqF// !in_itv/= (ltW ac)/= andbT; move: cba => /=.
+  rewrite gtr0_norm ?subr_gt0// ltrD2l ltrNr opprK => {}ac.
+  by case: a0 => //=; exact/ltW.
+- by exists 1%R => //= c cb1 + bc; apply; rewrite ?lt_eqF ?in_itv/= ?ltW.
+Qed.
+
+Let near_at_right a (b : itv_bound R) f eps : (BRight a < b)%O -> 0 < eps ->
+  {within [set` Interval (BLeft a) b], continuous f} ->
+  \forall t \near a^'+, normr (f a - f t) < eps.
+Proof.
+move=> ab eps_gt0 cf.
+move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (cf a).
+rewrite /dnbhs/= near_withinE !near_simpl// /prop_near1 /nbhs/=.
+rewrite -nbhs_subspace_in//; last first.
+  rewrite /= in_itv/= lexx//=.
+  by move: b ab {cf} => [[b|b]/=|[|]//]; rewrite bnd_simp// => /ltW.
+rewrite /within/= near_simpl; apply: filter_app.
+move: b ab {cf} => [b0 b/= /[!bnd_simp] ab|[//|_]].
+- exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
+  apply=> //; rewrite ?gt_eqF// !in_itv/= (ltW ac)/=; move: cba => /=.
+  rewrite ltr0_norm ?subr_lt0// opprB ltrD2r.
+  by case: b0 => //= /ltW.
+- by exists 2%R => //= c ca1 + ac; apply; rewrite ?gt_eqF ?in_itv/= ?ltW.
+Qed.
+
+Lemma continuous_within_itvP a b f : a < b ->
   {within `[a, b], continuous f} <->
   [/\ {in `]a, b[, continuous f}, f @ a^'+ --> f a & f @b^'- --> f b].
 Proof.
 move=> ab; split=> [abf|].
-  have [aab bab] : a \in `[a, b] /\ b \in `[a, b].
-    by rewrite !in_itv/= !lexx (ltW ab).
-  split; [|apply/cvgrPdist_lt => eps eps_gt0 /=..].
-  - suff : {in `]a, b[%classic, continuous f}.
-      by move=> P c W; apply: P; rewrite inE.
-    rewrite -continuous_open_subspace; last exact: interval_open.
+  split; [apply/in_continuous_mksetP|apply/cvgrPdist_lt => eps eps_gt0 /=..].
+  - rewrite -continuous_open_subspace; last exact: interval_open.
     by move: abf; exact/continuous_subspaceW/subset_itvW.
-  - move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf a).
-    rewrite /dnbhs/= near_withinE !near_simpl// /prop_near1 /nbhs/=.
-    rewrite -nbhs_subspace_in// /within/= near_simpl.
-    apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
-    apply=> //; rewrite ?gt_eqF// !in_itv/= (ltW ac)/=; move: cba => /=.
-    by rewrite ltr0_norm ?subr_lt0// opprB ltrD2r => /ltW.
-  - move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf b).
-    rewrite /dnbhs/= near_withinE !near_simpl /prop_near1 /nbhs/=.
-    rewrite -nbhs_subspace_in// /within/= near_simpl.
-    apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
-    apply=> //; rewrite ?lt_eqF// !in_itv/= (ltW ac)/= andbT; move: cba => /=.
-    by rewrite gtr0_norm ?subr_gt0// ltrD2l ltrNr opprK => /ltW.
+  - by apply: near_at_right => //; rewrite bnd_simp.
+  - by apply: near_at_left => //; rewrite bnd_simp.
 case=> ctsoo ctsL ctsR; apply/subspace_continuousP => x /andP[].
 rewrite !bnd_simp/= !le_eqVlt => /predU1P[<-{x}|ax] /predU1P[|].
 - by move/eqP; rewrite lt_eqF.
@@ -2124,58 +2159,39 @@ rewrite !bnd_simp/= !le_eqVlt => /predU1P[<-{x}|ax] /predU1P[|].
   by rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open].
 Qed.
 
-Lemma continuous_within_itvcyP {R : realType} a (f : R -> R) :
+Lemma continuous_within_itvcyP a (f : R -> R) :
   {within `[a, +oo[, continuous f} <->
   {in `]a, +oo[, continuous f} /\ f x @[x --> a^'+] --> f a.
 Proof.
-split=> [af|].
-  have aa : a \in `[a, +oo[ by rewrite !in_itv/= lexx.
-  split; [|apply/cvgrPdist_lt => eps eps_gt0 /=].
-  - suff : {in `]a, +oo[%classic, continuous f}.
-      by move=> P c W; apply: P; rewrite inE.
-    rewrite -continuous_open_subspace; last exact: interval_open.
-    move: af; apply/continuous_subspaceW.
-    by move=> ?/=; rewrite !in_itv/= !andbT; exact: ltW.
-  - move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (af a).
-    rewrite /dnbhs/= near_withinE near_simpl /prop_near1/nbhs/=.
-    rewrite -nbhs_subspace_in// /within/= near_simpl.
-    apply: filter_app; exists 2%R => //= c ca1 + ac.
-    by apply; rewrite ?gt_eqF ?in_itv/= ?ltW.
-move=> [cf fa].
-apply/subspace_continuousP => x /andP[].
+split=> [cf|].
+  split; [apply/in_continuous_mksetP|apply/cvgrPdist_lt => eps eps_gt0 /=].
+  - rewrite -continuous_open_subspace; last exact: interval_open.
+    by apply: continuous_subspaceW cf => ?; rewrite /= !in_itv !andbT/= => /ltW.
+  - by apply: near_at_right => //; rewrite bnd_simp.
+move=> [cf fa]; apply/subspace_continuousP => x /andP[].
 rewrite bnd_simp/= le_eqVlt => /predU1P[<-{x}|ax] _.
 - apply/cvgrPdist_lt => eps eps_gt0/=.
   move/cvgrPdist_lt/(_ _ eps_gt0) : fa.
-  rewrite /at_right !near_withinE.
-  apply: filter_app; exists 1%R => //= c c1a + ac.
-  rewrite in_itv/= andbT le_eqVlt in ac.
-  by case/predU1P : ac => [->|/[swap]/[apply]//]; rewrite subrr normr0.
+  rewrite /at_right !near_withinE; apply: filter_app.
+  exists 1%R => //= c c1a /[swap]; rewrite in_itv/= andbT le_eqVlt.
+  by move=> /predU1P[->|/[swap]/[apply]//]; rewrite subrr normr0.
 - have xaoo : x \in `]a, +oo[ by rewrite in_itv/= andbT.
   rewrite within_interior; first exact: cf.
   suff : `]a, +oo[ `<=` interior `[a, +oo[ by exact.
   rewrite -open_subsetE; last exact: interval_open.
   by move=> ?/=; rewrite !in_itv/= !andbT; exact: ltW.
 Qed.
 
-Lemma continuous_within_itvycP {R : realType} b (f : R -> R) :
+Lemma continuous_within_itvycP b (f : R -> R) :
   {within `]-oo, b], continuous f} <->
   {in `]-oo, b[, continuous f} /\ f x @[x --> b^'-] --> f b.
 Proof.
-split=> [bf|].
-  have bb : b \in `]-oo, b] by rewrite !in_itv/= lexx.
-  split; [|apply/cvgrPdist_lt => eps eps_gt0 /=].
-  - suff : {in `]-oo, b[%classic, continuous f}.
-      by move=> P c W; apply: P; rewrite inE.
-    rewrite -continuous_open_subspace; last exact: interval_open.
-    move: bf; apply/continuous_subspaceW.
-    by move=> ?/=; rewrite !in_itv/=; exact: ltW.
-  - move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (bf b).
-    rewrite /dnbhs/= near_withinE near_simpl /prop_near1/nbhs/=.
-    rewrite -nbhs_subspace_in// /within/= near_simpl.
-    apply: filter_app; exists 1%R => //= c cb1 + bc.
-    by apply; rewrite ?lt_eqF ?in_itv/= ?ltW.
-move=> [cf fb].
-apply/subspace_continuousP => x /andP[_].
+split=> [cf|].
+  split; [apply/in_continuous_mksetP|apply/cvgrPdist_lt => eps eps_gt0 /=].
+  - rewrite -continuous_open_subspace; last exact: interval_open.
+    by apply: continuous_subspaceW cf => ?/=; rewrite !in_itv/=; exact: ltW.
+  - by apply: near_at_left => //; rewrite bnd_simp.
+move=> [cf fb]; apply/subspace_continuousP => x /andP[_].
 rewrite bnd_simp/= le_eqVlt=> /predU1P[->{x}|xb].
 - apply/cvgrPdist_lt => eps eps_gt0/=.
   move/cvgrPdist_lt/(_ _ eps_gt0) : fb.
@@ -2190,6 +2206,8 @@ rewrite bnd_simp/= le_eqVlt=> /predU1P[->{x}|xb].
   by move=> ?/=; rewrite !in_itv/=; exact: ltW.
 Qed.
 
+End continuous_within_itvP.
+
 Lemma within_continuous_continuous {R : realType} a b (f : R -> R) x : (a < b)%R ->
   {within `[a, b], continuous f} -> x \in `]a, b[ -> {for x, continuous f}.
 Proof.