Definition of convex_cone

Stream: maths

[Apurva Nakade]

Hi, I'm trying to use the docs#convex_cone for linear programming and I'm a bit surprised by the definition. The scalars are required to only be positive, 0 < c. I checked the wikipedia reference and I can see where this definition is coming from.

However, most textbooks instead define convex cones by 0 ≤ c. For example, Section 2.1.5 here: https://web.stanford.edu/~boyd/cvxbook/bv_cvxbook.pdf

IMO the current definition is too weak for conic/linear programming. Would it be ok to define another structure closed_convex_cone which replaces 0 < c with 0 \le c and create some basic API for it similar to the convex_cone API? Or is this too much duplication.

Another option is to define a closed_convex_cone as something that is both a convex_cone and closed, but this definition will require the ring and the total space to be topological.

It is not clear to me which of the two options is more appropriate by mathlib standards.

[Apurva Nakade]

(deleted)

[Apurva Nakade]

(deleted)

[Apurva Nakade]

Here's a reference that suggests that the first approach is the prefered one (even though the definition does not provide a closed set in the topological sense): https://ti.inf.ethz.ch/ew/lehre/ApproxSDP09/notes/conelp.pdf