Convex exp (#873)

* Introduce convex

- introduce convex spaces
- proof of second_derivative_convex_pt
- using `{i01 R}`
- expR convex

Co-authored-by: Reynald Affeldt <[email protected]>
Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: Takafumi Saikawa <[email protected]>
Co-authored-by: zstone1 <[email protected]>
Co-authored-by: Yoshihiro Imai <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -130,6 +130,25 @@
     `discrete_pseudoMetricType`, and `pseudoMetric_bool`.
   + new lemmas `finite_compact`, `discrete_ball_center`, `compact_cauchy_cvg`
 
+- in `set_interval.v`:
+  + lemma `onem_factor`
+- in `set_interval.v`:
+  + lemmas `in1_subset_itv`, `subset_itvW`
+- in `normedtype.v`:
+  + lemmas `cvg_at_right_filter`, `cvg_at_left_filter`,
+    `cvg_at_right_within`, `cvg_at_left_within`
+- in `derive.v`:
+  + lemma `derivable_within_continuous`
+- in `realfun.v`:
+  + definition `derivable_oo_continuous_bnd`, lemma `derivable_oo_continuous_bnd_within`
+- in `exp.v`:
+  + lemmas `derive_expR`, `convex_expR`
+- new file `convex.v`:
+  + mixin `isConvexSpace`, structure `ConvexSpace`, notations `convType`,
+    `_ <| _ |> _`
+  + lemmas `conv1`, `second_derivative_convex`
+
+
 ### Changed
 
 - in `mathcomp_extra.v`

_CoqProject

@@ -40,6 +40,7 @@ theories/probability.v
 theories/summability.v
 theories/signed.v
 theories/itv.v
+theories/convex.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v

classical/set_interval.v

@@ -50,6 +50,21 @@ Qed.
 Lemma subset_itvP i j : {subset i <= j} <-> [set` i] `<=` [set` j].
 Proof. by []. Qed.
 
+Lemma in1_subset_itv (P : T -> Prop) i j :
+  [set` j] `<=` [set` i] -> {in i, forall x, P x} -> {in j, forall x, P x}.
+Proof. by move=> /subset_itvP ji iP z zB; apply: iP; exact: ji. Qed.
+
+Lemma subset_itvW x y z u b0 b1 :
+    (x <= y)%O -> (z <= u)%O ->
+  `]y, z[ `<=` [set` Interval (BSide b0 x) (BSide b1 u)].
+Proof.
+move=> xy zu; apply: (@subset_trans _ `]x, u[%classic).
+  move=> x0/=; rewrite 2!in_itv/= => /andP[].
+  by move=> /(le_lt_trans xy) ->/= /lt_le_trans; exact.
+by move: b0 b1 => [] [] /=; [exact: subset_itv_oo_co|exact: subset_itv_oo_cc|
+  exact: subset_refl|exact: subset_itv_oo_oc].
+Qed.
+
 Lemma set_itvoo x y : `]x, y[%classic = [set z | (x < z < y)%O].
 Proof. by []. Qed.
 
@@ -488,6 +503,12 @@ Lemma range_factor ba bb a b : a < b ->
                  [set` Interval (BSide ba 0) (BSide bb 1)].
 Proof. by move=> /(factor_itv_bij ba bb)/Pbij[f ->]; rewrite image_eq. Qed.
 
+Lemma onem_factor a b x : a != b -> `1-(factor a b x) = factor b a x.
+Proof.
+rewrite eq_sym -subr_eq0 => ab; rewrite /onem /factor -(divff ab) -mulrBl.
+by rewrite opprB addrA subrK -mulrNN opprB -invrN opprB.
+Qed.
+
 End line_path_factor_numFieldType.
 
 Lemma mem_factor_itv (R : realFieldType) ba bb (a b : R) :

theories/Make

@@ -30,6 +30,8 @@ numfun.v
 lebesgue_integral.v
 summability.v
 signed.v
+itv.v
+convex.v
 altreals/xfinmap.v
 altreals/discrete.v
 altreals/realseq.v

theories/convex.v

@@ -0,0 +1,248 @@
+(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
+From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
+From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
+From mathcomp.classical Require Import boolp classical_sets set_interval.
+From mathcomp.classical Require Import functions cardinality mathcomp_extra.
+Require Import ereal reals signed topology prodnormedzmodule.
+Require Import normedtype derive realfun itv.
+From HB Require Import structures.
+
+(******************************************************************************)
+(*                                Convexity                                   *)
+(*                                                                            *)
+(* This file provides a small account of convexity using convex spaces, to be *)
+(* completed with material from infotheo.                                     *)
+(*                                                                            *)
+(*   isConvexSpace R T == interface for convex spaces                         *)
+(*       ConvexSpace R == structure of convex space                           *)
+(*         a <| t |> b == convexity operator                                  *)
+(* E : lmodType R with R : realDomainType and R : realDomainType are shown to *)
+(* be convex spaces                                                           *)
+(*                                                                            *)
+(******************************************************************************)
+
+Reserved Notation "x <| p |> y" (format "x  <| p |>  y", at level 49).
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+Import numFieldTopology.Exports.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+
+Import numFieldNormedType.Exports.
+
+Declare Scope convex_scope.
+Local Open Scope convex_scope.
+
+HB.mixin Record isConvexSpace (R : realDomainType) (T : Type) := {
+  convexspacechoiceclass : Choice.class_of T ;
+  conv : {i01 R} -> T -> T -> T ;
+  conv0 : forall a b, conv 0%:i01 a b = a ;
+  convmm : forall (p : {i01 R}) a, conv p a a = a ;
+  convC : forall (p : {i01 R}) a b, conv p a b = conv (1 - p%:inum)%:i01 b a;
+  convA : forall (p q r : {i01 R}) (a b c : T),
+    p%:inum * (`1-(q%:inum)) = (`1-(p%:inum * q%:inum)) * r%:inum ->
+    conv p a (conv q b c) = conv (p%:inum * q%:inum)%:i01 (conv r a b) c
+}.
+
+#[short(type=convType)]
+HB.structure Definition ConvexSpace (R : realDomainType) :=
+  {T of isConvexSpace R T }.
+
+Canonical conv_eqType (R : realDomainType) (T : convType R) :=
+  Eval hnf in EqType (ConvexSpace.sort T) convexspacechoiceclass.
+Canonical conv_choiceType (R : realDomainType) (T : convType R) :=
+  Eval hnf in ChoiceType (ConvexSpace.sort T) convexspacechoiceclass.
+Coercion conv_choiceType : convType >-> choiceType.
+
+Notation "a <| p |> b" := (conv p a b) : convex_scope.
+
+Section convex_space_lemmas.
+Context R (A : convType R).
+Implicit Types a b : A.
+
+Lemma conv1 a b : a <| 1%:i01 |> b = b.
+Proof.
+rewrite convC/= [X in _ <| X |> _](_ : _ = 0%:i01) ?conv0//.
+by apply/val_inj => /=; rewrite subrr.
+Qed.
+
+End convex_space_lemmas.
+
+Local Open Scope convex_scope.
+
+Section lmodType_convex_space.
+Context {R : realDomainType} {E : lmodType R}.
+Implicit Type p q r : {i01 R}.
+
+Let avg p (a b : E) := `1-(p%:inum) *: a + p%:inum *: b.
+
+Let avg0 a b : avg 0%:i01 a b = a.
+Proof. by rewrite /avg/= onem0 scale0r scale1r addr0. Qed.
+
+Let avgI p x : avg p x x = x.
+Proof. by rewrite /avg -scalerDl/= addrC add_onemK scale1r. Qed.
+
+Let avgC p x y : avg p x y = avg (1 - (p%:inum))%:i01 y x.
+Proof. by rewrite /avg onemK addrC. Qed.
+
+Let avgA p q r (a b c : E) :
+  p%:inum * (`1-(q%:inum)) = (`1-(p%:inum * q%:inum)) * r%:inum ->
+  avg p a (avg q b c) = avg (p%:inum * q%:inum)%:i01 (avg r a b) c.
+Proof.
+move=> pq; rewrite /avg.
+rewrite [in LHS]scalerDr [in LHS]addrA [in RHS]scalerDr; congr (_ + _ + _).
+- rewrite scalerA; congr (_ *: _) => /=.
+  by rewrite mulrDr mulr1 mulrN -pq mulrBr mulr1 opprB addrA subrK.
+- by rewrite 2!scalerA; congr (_ *: _).
+- by rewrite scalerA.
+Qed.
+
+HB.instance Definition _ :=
+  @isConvexSpace.Build R E (Choice.class _) avg avg0 avgI avgC avgA.
+
+End lmodType_convex_space.
+
+Section realDomainType_convex_space.
+Context {R : realDomainType}.
+Implicit Types p q : {i01 R}.
+
+Let avg p (a b : [the lmodType R of R^o]) := a <| p |> b.
+
+Let avg0 a b : avg 0%:i01 a b = a.
+Proof. by rewrite /avg conv0. Qed.
+
+Let avgI p x : avg p x x = x.
+Proof. by rewrite /avg convmm. Qed.
+
+Let avgC p x y : avg p x y = avg (1 - (p%:inum))%:i01 y x.
+Proof. by rewrite /avg convC. Qed.
+
+Let avgA p q r (a b c : R) :
+  p%:inum * (`1-(q%:inum)) = (`1-(p%:inum * q%:inum)) * r%:inum ->
+  avg p a (avg q b c) = avg (p%:inum * q%:inum)%:i01 (avg r a b) c.
+Proof. by move=> h; rewrite /avg (convA _ _ r). Qed.
+
+HB.instance Definition _ := @isConvexSpace.Build R R^o
+  (Choice.class _) _ avg0 avgI avgC avgA.
+
+End realDomainType_convex_space.
+
+(* ref: http://www.math.wisc.edu/~nagel/convexity.pdf *)
+Section twice_derivable_convex.
+Context {R : realType}.
+Variables (f : R -> R^o) (a b : R^o).
+
+Let Df := 'D_1 f.
+Let DDf := 'D_1 Df.
+
+Hypothesis DDf_ge0 : forall x, a < x < b -> 0 <= DDf x.
+Hypothesis cvg_left : (f @ b^'-) --> f b.
+Hypothesis cvg_right : (f @ a^'+) --> f a.
+
+Let L x := f a + factor a b x * (f b - f a).
+
+Let LE x : a < b -> L x = factor b a x * f a + factor a b x * f b.
+Proof.
+move=> ab; rewrite /L -(@onem_factor _ a) ?lt_eqF// /onem mulrBl mul1r.
+by rewrite -addrA -mulrN -mulrDr (addrC (f b)).
+Qed.
+
+Let convexf_ptP : a < b -> (forall x, a <= x <= b -> 0 <= L x - f x) ->
+  forall t, f (a <| t |> b) <= f a <| t |> f b.
+Proof.
+move=> ab h t; set x := a <| t |> b; have /h : a <= x <= b.
+  by rewrite -(conv1 a b) -{1}(conv0 a b) /x !le_line_path//= itv_ge0/=.
+rewrite subr_ge0 => /le_trans; apply.
+by rewrite LE// /x line_pathK ?lt_eqF// convC line_pathK ?gt_eqF.
+Qed.
+
+Hypothesis HDf : {in `]a, b[, forall x, derivable f x 1}.
+Hypothesis HDDf : {in `]a, b[, forall x, derivable Df x 1}.
+
+Let cDf : {within `]a, b[, continuous Df}.
+Proof. by apply: derivable_within_continuous => z zab; exact: HDDf. Qed.
+
+Lemma second_derivative_convex (t : {i01 R}) : a <= b ->
+  f (a <| t |> b) <= f a <| t |> f b.
+Proof.
+rewrite le_eqVlt => /predU1P[<-|/[dup] ab]; first by rewrite !convmm.
+move/convexf_ptP; apply => x /andP[].
+rewrite le_eqVlt => /predU1P[<-|ax].
+  by rewrite /L factorl mul0r addr0 subrr.
+rewrite le_eqVlt => /predU1P[->|xb].
+  by rewrite /L factorr ?lt_eqF// mul1r addrAC addrA subrK subrr.
+have [c2 Ic2 Hc2] : exists2 c2, x < c2 < b & (f b - f x) / (b - x) = 'D_1 f c2.
+  have xbf : {in `]x, b[, forall z, derivable f z 1} :=
+    in1_subset_itv (subset_itvW _ _ (ltW ax) (lexx b)) HDf.
+  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))/cvg_at_right_filter.
+    have := derivable_within_continuous HDf.
+    rewrite continuous_open_subspace//; last exact: interval_open.
+    by apply; rewrite inE/= in_itv/= ax.
+  by exists z => //; rewrite fbfx -mulrA divff ?mulr1// subr_eq0 gt_eqF.
+have [c1 Ic1 Hc1] : exists2 c1, a < c1 < x & (f x - f a) / (x - a) = 'D_1 f c1.
+  have axf : {in `]a, x[, forall z, derivable f z 1} :=
+    in1_subset_itv (subset_itvW _ _ (lexx a) (ltW xb)) HDf.
+  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 _))/cvg_at_left_filter.
+    have := derivable_within_continuous HDf.
+    rewrite continuous_open_subspace//; last exact: interval_open.
+    by apply; rewrite inE/= in_itv/= ax.
+  by exists z => //; rewrite fxfa -mulrA divff ?mulr1// subr_eq0 gt_eqF.
+have c1c2 : c1 < c2.
+  by move: Ic2 Ic1 => /andP[+ _] => /[swap] /andP[_] /lt_trans; apply.
+have [d Id h] :
+    exists2 d, c1 < d < c2 & ('D_1 f c2 - 'D_1 f c1) / (c2 - c1) = DDf d.
+  have h : {in `]c1, c2[, forall z, derivable Df z 1}.
+    apply: (in1_subset_itv (subset_itvW _ _ (ltW (andP Ic1).1) (lexx _))).
+    apply: (in1_subset_itv (subset_itvW _ _ (lexx _) (ltW (andP Ic2).2))).
+    exact: HDDf.
+  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: cvg_at_right_filter.
+      move: cDf; rewrite continuous_open_subspace//; last exact: interval_open.
+      by apply; rewrite inE/= in_itv/= (andP Ic1).1 (lt_trans _ (andP Ic2).2).
+    + apply: cvg_at_left_filter.
+      move: cDf; rewrite continuous_open_subspace//; last exact: interval_open.
+      by apply; rewrite inE/= in_itv/= (andP Ic2).2 (lt_trans (andP Ic1).1).
+  by exists z => //; rewrite h -mulrA divff ?mulr1// subr_eq0 gt_eqF.
+have LfE : L x - f x =
+    ((x - a) * (b - x)) / (b - a) * ((f b - f x) / (b - x)) -
+    ((b - x) * factor a b x) * ((f x - f a) / (x - a)).
+  rewrite !mulrA -(mulrC (b - x)) -(mulrC (b - x)^-1) !mulrA.
+  rewrite mulVf ?mul1r ?subr_eq0 ?gt_eqF//.
+  rewrite -(mulrC (x - a)) -(mulrC (x - a)^-1) !mulrA.
+  rewrite mulVf ?mul1r ?subr_eq0 ?gt_eqF//.
+  rewrite -/(factor a b x).
+  rewrite -(opprB a b) -(opprB x b) invrN mulrNN -/(factor b a x).
+  rewrite -(@onem_factor _ a) ?lt_eqF//.
+  rewrite /onem mulrBl mul1r opprB addrA -mulrDr addrA subrK.
+  by rewrite /L -addrA addrC opprB -addrA (addrC (f a)).
+have {Hc1 Hc2} -> : L x - f x = (b - x) * (x - a) * (c2 - c1) / (b - a) *
+                                (('D_1 f c2 - 'D_1 f c1) / (c2 - c1)).
+  rewrite LfE Hc2 Hc1.
+  rewrite -(mulrC (b - x)) mulrA -mulrBr.
+  rewrite (mulrC ('D_1 f c2 - _)) ![in RHS]mulrA; congr *%R.
+  rewrite -2!mulrA; congr *%R.
+  by rewrite mulrCA divff ?mulr1// subr_eq0 gt_eqF.
+rewrite {}h mulr_ge0//; last first.
+  rewrite DDf_ge0//; apply/andP; split.
+    by rewrite (lt_trans (andP Ic1).1)//; case/andP : Id.
+  by rewrite (lt_trans (andP Id).2)//; case/andP : Ic2.
+rewrite mulr_ge0// ?invr_ge0 ?subr_ge0 ?(ltW ab)//.
+rewrite mulr_ge0// ?subr_ge0 ?(ltW c1c2)//.
+by rewrite mulr_ge0// subr_ge0 ltW.
+Qed.
+
+End twice_derivable_convex.

theories/derive.v

@@ -1042,6 +1042,14 @@ have -> : (fun h => (f \o shift x) h%:A) = f \o shift x.
 by have /diff_locally := dfx; rewrite diff1E // derive1E =>->.
 Qed.
 
+Lemma derivable_within_continuous f (i : interval R) :
+  {in i, forall x, derivable f x 1} -> {within [set` i], continuous f}.
+Proof.
+move=> di; apply/continuous_in_subspaceT => z /[1!inE] zA.
+apply/differentiable_continuous; rewrite -derivable1_diffP.
+by apply: di; rewrite inE.
+Qed.
+
 End DeriveRU.
 
 Section DeriveVW.

