Theorems · Theorem · functional analysis

ConvexOn.sSup_affine_eq

∀ {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E],
  IsClosed s →
    LowerSemicontinuousOn φ s →
      ConvexOn ℝ s φ →
        sSup {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑RCLike.re ∘ ⇑l) + Function.const (↑s) c} =
          s.domRestrict φ

A function φ : E → ℝ that is convex and lower-semicontinuous on a closed convex subset s is the supremum of a family of functions that are the restrictions to s of continuous affine linear functions in E.

Defined in

Mathlib.Analysis.Convex.Approximation

Cited by

3 results in Mathlib

Foundations

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

Assumes

RCLikeTopologicalSpaceAddCommGroupModuleModuleIsScalarTowerIsTopologicalAddGroupContinuousSMulLocallyConvexSpace