Module mathcomp.analysis.convex

From HB Require Import structures.
From mathcomp Require Import boot order 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 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 ``` ``` convex_set A == A : set M is a convex set M is an Lmodule over R : numDomainType convex_function f == f : E -> R is a convex function E is an Lmodule over R : numFieldType ```

Reserved Notation "x <| p |> y" (format "x <| p |> y", at level 49).

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

Lemma { : realFieldType} ( : R) :
0 <= r -> r <= 1 -> x < e -> y < e -> r * x + r.~ * y < e.

Proof.

move => r0 r1 xe ye.
have [->|] := eqVneq r 0; first by rewrite mul0r /onem subr0 add0r mul1r.
have [->|] := eqVneq r 1; first by rewrite mul1r /onem subrr mul0r addr0.
move=> rneq0 rneq1.
have -> : e = r * e + (1 -r) * e by rewrite -mulrDl addrCA subrr addr0 mul1r.
apply: ltrD.
rewrite lter_pM2l lt_neqAle; apply/andP; split => //; first by rewrite eq_sym.
by move: xe; rewrite lt_def; move/andP => []; rewrite eq_sym //.
by apply: ltW.
rewrite lter_pM2l /onem ?subr_gt0 ?ltW //.
by rewrite lt_def; apply/andP; split => //; rewrite eq_sym.
Qed.

Lemma { : realFieldType} ( : R):
0 <= r -> r <= 1 -> 0 <= x -> x <= e -> 0 <= y -> y <= e -> r * x + r.~ * y <= e.

Proof.

move => r0 r1 x0 xe y0 ye.
rewrite /onem.
have -> : e = r * e + (1 -r) * e by rewrite -mulrDl addrCA subrr addr0 mul1r.
apply: lerD; first by rewrite ler_pM.
by rewrite ler_pM ?subr_ge0 //.
Qed.

Declare Scope convex_scope.
Local Open Scope convex_scope.

Module .
Section def.
Variables ( : numDomainType) ( : Type) ( : {i01 R} -> T -> T -> T).

Local Notation := (conv p x y).

Definition := forall ( : {i01 R}) ( : 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 ( : comPzRingType) ( : R) :
  p = r * s ->
  1 - s = (1 - p) * (1 - q) ->
  (1 - p) * q = s * (1 - r).

Proof.

move=> prs spq; rewrite mulrBr [s * r]mulrC -prs mulr1 -[s](subKr 1) spq.
by rewrite addrAC -[X in _ = X - _]mulr1 -mulrBr subKr.
Qed.

Lemma ( : pzRingType) ( : R) :
1 - s = (1 - p) * (1 - q) ->
s = 1 - (1 - p) * (1 - q).

Proof.

by move/eqP; rewrite subr_eq addrC -subr_eq => /eqP ->. Qed.

Lemma ( : comUnitRingType) ( : R) :
  1 - p \is a GRing.unit ->
  p = r * s ->
  1 - s = (1 - p) * (1 - q) ->
  q = (s * (1 - r)) / (1 - p).

Proof.

by move=> p1unit /pq_sr /[apply] /(canRL (mulKr p1unit)); rewrite mulrC.
Qed.

Lemma ( : unitRingType) ( : R) :
s \is a GRing.unit -> p = r * s -> r = p / s.

Proof.

by move=> sunit /(canLR (mulrK sunit)) <-. Qed.

End lemmas.

End ConvexQuasiAssoc.

Definition := ConvexQuasiAssoc.law.

. () T := {
  conv : {i01 R} -> T -> T -> T ;
  conv1 : forall , conv 1%:i01 a b = a ;
  convmm : forall ( : {i01 R}) , conv p a a = a ;
  convC : forall ( : {i01 R}) , conv p a b = conv (1 - p%:inum)%:i01 b a;
  convA : convex_quasi_associative conv
}.

()
. () :=
  { of isConvexSpace R T & Choice T}.

Notation := (conv p a b) : convex_scope.

Section convex_space_lemmas.
Context ( : convType R).
Implicit Types a b : A.

Lemma : a <| 0%:i01 |> b = b.

Proof.

rewrite convC/= [X in _ <| X |> _](_ : _ = 1%:i01) ?conv1//.
by apply/val_inj => /=; rewrite subr0.
Qed.

End convex_space_lemmas.

Local Open Scope convex_scope.

Definition { : numDomainType} ( : lmodType R) : Type := E.

Section lmodType_convex_space.
Context { : numDomainType} { : lmodType R}.
Implicit Type p q r : {i01 R}.

Let := convex_lmodType E'.

Let ( : E) := p%:inum *: a + p%:inum.~ *: b.

Let : avg 1%:i01 a b = a.

Proof.

by rewrite /avg/= onem1 scale0r scale1r addr0. Qed.

Let : avg p x x = x.

Proof.

by rewrite /avg -scalerDl/= add_onemK scale1r. Qed.

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

Proof.

by rewrite /avg onemK addrC. Qed.

Let : convex_quasi_associative avg.

Proof.

move=> p q r s a b c prs spq; rewrite /avg.
rewrite [in LHS]scalerDr [in LHS]addrA [in RHS]scalerDr; congr (_ + _ + _).
- by rewrite scalerA mulrC prs.
- by rewrite !scalerA; congr *:%R; rewrite (ConvexQuasiAssoc.pq_sr prs).
- by rewrite scalerA spq.
Qed.

..on E.

.
isConvexSpace.Build R E avg1 avgI avgC avgA.

End lmodType_convex_space.

Lemma ( : numDomainType) ( : lmodType R) ( : {i01 R}) ( : convex_lmodType E) :
x <| t |> y + z' = (x + z' : convex_lmodType _) <| t |> (y + z').

Proof.

rewrite /conv/=.
rewrite !scalerDr -[in RHS]addrA.
rewrite [in X in (_ = _ + X)]addrCA [in X in (_ = _ + ( _ + X))]scalerBl.
by rewrite [in X in (_ = _ + ( _ + X))]addrCA addrN addr0 scale1r addrA.
Qed.

Definition ( : numDomainType) : Type := R^o.

Section numDomainType_convex_space.
Context { : numDomainType}.
Implicit Types p q : {i01 R}.

Let ( : convex_lmodType R^o) := a <| p |> b.

Let : avg 1%:i01 a b = a.

Proof.

exact: conv1. Qed.

Let : avg p x x = x.

Proof.

exact: convmm. Qed.

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

Proof.

exact: convC. Qed.

Let : convex_quasi_associative avg.

Proof.

exact: convA. Qed.

..Build R R^o
_ avg1 avgI avgC avgA.

End numDomainType_convex_space.

Section conv_numDomainType.
Context { : numDomainType}.

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

Proof.

move=> a0 b0.
have [->|t0] := eqVneq t 0%:i01; first by rewrite conv0.
have [->|t1] := eqVneq t 1%:i01; first by rewrite conv1.
rewrite addr_gt0// mulr_gt0//; first by rewrite lt_neqAle eq_sym t0 ge0.
by rewrite subr_gt0 lt_neqAle t1 le1.
Qed.

Lemma ( : R^o) ( : {i01 R}) :
a <| t |> b = t%:inum * a + t%:inum.~ * b.

Proof.

by []. Qed.

Let ( : R^o) ( : {i01 R}) :
a <| t |> b = t%:inum.~ * b + t%:inum * a.

Proof.

by rewrite addrC convRE. Qed.

Lemma ( : R^o) ( : {i01 R}) :
a <| t |> b = line_path b a t%:num.

Proof.

by rewrite convRCE. Qed.

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

Proof.

by rewrite !convRE opprD !mulrN. Qed.

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

Proof.

move=> ab; rewrite convRE mulrBl mul1r addrCA -mulrBr gerDl.
by rewrite mulr_ge0_le0// subr_le0.
Qed.

Lemma ( : R^o) ( : {i01 R}) : a <= b -> a <| t |> b \in `[a, b].

