convex_function generalized

CHANGELOG_UNRELEASED.md

@@ -70,6 +70,9 @@
 - in `derive.v`:
   + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV`
 
+- in `convex.v`:
+  + lemma `convexW`
+
 ### Changed
 
 - in `constructive_ereal.v`: fixed the infamous `%E` scope bug.
@@ -220,6 +223,9 @@
 - in `normed_module.v`, turned into `Let`'s:
   + local lemmas `add_continuous`, `scale_continuous`, `locally_convex`
 
+- moved from `tvs.v` to `convex.v`
+  + definition `convex`
+
 ### Renamed
 
 - in `topology_structure.v`
@@ -264,6 +270,9 @@
   + lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd`,
     `integral_itv_bndoo`
 
+- in `convex.v`:
+  + definition `convex_function` (from a realType as domain to a convex_lmodType as domain)
+
 ### Deprecated
 
 - in `lebesgue_integral_nonneg.v`:

theories/convex.v

@@ -220,7 +220,24 @@ Proof. by move=> ab; rewrite in_itv/= -lerN2 convN convC !conv_le ?lerN2. Qed.
 
 End conv_numDomainType.
 
-Definition convex_function (R : realType) (D : set R) (f : R -> R^o) :=
+Definition convex (R : numDomainType) (M : lmodType R)
+    (A : set (convex_lmodType M)) :=
+  forall x y lambda, x \in A -> y \in A -> x <| lambda |> y \in A.
+
+Lemma convexW (R : numDomainType) (M : lmodType R) (A : set (convex_lmodType M)) :
+  convex A <->
+  {in A &, forall x y (k : {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 convex_function (R : numFieldType) (E : lmodType R) (E' := convex_lmodType E) (D : set E') (f : E' -> R^o) :=
   forall (t : {i01 R}),
-    {in D &, forall (x y : R^o), (f (x <| t |> y) <= f x <| t |> f y)%R}.
+    {in D &, forall (x y : E'), (f (x <| t |> y) <= f x <| t |> f y)%R}.
 (* TODO: generalize to convTypes once we have ordered convTypes (mathcomp 2) *)

theories/hoelder.v

@@ -532,13 +532,14 @@ End hoelder2.
 Section convex_powR.
 Context {R : realType}.
 Local Open Scope ring_scope.
+Local Open Scope convex_scope.
 
 Lemma convex_powR p : 1 <= p ->
-  convex_function `[0, +oo[%classic (@powR R ^~ p).
+  convex_function (`[0, +oo[%classic : set R) (@powR R ^~ p).
 Proof.
 move=> p1 t x y /[!inE] /= /[!in_itv] /= /[!andbT] x_ge0 y_ge0.
-have p0 : 0 < p by rewrite (lt_le_trans _ p1).
-rewrite !convRE; set w1 := t%:num; set w2 := t%:inum.~.
+have p0 : 0 < p by rewrite (lt_le_trans _ p1).  
+rewrite convRE [X in X `^ _ <= _]convRE; set w1 := t%:num; set w2 := t%:inum.~.
 have [->|w20] := eqVneq w2 0.
   rewrite !mul0r !addr0; have [->|w10] := eqVneq w1 0.
     by rewrite !mul0r powR0// gt_eqF.

theories/normedtype_theory/normed_module.v

@@ -7,7 +7,7 @@ From mathcomp Require Import interval_inference fieldext falgebra.
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets filter functions cardinality.
 From mathcomp Require Import set_interval ereal reals topology real_interval.
-From mathcomp Require Import prodnormedzmodule tvs num_normedtype.
+From mathcomp Require Import convex prodnormedzmodule tvs num_normedtype.
 From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule.
 
 (**md**************************************************************************)
@@ -111,21 +111,27 @@ rewrite (@le_lt_trans _ _ (`|k - l| * M)) ?ler_wpM2l -?ltr_pdivlMr//.
 by near: l; apply: cvgr_dist_lt; rewrite // divr_gt0.
 Unshelve. all: by end_near. Qed.
 
+Local Open Scope convex_scope.
+
 (** NB: we have almost the same proof in `tvs.v` *)
 Let locally_convex :
-  exists2 B : set (set V), (forall b, b \in B -> convex b) & basis B.
-Proof.
-exists [set B | exists x r, B = ball x r].
-  move=> b; rewrite inE /= => [[x]] [r] -> z y l.
-  rewrite !inE -!ball_normE /= => zx yx l0; rewrite -subr_gt0 => l1.
-  have -> : x = l *: x + (1 - l) *: x by rewrite addrC scalerBl subrK scale1r.
-  rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first.
+  exists2 B : set (set (convex_lmodType V)), (forall b, b \in B -> convex b) & basis B.
+Proof.
+exists [set B | exists (x : convex_lmodType V) r, B = ball x r].
+  move=> b; rewrite inE => [[x]] [r] ->.
+  apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
+  have -> : x = x <| l |> x by rewrite convmm. (*TODO: this looks superfluous *)
+  rewrite /ball_/= inE/=.
+  rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType V) <| l |>
+                              (x - y : convex_lmodType V)); last first.
     by rewrite opprD addrACA -scalerBr -scalerBr.
-  rewrite (@le_lt_trans _ _ (`|l| * `|x - z| + `|1 - l| * `|x - y|))//.
+  rewrite (@le_lt_trans _ _ ((l%:num) * `|x - z| + l%:num.~ * `|x - y|))//.
+    rewrite -[in X in _ <= X + _](@ger0_norm _ l%:num)//.
+    rewrite -[in X in _ <= _ + X](@ger0_norm _ l%:num.~) ?subr_ge0//.
     by rewrite -!normrZ ler_normD.
-  rewrite (@lt_le_trans _ _ (`|l| * r + `|1 - l| * r ))//.
-    by rewrite ltr_leD// lter_pM2l// ?normrE ?gt_eqF// ltW.
-  by rewrite !gtr0_norm// -mulrDl addrC subrK mul1r.
+  rewrite (@lt_le_trans _ _ (l%:num * r + l%:num.~ * r ))//.
+    by rewrite ltr_leD// lter_pM2l// ?normrE ?gt_eqF ?ltW// subr_gt0.
+  by rewrite -mulrDl addrC subrK mul1r.
 split.
   move=> B [x] [r] ->.
   rewrite openE/= -ball_normE/= /interior => y /= bxy; rewrite -nbhs_ballE.

theories/normedtype_theory/tvs.v

@@ -2,8 +2,10 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector.
 From mathcomp Require Import interval_inference.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions cardinality.
-From mathcomp Require Import set_interval reals topology num_normedtype.
+From mathcomp Require Import convex set_interval reals topology num_normedtype.
 From mathcomp Require Import pseudometric_normed_Zmodule.
 
 (**md**************************************************************************)
@@ -306,10 +308,6 @@ HB.instance Definition _ :=
 
 HB.end.
 
-Definition convex (R : numDomainType) (M : lmodType R) (A : set M) :=
-  forall x y (lambda : R), x \in A -> y \in A ->
-  0 < lambda -> lambda < 1 -> lambda *: x + (1 - lambda) *: y \in A.
-
 HB.mixin Record Uniform_isTvs (R : numDomainType) E
     & Uniform E & GRing.Lmodule R E := {
   locally_convex : exists2 B : set (set E),
@@ -511,20 +509,30 @@ rewrite (@le_lt_trans _ _ (`|k - l| * M)) ?ler_wpM2l -?ltr_pdivlMr//.
 by near: l; apply: cvgr_dist_lt; rewrite // divr_gt0.
 Unshelve. all: by end_near. Qed.
 
+Local Open Scope convex_scope.
+
 Let standard_locally_convex :
   exists2 B : set (set R^o), (forall b, b \in B -> convex b) & basis B.
 Proof.
 exists [set B | exists x r, B = ball x r].
-  move=> b; rewrite inE /= => [[x]] [r] -> z y l.
-  rewrite !inE -!ball_normE /= => zx yx l0; rewrite -subr_gt0 => l1.
-  have -> : x = l *: x + (1 - l) *: x by rewrite addrC scalerBl subrK scale1r.
-  rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first.
-    by rewrite opprD addrACA -scalerBr -scalerBr.
-  rewrite (@le_lt_trans _ _ (`|l| * `|x - z| + `|1 - l| * `|x - y|))//.
-    by rewrite -!normrM ler_normD.
-  rewrite (@lt_le_trans _ _ (`|l| * r + `|1 - l| * r ))//.
-    by rewrite ltr_leD// lter_pM2l// ?normrE ?gt_eqF// ltW.
-  by rewrite !gtr0_norm// -mulrDl addrC subrK mul1r.
+  move=> b/= /[!inE]/= [[x]] [r] ->.
+  apply/convexW => z y; rewrite /ball/= !inE/= => zx yx l /[!inE]/= l0 l1.
+  (* conv lemma? *)
+  have -> : x = x <| l |> x by rewrite convmm. (*TODO: this looks superfluous *)
+  rewrite [X in `|X|](_ : _ = (x - z) <| l |> (x - y)); last first.
+    by rewrite opprD addrACA -mulrBr -mulrBr.
+ rewrite (@le_lt_trans _ _ ((`|x - z| : R^o) <| l |> `|x - y|))//.
+    rewrite -[in X in _ <= X + _](@ger0_norm _ l%:num)//.
+    rewrite -[in X in _ <= _ + X](@ger0_norm _ l%:num.~) ?subr_ge0//.
+    rewrite [X in `|X| <= _](_ : _ = l%:num * (x - z) + l%:num.~ * (x - y))//.
+    rewrite -[X in _ <= X + _]normrM.
+    rewrite -[X in _ <= _ + X]normrM.
+    by rewrite ler_normD.
+  rewrite (@lt_le_trans _ _ ((r : R^o) <| l |> r))//.
+    rewrite ltr_leD//.
+      by rewrite ltr_pM2l// normr_gt0// gt_eqF.
+    by rewrite ler_wpM2l// ?subr_ge0// ltW.
+  by rewrite convmm.
 split.
   move=> B [x] [r] ->.
   rewrite openE/= -ball_normE/= /interior => y /= bxy; rewrite -nbhs_ballE.
@@ -587,8 +595,10 @@ have : basis B.
   rewrite !nbhsE /=; split; first by exists a => //; split => //; exact: Beo.
   by exists b => //; split => // []; exact: Bfo.
 exists B => // => b; rewrite inE /= => [[]] bo [] be [] bf Bee [] Bff <-.
-move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2] l0 l1.
-by split; rewrite -inE; [apply: Bcb; rewrite ?inE|apply: Bcf; rewrite ?inE].
+move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2].
+split.
+  by apply/set_mem/Bcb; [exact/mem_set|exact/mem_set|exact/mem_set].
+by apply/set_mem/Bcf; [exact/mem_set|exact/mem_set|exact/mem_set].
 Qed.
 
 HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build