fixed connected continuous

cleanup topology fixing notations minor cleanups fixing build
math-comp · Jan 20, 2022 · d055a35 · d055a35
1 parent 3f7d5f0
commit d055a35
Show file tree

Hide file tree

Showing 4 changed files with 289 additions and 148 deletions.
diff --git a/theories/derive.v b/theories/derive.v
@@ -1301,16 +1301,15 @@ Qed.
 End Derive.
 
 Lemma EVT_max (R : realType) (f : R -> R) (a b : R) : (* TODO : Filter not infered *)
-  a <= b -> {in `[a, b]%R, continuous f} -> exists2 c, c \in `[a, b]%R &
+  a <= b -> {within `[a, b], continuous f} -> exists2 c, c \in `[a, b]%R &
   forall t, t \in `[a, b]%R -> f t <= f c.
 Proof.
 move=> leab fcont; set imf := [set t | (f @` `[a, b]) t].
 have imf_sup : has_sup imf.
-  split.
-    by exists (f a); apply/imageP; rewrite /= in_itv /= lexx.
-  have [M [Mreal imfltM]] : bounded_set (f @` `[a, b]).
-    apply/compact_bounded/continuous_compact; last exact: segment_compact.
-    by move=> ?; rewrite inE => /fcont.
+  split; first by exists (f a); apply/imageP; rewrite /= in_itv /= lexx.
+  have [M [Mreal imfltM]] : bounded_set (f @` `[a, b]). 
+    apply/compact_bounded/continuous_compact =>//. 
+    by exact: segment_compact.
   exists (M + 1); apply/ubP => y /imfltM yleM.
   apply: le_trans (yleM _ _); last by rewrite ltr_addl.
   by rewrite ler_norm.
@@ -1322,14 +1321,15 @@ have {}imf_ltsup : forall t, t \in `[a, b]%R -> f t < sup imf.
   rewrite falseE; apply: imf_ltsup; exists t => //.
   apply/eqP; rewrite eq_le supleft andbT.
   by move/ubP : (sup_upper_bound imf_sup); apply; exact: imageP.
-have invf_continuous : {in `[a, b]%R, continuous (fun t => (sup imf - f t)^-1 : R)}.
-  move=> t tab; apply: cvgV => //.
-    by rewrite subr_eq0 gt_eqF // imf_ltsup.
-  by apply: cvgD; [apply: cst_continuous|apply: cvgN; apply: fcont].
-have /ex_strict_bound_gt0 [k k_gt0 /= imVfltk] :
-   bounded_set ((fun t => (sup imf - f t)^-1) @` `[a, b]).
+set g := (fun t => (sup imf - f t)^-1 : R).
+have invf_continuous : {within `[a, b], continuous g}.
+  rewrite continuous_subspace_in=> t tab; apply: cvgV => //=.
+    rewrite subr_eq0 gt_eqF // imf_ltsup // in_itv //=.
+    by rewrite inE in tab; exact tab.
+  by apply: cvgD; [apply: cst_continuous | apply: cvgN; apply (fcont t)].
+have /ex_strict_bound_gt0 [k k_gt0 /= imVfltk] : bounded_set (g @` `[a, b]).
   apply/compact_bounded/continuous_compact; last exact: segment_compact.
-  by move=> ?; rewrite inE => /invf_continuous.
+  exact: invf_continuous.
 have : exists2 y, imf y & sup imf - k^-1 < y.
   by apply: sup_adherent => //; rewrite invr_gt0.
 move=> [y] -[t tab <-] {y}.
@@ -1340,12 +1340,12 @@ by rewrite (le_lt_trans (ler_norm _) _) ?imVfltk//; apply: imageP.
 Qed.
 
 Lemma EVT_min (R : realType) (f : R -> R) (a b : R) :
-  a <= b -> {in `[a, b]%R, continuous f} -> exists2 c, c \in `[a, b]%R &
+  a <= b -> {within `[a, b], continuous f} -> exists2 c, c \in `[a, b]%R &
   forall t, t \in `[a, b]%R -> f c <= f t.
 Proof.
 move=> leab fcont.
-have /(EVT_max leab) [c clr fcmax] : {in `[a, b]%R, continuous (- f)}.
-  by move=> ? /fcont; apply: continuousN.
+have /(EVT_max leab) [c clr fcmax] : {within `[a, b], continuous (- f)}.
+  move=> ?; apply: continuousN => ?; exact: fcont.
 by exists c => // ? /fcmax; rewrite ler_opp2.
 Qed.
 
@@ -1458,7 +1458,7 @@ Qed.
 
 Lemma Rolle (R : realType) (f : R -> R) (a b : R) :
   a < b -> (forall x, x \in `]a, b[%R -> derivable f x 1) ->
-  {in `[a, b]%R, continuous f} -> f a = f b ->
+  {within `[a, b], continuous f} -> f a = f b ->
   exists2 c, c \in `]a, b[%R & is_derive c 1 f 0.
 Proof.
 move=> ltab fdrvbl fcont faefb.
@@ -1488,62 +1488,84 @@ suff -> : f cmax = f cmin by rewrite fcmin // in_itv /= !ltW ?(itvP sab).
 by case: cmaxeaVb => ->; case: cmineaVb => ->.
 Qed.
 
+
 Lemma MVT (R : realType) (f df : R -> R) (a b : R) :
-  a <= b -> (forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) ->
-  {in `[a, b]%R, continuous f} ->
-  exists2 c, c \in `[a, b]%R & f b - f a = df c * (b - a).
+  a < b -> (forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) ->
+  {within `[a, b], continuous f} ->
+  exists2 c, c \in `]a, b[%R & f b - f a = df c * (b - a).
 Proof.
-move=> leab fdrvbl fcont; move: leab; rewrite le_eqVlt => /orP [/eqP aeb|altb].
-  by exists a; [rewrite inE/= aeb lexx|rewrite aeb !subrr mulr0].
+move=> altb fdrvbl fcont.
 set g := f + (- ( *:%R^~ ((f b - f a) / (b - a)) : R -> R)).
 have gdrvbl : forall x, x \in `]a, b[%R -> derivable g x 1.
   by move=> x /fdrvbl dfx; apply: derivableB => //; apply/derivable1_diffP.
-have gcont : {in `[a, b]%R, continuous g}.
-  move=> x /fcont fx; apply: continuousD fx _; apply: continuousN.
-  exact: scalel_continuous.
+have gcont : {within `[a, b], continuous g}.
+  move=> x; apply: continuousD _ ; first (move=>?; exact: fcont). 
+  by apply/continuousN/continuous_subspaceT => ? ?; apply: scalel_continuous.
 have gaegb : g a = g b.
   rewrite /g -![(_ - _ : _ -> _) _]/(_ - _).
   apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl.
   rewrite [_ *: _]mulrA mulrC mulrA mulVf.
     by rewrite mul1r addrCA subrr addr0.
   by apply: lt0r_neq0; rewrite subr_gt0.
 have [c cab dgc0] := Rolle altb gdrvbl gcont gaegb.
-exists c; first by rewrite in_itv /= ltW (itvP cab).
+exists c; first exact: cab. 
 have /fdrvbl dfc := cab; move/@derive_val: dgc0; rewrite deriveB //; last first.
   exact/derivable1_diffP.
 move/eqP; rewrite [X in _ - X]deriveE // derive_val diff_val scale1r subr_eq0.
 move/eqP->; rewrite -mulrA mulVf ?mulr1 //; apply: lt0r_neq0.
 by rewrite subr_gt0.
 Qed.
 
+(* Weakens MVT to work when the interval is a single point. *)
+Lemma MVT_point (R : realType) (f df : R -> R) (a b : R) :
+  a <= b -> (forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) ->
+  {within `[a, b], continuous f} ->
+  exists2 c, c \in `[a, b]%R & f b - f a = df c * (b - a).
+Proof.
+move=> leab fdrvbl fcont; move: leab; rewrite le_eqVlt => /orP [/eqP aeb|altb].
+  by exists a; [rewrite inE/= aeb lexx|rewrite aeb !subrr mulr0].
+have [c cab D] := MVT altb fdrvbl fcont.
+by exists c => //; rewrite in_itv /= ltW (itvP cab).
+Qed.
+
 Lemma ler0_derive1_nincr (R : realType) (f : R -> R) (a b : R) :
-  (forall x, x \in `[a, b]%R -> derivable f x 1) ->
-  (forall x, x \in `[a, b]%R -> f^`() x <= 0) ->
+  (forall x, x \in `]a, b[%R -> derivable f x 1) ->
+  (forall x, x \in `]a, b[%R -> f^`() x <= 0) ->
+  {within `[a,b], continuous f} ->
   forall x y, a <= x -> x <= y -> y <= b -> f y <= f x.
 Proof.
-move=> fdrvbl dfle0 x y leax lexy leyb; rewrite -subr_ge0.
+move=> fdrvbl dfle0 ctsf x y leax lexy leyb; rewrite -subr_ge0.
+move: lexy; rewrite le_eqVlt => /orP [/eqP xyb|xlty].
+  by rewrite xyb subrr.
 have itvW : {subset `[x, y]%R <= `[a, b]%R}.
   by apply/subitvP; rewrite /<=%O /= /<=%O /= leyb leax.
+have itvWlt : {subset `]x, y[%R <= `]a, b[%R}.
+  by apply subitvP; rewrite /<=%O /= /<=%O /= leyb leax.
 have fdrv z : z \in `]x, y[%R -> is_derive z 1 f (f^`()z).
-  rewrite inE => /andP [/ltW lexz /ltW lezy].
+  rewrite inE => /andP [lexz lezy].
   apply: DeriveDef; last by rewrite derive1E.
   apply: fdrvbl; rewrite inE; apply/andP.
-  by split; [exact: le_trans lexz | exact: le_trans leyb].
-have [] := @MVT _ f (f^`()) x y lexy fdrv.
-  by move=> ? /itvW /fdrvbl /derivable1_diffP /differentiable_continuous.
-move=> t /itvW /dfle0 dft dftxy; rewrite -oppr_le0 opprB dftxy.
-by apply: mulr_le0_ge0 => //; rewrite subr_ge0.
+  split; [exact: le_trans lexz | apply: le_trans]; first exact: lezy.
+  by rewrite /Order.le; exact: leyb.
+have [] := @MVT _ f (f^`()) x y xlty fdrv. 
+  apply: (@continuous_subspaceW _ _ _ `[a,b]); first exact: itvW. 
+  by rewrite continuous_subspace_in.
+move=> t /itvWlt dft dftxy; rewrite -oppr_le0 opprB dftxy. 
+apply: mulr_le0_ge0 => //; last by rewrite subr_ge0 ltW.
+exact: dfle0.
 Qed.
 
 Lemma le0r_derive1_ndecr (R : realType) (f : R -> R) (a b : R) :
-  (forall x, x \in `[a, b]%R -> derivable f x 1) ->
-  (forall x, x \in `[a, b]%R -> 0 <= f^`() x) ->
+  (forall x, x \in `]a, b[%R -> derivable f x 1) ->
+  (forall x, x \in `]a, b[%R -> 0 <= f^`() x) ->
+  {within `[a,b], continuous f} ->
   forall x y, a <= x -> x <= y -> y <= b -> f x <= f y.
 Proof.
-move=> fdrvbl dfge0 x y; rewrite -[f _ <= _]ler_opp2.
-apply: (@ler0_derive1_nincr _ (- f)) => t tab; first exact/derivableN/fdrvbl.
-rewrite derive1E deriveN; last exact: fdrvbl.
-by rewrite oppr_le0 -derive1E; apply: dfge0.
+move=> fdrvbl dfge0 fcont x y; rewrite -[f _ <= _]ler_opp2.
+apply (@ler0_derive1_nincr _ (- f)) => t tab; first exact/derivableN/fdrvbl.
+  rewrite derive1E deriveN; last exact: fdrvbl.
+  by rewrite oppr_le0 -derive1E; apply: dfge0.
+by apply: continuousN; exact: fcont.
 Qed.
 
 Lemma derive1_comp (R : realFieldType) (f g : R -> R) x :

diff --git a/theories/normedtype.v b/theories/normedtype.v
@@ -3328,58 +3328,23 @@ rewrite {1}(splitr x) ger_addl pmulr_lle0 // => /(lt_le_trans x0);
 Qed.
 
 Lemma IVT (R : realType) (f : R -> R) (a b v : R) :
-  a <= b -> {in `[a, b], continuous f} ->
+  a <= b -> {within `[a, b], continuous f} ->
   minr (f a) (f b) <= v <= maxr (f a) (f b) ->
   exists2 c, c \in `[a, b] & f c = v.
 Proof.
 move=> leab fcont; gen have ivt : f v fcont / f a <= v <= f b ->
     exists2 c, c \in `[a, b] & f c = v; last first.
   case: (leP (f a) (f b)) => [] _ fabv; first exact: ivt.
   have [||c cab /oppr_inj] := ivt (- f) (- v); last by exists c.
-    by move=> x /fcont; apply: continuousN.
+    by move=> x; apply: continuousN; apply: fcont.
   by rewrite ler_oppr opprK ler_oppr opprK andbC.
-move=> /andP[]; rewrite le_eqVlt => /orP [/eqP<- _|ltfav].
-  by exists a => //; rewrite in_itv /= lexx leab.
-rewrite le_eqVlt => /orP [/eqP->|ltvfb].
-  by exists b => //; rewrite in_itv /= lexx leab.
-set A := [set c | (c <= b) && (f c <= v)].
-have An0 : nonempty A by exists a; apply/andP; split=> //; apply: ltW.
-have supA : has_sup A by split=> //; exists b; apply/ubP => ? /andP [].
-have supAab : sup A \in `[a, b].
-  rewrite inE; apply/andP; split; last first.
-    by apply: sup_le_ub => //; apply/ubP => ? /andP [].
-  by move/ubP : (sup_upper_bound supA); apply; rewrite /A/= leab andTb ltW.
-exists (sup A) => //; have lefsupv : f (sup A) <= v.
-  rewrite leNgt; apply/negP => ltvfsup.
-  have vltfsup : 0 < f (sup A) - v by rewrite subr_gt0.
-  have /fcont /(_ _ (nbhsx_ballx _ (PosNum vltfsup))) [_/posnumP[d] supdfe]
-    := supAab.
-  have [t At supd_t] := sup_adherent supA [gt0 of d%:num].
-  suff /supdfe : ball (sup A) d%:num t.
-    rewrite /= /ball /= ltr_norml => /andP [_].
-    by rewrite ltr_add2l ltr_oppr opprK ltNge; have /andP [_ ->] := At.
-  rewrite /= /ball /= ger0_norm.
-    by rewrite ltr_subl_addr -ltr_subl_addl.
-  by rewrite subr_ge0; move/ubP : (sup_upper_bound supA); exact.
-apply/eqP; rewrite eq_le; apply/andP; split=> //.
-rewrite -subr_le0; apply/ler0_addgt0P => _/posnumP[e].
-rewrite ler_subl_addr -ler_subl_addl ltW //.
-have /fcont /(_ _ (nbhsx_ballx _ e)) [_/posnumP[d] supdfe] := supAab.
-have atrF := at_right_proper_filter (sup A); near (at_right (sup A)) => x.
-have /supdfe /= : ball (sup A) d%:num x.
-  by near: x; rewrite /= nbhs_simpl; exists d%:num => //.
-rewrite /= => /ltr_distlC_subl; apply: le_lt_trans.
-rewrite ler_add2r ltW //; suff : forall t, t \in `](sup A), b] -> v < f t.
-  apply; rewrite inE; apply/andP; split; first by near: x; exists 1.
-  near: x; exists (b - sup A) => /=.
-    rewrite subr_gt0 lt_def (itvP supAab) andbT; apply/negP => /eqP besup.
-    by move: lefsupv; rewrite leNgt -besup ltvfb.
-  move=> t lttb ltsupt; move: lttb; rewrite /= distrC.
-  by rewrite gtr0_norm ?subr_gt0 // ltr_add2r; apply: ltW.
-move=> t; rewrite in_itv /=; case/andP => ltsupt letb.
-apply/contra_lt: ltsupt => leftv.
-by move/ubP : (sup_upper_bound supA); apply; rewrite /A/= leftv letb.
-Unshelve. all: by end_near. Qed.
+move=> favfb; suff: (is_interval (f @` `[a,b])).
+  apply; last by exact: favfb. 
+    by exists a => //=; rewrite inE /<=%O /=; apply/andP.
+  by exists b => //=; rewrite inE /<=%O /=; apply/andP.
+apply/connected_intervalP/connected_continuous_connected => //.
+exact: segment_connected.
+Qed.
 
 (** Local properties in [R] *)
 

diff --git a/theories/realfun.v b/theories/realfun.v
@@ -27,6 +27,17 @@ Section real_inverse_functions.
 Variable R : realType.
 Implicit Types (a b : R) (f g : R -> R).
 
+(* TODO: this is a workaround to weaken {in I, continuous f} to use IVT. 
+   Updating this whole file to use {within [set` I], continuous f} is the
+   better, but more labor intensive approach 
+*)
+Lemma continuous_subspace_int ( I : interval R) (f : R -> R) : 
+  {in I, continuous f} -> {within [set` I], continuous f}. 
+Proof.
+move=> ctsf; apply: continuous_subspaceT => x Ix; apply: ctsf.
+by move: Ix; rewrite inE /=.
+Qed.
+
 Lemma itv_continuous_inj_le f (I : interval R) :
   (exists x y, [/\ x \in I, y \in I, x < y & f x <= f y]) ->
   {in I, continuous f} -> {in I &, injective f} ->
@@ -41,6 +52,17 @@ gen have main : f / forall c, {in I, continuous f} -> {in I &, injective f} ->
   move=> c fC fI a b aI bI faLfb aLc cLb.
   have intP := interval_is_interval aI bI.
   have cI : c \in I by rewrite intP// (ltW aLc) ltW.
+  (* TODO: this is a workaround to weaken {in I, continuous f} to use IVT. 
+     Updating this whole file to use {within [set` I], continuous f} is the
+     better, but more labor intensive approach *)
+  have ctsACf : {within `[a,c], continuous f}.
+    apply: continuous_subspaceT => x axc; apply: fC.
+    move:axc; rewrite /= inE /<=%O/= => /andP [? ?].
+    by apply/intP; rewrite (le_trans _ (ltW cLb)) // Bool.andb_true_r.
+  have ctsCBf : {within `[c,b], continuous f}.
+    apply: continuous_subspaceT => x axc; apply: fC.
+    move:axc; rewrite /= inE /<=%O/= => /andP [? ?].
+    by apply/intP; rewrite (le_trans (ltW aLc)).
   have [aLb alb'] : a < b /\ a <= b by rewrite ltW (lt_trans aLc).
   have [faLfc|fcLfa|/eqP faEfc] /= := ltrgtP (f a) (f c).
   - split; rewrite // lt_neqAle fxy // leNgt; apply/negP => fbLfc.
@@ -50,8 +72,6 @@ gen have main : f / forall c, {in I, continuous f} -> {in I &, injective f} ->
       have aLc' : a <= c by rewrite ltW.
       apply: IVT => //; last first.
         by case: ltrgtP faLfc; rewrite // (ltW faLfb) // ltW.
-      apply: sub_in1 fC => y; rewrite in_itv/= le_eqVlt andbC => /andP[yc].
-      by move=> /predU1P[<-//| /ltW L]; rewrite intP// L (le_trans _ (ltW cLb)).
     rewrite -(fI _ _ _ _ fdEfb) //.
     move: ad dc; rewrite le_eqVlt =>/predU1P[<-//| /ltW L] dc.
     by rewrite intP// L (le_trans _ (ltW cLb)).
@@ -60,9 +80,6 @@ gen have main : f / forall c, {in I, continuous f} -> {in I &, injective f} ->
     + have [d /andP[cLd dLb] /eqP] : exists2 d, c <= d <= b & f d = f a.
         have cLb' : c <= b by rewrite ltW.
         apply: IVT => //; last by case: ltrgtP fcLfb; rewrite // !ltW.
-        apply: sub_in1 fC => y; rewrite in_itv /= => /andP[yc].
-        rewrite le_eqVlt=> /predU1P[->//| /ltW L].
-        by rewrite intP// L (le_trans (ltW aLc)).
       have /(fxy f fI) : a < d by rewrite (lt_le_trans aLc).
       suff dI' : d \in I by rewrite eq_sym=> /(_ aI dI') => /negbTE ->.
       move: dLb; rewrite le_eqVlt => /predU1P[->//|/ltW db].
@@ -173,7 +190,7 @@ have lt_ab : a < b by case: (ltgtP a b) aLb faLfb => // ->; rewrite ltxx.
 have w : exists x y, [/\ x \in `[a, b], y \in `[a, b], x < y & f x <= f y].
   by exists a, b; rewrite !bound_itvE (ltW faLfb).
 have fle := itv_continuous_inj_le w ctf (can_in_inj fK).
-move=> x y xin yin; have := IVT aLb ctf.
+move=> x y xin yin; have := IVT aLb (continuous_subspace_int ctf).
 case: (ltrgtP (f a) (f b)) faLfb => // _ _ ivt.
 by have [[u uin <-] [v vin <-]] := (ivt _ xin, ivt _ yin); rewrite !fK// !fle.
 Qed.
@@ -203,7 +220,9 @@ Qed.
 
 Lemma segment_continuous_surjective a b f : a <= b ->
   {in `[a, b], continuous f} -> surjective `[a, b] (f @`[a, b]) f.
-Proof. by move=> le_ab fct y/= /IVT[]// x; exists x. Qed.
+Proof. 
+by move=> le_ab /continuous_subspace_int fct y/= /IVT[]// x; exists x.
+Qed.
 
 Lemma segment_continuous_le_surjective a b f : a <= b -> f a <= f b ->
   {in `[a, b], continuous f} -> surjective `[a, b] `[f a, f b] f.
@@ -482,7 +501,8 @@ move=> Hd.
 wlog xLy : x y / x <= y.
   by move=> H; case: (leP x y) => [/H |/ltW /H].
 rewrite -(subKr (f y) (f x)).
-case: (MVT xLy) => [x1 _ | _ _].
+case: (MVT_closed xLy) => [| _ _].
+  apply/continuous_subspaceT=> ? _.
   by apply/differentiable_continuous/derivable1_diffP.
 by rewrite mul0r => ->; rewrite subr0.
 Qed.