LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Uniform convexity gives unique asymptotic centers

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ . Let $X$ be a real or complex uniformly convex Banach space, let $(x_{n})_{n \in N}$ be a bounded sequence in $X$ , and let $C \subseteq X$ be nonempty, norm closed and convex. Define its asymptotic-radius function on $C$ by

$r (y) : = {lim sup}_{n \to \infty} ∥ x_{n} - y ∥ (y \in C) .$

Then there is a unique $c \in C$ such that

$r (c) = \inf_{y \in C} r (y) .$

The point $c$ is the asymptotic center of $(x_{n})$ relative to $C$ . Convexity uses real coefficients even when $X$ is complex.

Facts & Assumptions

Given: $X$ , $(x_{n})$ and $C$ as in the statement, with $R : = \inf_{y \in C} r (y)$ once that real infimum has been justified.

[F1]

For a bounded real sequence, its limit superior is the real infimum of its real tail suprema. If its limit superior is the real number $L$ , then for every $η > 0$ its terms are eventually less than $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}$ , For finite $L$ : $L = lim sup x_{k}$ iff for every $ε > 0$ one has $x_{k} < L + ε$ eventually and $x_{k} > L - ε$ frequently).

[F2]

Every nonempty subset of $R$ bounded below has a real infimum (Every nonempty set bounded below has an infimum).

[F3]

${A C}_{ω}$ supplies one member of each member of a sequence of nonempty sets (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F4]

For every real $η > 0$ there is an integer $N \geq 1$ with $1 / N < η$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[F5]

Uniform convexity says that for each $θ \in (0, 2]$ there is $δ > 0$ such that unit-ball vectors separated by at least $θ$ have midpoint norm at most $1 - δ$ (Uniformly convex Banach space).

[F6]

Every norm-Cauchy sequence in $X$ converges in $X$ (Banach space).

[F7]

A closed subset of a metric space contains the limit of each convergent sequence in it (A point lies in the closure of $A$ iff some sequence in $A$ converges to it, and a set is closed iff it is sequentially closed, using its choice-free closed-to-sequentially-closed direction).

[F8]

Convexity keeps real midpoints in $C$ , also in a complex normed space (Convex sets and continuous real-hyperplane separation in a normed space).

[F9]

Canonical positive naturals increase with their indices, and inversion reverses strict inequalities between positive elements. Consequently $1 / (j + 1) \to 0$ (Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order).

Proof

1.1

Choose $B \geq 0$ with $∥ x_{n} ∥ \leq B$ for every $n$ . For each $y \in C$ , $0 \leq ∥ x_{n} - y ∥ \leq B + ∥ y ∥$ , so [F1] makes $r (y)$ a finite nonnegative real. Thus ${r (y) : y \in C}$ is nonempty and bounded below by zero, and [F2] defines a finite real $R \geq 0$ .

givenF1F2

2.1

The function $r$ is $1$ -Lipschitz. Indeed, fix $y, z \in C$ and $η > 0$ . By [F1], eventually $∥ x_{n} - z ∥ < r (z) + η$ , and then $∥ x_{n} - y ∥ \leq ∥ x_{n} - z ∥ + ∥ z - y ∥ < r (z) + ∥ z - y ∥ + η$ . The corresponding tail supremum, and hence its infimum $r (y)$ , is at most $r (z) + ∥ z - y ∥ + η$ . If $r (y) > r (z) + ∥ z - y ∥$ , [F4] supplies a positive reciprocal smaller than that gap, contradicting this inequality. Hence $r (y) \leq r (z) + ∥ z - y ∥$ ; exchanging $y, z$ gives $∣ r (y) - r (z) ∣ \leq ∥ y - z ∥$ .

step 1.1F1F4

2.2

For $j \in N$ put $E_{j} : = {y \in C : r (y) < R + 1 / (j + 1)}$ . Each $E_{j}$ is nonempty by the defining greatest-lower-bound property of $R$ . Applying [F3] once to this countable family produces a sequence $(y_{j})$ with $y_{j} \in E_{j}$ for every $j$ . This is the proof's exact use of ${A C}_{ω}$ .

step 1.1F2F3

3.1

Suppose first that $R = 0$ . Given $ε > 0$ , [F4] and [F9] give a threshold $J$ such that $1 / (j + 1) < ε / 8$ for $j \geq J$ . For $j, k \geq J$ , [F1] gives one index $n$ beyond the two eventual thresholds at tolerance $ε / 8$ . Then $∥ y_{j} - y_{k} ∥ \leq ∥ y_{j} - x_{n} ∥ + ∥ x_{n} - y_{k} ∥ < r (y_{j}) + r (y_{k}) + ε / 4 < ε / 2.$ Thus $(y_{j})$ is Cauchy when $R = 0$ .

