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

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`

.