MATHLIBANNEX / CANONICAL DECLARATION CARD

A support face is the convex hull of the maximizing generators

MathlibAnnex.convexHull_maxSlice_eq_supportFace

theorem

Identifies the points of a convex hull on a supporting level by discarding generators with zero weight.

Statement

Let be a nonempty compact subset of a finite-dimensional real normed space and let be a continuous linear functional. Set

Then

The right side is the support face at the maximum of .

Assumptions

The ambient space is a finite-dimensional real normed vector space. The set is nonempty and compact, and is continuous and real-linear. The set need not be convex; may be zero.

Conclusion

The entire support face is generated by the original points of at which attains its maximum. In particular, one need not introduce new generators from the interior of the convex hull.

Notes

Continuity and compactness give a maximizer in , so is nonempty. It is the intersection of with the closed level set , hence compact. These two facts make the maximum slice eligible for another refinement; membership in that refined set is precisely membership in together with equality to the maximum.

Proof route

One inclusion follows from convexity of a level set. For the reverse inclusion, a convex representation at the maximum has zero total gap, forcing every positive-weight generator to lie at that maximum.

Proof steps

  1. The maximum exists because is nonempty compact and is continuous. Put . Linearity makes convex, and . Hence

    Here the first containment uses both monotonicity of the convex hull and convexity of . It remains valid when .

  2. Conversely, let satisfy . Choose a finite convex representation with , and . Each gap is nonnegative, and linearity gives

    A finite sum of nonnegative terms is zero only if every term is zero. Therefore implies , so .

  3. Remove the zero-weight terms. The remaining weights still sum to , their weighted sum is still , and every remaining generator belongs to . Thus , proving the reverse inclusion and the equality.

Main citations

Lean source signature (exact)

theorem convexHull_maxSlice_eq_supportFace [FiniteDimensional ℝ E]
    (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) :
    convexHull ℝ (maxSlice K ℓ) = supportFace K ℓ
In the source Mathematical meaning
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] The finite-dimensional real normed ambient space.
(K : TopologicalSpace.NonemptyCompacts E) The set with its nonemptiness and compactness; convexity is not included.
(ℓ : E →L[ℝ] ℝ) The continuous real-linear functional , possibly zero. In this Card .
maxSlice K ℓ The original maximum slice , as defined in the cited declaration.
In the source Mathematical meaning
supportFace K ℓ The set , as defined in the cited support-face declaration.
convexHull ℝ (maxSlice K ℓ) = supportFace K ℓ The conclusion .
Exact surrounding binder context (separate excerpt) 
noncomputable section

open Set
open TopologicalSpace

namespace MathlibAnnex

universe u

variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Exact content identity

Declaration: MathlibAnnex.convexHull_maxSlice_eq_supportFace

Accepted content SHA-256: 8b332398f902875f464ae106ef414d493cbd6508fad62cb990831c6250d058ce

Accepted source guide SHA-256: ccdf64d5074c7231129343a64b426db48c749a70fd768b861dd3eda012266813

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