Simplices, locally simplicial sets, and upper semicontinuity

A convex function is upper semicontinuous relative to any locally simplicial subset of its effective domain, so a closed convex function is continuous relative to such a set. This is the sharp form of "a convex function is continuous on a simplex in its domain": the phenomenon is genuinely about simplices and fails for arbitrary convex subsets of dom f. The application is an extension theorem: a finite convex function on ri C, bounded above on bounded subsets, extends uniquely to a continuous finite convex function on a locally simplicial convex C.

Main definitions

• IsSimplex S — S is the convex hull of a finite affinely independent family.
• LocallySimplicial S — every point of S has a neighbourhood in which S coincides with a finite union of simplices contained in S; every polyhedral convex set is one.

Main results

• ConvexFn.upperSemicontinuousWithinAt_convexHull_range — the analytic core: a convex function finite on the vertices of a simplex is upper semicontinuous relative to that simplex, at every one of its points.
• ConvexFn.upperSemicontinuousOn_of_locallySimplicial — the same, relative to any locally simplicial subset of dom f.
• ConvexFn.continuousOn_of_locallySimplicial — continuity there, for a closed f.
• exists_closedFn_continuousOn_of_locallySimplicial, eqOn_of_continuousOn_of_eqOn_relint — the extension theorem, existence and uniqueness.

Implementation notes

The analytic core needs no triangulation. Rockafellar reduces to the case where x is a vertex of the simplex by triangulating around x. Instead, writing x = Σ μᵢ vᵢ and z = Σ wᵢ vᵢ, every z whose weights satisfy wᵢ ≥ (1 - ε) μᵢ is (1 - ε) x + ε y with y again in the simplex, for a fixed ε chosen in advance from the target bound; convexity then bounds f z by (1 - ε) β + ε ν. That weight condition holds on a neighbourhood of x by compactness of the standard simplex, affine independence making the weights of a point unique — the only use of affine independence, and the only use of a topology: no metric, no finite dimension.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §10.

Barycentric weights

def Tdaf.ConvexAnalysis.weightPt {ι : Type u_1} [Fintype ι] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (v : ι → E) (w : ι → ℝ) : E

The point with barycentric weights w relative to the family v.

Equations

• Tdaf.ConvexAnalysis.weightPt v w = ∑ i : ι, w i • v i

theorem Tdaf.ConvexAnalysis.weightPt_eq_affineCombination {ι : Type u_1} [Fintype ι] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (v : ι → E) {w : ι → ℝ} (hw : ∑ i : ι, w i = 1) : weightPt v w = (Finset.affineCombination ℝ Finset.univ v) w

theorem Tdaf.ConvexAnalysis.convexHull_range_eq_image_stdSimplex {ι : Type u_1} [Fintype ι] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (v : ι → E) : (convexHull ℝ) (Set.range v) = weightPt v '' stdSimplex ℝ ι

A convex hull of finitely many points is the image of the standard simplex under the weight map.

theorem Tdaf.ConvexAnalysis.weightPt_combo {ι : Type u_1} [Fintype ι] {E : Type u_2} [AddCommGroup E] [Module ℝ E] (v : ι → E) (w₁ w₂ : ι → ℝ) (a b : ℝ) : (weightPt v fun (i : ι) => a * w₁ i + b * w₂ i) = a • weightPt v w₁ + b • weightPt v w₂

The weight map is affine in the weights: a convex combination of weight vectors gives the corresponding convex combination of points.

Simplices and locally simplicial sets

def Tdaf.ConvexAnalysis.IsSimplex {E : Type u_1} [AddCommGroup E] [Module ℝ E] (S : Set E) : Prop

A simplex: the convex hull of a finite affinely independent family of points.

Equations

• Tdaf.ConvexAnalysis.IsSimplex S = ∃ (ι : Type) (x : Fintype ι) (v : ι → E), AffineIndependent ℝ v ∧ S = (convexHull ℝ) (Set.range v)

