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

Epigraph separation for convex functions

This file records the project-local interface to Mathlib's geometric Hahn-Banach separation theorem for strict epigraphs. It is intended for the endpoint-attainment step in the Aleksandrov proof: supporting functionals are produced by applying Mathlib separation, not by reproving Hahn-Banach.

def AleksandrovDifferentiability.strictEpigraphOn {E : Type u_1} (s : Set E) (u : E → ℝ) : Set (E × ℝ)

The strict epigraph of a function over a set.

Equations

• AleksandrovDifferentiability.strictEpigraphOn s u = {p : E × ℝ | p.1 ∈ s ∧ u p.1 < p.2}

theorem AleksandrovDifferentiability.ConvexOn.convex_strictEpigraphOn {E : Type u_1} [NormedAddCommGroup E] {s : Set E} {u : E → ℝ} [NormedSpace ℝ E] (hu : ConvexOn ℝ s u) : Convex ℝ (strictEpigraphOn s u)

A convex function has a convex strict epigraph over its convexity domain.

theorem AleksandrovDifferentiability.isOpen_strictEpigraphOn_of_continuousOn {E : Type u_1} [NormedAddCommGroup E] {s : Set E} {u : E → ℝ} (hs : IsOpen s) (hu : ContinuousOn u s) : IsOpen (strictEpigraphOn s u)

If u is continuous on an open set, then its strict epigraph over that set is open.

theorem AleksandrovDifferentiability.ConvexOn.exists_strongDual_lt_on_strictEpigraphOn {E : Type u_1} [NormedAddCommGroup E] {s : Set E} {u : E → ℝ} {x : E} {r : ℝ} [NormedSpace ℝ E] (hu : ConvexOn ℝ s u) (hs : IsOpen s) (hcont : ContinuousOn u s) (hx : (x, r) ∉ strictEpigraphOn s u) : ∃ (ℓ : StrongDual ℝ (E × ℝ)), ∀ p ∈ strictEpigraphOn s u, ℓ p < ℓ (x, r)

Apply Mathlib's geometric Hahn-Banach theorem to separate a point from the strict epigraph of a convex function over an open set.

This is the project-local separation interface for later endpoint-attainment work.

theorem AleksandrovDifferentiability.ConvexOn.exists_strongDual_lt_on_strictEpigraphOn_of_isOpen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {u : E → ℝ} {x : E} {r : ℝ} (hu : ConvexOn ℝ s u) (hs : IsOpen s) (hx : (x, r) ∉ strictEpigraphOn s u) : ∃ (ℓ : StrongDual ℝ (E × ℝ)), ∀ p ∈ strictEpigraphOn s u, ℓ p < ℓ (x, r)

On an open convex set in finite dimension, a convex function has open strict epigraph and therefore admits the Mathlib separation conclusion for every point outside that strict epigraph.

theorem AleksandrovDifferentiability.strictEpigraphOn_separatingFunctional_vertical_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hx : x ∈ s) (ℓ : StrongDual ℝ (E × ℝ)) (hsep : ∀ p ∈ strictEpigraphOn s u, ℓ p < ℓ (x, u x)) : ℓ (0, 1) < 0

A separator of the strict epigraph from the graph point (x, u x) has negative vertical coefficient.

This is the first normalization fact needed to turn Mathlib's abstract separating functional into an affine supporting functional for u.

theorem AleksandrovDifferentiability.ConvexOn.exists_strongDual_lt_on_strictEpigraphOn_graph_point_of_isOpen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hs : IsOpen s) (hx : x ∈ s) : ∃ (ℓ : StrongDual ℝ (E × ℝ)), (∀ p ∈ strictEpigraphOn s u, ℓ p < ℓ (x, u x)) ∧ ℓ (0, 1) < 0

Separation of the strict epigraph from a graph point, with the vertical negativity normalization already extracted.

The separation itself is Mathlib's geometric Hahn-Banach theorem applied by ConvexOn.exists_strongDual_lt_on_strictEpigraphOn_of_isOpen.

noncomputable def AleksandrovDifferentiability.strictEpigraphOn.normalizedHorizontalFunctional {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ℓ : StrongDual ℝ (E × ℝ)) : StrongDual ℝ E

The horizontal part of a separator, normalized by its negative vertical coefficient.

Equations

• AleksandrovDifferentiability.strictEpigraphOn.normalizedHorizontalFunctional ℓ = -(ℓ (0, 1))⁻¹ • ℓ ∘SL ContinuousLinearMap.inl ℝ E ℝ

theorem AleksandrovDifferentiability.strictEpigraphOn.normalizedHorizontalFunctional_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ℓ : StrongDual ℝ (E × ℝ)) (v : E) : (normalizedHorizontalFunctional ℓ) v = -ℓ (v, 0) / ℓ (0, 1)

theorem AleksandrovDifferentiability.strictEpigraphOn_separatingFunctional_graph_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {u : E → ℝ} {x y : E} (hy : y ∈ s) (ℓ : StrongDual ℝ (E × ℝ)) (hvert : ℓ (0, 1) < 0) (hsep : ∀ p ∈ strictEpigraphOn s u, ℓ p < ℓ (x, u x)) : ℓ (y, u y) ≤ ℓ (x, u x)

The strict-epigraph separator also separates the closed graph pointwise.

theorem AleksandrovDifferentiability.strictEpigraphOn_normalizedHorizontalFunctional_supporting_inequality {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {u : E → ℝ} {x y : E} (hy : y ∈ s) (ℓ : StrongDual ℝ (E × ℝ)) (hvert : ℓ (0, 1) < 0) (hsep : ∀ p ∈ strictEpigraphOn s u, ℓ p < ℓ (x, u x)) : u x + (strictEpigraphOn.normalizedHorizontalFunctional ℓ) (y - x) ≤ u y

The normalized horizontal part of a strict-epigraph separator supports the function at the separated graph point.

theorem AleksandrovDifferentiability.ConvexOn.exists_supportingFunctionalAt_of_isOpen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ s u) (hs : IsOpen s) (hx : x ∈ s) : ∃ (φ : StrongDual ℝ E), ∀ y ∈ s, u x + φ (y - x) ≤ u y

A convex function on an open finite-dimensional domain admits a supporting continuous linear functional at every point of the domain.

This is the graph-point consequence of Mathlib epigraph separation. Endpoint-specific arguments will add the extra normalization q = ℓ z; this theorem supplies the ambient support inequality itself.