LemmaStatement: AI-adaptedProof: 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.

Submultiplicative root limit

Statement

Let $(u_{n})_{n \geq 1}$ be a positive-indexed family of nonnegative real numbers satisfying the submultiplicative inequality

$u_{m + n} \leq u_{m} u_{n} for all m, n \geq 1.$

Then the $N$ -indexed sequence $v_{j} : = u_{j + 1}^{1 / (j + 1)}$ ( $j \geq 0$ ) converges in $R$ . Writing the limit of the positive-indexed root family for this sequence limit,

$\lim_{n \to \infty} u_{n}^{1 / n} = \inf_{n \geq 1} u_{n}^{1 / n} .$

The case of a vanishing term is included: if $u_{k} = 0$ for some $k \geq 1$ , then $u_{n} = 0$ for all $n \geq k$ and both sides equal $0$ .

Facts & Assumptions

Given: A positive-indexed family $(u_{n})_{n \geq 1}$ of reals with $u_{n} \geq 0$ and $u_{m + n} \leq u_{m} u_{n}$ for all $m, n \geq 1$ ; put $u_{0} : = 1$ and extend the inequality by this convention, so that $u_{m + 0} = u_{m} \leq u_{m} u_{0}$ . Define $v_{j} = u_{j + 1}^{1 / (j + 1)}$ for $j \in N$ ; no zeroth root is defined.

[L1]

For every $a \geq 0$ and $n \geq 1$ there is a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ; moreover $0^{1 / n} = 0$ and $a^{1 / n} > 0$ when $a > 0$ (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ).

[L2]

For $x, y \geq 0$ and $n \geq 1$ : $x \leq y$ if and only if $x^{n} \leq y^{n}$ , and $x < y$ if and only if $x^{n} < y^{n}$ . Consequently $(x y)^{1 / n} = x^{1 / n} y^{1 / n}$ and $x \leq y$ implies $x^{1 / n} \leq y^{1 / n}$ , since both sides are nonnegative and have the same $n$ -th power (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ).

[L3]

For a sequence $(x_{k})$ of reals the limit superior and limit inferior are elements of $\overline{R}$ with ${lim inf}_{k} x_{k} \leq {lim sup}_{k} x_{k}$ , and $(x_{k})$ converges to $L \in R$ exactly when ${lim inf}_{k} x_{k} = {lim sup}_{k} x_{k} = L$ (Limit superior and limit inferior of a real sequence as $\inf_{n} \sup_{k \geq n} x_{k}$ and $\sup_{n} \inf_{k \geq n} x_{k}$ in $\overline{R}$ , A real sequence converges to $L \in R$ iff $lim inf x_{k} = lim sup x_{k} = L$ , and diverges to $\pm \infty$ iff both equal $\pm \infty$ ).

[L4]

If $x_{k} \leq y_{k}$ eventually, then ${lim sup}_{k} x_{k} \leq {lim sup}_{k} y_{k}$ and ${lim inf}_{k} x_{k} \leq {lim inf}_{k} y_{k}$ (If $x_{k} \leq y_{k}$ eventually then $lim sup x_{k} \leq lim sup y_{k}$ and $lim inf x_{k} \leq lim inf y_{k}$ ).

[L5]

For every real $c > 0$ , the $N$ -indexed sequence $d_{j} = c^{1 / (j + 1)}$ converges to $1$ (For every $a > 0$ , $a^{1 / n} \to 1$ ).

Proof

technique · direct

1.1

Put $L : = \inf {u_{n}^{1 / n} : n \geq 1}$ , a real number in $[0, \infty)$ because $u_{1}^{1 / 1} = u_{1}$ is finite and every term is $\geq 0$ ; by definition of the infimum, $u_{n}^{1 / n} \geq L$ for every $n \geq 1$ .

L1algebra

1.2

If $u_{k} = 0$ for some $k \geq 1$ then $u_{n} = 0$ for every $n \geq k$ : writing $n = k + (n - k)$ with $n - k \geq 0$ , the hypothesis and the convention $u_{0} = 1$ give $u_{n} \leq u_{k} u_{n - k} = 0$ , while $u_{n} \geq 0$ by assumption.

givenalgebra

1.3