theories/exp.v

@@ -5,6 +5,7 @@ From mathcomp.classical Require Import boolp classical_sets functions.
 From mathcomp.classical Require Import mathcomp_extra.
 Require Import reals ereal nsatz_realtype.
 Require Import signed topology normedtype landau sequences derive realfun.
+Require Import itv convex.
 
 (******************************************************************************)
 (*               Theory of exponential/logarithm functions                    *)
@@ -349,6 +350,9 @@ Qed.
 Lemma derivable_expR x : derivable expR x 1.
 Proof. by apply: ex_derive; apply: is_derive_exp. Qed.
 
+Lemma derive_expR : 'D_1 expR = expR :> (R -> R).
+Proof. by apply/funext => r /=; rewrite derive_val. Qed.
+
 Lemma continuous_expR : continuous (@expR R).
 Proof.
 by move=> x; exact/differentiable_continuous/derivable1_diffP/derivable_expR.
@@ -464,6 +468,18 @@ have /expR_total_gt1[y [H1y H2y H3y]] : 1 <= x^-1 by rewrite ltW // !invf_cp1.
 by exists (-y); rewrite expRN H3y invrK.
 Qed.
 
+Local Open Scope convex_scope.
+Lemma convex_expR (t : {i01 R}) (a b : R^o) : a <= b ->
+  expR (a <| t |> b) <= (expR a : R^o) <| t |> (expR b : R^o).
+Proof.
+move=> ab; apply: second_derivative_convex => //.
+- by move=> x axb; rewrite derive_expR derive_val expR_ge0.
+- exact/cvg_at_left_filter/continuous_expR.
+- exact/cvg_at_right_filter/continuous_expR.
+- by move=> z zab; rewrite derive_expR; exact: derivable_expR.
+Qed.
+Local Close Scope convex_scope.
+
 End expR.
 
 Section Ln.