A unique subgradient forces differentiability

A proper convex function on a finite-dimensional space is differentiable at x exactly when it has a single subgradient there, and that subgradient is then the gradient. The forward half is subgradient_eq_singleton_of_hasFDerivAt; the converse is proved here, and with it the exposed points of epi f* and of a support set move from a subgradient form to a gradient form.

The substance is an interior step the book passes over. ∂f x = {y₀} leaves no room for a normal direction to dom f, and in finite dimensions a convex set is a neighbourhood of every point at which its normal cone is trivial. With x interior, f'(x; ·) is finite in every direction, hence continuous and closed, so the support-function formula — which computes only cl f'(x; ·) — computes f'(x; ·) itself, and it is linear.

Main results

• mem_interior_dom_of_subgradient_eq_singleton — the interior step.
• hasGradientAt_iff_subgradient_eq_singleton — the equivalence in full (Theorem 25.1 in [^1]), with differentiableAtFn_iff_exists_subgradient_eq_singleton naming no gradient.
• hasGradientAt_clFn_iff — ∇(cl f) = ∇f: a closure changes no gradient and creates none.
• mem_exposedPoints_epi_conj_iff_hasGradientAt, mem_exposedPoints_supportSet_iff_hasGradientAt — the exposed points of epi f* and of a support set, for a merely proper convex f, by reduction to cl f. Only the gradients transfer: ∂f = ∂(cl f) fails at relative boundary points, so the subgradient forms in Gradient.lean keep their ClosedFn hypothesis.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §23, §25.

The interior step

