Skip to content

Straszewicz's theorem

TheoremConvex hull of a compact set is compact#✓fully proved

Let \(E\) be a finite-dimensional real normed space. If \(K \subseteq E\) is compact, then the convex hull of \(K\) is compact.

theorem IsCompact.convexHull_of_compact {K : Set E} (hK : IsCompact K) :
    IsCompact (convexHull ℝ K)
Used by 2
Used byJung's theorem · Straszewicz's theorem

DefinitionDifference quotients#✓fully proved

Let \(E\) be a real normed space and \(E^*\) its continuous dual. For \(h : E^* \to \mathbb{R}\) and \(x, v \in E^*\), the difference quotients of \(h\) at \(x\) in direction \(v\) form the set \(\{(h(x + t v) - h(x))/t : t > 0\}\).

When \(h\) is convex this set is bounded below, and its infimum is the one-sided directional derivative of \(h\) at \(x\) in direction \(v\).

noncomputable def dirQuot (h : StrongDual ℝ E → ℝ) (x v : StrongDual ℝ E) : Set ℝ :=
  (fun t : ℝ => (h (x + t • v) - h x) / t) '' Ioi 0
Used by 9
Used byMazur's theorem for support functions · Directional derivative · Continuity of the directional derivative of a support function in the direction · Subadditivity of the directional derivative · Strict sublevel sets of the symmetrized directional derivative are open · Lipschitz bound on directional derivatives of a support function · Directional derivative in direction zero · Difference quotients of a convex function are bounded below · A maximizer bounds the directional derivative of the support function from below

DefinitionDirectional derivative#✓fully proved

