Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Spectral radius formula

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let A be a unital complex Banach algebra and let a∈A, with spectral radius r(a) (Spectral radius). Then

r(a)  =  lim⁡n→∞∥an∥1/n  =  inf⁡n≥1∥an∥1/n,

Here the root sequence means vj=∥aj+1∥1/(j+1) for j∈N; a0=1, and no zeroth root is used. The Axiom of Choice is used only through the spectrum nonemptiness and Hahn–Banach content of Spectral radius, The norm of a vector is the supremum of |f(x)| over the dual unit ball and the declared polynomial spectral-mapping supplier; the analytic estimate itself is choice-free.

Facts & Assumptions

Given: A unital complex Banach algebra A, an element a∈A, and the spectrum, resolvent set, resolvent and spectral radius of a (Spectrum and resolvent set in a Banach algebra, Spectral radius).

[L1]

A is complete with ∥1∥=1, ∥xy∥≤∥x∥ ∥y∥ and am+n=aman for all m,n≥0 (Unital Banach algebra).

[L2]

If ∥y∥<1 then 1−y is invertible with (1−y)−1=∑n≥0yn and ∥(1−y)−1−∑n≤Nyn∥≤∥y∥N+1/(1−∥y∥) (Neumann series).

[L3]

R(z,a)=(z1−a)−1 on ρA(a), and R(z,a)−R(w,a)=(w−z)R(z,a)R(w,a) for z,w∈ρA(a) (Spectrum and resolvent set in a Banach algebra, Resolvent identity).

[L4]

ρA(a) is open and z↦R(z,a) is holomorphic there with continuous norm, with R′(z,a)=−R(z,a)2 (Resolvent is Banach-valued holomorphic).

[L5]

If f is holomorphic on a disc containing the closed disc of radius ρ>0 around 0, then for every n≥0 f(n)(0)=n!2πi∫∣ζ∣=ρf(ζ)ζn+1 dζ (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle).

[L6]

For every integer m and every ρ>0, ∫∣ζ∣=ρζm dζ equals 2πi when m=−1 and 0 otherwise (On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1).

[L7]

For every x in a complex normed space, ∥x∥=sup⁡{∣φ(x)∣:φ∈X∗, ∥φ∥≤1} (The norm of a vector is the supremum of |f(x)| over the dual unit ball).

[L8]

With roots interpreted as the zero-based sequence uj+11/(j+1), if un≥0 and um+n≤umun for all m,n≥1, then lim⁡nun1/n=inf⁡nun1/n (Submultiplicative root limit).

[L9]

For every polynomial p, σA(p(a))=p(σA(a)), so in particular σA(an)={λn:λ∈σA(a)} for n≥1 (Polynomial spectral mapping).

[L10]

r(a)=max⁡{∣z∣:z∈σA(a)} and r(b)≤∥b∥ for every b∈A (Spectral radius).

[L11]

For every c>0 the sequence dj=c1/(j+1), j∈N, converges to 1 (For every a>0, a1/n→1).

[L12]

For a rectifiable contour, the modulus of the integral is at most its length times an upper bound for the integrand modulus (ML estimate: a contour integral is bounded by a supremum bound times path length).

[A1]

The standing hypothesis is the Axiom of Choice, used through [L10], [L7] and the declared [L9] interface (The Axiom of Choice).

Proof

technique · direct
1.1L1L3L10A1algebra

First, if a=0, then r(a)=0 by 0≤r(a)≤∥a∥ in [L10], and every positive power and root norm is zero, proving the formula. In the remainder assume a≠0, so ∥a∥>0 and divisions by this number are legitimate. For z≠0 one has 1−za=−z (a−z−11); hence 1−za is invertible exactly when a−z−11 is, that is exactly when z−1∈ρA(a).

1.2L1algebra

For every n≥1 one has ∥am+n∥≤∥am∥ ∥an∥ for all m,n≥1, so the positive-indexed family un:=∥an∥ is submultiplicative and nonnegative, and its root sequence is vj=uj+11/(j+1) for j≥0.

1.3L9L10algebra

For every n≥1, [L9] gives σA(an)={λn:λ∈σA(a)}, hence by [L10] applied to an and the multiplicativity of the modulus, r(an)=max⁡{∣λ∣n:λ∈σA(a)}=r(a)n; and r(an)≤∥an∥ by the last clause of [L10], so r(a)n≤∥an∥.

2.1step 1.1L2L1algebra

For ∣z∣<1/∥a∥ one has ∥za∥=∣z∣ ∥a∥<1, so [L2] applies to y:=za and gives (1−za)−1=∑n≥0anzn; comparing with the identity of [step 1.1] this is a power series in z whose value at z=0 is 1 and whose linear coefficient is a.

2.2step 1.1L10L3

