Where a convex function is differentiable

The continuity theory of one-sided derivatives, read as an existence theory for derivatives. A convex function on the line has a two-sided derivative off a countable set, and that derivative is continuous and nondecreasing there. In a fixed direction y, the two-sided directional derivative exists exactly where x ↦ f'(x; y) is continuous, and that happens on a dense subset of int (dom f).

Main results

• continuousAt_rightDeriv_iff — a continuity criterion: f'₊ is continuous at x exactly when f'₋(x) = f'₊(x).
• countable_leftDeriv_ne_rightDeriv — the jump set of f'₊ is countable.
• differentiableAtFn_iff_leftDeriv_eq_rightDeriv — on the line, differentiability at an interior point of dom f is the equality of the two one-sided derivatives.
• countable_not_differentiableAtFn, continuousAt_rightDeriv_of_differentiableAtFn, subset_closure_differentiableAtFn — a countable exceptional set, continuity of the derivative where it exists, and density of the points of differentiability (Theorem 25.3 in [^1]).
• continuousAt_dirDeriv_iff, subset_closure_twoSided_dirDeriv — the same in a fixed direction (Theorem 25.4 in [^1]).

Implementation notes

rightDeriv f is defined on the whole line, not only on the set D where the derivative exists, so the continuity assertions here are the ordinary ContinuousAt, stronger than the book's "continuous relative to D". Monotonicity is likewise global.

Three of the classical hypotheses are absent. The countability and density clauses need no closedness of f, because only the easy half of the continuity criterion is used; closedness enters only in the converse, through the one-sided limit formulas for f'₊. The directional form needs no y ≠ 0, since at y = 0 both sides hold, and its density clause is proved by restricting to a line rather than through Lebesgue measure, so it needs no finite-dimensionality.

References

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

A continuity criterion for f'₊

theorem Tdaf.ConvexAnalysis.leftDeriv_eq_rightDeriv_of_continuousAt {f : ℝ → EReal} {x : ℝ} (hf : ConvexFn f) (hp : Proper f) (hc : ContinuousAt (rightDeriv f) x) : leftDeriv f x = rightDeriv f x

