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

Line-lift consequences of epigraph separation

This file connects the epigraph-separation support functional with the line-lift interfaces used later in the Aleksandrov proof. It still does not prove the endpoint-specific normalization q = ℓ z; it packages the support and nonemptiness consequences needed by the compact endpoint attainment wrappers.

theorem AleksandrovDifferentiability.ConvexOn.exists_lineSubgradientLiftsToAmbientFunctional_supportingValue_of_isOpen {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t : ℝ} (hu : ConvexOn ℝ s u) (hs : IsOpen s) (hpoint : x + t • z ∈ s) : ∃ (q : ℝ), LineSubgradientLiftsToAmbientFunctional s u x z t q

On an open finite-dimensional convex domain, epigraph separation gives a functional line lift at the directional value of the supporting functional.

theorem AleksandrovDifferentiability.ConvexOn.lineSubgradientLiftsToAmbientFunctional_of_isOpen {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {u : E → ℝ} {x z : E} {t q : ℝ} (hu : ConvexOn ℝ s u) (hs : IsOpen s) (hq : SubgradientOn (lineDomain s x z) (AleksandrovDifferentiability.lineRestriction u x z) t q) : LineSubgradientLiftsToAmbientFunctional s u x z t q

A line subgradient lifts to an ambient supporting functional on open finite-dimensional convex domains.

The proof separates Mathlib's strict epigraph from the affine line minorant determined by the one-dimensional subgradient. Since the separated convex set is the whole affine line, the separating functional is constant on its direction; after normalizing by the negative vertical coefficient, this forces the horizontal supporting functional to take the prescribed value on z.

This is the project-local Hahn-Banach step: it uses Mathlib separation via geometric_hahn_banach_open, and does not reprove Hahn-Banach.

theorem AleksandrovDifferentiability.ConvexOn.subgradient_set_nonempty_of_isOpen {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hs : IsOpen s) (hx : x ∈ s) : {p : E | SubgradientOn s u x p}.Nonempty

On an open finite-dimensional convex domain in a complete real inner-product space, the subdifferential is nonempty at every point of the domain.

This is the vector-valued Riesz form of the supporting functional produced by Mathlib epigraph separation.

theorem AleksandrovDifferentiability.ConvexOn.eventually_subgradient_set_nonempty_of_isOpen {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hs : IsOpen s) (hsegment : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, x + t • z ∈ s) : ∀ᶠ (z : E) in nhds 0, ∀ t ∈ Set.uIoc 0 1, {p : E | SubgradientOn s u (x + t • z) p}.Nonempty

Eventual subgradient nonemptiness along a family of short segments contained in an open finite-dimensional convex domain.