Convex cones #
In a π-module E, we define a convex cone as a set s such that a β’ x + b β’ y β s whenever
x, y β s and a, b > 0. We prove that convex cones form a complete_lattice, and define their
images (convex_cone.map) and preimages (convex_cone.comap) under linear maps.
We define pointed, blunt, flat and salient cones, and prove the correspondence between convex cones and ordered modules.
We also define convex.to_cone to be the minimal cone that includes a given convex set.
We define set.inner_dual_cone to be the cone consisting of all points y such that for
all points x in a given set 0 β€ βͺ x, y β«.
Main statements #
We prove two extension theorems:
riesz_extension: M. Riesz extension theorem says that ifsis a convex cone in a real vector spaceE,pis a submodule ofEsuch thatp + s = E, andfis a linear functionp β βwhich is nonnegative onp β© s, then there exists a globally defined linear functiong : E β βthat agrees withfonp, and is nonnegative ons.exists_extension_of_le_sublinear: Hahn-Banach theorem: ifN : E β βis a sublinear map,fis a linear map defined on a subspace ofE, andf x β€ N xfor allxin the domain off, thenfcan be extended to the whole space to a linear mapgsuch thatg x β€ N xfor allx
Implementation notes #
While convex π is a predicate on sets, convex_cone π E is a bundled convex cone.
References #
Definition of convex_cone and basic properties #
- carrier : set E
- smul_mem' : β β¦c : πβ¦, 0 < c β β β¦x : Eβ¦, x β self.carrier β c β’ x β self.carrier
- add_mem' : β β¦x : Eβ¦, x β self.carrier β β β¦y : Eβ¦, y β self.carrier β x + y β self.carrier
A convex cone is a subset s of a π-module such that a β’ x + b β’ y β s whenever a, b > 0
and x, y β s.
Instances for convex_cone
Equations
- convex_cone.set.has_coe = {coe := convex_cone.carrier _inst_3}
Equations
- convex_cone.has_mem = {mem := Ξ» (m : E) (S : convex_cone π E), m β S.carrier}
Equations
- convex_cone.has_le = {le := Ξ» (S T : convex_cone π E), S.carrier β T.carrier}
Equations
- convex_cone.has_lt = {lt := Ξ» (S T : convex_cone π E), S.carrier β T.carrier}
Informal translation
Let $S$ be a convex cone in $E$. Then $x\in S$ if and only if $x\in\operatorname{span}(S)$.
Informal translation
Let $E$ be a commutative monoid with identity and let $s$ be a subset of $E$. Then $s$ is a convex cone if and only if $s$ is closed under scalar multiplication and addition.
Two convex_cones are equal if the underlying sets are equal.
Informal translation
Let $S$ and $T$ be convex cones in a vector space $E$ over an ordered field $K$. If $S$ and $T$ are equal as subsets of $E$, then $S$ and $T$ are equal as convex cones.
Two convex_cones are equal if and only if the underlying sets are equal.
Informal translation
Two convex cones $S$ and $T$ are equal if and only if their underlying sets are equal.
Two convex_cones are equal if they have the same elements.
Informal translation
Two convex cones $S$ and $T$ are equal if and only if $S\subset T$ and $T\subset S$.
Informal translation
Let $S$ be a convex cone in a vector space $E$ over a ordered field $K$. If $c>0$ and $x\in S$, then $cx\in S$.
Informal translation
Let $S$ be a convex cone in a vector space $E$ over a ordered field $K$. If $x,y\in S$, then $x+y\in S$.
Informal translation
Let $S$ and $T$ be convex cones in a vector space $E$ over an ordered field $K$. Then $S\cap T$ is a convex cone and $S\cap T=S\cap T$.
Informal translation
Let $S$ and $T$ be convex cones in a vector space $E$ over an ordered field $K$. Then $x\in S\cap T$ if and only if $x\in S$ and $x\in T$.
Equations
- convex_cone.has_Inf = {Inf := Ξ» (S : set (convex_cone π E)), {carrier := β (s : convex_cone π E) (H : s β S), βs, smul_mem' := _, add_mem' := _}}
Informal translation
Let $S$ be a set of convex cones in a vector space $E$ over an ordered field $K$. Then $x\in\bigcap S$ if and only if $x\in s$ for all $s\in S$.
Informal translation
The bottom of a convex cone is empty.
Informal translation
Let $E$ be a vector space over a field $K$ and let $x\in E$. Then $x\in\top$.
Equations
- convex_cone.complete_lattice π = {sup := Ξ» (a b : convex_cone π E), has_Inf.Inf {x : convex_cone π E | a β€ x β§ b β€ x}, le := has_le.le convex_cone.has_le, lt := has_lt.lt convex_cone.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf convex_cone.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := Ξ» (s : set (convex_cone π E)), has_Inf.Inf {T : convex_cone π E | β (S : convex_cone π E), S β s β S β€ T}, le_Sup := _, Sup_le := _, Inf := has_Inf.Inf convex_cone.has_Inf, Inf_le := _, le_Inf := _, top := β€, bot := β₯, le_top := _, bot_le := _}
Equations
- convex_cone.inhabited π = {default := β₯}
Informal translation
Let $S$ be a convex cone in a vector space $E$ over a ordered field $K$. Then $S$ is a convex set.
Informal translation
Let $S$ be a convex cone in a vector space $E$ over a linearly ordered field $K$. Then $cx\in S$ if and only if $x\in S$ for all $c\in K$ with $c>0$.
The image of a convex cone under a π-linear map is a convex cone.
Informal translation
Let $E, F, G$ be vector spaces over a linear ordered field $\mathbb{K}$. Let $f:E\to F$ and $g:F\to G$ be linear maps. Then $g\circ f$ is a linear map from $E$ to $G$ and $(g\circ f)(S)=g(f(S))$ for any convex cone $S$ in $E$.
Informal translation
Let $S$ be a convex cone in a vector space $E$ over a linear ordered field $K$. Then the identity map on $E$ maps $S$ to itself.
The preimage of a convex cone under a π-linear map is a convex cone.
Informal translation
Let $E$ be a vector space over a field $\mathbb{K}$ and let $S$ be a convex cone in $E$. Then the convex cone $S$ is equal to the image of $S$ under the identity map.
Informal translation
Let $E, F, G$ be vector spaces over a field $\mathbb{K}$ and let $S$ be a convex cone in $G$. Then the composition of the linear maps $g:F\to G$ and $f:E\to F$ induces a linear map $g\circ f:E\to G$. Then the convex cone $S$ is mapped to a convex cone in $E$ by $g\circ f$ if and only if $S$ is mapped to a convex cone in $F$ by $g$ and then to a convex cone in $E$ by $f$.
Informal translation
Let $f:E\to F$ be a linear map between two vector spaces over a linear ordered field $K$. Let $S$ be a convex cone in $F$. Then $x\in E$ is in the preimage of $S$ under $f$ if and only if $f(x)$ is in $S$.
Constructs an ordered module given an ordered_add_comm_group, a cone, and a proof that
the order relation is the one defined by the cone.
Informal translation
Let $S$ be a convex cone in a vector space $E$ over a linear ordered field $K$. Suppose that for all $x,y\in E$, $x\leq y$ if and only if $y-x\in S$. Then $E$ is an ordered $K$-module.
Convex cones with extra properties #
A convex cone is pointed if it includes 0.
A convex cone is blunt if it doesn't include 0.
Informal translation
A convex cone $S$ is pointed if and only if it is not blunt.
Informal translation
A convex cone $S$ is blunt if and only if $S$ is not pointed.
A convex cone is flat if it contains some nonzero vector x and its opposite -x.
A convex cone is salient if it doesn't include x and -x for any nonzero x.
Informal translation
A convex cone $S$ is salient if and only if it is not flat.
A flat cone is always pointed (contains 0).
Informal translation
Let $S$ be a convex cone in a vector space $E$ over an ordered field $K$. If $S$ is flat, then $S$ is pointed.
A blunt cone (one not containing 0) is always salient.
Informal translation
Let $S$ be a convex cone in a vector space $E$ over an ordered field $K$. If $S$ is blunt, then $S$ is salient.
A pointed convex cone defines a preorder.
A pointed and salient cone defines a partial order.
Equations
- S.to_partial_order hβ hβ = {le := preorder.le (S.to_preorder hβ), lt := preorder.lt (S.to_preorder hβ), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
A pointed and salient cone defines an ordered_add_comm_group.
Equations
- S.to_ordered_add_comm_group hβ hβ = {add := add_comm_group.add (show add_comm_group E, from _inst_2), add_assoc := _, zero := add_comm_group.zero (show add_comm_group E, from _inst_2), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (show add_comm_group E, from _inst_2), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (show add_comm_group E, from _inst_2), sub := add_comm_group.sub (show add_comm_group E, from _inst_2), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (show add_comm_group E, from _inst_2), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := partial_order.le (S.to_partial_order hβ hβ), lt := partial_order.lt (S.to_partial_order hβ hβ), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
Positive cone of an ordered module #
The positive cone is the convex cone formed by the set of nonnegative elements in an ordered module.
The positive cone of an ordered module is always salient.
Informal translation
The positive cone of an ordered vector space is salient.
The positive cone of an ordered module is always pointed.
Informal translation
The positive cone of an ordered vector space is pointed.
Cone over a convex set #
The set of vectors proportional to those in a convex set forms a convex cone.
Informal translation
Let $E$ be a vector space over a linear ordered field $K$ and let $s$ be a convex subset of $E$. Then $x\in\operatorname{cone}(s)$ if and only if there is a $c\in K$ such that $c>0$ and there is a $y\in s$ such that $c\cdot y=x$.
Informal translation
Let $E$ be a vector space over a linear ordered field $K$ and let $s$ be a convex subset of $E$. Then $x\in\operatorname{cone}(s)$ if and only if there is a $c\in K$ such that $0
Informal translation
Let $E$ be a vector space over a linear ordered field $K$ and let $s$ be a convex subset of $E$. Then $s$ is contained in the convex cone generated by $s$.
hs.to_cone s is the least cone that includes s.
Informal translation
Let $E$ be a vector space over a linear ordered field $K$ and let $s$ be a convex subset of $E$. Then the convex cone generated by $s$ is the smallest convex cone containing $s$.
Informal translation
Let $E$ be a vector space over a linear ordered field $K$ and let $s$ be a convex subset of $E$. Then the convex cone generated by $s$ is the intersection of all convex cones containing $s$.
Informal translation
The convex hull of a set $S$ is the smallest convex cone containing $S$.
Informal translation
The convex hull of a set $S$ is the smallest convex cone containing $S$.
M. Riesz extension theorem #
Given a convex cone s in a vector space E, a submodule p, and a linear f : p β β, assume
that f is nonnegative on p β© s and p + s = E. Then there exists a globally defined linear
function g : E β β that agrees with f on p, and is nonnegative on s.
We prove this theorem using Zorn's lemma. riesz_extension.step is the main part of the proof.
It says that if the domain p of f is not the whole space, then f can be extended to a larger
subspace p β span β {y} without breaking the non-negativity condition.
In riesz_extension.exists_top we use Zorn's lemma to prove that we can extend f
to a linear map g on β€ : submodule E. Mathematically this is the same as a linear map on E
but in Lean β€ : submodule E is isomorphic but is not equal to E. In riesz_extension
we use this isomorphism to prove the theorem.
Induction step in M. Riesz extension theorem. Given a convex cone s in a vector space E,
a partially defined linear map f : f.domain β β, assume that f is nonnegative on f.domain β© p
and p + s = E. If f is not defined on the whole E, then we can extend it to a larger
submodule without breaking the non-negativity condition.
Informal translation
Let $E$ be an additive commutative group and a $\mathbb{R}$-module. Let $s$ be a convex cone in $E$. Let $f:E\to\mathbb{R}$ be a linear map. Suppose that $f$ is nonnegative on $s$, that $s$ is dense in $E$, and that $f$ is not surjective. Then there is a linear map $g:E\to\mathbb{R}$ such that $f
Informal translation
Let $E$ be a real vector space and let $s$ be a convex cone in $E$. Let $p$ be a linear positive map from $E$ to $\mathbb{R}$ such that $p(x)\geq 0$ for all $x\in s$ and such that $s$ is dense in $E$. Then there exists a linear positive map $q$ from $E$ to $\mathbb{R}$ such that $q\geq p$ and $q$ is defined on all of $E$.
M. Riesz extension theorem: given a convex cone s in a vector space E, a submodule p,
and a linear f : p β β, assume that f is nonnegative on p β© s and p + s = E. Then
there exists a globally defined linear function g : E β β that agrees with f on p,
and is nonnegative on s.
Informal translation
Let $E$ be a real vector space and let $s$ be a convex cone in $E$. Let $f:E\to\mathbb{R}$ be a linear map. Suppose that $f$ is nonnegative on $s$ and that $s$ is dense in $E$. Then there is a linear map $g:E\to\mathbb{R}$ such that $g$ agrees with $f$ on $s$ and $g$ is nonnegative on $s$.
Hahn-Banach theorem: if N : E β β is a sublinear map, f is a linear map
defined on a subspace of E, and f x β€ N x for all x in the domain of f,
then f can be extended to the whole space to a linear map g such that g x β€ N x
for all x.
Informal translation
Let $E$ be an additive commutative group and a real module. Let $f:E\to\mathbb{R}$ be a linear map. Let $N:E\to\mathbb{R}$ be a function such that $N(cx)=cN(x)$ for all $c>0$ and $N(x+y)\leq N(x)+N(y)$ for all $x,y\in E$. Suppose that $f(x)\leq N(x)$ for all $x\in E$. Then there exists a linear map $g:E\to\mathbb{R}$ such that $g(x
The dual cone #
The dual cone is the cone consisting of all points y such that for
all points x in a given set 0 β€ βͺ x, y β«.
Equations
- s.inner_dual_cone = {carrier := {y : H | β (x : H), x β s β 0 β€ has_inner.inner x y}, smul_mem' := _, add_mem' := _}
Informal translation
Let $H$ be a real inner product space and let $s$ be a subset of $H$. Then $y\in s^\circ$ if and only if $x\in s$ implies $\langle x,y\rangle\geq 0$.
Informal translation
The inner dual cone of the empty set is the whole space.
Informal translation
Let $H$ be a real inner product space and let $s, t$ be subsets of $H$. If $t\subset s$, then $s^\circ\subset t^\circ$.
Informal translation
Let $H$ be a real inner product space and let $s$ be a subset of $H$. Then the dual cone of $s$ is pointed.