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

Exposed points and Mathlib bridges

This module defines the project-local exposed-point carrier and relates it to Mathlib Set.exposedPoints.

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

Recession directions of a set s based at p.

For a closed convex set this is independent of the base point p once p ∈ s, but the based version is enough for the exposed-point step in Rockafellar 25.6.

Equations

• AleksandrovDifferentiability.recessionDirectionsAt s p = {q : E | ∀ ⦃t : ℝ⦄, 0 ≤ t → p + t • q ∈ s}

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

Directions of affine lines through p contained in s.

Equations

• AleksandrovDifferentiability.lineDirectionsAt s p = {q : E | ∀ (t : ℝ), p + t • q ∈ s}

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

A set contains no nontrivial affine line.

Equations

• AleksandrovDifferentiability.HasNoAffineLines s = ∀ ⦃p q : E⦄, p ∈ s → q ∈ AleksandrovDifferentiability.lineDirectionsAt s p → q = 0

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

The exposed points of a set, with the exposing normal existentially packaged.

Rockafellar 25.6 uses Straszewicz's theorem to approximate extreme points by exposed points. This set is the Lean-facing carrier for that exposed-point reduction.

Equations

• AleksandrovDifferentiability.exposedPoints s = {p : E | ∃ (normal : E), AleksandrovDifferentiability.ExposesPoint s normal p}

theorem AleksandrovDifferentiability.exposedPoints_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} : exposedPoints s ⊆ s

An exposed point is a point of the original set.

theorem AleksandrovDifferentiability.exists_unit_exposesPoint_of_mem_exposedPoints_of_exists_unit_vector {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {p : E} (hp : p ∈ exposedPoints s) (hunit : ∃ (unitNormal : E), ‖unitNormal‖ = 1) : ∃ (unitNormal : E), ‖unitNormal‖ = 1 ∧ ExposesPoint s unitNormal p

An exposed point admits a unit exposing normal whenever the ambient space has a unit vector.

This is the existential form used after applying Straszewicz: the exposed-point carrier only stores some exposing normal, and this lemma recovers Rockafellar's unit normal.

theorem AleksandrovDifferentiability.ExposesPoint.mem_mathlib_exposedPoints {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} {normal p : E} (hexposed : ExposesPoint s normal p) : p ∈ Set.exposedPoints ℝ s

A project-local exposed point is a Mathlib exposed point.

theorem AleksandrovDifferentiability.mem_exposedPoints_of_mem_mathlib_exposedPoints {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} {p : E} (hp : p ∈ Set.exposedPoints ℝ s) : p ∈ exposedPoints s

A Mathlib exposed point is a project-local exposed point, using Fréchet-Riesz to represent the exposing functional by an inner-product normal vector.

theorem AleksandrovDifferentiability.exposedPoints_eq_mathlib_exposedPoints {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (s : Set E) : exposedPoints s = Set.exposedPoints ℝ s

In complete real inner product spaces, the project-local exposed points are exactly Mathlib's exposed points.

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

Mathlib exposed points are exactly project-local singleton exposed faces, for some normal.

theorem AleksandrovDifferentiability.mem_mathlib_exposedPoints_of_unique_isMaxOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {p : E} {l : StrongDual ℝ E} (hp : p ∈ s) (hmax : IsMaxOn (⇑l) s p) (hunique : ∀ ⦃q : E⦄, q ∈ s → l q = l p → q = p) : p ∈ Set.exposedPoints ℝ s

A unique maximizer of a continuous linear functional is a Mathlib exposed point.

This is the basic exposed-point recognition lemma used in the Rockafellar 25.6 route: once a linear functional has a unique maximizer on a convex set, that maximizer belongs to Set.exposedPoints. No convexity is needed for this definitional bridge.

theorem AleksandrovDifferentiability.exists_unique_isMaxOn_of_mem_mathlib_exposedPoints {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {p : E} (hp : p ∈ Set.exposedPoints ℝ s) : ∃ (l : StrongDual ℝ E), IsMaxOn (⇑l) s p ∧ ∀ ⦃q : E⦄, q ∈ s → l q = l p → q = p

A Mathlib exposed point supplies a continuous linear functional with a unique maximum.

This is the unpacked form of Set.exposedPoints, phrased with IsMaxOn so later Rockafellar-style arguments can use the standard extremum API.