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 an absolutely convex absorbing set is a seminorm

Statement

If $C$ is absolutely convex and absorbing, then $p_{C} (λ x) = ∣ λ ∣ p_{C} (x)$ for every scalar $λ$ , and $p_{C}$ is a seminorm. It need not be positive definite.

Facts & Assumptions

Given: An absolutely convex absorbing $C \subseteq X$ , $x \in X$ , and $λ \in K$ .

[F1]

For convex absorbing $C$ , $p_{C}$ is nonnegative, subadditive, and homogeneous for nonnegative real scalars (The gauge of a convex absorbing set is sublinear).

Proof

technique · direct

1.1

If $λ = 0$ the assertion follows from [F1]. For $λ \neq 0$ , balancedness gives $(λ / ∣ λ ∣) C = C$ : one inclusion is balancedness and the reverse follows by applying it to the inverse scalar.

F1givenalgebra

2.1

Hence $λ x \in t C$ exactly when $x \in (t / ∣ λ ∣) C$ , so taking infima yields $p_{C} (λ x) = ∣ λ ∣ p_{C} (x)$ . Together with [F1] this is precisely the seminorm axioms.

step 1.1F1algebra∎

Depends on

Used by

Gauges of norm balls and finite-dimensional ellipsoids Example

Dependency tree · two levels

5 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)