Essential smoothness

A convex function is essentially smooth when the interior C of its effective domain is non-empty, f is differentiable throughout C, and ‖∇f xᵢ‖ → ∞ along every sequence in C approaching a point outside C. For a closed proper convex function on a finite-dimensional inner product space this happens exactly when the subdifferential is single-valued, and in that case ∂f is the gradient on C and empty elsewhere — so the multivalued object ∂f carries precisely the information of the classical gradient mapping. That is what makes the Legendre transformation work.

Main results

• EssentiallySmooth f — the three conditions above, with the gradient written as fderiv ℝ (fun z => (f z).toReal).
• domSubgradient_eq_interior_dom_of_essentiallySmooth — dom ∂f = int (dom f).
• subsingleton_subgradient_iff_essentiallySmooth — essential smoothness is exactly single-valuedness of ∂f (Theorem 26.1 in [^1]).

Implementation notes

Condition (c) is stated at every point outside C, where the book states it at boundary points of C. Since C is open the two readings agree, and this one avoids re-deriving boundaryness at every use. Gradients are compared through their Riesz representatives, since ∂f x for the pairing innerₗ E is a set of vectors while fderiv lands in StrongDual ℝ E.

References

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

structure Tdaf.ConvexAnalysis.EssentiallySmooth {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → EReal) : Prop

Essential smoothness. Writing C = int (dom f): (a) C is non-empty, (b) f is differentiable throughout C, and (c) ‖∇f xᵢ‖ → ∞ for every sequence in C converging to a point outside C. A finite differentiable convex function on the whole space is essentially smooth, (c) holding vacuously.

• interior_dom_nonempty : (interior (dom f)).Nonempty

  (a) The effective domain has non-empty interior.

• differentiableAtFn ⦃z : E⦄ : z ∈ interior (dom f) → DifferentiableAtFn f z

  (b) f is differentiable at every interior point of its effective domain.

• tendsto_norm_fderiv ⦃z : E⦄ : z ∉ interior (dom f) → ∀ (zs : ℕ → E), (∀ (i : ℕ), zs i ∈ interior (dom f)) → Filter.Tendsto zs Filter.atTop (nhds z) → Filter.Tendsto (fun (i : ℕ) => ‖fderiv ℝ (fun (w : E) => (f w).toReal) (zs i)‖) Filter.atTop Filter.atTop

  (c) The gradient blows up along every approach to a point outside the interior.

theorem Tdaf.ConvexAnalysis.subgradient_eq_singleton_of_essentiallySmooth {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {x : E} (hf : ConvexFn f) (hes : EssentiallySmooth f) (hx : x ∈ interior (dom f)) : subgradient (innerₗ E) f x = {(InnerProductSpace.toDual ℝ E).symm (fderiv ℝ (fun (w : E) => (f w).toReal) x)}

On the interior of the effective domain, an essentially smooth function has exactly one subgradient, namely its gradient.

theorem Tdaf.ConvexAnalysis.subgradient_eq_empty_of_essentiallySmooth {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {x : E} (hf : ConvexFn f) (hp : Proper f) (hcl : ClosedFn f) (hes : EssentiallySmooth f) (hx : x ∉ interior (dom f)) : subgradient (innerₗ E) f x = ∅

Off the interior of the effective domain, an essentially smooth closed proper convex function has no subgradient: a subgradient at x would force a sequence of gradients to converge, which condition (c) forbids.

theorem Tdaf.ConvexAnalysis.domSubgradient_eq_interior_dom_of_essentiallySmooth {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) (hcl : ClosedFn f) (hes : EssentiallySmooth f) : domSubgradient (innerₗ E) f = interior (dom f)

For an essentially smooth closed proper convex function, dom ∂f is exactly the interior of the effective domain.

theorem Tdaf.ConvexAnalysis.subsingleton_subgradient_of_essentiallySmooth {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) (hcl : ClosedFn f) (hes : EssentiallySmooth f) (x : E) : (subgradient (innerₗ E) f x).Subsingleton

An essentially smooth closed proper convex function has a single-valued subdifferential.

theorem Tdaf.ConvexAnalysis.differentiableAtFn_of_subsingleton_subgradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {x : E} (hf : ConvexFn f) (hp : Proper f) (h : ∀ (z : E), (subgradient (innerₗ E) f z).Subsingleton) (hx : x ∈ intrinsicInterior ℝ (dom f)) : DifferentiableAtFn f x

A single-valued subdifferential is a gradient on the relative interior: a subgradient exists at every point of ri (dom f), single-valuedness makes it the only one, and a lone subgradient is a gradient.

theorem Tdaf.ConvexAnalysis.essentiallySmooth_of_subsingleton_subgradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) (hcl : ClosedFn f) (h : ∀ (z : E), (subgradient (innerₗ E) f z).Subsingleton) : EssentiallySmooth f

The substantive half: a closed proper convex function with a single-valued subdifferential is essentially smooth. Conditions (a) and (b) hold because a gradient exists only at interior points, forcing ri (dom f) = int (dom f); condition (c) holds because a bounded subsequence of gradients would converge to a subgradient at the limit point.

theorem Tdaf.ConvexAnalysis.subsingleton_subgradient_iff_essentiallySmooth {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) (hcl : ClosedFn f) : (∀ (z : E), (subgradient (innerₗ E) f z).Subsingleton) ↔ EssentiallySmooth f

For a closed proper convex function, single-valuedness of the subdifferential and essential smoothness are the same thing.