Module mathcomp.analysis.convex
From HB Require Import structures.From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrint ssrnum interval.
From mathcomp Require Import interval_inference.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
From mathcomp Require Import reals topology.
# Convexity
This file provides a small account of convexity using convex spaces, to be
completed with material from InfoTheo.
```
convex_quasi_associative == quasi-associativity of the operator of
convex spaces
isConvexSpace R T == interface for convex spaces with
R : numDomainType
The HB class is ConvexSpace.
a <| t |> b == convexity operator
```
For `R : numDomainType`, `E : lmodType R` and `R` itself are shown to be
convex spaces with the following aliases:
```
convex_lmodType E == E : lmodType R as a convex space
convex_numDomainType R == R : numDomainType as a convex space
```
Reserved Notation "x <| p |> y" (format "x <| p |> y", at level 49).
Set SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Declare Scope convex_scope.
Local Open Scope convex_scope.
Module ConvexQuasiAssoc.
Section def.
Variables (R : numDomainType) (T : Type) (conv : {i01 R} -> T -> T -> T).
Local Notation "x <| p |> y" := (conv p x y).
Definition law := forall (p q r s : {i01 R}) (a b c : T),
p%:num = r%:num * s%:num ->
s%:num.~ = p%:num.~ * q%:num.~ ->
a <| p |> (b <| q |> c) = (a <| r |> b) <| s |> c.
End def.
technical relations between the parameters of the quasi-associativity law
Section lemmas.Lemma pq_sr (R : comPzRingType) (p q r s : R) :
p = r * s ->
1 - s = (1 - p) * (1 - q) ->
(1 - p) * q = s * (1 - r).
Proof.
Lemma sE (R : pzRingType) (p q s : R) :
1 - s = (1 - p) * (1 - q) ->
s = 1 - (1 - p) * (1 - q).
Lemma qE (R : comUnitRingType) (p q r s : R) :
1 - p \is a GRing.unit ->
p = r * s ->
1 - s = (1 - p) * (1 - q) ->
q = (s * (1 - r)) / (1 - p).
Lemma rE (R : unitRingType) (p r s : R) :
s \is a GRing.unit -> p = r * s -> r = p / s.
End lemmas.
End ConvexQuasiAssoc.
Definition convex_quasi_associative := ConvexQuasiAssoc.law.
HB.mixin Record isConvexSpace (R : numDomainType) T := {
conv : {i01 R} -> T -> T -> T ;
conv1 : forall a b, conv 1%: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 : convex_quasi_associative conv
}.
#[short(type=convType)]
HB.structure Definition ConvexSpace (R : numDomainType) :=
{T of isConvexSpace R T & Choice T}.
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 conv0 a b : a <| 0%:i01 |> b = b.
Proof.
End convex_space_lemmas.
Local Open Scope convex_scope.
Definition convex_lmodType {R : numDomainType} (E : lmodType R) : Type := E.
Section lmodType_convex_space.
Context {R : numDomainType} {E' : lmodType R}.
Implicit Type p q r : {i01 R}.
Let E := convex_lmodType E'.
Let avg p (a b : E) := p%:inum *: a + p%:inum.~ *: b.
Let avg1 a b : avg 1%: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 : convex_quasi_associative avg.
Proof.
HB.instance Definition _ := Choice.on E.
HB.instance Definition _ :=
isConvexSpace.Build R E avg1 avgI avgC avgA.
End lmodType_convex_space.
Definition convex_numDomainType (R : numDomainType) : Type := R^o.
Section numDomainType_convex_space.
Context {R : numDomainType}.
Implicit Types p q : {i01 R}.
Let avg p (a b : convex_lmodType R^o) := a <| p |> b.
Let avg1 a b : avg 1%:i01 a b = a.
Proof.
Let avgI p x : avg p x x = x.
Proof.
Let avgC p x y : avg p x y = avg (1 - (p%:inum))%:i01 y x.
Proof.
Let avgA : convex_quasi_associative avg.
Proof.
HB.instance Definition _ := @isConvexSpace.Build R R^o
_ avg1 avgI avgC avgA.
End numDomainType_convex_space.
Section conv_numDomainType.
Context {R : numDomainType}.
Lemma convR_gt0 (a b : R^o) (t : {i01 R}) : 0 < a -> 0 < b -> 0 < a <| t |> b.
Proof.
Lemma convRE (a b : R^o) (t : {i01 R}) :
a <| t |> b = t%:inum * a + t%:inum.~ * b.
Proof.
by []. Qed.
Let convRCE (a b : R^o) (t : {i01 R}) :
a <| t |> b = t%:inum.~ * b + t%:inum * a.
Lemma convR_line_path (a b : R^o) (t : {i01 R}) :
a <| t |> b = line_path b a t%:num.
Proof.
Lemma convN (a b : R^o) (t : {i01 R}) : - (a <| t |> b) = - a <| t |> - b.
Lemma conv_le (a b : R^o) (t : {i01 R}) : a <= b -> a <| t |> b <= b.
Proof.
Lemma convR_itv (a b : R^o) (t : {i01 R}) : a <= b -> a <| t |> b \in `[a, b].
End conv_numDomainType.
Definition convex_function (R : realType) (D : set R) (f : R -> R^o) :=
forall (t : {i01 R}),
{in D &, forall (x y : R^o), (f (x <| t |> y) <= f x <| t |> f y)%R}.