# mathlibdocumentation

analysis.convex.cone

# 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 if s is a convex cone in a real vector space E, p is a submodule of E such that p + s = E, and f is a linear function p β β which is nonnegative on p β© s, then there exists a globally defined linear function g : E β β that agrees with f on p, and is nonnegative on s.
• exists_extension_of_le_sublinear: 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

## 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 #

structure convex_cone (π : Type u_1) (E : Type u_2) [ordered_semiring π] [has_smul π E] :
Type u_2

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
@[protected, instance]
def convex_cone.set.has_coe {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] :
has_coe (convex_cone π E) (set E)
Equations
@[protected, instance]
def convex_cone.has_mem {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] :
(convex_cone π E)
Equations
@[protected, instance]
def convex_cone.has_le {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] :
has_le (convex_cone π E)
Equations
@[protected, instance]
def convex_cone.has_lt {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] :
has_lt (convex_cone π E)
Equations
@[simp, norm_cast]
theorem convex_cone.mem_coe {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) {x : E} :
Informal translation

Let $S$ be a convex cone in $E$. Then $x\in S$ if and only if $x\in\operatorname{span}(S)$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem convex_cone.mem_mk {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] {s : set E} {hβ : β β¦c : πβ¦, 0 < c β β β¦x : Eβ¦, x β s β c β’ x β s} {hβ : β β¦x : Eβ¦, x β s β β β¦y : Eβ¦, y β s β x + y β s} {x : E} :
x β {carrier := s, smul_mem' := hβ, add_mem' := hβ} β x β 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.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem convex_cone.ext' {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] {S T : convex_cone π E} (h : βS = βT) :
S = T

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.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
theorem convex_cone.ext'_iff {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] {S T : convex_cone π E} :

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.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[ext]
theorem convex_cone.ext {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] {S T : convex_cone π E} (h : β (x : E), x β S β x β T) :
S = T

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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem convex_cone.smul_mem {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) {c : π} {x : E} (hc : 0 < c) (hx : x β 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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem convex_cone.add_mem {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) β¦x : Eβ¦ (hx : x β S) β¦y : Eβ¦ (hy : y β S) :
x + y β 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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
def convex_cone.has_inf {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] :
has_inf (convex_cone π E)
Equations
theorem convex_cone.coe_inf {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S T : convex_cone π E) :
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem convex_cone.mem_inf {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S T : convex_cone π E) {x : E} :
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
def convex_cone.has_Inf {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] :
has_Inf (convex_cone π E)
Equations
theorem convex_cone.mem_Inf {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] {x : E} {S : set (convex_cone π E)} :
β β (s : convex_cone π E), s β S β x β s
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
def convex_cone.has_bot (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] :
has_bot (convex_cone π E)
Equations
theorem convex_cone.mem_bot (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] (x : E) :
Informal translation

The bottom of a convex cone is empty.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
def convex_cone.has_top (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] :
has_top (convex_cone π E)
Equations
theorem convex_cone.mem_top (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] (x : E) :
Informal translation

Let $E$ be a vector space over a field $K$ and let $x\in E$. Then $x\in\top$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
def convex_cone.complete_lattice (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] :
Equations
@[protected, instance]
def convex_cone.inhabited (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_smul π E] :
inhabited (convex_cone π E)
Equations
@[protected]
theorem convex_cone.convex {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] (S : convex_cone π E) :
convex π βS
Informal translation

Let $S$ be a convex cone in a vector space $E$ over a ordered field $K$. Then $S$ is a convex set.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem convex_cone.smul_mem_iff {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [mul_action π E] (S : convex_cone π E) {c : π} (hc : 0 < c) {x : E} :
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def convex_cone.map {π : Type u_1} {E : Type u_2} {F : Type u_3} [linear_ordered_field π] [module π E] [module π F] (f : E ββ[π] F) (S : convex_cone π E) :
convex_cone π F

The image of a convex cone under a π-linear map is a convex cone.

Equations
theorem convex_cone.map_map {π : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [linear_ordered_field π] [module π E] [module π F] [module π G] (g : F ββ[π] G) (f : E ββ[π] F) (S : convex_cone π E) :
S) = convex_cone.map (g.comp f) S
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem convex_cone.map_id {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (S : convex_cone π 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.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def convex_cone.comap {π : Type u_1} {E : Type u_2} {F : Type u_3} [linear_ordered_field π] [module π E] [module π F] (f : E ββ[π] F) (S : convex_cone π F) :
convex_cone π E

The preimage of a convex cone under a π-linear map is a convex cone.

Equations
@[simp]
theorem convex_cone.comap_id {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (S : convex_cone π E) :
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.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem convex_cone.comap_comap {π : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [linear_ordered_field π] [module π E] [module π F] [module π G] (g : F ββ[π] G) (f : E ββ[π] F) (S : convex_cone π G) :
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem convex_cone.mem_comap {π : Type u_1} {E : Type u_2} {F : Type u_3} [linear_ordered_field π] [module π E] [module π F] {f : E ββ[π] F} {S : convex_cone π F} {x : E} :
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem convex_cone.to_ordered_smul {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (S : convex_cone π E) (h : β (x y : E), x β€ y β y - x β S) :
ordered_smul π E

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.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?

### Convex cones with extra properties #

def convex_cone.pointed {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) :
Prop

A convex cone is pointed if it includes 0.

Equations
def convex_cone.blunt {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) :
Prop

A convex cone is blunt if it doesn't include 0.

Equations
theorem convex_cone.pointed_iff_not_blunt {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) :
Informal translation

A convex cone $S$ is pointed if and only if it is not blunt.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem convex_cone.blunt_iff_not_pointed {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) :
Informal translation

A convex cone $S$ is blunt if and only if $S$ is not pointed.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def convex_cone.flat {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) :
Prop

A convex cone is flat if it contains some nonzero vector x and its opposite -x.

Equations
def convex_cone.salient {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) :
Prop

A convex cone is salient if it doesn't include x and -x for any nonzero x.

Equations
theorem convex_cone.salient_iff_not_flat {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) :
Informal translation

A convex cone $S$ is salient if and only if it is not flat.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem convex_cone.flat.pointed {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] {S : convex_cone π E} (hS : S.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.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem convex_cone.blunt.salient {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] {S : convex_cone π E} :
S.blunt β S.salient

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.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def convex_cone.to_preorder {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) (hβ : S.pointed) :

A pointed convex cone defines a preorder.

Equations
def convex_cone.to_partial_order {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) (hβ : S.pointed) (hβ : S.salient) :

A pointed and salient cone defines a partial order.

Equations
def convex_cone.to_ordered_add_comm_group {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] (S : convex_cone π E) (hβ : S.pointed) (hβ : S.salient) :

A pointed and salient cone defines an ordered_add_comm_group.

Equations

### Positive cone of an ordered module #

def convex_cone.positive_cone (π : Type u_1) (E : Type u_2) [ordered_semiring π] [module π E] [ordered_smul π E] :
convex_cone π E

The positive cone is the convex cone formed by the set of nonnegative elements in an ordered module.

Equations
theorem convex_cone.salient_positive_cone (π : Type u_1) (E : Type u_2) [ordered_semiring π] [module π E] [ordered_smul π E] :

The positive cone of an ordered module is always salient.

Informal translation

The positive cone of an ordered vector space is salient.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem convex_cone.pointed_positive_cone (π : Type u_1) (E : Type u_2) [ordered_semiring π] [module π E] [ordered_smul π E] :

The positive cone of an ordered module is always pointed.

Informal translation

The positive cone of an ordered vector space is pointed.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?

### Cone over a convex set #

def convex.to_cone {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (s : set E) (hs : convex π s) :
convex_cone π E

The set of vectors proportional to those in a convex set forms a convex cone.

Equations
theorem convex.mem_to_cone {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] {s : set E} (hs : convex π s) {x : E} :
x β hs β β (c : π), 0 < c β§ β (y : E) (H : y β s), c β’ 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 $c>0$ and there is a $y\in s$ such that $c\cdot y=x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem convex.mem_to_cone' {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] {s : set E} (hs : convex π s) {x : E} :
x β hs β β (c : π), 0 < c β§ c β’ x β 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 $x\in\operatorname{cone}(s)$ if and only if there is a $c\in K$ such that $0 This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API. Does this translation look correct? theorem convex.subset_to_cone {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] {s : set E} (hs : convex π 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$s$is contained in the convex cone generated by$s$. This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API. Does this translation look correct? theorem convex.to_cone_is_least {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] {s : set E} (hs : convex π s) : is_least {t : convex_cone π E | s β βt} hs) 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$. This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API. Does this translation look correct? theorem convex.to_cone_eq_Inf {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] {s : set E} (hs : convex π s) : hs = has_Inf.Inf {t : convex_cone π E | s β βt} 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$. This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API. Does this translation look correct? theorem convex_hull_to_cone_is_least {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (s : set E) : is_least {t : convex_cone π E | s β βt} (convex.to_cone (β(convex_hull π) s) _) Informal translation The convex hull of a set$S$is the smallest convex cone containing$S$. This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API. Does this translation look correct? theorem convex_hull_to_cone_eq_Inf {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (s : set E) : convex.to_cone (β(convex_hull π) s) _ = has_Inf.Inf {t : convex_cone π E | s β βt} Informal translation The convex hull of a set$S$is the smallest convex cone containing$S$. This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API. Does this translation look correct? ### 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. theorem riesz_extension.step {E : Type u_2} [ E] (s : E) (f : β) (nonneg : β (x : β₯(f.domain)), βx β s β 0 β€ βf x) (dense : β (y : E), β (x : β₯(f.domain)), βx + y β s) (hdom : f.domain β β€) : β (g : , f < g β§ β (x : β₯(g.domain)), βx β s β 0 β€ βg x 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

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem riesz_extension.exists_top {E : Type u_2} [ E] (s : E) (p : β) (hp_nonneg : β (x : β₯(p.domain)), βx β s β 0 β€ βp x) (hp_dense : β (y : E), β (x : β₯(p.domain)), βx + y β s) :
β (q : (H : q β₯ p), β§ β (x : β₯(q.domain)), βx β s β 0 β€ βq x
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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem riesz_extension {E : Type u_2} [ E] (s : E) (f : β) (nonneg : β (x : β₯(f.domain)), βx β s β 0 β€ βf x) (dense : β (y : E), β (x : β₯(f.domain)), βx + y β s) :
β (g : , (β (x : β₯(f.domain)), βg βx = βf x) β§ β (x : E), x β s β 0 β€ βg x

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$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem exists_extension_of_le_sublinear {E : Type u_2} [ E] (f : β) (N : E β β) (N_hom : β (c : β), 0 < c β β (x : E), N (c β’ x) = c * N x) (N_add : β (x y : E), N (x + y) β€ N x + N y) (hf : β (x : β₯(f.domain)), βf x β€ N βx) :
β (g : , (β (x : β₯(f.domain)), βg βx = βf x) β§ β (x : E), βg x β€ N x

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 This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API. Does this translation look correct? ### The dual cone # def set.inner_dual_cone {H : Type u_5} (s : set H) : 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 theorem mem_inner_dual_cone {H : Type u_5} (y : H) (s : set H) : β β (x : H), x β s β 0 β€ 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$. This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API. Does this translation look correct? @[simp] theorem inner_dual_cone_empty {H : Type u_5} : Informal translation The inner dual cone of the empty set is the whole space. This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API. Does this translation look correct? theorem inner_dual_cone_le_inner_dual_cone {H : Type u_5} (s t : set H) (h : t β s) : 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$. This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API. Does this translation look correct? theorem pointed_inner_dual_cone {H : Type u_5} (s : set H) : 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.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?