Convex cones
In a vector space E over ℝ, we define a convex cone as a subset 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 semimodules.
We also define convex.to_cone to be the minimal cone that includes a given convex set.
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 is a bundled convex cone.
References
- https://en.wikipedia.org/wiki/Convex_cone
TODO
- Define the dual cone.
Definition of convex_cone and basic properties
Equations
- convex_cone.has_coe = {coe := convex_cone.carrier _inst_2}
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_cones are equal if the underlying subsets are equal.
Two convex_cones are equal if and only if the underlying subsets are equal.
Two convex_cones 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), 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 := _, top := ⊤, le_top := _, bot := ⊥, bot_le := _, Sup := λ (s : set (convex_cone E)), Inf {T : convex_cone E | ∀ (S : convex_cone E), S ∈ s → S ≤ T}, Inf := Inf convex_cone.has_Inf, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
Equations
The image of a convex cone under an ℝ-linear map is a convex cone.
The preimage of a convex cone under an ℝ-linear map is a convex cone.
Constructs an ordered semimodule given an ordered_add_comm_group, a cone, and a proof that
the order relation is the one defined by the cone.
Equations
- S.to_ordered_semimodule h = {to_semimodule := _inst_8, smul_lt_smul_of_pos := _, lt_of_smul_lt_smul_of_nonneg := _}
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 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_1), add_assoc := _, zero := add_comm_group.zero (show add_comm_group E, from _inst_1), zero_add := _, add_zero := _, neg := add_comm_group.neg (show add_comm_group E, from _inst_1), 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 semimodule
The positive cone is the convex cone formed by the set of nonnegative elements in an ordered semimodule.
The positive cone of an ordered semimodule is always salient.
The positive cone of an ordered semimodule 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.