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

source
theorem RieszExtension.step {E : Type u_2} [AddCommGroup E] [Module ℝ E] (s : ConvexCone ℝ 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.

source
theorem RieszExtension.exists_top {E : Type u_2} [AddCommGroup E] [Module ℝ E] (s : ConvexCone ℝ 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
source
theorem riesz_extension {E : Type u_2} [AddCommGroup E] [Module ℝ E] (s : ConvexCone ℝ 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`.

source
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`.