Library mathcomp.analysis.convex

(* 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 Require Import mathcomp_extra boolp classical_sets set_interval.
From mathcomp Require Import functions cardinality.
Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
Require Import 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.

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.


#[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.

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.

Let avgI p x : avg p x x = x.

Let avgC p x y : avg p x y = avg (1 - (p%:inum))%:i01 y x.

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.


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.

Let avgI p x : avg p x x = x.

Let avgC p x y : avg p x y = avg (1 - (p%:inum))%:i01 y x.

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.


End realDomainType_convex_space.

Section conv_realDomainType.
Context {R : realDomainType}.

Lemma conv_gt0 (a b : R^o) (t : {i01 R}) : 0 < a 0 < b 0 < a <| t |> b.

Lemma convRE (a b : R^o) (t : {i01 R}) : a <| t |> b = `1-(t%:inum) × a + t%:inum × b.

End conv_realDomainType.

Definition convex_function (R : realType) (D : set R) (f : R R^o) :=
   (t : {i01 R}), {in D &, (x y : R^o), (f (x <| t |> y) f x <| t |> f y)%R}.
TODO: generalize to convTypes once we have ordered convTypes (mathcomp 2) 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 : 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.

Let convexf_ptP : a < b ( x, a x b 0 L x - f x)
   t, f (a <| t |> b) f a <| t |> f b.

Hypothesis HDf : {in `]a, b[, x, derivable f x 1}.
Hypothesis HDDf : {in `]a, b[, x, derivable Df x 1}.

Let cDf : {within `]a, b[, continuous Df}.

Lemma second_derivative_convex (t : {i01 R}) : a b
  f (a <| t |> b) f a <| t |> f b.

End twice_derivable_convex.