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.
has empty subdifferential on the unit-sphere boundary
Statement refuted
Every convex real-valued function on a closed convex domain has a subgradient at every domain point.
Facts & Assumptions
Given: Let for (The -norms for rational , and ) and define on , with convexity as in Convex and strictly convex functions on Euclidean convex sets. For the comparison with the interior-point theorem, assume the Axiom of Choice and the Axiom of Countable Choice (The Axiom of Choice, The Axiom of Countable Choice ()).
A vector is a subgradient of at when for every in the domain (Subgradients and the subdifferential of a convex function).
Assuming the Axiom of Choice and the Axiom of Countable Choice, a convex function has nonempty subdifferential at every interior point of its domain (A convex function has a subgradient at every interior point of its domain).
The Euclidean norm is a norm on and satisfies the triangle inequality (Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation).
Counterexample
Put . The lifted vectors have norm one in . By the triangle inequality in [L2], the convex combination has norm at most one, so its nonnegative last coordinate is at most . Negating gives the convexity inequality for on the whole closed ball.
Fix a unit vector and suppose satisfied [F1] at . Testing for gives The right side is unbounded as approaches , impossible for the fixed vector . Hence .
Step 2.1 applies to every sphere point, while [L1] gives nonempty subdifferentials at every interior point. Thus the interior hypothesis in the existence theorem is sharp.
Depends on
- Convex and strictly convex functions on Euclidean convex sets
- Subgradients and the subdifferential of a convex function
- A convex function has a subgradient at every interior point of its domain
- Cauchy-Schwarz $\lvert\langle x,y\rangle\rvert \le \lVert x\rVert_2\lVert y\rVert_2$ with its equality case, the triangle inequality for $\lVert\cdot\rVert_2$, the parallelogram law and polarisation
- The $p$-norms $\lVert x\rVert_p$ for rational $p \ge 1$, and $\lVert x\rVert_\infty$
- The Axiom of Choice
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
37 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
- CUHK ENGG 5501 Convex Analysis notes (standard reference, not scraped)