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} [AddCommGroup E] [Module ℝ E] (s : PointedCone ℝ E) (f : E →ₗ.[ℝ] ℝ) (nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x) (dense : ∀ (y : E), ∃ (x : ↥f.domain), ↑x + y ∈ s) (hdom : f.domain ≠ ⊤) : ∃ (g : E →ₗ.[ℝ] ℝ), 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.

theorem RieszExtension.exists_top {E : Type u_2} [AddCommGroup E] [Module ℝ E] (s : PointedCone ℝ E) (p : E →ₗ.[ℝ] ℝ) (hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x) (hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), ↑x + y ∈ s) : ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), ↑x ∈ s → 0 ≤ ↑q x

theorem riesz_extension {E : Type u_2} [AddCommGroup E] [Module ℝ E] (s : PointedCone ℝ E) (f : E →ₗ.[ℝ] ℝ) (nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x) (dense : ∀ (y : E), ∃ (x : ↥f.domain), ↑x + y ∈ s) : ∃ (g : E →ₗ[ℝ] ℝ), (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ 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.

theorem exists_extension_of_le_sublinear {E : Type u_2} [AddCommGroup E] [Module ℝ E] (f : E →ₗ.[ℝ] ℝ) (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 : E →ₗ[ℝ] ℝ), (∀ (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.