Continuity of f'₊ at x forces the two-sided derivative: monotonicity gives f'₊(z) → ⨆ {f'₊(z) | z < x} as z ↑ x, continuity identifies that supremum with f'₊(x), and every f'₊(z) with z < x lies below f'₋(x). Unlike the converse this needs no closedness.

theorem Tdaf.ConvexAnalysis.continuousAt_rightDeriv_iff {f : ℝ → EReal} (hf : ClosedProperConvexFn f) (x : ℝ) : ContinuousAt (rightDeriv f) x ↔ leftDeriv f x = rightDeriv f x

For a closed proper convex function on the line, the nondecreasing function f'₊ is continuous at x exactly when it agrees with f'₋ there.

theorem Tdaf.ConvexAnalysis.countable_leftDeriv_ne_rightDeriv {f : ℝ → EReal} (hf : ConvexFn f) (hp : Proper f) : {x : ℝ | leftDeriv f x ≠ rightDeriv f x}.Countable

The jump set of f'₊ is countable: f'₊ is nondecreasing into the second-countable order topology of EReal, and its discontinuity set contains the set where f'₋ ≠ f'₊.

The two-sided derivative on the line

theorem Tdaf.ConvexAnalysis.dirDeriv_eq_of_leftDeriv_eq_rightDeriv {f : ℝ → EReal} {x : ℝ} (hf : ConvexFn f) (hp : Proper f) (hx : x ∈ interior (dom f)) (h : leftDeriv f x = rightDeriv f x) (v : ℝ) : dirDeriv f x v = ↑((rightDeriv f x).toReal * v)

On the line a two-sided derivative makes f'(x; ·) linear: positive homogeneity reduces f'(x; v) to the directions ±1, where the values are f'₊(x) and -f'₋(x).

theorem Tdaf.ConvexAnalysis.differentiableAtFn_iff_leftDeriv_eq_rightDeriv {f : ℝ → EReal} {x : ℝ} (hf : ConvexFn f) (hp : Proper f) (hx : x ∈ interior (dom f)) : DifferentiableAtFn f x ↔ leftDeriv f x = rightDeriv f x

On the line, a convex function is differentiable at an interior point of its effective domain exactly when its two one-sided derivatives agree there.

Differentiability off a countable set

theorem Tdaf.ConvexAnalysis.countable_not_differentiableAtFn {f : ℝ → EReal} (hf : ConvexFn f) (hp : Proper f) : {x : ℝ | x ∈ interior (dom f) ∧ ¬DifferentiableAtFn f x}.Countable

First assertion: a convex function on the line is differentiable at all but countably many points of the interior of its effective domain. No closedness is needed, so the usual preliminary extension of f to a closed proper convex function on ℝ is not made.

theorem Tdaf.ConvexAnalysis.continuousAt_rightDeriv_of_differentiableAtFn {f : ℝ → EReal} {x : ℝ} (hf : ClosedProperConvexFn f) (hx : x ∈ interior (dom f)) (hd : DifferentiableAtFn f x) : ContinuousAt (rightDeriv f) x

Second assertion: the derivative is continuous where it exists. Stronger than "continuous relative to D": rightDeriv f is continuous at x on the whole line.

theorem Tdaf.ConvexAnalysis.subset_closure_differentiableAtFn {f : ℝ → EReal} (hf : ConvexFn f) (hp : Proper f) : interior (dom f) ⊆ closure {z : ℝ | DifferentiableAtFn f z}

Third assertion: the points of differentiability are dense in the interior of the effective domain, a countable subset of ℝ having dense complement.

Restriction to a line

theorem Tdaf.ConvexAnalysis.convexFn_lineRestrict {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} (hf : ConvexFn f) (x y : E) : ConvexFn fun (t : ℝ) => f (x + t • y)

The restriction of f to the line t ↦ x + t • y is convex.

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

The restriction of f to a line through a point of dom f is proper.

theorem Tdaf.ConvexAnalysis.dirDeriv_lineRestrict {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → EReal) (x y : E) (t v : ℝ) : dirDeriv (fun (s : ℝ) => f (x + s • y)) t v = dirDeriv f (x + t • y) (v • y)

The one-dimensional restriction computes the directional derivative along the line. This is what lets the one-dimensional theory be applied in a fixed direction.

The two-sided derivative in a fixed direction

theorem Tdaf.ConvexAnalysis.upperSemicontinuousAt_dirDeriv_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {x : E} [FiniteDimensional ℝ E] (hf : ConvexFn f) (hp : Proper f) (hx : x ∈ interior (dom f)) (y : E) : UpperSemicontinuousAt (fun (z : E) => dirDeriv f z y) x

For a fixed direction y, the function z ↦ f'(z; y) is upper semicontinuous at every interior point of dom f.

theorem Tdaf.ConvexAnalysis.dirDeriv_sub_smul_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {x : E} (hp : Proper f) (hfx : f x < ⊤) (y : E) {l : ℝ} (hl : 0 < l) : dirDeriv f (x - l • y) y ≤ -dirDeriv f x (-y)

For every λ > 0, f'(x - λ y; y) ≤ (f x - f (x - λ y)) / λ ≤ -f'(x; -y): the first inequality is the term of the defining infimum at x - λ y with step λ, which lands exactly on x, and the second is the corresponding term at x in the direction -y, negated. No convexity and no interiority are used, only properness.

theorem Tdaf.ConvexAnalysis.continuousAt_dirDeriv_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {x : E} [FiniteDimensional ℝ E] (hf : ConvexFn f) (hp : Proper f) (hx : x ∈ interior (dom f)) (y : E) : ContinuousAt (fun (z : E) => dirDeriv f z y) x ↔ dirDeriv f x y = -dirDeriv f x (-y)

First assertion: on the interior of dom f, the set where the two-sided directional derivative in the direction y exists is exactly the set where x ↦ f'(x; y) is continuous. The usual y ≠ 0 is not needed — at y = 0 both sides hold.

theorem Tdaf.ConvexAnalysis.subset_closure_twoSided_dirDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) (y : E) : interior (dom f) ⊆ closure {z : E | z ∈ interior (dom f) ∧ dirDeriv f z y = -dirDeriv f z (-y)}

Density: the points of int (dom f) at which the two-sided directional derivative in the direction y exists are dense in int (dom f). Proved on a line rather than through Lebesgue measure: t ↦ f (x + t • y) is a proper convex function of one variable whose one-sided derivatives at t are f'(x + t y; ±y), and its jump set is countable.