CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

An everywhere-positive-definite Hessian implies strict convexity

Statement

Let $f : U \to R$ be $C^{2}$ on an open convex set. An everywhere-positive-definite Hessian implies strict convexity.

Facts & Assumptions

Given: The line-restriction formula from A $C^{2}$ function is convex exactly when its Hessian is positive semidefinite and the total chain rule The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ .

[F1]

A symmetric quadratic form is positive definite when $q_{H} (h) > 0$ for every $h \neq 0$ (Positive definite, negative definite, semidefinite, and indefinite quadratic forms).

[L1]

If a real function is continuous on an order-convex interval, differentiable at every interior point, and has positive derivative at every interior point, then it is strictly increasing (On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed).

[L2]

For a continuous real function on a closed interval that is differentiable in its interior, one secant slope equals an interior derivative (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

Proof

technique · direct

1.1

Fix distinct $x, y \in U$ , put $v = y - x \neq 0$ , and define $ϕ (t) = f (x + t v)$ . The chain rule gives $ϕ^{''} (t) = ⟨ H_{f} (x + t v) v, v ⟩ > 0$ by [F1].

F1givenalgebra

2.1

Applying [L1] to $ϕ^{'}$ makes $ϕ^{'}$ strictly increasing. For $0 < t < 1$ , apply [L2] on $[0, t]$ and $[t, 1]$ : the two secant slopes equal $ϕ^{'} (r)$ and $ϕ^{'} (s)$ for some $r < t < s$ , so the first slope is strictly smaller than the second. Rearranging gives $ϕ (t) < (1 - t) ϕ (0) + t ϕ (1)$ . This is strict convexity of $f$ ; the endpoints are excluded exactly as the definition requires.

step 1.1L1L2algebra∎

Depends on

Used by

The Euclidean norm and its square are convex, with a ball of subgradients at zero for the norm Example

Dependency tree · two levels

28 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

S. Boyd and L. Vandenberghe, Convex Optimization, §3.1.4 (standard reference, not scraped)