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

Supporting balls in the Straszewicz argument

This module contains the elementary Hilbert-space geometry used in Rockafellar's proof of Straszewicz's theorem: a point of a set which is farthest from a center is exposed by the supporting hyperplane to the corresponding closed ball.

theorem AleksandrovDifferentiability.inner_lt_of_norm_sub_center_le_of_forall_norm_sub_sq_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {normal x p : E} {u lam : ℝ} (hlam : 0 < lam) (hp : p ∈ s) (hbound : ∀ ⦃z : E⦄, z ∈ s → ‖z - x‖ ^ 2 < 2 * lam * (inner ℝ normal x - u)) (hfar : ‖x - (x - lam • normal)‖ ≤ ‖p - (x - lam • normal)‖) : u < inner ℝ normal p

A farthest point from a sufficiently shifted center lies outside the separating halfspace.

This is the Pythagorean calculation in Rockafellar's proof of Straszewicz's theorem. The center is x - lam • normal, where x is outside the halfspace {z | inner normal z ≤ u}. If all points of s are close enough to x, then any point at least as far from this shifted center as x cannot belong to that halfspace.

theorem AleksandrovDifferentiability.exposesPoint_of_subset_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {y p : E} (hp : p ∈ s) (hsub : s ⊆ Metric.closedBall y ‖p - y‖) : ExposesPoint s (p - y) p

If a set lies in the closed ball centered at y with p on the boundary, then the supporting hyperplane to that ball at p exposes p in the set.

This is the final geometric step in Rockafellar's proof of Straszewicz's theorem: once p is chosen to maximize z ↦ ‖z - y‖ on s, the normal p - y strictly maximizes z ↦ inner ℝ (p - y) z at p.

theorem AleksandrovDifferentiability.exposesPoint_of_forall_norm_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {y p : E} (hp : p ∈ s) (hmax : ∀ ⦃r : E⦄, r ∈ s → ‖r - y‖ ≤ ‖p - y‖) : ExposesPoint s (p - y) p

Farthest points from a center are exposed by the corresponding supporting ball.

theorem AleksandrovDifferentiability.exists_exposesPoint_and_inner_lt_of_forall_norm_sub_sq_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} (hcompact : IsCompact s) {normal x : E} {u lam : ℝ} (hx : x ∈ s) (hlam : 0 < lam) (hbound : ∀ ⦃z : E⦄, z ∈ s → ‖z - x‖ ^ 2 < 2 * lam * (inner ℝ normal x - u)) : ∃ p ∈ s, ExposesPoint s (p - (x - lam • normal)) p ∧ u < inner ℝ normal p

If the shifted center is far enough from the halfspace, a farthest point is an exposed point outside that halfspace.

This packages the compact choice of p in Rockafellar's proof, assuming the scalar lam has already been chosen so that all points of s satisfy the required squared-distance bound from x.

theorem AleksandrovDifferentiability.exists_mathlib_exposedPoint_inner_lt_of_isCompact_of_inner_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} (hcompact : IsCompact s) {normal x : E} {u : ℝ} (hx : x ∈ s) (hgap : u < inner ℝ normal x) : ∃ p ∈ Set.exposedPoints ℝ s, u < inner ℝ normal p

Compact supporting-ball separation: if a point of a compact set lies outside a halfspace, then some exposed point of the set lies outside the same halfspace.

This is the Lean-facing form of the final construction in Rockafellar's proof of Straszewicz's theorem. Choose the shifted center far enough from x in the opposite normal direction, maximize distance from that center on the compact set, and use the supporting ball at the maximizer.

theorem AleksandrovDifferentiability.exists_exposesPoint_of_isCompact_farthest {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} (hcompact : IsCompact s) (hne : s.Nonempty) (y : E) : ∃ p ∈ s, ExposesPoint s (p - y) p

A nonempty compact set has a farthest point from y, and that point is exposed by the supporting ball centered at y.

This packages the final choice in Rockafellar's proof of Straszewicz's theorem: after arranging that every point of s lies in a suitable ball centered at y, choose a point maximizing z ↦ ‖z - y‖; the supporting hyperplane to that ball exposes the maximizer.