C1 and lipschitz

CHANGELOG_UNRELEASED.md

@@ -81,6 +81,10 @@
 - in `lebesgue_integral.v`:
   + lemmas `integrableP`, `measurable_int`
 
+- in `realfun.v`:
+  + definition `C1`
+  + lemma `C1_lipschitz`
+
 ### Changed
 
 - in `lebesgue_measure.v`

classical/cardinality.v

@@ -2,7 +2,8 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From mathcomp Require Import finset.
-Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import functions.
 
 (******************************************************************************)
 (*                              Cardinality                                   *)

classical/classical_sets.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg matrix finmap order ssrnum.
 From mathcomp Require Import ssrint interval.
-Require Import mathcomp_extra boolp.
+From mathcomp.classical Require Import mathcomp_extra boolp.
 
 (******************************************************************************)
 (* This file develops a basic theory of sets and types equipped with a        *)

classical/fsbigop.v

@@ -1,6 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
-Require Import mathcomp_extra boolp classical_sets functions cardinality.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import functions cardinality.
 
 (******************************************************************************)
 (*                     Finitely-supported big operators                       *)

classical/functions.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From HB Require Import structures.
-Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
 Add Search Blacklist "__canonical__".
 Add Search Blacklist "__functions_".
 Add Search Blacklist "_factory_".

classical/set_interval.v

@@ -1,6 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
-Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import functions.
 From HB Require Import structures.
 
 (******************************************************************************)

theories/itv.v

@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
-From mathcomp Require Import interval mathcomp_extra.
-From mathcomp.classical Require Import boolp.
+From mathcomp Require Import interval.
+From mathcomp.classical Require Import boolp mathcomp_extra.
 Require Import signed.
 
 (******************************************************************************)

theories/probability.v

@@ -1,11 +1,11 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap.
-Require Import mathcomp_extra boolp reals ereal.
 From HB Require Import structures.
-Require Import classical_sets signed functions topology normedtype cardinality.
-Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral.
-Require Import exp.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import functions cardinality.
+Require Import reals ereal signed topology normedtype sequences esum measure.
+Require Import exp numfun lebesgue_measure lebesgue_integral.
 
 (******************************************************************************)
 (*                       Probability (experimental)                           *)

theories/realfun.v

@@ -13,6 +13,8 @@ From HB Require Import structures.
 (*                                                                            *)
 (*   derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and       *)
 (*                                        continuous up to the boundary       *)
