English
Let s be a convex cone in a real vector space E, let p be a submodule (subspace) of E, and let f be a linear map from p to R. Suppose f is nonnegative on p ∩ s and p + s = E. Then there exists a linear map g : E → R extending f (i.e., g|p = f) and such that g is nonnegative on s.
Русский
Пусть s — выпуклый конус в вещественном векторном пространстве E, p — его подсдержка (подпространство) и f: p → R — линейное отображение, удовлетворяющее неотрицательности на p ∩ s и p + s = E. Тогда существует линейное отображение g: E → R, которое расширяет f и сохраняет неотрицательность на s.
LaTeX
$$$\\text{Let }s\\subset E\\text{ be a convex cone }p\\le E\\text{ a subspace},\\ f: p\\to\\mathbb{R}\\text{ linear},\\ f(x)\\ge 0\\text{ for all }x\\in p\\cap s\\text{ and }p+s=E. \\\\ \\text{Then }\\exists g:E\\to\\mathbb{R}\\text{ linear with }g|_p=f\\text{ and }g(x)\\ge 0\\text{ for all }x\\in s.$$$
Lean4
/-- 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 riesz_extension (s : ConvexCone ℝ E) (f : E →ₗ.[ℝ] ℝ) (nonneg : ∀ x : f.domain, (x : E) ∈ s → 0 ≤ f x)
(dense : ∀ y, ∃ x : f.domain, (x : E) + y ∈ s) : ∃ g : E →ₗ[ℝ] ℝ, (∀ x : f.domain, g x = f x) ∧ ∀ x ∈ s, 0 ≤ g x :=
by
rcases RieszExtension.exists_top s f nonneg dense with ⟨⟨g_dom, g⟩, ⟨-, hfg⟩, rfl : g_dom = ⊤, hgs⟩
refine ⟨g.comp (LinearMap.id.codRestrict ⊤ fun _ ↦ trivial), ?_, ?_⟩
· exact fun x => (hfg rfl).symm
· exact fun x hx => hgs ⟨x, _⟩ hx