theorem Tdaf.ConvexAnalysis.mem_interior_dom_of_subgradient_eq_singleton {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {x : E} {y₀ : F} [IsCompatiblePairing B] (hf : ConvexFn f) (hp : Proper f) (h : subgradient B f x = {y₀}) : x ∈ interior (dom f)

A lone subgradient puts x in the interior of dom f: it leaves no room for a normal direction to dom f, and in finite dimensions a convex set is a neighbourhood of every point at which its normal cone is trivial.

The converse half

theorem Tdaf.ConvexAnalysis.closedFn_dirDeriv_of_mem_interior_dom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {x : E} (hf : ConvexFn f) (hp : Proper f) (hx : x ∈ interior (dom f)) : ClosedFn (dirDeriv f x)

At an interior point of dom f the directional derivative is its own closure: it is finite in every direction there, hence a finite convex function on the whole space, hence continuous. This is what removes the cl from the support-function formula for f'(x; ·).

theorem Tdaf.ConvexAnalysis.hasGradientAt_evalCLM_of_subgradient_eq_singleton {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {x : E} {y₀ : F} [IsCompatiblePairing B] (hf : ConvexFn f) (hp : Proper f) (h : subgradient B f x = {y₀}) : HasGradientAt f ((evalCLM B) y₀) x

The converse half: a convex function with a unique subgradient at x is differentiable there, and the subgradient is the gradient. Properness replaces the usual "let f be finite at x", which is weaker only in appearance: where f = -∞, every element of F is a subgradient.

The equivalence in full

theorem Tdaf.ConvexAnalysis.hasGradientAt_of_subgradient_eq_singleton {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {x : E} {f' : StrongDual ℝ E} (hf : ConvexFn f) (hp : Proper f) (h : subgradient (topDualPairing ℝ E).flip f x = {f'}) : HasGradientAt f f' x

The converse half in the pairing of E with its continuous dual: there evalCLM is the identity, so the unique subgradient is the gradient.

theorem Tdaf.ConvexAnalysis.hasGradientAt_iff_subgradient_eq_singleton {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {x : E} {f' : StrongDual ℝ E} (hf : ConvexFn f) (hp : Proper f) : HasGradientAt f f' x ↔ subgradient (topDualPairing ℝ E).flip f x = {f'}

For a proper convex function, having gradient f' at x and having f' as sole subgradient at x are the same thing.

theorem Tdaf.ConvexAnalysis.differentiableAtFn_iff_exists_subgradient_eq_singleton {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {x : E} (hf : ConvexFn f) (hp : Proper f) : DifferentiableAtFn f x ↔ ∃ (y : StrongDual ℝ E), subgradient (topDualPairing ℝ E).flip f x = {y}

Differentiability at x is exactly the subdifferential being a single point.

∇(cl f) = ∇f

theorem Tdaf.ConvexAnalysis.ConvexFn.clFn_eventuallyEq_of_mem_interior_dom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {x : E} (hf : ConvexFn f) (hx : x ∈ interior (dom f)) : clFn f =ᶠ[nhds x] f

cl f agrees with f on a whole neighbourhood of an interior point of dom f, since interior (dom f) is open and sits inside ri (dom f).

theorem Tdaf.ConvexAnalysis.hasGradientAt_clFn_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {x : E} {f' : StrongDual ℝ E} (hf : ConvexFn f) (hp : Proper f) : HasGradientAt (clFn f) f' x ↔ HasGradientAt f f' x

∇(cl f) = ∇f for a proper convex f: a closure changes no gradient, and creates none. One direction holds because a gradient of f at x puts x in int (dom f), where the two functions agree on a neighbourhood; the other needs ConvexFn.interior_dom_clFn, since a gradient of cl f only supplies a point interior to the larger domain dom (cl f).

theorem Tdaf.ConvexAnalysis.differentiableAtFn_clFn_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {x : E} (hf : ConvexFn f) (hp : Proper f) : DifferentiableAtFn (clFn f) x ↔ DifferentiableAtFn f x

∇(cl f) = ∇f, in the form that names no gradient.

Exposed points without closedness

theorem Tdaf.ConvexAnalysis.exists_subgradient_clFn_eq_singleton_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} [IsCompatiblePairing B] (hf : ConvexFn f) (hp : Proper f) {y : F} : (∃ (x : E), subgradient B (clFn f) x = {y}) ↔ ∃ (x : E), subgradient B f x = {y}

A subdifferential that is a single point is unchanged by taking the closure: ∂(cl f) = ∂f wherever (cl f) x = f x, and a singleton subdifferential puts x inside ri (dom f), where the two functions do agree.

theorem Tdaf.ConvexAnalysis.mem_exposedPoints_epi_conj_iff_of_proper {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} [TopologicalSpace F] [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (hf : ConvexFn f) (hp : Proper f) {y : F} {μ : ℝ} : (y, μ) ∈ Set.exposedPoints ℝ (epi (conj B f)) ↔ conj B f y = ↑μ ∧ ∃ (x : E), subgradient B f x = {y}

The exposed points of epi f* for f merely proper convex. (cl f)* = f*, and cl f has exactly the same points of single-valued subdifferential as f, so the ClosedFn hypothesis of mem_exposedPoints_epi_conj_iff can be discharged by passing to cl f.

theorem Tdaf.ConvexAnalysis.mem_exposedPoints_supportSet_iff_of_proper {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : F → EReal} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] (hgh : PosHomogeneous g) (hgc : ConvexFn g) (hgp : Proper g) {z : E} : z ∈ Set.exposedPoints ℝ (supportSet B.flip g) ↔ ∃ (y : F), subgradient B.flip g y = {z}

The exposed points of a support set for g merely positively homogeneous proper convex. The reduction to cl g is done directly here; cl g supports the same set and is again positively homogeneous.

Exposed points in differentiability form

theorem Tdaf.ConvexAnalysis.mem_exposedPoints_epi_conj_iff_hasGradientAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) {y : StrongDual ℝ E} {μ : ℝ} : (y, μ) ∈ Set.exposedPoints ℝ (epi (conj (topDualPairing ℝ E).flip f)) ↔ conj (topDualPairing ℝ E).flip f y = ↑μ ∧ ∃ (x : E), HasGradientAt f y x

The exposed points of epi f* are the points (∇f x, f* (∇f x)) at which f is differentiable. f need not be closed.

theorem Tdaf.ConvexAnalysis.mem_exposedPoints_supportSet_iff_hasGradientAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hgh : PosHomogeneous f) (hgc : ConvexFn f) (hgp : Proper f) {z : StrongDual ℝ E} : z ∈ Set.exposedPoints ℝ (supportSet (topDualPairing ℝ E).flip f) ↔ ∃ (y : E), HasGradientAt f z y

For a proper convex positively homogeneous f, the exposed points of the closed convex set that f supports are exactly its gradients. Again f need not be closed.