convex_function generalized

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

Author: mkerjean

CHANGELOG_UNRELEASED.md

@@ -220,6 +220,7 @@
 - in `normed_module.v`, turned into `Let`'s:
   + local lemmas `add_continuous`, `scale_continuous`, `locally_convex`
 
+  
 ### Renamed
 
 - in `topology_structure.v`
@@ -264,6 +265,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,8 @@ 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_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.