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.
Local convexity, convex and balanced sets, and the continuous dual
Definition
Let be a real or complex TVS (Topological vector spaces over the real and complex fields). A subset is convex if whenever and , with real coefficients even when is complex. Its convex hull is In particular . This is the smallest convex superset of : single-term sums contain , and concatenating two weighted lists proves convexity. Every convex superset contains every finite convex combination: induct on list length, remove a zero coefficient, and otherwise group the first terms with weight . If the value is ; if , divide those first weights by and apply the induction hypothesis followed by binary convexity.
A set is balanced if for every scalar with , and absolutely convex if it is convex and balanced. Empty sets satisfy both conditions; every nonempty balanced set contains zero, by taking , and is symmetric, by taking twice.
The TVS is locally convex if every zero-neighborhood contains a convex zero-neighborhood. Equivalently it has a base of open convex zero-neighborhoods. Indeed, if is a convex zero-neighborhood, its interior contains zero. For and , the set is open: it is a union of translates of the open set , using Translations, dilations and absorption in a topological vector space. It contains and lies in , so this point lies in the interior. The cases are immediate. Conversely an open convex zero-neighborhood is a convex zero-neighborhood.
A seminorm is a finite-valued satisfying and for all scalars. It is continuous if continuous for the given topology and the usual real topology. Thus , but need not imply . Over the underlying real vector space it is sublinear in the sense of A sublinear functional on a real vector space; restriction of scalars is justified by A field is a vector space over itself, and over any subfield every -vector space is a -vector space by restricting the scalars.
The continuous dual consists of all continuous -linear maps . The scalar field is a vector space over itself by A field is a vector space over itself, and over any subfield every -vector space is a -vector space by restricting the scalars, clause 1, so these are linear functionals as in Linear functionals and the algebraic dual . Pointwise operations make a vector subspace of the algebraic dual: zero is continuous, and sums and scalar multiples are continuous by the scalar-operation continuity proved in Translations, dilations and absorption in a topological vector space. Explicitly, continuity of at bounds their errors by to control the sum, and by to control . All linear axioms are inherited pointwise.
For separation inequalities write , or over . The real part is continuous because . It is real-linear. No Hahn–Banach or choice principle is part of these definitions.
Depends on
- Topological vector spaces over the real and complex fields
- Translations, dilations and absorption in a topological vector space
- Linear functionals and the algebraic dual $V^*=\mathcal L(V,F)$
- A sublinear functional on a real vector space
- A field is a vector space over itself, and over any subfield $K \subseteq F$ every $F$-vector space is a $K$-vector space by restricting the scalars
Used by
- A convex function can have a nonconvex maximum set Counterexample
- Minkowski gauge for an open convex zero-neighborhood Definition
- Arbitrary products of the scalar field are locally convex Example
- Coordinate functionals give an explicit uniform separating gap Example
- Continuity, sublinearity and strict sublevels of an open convex gauge Lemma
- Convex closures and hulls of finitely many compact convex sets Lemma
- Open and closed balanced convex zero-neighborhood refinements Lemma
- Continuous separation when one convex set is open Theorem
- The continuous dual separates points in a Hausdorff locally convex space Theorem
- Uniform strict separation of compact and closed convex sets Theorem
Dependency tree · two levels
26 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
- Gerald Teschl, Topics in Real and Functional Analysis (17 November 2017) (standard reference, not scraped)
- Theo Bühler and Dietmar Salamon, Functional Analysis (8 June 2017) (standard reference, not scraped)
- Harald Hanche-Olsen, Topological vector spaces, version 1.6 (bibliographic origin; complete local argument replaces unavailable backing) (standard reference, not scraped)