Experiment : Tvs

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,12 @@
 - 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`
+
+- in convex.v
+  + definition `convex_function` generalized from a realspace as domain to a lmodType as domain
+
 ### Renamed
 
 - in `topology_structure.v`
@@ -264,6 +273,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`:

_CoqProject

@@ -143,6 +143,8 @@ theories/kernel.v
 theories/pi_irrational.v
 theories/gauss_integral.v
 
+theories/hahn_banach_theorem.v
+
 theories/all_analysis.v
 
 theories/showcase/summability.v

classical/filter.v

@@ -245,6 +245,11 @@ HB.structure Definition Nbhs := {T of Choice T & hasNbhs T}.
 #[short(type="pnbhsType")]
 HB.structure Definition PointedNbhs := {T of Pointed T & hasNbhs T}.
 
+HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}.
+HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}.
+HB.structure Definition NbhsLmodule (K : numDomainType) :=
+  {M of Nbhs M & GRing.Lmodule K M}.
+
 Definition filter_from {I T : Type} (D : set I) (B : I -> set T) :
   set_system T := [set P | exists2 i, D i & B i `<=` P].
 

theories/Make

@@ -104,6 +104,9 @@ probability_theory/beta_distribution.v
 probability_theory/probability.v
 
 convex.v
+
+hahn_banach_theorem.v
+
 charge.v
 kernel.v
 pi_irrational.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/derive.v

@@ -322,9 +322,9 @@ evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first.
   rewrite funeqE=> h.
   by rewrite -[_ - _]addrA addrC subrKA scalerDr addrC linearZ scalerA /g.
 apply: cvg_lim => //.
-pose g1 : R -> W := fun h => (h^-1 * h) *: 'd f a v.
-pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ).
-rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD.
+pose g1 := fun h => (h^-1 * h) *: 'd f a v.
+pose g2 := fun h : R => h^-1 *: k (h *: v ).
+rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: pseudometric_normed_Zmodule.cvgD.
   rewrite -(scale1r (_ _ v)); apply: cvgZr_tmp => /= X [e e0].
   rewrite /ball_ /= => eX.
   apply/nbhs_ballP.
@@ -415,7 +415,7 @@ Fact dadd (f g : V -> W) x :
   continuous ('d f x \+ 'd g x) /\
   (f + g) \o shift x = cst ((f + g) x) + ('d f x \+ 'd g x) +o_ 0 id.
 Proof.
-move=> df dg; split => [?|]; do ?exact: continuousD.
+move=> df dg; split => [?|]; do ?exact: normed_module.continuousD.
 apply/(@eqaddoE R); rewrite funeqE => y /=.
 by rewrite !fctE ![_ (_ + x)]diff_locallyx// addrACA addox addrACA.
 Qed.