Let \(E\) be a real normed space with continuous dual \(E^*\). For \(h : E^* \to \mathbb{R}\) and \(x, v \in E^*\), the directional derivative of \(h\) at \(x\) in direction \(v\) is the infimum of the difference quotients, \(h'(x; v) = \inf_{t > 0} \frac{h(x + t v) - h(x)}{t}\), which is taken to be \(0\) when these quotients are not bounded below.

For convex \(h\) the quotients are bounded below, so this is the usual one-sided directional derivative.

noncomputable def dirDeriv (h : StrongDual ℝ E → ℝ) (x v : StrongDual ℝ E) : ℝ :=
  sInf (dirQuot h x v)
Uses 1 · Used by 10
Statement usesDifference quotients
Used byMazur's theorem for support functions · Opposite directional derivatives have nonnegative sum · Continuity of the directional derivative of a support function in the direction · Subadditivity of the directional derivative · Strict sublevel sets of the symmetrized directional derivative are open · Lipschitz bound on directional derivatives of a support function · Directional derivative in direction zero · Gateaux points · Maximizers at a Gateaux point of the support function are unique · A maximizer bounds the directional derivative of the support function from below

TheoremRestriction of a convex function to a line#✓fully proved

Let \(E\) be a real normed space with continuous dual \(E^*\), and let \(h : E^* \to \mathbb{R}\) be convex. For all \(x, v \in E^*\), the function \(s \mapsto h(x + s v)\) is convex on \(\mathbb{R}\).

theorem convexOn_line (hconv : ConvexOn ℝ univ h) (v : StrongDual ℝ E) :
    ConvexOn ℝ univ (fun s : ℝ => h (x + s • v))
Used by 1
Used byDifference quotients of a convex function are bounded below

TheoremDifference quotients of a convex function are bounded below#✓fully proved

Let \(E\) be a real normed space, \(E^*\) its continuous dual, and \(h : E^* \to \mathbb{R}\) a convex function. For all \(x, v \in E^*\), the set of difference quotients \(\{(h(x + t v) - h(x))/t : t > 0\}\) is bounded below.

The bound comes from comparing slopes of \(h\) on the line through \(x\) in direction \(v\).

theorem dirQuot_bddBelow (hconv : ConvexOn ℝ univ h) (v : StrongDual ℝ E) :
    BddBelow (dirQuot h x v)
Uses 2 · Used by 5
Statement usesDifference quotients
Proof usesRestriction of a convex function to a line
Used byMazur's theorem for support functions · Continuity of the directional derivative of a support function in the direction · Subadditivity of the directional derivative · Strict sublevel sets of the symmetrized directional derivative are open · Lipschitz bound on directional derivatives of a support function

TheoremSubadditivity of the directional derivative#✓fully proved

Let \(E\) be a real normed space with continuous dual \(E^*\), let \(h : E^* \to \mathbb{R}\) be convex, and write \(h'(x; v)\) for the directional derivative of \(h\) at \(x\) in direction \(v\). For all \(x, v, w \in E^*\), \(h'(x; v + w) \le h'(x; v) + h'(x; w)\).

theorem dirDeriv_subadd (hconv : ConvexOn ℝ univ h) (v w : StrongDual ℝ E) :
    dirDeriv h x (v + w) ≤ dirDeriv h x v + dirDeriv h x w
Uses 3 · Used by 2
Statement usesDirectional derivative
Proof usesDifference quotients · Difference quotients of a convex function are bounded below
Used byOpposite directional derivatives have nonnegative sum · Continuity of the directional derivative of a support function in the direction

TheoremDirectional derivative in direction zero#✓fully proved

Let \(E\) be a real normed space with continuous dual \(E^*\) and let \(h : E^* \to \mathbb{R}\) be any function. For every \(x \in E^*\), the directional derivative of \(h\) at \(x\) in direction \(0\) is \(0\).

theorem dirDeriv_zero : dirDeriv h x 0 = 0
Uses 2 · Used by 2
Statement usesDirectional derivative
Proof usesDifference quotients
Used byMazur's theorem for support functions · Opposite directional derivatives have nonnegative sum

TheoremOpposite directional derivatives have nonnegative sum#✓fully proved

Let \(E\) be a real normed space with continuous dual \(E^*\), let \(h : E^* \to \mathbb{R}\) be convex, and write \(h'(x; v)\) for the directional derivative of \(h\) at \(x\) in direction \(v\). For all \(x, v \in E^*\), \(h'(x; v) + h'(x; -v) \ge 0\).

theorem dirDeriv_add_neg_nonneg (hconv : ConvexOn ℝ univ h) (v : StrongDual ℝ E) :
    0 ≤ dirDeriv h x v + dirDeriv h x (-v)
Uses 3 · Used by 1
Statement usesDirectional derivative
Proof usesSubadditivity of the directional derivative · Directional derivative in direction zero
Used byMazur's theorem for support functions
22 fully proved

Support

DefinitionSupport function#✓fully proved

For a set \(K\) in a real normed space \(E\), the support function of \(K\) sends a continuous linear functional \(\ell\) on \(E\) to the supremum \(\sup_{x \in K} \ell(x)\) of the values of \(\ell\) on \(K\).

The supremum is taken in \(\mathbb{R}\), so it is \(0\) when \(K\) is empty or \(\ell\) is unbounded above on \(K\); for nonempty compact \(K\) it is attained.

noncomputable def suppFunc (K : Set E) : StrongDual ℝ E → ℝ :=
  fun l => sSup ((fun x => l x) '' K)
Used by 12
Used byMazur's theorem for support functions · Continuity of the directional derivative of a support function in the direction · Strict sublevel sets of the symmetrized directional derivative are open · Lipschitz bound on directional derivatives of a support function · Maximizers at a Gateaux point of the support function are unique · A maximizer bounds the directional derivative of the support function from below · Straszewicz's theorem · The support function of a compact set is attained · The support function of a compact set is continuous · The support function of a compact set is convex · The support function of a compact set is Lipschitz · A unique maximizer of a linear functional is an exposed point

TheoremThe support function of a compact set is attained#✓fully proved

Let \(K\) be a nonempty compact subset of a real normed space \(E\), and let \(h_K(l) = \sup_{x \in K} l(x)\) be its support function on the continuous dual \(E^*\). For every \(l \in E^*\) there is \(x \in K\) with \(l(x) = h_K(l)\).

theorem suppFunc_attain (hK : IsCompact K) (hKne : K.Nonempty) (l : StrongDual ℝ E) :
    ∃ x ∈ K, l x = suppFunc K l
Uses 1 · Used by 2
Statement usesSupport function
Used byStraszewicz's theorem · The support function of a compact set is Lipschitz

TheoremThe support function of a compact set is convex#✓fully proved

Let \(K\) be a nonempty compact subset of a real normed space \(E\). Its support function \(h_K(l) = \sup_{x \in K} l(x)\) is a convex function on the whole continuous dual \(E^*\).

theorem suppFunc_convex (hK : IsCompact K) (hKne : K.Nonempty) :
    ConvexOn ℝ univ (suppFunc K)
Uses 1 · Used by 4
Statement usesSupport function
Used byMazur's theorem for support functions · Continuity of the directional derivative of a support function in the direction · Strict sublevel sets of the symmetrized directional derivative are open · Lipschitz bound on directional derivatives of a support function

TheoremThe support function of a compact set is Lipschitz#✓fully proved

Let \(K\) be a nonempty compact subset of a real normed space \(E\), and let \(h_K(l) = \sup_{x \in K} l(x)\) be its support function on the continuous dual \(E^*\). There is a constant \(C \ge 0\) such that \(h_K(l_1) - h_K(l_2) \le C \|l_1 - l_2\|\) for all \(l_1, l_2 \in E^*\), where \(\|\cdot\|\) is the operator norm.

theorem suppFunc_lipschitz (hK : IsCompact K) (hKne : K.Nonempty) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ l₁ l₂ : StrongDual ℝ E,
      suppFunc K l₁ - suppFunc K l₂ ≤ C * ‖l₁ - l₂‖
Uses 2 · Used by 3
Statement usesSupport function
Proof usesThe support function of a compact set is attained
Used byMazur's theorem for support functions · Continuity of the directional derivative of a support function in the direction · The support function of a compact set is continuous

TheoremThe support function of a compact set is continuous#✓fully proved

Let \(K\) be a nonempty compact subset of a real normed space \(E\). Its support function \(h_K(l) = \sup_{x \in K} l(x)\) is continuous on the continuous dual \(E^*\) with the operator norm.

theorem suppFunc_continuous (hK : IsCompact K) (hKne : K.Nonempty) :
    Continuous (suppFunc K)
Uses 2 · Used by 1
Statement usesSupport function
Proof usesThe support function of a compact set is Lipschitz
Used byStrict sublevel sets of the symmetrized directional derivative are open

DefinitionGateaux points#✓fully proved

Let \(E\) be a real normed space, \(E^*\) its continuous dual, and \(h : E^* \to \mathbb{R}\). For \(x, v \in E^*\) let \(h'(x; v)\) be the infimum of the difference quotients \((h(x + t v) - h(x))/t\) over \(t > 0\), taken to be \(0\) when they are unbounded below. A point \(x \in E^*\) is a Gateaux point of \(h\) when \(h'(x; v) + h'(x; -v) \le 0\) for every \(v \in E^*\).

def GateauxPt (h : StrongDual ℝ E → ℝ) (x : StrongDual ℝ E) : Prop :=
  ∀ v, dirDeriv h x v + dirDeriv h x (-v) ≤ 0
Uses 1 · Used by 3
Statement usesDirectional derivative
Used byMazur's theorem for support functions · Maximizers at a Gateaux point of the support function are unique · Straszewicz's theorem

TheoremStrict sublevel sets of the symmetrized directional derivative are open#✓fully proved

Let \(E\) be a real normed space with continuous dual \(E^*\), let \(K \subseteq E\) be a nonempty compact set with support function \(h_K\), and write \(h_K'(x; v)\) for the directional derivative of \(h_K\) at \(x\) in direction \(v\). For every \(v \in E^*\) and every real \(c\), the set of \(x \in E^*\) with \(h_K'(x; v) + h_K'(x; -v) < c\) is open.

theorem dirDeriv_sublevel_open (hK : IsCompact K) (hKne : K.Nonempty)
    (v : StrongDual ℝ E) (c : ℝ) :
    IsOpen {x | dirDeriv (suppFunc K) x v + dirDeriv (suppFunc K) x (-v) < c}
Uses 6 · Used by 1
Statement usesDirectional derivative · Support function
Proof usesDifference quotients · Difference quotients of a convex function are bounded below · The support function of a compact set is continuous · The support function of a compact set is convex
Used byMazur's theorem for support functions

TheoremContinuity of the directional derivative of a support function in the direction#✓fully proved

Let \(E\) be a real normed space with continuous dual \(E^*\), let \(K \subseteq E\) be a nonempty compact set with support function \(h_K\), and write \(h_K'(x; w)\) for the directional derivative of \(h_K\) at \(x\) in direction \(w\). For every \(x \in E^*\), the map \(w \mapsto h_K'(x; w)\) is continuous on \(E^*\).

theorem dirDeriv_continuous_in_v (hK : IsCompact K) (hKne : K.Nonempty)
    (x : StrongDual ℝ E) :
    Continuous (fun w => dirDeriv (suppFunc K) x w)
Uses 7 · Used by 1
Statement usesDirectional derivative · Support function
Proof usesSubadditivity of the directional derivative · Difference quotients · Difference quotients of a convex function are bounded below · The support function of a compact set is convex · The support function of a compact set is Lipschitz
Used byMazur's theorem for support functions

TheoremLipschitz bound on directional derivatives of a support function#✓fully proved

Let \(E\) be a real normed space with continuous dual \(E^*\), let \(K \subseteq E\) be a nonempty compact set with support function \(h_K\), and write \(h_K'(x; w)\) for the directional derivative of \(h_K\) at \(x\) in direction \(w\). If \(C\) is a real number with \(h_K(\ell_1) - h_K(\ell_2) \le C \|\ell_1 - \ell_2\|\) for all \(\ell_1, \ell_2 \in E^*\), then \(h_K'(x; w) \le C \|w\|\) for all \(x, w \in E^*\).

theorem dirDeriv_suppFunc_bound (hK : IsCompact K) (hKne : K.Nonempty)
    {C : ℝ} (hlip : ∀ l₁ l₂ : StrongDual ℝ E,
      suppFunc K l₁ - suppFunc K l₂ ≤ C * ‖l₁ - l₂‖)
    (x w : StrongDual ℝ E) : dirDeriv (suppFunc K) x w ≤ C * ‖w‖
Uses 5 · Used by 1
Statement usesDirectional derivative · Support function
Proof usesDifference quotients · Difference quotients of a convex function are bounded below · The support function of a compact set is convex
Used byMazur's theorem for support functions

TheoremMazur's theorem for support functions#✓fully proved

Let \(E\) be a finite-dimensional real normed space with continuous dual \(E^*\), let \(K \subseteq E\) be a nonempty compact set with support function \(h_K\), and write \(h_K'(\ell; v)\) for the directional derivative of \(h_K\) at \(\ell\) in direction \(v\). Then the Gateaux points of \(h_K\), that is, the functionals \(\ell \in E^*\) with \(h_K'(\ell; v) + h_K'(\ell; -v) \le 0\) for every \(v \in E^*\), form a dense subset of \(E^*\).

theorem dense_gateaux (hK : IsCompact K) (hKne : K.Nonempty) :
    Dense {l | GateauxPt (suppFunc K) l}
Uses 12 · Used by 1
Statement usesGateaux points · Support function
Proof usesDirectional derivative · Opposite directional derivatives have nonnegative sum · Continuity of the directional derivative of a support function in the direction · Strict sublevel sets of the symmetrized directional derivative are open · Lipschitz bound on directional derivatives of a support function · Directional derivative in direction zero · Difference quotients · Difference quotients of a convex function are bounded below · The support function of a compact set is convex · The support function of a compact set is Lipschitz
Used byStraszewicz's theorem

Gateaux Exposed

TheoremA maximizer bounds the directional derivative of the support function from below#✓fully proved

Let \(K\) be a nonempty compact subset of a real normed space \(E\), let \(h_K(l) = \sup_{y \in K} l(y)\) be its support function on the continuous dual \(E^*\), and write \(h_K'(u; v)\) for the directional derivative of \(h_K\) at \(u\) in direction \(v\). If \(u \in E^*\) and \(z \in K\) satisfy \(u(z) = h_K(u)\), then \(v(z) \le h_K'(u; v)\) for every \(v \in E^*\).

theorem maximizer_dirDeriv_ge {K : Set E} (hK : IsCompact K) (hKne : K.Nonempty)
    {u : StrongDual ℝ E} {z : E} (hzK : z ∈ K) (hmax : u z = suppFunc K u)
    (v : StrongDual ℝ E) : v z ≤ dirDeriv (suppFunc K) u v
Uses 3 · Used by 1
Statement usesDirectional derivative · Support function
Proof usesDifference quotients
Used byMaximizers at a Gateaux point of the support function are unique

TheoremMaximizers at a Gateaux point of the support function are unique#✓fully proved

Let \(K\) be a nonempty compact subset of a real normed space \(E\), and let \(h_K(l) = \sup_{y \in K} l(y)\) be its support function on the continuous dual \(E^*\). If \(l \in E^*\) is a Gateaux point of \(h_K\) and \(z_1, z_2 \in K\) satisfy \(l(z_1) = h_K(l)\) and \(l(z_2) = h_K(l)\), then \(z_1 = z_2\).

theorem gateaux_unique_maximizer {K : Set E} (hK : IsCompact K) (hKne : K.Nonempty)
    {l : StrongDual ℝ E} (hG : GateauxPt (suppFunc K) l)
    {z₁ z₂ : E} (h₁ : z₁ ∈ K) (h₂ : z₂ ∈ K)
    (e₁ : l z₁ = suppFunc K l) (e₂ : l z₂ = suppFunc K l) : z₁ = z₂
Uses 4 · Used by 1
Statement usesGateaux points · Support function
Proof usesDirectional derivative · A maximizer bounds the directional derivative of the support function from below
Used byStraszewicz's theorem

TheoremA unique maximizer of a linear functional is an exposed point#✓fully proved

Let \(K\) be a nonempty compact set in a real normed space \(E\), let \(\ell\) be a continuous linear functional on \(E\), and let \(h_K\) be the support function of \(K\). If \(z \in K\) satisfies \(\ell(z) = h_K(\ell)\) and every \(y \in K\) with \(\ell(y) = h_K(\ell)\) equals \(z\), then \(z\) is an exposed point of \(K\).

theorem unique_maximizer_exposed {K : Set E} (hK : IsCompact K) (hKne : K.Nonempty)
    {l : StrongDual ℝ E} {z : E} (hzK : z ∈ K) (hmax : l z = suppFunc K l)
    (huniq : ∀ y ∈ K, l y = suppFunc K l → y = z) :
    z ∈ K.exposedPoints ℝ
Uses 1 · Used by 1
Statement usesSupport function
Used byStraszewicz's theorem

Straszewicz Main

TheoremStraszewicz's theorem#✓fully proved

Let \(E\) be a finite-dimensional real normed space and let \(A \subseteq E\) be a compact convex set. Then every extreme point of \(A\) lies in the closure of the set of exposed points of \(A\).

theorem straszewicz_theorem {A : Set E} (hA_compact : IsCompact A)
    (hA_convex : Convex ℝ A) :
    A.extremePoints ℝ ⊆ closure (A.exposedPoints ℝ)
Uses 7
Proof usesGateaux points · Convex hull of a compact set is compact · Mazur's theorem for support functions · Maximizers at a Gateaux point of the support function are unique · Support function · The support function of a compact set is attained · A unique maximizer of a linear functional is an exposed point

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.