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 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.
TODO
Define predicates
blunt,pointed,flat,sailent, see WikipediaDefine 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), 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 := _, top := ⊤, le_top := _, bot := ⊥, bot_le := _, Sup := λ (s : set (convex_cone E)), has_Inf.Inf {T : convex_cone E | ∀ (S : convex_cone E), S ∈ s → S ≤ T}, Inf := has_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.
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.