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