Proof.

by move=> ab; rewrite in_itv/= -lerN2 convN convC !conv_le ?lerN2. Qed.

End conv_numDomainType.

Definition ( : numDomainType) ( : lmodType R)
    ( : set (convex_lmodType M)) :=
  forall , x \in A -> y \in A -> x <| lambda |> y \in A.

Lemma ( : numDomainType) ( : lmodType R)
    ( : set (convex_lmodType M)) :
  convex_set A <->
  {in A &, forall ( : {i01 R}),
    0 < k%:num -> k%:num < 1 -> x <| k |> y \in A}.

Proof.

split => [cA x y xA yA k k0 k1|cA x y l xA yA].
by have /(_ k) := cA _ _ _ xA yA.
have [->|l0] := eqVneq l 0%:i01; first by rewrite conv0.
have [->|l1] := eqVneq l 1%:i01; first by rewrite conv1.
apply: cA => //.
- by rewrite lt_neqAle eq_sym l0 ge0.
- by rewrite lt_neqAle l1 le1.
Qed.

Definition ( : numFieldType) ( : lmodType R)
    ( := convex_lmodType E) ( : set E') ( : E' -> R^o) :=
  forall ( : {i01 R}),
    {in D &, forall ( : E'), (f (x <| t |> y) <= f x <| t |> f y)%R}.

Files

Module mathcomp.analysis.convex