Condition (c) of essential smoothness, in directional-derivative form

Given conditions (a) and (b) of essential smoothness, condition (c) — the norms of the gradients blow up at the boundary of C = int (dom f) — may be replaced by

(c')  f'(x + λ(a − x); a − x) ↓ −∞ as λ ↓ 0,   for every a ∈ C and every x ∉ C.

Both say the same thing at a single point x, namely that ∂f x = ∅: (c) because ∂f has a closed graph and is recovered from limits of gradients, and (c') because along the line through x and a the directional derivative collapses to −∞ exactly when ∂f x is empty. Those two halves are separate theorems below, so either can be used on its own.

Main results

• closedProperConvexFn_lineRestrict — the restriction of a closed proper convex function to a line is closed proper convex, based at any point of the line, not only a point of dom f.
• subgradient_eq_empty_iff_tendsto_dirDeriv, subgradient_eq_empty_iff_tendsto_norm_fderiv — conditions (c') and (c) at x each say that ∂f x = ∅.
• essentiallySmooth_iff_tendsto_dirDeriv — (c) may be replaced by (c') (Lemma 26.2 in [^1]).

Implementation notes

f is assumed closed, where the book says "without loss of generality" and replaces f by cl f; every consumer already carries ClosedFn f. Condition (c') is stated as a Tendsto to 𝓝 ⊥: the book's ↓ also records monotonicity of λ ↦ f'(x + λ(a − x); a − x), but only the value of the limit is used.

References

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

The restriction to a line, based at an arbitrary point

theorem Tdaf.ConvexAnalysis.closedFn_lineRestrict {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} (hp : Proper f) (hcl : ClosedFn f) (x y : E) : ClosedFn fun (t : ℝ) => f (x + t • y)

The restriction of a closed function to a line is closed.

theorem Tdaf.ConvexAnalysis.proper_lineRestrict_of_mem_dom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {x y : E} (hp : Proper f) {t₀ : ℝ} (ht : x + t₀ • y ∈ dom f) : Proper fun (t : ℝ) => f (x + t • y)

The restriction of a proper function to a line is proper as soon as the line meets dom f. Unlike proper_lineRestrict, this does not ask the base point to lie in dom f — here the base point x is precisely the one that may fail to.

theorem Tdaf.ConvexAnalysis.closedProperConvexFn_lineRestrict {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {x y : E} (hf : ConvexFn f) (hp : Proper f) (hcl : ClosedFn f) {t₀ : ℝ} (ht : x + t₀ • y ∈ dom f) : ClosedProperConvexFn fun (t : ℝ) => f (x + t • y)

The restriction of a closed proper convex function to a line meeting dom f is closed proper convex, which is what the one-dimensional theory runs on.

theorem Tdaf.ConvexAnalysis.rightDeriv_lineRestrict_eq_dirDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} (hp : Proper f) (x y : E) {t : ℝ} (ht : ∃ (s : ℝ), t < s ∧ f (x + s • y) < ⊤) : rightDeriv (fun (s : ℝ) => f (x + s • y)) t = dirDeriv f (x + t • y) y

The right derivative of the restriction is the directional derivative along the line. Both sides are −∞ where f (x + t y) = ⊤, so the only hypothesis needed is that the line meets dom f somewhere to the right of t; without it g'₊(t) is +∞ by fiat and the two differ.

The directional derivative along a segment

theorem Tdaf.ConvexAnalysis.tendsto_dirDeriv_lineRestrict {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {a : E} (hf : ConvexFn f) (hp : Proper f) (hcl : ClosedFn f) (ha : a ∈ dom f) (x : E) : Filter.Tendsto (fun (t : ℝ) => dirDeriv f (x + t • (a - x)) (a - x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (rightDeriv (fun (s : ℝ) => f (x + s • (a - x))) 0))

Along the segment from x to a, the directional derivative f'(x + t(a − x); a − x) tends, as t decreases to 0, to the right derivative at 0 of the restriction of f to that line.

Condition (c') at a single point

theorem Tdaf.ConvexAnalysis.rightDeriv_lineRestrict_zero_eq_bot_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {a : E} (hf : ConvexFn f) (hp : Proper f) (ha : a ∈ intrinsicInterior ℝ (dom f)) (x : E) : rightDeriv (fun (s : ℝ) => f (x + s • (a - x))) 0 = ⊥ ↔ subgradient (innerₗ E) f x = ∅

g'₊(0) = −∞ exactly when f has no subgradient at x, where g is the restriction of f to the line from x towards a relative interior point a of dom f. Off dom f both sides hold; on dom f the right derivative is f'(x; a − x), which is −∞ exactly when ∂f x is empty.

theorem Tdaf.ConvexAnalysis.subgradient_eq_empty_iff_tendsto_dirDeriv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {a : E} (hf : ConvexFn f) (hp : Proper f) (hcl : ClosedFn f) (ha : a ∈ intrinsicInterior ℝ (dom f)) (x : E) : subgradient (innerₗ E) f x = ∅ ↔ Filter.Tendsto (fun (t : ℝ) => dirDeriv f (x + t • (a - x)) (a - x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds ⊥)

Condition (c') at x says exactly that f has no subgradient at x.

theorem Tdaf.ConvexAnalysis.subgradient_eq_empty_iff_tendsto_norm_fderiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) (hcl : ClosedFn f) (hne : (interior (dom f)).Nonempty) (hdiff : ∀ ⦃z : E⦄, z ∈ interior (dom f) → DifferentiableAtFn f z) (x : E) : subgradient (innerₗ E) f x = ∅ ↔ ∀ (zs : ℕ → E), (∀ (i : ℕ), zs i ∈ interior (dom f)) → Filter.Tendsto zs Filter.atTop (nhds x) → Filter.Tendsto (fun (i : ℕ) => ‖fderiv ℝ (fun (w : E) => (f w).toReal) (zs i)‖) Filter.atTop Filter.atTop

Condition (c) at x says exactly that f has no subgradient at x. Forwards, a bounded subsequence of gradients has a convergent sub-subsequence whose limit is a subgradient at x. Backwards, a subgradient at x is built from limits of gradients, and that produces a convergent sequence of gradients which (c) forbids.

theorem Tdaf.ConvexAnalysis.tendsto_norm_fderiv_iff_tendsto_dirDeriv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {a : E} (hf : ConvexFn f) (hp : Proper f) (hcl : ClosedFn f) (hne : (interior (dom f)).Nonempty) (hdiff : ∀ ⦃z : E⦄, z ∈ interior (dom f) → DifferentiableAtFn f z) (ha : a ∈ interior (dom f)) (x : E) : (∀ (zs : ℕ → E), (∀ (i : ℕ), zs i ∈ interior (dom f)) → Filter.Tendsto zs Filter.atTop (nhds x) → Filter.Tendsto (fun (i : ℕ) => ‖fderiv ℝ (fun (w : E) => (f w).toReal) (zs i)‖) Filter.atTop Filter.atTop) ↔ Filter.Tendsto (fun (t : ℝ) => dirDeriv f (x + t • (a - x)) (a - x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds ⊥)

At a single point: given (a) and (b), condition (c) at x and condition (c') at x in the direction of any a ∈ C say the same thing.

theorem Tdaf.ConvexAnalysis.essentiallySmooth_iff_tendsto_dirDeriv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) (hcl : ClosedFn f) (hne : (interior (dom f)).Nonempty) (hdiff : ∀ ⦃z : E⦄, z ∈ interior (dom f) → DifferentiableAtFn f z) : EssentiallySmooth f ↔ ∀ x ∉ interior (dom f), ∀ a ∈ interior (dom f), Filter.Tendsto (fun (t : ℝ) => dirDeriv f (x + t • (a - x)) (a - x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds ⊥)

For a closed proper convex function satisfying (a) and (b), essential smoothness is condition (c'), the collapse of the directional derivative to −∞ along every segment reaching a point outside C = int (dom f).