Module mathcomp.analysis.convex

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

Section conv_realDomainType .
Context {R : realDomainType}.

Lemma conv_gt0 ( a b : R^o) ( t : {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//; last by rewrite lt_neqAle eq_sym t0/=.
by rewrite onem_gt0// lt_neqAle t1/=.
Qed.

Lemma convRE ( a b : R^o) ( t : {i01 R}) : a <| t |> b = `1-(t%:inum) * a + t%:inum * b.
Proof.
by []. Qed.

End conv_realDomainType.

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

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.
Generated by a fork of coq2html