# Documentation

Mathlib.Analysis.Convex.Cone.Extension

# Extension theorems #

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

### 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. RieszExtension.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 RieszExtension.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 RieszExtension.step {E : Type u_2} [] [] (s : ) (f : ) (nonneg : ∀ (x : f.domain), x s0 f x) (dense : ∀ (y : E), ∃ (x : f.domain), x + y s) (hdom : f.domain ) :
∃ (g : ), f < g ∀ (x : g.domain), x s0 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.

theorem RieszExtension.exists_top {E : Type u_2} [] [] (s : ) (p : ) (hp_nonneg : ∀ (x : p.domain), x s0 p x) (hp_dense : ∀ (y : E), ∃ (x : p.domain), x + y s) :
∃ q ≥ p, q.domain = ∀ (x : q.domain), x s0 q x
theorem riesz_extension {E : Type u_2} [] [] (s : ) (f : ) (nonneg : ∀ (x : f.domain), x s0 f x) (dense : ∀ (y : E), ∃ (x : f.domain), x + y s) :
∃ (g : ), (∀ (x : f.domain), g x = f x) xs, 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.

theorem exists_extension_of_le_sublinear {E : Type u_2} [] [] (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.