def Tdaf.ConvexAnalysis.LocallySimplicial {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (S : Set E) : Prop

Rockafellar's locally simplicial sets: near each of its points, S agrees with a finite union of simplices contained in S. Such a set need be neither convex nor closed.

Equations

• One or more equations did not get rendered due to their size.

theorem Tdaf.ConvexAnalysis.IsSimplex.isCompact {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {S : Set E} (hS : IsSimplex S) : IsCompact S

A simplex is compact: it is the convex hull of a finite set.

The analytic core: upper semicontinuity relative to a simplex

theorem Tdaf.ConvexAnalysis.ConvexFn.upperSemicontinuousWithinAt_convexHull_range {ι : Type u_1} [Finite ι] {E : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] {f : E → EReal} (hf : ConvexFn f) {v : ι → E} (hv : AffineIndependent ℝ v) (hdom : ∀ (i : ι), v i ∈ dom f) {x : E} (hx : x ∈ (convexHull ℝ) (Set.range v)) : UpperSemicontinuousWithinAt f ((convexHull ℝ) (Set.range v)) x

A convex function whose value at each vertex of a simplex is < ⊤ is upper semicontinuous relative to that simplex, at every point of it.

Upper semicontinuity on a locally simplicial set

theorem Tdaf.ConvexAnalysis.ConvexFn.upperSemicontinuousOn_of_locallySimplicial {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] {f : E → EReal} {S : Set E} (hf : ConvexFn f) (hS : LocallySimplicial S) (hSdom : S ⊆ dom f) : UpperSemicontinuousOn f S

A convex function is upper semicontinuous relative to any locally simplicial subset of its effective domain.

theorem Tdaf.ConvexAnalysis.ConvexFn.continuousOn_of_locallySimplicial {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] {f : E → EReal} {S : Set E} (hf : ConvexFn f) (hlsc : LowerSemicontinuous f) (hS : LocallySimplicial S) (hSdom : S ⊆ dom f) : ContinuousOn f S

A closed convex function is continuous relative to any locally simplicial subset of its effective domain. Lower semicontinuity supplies one half of tendsto_order and upper semicontinuity the other.

Extension from the relative interior

theorem Tdaf.ConvexAnalysis.eqOn_of_continuousOn_of_eqOn_relint {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Convex ℝ C) {g₁ g₂ : E → EReal} (h₁ : ContinuousOn g₁ C) (h₂ : ContinuousOn g₂ C) (h : Set.EqOn g₁ g₂ (intrinsicInterior ℝ C)) : Set.EqOn g₁ g₂ C

ri C is dense in C, so two functions continuous relative to C that agree on ri C agree on all of C. This is the uniqueness half of the extension theorem, and it needs neither convexity of the functions nor local simpliciality of C.

theorem Tdaf.ConvexAnalysis.exists_closedFn_continuousOn_of_locallySimplicial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} {f : E → EReal} (hC : Convex ℝ C) (hCls : LocallySimplicial C) (hne : C.Nonempty) (hf : ConvexFn f) (hbot : ∀ (x : E), f x ≠ ⊥) (hdom : dom f = intrinsicInterior ℝ C) (hbdd : ∀ S ⊆ intrinsicInterior ℝ C, Bornology.IsBounded S → ∃ (c : ℝ), ∀ x ∈ S, f x ≤ ↑c) : ∃ (g : E → EReal), ConvexFn g ∧ ClosedFn g ∧ Proper g ∧ Set.EqOn g f (intrinsicInterior ℝ C) ∧ C ⊆ dom g ∧ ContinuousOn g C

The extension theorem, existence. A convex function finite exactly on ri C and bounded above on every bounded subset of ri C has a closure that is finite and continuous on the whole of a locally simplicial convex C, and still agrees with f on ri C. Uniqueness is eqOn_of_continuousOn_of_eqOn_relint.