add lemmas for derivable_oo/Nyo/oy_continuous_bnd

CHANGELOG_UNRELEASED.md

@@ -172,6 +172,15 @@
 - in `constructive_ereal.v`:
   + lemmas `div1e`, `divee`, `inve_eq1`, `Nyconjugate`
 
+- in `realfun.v`:
+  + lemmas `derivable_oy_continuous_within_itvcy`,
+           `derivable_oy_continuous_within_itvNyc`,
+  + lemmas `derivable_oo_continuous_bndW`,
+           `derivable_oy_continuous_bndW_oo`,
+           `derivable_oy_continuous_bndW`,
+           `derivable_Nyo_continuous_bndW_oo`,
+           `derivable_Nyo_continuous_bndW`
+
 ### Changed
 
 - in `measure.v`:

theories/realfun.v

@@ -1188,8 +1188,134 @@ Definition derivable_Nyo_continuous_bnd (f : R -> V) (x : R) :=
 Definition derivable_oy_continuous_bnd (f : R -> V) (x : R) :=
   {in `]x, +oo[, forall x, derivable f x 1} /\ f @ x^'+ --> f x.
 
+Lemma derivable_oy_continuous_within_itvcy (f : R -> V) (x : R) :
+  derivable_oy_continuous_bnd f x -> {within `[x, +oo[, continuous f}.
+Proof.
+move=> [df cfx].
+apply/subspace_continuousP => z /=.
+rewrite in_itv/= => /andP[]; rewrite le_eqVlt => /predU1P[<-{z} _|].
+  have := cvg_at_right_within cfx; apply: cvg_trans; apply: cvg_app.
+  by apply: within_subset => z/=; rewrite in_itv/= => /andP[].
+move=> xz _.
+apply: cvg_within_filter.
+apply/differentiable_continuous; rewrite -derivable1_diffP.
+by apply: df; rewrite in_itv/= xz.
+Qed.
+
+Lemma derivable_oy_continuous_within_itvNyc (f : R -> V) (x : R) :
+  derivable_Nyo_continuous_bnd f x -> {within `]-oo, x], continuous f}.
+Proof.
+move=> [df cfx].
+apply/subspace_continuousP => z /=.
+rewrite in_itv/=; rewrite le_eqVlt => /predU1P[->{z}|].
+  have := cvg_at_left_within cfx; apply: cvg_trans; apply: cvg_app.
+  by apply: within_subset => z/=; rewrite in_itv/=.
+move=> cx.
+apply: cvg_within_filter.
+apply/differentiable_continuous; rewrite -derivable1_diffP.
+by apply: df; rewrite in_itv/=.
+Qed.
+
 End derivable_oo_continuous_bnd.
 
+Section derivable_oo_continuous_bndW.
+Context {R : realFieldType} {V : normedModType R}.
+
+Lemma derivable_oo_continuous_bndW (a b c d : R) (f : R -> V) :
+  (c < d) ->
+  (a <= c) -> (d <= b) ->
+  derivable_oo_continuous_bnd f a b ->
+  derivable_oo_continuous_bnd f c d.
+Proof.
+move=> cd ac db [/[dup]df + fa fb].
+move/derivable_within_continuous; rewrite continuous_open_subspace// => cf.
+split.
+- apply: in1_subset_itv df.
+  exact: subset_itvW.
+- move: ac; rewrite le_eqVlt => /predU1P[<- //|ac].
+  apply: cvg_at_right_filter.
+  by apply: cf; rewrite inE/= in_itv/= ac/= (lt_le_trans cd db).
+- move: db; rewrite le_eqVlt => /predU1P[-> //|db].
+  apply: cvg_at_left_filter.
+  by apply cf; rewrite inE/= in_itv/= db andbT (le_lt_trans ac cd).
+Qed.
+
+Lemma derivable_oy_continuous_bndW_oo (a c d : R) (f : R -> V) :
+  (c < d) ->
+  (a <= c) ->
+  derivable_oy_continuous_bnd f a ->
+  derivable_oo_continuous_bnd f c d.
+Proof.
+move=> cd ac[df fa].
+split => //.
+- apply: in1_subset_itv df.
+  exact: subset_itv.
+- move: ac; rewrite le_eqVlt => /predU1P[<-//|ac].
+  apply: cvg_at_right_filter.
+  have := derivable_within_continuous df.
+  rewrite continuous_open_subspace//; apply.
+  by rewrite inE/= in_itv/= ac.
+- apply: cvg_at_left_filter.
+  have := derivable_within_continuous df.
+  rewrite continuous_open_subspace//; apply.
+  by rewrite inE/= in_itv/= (le_lt_trans ac cd).
+Qed.
+
+Lemma derivable_oy_continuous_bndW (a c : R) (f : R -> V) :
+  (a <= c) ->
+  derivable_oy_continuous_bnd f a ->
+  derivable_oy_continuous_bnd f c.
+Proof.
+move=> ac[df fa].
+split => //.
+- apply: in1_subset_itv df.
+  exact: subset_itv.
+- move: ac; rewrite le_eqVlt => /predU1P[<- //|ac].
+  apply: cvg_at_right_filter.
+  have := derivable_within_continuous df.
+  rewrite continuous_open_subspace//; apply.
+  by rewrite inE/= in_itv/= ac.
+Qed.
+
+Lemma derivable_Nyo_continuous_bndW_oo (b c d : R) (f : R -> V) :
+  (c < d) ->
+  (d <= b) ->
+  derivable_Nyo_continuous_bnd f b ->
+  derivable_oo_continuous_bnd f c d.
+Proof.
+move=> cd db [df fa].
+split => //.
+- apply: in1_subset_itv df.
+  exact: subset_itv.
+- apply: cvg_at_right_filter.
+  have := derivable_within_continuous df.
+  rewrite continuous_open_subspace//; apply.
+  by rewrite inE/= in_itv/= (lt_le_trans cd db).
+- move: db; rewrite le_eqVlt => /predU1P[-> //|db].
+  apply: cvg_at_left_filter.
+  have := derivable_within_continuous df.
+  rewrite continuous_open_subspace//; apply.
+  by rewrite inE/= in_itv/=.
+Qed.
+
+Lemma derivable_Nyo_continuous_bndW (b d : R) (f : R -> V) :
+  (d <= b) ->
+  derivable_Nyo_continuous_bnd f b ->
+  derivable_Nyo_continuous_bnd f d.
+Proof.
+move=> db [df fa].
+split => //.
+- apply: in1_subset_itv df.
+  exact: subset_itv.
+- move: db; rewrite le_eqVlt => /predU1P[-> //|db].
+  apply: cvg_at_left_filter.
+  have := derivable_within_continuous df.
+  rewrite continuous_open_subspace//; apply.
+  by rewrite inE/= in_itv/=.
+Qed.
+
+End derivable_oo_continuous_bndW.
+
 Section real_inverse_functions.
 Variable R : realType.
 Implicit Types (a b : R) (f g : R -> R).