Now suppose $u_{n} > 0$ for every $n \geq 1$ . Fix $k \geq 1$ , put $t : = u_{k}^{1 / k} > 0$ and $C_{k} : = \max {u_{r} : 0 \leq r < k} > 0$ ; then for every $n \geq k$ , writing $n = q k + r$ with $q \geq 1$ and $0 \leq r < k$ , iterated submultiplicativity gives $u_{n} \leq u_{k}^{q} u_{r} \leq u_{k}^{q} C_{k}$ .

givenL1algebra

2.1

Suppose $u_{k} = 0$ for some $k$ . Then $u_{n}^{1 / n} = 0$ for all $n \geq k$ by [step 1.2] and [L1], and $L = 0$ because the term $u_{k}^{1 / k} = 0$ occurs in the set whose infimum is $L$ ; hence $v_{j} = 0$ for $j \geq k - 1$ and $v_{j} \to 0 = L$ .

step 1.2step 1.1L1L3

2.2

With $t = u_{k}^{1 / k} > 0$ as in [step 1.3] the bound $u_{k}^{q} \leq t^{n} B_{k}$ holds for $n = q k + r \geq k$ and the constant $B_{k} : = \max (1, t^{- k})$ : indeed $u_{k}^{q} = (t^{k})^{q} = t^{k q} = t^{n - r}$ by the integer index laws, and the correction factor satisfies $t^{- r} \leq t^{- k} \leq B_{k}$ when $t \leq 1$ (then $r < k$ makes $t^{- r} \leq t^{- k}$ ) and $t^{- r} \leq 1 \leq B_{k}$ when $t \geq 1$ , so in both cases $t^{n - r} = t^{n} t^{- r} \leq t^{n} B_{k}$ .

step 1.3L1L2algebra

2.3

On the other hand every term satisfies $v_{j} = u_{j + 1}^{1 / (j + 1)} \geq L$ by [step 1.1], so the liminf clause of [L4] applied to the constant sequence $L$ gives $L = {lim inf}_{j} L \leq {lim inf}_{j} v_{j}$ , that is ${lim inf}_{j} v_{j} \geq L$ .

step 1.1L4

3.1

Define the positive constant $D_{k} : = \max (1, t^{- k}) C_{k}$ . Combining [step 1.3] and [step 2.2] gives $u_{n} \leq t^{n} D_{k}$ , hence $u_{n}^{1 / n} \leq t D_{k}^{1 / n}$ for every $n \geq k$ , taking $n$ -th roots by [L2].

step 1.3step 2.2L1L2

4.1

Apply [L5] to $d_{j} = D_{k}^{1 / (j + 1)}$ . Substituting $n = j + 1$ in step 3.1 gives $v_{j} \leq t d_{j}$ whenever $j + 1 \geq k$ . Since $d_{j} \to 1$ , for every real $ε > 0$ the inequality $d_{j} \leq 1 + ε$ holds eventually; hence $v_{j} \leq t (1 + ε)$ eventually, and [L4] gives ${lim sup}_{j} v_{j} \leq t (1 + ε)$ .

step 3.1L4L5algebra

5.1

Since $ε > 0$ was arbitrary in [step 4.1] and $t = u_{k}^{1 / k}$ , one has ${lim sup}_{j} v_{j} \leq u_{k}^{1 / k}$ for every $k \geq 1$ , hence ${lim sup}_{j} v_{j} \leq L$ .

step 4.1step 1.1algebra

6.1

In the positive case, [step 5.1] and [step 2.3] yield $lim sup \leq L \leq lim inf \leq lim sup$ , so all three (for the sequence $v$ ) are equal to $L$ and $v_{j} \to L$ by [L3]; in the vanishing case [step 2.1] gives the same conclusion. Hence in all cases $\lim_{n} u_{n}^{1 / n} = \inf_{n \geq 1} u_{n}^{1 / n}$ .

step 2.1step 5.1step 2.3L3∎

Depends on

Used by

Spectral radius formula Theorem

Dependency tree · two levels

50 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

Theo Bühler and Dietmar A. Salamon, Functional Analysis — the root-test step of Theorem 5.20, printed p. 222 (standard reference, not scraped)
Vahid Shirbisheh, Lectures on C-star Algebras, v2 — §2.3, printed pp. 30–33 (standard reference, not scraped)