Extreme points of unit balls

TheoremExtreme points of the unit ball of continuous real functions#✓fully proved

The extreme points of the closed unit ball of C(X, ℝ), for X compact Hausdorff, are exactly the functions with |f x| = 1 for every x.

theorem extremePoints_closedBall_continuousMap :
    (Metric.closedBall (0 : C(X, ℝ)) 1).extremePoints ℝ = {f | ∀ x, |f x| = 1}

Used by 1

Used byMembership criterion for extreme points of the unit ball of \(C(X)\)

TheoremMembership criterion for extreme points of the unit ball of \(C(X)\)#✓fully proved

Membership form of extremePoints_closedBall_continuousMap.

theorem mem_extremePoints_closedBall_continuousMap {f : C(X, ℝ)} :
    f ∈ (Metric.closedBall (0 : C(X, ℝ)) 1).extremePoints ℝ ↔ ∀ x, |f x| = 1

Uses 1

Proof usesExtreme points of the unit ball of continuous real functions

TheoremExtreme points of the unit ball of finite \(\ell^\infty\)#✓fully proved

The extreme points of the closed unit ball of PiLp ∞ (fun _ : ι => 𝕜) are exactly the vectors all of whose coordinates have norm 1. If some coordinate has norm < 1, a small perturbation of that coordinate stays in the ball and exhibits the point as a midpoint; conversely, a vector with all coordinates of norm 1 that is a convex combination of two ball points must agree with both of them coordinatewise, by strict convexity of the scalar field.

theorem extremePoints_closedBall_piLp_top :
    (Metric.closedBall (0 : PiLp ∞ fun _ : ι => 𝕜) 1).extremePoints ℝ =
      {x | ∀ i, ‖x i‖ = 1}

TheoremExtreme points of the unit ball of finite \(\ell^1\)#✓fully proved

The extreme points of the closed unit ball of PiLp 1 (fun _ : ι => 𝕜) are exactly the unit multiples of the coordinate vectors. The proof: an extreme point must have norm 1 (otherwise a one-coordinate perturbation stays in the ball and exhibits it as a midpoint), and it cannot have two nonzero coordinates (otherwise mass can be transferred between them, in the direction of the phases of the two coordinates, staying at norm 1 on both sides). Conversely, a unit multiple of a coordinate vector is extreme: a convex combination equalling it must have total norm 1, hence coordinatewise triangle equality, hence vanishing off the coordinate, and strict convexity of the scalar field at the coordinate.

theorem extremePoints_closedBall_piLp_one :
    (Metric.closedBall (0 : PiLp 1 fun _ : ι => 𝕜) 1).extremePoints ℝ =
      {x | ∃ i, ∃ c : 𝕜, ‖c‖ = 1 ∧ x = PiLp.single 1 i c}

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.