Theorems · Theorem · functional analysis

riesz_extension

• 1000+ list: M. Riesz extension theorem

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

Defined in

Mathlib.Analysis.Convex.Cone.Extension

Cited by

1 results in Mathlib

Foundations

Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupModule