fixes #1734 (#1747)

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -357,6 +357,13 @@
 - in `sequences.v`:
   + `adjacent` -> `adjacent_seq`
 
+- in `realfun.v`:
+  + `derivable_oo_continuous_bnd` -> `derivable_oo_LRcontinuous`
+  + `derivable_oo_continuous_bnd_within` -> `derivable_oo_LRcontinuous_within`
+  + `derivable_Nyo_continuous_bnd` -> `derivable_Nyo_Lcontinuous`
+  + `derivable_oy_continuous_bnd` -> `derivable_oy_Rcontinuous`
+  + `derivable_oy_continuous_within_itvcy` -> `derivable_oy_Rcontinuous_within_itvcy`
+
 ### Generalized
 
 - in `pseudometric_normed_Zmodule.v`:

theories/convex.v

@@ -281,7 +281,7 @@ have [c2 Ic2 Hc2] : exists2 c2, x < c2 < b & (f b - f x) / (b - x) = 'D_1 f c2.
   have derivef z : z \in `]x, b[ -> is_derive z 1 f ('D_1 f z).
     by move=> zxb; apply/derivableP/xbf; exact: zxb.
   have [|z zxb fbfx] := MVT xb derivef.
-    apply/(derivable_oo_continuous_bnd_within (And3 xbf _ cvg_left)).
+    apply/(derivable_oo_LRcontinuous_within (And3 xbf _ cvg_left)).
     apply/cvg_at_right_filter.
     have := derivable_within_continuous HDf.
     rewrite continuous_open_subspace//.
@@ -293,7 +293,7 @@ have [c1 Ic1 Hc1] : exists2 c1, a < c1 < x & (f x - f a) / (x - a) = 'D_1 f c1.
   have derivef z : z \in `]a, x[ -> is_derive z 1 f ('D_1 f z).
     by move=> zax; apply /derivableP/axf.
   have [|z zax fxfa] := MVT ax derivef.
-    apply/(derivable_oo_continuous_bnd_within (And3 axf cvg_right _)).
+    apply/(derivable_oo_LRcontinuous_within (And3 axf cvg_right _)).
     apply/cvg_at_left_filter.
     have := derivable_within_continuous HDf.
     rewrite continuous_open_subspace//.
@@ -311,7 +311,7 @@ have [d Id h] :
   have derivef z : z \in `]c1, c2[ -> is_derive z 1 Df ('D_1 Df z).
     by move=> zc1c2; apply/derivableP/h.
   have [|z zc1c2 {}h] := MVT c1c2 derivef.
-    apply: (derivable_oo_continuous_bnd_within (And3 h _ _)).
+    apply: (derivable_oo_LRcontinuous_within (And3 h _ _)).
     + apply: cvg_at_right_filter.
       move: cDf; rewrite continuous_open_subspace//.
       by apply; rewrite inE/= in_itv/= (andP Ic1).1 (lt_trans _ (andP Ic2).2).

theories/ftc.v

@@ -544,7 +544,7 @@ Qed.
 
 Corollary continuous_FTC2 f F a b : (a < b)%R ->
   {within `[a, b], continuous f} ->
-  derivable_oo_continuous_bnd F a b ->
+  derivable_oo_LRcontinuous F a b ->
   {in `]a, b[, F^`() =1 f} ->
   (\int[mu]_(x in `[a, b]) (f x)%:E = (F b)%:E - (F a)%:E)%E.
 Proof.
@@ -791,10 +791,10 @@ Implicit Types (F G f g : R -> R) (a b : R).
 
 Lemma integration_by_parts F G f g a b : (a < b)%R ->
     {within `[a, b], continuous f} ->
-    derivable_oo_continuous_bnd F a b ->
+    derivable_oo_LRcontinuous F a b ->
     {in `]a, b[, F^`() =1 f} ->
     {within `[a, b], continuous g} ->
-    derivable_oo_continuous_bnd G a b ->
+    derivable_oo_LRcontinuous G a b ->
     {in `]a, b[, G^`() =1 g} ->
   \int[mu]_(x in `[a, b]) (F x * g x)%:E = (F b * G b - F a * G a)%:E -
   \int[mu]_(x in `[a, b]) (f x * G x)%:E.
@@ -804,13 +804,13 @@ have cfg : {within `[a, b], continuous (f * G + F * g)%R}.
   apply/subspace_continuousP => x abx; apply: cvgD.
   - apply: cvgM.
     + by move/subspace_continuousP : cf; exact.
-    + have := derivable_oo_continuous_bnd_within Gab.
+    + have := derivable_oo_LRcontinuous_within Gab.
       by move/subspace_continuousP; exact.
   - apply: cvgM.
-    + have := derivable_oo_continuous_bnd_within Fab.
+    + have := derivable_oo_LRcontinuous_within Fab.
       by move/subspace_continuousP; exact.
     + by move/subspace_continuousP : cg; exact.
-have FGab : derivable_oo_continuous_bnd (F * G)%R a b.
+have FGab : derivable_oo_LRcontinuous (F * G)%R a b.
   move: Fab Gab => /= [abF FFa FFb] [abG GGa GGb];split; [|exact:cvgM..].
   by move=> z zab; apply: derivableM; [exact: abF|exact: abG].
 have FGfg : {in `]a, b[, (F * G)^`() =1 f * G + F * g}%R.
@@ -823,13 +823,13 @@ have ? : mu.-integrable `[a, b] (fun x => ((f * G) x)%:E).
   apply: continuous_compact_integrable => //; first exact: segment_compact.
   apply/subspace_continuousP => x abx; apply: cvgM.
   + by move/subspace_continuousP : cf; exact.
-  + have := derivable_oo_continuous_bnd_within Gab.
+  + have := derivable_oo_LRcontinuous_within Gab.
     by move/subspace_continuousP; exact.
 rewrite /= integralD//=.
 - by rewrite addeAC subee ?add0e// integrable_fin_num.
 - apply: continuous_compact_integrable => //; first exact: segment_compact.
   apply/subspace_continuousP => x abx;apply: cvgM.
-  + have := derivable_oo_continuous_bnd_within Fab.
+  + have := derivable_oo_LRcontinuous_within Fab.
     by move/subspace_continuousP; exact.
   + by move/subspace_continuousP : cg; exact.
 Qed.
@@ -844,10 +844,10 @@ Implicit Types (F G f g : R -> R) (a b : R).
 Lemma Rintegration_by_parts F G f g a b :
     (a < b)%R ->
     {within `[a, b], continuous f} ->
-    derivable_oo_continuous_bnd F a b ->
+    derivable_oo_LRcontinuous F a b ->
     {in `]a, b[, F^`() =1 f} ->
     {within `[a, b], continuous g} ->
-    derivable_oo_continuous_bnd G a b ->
+    derivable_oo_LRcontinuous G a b ->
     {in `]a, b[, G^`() =1 g} ->
   \int[mu]_(x in `[a, b]) (F x * g x) = (F b * G b - F a * G a) -
   \int[mu]_(x in `[a, b]) (f x * G x).
@@ -861,7 +861,7 @@ suff: mu.-integrable `[a, b] (fun x => (f x * G x)%:E).
 apply: continuous_compact_integrable.
   exact: segment_compact.
 move=> /= z; apply: continuousM; [exact: cf|].
-exact: (derivable_oo_continuous_bnd_within Gab).
+exact: (derivable_oo_LRcontinuous_within Gab).
 Qed.
 
 End Rintegration_by_parts.
@@ -1054,13 +1054,13 @@ Lemma integration_by_substitution_decreasing F G a b : (a < b)%R ->
   {in `]a, b[, continuous F^`()} ->
   cvg (F^`() x @[x --> a^'+]) ->
   cvg (F^`() x @[x --> b^'-]) ->
-  derivable_oo_continuous_bnd F a b ->
+  derivable_oo_LRcontinuous F a b ->
   {within `[F b, F a], continuous G} ->
   \int[mu]_(x in `[F b, F a]) (G x)%:E =
   \int[mu]_(x in `[a, b]) (((G \o F) * - F^`()) x)%:E.
 Proof.
 move=> ab decrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] Fab cG.
-have cF := derivable_oo_continuous_bnd_within Fab.
+have cF := derivable_oo_LRcontinuous_within Fab.
 have FbFa : (F b < F a)%R by apply: decrF; rewrite //= in_itv/= (ltW ab) lexx.
 have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R.
   apply: measurable_funM.
@@ -1077,7 +1077,7 @@ have {}mGFF' : measurable_fun `[a, b] ((G \o F) * F^`())%R.
 have intG : mu.-integrable `[F b, F a] (EFin \o G).
   by apply: continuous_compact_integrable => //; exact: segment_compact.
 pose PG x := parameterized_integral mu (F b) x G.
-have PGFbFa : derivable_oo_continuous_bnd PG (F b) (F a).
+have PGFbFa : derivable_oo_LRcontinuous PG (F b) (F a).
   have [/= dF rF lF] := Fab; split => /=.
   - move=> x xFbFa /=.
     have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[].
@@ -1147,7 +1147,7 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first.
     apply: cvgN; apply: cvg_trans F'bl; apply: near_eq_cvg.
     by near=> z; rewrite fE// in_itv/=; apply/andP; split.
 - have [/= dF rF lF] := Fab.
-  have := derivable_oo_continuous_bnd_within PGFbFa.
+  have := derivable_oo_LRcontinuous_within PGFbFa.
   move=> /(continuous_within_itvP _ FbFa)[_ PGFb PGFa]; split => /=.
   - move=> x xab; apply/derivable1_diffP; apply: differentiable_comp => //.
     apply: differentiable_comp; apply/derivable1_diffP.
@@ -1205,7 +1205,7 @@ Lemma integration_by_substitution_increasing F G a b : (a < b)%R ->
   {in `]a, b[, continuous F^`()} ->
   cvg (F^`() x @[x --> a^'+]) ->
   cvg (F^`() x @[x --> b^'-]) ->
-  derivable_oo_continuous_bnd F a b ->
+  derivable_oo_LRcontinuous F a b ->
   {within `[F a, F b], continuous G} ->
   \int[mu]_(x in `[F a, F b]) (G x)%:E =
   \int[mu]_(x in `[a, b]) (((G \o F) * F^`()) x)%:E.
@@ -1275,7 +1275,7 @@ Lemma decreasing_ge0_integration_by_substitutiony F G a :
   {in `]a, +oo[, continuous F^`()} ->
   cvg (F^`() x @[x --> a^'+]) ->
   cvg (F^`() x @[x --> +oo%R]) ->
-  derivable_oy_continuous_bnd F a -> F x @[x --> +oo%R] --> -oo%R ->
+  derivable_oy_Rcontinuous F a -> F x @[x --> +oo%R] --> -oo%R ->
   {within `]-oo, F a], continuous G} ->
   {in `]-oo, F a[, forall x, (0 <= G x)%R} ->
   \int[mu]_(x in `]-oo, F a]) (G x)%:E =
@@ -1452,7 +1452,7 @@ Lemma increasing_ge0_integration_by_substitutiony F G a :
   {in `]a, +oo[, continuous F^`()} ->
   cvg (F^`() x @[x --> a^'+]) ->
   cvg (F^`() x @[x --> +oo%R]) ->
-  derivable_oy_continuous_bnd F a -> F x @[x --> +oo%R] --> +oo%R->
+  derivable_oy_Rcontinuous F a -> F x @[x --> +oo%R] --> +oo%R->
   {within `[F a, +oo[, continuous G} ->
   {in `]F a, +oo[, forall x, (0 <= G x)%R} ->
   \int[mu]_(x in `[F a, +oo[) (G x)%:E =
@@ -1551,7 +1551,7 @@ Lemma increasing_ge0_integration_by_substitutionNy F G b :
   {in `]-oo, b[, continuous F^`()} ->
   cvg (F^`() x @[x --> -oo%R]) ->
   F^`() x @[x --> b^'-] --> F^`() b (* TODO: try with cvg (F^`() x @[x --> b^'-]) *) ->
-  derivable_Nyo_continuous_bnd F b -> F x @[x --> -oo%R] --> -oo%R->
+  derivable_Nyo_Lcontinuous F b -> F x @[x --> -oo%R] --> -oo%R->
   {within `]-oo, F b], continuous G} ->
   {in `]-oo, F b[, forall x, (0 <= G x)%R} ->
   \int[mu]_(x in `]-oo, F b]) (G x)%:E =

