Compactness of subgradient images of convex functions

Let E be a finite-dimensional real inner product space and let f : E → EReal be convex (convex real epigraph, never ⊥), with D the interior of its effective domain {x | f x ≠ ⊤}. Since f is continuous on D, its subgradients for the inner product are bounded over every compact K ⊆ D, and the graph of the subdifferential over a closed K ⊆ D is closed. More generally, closedness of this graph only needs finiteness and continuity of the real representative on K. Hence the subgradient image ∂f(K) = ⋃ x ∈ K, ∂f(x) of a compact subset of D is compact. The same compactness, with Rademacher's theorem, shows that f has a subgradient at every point of D; in particular a real function convex on an open set has a supporting hyperplane at each point.

For a real function u continuous on the compact closure of a set Ω, every slope of an affine function through a point of the graph over Ω that lies below u on the frontier of Ω is a supporting slope on the closure at some point of Ω. The argument works for continuous linear functionals on a real normed space; the inner-product form is a specialization. Consequently, if w ≤ u on the frontier of Ω, the subgradients of w relative to Ω at points where u < w, and their small perturbations, are subgradients of u relative to Ω: this is the comparison step behind the comparison principle for the Monge–Ampère equation.

In a seminormed real inner product space, if real functions F k converge to u locally uniformly on an open set Ω, with u continuous on Ω, their subgradients relative to Ω at points of a compact K ⊆ Ω are eventually bounded. If the space is proper, every open neighbourhood of the subgradient image of K under u eventually contains that of K under F k.

Main statements

• TauCeti.mul_norm_le_of_forall_add_inner_le — a subgradient of u at x relative to Ω is bounded in terms of a bound for |u| on a ball about x inside Ω;
• TauCeti.exists_norm_le_of_mem_subdifferential — the subgradients of f are bounded over compact subsets of D;
• TauCeti.isClosed_setOf_mem_subdifferential — the graph of the subdifferential over a closed set on which the function is finite and its real representative is continuous is closed;
• TauCeti.isCompact_setOf_mem_subdifferential and TauCeti.isCompact_subgradientImage — the graph of the subdifferential over a compact subset of D, and the subgradient image of such a set, are compact;
• TauCeti.nonempty_subdifferential_of_mem_interior — the subdifferential is nonempty at every point of D, and TauCeti.eventually_nonempty_subdifferential at every point near a point around which f is finite;
• ConvexOn.exists_forall_add_inner_le — a real function convex on an open set has a subgradient relative to that set at each of its points;
• TauCeti.exists_forall_add_apply_le_of_forall_frontier — continuous-linear-functional slopes below the boundary values support the function on the closure at an interior-domain point;
• TauCeti.exists_forall_add_inner_le_of_forall_frontier — slopes of affine functions through a point of the graph that lie below the boundary values are subgradients at points of Ω;
• TauCeti.exists_forall_add_inner_add_le_of_forall_frontier_le — if w ≤ u on the frontier of Ω, small perturbations of a subgradient of w at a point where u < w are subgradients of u at points of Ω;
• TauCeti.exists_eventually_norm_le_of_tendstoLocallyUniformlyOn — subgradients of a locally uniformly convergent family are eventually bounded over compact sets;
• TauCeti.eventually_biUnion_subset_of_tendstoLocallyUniformlyOn — upper semicontinuity of subgradient images under locally uniform convergence.

References

• R. T. Rockafellar, Convex Analysis, Princeton Mathematical Series 28, 1970, Theorem 24.7.
• C. E. Gutiérrez, The Monge–Ampère Equation, 2nd ed., Progress in Nonlinear Differential Equations and Their Applications 89, Birkhäuser, 2016, §§1.1–1.2.

