Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Exposed faces

This module defines the project-local exposed-face and strictly exposed-point predicates and proves their basic compactness, convexity, and extremality properties.

def AleksandrovDifferentiability.ExposesPoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (normal p : E) : Prop

A vector normal exposes the point p of a set s.

This is the exact form used in Rockafellar 25.6: the exposed face in direction normal is the singleton {p}.

Equations

• AleksandrovDifferentiability.ExposesPoint s normal p = (p ∈ s ∧ ∀ ⦃r : E⦄, r ∈ s → r ≠ p → inner ℝ normal r < inner ℝ normal p)

def AleksandrovDifferentiability.exposedFace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (normal : E) : Set E

The exposed face of s in the direction normal.

This is Rockafellar's notation ∂f(x)_y in set-theoretic form: the points of s where the linear functional r ↦ normal · r attains its supremal value on s, written without mentioning the supremum.

Equations

• AleksandrovDifferentiability.exposedFace s normal = {p : E | p ∈ s ∧ ∀ ⦃r : E⦄, r ∈ s → inner ℝ normal r ≤ inner ℝ normal p}

theorem AleksandrovDifferentiability.exposedFace_isExposed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (s : Set E) (normal : E) : IsExposed ℝ s (exposedFace s normal)

The project-local exposed face is a Mathlib exposed set.

theorem AleksandrovDifferentiability.isCompact_exposedFace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} (hcompact : IsCompact s) (normal : E) : IsCompact (exposedFace s normal)

Exposed faces of compact sets are compact.

theorem AleksandrovDifferentiability.convex_exposedFace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} (hconv : Convex ℝ s) (normal : E) : Convex ℝ (exposedFace s normal)

Exposed faces of convex sets are convex.

theorem AleksandrovDifferentiability.exposedFace_isExtreme {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (s : Set E) (normal : E) : IsExtreme ℝ s (exposedFace s normal)

Exposed faces are extreme subsets of the original set.

theorem AleksandrovDifferentiability.IsCompact.exposedFace_nonempty {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} (hcompact : IsCompact s) (hne : s.Nonempty) (normal : E) : (exposedFace s normal).Nonempty

A nonempty compact set has a nonempty exposed face in every direction.

theorem AleksandrovDifferentiability.exposedFace_extremePoints_subset_extremePoints {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (s : Set E) (normal : E) : Set.extremePoints ℝ (exposedFace s normal) ⊆ Set.extremePoints ℝ s

Extreme points of an exposed face are extreme points of the original set.

theorem AleksandrovDifferentiability.mem_mathlib_exposedPoints_of_exposedFace_eq_singleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} {normal p : E} (hface : exposedFace s normal = {p}) : p ∈ Set.exposedPoints ℝ s

If an exposed face is a singleton, its point is a Mathlib exposed point.