theories/realfun.v

@@ -21,12 +21,12 @@ From mathcomp Require Import normedtype derive sequences real_interval.
 (*         increasing_fun f == the function f is (strictly) increasing        *)
 (*         decreasing_fun f == the function f is (strictly) decreasing        *)
 (*                                                                            *)
-(*   derivable_oo_continuous_bnd f x y == f is derivable in `]x, y[ and       *)
+(*     derivable_oo_LRcontinuous f x y == f is derivable in `]x, y[ and       *)
 (*                             continuous up to the boundary, i.e.,           *)
 (*                             f @ x^'+ --> f x  and  f @ y^'- --> f y        *)
-(*     derivable_oy_continuous_bnd f x == f is derivable in `]x, +oo[ and     *)
+(*        derivable_oy_Rcontinuous f x == f is derivable in `]x, +oo[ and     *)
 (*                             f @ x^'+ --> f x                               *)
-(*    derivable_Nyo_continuous_bnd f x == f is derivable in `]-oo, x[ and     *)
+(*       derivable_Nyo_Lcontinuous f x == f is derivable in `]-oo, x[ and     *)
 (*                             f @ x^'- --> f x                               *)
 (*                                                                            *)
 (*      itv_partition a b s == s is a partition of the interval `[a, b]       *)
@@ -1163,15 +1163,15 @@ End lime_sup_inf.
 #[deprecated(since="mathcomp-analysis 1.3.0", note="use `limf_esup_ge0` instead")]
 Notation lime_sup_ge0 := __deprecated__lime_sup_ge0 (only parsing).
 
-Section derivable_oo_continuous_bnd.
+Section derivable_oo_LRcontinuous.
 Context {R : numFieldType} {V : normedModType R}.
 
-Definition derivable_oo_continuous_bnd (f : R -> V) (x y : R) :=
+Definition derivable_oo_LRcontinuous (f : R -> V) (x y : R) :=
   [/\ {in `]x, y[, forall x, derivable f x 1},
       f @ x^'+ --> f x & f @ y^'- --> f y].
 
-Lemma derivable_oo_continuous_bnd_within (f : R -> V) (x y : R) :
-  derivable_oo_continuous_bnd f x y -> {within `[x, y], continuous f}.
+Lemma derivable_oo_LRcontinuous_within (f : R -> V) (x y : R) :
+  derivable_oo_LRcontinuous f x y -> {within `[x, y], continuous f}.
 Proof.
 move=> [fxy fxr fyl]; apply/subspace_continuousP => z /=.
 rewrite in_itv/= => /andP[]; rewrite le_eqVlt => /predU1P[<-{z} xy|].
@@ -1186,14 +1186,14 @@ apply/differentiable_continuous; rewrite -derivable1_diffP.
 by apply: fxy; rewrite in_itv/= xz zy.
 Qed.
 
-Definition derivable_Nyo_continuous_bnd (f : R -> V) (x : R) :=
+Definition derivable_Nyo_Lcontinuous (f : R -> V) (x : R) :=
   {in `]-oo, x[, forall x, derivable f x 1} /\ f @ x^'- --> f x.
 
-Definition derivable_oy_continuous_bnd (f : R -> V) (x : R) :=
+Definition derivable_oy_Rcontinuous (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}.
+Lemma derivable_oy_Rcontinuous_within_itvcy (f : R -> V) (x : R) :
+  derivable_oy_Rcontinuous f x -> {within `[x, +oo[, continuous f}.
 Proof.
 move=> [df cfx]; apply/subspace_continuousP => z /=.
 rewrite in_itv/= => /andP[]; rewrite le_eqVlt => /predU1P[<-{z} _|].
@@ -1204,8 +1204,8 @@ apply/differentiable_continuous; rewrite -derivable1_diffP.
 by apply: df; rewrite in_itv/= xz.
 Qed.
 
-Lemma derivable_Noy_continuous_within_itvNyc (f : R -> V) (x : R) :
-  derivable_Nyo_continuous_bnd f x -> {within `]-oo, x], continuous f}.
+Lemma derivable_Noy_Lcontinuous_within_itvNyc (f : R -> V) (x : R) :
+  derivable_Nyo_Lcontinuous f x -> {within `]-oo, x], continuous f}.
 Proof.
 move=> [df cfx]; apply/subspace_continuousP => z /=.
 rewrite in_itv/=; rewrite le_eqVlt => /predU1P[->{z}|].
@@ -1216,16 +1216,28 @@ apply/differentiable_continuous; rewrite -derivable1_diffP.
 by apply: df; rewrite in_itv.
 Qed.
 
-End derivable_oo_continuous_bnd.
+End derivable_oo_LRcontinuous.
+(*#[deprecated(since="mathcomp-analysis 1.14.0", note="use `derivable_oo_LRcontinuous` instead")]
+Notation derivable_oo_continuous_bnd := derivable_oo_LRcontinuous (only parsing).
+#[deprecated(since="mathcomp-analysis 1.14.0", note="use `derivable_oo_LRcontinuous_within` instead")]
+Notation derivable_oo_continuous_bnd_within := derivable_oo_LRcontinuous_within (only parsing).
+#[deprecated(since="mathcomp-analysis 1.14.0", note="use `derivable_Nyo_Lcontinuous` instead")]
+Notation derivable_Nyo_continuous_bnd := derivable_Nyo_Lcontinuous (only parsing).
+#[deprecated(since="mathcomp-analysis 1.14.0", note="use `derivable_oy_Rcontinuous` instead")]
+Notation derivable_oy_continuous_bnd := derivable_oy_Rcontinuous (only parsing).
+#[deprecated(since="mathcomp-analysis 1.14.0", note="use `derivable_oy_Rcontinuous_within_itvcy` instead")]
+Notation derivable_oy_continuous_within_itvcy := derivable_oy_Rcontinuous_within_itvcy (only parsing).
+#[deprecated(since="mathcomp-analysis 1.14.0", note="use `derivable_Noy_Lcontinuous_within_itvNyc` instead")]
+Notation derivable_Noy_continuous_within_itvNyc := derivable_Noy_Lcontinuous_within_itvNyc (only parsing).*)
 
 Section derivable_oo_continuousW.
 Context {R : realFieldType} {V : normedModType R}.
 
 Lemma derivable_oo_continuousW (a b c d : R) (f : R -> V) :
   c < d ->
   `[c, d] `<=` `[a, b] ->
-  derivable_oo_continuous_bnd f a b ->
-  derivable_oo_continuous_bnd f c d.
+  derivable_oo_LRcontinuous f a b ->
+  derivable_oo_LRcontinuous f c d.
 Proof.
 move=> cd cdab [/[dup]df + fa fb].
 have /andP[ac db] : (a <= c) && (d <= b).
@@ -1247,8 +1259,8 @@ Qed.
 Lemma derivable_oy_continuousWoo (a c d : R) (f : R -> V) :
   c < d ->
   a <= c ->
-  derivable_oy_continuous_bnd f a ->
-  derivable_oo_continuous_bnd f c d.
+  derivable_oy_Rcontinuous f a ->
+  derivable_oo_LRcontinuous f c d.
 Proof.
 move=> cd ac [df fa]; split.
 - by apply: in1_subset_itv df; exact: subset_itv.
@@ -1265,8 +1277,8 @@ Qed.
 
 Lemma derivable_oy_continuousW (a c : R) (f : R -> V) :
   a <= c ->
-  derivable_oy_continuous_bnd f a ->
-  derivable_oy_continuous_bnd f c.
+  derivable_oy_Rcontinuous f a ->
+  derivable_oy_Rcontinuous f c.
 Proof.
 move=> ac [df fa]; split.
 - by apply: in1_subset_itv df; exact: subset_itv.
@@ -1280,8 +1292,8 @@ Qed.
 Lemma derivable_Nyo_continuousWoo (b c d : R) (f : R -> V) :
   c < d ->
   d <= b ->
-  derivable_Nyo_continuous_bnd f b ->
-  derivable_oo_continuous_bnd f c d.
+  derivable_Nyo_Lcontinuous f b ->
+  derivable_oo_LRcontinuous f c d.
 Proof.
 move=> cd db [df fa]; split.
 - by apply: in1_subset_itv df; exact: subset_itv.
@@ -1298,8 +1310,8 @@ Qed.
 
 Lemma derivable_Nyo_continuousW (b d : R) (f : R -> V) :
   d <= b ->
-  derivable_Nyo_continuous_bnd f b ->
-  derivable_Nyo_continuous_bnd f d.
+  derivable_Nyo_Lcontinuous f b ->
+  derivable_Nyo_Lcontinuous f d.
 Proof.
 move=> db [df fa]; split.
 - by apply: in1_subset_itv df; exact: subset_itv.