LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)

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.

Concave supporting bound, affine maxima, and Hessian sign

Statement

Let $U \subseteq R^{d}$ , $d \geq 1$ , be open, and let $f : U \to R$ be differentiable. For $x, y \in U$ , suppose the whole segment $[x, y]$ lies in $U$ and its concavity inequality holds:

$f (x + t (y - x)) \geq (1 - t) f (x) + t f (y) (0 \leq t \leq 1) .$

Then the supporting bound is $f (y) \leq f (x) + D f (x) (y - x)$ . In particular this bound holds for every $x, y$ in any convex subset of $U$ on which $f$ is concave. No global convexity of $U$ is assumed.

Let $A : R^{d} \to R^{k}$ be linear, $b \in R^{k}$ , and $F = U \cap {x : A x = b}$ . Suppose $x_{*} \in F$ , $D f (x_{*}) h = 0$ for every $h \in \ker A$ , and for every $y \in F$ the segment $[x_{*}, y]$ lies in $U$ and has the displayed concavity inequality. Then $x_{*}$ is a global maximum of $f$ on $F$ . If $F$ is convex and $f ∣_{F}$ is strictly concave, meaning the inequality is strict for distinct endpoints and $0 < t < 1$ , the maximum is unique.

For the curvature clause, suppose $f \in C^{2} (U)$ and fix $x \in U$ . If, for every $h \in R^{d}$ , all sufficiently small $∣ t ∣$ satisfy $x \pm t h \in U$ and

$f (x + t h) + f (x - t h) \leq 2 f (x),$

then the Hessian bilinear form $D^{2} f (x) = D (D f) (x)$ satisfies $D^{2} f (x) [h, h] \leq 0$ for every $h$ . This condition holds whenever $f$ is concave on a neighborhood of $x$ . Thus a $C^{2}$ function concave on an open convex region has negative-semidefinite Hessian there. Concavity alone does not assert strict curvature.

Facts & Assumptions

Given: The open domain, differentiability, and the stated admissible segments and concavity inequalities; affine constraints and stationarity for the maximum clause; strict concavity or $C^{2}$ regularity only for their respective further clauses.

[F1]

A convex subset of $R^{m}$ contains every line segment between two of its points: every segment between points of a convex set stays in that set.

[F2]

The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder: $f (x + h) = f (x) + D f (x) h + o (∥ h ∥)$ at each point of differentiability.

[F3]

If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ and $C^{k}$ Euclidean maps and diffeomorphisms: continuous first and second coordinate partials give total derivatives of $f$ and its vector of first partials; thus a $C^{2}$ function restricted to the line $t \mapsto x + t h$ is $C^{2}$ , with second derivative $D^{2} f (x + t h) [h, h]$ .

[F4]

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)$ : a real function continuous on a closed interval and differentiable inside it has an interior derivative equal to its endpoint secant slope.

Proof

1.1givenF1F2algebra

For an admissible pair $x, y$ and $0 < t < 1$ , the given concavity inequality yields $f (y) - f (x) \leq (f (x + t (y - x)) - f (x)) / t$ . By [F2] the right side tends to $D f (x) (y - x)$ as $t ↓ 0$ , proving the supporting bound. The convex-region specialization follows from [F1] and the concavity inequality on that region; it does not require any other segment of $U$ to be admissible.

2.1givenF1step 1.1algebra

For $y \in F$ , linearity gives $A (y - x_{*}) = 0$ , so stationarity yields $D f (x_{*}) (y - x_{*}) = 0$ . The assumed segment from $x_{*}$ to $y$ permits step 1.1, hence $f (y) \leq f (x_{*})$ , proving global maximality. If $F$ is convex and two distinct points maximize $f$ , their midpoint lies in $F$ by [F1], while strict concavity would give a strictly larger midpoint value. Thus the maximum is unique under the further hypothesis.

3.1givenF1F3F4algebra∎

Under the $C^{2}$ and local midpoint hypotheses, fix $h$ and put $g (t) = f (x + t h)$ near zero. By [F3], $g^{''} (0) = D^{2} f (x) [h, h]$ . Define $R (t) = g (t) - g (0) - g^{'} (0) t - \frac{1}{2} g^{''} (0) t^{2}$ . Differentiability of $g^{'}$ gives $R^{'} (s) = o (∣ s ∣)$ ; [F4] on the interval between $0$ and $t$ gives $R (t) = t R^{'} (ξ_{t}) = o (t^{2})$ , since $∣ ξ_{t} ∣ \leq ∣ t ∣$ . Therefore $(g (t) + g (- t) - 2 g (0)) / t^{2} \to g^{''} (0)$ . Its numerator is nonpositive by hypothesis, so $D^{2} f (x) [h, h] \leq 0$ . Concavity on a neighborhood implies that midpoint hypothesis on every sufficiently short centered segment; this proves all Hessian claims without strengthening the domain assumptions.

Depends on

Dependency tree · 2 levels

Sources

P. Bianchi, O. Fercoq, and W. Hachem, Elements of Convex Analysis and Optimization, §1.5