Approximation to convex functions

In this file we show that a convex lower-semicontinuous function is the upper envelope of a family of continuous affine linear functions. We follow the proof in [Bou87].

Main Statement

• sSup_affine_eq : 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.
• sSup_of_countable_affine_eq : Suppose E is a HereditarilyLindelofSpace. A function φ : E → ℝ that is convex and lower-semicontinuous on a closed convex subset s is the supremum of a family of countably many functions that are the restrictions to s of continuous affine linear functions.

theorem ConvexOn.convex_re_epigraph {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [RCLike 𝕜] [AddCommMonoid E] [Module ℝ E] (hφcv : ConvexOn ℝ s φ) : Convex ℝ {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ RCLike.re p.2}

theorem LowerSemicontinuousOn.isClosed_re_epigraph {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [RCLike 𝕜] [TopologicalSpace E] (hsc : IsClosed s) (hφ_cont : LowerSemicontinuousOn φ s) : IsClosed {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ RCLike.re p.2}

theorem ConvexOn.exists_affine_le_of_lt {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [RCLike 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] {x : E} {a : ℝ} (hx : x ∈ s) (hax : a < φ x) (hsc : IsClosed s) (hφc : LowerSemicontinuousOn φ s) (hφcv : ConvexOn ℝ s φ) : ∃ (l : E →L[𝕜] 𝕜) (c : ℝ), s.restrict (⇑RCLike.re ∘ ⇑l) + Function.const (↑s) c ≤ s.restrict φ ∧ RCLike.re (l x) + c = a

Let φ : E → ℝ be a convex and lower-semicontinuous function on a closed convex subset s. For any point x ∈ s and a < φ x, there exists a continuous affine linear function f in E such that f ≤ φ on s and f x = a. This is an auxiliary lemma used in the proof of ConvexOn.sSup_affine_eq.

theorem ConvexOn.sSup_affine_eq {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [RCLike 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] (hsc : IsClosed s) (hφc : LowerSemicontinuousOn φ s) (hφcv : ConvexOn ℝ s φ) : sSup {f : ↑s → ℝ | f ≤ s.restrict φ ∧ ∃ (l : E →L[𝕜] 𝕜) (c : ℝ), f = s.restrict (⇑RCLike.re ∘ ⇑l) + Function.const (↑s) c} = s.restrict φ

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.

theorem ConvexOn.sSup_of_countable_affine_eq {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [RCLike 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E] (hsc : IsClosed s) (hφc : LowerSemicontinuousOn φ s) (hφcv : ConvexOn ℝ s φ) : ∃ (𝓕' : Set (↑s → ℝ)), 𝓕'.Countable ∧ sSup 𝓕' = s.restrict φ ∧ ∀ f ∈ 𝓕', ∃ (l : E →L[𝕜] 𝕜) (c : ℝ), f = s.restrict (⇑RCLike.re ∘ ⇑l) + Function.const (↑s) c

The countable version of sSup_affine_eq.

theorem ConvexOn.sSup_of_nat_affine_eq {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [RCLike 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E] (hsc : IsClosed s) (hφc : LowerSemicontinuousOn φ s) (hφcv : ConvexOn ℝ s φ) : ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ), ⨆ (i : ℕ), s.restrict (⇑RCLike.re ∘ ⇑(l i)) + Function.const (↑s) (c i) = s.restrict φ

The sequential version of sSup_of_countable_affine_eq.

theorem ConvexOn.univ_sSup_affine_eq {𝕜 : Type u_1} {E : Type u_2} {φ : E → ℝ} [RCLike 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] (hφc : LowerSemicontinuous φ) (hφcv : ConvexOn ℝ Set.univ φ) : sSup {f : E → ℝ | f ≤ φ ∧ ∃ (l : E →L[𝕜] 𝕜) (c : ℝ), f = ⇑RCLike.re ∘ ⇑l + Function.const E c} = φ

A function φ : E → ℝ that is convex and lower-semicontinuous is the supremum of a family of of continuous affine linear functions.

theorem ConvexOn.univ_sSup_of_countable_affine_eq {𝕜 : Type u_1} {E : Type u_2} {φ : E → ℝ} [RCLike 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E] (hφc : LowerSemicontinuous φ) (hφcv : ConvexOn ℝ Set.univ φ) : ∃ (𝓕' : Set (E → ℝ)), 𝓕'.Countable ∧ sSup 𝓕' = φ ∧ ∀ f ∈ 𝓕', ∃ (l : E →L[𝕜] 𝕜) (c : ℝ), f = ⇑RCLike.re ∘ ⇑l + Function.const E c

The countable version of univ_sSup_affine_eq.

theorem ConvexOn.univ_sSup_of_nat_affine_eq {𝕜 : Type u_1} {E : Type u_2} {φ : E → ℝ} [RCLike 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E] (hφc : LowerSemicontinuous φ) (hφcv : ConvexOn ℝ Set.univ φ) : ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ), ⨆ (i : ℕ), ⇑RCLike.re ∘ ⇑(l i) + Function.const E (c i) = φ

The sequential version of univ_sSup_of_countable_affine_eq.

theorem ConvexOn.real_sSup_affine_eq {E : Type u_2} {s : Set E} {φ : E → ℝ} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] (hsc : IsClosed s) (hφc : LowerSemicontinuousOn φ s) (hφcv : ConvexOn ℝ s φ) : sSup {f : ↑s → ℝ | f ≤ s.restrict φ ∧ ∃ (l : E →L[ℝ] ℝ) (c : ℝ), f = s.restrict ⇑l + Function.const (↑s) c} = s.restrict φ

The real version of sSup_affine_eq.

theorem ConvexOn.real_sSup_of_countable_affine_eq {E : Type u_2} {s : Set E} {φ : E → ℝ} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E] (hsc : IsClosed s) (hφc : LowerSemicontinuousOn φ s) (hφcv : ConvexOn ℝ s φ) : ∃ (𝓕' : Set (↑s → ℝ)), 𝓕'.Countable ∧ sSup 𝓕' = s.restrict φ ∧ ∀ f ∈ 𝓕', ∃ (l : E →L[ℝ] ℝ) (c : ℝ), f = s.restrict ⇑l + Function.const (↑s) c

The real version of sSup_of_countable_affine_eq.

theorem ConvexOn.real_sSup_of_nat_affine_eq {E : Type u_2} {s : Set E} {φ : E → ℝ} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E] (hsc : IsClosed s) (hφc : LowerSemicontinuousOn φ s) (hφcv : ConvexOn ℝ s φ) : ∃ (l : ℕ → E →L[ℝ] ℝ) (c : ℕ → ℝ), ⨆ (i : ℕ), s.restrict ⇑(l i) + Function.const (↑s) (c i) = s.restrict φ

The real version of sSup_of_nat_affine_eq.

theorem ConvexOn.real_univ_sSup_affine_eq {E : Type u_2} {φ : E → ℝ} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] (hφc : LowerSemicontinuous φ) (hφcv : ConvexOn ℝ Set.univ φ) : sSup {f : E → ℝ | f ≤ φ ∧ ∃ (l : E →L[ℝ] ℝ) (c : ℝ), f = ⇑l + Function.const E c} = φ

The real version of univ_sSup_affine_eq.

theorem ConvexOn.real_univ_sSup_of_countable_affine_eq {E : Type u_2} {φ : E → ℝ} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E] (hφc : LowerSemicontinuous φ) (hφcv : ConvexOn ℝ Set.univ φ) : ∃ (𝓕' : Set (E → ℝ)), 𝓕'.Countable ∧ sSup 𝓕' = φ ∧ ∀ f ∈ 𝓕', ∃ (l : E →L[ℝ] ℝ) (c : ℝ), f = ⇑l + Function.const E c

The real version of univ_sSup_of_countable_affine_eq.

theorem ConvexOn.real_univ_sSup_of_nat_affine_eq {E : Type u_2} {φ : E → ℝ} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E] (hφc : LowerSemicontinuous φ) (hφcv : ConvexOn ℝ Set.univ φ) : ∃ (l : ℕ → E →L[ℝ] ℝ) (c : ℕ → ℝ), ⨆ (i : ℕ), ⇑(l i) + Function.const E (c i) = φ

The real version of univ_sSup_of_nat_affine_eq.