Hessians and convexity

Let f : E → EReal be convex (convex real epigraph, never ⊥) on a real inner product space, with real representative F x = (f x).toReal and D the interior of the effective domain {x | f x ≠ ⊤}. At a point of D near which F is differentiable, the gradient ∇ F is a subgradient of f, so it is a monotone map. This file records what monotonicity says about the derivative H of ∇ F at a point where it exists, the Hessian of F represented as an endomorphism of E.

H is a positive operator: it is symmetric by Schwarz's theorem, and ⟪H v, v⟫ ≥ 0 because t ↦ ⟪∇ F (x + t • v), v⟫ is nondecreasing. In particular det H ≥ 0.

Conversely, a real function on an open convex set whose gradient has a derivative H x with ⟪H x v, v⟫ ≥ 0 at every point is convex: along each segment it has a nonnegative second derivative.

Main statements

• TauCeti.isPositive_of_hasFDerivAt_gradient and ConvexOn.isPositive_of_hasFDerivAt_gradient — the Hessian of a convex function, extended-real or real-valued, is a positive operator;
• TauCeti.convexOn_of_hasFDerivAt_gradient — a function with positive Hessian on an open convex set is convex there.

References

• R. T. Rockafellar, Convex Analysis, Princeton Mathematical Series 28, 1970, Theorem 4.5 (second-order characterisation of convexity) and §24 (monotonicity of the subdifferential).

theorem TauCeti.isPositive_of_hasFDerivAt_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {H : E →L[ℝ] E} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {x : E} (hx : x ∈ interior {x : E | f x ≠ ⊤}) (hd : ∀ᶠ (y : E) in nhds x, DifferentiableAt ℝ (fun (x' : E) => (f x').toReal) y) (hH : HasFDerivAt (gradient fun (x' : E) => (f x').toReal) H x) : (↑H).IsPositive

The Hessian of a convex function is a positive operator. Let f : E → EReal be convex and never ⊥, let x be an interior point of its effective domain near which the real representative F is differentiable, and let H be the derivative of ∇ F at x. Then H is symmetric and ⟪H v, v⟫ ≥ 0 for every v.

theorem ConvexOn.isPositive_of_hasFDerivAt_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H : E →L[ℝ] E} {s : Set E} {F : E → ℝ} (hF : ConvexOn ℝ s F) {x : E} (hx : s ∈ nhds x) (hd : ∀ᶠ (y : E) in nhds x, DifferentiableAt ℝ F y) (hH : HasFDerivAt (gradient F) H x) : (↑H).IsPositive

The Hessian of a real convex function is a positive operator. Let F : E → ℝ be convex on a neighbourhood s of x and differentiable near x, and let H be the derivative of ∇ F at x. Then H is symmetric and ⟪H v, v⟫ ≥ 0 for every v.

theorem TauCeti.convexOn_of_hasFDerivAt_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} (hs : Convex ℝ s) (hso : IsOpen s) {F : E → ℝ} {H : E → E →L[ℝ] E} (hF : ∀ x ∈ s, DifferentiableAt ℝ F x) (hH : ∀ x ∈ s, HasFDerivAt (gradient F) (H x) x) (hpos : ∀ x ∈ s, ∀ (v : E), 0 ≤ inner ℝ ((H x) v) v) : ConvexOn ℝ s F

A function with positive Hessian is convex. Let s be an open convex set and let F : E → ℝ be differentiable on s, with the gradient ∇ F having derivative H x at each x ∈ s. If ⟪H x v, v⟫ ≥ 0 for every x ∈ s and every v, then F is convex on s. This is the converse of ConvexOn.isPositive_of_hasFDerivAt_gradient.