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 can have a nonconvex maximum set
Statement refuted
The maximum set of a continuous convex real function on a compact convex set is always a face.
Here a face of a convex set means a convex subset such that, whenever , and , both belong to . A subset with just this endpoint property is called extremal; convexity is an additional requirement for being a face.
Facts & Assumptions
Given: and , .
Convexity uses real coefficients in (Local convexity, convex and balanced sets, and the continuous dual).
Closed bounded subsets of are compact in its usual product topology (A subset of with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology, dimension one).
Counterexample
The interval is convex since implies for . It is closed, its complement being the open rays and , and bounded by one in absolute value. Hence it is nonempty compact convex. For , , which proves continuity on directly.
For and , Thus , the defining convexity inequality for a function. It includes and , where equality holds.
On , with equality exactly when or , because and both factors are nonnegative. The maximum set is therefore . Its midpoint is zero, and , so . Thus is not convex and cannot be a face. This refutes the claim with a continuous convex function on a compact convex set.
Nevertheless is extremal. If with and , then . Each summand is nonnegative and each coefficient is positive, so . Similarly a combination equal to gives and forces . Thus the endpoint property holds even though convexity fails. All witnesses and computations are explicit and choice-free.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
17 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
- Harald Hanche-Olsen, Topological vector spaces, version 1.6 (bibliographic origin; complete local argument replaces unavailable backing) (standard reference, not scraped)