Relative interiors, interiors and affine hulls from the support function

The support function of a set records the closed half-spaces containing it, and therefore knows the closed convex hull exactly: x ∈ cl (conv s) if and only if ⟨x, y⟩ ≤ δ*(y ∣ s) for every y. In finite dimensions it knows more — the relative interior, the interior and the affine hull of a convex set can all be read off from which of those inequalities are strict.

The dividing line is the set of directions in which the support function is additively reversible, -δ*(-y ∣ C) = δ*(y ∣ C). These are exactly the directions in which ⟨·, y⟩ is constant on C, i.e. along which C lies inside a hyperplane; no inequality can be strict there. The relative interior asks for strictness everywhere else; the interior asks for strictness in every direction but 0, so there are no reversible directions to spare; and the affine hull asks for equality in the reversible directions and nothing at all elsewhere.

Main results

• supportFn_neg_eq_neg_iff, neg_supportFn_neg_eq_iff — the reversible directions of a support function are its directions of constancy.
• mem_relint_iff_lt_supportFn, mem_interior_iff_lt_supportFn — the ri and int clauses (Theorem 13.1 in [^1]).
• mem_affineSpan_iff_eq_supportFn — the aff clause: the affine hull of a set is the intersection of the hyperplanes containing it. No convexity is needed.
• isBounded_iff_forall_bddAbove — a set is bounded in the norm exactly when its support function is finite everywhere.

The closure clause is mem_closure_convexHull_iff_le_supportFn, in Duality/Support.lean; it is the one clause of the four that holds in any locally convex space.

Divergences from the reference

All three clauses here are genuinely finite-dimensional. Let φ be a discontinuous linear functional and C = ker φ, a dense proper subspace: then aff C = ri C = C while int C = ∅, and since a continuous functional constant on a dense set vanishes, the reversible directions of δ*(· ∣ C) are exactly the y with ⟨·, y⟩ = 0 and δ*(y ∣ C) = +∞ elsewhere. All three conditions are then satisfied by every point of the space.

The int clause carries two hypotheses the book does not write. B.SeparatingRight: over ℝⁿ paired with itself, y ≠ 0 and ⟨·, y⟩ ≠ 0 are the same condition, but over a general pairing a y ≠ 0 pairing trivially with E would demand ⟨x, y⟩ = 0 < δ*(y ∣ C) = 0. C.Nonempty: for C = ∅ the condition is false as soon as some y ≠ 0 exists, and vacuously true over the zero space, where int ∅ = ∅.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §13 and §1.

Directions of constancy

theorem Tdaf.ConvexAnalysis.supportFn_eq_coe_of_forall_eq {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} {y : F} (hs : s.Nonempty) {c : ℝ} (h : ∀ x ∈ s, (B x) y = c) : supportFn B s y = ↑c

The support function in a direction of constancy is that constant.

theorem Tdaf.ConvexAnalysis.supportFn_neg_eq_neg_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} (hs : s.Nonempty) (y : F) : supportFn B s (-y) = -supportFn B s y ↔ ∃ (c : ℝ), ∀ x ∈ s, (B x) y = c

A support function is additively reversible in the direction y exactly when ⟨·, y⟩ is constant on the set: δ*(-y | s) = -δ*(y | s) says that the supremum and the infimum of ⟨·, y⟩ over s agree. Nonemptiness is needed — for s = ∅ both sides are -∞ and -(-∞) = +∞.

theorem Tdaf.ConvexAnalysis.neg_supportFn_neg_eq_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Set E} (hs : s.Nonempty) (y : F) : -supportFn B s (-y) = supportFn B s y ↔ ∃ (c : ℝ), ∀ x ∈ s, (B x) y = c

supportFn_neg_eq_neg_iff in the orientation the clauses below use: -δ*(-y | s) = δ*(y | s).

The relative interior, the interior and the affine hull

theorem Tdaf.ConvexAnalysis.exists_forall_eq_of_notMem_affineSpan {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {C : Set E} (hne : C.Nonempty) {x : E} (hx : x ∉ affineSpan ℝ C) : ∃ (y : F) (c : ℝ), (∀ z ∈ C, (B z) y = c) ∧ (B x) y ≠ c

A point outside the affine hull is cut away from it by a direction of constancy. The affine hull is closed because the dimension is finite, so a point outside it is strongly separated from it, and a functional bounded below on an affine set is constant on it.

theorem Tdaf.ConvexAnalysis.mem_relint_iff_lt_supportFn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {C : Set E} (hC : Convex ℝ C) (x : E) : x ∈ intrinsicInterior ℝ C ↔ (∀ (y : F), ↑((B x) y) ≤ supportFn B C y) ∧ ∀ (y : F), -supportFn B C (-y) ≠ supportFn B C y → ↑((B x) y) < supportFn B C y

The ri clause: a point lies in the relative interior of a convex set exactly when it satisfies every inequality the support function records, strictly in every direction in which the support function is not additively reversible.

Read through the pairing: ⟨x, y⟩ ≤ δ*(y | C) is an equality precisely when ⟨·, y⟩ attains its maximum over C at x, and that is compatible with x ∈ ri C only for a ⟨·, y⟩ constant on C.

theorem Tdaf.ConvexAnalysis.mem_interior_iff_lt_supportFn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {C : Set E} (hC : Convex ℝ C) (hne : C.Nonempty) (hB : B.SeparatingRight) (x : E) : x ∈ interior C ↔ ∀ (y : F), y ≠ 0 → ↑((B x) y) < supportFn B C y

The int clause: a point lies in the interior of a nonempty convex set exactly when it satisfies strictly every inequality the support function records in a nonzero direction. The relative interior is the interior exactly when 0 is the only reversible direction, and asking for strictness in every nonzero direction asks for both at once.

theorem Tdaf.ConvexAnalysis.mem_affineSpan_iff_eq_supportFn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {C : Set E} (hne : C.Nonempty) (x : E) : x ∈ affineSpan ℝ C ↔ ∀ (y : F), -supportFn B C (-y) = supportFn B C y → ↑((B x) y) = supportFn B C y

The aff clause: the affine hull of a nonempty set is the set of points satisfying with equality every inequality the support function records reversibly. Convexity is not needed.

Boundedness in the norm

theorem Tdaf.ConvexAnalysis.isBounded_iff_forall_bddAbove {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {C : Set E} : Bornology.IsBounded C ↔ ∀ (y : F), ∃ (c : ℝ), ∀ x ∈ C, (B x) y ≤ c

Boundedness in the norm: in finite dimensions a set is bounded in the norm exactly when every ⟨·, y⟩ is bounded above on it, i.e. exactly when its support function is finite everywhere.

exists_supportFn_finite_iff states the same equivalence with "bounded" read in the pairing sense, and holds in any locally convex space. What is finite-dimensional here is the upgrade to Bornology.IsBounded, a coordinate estimate against a finite basis.