Documentation

Mathlib.Analysis.Convex.Cone.Extension

Extension theorems #

We prove two extension theorems:

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 : ConvexCone E) (f : E →ₗ.[] ) (nonneg : ∀ (x : f.domain), x s0 f x) (dense : ∀ (y : E), ∃ (x : f.domain), x + y s) (hdom : f.domain ) :
∃ (g : E →ₗ.[] ), 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} [AddCommGroup E] [Module E] (s : ConvexCone E) (p : E →ₗ.[] ) (hp_nonneg : ∀ (x : p.domain), x s0 p x) (hp_dense : ∀ (y : E), ∃ (x : p.domain), x + y s) :
qp, q.domain = ∀ (x : q.domain), x s0 q x
theorem riesz_extension {E : Type u_2} [AddCommGroup E] [Module E] (s : ConvexCone E) (f : E →ₗ.[] ) (nonneg : ∀ (x : f.domain), x s0 f x) (dense : ∀ (y : E), ∃ (x : f.domain), x + y s) :
∃ (g : E →ₗ[] ), (∀ (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} [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.