Tangent half-spaces of a convex set

A hyperplane is tangent to a closed convex set C at a point y when it is the unique supporting hyperplane to C at y, and a tangent half-space is a supporting half-space whose boundary hyperplane is tangent. The theorem proved here is that a closed convex set with nonempty interior is the intersection of its tangent closed half-spaces — a sharpening of the statement that a closed convex set is the intersection of all the closed half-spaces containing it.

The interior hypothesis is not removable as stated: a closed convex set with empty interior lies in a proper affine subspace and has no tangent hyperplane anywhere, since every supporting hyperplane at a point can be tilted around that subspace. The right general statement intersects the tangent half-spaces within the affine hull and adds the affine hull itself.

Tangency is dual to exposedness: after translating so that 0 ∈ int C, the tangent half-spaces of C correspond exactly to the exposed points of the polar C°, and this correspondence carries the proof.

Main definitions

• IsSupportingAt C f y — y ∈ C and the linear functional f attains its maximum over C at y, so {z | f z ≤ f y} is a supporting half-space and {z | f z = f y} a supporting hyperplane.
• IsTangentAt C f y — that supporting hyperplane is the only one at y: every nonzero functional supported at y is a positive multiple of f.

Main results

• eq_iInter_tangent_halfSpaces — a closed convex set with nonempty interior is the intersection of the closed half-spaces tangent to it.
• exists_isTangentAt_lt_of_zero_mem_interior — the separating form: a point outside such a set is cut off by a tangent half-space.

Implementation notes

The proof stays in the polar picture rather than homogenising. After translating so that 0 ∈ int C, the polar C° is compact; Minkowski's theorem writes it as the hull of its extreme points, Straszewicz's theorem puts those in the closure of its exposed points, and the exposed points of C° are exactly the normals of the tangent half-spaces to C. So a point outside C is already excluded by the half-space of some exposed point of C°. Identifying an exposing functional on E* with a point of E, which produces the point of contact, uses reflexivity (Module.evalEquiv, packaged as exists_forall_apply_eq) — a step invisible in ℝⁿ.

References

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

Supporting and tangent hyperplanes

def Tdaf.ConvexAnalysis.IsSupportingAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (C : Set E) (f : StrongDual ℝ E) (y : E) : Prop

f supports C at y: the point y belongs to C and maximises f over C, so that {z | f z ≤ f y} is a supporting half-space and {z | f z = f y} a supporting hyperplane.

Equations

• Tdaf.ConvexAnalysis.IsSupportingAt C f y = (y ∈ C ∧ ∀ z ∈ C, f z ≤ f y)

def Tdaf.ConvexAnalysis.IsTangentAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (C : Set E) (f : StrongDual ℝ E) (y : E) : Prop

The hyperplane {z | f z = f y} is tangent to C at y: it supports C at y, and it is the only supporting hyperplane there. Uniqueness is stated up to a positive multiple of the functional — a hyperplane determines its functional up to a nonzero scalar, and the supporting inequality fixes the sign.

Equations

• Tdaf.ConvexAnalysis.IsTangentAt C f y = (f ≠ 0 ∧ Tdaf.ConvexAnalysis.IsSupportingAt C f y ∧ ∀ (g : StrongDual ℝ E), g ≠ 0 → (∀ z ∈ C, g z ≤ g y) → ∃ (a : ℝ), 0 < a ∧ g = a • f)

theorem Tdaf.ConvexAnalysis.IsTangentAt.subset_halfSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : StrongDual ℝ E} {y : E} (h : IsTangentAt C f y) : C ⊆ {z : E | f z ≤ f y}

A tangent half-space contains C.

theorem Tdaf.ConvexAnalysis.IsTangentAt.shift {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : StrongDual ℝ E} {y x₁ : E} (h : IsTangentAt {z : E | z + x₁ ∈ C} f y) : IsTangentAt C f (y + x₁)

Tangency is invariant under translation: {z | z + x₁ ∈ C} is C shifted by -x₁.

A convex set is the intersection of its tangent half-spaces

theorem Tdaf.ConvexAnalysis.exists_isTangentAt_lt_of_zero_mem_interior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} [FiniteDimensional ℝ E] (hC : Convex ℝ C) (hCcl : IsClosed C) (h0 : 0 ∈ interior C) {x₀ : E} (hx₀ : x₀ ∉ C) : ∃ (f : StrongDual ℝ E) (y : E), IsTangentAt C f y ∧ f y < f x₀

For a closed convex set with the origin in its interior, every point outside is cut off by a tangent half-space. The normal of that half-space is an exposed point of the polar C°, which is compact because 0 ∈ int C.

theorem Tdaf.ConvexAnalysis.eq_iInter_tangent_halfSpaces {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} [FiniteDimensional ℝ E] (hC : Convex ℝ C) (hCcl : IsClosed C) (hint : (interior C).Nonempty) : ⋂ (f : StrongDual ℝ E), ⋂ (y : E), ⋂ (_ : IsTangentAt C f y), {z : E | f z ≤ f y} = C

A closed convex set with nonempty interior is the intersection of the closed half-spaces tangent to it. ("n-dimensional in ℝⁿ" is (interior C).Nonempty.) This sharpens isClosed_convex_eq_iInter_halfspaces, which intersects all the closed half-spaces containing C.