step 2.2F1F4F9

3.2

Now suppose $R > 0$ , and fix $ε > 0$ . Put $θ : = \min {1, ε / (R + 1)} \in (0, 1]$ . Choose the $δ > 0$ from [F5], replace it by $δ_{0} : = \min {δ, 1 / 2}$ , and set $a : = \min {1 / 2, R δ_{0} / 2} > 0, t : = R + a .$ Then $t < R + 1$ and $t (1 - δ_{0}) < R$ . By [F4] and [F9], for all sufficiently large $j, k$ one has $r (y_{j}), r (y_{k}) < t$ . If such $j, k$ also satisfied $∥ y_{j} - y_{k} ∥ \geq ε$ , [F1] would give a common tail on which both $∥ x_{n} - y_{j} ∥ < t$ and $∥ x_{n} - y_{k} ∥ < t$ . On that tail the vectors $u_{n} : = \frac{x_{n} - y_{j}}{t}, v_{n} : = \frac{x_{n} - y_{k}}{t}$ belong to the unit ball and satisfy $∥ u_{n} - v_{n} ∥ = ∥ y_{j} - y_{k} ∥ / t > ε / (R + 1) \geq θ$ . Uniform convexity therefore gives $∥ x_{n} - \frac{y_{j} + y_{k}}{2} ∥ = t ∥ \frac{u_{n} + v_{n}}{2} ∥ \leq t (1 - δ_{0})$ throughout that tail. The midpoint lies in $C$ by [F8], and [F1] now yields $r ((y_{j} + y_{k}) / 2) \leq t (1 - δ_{0}) < R$ , contradicting the definition of $R$ . Consequently $∥ y_{j} - y_{k} ∥ < ε$ for all sufficiently large $j, k$ ; $(y_{j})$ is Cauchy also when $R > 0$ .

step 2.2F1F4F5F8F9

4.1

By [F6] there is $c \in X$ with $y_{j} \to c$ , and [F7] gives $c \in C$ . The lower-bound property gives $R \leq r (c)$ . Conversely, the Lipschitz estimate gives $r (c) \leq r (y_{j}) + ∥ c - y_{j} ∥ < R + 1 / (j + 1) + ∥ c - y_{j} ∥$ for every $j$ . If $r (c) > R$ , [F4], [F9] and convergence make the sum $1 / (j + 1) + ∥ c - y_{j} ∥$ smaller than this positive gap for some $j$ , a contradiction. Hence $r (c) = R$ , so a minimizer exists.

step 2.1step 2.2step 3.1step 3.2F4F6F7F9

4.2

To prove uniqueness, let $c, d \in C$ both have radius $R$ . If $R = 0$ and $c \neq d$ , take $η = ∥ c - d ∥ / 3$ in [F1]; at one sufficiently large $n$ the triangle inequality gives $∥ c - d ∥ < 2 η$ , a contradiction. If $R > 0$ and $c \neq d$ , repeat step 3.2 with $ε = ∥ c - d ∥$ , the same $θ, δ_{0}, a, t$ , and the two fixed points $c, d$ . Their radii equal $R < t$ , so [F1] again gives a common tail, while [F5] makes the radius of their midpoint at most $t (1 - δ_{0}) < R$ . By [F8] that midpoint lies in $C$ , the same contradiction. Thus $c = d$ .

step 1.1step 3.2F1F5F8

5.1

Steps 4.1 and 4.2 give the asserted unique asymptotic center. The zero space is included: its only nonempty subset is the singleton ${0}$ and the radius is zero. A singleton $C$ is likewise immediate. The argument uses only real norms and real midpoints, so it is unchanged over complex scalars. The set $C$ is expressly nonempty; no minimizer is asserted for the empty set.

step 4.1step 4.2∎

Source notes

Lim defines asymptotic radius and center for decreasing tails of a bounded net in §1, then proves nonemptiness and uniqueness for closed convex subsets of uniformly convex Banach spaces in Proposition 1 and Theorem 1 on printed pp. 422–423. The local proof is independent and makes its Countable Choice use explicit.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 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

Teck-Cheong Lim, On Asymptotic Centers and Fixed Points of Nonexpansive Mappings (standard reference, not scraped)