LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06

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.

The gauge of a convex absorbing set is sublinear

Statement

If $C \subseteq X$ is convex and absorbing, then its gauge satisfies $p_{C} (r x) = r p_{C} (x)$ for $r \geq 0$ and $p_{C} (x + y) \leq p_{C} (x) + p_{C} (y)$ . Thus $p_{C}$ is a real sublinear functional.

Facts & Assumptions

Given: A convex absorbing set $C \subseteq X$ and $x, y \in X$ .

[F1]

The gauge is $p_{C} (z) = \inf {t > 0 : z \in t C}$ , and its defining set is nonempty (Minkowski functional of an absorbing set).

Proof

technique · direct

1.1

For $r > 0$ , $r x \in t C$ holds exactly when $x \in (t / r) C$ ; taking infima gives $p_{C} (r x) = r p_{C} (x)$ , while $r = 0$ gives $p_{C} (0) = 0$ .

F1givenalgebra

1.2

Absorption and convexity first give $0 \in C$ . Given $a > p_{C} (x)$ and $b > p_{C} (y)$ , choose $s < a$ , $t < b$ with $x \in s C$ , $y \in t C$ ; convexity with $0$ enlarges these to $x = a c$ , $y = b d$ for some $c, d \in C$ . Then $(a c + b d) / (a + b) \in C$ , hence $x + y \in (a + b) C$ .

F1givenchoose

2.1

Therefore $p_{C} (x + y) \leq a + b$ for every such $a, b$ ; letting them decrease to the two infima proves subadditivity.

step 1.2F1algebra∎

Depends on

Used by

A gauge of a nonbalanced set need not be a seminorm Counterexample
An open convex neighbourhood is recovered from its gauge Lemma
The gauge of an absolutely convex absorbing set is a seminorm Lemma
Separate a point from an open convex set Theorem

Dependency tree · two levels

4 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, Lemma 5.1 (standard reference, not scraped)