Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-09
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 open convex gauge is sublinear and recovers its set

Statement

Let U be an open convex neighbourhood of zero in a real or complex normed space X, and fix r>0 with B(0,r)U. Its gauge satisfies 0pU(x)x/r,pU(tx)=tpU(x)(t0), pU(x+y)pU(x)+pU(y),U={x:pU(x)<1}, pU(x)pU(y)xy/r. In particular it is a sublinear functional on the underlying real space. No symmetry identity is asserted.

Facts & Assumptions

[F1]

pU(x)=infSx for the nonempty positive admissible-scale set Sx, and pU(0)=0 (The finite gauge of an open convex neighbourhood of zero).

[F2]

For a nonempty lower-bounded real set and a lower bound l, one has l=infS if and only if for each ε>0 there is sS with s<l+ε (Epsilon characterisation of the infimum).

[F3]

Sublinearity means subadditivity and homogeneity for every real scalar at least zero (A sublinear functional on a real vector space).

Proof

Given: An open convex UX with 0U and r>0 such that B(0,r)U.

1.1

Write p=pU. The gauge definition gives p(x)0. For every t>x/r one has x/tB(0,r)U, so p(x)t. If p(x)>x/r, their midpoint is such a t smaller than p(x), impossible. Hence p(x)x/r.

givenF1algebra
1.2

For a>0, the condition sSax is equivalent to s/aSx, so Sax=aSx. The number ap(x) is a lower bound of this set. Conversely, for every ε>0, choose tSx with t<p(x)+ε/a; then atSax and at<ap(x)+ε. The infimum criterion gives p(ax)=ap(x). For a=0, both sides are zero by p(0)=0.

F1F2algebra
1.3

If s>p(x), choose sSx with s<s using the infimum criterion with ε=sp(x). Since 0<s/s<1, convexity and 0U give x/s=(s/s)(x/s)+(1s/s)0U. Thus every s>p(x) is admissible.

F1F2algebra
1.4

If p(x)<1, choose sSx with s<1 using the infimum criterion with ε=1p(x). Then 0<s<1 and x=s(x/s)+(1s)0U by convexity.

F1F2algebra
2.1

Given ε>0, set s=p(x)+ε and t=p(y)+ε. Both are positive and admissible by step 1.3. Convexity gives (x+y)/(s+t)=(s/(s+t))(x/s)+(t/(s+t))(y/t)U. Hence p(x+y)s+t=p(x)+p(y)+2ε. If the desired inequality failed with positive difference d, taking ε=d/4 would give dd/2. Therefore p(x+y)p(x)+p(y). Together with step 1.2, this is sublinearity on the real space.

step 1.2step 1.3F1F3algebra
2.2

Conversely, let xU. For x=0, p(x)=0<1. If x0, openness gives η>0 with B(x,η)U. Put d=η/(2x)>0. Since (1+d)xx=η/2, (1+d)xU, so 1/(1+d)Sx and p(x)1/(1+d)<1. This proves both inclusions in the asserted set equality.

step 1.4F1algebra
3.1

Subadditivity gives p(x)p(y)p(xy)xy/r and, with x,y interchanged, p(y)p(x)p(yx)xy/r. These two real inequalities yield the Lipschitz bound. When x=y both differences are zero; no use of p(v)=p(v) occurs.

step 1.1step 2.1algebra

Source notes

Brezis Lemma 1.2, p.6, full proof; Teschl Lemma 5.1, p.138, full proof.

Depends on

Used by

Dependency tree · two levels

12 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