Local boundedness of the subdifferential

A proper convex function is Lipschitz on every compact subset S of the interior of its effective domain, and the same constant bounds its subgradients and its directional derivatives there: there is a K ≥ 0 with f Lipschitz on S with constant K, with ⟨z, y⟩ ≤ K ‖z‖ for every x ∈ S, every y ∈ ∂f x and every direction z, and with f'(x; z) ≤ K ‖z‖ for every x ∈ S. When f is in addition closed, the image ∂f(S) = ⋃ {∂f x | x ∈ S} is nonempty and compact.

Main results

• exists_lipschitz_forall_pairing_le_of_isCompact — the three bounds with one constant, over an arbitrary pairing (Theorem 24.7 in [^1]); exists_forall_norm_le_of_isCompact gives ‖y‖ ≤ K.
• isCompact_subgradient, isCompact_image_subgradientRel — ∂f x and ∂f(S) are compact, hence closed and bounded, and ∂f(S) is non-empty.

Implementation notes

The bound on subgradients is stated as ⟨z, y⟩ ≤ K ‖z‖ for all z, which asks for no norm on the dual side; when F = E is an inner-product space, reading it at z = y gives ‖y‖ ≤ K. The compactness statements are for a real inner-product space paired with itself, and closedness of f is used only for them.

References

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

The quantitative half

theorem Tdaf.ConvexAnalysis.mem_cthickening_add_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {S : Set E} {x : E} (hx : x ∈ S) {δ : ℝ} (hδ : 0 < δ) {z : E} (hz : z ≠ 0) : x + (δ / ‖z‖) • z ∈ Metric.cthickening δ S

Moving a point of S a distance δ in any direction keeps it inside the collar cthickening δ S.

theorem Tdaf.ConvexAnalysis.exists_lipschitz_forall_pairing_le_of_isCompact {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) {S : Set E} (hS : IsCompact S) (hSD : S ⊆ interior (dom f)) : ∃ (K : NNReal), LipschitzOnWith K (fun (x : E) => (f x).toReal) S ∧ (∀ x ∈ S, ∀ y ∈ subgradient B f x, ∀ (z : E), (B z) y ≤ ↑K * ‖z‖) ∧ ∀ x ∈ S, ∀ (z : E), dirDeriv f x z ≤ ↑(↑K * ‖z‖)

The quantitative half. On a compact S ⊆ int (dom f) a single constant K is simultaneously a Lipschitz constant for f, a bound ⟨z, y⟩ ≤ K ‖z‖ for every subgradient at every point of S, and a bound f'(x; z) ≤ K ‖z‖ for the directional derivatives. K is taken to be a Lipschitz constant on a compact collar cthickening δ S ⊆ int (dom f), and the other two bounds are read off it at the point x + (δ / ‖z‖) • z, which stays in the collar.

The topological half

theorem Tdaf.ConvexAnalysis.exists_forall_norm_le_of_isCompact {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) {S : Set E} (hS : IsCompact S) (hSD : S ⊆ interior (dom f)) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ x ∈ S, ∀ y ∈ subgradient (innerₗ E) f x, ‖y‖ ≤ K

The norm form of the subgradient bound: on a compact S ⊆ int (dom f) a single constant bounds ‖y‖ for every subgradient y at every point of S.

theorem Tdaf.ConvexAnalysis.isCompact_subgradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) {x : E} (hx : x ∈ interior (dom f)) : IsCompact (subgradient (innerₗ E) f x)

∂f x is compact at every interior point of dom f: closed because it is an intersection of closed half-spaces, and bounded by the constant above.

theorem Tdaf.ConvexAnalysis.image_subgradientRel_nonempty {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) {S : Set E} (hne : S.Nonempty) (hSD : S ⊆ interior (dom f)) : ((subgradientRel (innerₗ E) f).image S).Nonempty

Nonemptiness: ∂f(S) ≠ ∅ for a nonempty S ⊆ int (dom f).

theorem Tdaf.ConvexAnalysis.isCompact_image_subgradientRel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ClosedProperConvexFn f) {S : Set E} (hS : IsCompact S) (hSD : S ⊆ interior (dom f)) : IsCompact ((subgradientRel (innerₗ E) f).image S)

The topological half: ∂f(S) is compact for a closed proper convex f and a compact S ⊆ int (dom f). The graph of ∂f is closed, so it meets the compact box S ×ˢ closedBall 0 K in a compact set of which ∂f(S) is the projection.