theorem TauCeti.mul_norm_le_of_forall_add_inner_le {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {Ω : Set E} {u : E → ℝ} {x y : E} {δ M : ℝ} (hδ : 0 ≤ δ) (hΩ : Metric.closedBall x δ ⊆ Ω) (hM : ∀ z ∈ Metric.closedBall x δ, |u z| ≤ M) (hy : ∀ x' ∈ Ω, u x + inner ℝ (x' - x) y ≤ u x') : δ * ‖y‖ ≤ 2 * M

Subgradients are bounded by the size of the function. If y is a subgradient of u relative to Ω at x, the closed ball of radius δ ≥ 0 about x lies in Ω, and |u| ≤ M on that ball, then δ * ‖y‖ ≤ 2 * M.

theorem TauCeti.isClosed_setOf_mem_subdifferential {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → EReal} (hbot : ∀ (x : E), f x ≠ ⊥) {K : Set E} (hK : IsClosed K) (hKf : K ⊆ {x : E | f x ≠ ⊤}) (hf : ContinuousOn (fun (x : E) => (f x).toReal) K) : IsClosed {z : E × E | z.1 ∈ K ∧ z.2 ∈ subdifferential (innerₗ E) f z.1}

The graph of the subdifferential of f : E → EReal, never ⊥, over a closed set K is closed if f is finite on K and its real representative is continuous there.

theorem TauCeti.exists_norm_le_of_mem_subdifferential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {K : Set E} (hK : IsCompact K) (hKD : K ⊆ interior {x : E | f x ≠ ⊤}) : ∃ (R : ℝ), ∀ x ∈ K, ∀ y ∈ subdifferential (innerₗ E) f x, ‖y‖ ≤ R

Subgradients of a convex function are locally bounded. The subgradients of a convex f : E → EReal on a finite-dimensional real inner product space are bounded over a compact subset K of the interior of the effective domain.

theorem TauCeti.isCompact_setOf_mem_subdifferential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {K : Set E} (hK : IsCompact K) (hKD : K ⊆ interior {x : E | f x ≠ ⊤}) : IsCompact {z : E × E | z.1 ∈ K ∧ z.2 ∈ subdifferential (innerₗ E) f z.1}

The graph of the subdifferential of a convex f : E → EReal over a compact subset K of the interior of the effective domain is compact.

theorem TauCeti.isCompact_subgradientImage {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {K : Set E} (hK : IsCompact K) (hKD : K ⊆ interior {x : E | f x ≠ ⊤}) : IsCompact (subgradientImage (innerₗ E) f K)

Subgradient images of compact sets are compact. For a convex f : E → EReal on a finite-dimensional real inner product space, the subgradient image of a compact subset of the interior of the effective domain is compact.

theorem TauCeti.nonempty_subdifferential_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {x : E} (hx : x ∈ interior {x : E | f x ≠ ⊤}) : (subdifferential (innerₗ E) f x).Nonempty

Subgradients exist in the interior of the domain. A convex f : E → EReal on a finite-dimensional real inner product space has a subgradient at every interior point of its effective domain.

theorem TauCeti.eventually_nonempty_subdifferential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {x : E} (hdom : ∀ᶠ (x' : E) in nhds x, f x' ≠ ⊤) : ∀ᶠ (x' : E) in nhds x, (subdifferential (innerₗ E) f x').Nonempty

If a convex f : E → EReal is finite at every point near x, then it has a subgradient at every point near x.

theorem ConvexOn.exists_forall_add_inner_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} (hΩ : IsOpen Ω) (hu : ConvexOn ℝ Ω u) {x : E} (hx : x ∈ Ω) : ∃ (p : E), ∀ y ∈ Ω, u x + inner ℝ (y - x) p ≤ u y

Supporting hyperplanes of convex functions. A real function convex on an open subset Ω of a finite-dimensional real inner product space has a subgradient relative to Ω at every point x ∈ Ω: some p satisfies u x + ⟪y - x, p⟫ ≤ u y for every y ∈ Ω.

theorem TauCeti.exists_forall_add_apply_le_of_forall_frontier {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {S : Set E} {u : E → ℝ} (hS : IsCompact (closure S)) (hu : ContinuousOn u (closure S)) {x₀ : E} (hx₀ : x₀ ∈ S) {p : E →L[ℝ] ℝ} (hp : ∀ y ∈ frontier S, u x₀ + p (y - x₀) ≤ u y) : ∃ x ∈ S, ∀ y ∈ closure S, u x + p (y - x) ≤ u y

A slope of an affine function through a graph point over the domain that lies below u on the frontier is a supporting slope on the closure at some point of the domain.

theorem TauCeti.exists_forall_add_inner_le_of_forall_frontier {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {Ω : Set E} {u : E → ℝ} (hΩ : IsCompact (closure Ω)) (hu : ContinuousOn u (closure Ω)) {x₀ : E} (hx₀ : x₀ ∈ Ω) {p : E} (hp : ∀ x ∈ frontier Ω, u x₀ + inner ℝ (x - x₀) p ≤ u x) : ∃ x₁ ∈ Ω, ∀ x ∈ Ω, u x₁ + inner ℝ (x - x₁) p ≤ u x

Slopes below the boundary values are subgradients. Let Ω have compact closure, let u be continuous on its closure, and let x₀ ∈ Ω. If the affine function x ↦ u x₀ + ⟪x - x₀, p⟫ lies below u on the frontier of Ω, then p is a subgradient of u relative to Ω at some point x₁ ∈ Ω: u x₁ + ⟪x - x₁, p⟫ ≤ u x for every x ∈ Ω.

theorem TauCeti.exists_forall_add_inner_add_le_of_forall_frontier_le {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {Ω : Set E} {u w : E → ℝ} (hΩ : IsCompact (closure Ω)) (hu : ContinuousOn u (closure Ω)) (hw : ContinuousOn w (closure Ω)) (hfr : ∀ x ∈ frontier Ω, w x ≤ u x) {x₀ : E} (hx₀ : x₀ ∈ Ω) {p q : E} (hp : ∀ x ∈ Ω, w x₀ + inner ℝ (x - x₀) p ≤ w x) (hq : ‖q‖ * Metric.diam Ω ≤ w x₀ - u x₀) : ∃ x₁ ∈ Ω, ∀ x ∈ Ω, u x₁ + inner ℝ (x - x₁) (p + q) ≤ u x

Supporting slopes of a function lying above at x₀ and below on the frontier. Let Ω have compact closure, let u and w be continuous on its closure with w ≤ u on the frontier of Ω, and let p be a subgradient of w relative to Ω at x₀ ∈ Ω. Then for every q with ‖q‖ * diam Ω ≤ w x₀ - u x₀, the slope p + q is a subgradient of u relative to Ω at some point x₁ ∈ Ω. For q = 0 this says that the subgradients of w at points where u ≤ w are subgradients of u.

theorem TauCeti.exists_eventually_norm_le_of_tendstoLocallyUniformlyOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} {F : ι → E → ℝ} {u : E → ℝ} {Ω : Set E} (hΩ : IsOpen Ω) (hu : ContinuousOn u Ω) (hFu : TendstoLocallyUniformlyOn F u l Ω) {K : Set E} (hK : IsCompact K) (hKΩ : K ⊆ Ω) : ∃ (R : ℝ), ∀ᶠ (k : ι) in l, ∀ x ∈ K, ∀ (y : E), (∀ x' ∈ Ω, F k x + inner ℝ (x' - x) y ≤ F k x') → ‖y‖ ≤ R

Subgradients are eventually locally bounded. Let F k → u locally uniformly on an open set Ω, with u continuous on Ω, and let K ⊆ Ω be compact. Then the subgradients of F k relative to Ω at points of K are eventually bounded, uniformly in k.

theorem TauCeti.eventually_biUnion_subset_of_tendstoLocallyUniformlyOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [ProperSpace E] {ι : Type u_2} {l : Filter ι} {F : ι → E → ℝ} {u : E → ℝ} {Ω : Set E} (hΩ : IsOpen Ω) (hu : ContinuousOn u Ω) (hFu : TendstoLocallyUniformlyOn F u l Ω) {K : Set E} (hK : IsCompact K) (hKΩ : K ⊆ Ω) {V : Set E} (hV : IsOpen V) (hKV : ⋃ x ∈ K, {y : E | ∀ x' ∈ Ω, u x + inner ℝ (x' - x) y ≤ u x'} ⊆ V) : ∀ᶠ (k : ι) in l, ⋃ x ∈ K, {y : E | ∀ x' ∈ Ω, F k x + inner ℝ (x' - x) y ≤ F k x'} ⊆ V

Upper semicontinuity of subgradient images. Let F k → u locally uniformly on an open set Ω, with u continuous on Ω, and let K ⊆ Ω be compact. Then every open set V containing the subgradients of u relative to Ω at points of K eventually contains the subgradients of F k relative to Ω at points of K.