TheoremStatement: 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.

A convex function on an open convex set is locally Lipschitz

Statement

Let $n \in N$ , let $U \subseteq R^{n}$ be open and convex, and let $f : U \to R$ be convex. Then $f$ is locally Lipschitz on $U$ : every $a \in U$ has a neighbourhood on which one finite constant bounds $∣ f (x) - f (y) ∣$ by $∥ x - y ∥_{2}$ .

Facts & Assumptions

Given: The function and domain in the Statement. When $n \geq 1$ , the sup and Euclidean norms have the conventions of The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ and are genuine norms inducing the published metrics Each $∥ \cdot ∥_{p}$ is a norm on $R^{n}$ , and the induced metrics are exactly $d_{1}$ , $d_{2}$ and $d_{\infty}$ of the published metric-spaces page.

[L1]

If a closed sup-norm cube about an interior point lies in the convex domain, then $f$ is bounded above on that cube and bounded above and below on its concentric half-sized cube (A convex function is bounded above and below on a smaller interior cube).

[F1]

A function is Lipschitz with constant $L$ when its output distance is at most $L$ times its input distance for every pair of domain points (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction).

Proof

technique · direct

1.1

If $U = \emptyset$ , the conclusion is vacuous. If $n = 0$ and $U$ is nonempty, then $U = R^{0}$ is a singleton and $f$ is Lipschitz with constant zero. Hence assume $n \geq 1$ and fix $a \in U$ . Choose $r > 0$ such that $Q (a, 2 r) \subseteq U$ . Apply [L1] to obtain $M \geq 0$ with $∣ f ∣ \leq M$ on the half cube $Q (a, r)$ , and use $Q (a, r / 2)$ as the inner cube of test points.

L1given

2.1

Take distinct $x, y \in Q (a, r / 2)$ , put $d = ∥ y - x ∥_{\infty}$ , and extend the ray from $x$ through $y$ until it first reaches $z \in \partial Q (a, r)$ . Writing $z = x + s (y - x) / d$ , one has $s \geq r / 2$ and $y = (1 - d / s) x + (d / s) z$ . Convexity and step 1.1 give $f (y) - f (x) \leq 4 M d / r$ ; reversing $x, y$ gives $∣ f (y) - f (x) ∣ \leq 4 M ∥ x - y ∥_{\infty} / r$ .

step 1.1L1algebra

3.1

Since $∥ x - y ∥_{\infty} \leq ∥ x - y ∥_{2}$ , step 2.1 is the condition [F1] on $Q (a, r / 2)$ with constant $4 M / r$ . Hence $f$ is locally Lipschitz at every $a \in U$ .

step 2.1F1algebra∎

Depends on

Used by

A convex function on an open convex set is continuous Corollary

Dependency tree · two levels

38 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

D. Bertsekas, MIT 6.253 Convex Analysis and Optimization, Lecture 4 (standard reference, not scraped)
S. Boyd and L. Vandenberghe, Convex Optimization, §3.1 (standard reference, not scraped)