Fix a real R>r(a) and put DR:={z∈C:∣z∣<1/R}. For z∈DR with z≠0 one has ∣z−1∣>R>r(a), so z−1∉σA(a) because every spectral point has modulus at most r(a); by [step 1.1] the element 1−za is invertible. Hence the function h(z):=(1−za)−1 for z≠0, h(0):=1, is a well-defined map DR→A.

3.1step 2.2step 1.1L3L4

h is complex differentiable at every z0∈DR, z0≠0: by [step 1.1] one has h(z)=z−1R(z−1,a) for z≠0, so with u:=z−1, v:=z0−1 the difference is h(z)−h(z0)=uR(u)−vR(v)=(v−u) a R(u)R(v), the identity following from the resolvent identity [L3] in the form R(u)−R(v)=(v−u)R(u)R(v) together with the rearrangement 1−vR(v)=−aR(v) of vR(v)=1+aR(v); since v−u=(z−z0)/(zz0), the difference quotient is h(z)−h(z0)z−z0=a R(z−1)R(z0−1)zz0, which converges to a R(z0−1)2/z02 as z→z0 by continuity of the resolvent [L4] and of 1/z.

4.1step 2.1step 3.1L2L1algebra

At z0=0 the map h is complex differentiable with h′(0)=a: by [step 2.1], h(z)=1+za+∑n≥2anzn for ∣z∣<1/∥a∥, and the remainder is bounded by ∑n≥2∥a∥n∣z∣n=∣z∣2∥a∥2/(1−∣z∣ ∥a∥)=o(∣z∣). Combined with [step 3.1] this shows that h is holomorphic on DR.

5.1step 4.1L4algebra

Let φ∈A∗ be a bounded linear functional and let g:=φ∘h:DR→C. Since h is holomorphic by [step 4.1] and φ is continuous linear, g is holomorphic on DR with g′(z)=φ(h′(z)).

6.1step 2.2step 4.1step 5.1L5

Fix R′ with r(a)<R′<R and put DR′:={z:∣z∣<1/R′}. The argument of steps 2.2-4.1 with R′ in place of R shows that h is holomorphic on DR′; since 1/R<1/R′, the disc DR′ contains the closed disc of radius 1/R around 0, the same inverse formula extends h consistently, and g=φ∘h extends by that formula as well. Thus [L5] applies to this extended g with ρ=1/R and gives g(n)(0)=n!2πi∫∣ζ∣=1/Rg(ζ)ζ−n−1 dζ for every n≥0.

7.1step 6.1step 2.1L2L5L6L12algebra

For 0<ρ<min⁡(1/R, 1/∥a∥) the series of [step 2.1] converges uniformly on the circle ∣ζ∣=ρ, so g(ζ)=φ((1−ζa)−1)=∑k≥0φ(ak)ζk uniformly there, and [L5] also applies on this smaller circle. For fixed n, the uniform remainder after multiplying by ζ−n−1 is bounded by ∥φ∥ρ−n−1(ρ∥a∥)N+1/(1−ρ∥a∥), which tends to zero. By [L12] its integral tends to zero. Integrating the finite sums and using [L6] therefore gives g(n)(0)=n! φ(an) for every n≥0.

8.1step 6.1step 7.1step 4.1L4L12algebra

Norm estimate for the coefficients, using [L12] on the circle of length 2π/R: for n≥0, by [step 7.1] and the integral formula of [step 6.1], ∣φ(an)∣=12π∣∫∣ζ∣=1/Rg(ζ)ζ−n−1dζ∣≤(sup⁡∣ζ∣=1/R∥h(ζ)∥)∥φ∥ Rn; the supremum is finite because [step 6.1] places the circle ∣ζ∣=1/R as a compact subset of the larger disc DR′, on which the argument of [step 4.1] makes h holomorphic and hence continuous.

9.1step 8.1step 1.2L7L8L11algebra

Put CR:=sup⁡∣ζ∣=1/R∥h(ζ)∥<∞. This constant is positive because h(1/R) is invertible and therefore nonzero. Taking the supremum in [step 8.1] over all φ with ∥φ∥≤1 and using [L7] gives ∥an∥≤CRRn for every n≥0; hence vj≤RCR1/(j+1) for every j≥0. By [L8] and step 1.2, vj has a real limit Q equal to the stated infimum. By [L11], CR1/(j+1)→1, and passing to these real limits gives Q≤R. (If Q>R, convergence of both sequences would contradict their termwise inequality.) Since this holds for every R>r(a), Q≤r(a): otherwise choose R=(Q+r(a))/2.

10.1step 1.1step 1.2step 1.3step 9.1L8∎

By [L8] applied to the submultiplicative family un=∥an∥ of [step 1.2], the limit Q:=lim⁡jvj=inf⁡n∥an∥1/n exists; [step 9.1] gives Q≤r(a), while [step 1.3] gives ∥an∥1/n≥r(a) for every n, hence Q≥r(a). Therefore Q=r(a) and the formula holds for a≠0; step 1.1 already proved the zero case.

Depends on

Dependency tree · 2 levels

Sources