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

Strict exposed points

This module proves the singleton exposed-face characterization, unit-normal normalization, and the singleton norm-thickening estimate for project-local exposed points.

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

An exposing normal selects its exposed point as a member of the corresponding exposed face.

theorem AleksandrovDifferentiability.ExposesPoint.exposedFace_eq_singleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {normal p : E} (hexposed : ExposesPoint s normal p) : exposedFace s normal = {p}

A strictly exposing normal has singleton exposed face.

theorem AleksandrovDifferentiability.exposesPoint_of_exposedFace_eq_singleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {normal p : E} (hface : exposedFace s normal = {p}) : ExposesPoint s normal p

If the exposed face in direction normal is {p}, then normal strictly exposes p.

This is the converse to ExposesPoint.exposedFace_eq_singleton, and lets us pass from Rockafellar's exposed-face notation back to the project-local strict exposed-point predicate.

theorem AleksandrovDifferentiability.exposesPoint_iff_exposedFace_eq_singleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {normal p : E} : ExposesPoint s normal p ↔ exposedFace s normal = {p}

Strict exposure is equivalent to the exposed face being the corresponding singleton.

theorem AleksandrovDifferentiability.ExposesPoint.pos_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {normal p : E} (hexposed : ExposesPoint s normal p) {c : ℝ} (hc : 0 < c) : ExposesPoint s (c • normal) p

Multiplying an exposing normal by a positive scalar preserves the exposed point.

theorem AleksandrovDifferentiability.norm_inv_norm_smul_eq_one_of_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {normal : E} (hnormal : normal ≠ 0) : ‖‖normal‖⁻¹ • normal‖ = 1

The usual normalization of a nonzero vector has norm one.

theorem AleksandrovDifferentiability.ExposesPoint.unit_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {normal p : E} (hexposed : ExposesPoint s normal p) (hnormal : normal ≠ 0) : ExposesPoint s (‖normal‖⁻¹ • normal) p

A nonzero exposing normal can be normalized to a unit exposing normal.

theorem AleksandrovDifferentiability.ExposesPoint.exists_unit_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {normal p : E} (hexposed : ExposesPoint s normal p) (hnormal : normal ≠ 0) : ∃ (unitNormal : E), ‖unitNormal‖ = 1 ∧ ExposesPoint s unitNormal p

A packaged unit-normal version of a nonzero exposing normal.

theorem AleksandrovDifferentiability.ExposesPoint.subset_singleton_of_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {p : E} (hexposed : ExposesPoint s 0 p) : s ⊆ {p}

If the zero normal exposes p, then the exposed set is contained in {p}.

theorem AleksandrovDifferentiability.ExposesPoint.normal_ne_zero_of_exists_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {normal p : E} (hexposed : ExposesPoint s normal p) (hnontrivial : ∃ r ∈ s, r ≠ p) : normal ≠ 0

If an exposed set contains a point different from p, then any normal exposing p is nonzero.

theorem AleksandrovDifferentiability.ExposesPoint.exists_unit_or_subset_singleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {normal p : E} (hexposed : ExposesPoint s normal p) : (∃ (unitNormal : E), ‖unitNormal‖ = 1 ∧ ExposesPoint s unitNormal p) ∨ s ⊆ {p}

An exposed point either has a unit exposing normal, or the whole exposed set is the singleton containing that point.

This is the precise normalization dichotomy behind Rockafellar's phrase "choose a unit vector which exposes p": outside the degenerate singleton case, the exposing normal can be normalized.

theorem AleksandrovDifferentiability.ExposesPoint.of_subset_singleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {p normal : E} (hp : p ∈ s) (hsubset : s ⊆ {p}) : ExposesPoint s normal p

If s is contained in {p} and contains p, then every normal exposes p on s.

This packages the degenerate singleton case of exposed points.

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

If the ambient space has some unit vector, then every exposed point admits a unit exposing normal.

For nonzero exposing normals this is normalization. For the zero-normal case, the exposed set is contained in {p}, so any ambient unit vector exposes p vacuously.

theorem AleksandrovDifferentiability.norm_sub_lt_of_mem_normThickening_singleton {E : Type u_1} [NormedAddCommGroup E] {x p : E} {ε : ℝ} (hx : x ∈ normThickening {p} ε) : ‖x - p‖ < ε

Thickening of a singleton gives the corresponding norm estimate.