+(*                           C1 a b f  == f is a continuously differentiable  *)
+(*                                        function on `[a, b]                 *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -53,6 +55,112 @@ Qed.
 
 End derivable_oo_continuous_bnd.
 
+Section derivable_left_right.
+Context {R : numFieldType} {V W : normedModType R}.
+
+Definition derivable_left (f : V -> W) a v :=
+  cvg ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ 0^'-).
+
+Definition derivable_right (f : V -> W) a v :=
+  cvg ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ 0^'+).
+
+End derivable_left_right.
+
+Section C1.
+Context {R : realType}.
+
+Definition C1 (a b : R) (f : R^o -> R^o) :=
+  [/\ {in `]a, b[, forall x, derivable f x 1},
+      derivable_right f a 1 /\ derivable_left f a 1,
+      f^`() @ a^'+ --> f^`() a /\ f^`() @ b^'- --> f^`() b &
+      {within `[a, b], continuous f^`()} ].
+
+Lemma derivable_right_continuous (a : R) (f : R^o -> R^o) :
+  derivable_right f a 1 -> f^`() @ a^'+ --> f^`() a ->
+  f x @[x --> a^'+] --> f a.
+Proof.
+move=> dfa fa.
+have : f x - f a @[x --> a^'+] --> 0.
+  suff H1 : ((f x - f a) / (x - a)) * (x - a) @[x --> a^'+] --> 0.
+    apply: cvg_trans H1.
+    apply: near_eq_cvg.
+    rewrite near_withinE.
+    near=> t; move=> ta.
+    by rewrite -mulrA mulVf ?mulr1// subr_eq0 gt_eqF.
+  rewrite -[in X in _ --> X](mulr0 (f^`() a)).
+  apply: cvgM.
+    admit. (* ??? *)
+  rewrite -(subrr a).
+  apply: cvg_at_right_filter.
+  apply: cvgB.
+  exact: cvg_id.
+  exact: cvg_cst.
+move/cvg_sub0; apply.
+exact: cvg_cst.
+Admitted.
+
+Lemma derivable_left_continuous (b : R) (f : R^o -> R^o) :
+  derivable_left f b 1 -> f^`() @ b^'- --> f^`() b ->
+  f x @[x --> b^'-] --> f b.
+Proof.
+(* same as above *)
+Admitted.
+
+Lemma C1_lipschitz (a b : R) (f : R^o -> R^o) :
+  C1 a b f -> [lipschitz f x | x in `[a, b]].
+Proof.
+move=> [df [dfa dfb] [cf'a cf'b] cf]; have [|ab] := leP b a.
+  rewrite le_eqVlt => /predU1P[->|ba].
+    by rewrite set_itvE; exact: lipschitz_set1.
+  by rewrite set_itv_ge ?bnd_simp -?ltNge//; exact: lipschitz_set0.
+have : {within `[a, b], continuous (fun x => `|f^`() x|)}.
+  by move=> x; apply: continuous_comp; [exact: cf|exact: norm_continuous].
+move=> /(EVT_max (ltW ab))[c cab dfmax].
+pose M := `|f^`() c|; apply: (@klipschitzW _ _ _ M).
+  apply: (@globally_properfilter _ _ (a, a)); apply inferP.
+  by rewrite /= in_itv /= lexx (ltW ab).
+move=> [x y] /= [xab yab] /=.
+wlog : x y xab yab / x < y.
+  move=> h; have [|] := ltP x y; first exact: (h x y xab yab).
+  rewrite le_eqVlt => /predU1P[->|]; first by rewrite !subrr !normr0 mulr0.
+  by rewrite distrC (distrC x); exact: (h y x yab xab).
+move=> xy.
+have xyabo : `]x, y[ `<=` `]a, b[.
+  move=> d /= dxy; move: dxy xab yab; rewrite !in_itv/=.
+  move=> /andP[xz zy]/andP[ax xb] /andP[ay yb].
+  by rewrite (le_lt_trans ax xz)//= (lt_le_trans zy yb).
+have xydf (z : R) : z \in `]x, y[ -> differentiable f z.
+  move=> zxy; apply/derivable1_diffP/df.
+  exact: xyabo.
+have xyab : `[x, y] `<=` `[a, b].
+  move=> d /= dxy; move: dxy xab yab; rewrite !in_itv/=.
+  move=> /andP[xd dy]/andP[ax xb] /andP[ay yb].
+  by rewrite (le_trans ax xd)//= (le_trans dy yb).
+have: {within `[x, y], continuous f}.
+  have dfxy : {in `]x, y[, forall z : R, derivable f z 1}.
+    by move=> z zxy; apply: df; exact: xyabo.
+  have fx : f @ x^'+ --> f x.
+    move: xab; rewrite in_itv/= 2!le_eqVlt => /andP[/predU1P[ax _|ax]].
+      rewrite -ax.
+      exact: derivable_right_continuous.
+    move=> /predU1P[xb|xb].
+      admit. (* same as above *)
+    apply: cvg_at_right_filter.
+    apply: differentiable_continuous.
+    apply/derivable1_diffP.
+    apply: df.
+    by rewrite in_itv/= ax.
+  have fy : f @ y^'- --> f y.
+    admit. (* same as above *)
+  have /continuous_subspaceW := derivable_oo_continuous_bnd_within (And3 dfxy fx fy).
+  exact.
+move=> /(MVT xy (fun z h => derivableP (diff_derivable (xydf z h))))[d dxy mvt].
+rewrite distrC {}mvt -derive1E normrM (distrC y) ler_pmul//.
+exact/dfmax/xyab/subset_itv_oo_cc.
+Admitted.
+
+End C1.
+
 Section real_inverse_functions.
 Variable R : realType.
 Implicit Types (a b : R) (f g : R -> R).