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 ifs
is a convex cone in a real vector spaceE
,p
is a submodule ofE
such thatp + s = E
, andf
is a linear functionp β β
which is nonnegative onp β© s
, then there exists a globally defined linear functiong : E β β
that agrees withf
onp
, and is nonnegative ons
.exists_extension_of_le_sublinear
: Hahn-Banach theorem: ifN : E β β
is a sublinear map,f
is a linear map defined on a subspace ofE
, andf x β€ N x
for allx
in the domain off
, thenf
can be extended to the whole space to a linear mapg
such thatg x β€ N x
for 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}
Two convex_cone
s are equal if the underlying sets are equal.
Two convex_cone
s are equal if and only if the underlying sets are equal.
Two convex_cone
s are equal if they have the same elements.
Equations
- convex_cone.has_Inf = {Inf := Ξ» (S : set (convex_cone π E)), {carrier := β (s : convex_cone π E) (H : s β S), βs, smul_mem' := _, add_mem' := _}}
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 := β₯}
The image of a convex cone under a π
-linear map is a convex cone.
The preimage of a convex cone under a π
-linear map is a convex cone.
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.
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
.
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
.
A flat cone is always pointed (contains 0
).
A blunt cone (one not containing 0
) is always 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.
The positive cone of an ordered module is always pointed.
Cone over a convex set #
The set of vectors proportional to those in a convex set forms a convex cone.
hs.to_cone s
is the least cone that includes 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.
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
.
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
.
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' := _}