@@ -424,7 +424,7 @@ Fact dopp (f : V -> W) x :
   differentiable f x -> continuous (- ('d f x : V -> W)) /\
   (- f) \o shift x = cst (- f x) \- 'd f x +o_ 0 id.
 Proof.
-move=> df; split; first by move=> ?; apply: continuousN.
+move=> df; split; first by move=> ?; apply: normed_module.continuousN.
 apply/eqaddoE; rewrite funeqE => y /=.
 by rewrite -[(- f) _]/(- (_ _)) diff_locallyx// !opprD oppox.
 Qed.
@@ -820,7 +820,7 @@ Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p :
     (fun q => f p.1 q.2 + f q.1 p.2) +o_ (0 : U * V') id.
 Proof.
 move=> fc; split=> [q|].
-  by apply: (@continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2));
+  by apply: (@normed_module.continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2));
     move=> A /(fc (_.1, _.2)) /= /nbhs_ballP [_ /posnumP[e] fpqe_A];
     apply/nbhs_ballP; exists e%:num => //= r [? ?]; exact: (fpqe_A (_.1, _.2)).
 apply/eqaddoE; rewrite funeqE => q /=.
@@ -1130,7 +1130,7 @@ move=> df dg.
 evar (fg : R -> W); rewrite [X in X @ _](_ : _ = fg) /=; last first.
   rewrite funeqE => h.
   by rewrite !scalerDr scalerN scalerDr opprD addrACA -!scalerBr /fg.
-exact: cvgD.
+exact: pseudometric_normed_Zmodule.cvgD.
 Qed.
 
 Lemma deriveD f g (x v : V) : derivable f x v -> derivable g x v ->
@@ -1286,7 +1286,7 @@ evar (fg : R -> R); rewrite [X in X @ _](_ : _ = fg) /=; last first.
     by rewrite !scalerBr -addrA ![g x *: _]mulrC addKr.
   rewrite scalerDr scalerA mulrC -scalerA.
   by rewrite [_ *: (g x *: _)]scalerA mulrC -scalerA /fg.
-apply: cvgD; last exact: cvgZl_tmp df.
+apply: pseudometric_normed_Zmodule.cvgD; last exact: cvgZl_tmp df.
 apply: cvg_comp2 (@scale_continuous _ _ (_, _)) => /=; last exact: dg.
 suff : {for 0, continuous (fun h : R => f(h *: v + x))}.
   by move=> /continuous_withinNx; rewrite scale0r add0r.
@@ -1447,7 +1447,7 @@ pose g t : R := (sup (f @` A) - f t)^-1.
 have invf_continuous : {within A, continuous g}.
   rewrite continuous_subspace_in => t tA; apply: cvgV => //=.
     by rewrite subr_eq0 gt_eqF// AfsupfA//; rewrite inE in tA.
-  by apply: cvgD; [exact: cst_continuous | apply: cvgN; exact: cf].
+  by apply: pseudometric_normed_Zmodule.cvgD; [exact: cst_continuous | apply: cvgN; exact: cf].
 have /ex_strict_bound_gt0[k k_gt0 /= imVfltk] : bounded_set (g @` A).
   exact/compact_bounded/continuous_compact.
 have [_ [t tA <-]] : exists2 y, (f @` A) y & sup (f @` A) - k^-1 < y.
@@ -1465,7 +1465,7 @@ Lemma compact_EVT_min (T : topologicalType) (R : realType) (f : T -> R)
 Proof.
 move=> A0 cA cf.
 have /(compact_EVT_max A0 cA)[c cinA fcmin] : {within A, continuous (- f)}.
-  by move=> ?; apply: continuousN => ?; exact: cf.
+  by move=> ?; apply: normed_module.continuousN => ?; exact: cf.
 by exists c => // t tA; rewrite -lerN2 fcmin.
 Qed.
 
@@ -1604,8 +1604,8 @@ set g := f + (- ( *:%R^~ ((f b - f a) / (b - a)) : R -> R)).
 have gdrvbl x : x \in `]a, b[%R -> derivable g x 1.
   by move=> /fdrvbl dfx; apply/derivableB/derivable1_diffP.
 have gcont : {within `[a, b], continuous g}.
-  move=> x; apply: continuousD _ ; first exact: fcont.
-  exact/continuousN/continuous_subspaceT/scalel_continuous.
+  move=> x; apply: normed_module.continuousD _ ; first exact: fcont.
+  exact/normed_module.continuousN/continuous_subspaceT/scalel_continuous.
 have gaegb : g a = g b.
   rewrite /g -![(_ - _ : _ -> _) _]/(_ - _).
   apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl.
@@ -1690,7 +1690,7 @@ apply: ger0_derive1_le.
 - move => x xab; exact/derivableN/df.
 - move => x xab; rewrite derive1E deriveN; last exact: df.
   by rewrite -derive1E oppr_ge0 dfle0.
-by move=> x; exact/continuousN/cf.
+by move=> x; exact/normed_module.continuousN/cf.
 Qed.
 
 Lemma ler0_derive1_le_cc :{within `[a, b], continuous f} ->
@@ -1797,7 +1797,7 @@ apply: gtr0_derive1_lt.
 - move => x xab; exact/derivableN/df.
 - move => x xab; rewrite derive1E deriveN; last exact: df.
   by rewrite -derive1E oppr_gt0 dflt0.
-by move=> x; exact/continuousN/cf.
+by move=> x; exact/normed_module.continuousN/cf.
 Qed.
 
 Lemma ltr0_derive1_lt_cc : {within `[a, b], continuous f} ->