The finitary content of sunny nonexpansive retractions

TL;DR

This paper employs proof mining techniques to extract explicit uniform rates of metastability for the convergence of approximants to fixed points of pseudocontractive mappings in certain Banach spaces, extending classical results.

Contribution

It introduces a novel proof mining approach to derive explicit convergence rates in Banach spaces with specific geometric properties, utilizing the existence of a modulus of uniqueness.

Findings

Derived a uniform rate of metastability for fixed point approximations

Extended proof mining techniques to Banach spaces with uniform convexity and smoothness

Produced explicit bounds interpretable in higher-type systems

Abstract

We use techniques of proof mining to extract a uniform rate of metastability (in the sense of Tao) for the strong convergence of approximants to fixed points of uniformly continuous pseudocontractive mappings in Banach spaces which are uniformly convex and uniformly smooth, i.e. a slightly restricted form of the classical result of Reich. This is made possible by the existence of a modulus of uniqueness specific to uniformly convex Banach spaces and by the arithmetization of the use of the limit superior. The metastable convergence can thus be proved in a system which has the same provably total functions as first-order arithmetic and therefore one may interpret the resulting proof in G\"odel's system $T$ of higher-type functionals. The witness so obtained is then majorized (in the sense of Howard) in order to produce the final bound, which is shown to be definable in the subsystem $T_1$. This piece of information is further used to obtain rates of metastability to results which were previously only analyzed from the point of view of proof mining in the context of Hilbert spaces, i.e. the convergence of the iterative schemas of Halpern and Bruck.

Equations

$$T_t:C\to C,T_t(y):=tT(y)+(1-t)x.$$

$$\forall x\in C\forall t\ge 0(Qx+t(x-Qx)\in C\to Q(Qx+t(x-Qx))=Qx)$$

$$\forall x\in C\forall y\in E(⟨x-Qx,j(y-Qx)⟩\le 0)$$

$$x_{n+1}:={\lambda }_{n+1}u+(1-{\lambda }_{n+1})T{x}_n$$

$$x_{n+1}:=\left(1-{\lambda }_n\right)x_n+{\lambda }_{n}T{x}_n-{\lambda }_n{\theta }_n\left(x_n-x_1\right)$$

$$(\ast )\forall k\in \mathbb{N}\forall g\in {\mathbb{N}}^{\mathbb{N}}\exists N\le \Theta (k,g)\forall n,m\in [N,N+g(N)]\left(\Vert x_n-x_m\Vert <\frac{1}{k+1}\right),$$

$$\forall k\in \mathbb{N}\forall g\in {\mathbb{N}}^{\mathbb{N}}\exists N\in \mathbb{N}\forall n,m\in [N,N+g(N)]\left(\Vert x_n-x_m\Vert <\frac{1}{k+1}\right),$$

$$F(z):=\underset{n\to \infty }{\mathrm{limsup}}\Vert x_{t_n}-z{\Vert }^2,$$

$$(\ast \ast )\forall z\in C\exists a\in {\mathbb{R}}^{+}(a=\underset{n\to \infty }{\mathrm{limsup}}\Vert x_{t_n}-z{\Vert }^2),$$

$$\delta_{X}(\varepsilon):=\inf\left\{1-\left\|\frac{x+y}{2}\right\|\bigm{|}\|x\|=\|y\|=1,\|x-y\|\geq\varepsilon\right\}$$

$${\delta }_X(\epsilon )$$

$$\Vert \frac{x+y}{2}\Vert \le 1-\eta (\epsilon ).$$

$${\psi }_{b,\eta }(\epsilon ):=\min \left(\frac{{\left(\min \left(\frac{\epsilon }{2},\frac{{\epsilon }^2}{72b}{\eta }^2\left(\frac{\epsilon }{2b}\right)\right)\right)}^2}{4},\frac{{\epsilon }^2}{48}{\eta }^2\left(\frac{\epsilon }{2b}\right)\right).$$

$${\Vert \frac{x+y}{2}\Vert }^2+{\psi }_{b,\eta }(\epsilon )\le \frac{1}{2}\Vert x{\Vert }^2+\frac{1}{2}\Vert y{\Vert }^2.$$

$$J(x):=\{x^{\ast }\in X^{\ast }\mid x^{\ast }(x)=\Vert x{\Vert }^2,\Vert x^{\ast }\Vert =\Vert x\Vert \}.$$

$$\underset{h\to 0}{\lim }\frac{\Vert x+hy\Vert -\Vert x\Vert }{h}$$

$$\Vert x+y{\Vert }^2\le \Vert x{\Vert }^2+2⟨y,j(x+y)⟩$$

$$\Vert x+y{\Vert }^2$$

$$=⟨x,j(x+y)⟩+⟨y,j(x+y)⟩$$

$$\le \Vert x+y\Vert \Vert x||+⟨y,j(x+y)⟩$$

$$\le \frac{1}{2}(\Vert x{\Vert }^2+\Vert x+y{\Vert }^2)+⟨y,j(x+y)⟩,$$

$$\rho_{X}(t):=\sup\left\{\frac{\|x+y\|+\|x-y\|}{2}-1\bigm{|}\|x\|=1,\|y\|=t\right\},$$

$$\Vert x+y\Vert +\Vert x-y\Vert \le 2+\epsilon \Vert y\Vert .$$

$$r_1(\epsilon ):=\min (\epsilon ,2),r_2(b):=\max (b,1),{\omega }_{\tau }(b,\epsilon ):=\frac{r_1(\epsilon {)}^2}{12r_2(b)}\cdot \tau \left(\frac{r_1(\epsilon )}{2r_2(b)}\right).$$

$$Q(Qx+t(x-Qx))=Qx,\text{mbox}ifQx+t(x-Qx)\in C.$$

$$⟨x-Qx,j(y-Qx)⟩\le 0.$$

$$⟨x-Q_{1}x,j(Q_{2}x-Q_{1}x)⟩\le 0$$

$$⟨x-Q_{2}x,j(Q_{1}x-Q_{2}x)⟩\le 0.$$

$$t\Vert x-y\Vert \le \Vert (t+1)(x-y)-(Tx-Ty)\Vert .$$

$$\left(1+\frac{1}{t}\right)\Vert x-y\Vert$$

$$\le \Vert \left(1+\frac{1}{t}\right)(x-y)-\frac{1}{t}(Tx-Ty)\Vert +\frac{1}{t}\Vert x-y\Vert ,$$

$$\Vert x-y\Vert \le \Vert \left(1+\frac{1}{t}\right)(x-y)-\frac{1}{t}(Tx-Ty)\Vert .$$

Full text

Mathematics Subject Classification 2010: 47H06, 47H09, 47H10, 03F10.

Keywords: Proof mining, sunny nonexpansive retractions, metastability, resolvents, pseudocontractions, functional interpretation, Halpern iteration, Bruck iteration, uniformly convex Banach spaces, uniformly smooth Banach spaces.

1 Introduction

Let $(X,\|\cdot\|)$ be a real Banach space, $C\subseteq X$ be a nonempty bounded closed convex subset and $T:C\to C$ be a nonexpansive mapping. For $t\in(0,1)$ and $x\in C,$ let $x_{t}$ be the unique fixed point of the strict contraction

[TABLE]

In 1967, Browder [9] and Halpern [33] independently proved in the case where $X$ is a Hilbert space that for $t\to 1,$ the path $(x_{t})$ strongly converges and its limit is the fixed point of $T$ which is closest to $x,$ i.e. $Px,$ where $P:C\to Fix(T)$ is the metric projection onto $Fix(T).$ Both proofs for the strong convergence do not readily generalize even to the class of $L^{p}$ spaces (other than $L^{2}$).

That the strong convergence does hold in this case was finally shown in 1980, when Reich established in the celebrated paper [60] that it actually holds in any uniformly smooth space. Moreover, Reich showed that the limit is $Qx,$ where $Q$ is the unique sunny nonexpansive retraction $Q:C\to Fix(T)$. This result has subsequently been extended in many ways including the context of families of operators [1, 2, 3].

The significance of Reich’s theorem is twofold:

• •

It provides for the first time an algorithmic approach to the construction of sunny nonexpansive retractions. This aspect is highlighted e.g. in [21, 1].

• •

Many important iterative algorithms in nonlinear analysis are shown to be strongly convergent by proving that they asymptotically approach $(x_{t_{n}})$ (for some suitable sequence $(t_{n})\subseteq(0,1)$ converging to $1$).

We start discussing the first item in more detail. Nonexpansive retractions were first considered by Bruck in [11], who showed – using Zorn’s lemma – that $Fix(T)$ is a nonexpansive retract of $C,$ whenever $X$ is a real reflexive strictly convex Banach space. This result was generalized further in [12], in particular, to reflexive Banach spaces which have the conditional fixed point property for nonexpansive mappings which e.g. includes all uniformly smooth spaces. Since metric projections onto closed convex subsets are nonexpansive only in Hilbert spaces, nonexpansive retractions are, already for $L^{p}$ spaces (again, other than $L^{2}$), very different from metric projections and may not even exist although the metric projection does. For example, Bruck showed in [14] that no real Banach space $X$ with $\dim X\geq 3$ has a bounded smooth subset $E\subset X$ with nonempty interior which is the range of a nonexpansive retraction $Q:X\to E$ unless $X$ is a Hilbert space.

Retractions $Q:C\to E\subseteq C$ are called sunny if the property

[TABLE]

holds. In smooth Banach spaces, for a retraction $Q$ to be nonexpansive and sunny it is necessary and sufficient for the variational inequality (where $j$ denotes the single-valued normalized duality map)

[TABLE]

to hold, which in Hilbert spaces characterizes the metric projection. Thus, the relevance of sunny nonexpansive retractions is that they are in many respects the right substitute for the metric projection outside Hilbert spaces. From this characterization it follows that there is at most one sunny nonexpansive retraction $Q:C\to E$ in smooth spaces (in [13], Bruck used the term ‘nonexpansive projection’ instead of the nowadays common name ‘sunny nonexpansive retraction’). If $X$ is even uniformly smooth and strictly convex and $E=Fix(T)$ is the fixed point set of a nonexpansive mapping $T:C\to C,$ then the unique sunny nonexpansive retraction $Q:C\to Fix(T)$ necessarily exists [13]. Bruck’s proof is, however, highly nonconstructive. Reich’s theorem establishes that the sunny nonexpansive retraction can be obtained as the limit of objects $x_{t}$ which are constructively available (since Banach’s fixed point theorem is constructive). Our logical analysis of the proofs due to Morales of Reich’s theorem implies that the pointwise existence of sunny nonexpansive retracts can be carried out in a logically fairly weak formal system (see Remark 6.6) which is of foundational interest.

As stated in the second item above, the great relevance of Reich’s theorem for algorithmic purposes can also be seen from the fact that it implies the strong convergence of important iterative algorithms: in [33], the so-called Halpern iteration (starting from some $x_{0}\in C$ and using $u\in C$ as anchor)

[TABLE]

is considered for $(\lambda_{n})\subset[0,1]$ and – in Hilbert spaces – shown to converge to $Pu$ for the metric projection $P:C\to Fix(T)$ under very restrictive conditions on $(\lambda_{n}).$ In a milestone paper [67], Wittmann generalized this to much more general sequences $(\lambda_{n})$ including for the first time the case $\lambda_{n}:=1/(n+1).$ If $T$ is linear and $u=x_{0}$, then $x_{n}$ coincides (for this choice of $(\lambda_{n})$) with the ergodic average $\frac{1}{n+1}\sum^{n}_{i=0}T^{i}x_{0}$ and so Wittmann’s theorem is a nonlinear generalization of the classical von Neumann mean ergodic theorem, while remaining strongly convergent (without linearity, the usual ergodic averages are known to converge only weakly by results due to [6] and [26]). In [62], Wittmann’s theorem is generalized to uniformly smooth Banach spaces by reducing the strong convergence of $(x_{n})$ to that of $(x_{t})$ and then applying Reich’s theorem (in fact, [62] considers a somewhat larger class of spaces). For Halpern’s more restrictive sequences $(\lambda_{n}),$ this had already been shown in [60].

Reich [60] established his theorem not only for nonexpansive mappings but even for set-valued accretive operators satisfying the range condition which, in particular, covers the important class of continuous pseudocontractions, introduced by Browder [8], which extend the class of nonexpansive mappings and which play a crucial role in the abstract formulation of Cauchy problems. For pseudocontractions one can no longer use the Halpern iterative schema but has to apply a more complicated schema due to Bruck [15]

[TABLE]

for suitable sequences $(\lambda_{n})$, $(\theta_{n})$ in $[0,1].$ In [18], it is shown that for Lipschitzian pseudocontractions (a class which still strictly generalizes the class of nonexpansive mappings and which contains the class of strict pseudocontractions due to [10]) the strong convergence of the Bruck iteration schema can be shown using the strong convergence of $(x_{t}),$ i.e. again by reduction to Reich’s theorem.

Furthermore, recently, in [4], a Halpern-type variant of the famous proximal point algorithm was shown to strongly converge by a similar reduction.

These and many other results point to the paramount significance of this result of Reich. In this paper, we give for the first time a quantitative account of it. From results of Neumann [56] on the Halpern iteration and the aforementioned connection with the convergence of $(x_{t})$ (which was treated quantitatively in [46]), it follows that even for the case of Hilbert spaces, in fact, already for $X:=\mathbb{R}$ and $C:=[0,1],$ there are simple computable mappings $T:C\to C$ for which $(x_{n}):=(x_{1-\frac{1}{n+1}})$ with the anchor point $x:=0$ does not have a computable rate of convergence. In this situation, the next best thing one can hope for is an effective so-called rate of metastability – in the sense of Terence Tao [65, 66], the name having been suggested to him by Jennifer Chayes – i.e. a function $\Theta:\mathbb{N}\times\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ such that

[TABLE]

where $[N,N+g(N)]:=\{N,N+1,N+2,\ldots,N+g(N)\},$ whose complexity reflects the computational content of the original convergence proof from which it is extractable by proof-theoretic methods (see [40]). Note that $(*)$ provides a quantitative form of

[TABLE]

which, noneffectively, is equivalent to the ordinary Cauchy property of $(x_{n}).$ In proof theory, the metastable version of the original Cauchy statement is known as the Kreisel no-counterexample interpretation [50, 51]. General so-called logical metatheorems due to [39, 27, 40, 23, 46, 31] guarantee the extractability of explicit effective bounds, in particular of rates of metastability, for large classes of proofs and provide algorithms for their actual extraction from a given proof based on modern variants and extensions of Gödel’s [30] famous functional (‘Dialectica’) interpretation. Moreover, these bounds only depend on $X$, $C$ and $T$ via ‘majorizing’ data (such as moduli of smoothness on $X$ or of uniform continuity of $T$ and norm bounds on the elements of $C$). These developments are all part of the research program of ‘proof mining’, that aims to apply these logical techniques to proofs in a broad range of areas of mainstream mathematics, such as nonlinear analysis, convex optimization, commutative algebra, ergodic theory or topological dynamics; the standard introduction to the field is [40], while more recent surveys are [42, 43].

For the Hilbert space case of the problem at hand, such $\Theta$’s of low primitive recursive complexity have already been extracted both for the Browder-Halpern theorem and for Wittmann’s theorem in [41], and an alternative way of using proof mining to derive these and related results was recently explored in [25].

However, a quantitative analysis of Reich’s generalization to Banach spaces had been a major challenge of the ‘proof mining’ paradigm for about ten years. The present paper, which for the first time succeeds in achieving such an analysis, is the technically most complex extraction of a metastability bound for a strong convergence theorem in analysis which has ever been carried out. The enormous complexity of the final bound reflects the profound combinatorial and computational content of Reich’s deep theorem.

More specifically, in the present paper, we extract for the first time a rate of metastability for the convergence of $(x_{t})$ for uniformly continuous pseudocontractions within the class of Banach spaces which are uniformly smooth and uniformly convex (which covers all $L^{p}$ spaces for $1<p<\infty$). Using quantitative results extracted already in [46], this also gives the first explicit rate of metastability for the extension (due to [62]) of Wittmann’s theorem to this class of spaces as well as, using quantitative results from [49], the first rate of metastability for Bruck’s iteration for this class. All previous results only considered the class of Hilbert spaces (or geodesic generalizations of Hilbert spaces such as CAT(0) spaces [45] or CAT($\kappa$) spaces for $\kappa\geq 0$ [52]). As predicted by general logical metatheorems from [40, 46], the rate of metastability (in the case where $t_{n}:=1-\frac{1}{n+1}$) only depends (in addition to $\varepsilon$ and $g$) on a norm bound $b$ on the elements in $C$, on moduli $\tau$, $\eta$ of uniform smoothness and convexity, respectively, of $X$ and on a modulus $\theta$ of uniform continuity of $T$.

Our extraction of $\Theta$ analyzes the proof of Reich’s theorem given in 1990 by Morales [55]. This proof uses that the continuous convex function

[TABLE]

where $(t_{n})$ is a sequence in $(0,1)$ which converges to $1,$ attains its infimum on the closed convex bounded set $C$ since $X$ is reflexive, being uniformly smooth. (Reich’s original proof [60] produced the operator $F$ as the limit of a subsequence, which was shown to be well-defined in [61]; later developments of the idea, even to this day, generally use a simplification of this by applying a Banach limit to the original sequence – see, e.g., [17, 16, 64]; to our knowledge, the above definition – lifted from the theory of asymptotic centers [22] – was first used by Morales in this context and afterwards picked up by few other authors.) The proof then continues by forming the set of all points on which $F$ attains its infimum, showing that this set is invariant under the action of (the resolvent of) $T$ and thus (the resolvent, and therefore) $T$ has a fixed point in this set. (The detour via the resolvent is not needed for nonexpansive mappings.) In the deductive framework to which the known proof-theoretic bound extraction methods apply, it is not clear how to define $F$ as an object given as we do not have a term which assigns to a bounded sequence of reals its $\limsup$ (in technical terms this is due to the fact the functional interpretation of having such a term has no solution by majorizable functionals; only if $X$ would be assumed as separable – which we have to avoid, however, for general reasons discussed in [40] as this prevents the extraction of uniform bounds – then using the continuity of $F$ it would be enough to define $F$ on a dense sequence and this could be done in our setting). So we aim to replace the use of $F$ as an object by

[TABLE]

where ‘$a=\limsup_{n\to\infty}\|x_{t_{n}}-z\|^{2}$’ is logically complex, namely it is a so-called $\Pi^{0}_{3}$ statement.

This makes it difficult to formalize the above arguments in a setting which only allows one to use $(**).$ That is why we add the additional assumption that $X$ is a uniformly convex Banach space which yields that $F$ is a uniformly convex function. This is usually used to prove that asymptotic centers are unique in this class of spaces, and we show that one can construct (by way of Proposition 2.4) a modulus of uniqueness for the infimum problem stating that – given $\varepsilon>0$ – there is a $\delta>0$ such that $\delta$-approximate infima points are $\varepsilon$-close to each other (for more details, see e.g. its use in Claims 2 and 3 of the proof in Section 3). It is then sufficient to consider only $\delta$-infima points instead of actual infima points. The resulting proof can then be shown to be formalizable with the use of arithmetical comprehension which already guarantees the extractability of a rate of metastability which is definable in the calculus $T+B_{0,1},$ where $T$ is the system of the Hilbert-Gödel [34, 30] primitive recursive functionals of finite type and $B_{0,1}$ is the schema of Spector’s [63] bar recursion (of lowest type). We then show that the use of real limsup’s can be replaced – using a process of arithmetization, see [36] and Remark 4.1 – by that of $\varepsilon$-limsup’s whose existence can be shown using just induction (more precisely, using $\Pi^{0}_{2}$-induction, to which it is equivalent and which – by Parsons [58] – has a solution in the fragment $T_{1}$ of $T$).

Since the existence of $\delta$-infima of $F$ also requires only induction, it follows from this that one gets a rate of metastability which is primitive recursive in the extended sense of $T.$ The analysis of the $\delta$-infima argument shows that $T_{2}$ suffices. When the details of the extraction are all carried out, it turns out that for the particular instances of that argument used, actually $T_{1}$ suffices, which, therefore, is the complexity of our final bound. The statement $(*)$ with this explicit bound provides a finitary version (in the sense of Tao) of the theorem that $(x_{t})$ converges to the sunny nonexpansive retraction $Qx$ of $x$ (and so, in particular, also of the existence of $Q$ itself) since the latter can be derived from $(*)$ by an elementary proof. In particular, it follows that only a single instance of $\Pi^{0}_{1}$-comprehension is needed (or, as seen from the viewpoint of constructive mathematics and in the presence of $\Pi^{0}_{1}$-AC0,0 choice for numbers, only the $\Sigma^{0}_{1}$ law of excluded middle) to derive the theorem. We believe that our analysis exhibits the explicit numerical content of the existence proof for $Q.$ Only future research will show whether the complexity class $T_{1}$ is the best possible or whether an ordinary primitive recursive rate $\Theta\in T_{0}$ can be achieved (or even whether a close examination of our bound might show that it can already be defined in $T_{0}$, see Remark 6.3).

The next section introduces the preliminary notions used to discuss and prove our result, namely on uniformly convex and uniformly smooth spaces, and on nonexpansive retractions and pseudocontractions. Highlights include the modulus of convexity for the squared norm of a uniformly convex space – which has as an immediate consequence the uniform convexity of the function $F$ discussed above – as well as the introduction of the resolvent $g_{T}$ of a continuous pseudocontraction $T$ that allows one to use nonexpansiveness arguments as needed. Section 3 details the way to an intermediate proof of the main result where the use of $F$ as an operator has been eliminated and only $\varepsilon$-infima of it are needed, which are made useful by means of the modulus of uniqueness. In Section 4 even this use of $F$ in the form of pointwise limsup’s is removed, as they are replaced with approximate limsup’s. Some care must be taken to ensure that approximate limsup’s may be shown to exist using just induction (Proposition 4.3) and that they are useful for our purposes (Lemma 4.5). Finally, in Section 5, the higher-order portions of the witness extraction are carried out, yielding a highly complex, though structured, realizer. In Section 6 this realizer is progressively majorized in order to obtain our goal, namely a rate of metastability. It is argued there both that this final bound $\Theta$ is expressible in $T_{1}$ and that the metastability statement is a true finitization (again in the sense of T. Tao) of the full form of the original strong convergence statement. Playing the role of an epilogue, Section 7 presents two completions by means of our result of proof mining analyses which had only been carried partially (in the sense that a rate of metastability was produced assuming such a rate for $(x_{t_{n}})$ be given which so far was known only in the Hilbert space case), namely the strong convergence of the iterations of B. Halpern and R. E. Bruck.

2 Preliminaries

2.1 Classes of Banach spaces

2.1.1 Uniformly convex spaces

Definition 2.1** (cf. [19, 20]).**

Let $X$ be a Banach space. We call the function $\delta_{X}:(0,2]\to\mathbb{R}$, defined, for all $\varepsilon\in(0,2]$, by:

[TABLE]

“the” modulus of convexity of $X$.

The following result shows that this modulus can be obtained in a less strict way.

Proposition 2.2** ([53, p. 60]).**

Let $X$ be a Banach space. Then, for all $\varepsilon\in(0,2]$,

[TABLE]

Corollary 2.3**.**

Let $X$ be a Banach space. TFAE:

1. (a)

for all $\varepsilon\in(0,2]$, $\delta_{X}(\varepsilon)>0$. 2. (b)

there is an $\eta:(0,2]\to(0,1]$ (called “a” modulus of convexity) such that for all $\varepsilon\in(0,2]$ and all $x,y\in X$ with $\|x\|\leq 1$, $\|y\|\leq 1$ and $\|x-y\|\geq\varepsilon$ one has that

[TABLE]

(One can, obviously, for the implication “(a) $\Rightarrow$ (b)”, put, for all $\varepsilon$, $\eta(\varepsilon):=\delta_{X}(\varepsilon)$.) In this case, $X$ is called uniformly convex.

The following is an application of a recent proof mining result of Bačák and the first author, specifically [5, Proposition 3.2], itself a quantitative version of a theorem of Zălinescu [70, Theorem 4.1]. We remark that a similar kind of result (i.e. with a different modulus) may be obtained by adapting an argument from [69, Section 2] to work with $\eta$ instead of $\delta_{X}$. The non-quantitative version may also be found in the statement of [68, Theorem 2], but the proof given there is highly non-constructive.

Proposition 2.4**.**

Let $X$ be a uniformly convex Banach space having $\eta$ as a modulus and let $b\geq\frac{1}{2}$. Put, for all $\varepsilon\in(0,2]$,

[TABLE]

Then, for all $\varepsilon\in(0,2]$:

1. (a)

$\psi_{b,\eta}(\varepsilon)>0$. 2. (b)

for all $x,y\in X$ with $\|x\|\leq b$, $\|y\|\leq b$, $\|x-y\|\geq\varepsilon$, we have that

[TABLE]

Proof.

We may assume that $x,y\not=0.$ We seek to apply [5, Proposition 3.2]. We need, then, only to pass from $x$ to $\frac{x}{\|x\|}$ and from $y$ to $\frac{y}{\|y\|}$ and then to put $r:=b$, $\alpha:=\|x\|$, $\beta:=\|y\|$ and $\Phi$ to be the squaring function. To obtain the conclusion, one has to verify that, for an arbitrary $r>0$, the squaring function has on the interval $[0,r]$ the function $\varepsilon\mapsto\frac{\varepsilon^{2}}{4}$ as a modulus of uniform convexity, $\varepsilon\mapsto\frac{\varepsilon}{2r}$ as a modulus of uniform continuity and $\varepsilon\mapsto\varepsilon^{2}$ as a modulus of uniform increasingness. ∎

2.1.2 Smooth and uniformly smooth spaces

Definition 2.5**.**

Let $X$ be a Banach space. We define the normalized duality mapping of $X$ to be the map $J:X\to 2^{X^{*}}$, defined, for all $x\in X$, by

[TABLE]

A Banach space $X$ is called smooth if for any $x\in X$ with $\|x\|=1$, we have that for any $y\in X$ with $\|y\|=1$, the limit

[TABLE]

exists. This condition has been proven to be equivalent to the fact that the normalized duality mapping of the space, $J:X\to 2^{X^{*}}$, is single-valued – and we shall denote its unique section by $j:X\to X^{*}$. Therefore, for all $x\in E$, $j(x)(x)=\|x\|^{2}$ and $\|j(x)\|=\|x\|$. Hilbert spaces are smooth, and clearly $j(x)(y)$ is then simply $\langle y,x\rangle$, for any $x,y$ in the space. Because of this, we may consider the $j$ to be a generalized variant of the inner product, sharing some of its nice properties. We shall generally denote, for all spaces $X$, all $x^{*}\in X^{*}$ and $y\in X$, $x^{*}(y)$ by $\langle y,x^{*}\rangle$. In addition, the homogeneity of $j$ – i.e. that for all $x\in X$ and $t\in\mathbb{R}$, $j(tx)=tj(x)$ – follows immediately from the definition of the duality mapping.

Remark 2.6**.**

These notions of smoothness were introduced in [20], under the name of flattening.

Lemma 2.7** (cf. [59, Lemma 1]).**

Let $X$ be a smooth space and $x,y\in X$. Then

[TABLE]

Proof.

We have that

[TABLE]

from which the conclusion follows. ∎

Definition 2.8** ([53, Definition 1.e.1.(ii)]).**

Let $X$ be a Banach space. We call the function $\rho_{X}:(0,\infty)\to\mathbb{R}$, defined, for all $t>0$, by

[TABLE]

“the” modulus of smoothness of $X$. We remark that for all $t$, $0\leq\rho_{X}(t)\leq t$.

The following characterization is immediate.

Proposition 2.9**.**

Let $X$ be a Banach space. TFAE:

1. (a)

$\lim\limits_{t\to 0}\frac{\rho_{X}(t)}{t}=0$. 2. (b)

there is a $\tau:(0,\infty)\to(0,\infty)$ (called “a” modulus of smoothness) such that for all $\varepsilon>0$ and all $x,y\in X$ with $\|x\|=1$, $\|y\|\leq\tau(\varepsilon)$ one has that

[TABLE]

In this case, $X$ is called uniformly smooth.

Remark 2.10**.**

A uniformly smooth space is smooth, and this condition is equivalent to the limit in (1) being attained uniformly in the pair of variables $(x,y)$.

Remark 2.11**.**

Unlike in the case of convexity, “the” modulus of smoothness is not “a” modulus of smoothness.

Proposition 2.12** (cf. [46, Proposition 2.5]).**

Let $X$ be a uniformly smooth Banach space with modulus $\tau$. Put, for all $b>0$ and $\varepsilon>0$,

[TABLE]

Then for all $b>0$, $\varepsilon>0$ and all $x,y\in X$ with $\|x\|\leq b$ and $\|y\|\leq b$, if $\|x-y\|\leq\omega_{\tau}(b,\varepsilon)$ then $\|j(x)-j(y)\|\leq\varepsilon$.

In the PhD thesis of Bénilan [7, p. 0.5, Proposition 0.3], it is shown that the norm-to-norm uniform continuity on bounded subsets of an arbitrary duality selection mapping is in fact equivalent to uniform smoothness. A more recent proof which uses ideas due to Giles [28] may be found in [48, Appendix A].

2.2 Classes of mappings

In this section, we fix a smooth Banach space $X$ and $C\subseteq X$ a closed, convex, nonempty subset.

2.2.1 Nonexpansive mappings and sunny nonexpansive retractions

Definition 2.13**.**

A map $Q:C\to X$ is called nonexpansive if for all $x,y\in C$, $\|Qx-Qy\|\leq\|x-y\|$.

Let $E\subseteq C$ be nonempty.

Definition 2.14**.**

A map $Q:C\to E$ is called a retraction if for all $x\in E$, $Qx=x$.

Definition 2.15**.**

A retraction $Q:C\to E$ is called sunny if for all $x\in C$ and $t\geq 0$,

[TABLE]

Proposition 2.16** ([29, Lemma 1.13.1]).**

Let $Q:C\to E$ be a retraction. Then $Q$ is sunny and nonexpansive if and only if for all $x\in C$ and $y\in E$,

[TABLE]

Proposition 2.17**.**

There is at most one sunny nonexpansive retraction from $C$ to $E$.

Proof.

Let $Q_{1}$ and $Q_{2}$ be two such retractions. Let $x\in C$. It follows that

[TABLE]

and

[TABLE]

Using the homogeneity of $j$ and then summing up, it follows that $\|Q_{2}x-Q_{1}x\|^{2}\leq 0$ and therefore $Q_{1}x=Q_{2}x$. ∎

2.2.2 Pseudocontractions

Definition 2.18**.**

Let $T:C\to C$. We call a function $\theta:(0,\infty)\to(0,\infty)$ a modulus of continuity for $T$ if for all $\varepsilon>0$ and $x,y\in C$ with $\|x-y\|\leq\theta(\varepsilon)$, we have that $\|Tx-Ty\|\leq\varepsilon$.

Remark 2.19**.**

A map $T:C\to C$ has a modulus of continuity iff it is uniformly continuous.

Definition 2.20** ([8, Definition 1]).**

A map $T:C\to C$ is called a pseudocontraction if for all $x,y\in C$ and $t>0$, we have that

[TABLE]

Proposition 2.21**.**

Any nonexpansive map is a pseudocontraction.

Proof.

Let $T:C\to C$ be nonexpansive. Let $x,y\in C$ and $t>0$. We have that

[TABLE]

so

[TABLE]

Multiplying by $t$, we obtain our conclusion. ∎

We have the following equivalence.

Proposition 2.22** ([8, Proposition 1]).**

Let $T:C\to C$. Then $T$ is a pseudocontraction if and only if for all $x,y\in C$,

[TABLE]

Definition 2.23** (cf. [32, (2.9)]).**

Let $k\in(0,1)$. A map $T:C\to C$ is called a $k$-strong pseudocontraction* if for all $x,y\in C$,*

[TABLE]

Proposition 2.24**.**

Let $T:C\to C$ be a continuous pseudocontraction, $k\in(0,1)$ and $u\in C$. Define the map $U:C\to C$, by putting, for all $x\in C$, $Ux:=kTx+(1-k)u$. Then $U$ is a continuous $k$-strong pseudocontraction.

Proof.

We have that for all $x$, $Tx=\frac{1}{k}Ux-\frac{1-k}{k}u$, so for all $x,y$,

[TABLE]

from which our conclusion follows. ∎

Proposition 2.25**.**

Let $k\in(0,1)$ and $T:C\to C$ be a continuous $k$-strong pseudocontraction. Then $T$ has a unique fixed point.

Proof.

If $x$ and $y$ are fixed points of $T$, $\|x-y\|^{2}\leq k\|x-y\|^{2}$, so $x=y$. The existence of a fixed point follows from [54, Proposition 3] and the convexity of $C$. ∎

Definition 2.26**.**

If $T:C\to C$ is a pseudocontraction, we define the map $f_{T}:C\to X$, for all $x\in C$, by $f_{T}(x):=2x-Tx$.

Proposition 2.27**.**

Let $T:C\to C$ be a continuous pseudocontraction. Then for all $y\in C$ there is a unique $x\in C$ such that $f_{T}(x)=y$.

Proof.

Let $y\in C$. Define the map $U:C\to C$, for all $z\in C$, by $Uz:=\frac{Tz+y}{2}$. Then, by Proposition 2.24, $U$ is a continuous $\frac{1}{2}$-strong pseudocontraction. Since we have that for all $x\in C$, $f_{T}(x)=y$ iff $Ux=x$, the conclusion follows by applying Proposition 2.25. ∎

Definition 2.28**.**

If $T:C\to C$ is a continuous pseudocontraction, we define the map $g_{T}:C\to C$ by putting, for all $y\in C$, $g_{T}(y)$ to be the unique $x\in C$ such that $f_{T}(x)=y$.

Notation 2.29**.**

For any function $\theta:(0,\infty)\to(0,\infty)$ and for any $\varepsilon>0$, put $\tilde{\theta}(\varepsilon):=\min\left(\frac{\varepsilon}{4},\theta\left(\frac{\varepsilon}{2}\right)\right)$.

Proposition 2.30**.**

Let $T:C\to C$ be a continuous pseudocontraction. Then:

1. (i)

for all $y\in C$, $f_{T}(g_{T}(y))=y$; 2. (ii)

$g_{T}$* is nonexpansive;* 3. (iii)

for all $x\in C$, $\|x-g_{T}x\|\leq\|x-Tx\|$; 4. (iv)

$g_{T}$* and $T$ have the same fixed points;* 5. (v)

if $T$ is uniformly continuous with modulus $\theta$, then for all $x\in C$ and all $\varepsilon>0$, with $\|x-g_{T}x\|\leq\tilde{\theta}(\varepsilon)$, we have that $\|x-Tx\|\leq\varepsilon$.

Proof.

1. (i)

Immediately, from the definition of $g_{T}$. 2. (ii)

Let $x,y\in C$ and apply (2) for $x\mapsto g_{T}(x)$, $y\mapsto g_{T}(y)$ and $t\mapsto 1$ to obtain – using (i) – that

[TABLE] 3. (iii)

Let $x\in C$ and apply (2) for $x\mapsto x$, $y\mapsto g_{T}(x)$ and $t\mapsto 1$ to obtain – again, using (i) – that

[TABLE] 4. (iv)

One direction follows from (iii). For the other, let $p\in C$ be such that $g_{T}p=p$. Then $p=f_{T}g_{T}p=f_{T}p=2p-Tp$, so $p$ is a fixed point of $T$. 5. (v)

What follows is a quantitative version of the proof of (iv). If $\|x-g_{T}x\|\leq\theta\left(\frac{\varepsilon}{2}\right)$, then $\|Tx-Tg_{T}x\|\leq\frac{\varepsilon}{2}$. Therefore, we have that

[TABLE]

∎

Definition 2.31**.**

If $T:C\to C$ is a continuous pseudocontraction, we define the map $h_{T}:C\to C$ by putting $h_{T}:=T$ if $T$ is nonexpansive and $h_{T}:=g_{T}$ otherwise.

The map $h_{T}$ is defined purely for our convenience, as we could have used $g_{T}$ regardless of the status of $T$, but we want to emphasize that if $T$ is nonexpansive, then the use of $T$ is sufficient.

Corollary 2.32**.**

Let $T:C\to C$ be a continuous pseudocontraction. Then:

1. (i)

$h_{T}$* is nonexpansive;* 2. (ii)

for all $x\in C$, $\|x-h_{T}x\|\leq\|x-Tx\|$; 3. (iii)

if $T$ is uniformly continuous with modulus $\theta$, then for all $x\in C$ and all $\varepsilon>0$, with $\|x-h_{T}x\|\leq\tilde{\theta}(\varepsilon)$, we have that $\|x-Tx\|\leq\varepsilon$; 4. (iv)

$h_{T}$* and $T$ have the same fixed points.*

3 The proof using limsup’s but only $\varepsilon$-infima

The main focus of this paper is the following theorem (here and below $\mathbb{N}^{*}:=\{1,2,3,\ldots\}$).

Theorem 3.1** (cf. [60]).**

Let $X$ be a Banach space which is uniformly convex with modulus $\eta$ and uniformly smooth with modulus $\tau$. Let $C\subseteq X$ a closed, convex, nonempty subset. Let $b\in\mathbb{N}^{*}$ be such that for all $y\in C$, $\|y\|\leq b$ and the diameter of $C$ is bounded by $b$. Let $T:C\to C$ be a pseudocontraction that is uniformly continuous with modulus $\theta$ and $x\in C$. For all $t\in(0,1)$ put $x_{t}$ to be the unique point in $C$ such that $x_{t}=tTx_{t}+(1-t)x$ (which exists by Propositions 2.24 and 2.25). Then for all $(t_{n})\subseteq(0,1)$ such that $\lim\limits_{n\to\infty}t_{n}=1$ we have that $(x_{t_{n}})$ is Cauchy.

This theorem was first proven by Reich [60] without the assumption of uniform convexity. The starting point of our investigations is the proof given by Morales [55], which we shall now illustrate, after giving a preliminary lemma.

Lemma 3.2**.**

Let $(a_{n})$, $(b_{n})$ be two bounded sequences of reals. Then

[TABLE]

Proof.

We have that:

[TABLE]

∎

Proof of the theorem. We first show that for all $(t_{n})\subseteq(0,1)$ such that $\lim\limits_{n\to\infty}t_{n}=1$, there exist a $p\in Fix(T)$ and $(n_{k})$, strictly increasing, such that $(x_{t_{n_{k}}})\to p$. Put, for all $n$, $x_{n}:=x_{t_{n}}$. Then, for all $n$,

[TABLE]

so $\lim_{n\to\infty}\|x_{n}-Tx_{n}\|=0$ and therefore (by Corollary 2.32.(ii)) $\lim_{n\to\infty}\|x_{n}-h_{T}x_{n}\|=0$. Define now $F:C\to\mathbb{R}^{+}$, for all $z\in C$, by $F(z):=\limsup_{n\to\infty}\|x_{n}-z\|$. Let $K$ be the set of minimizers of $F$.

Claim. There is a $p\in K\cap Fix(T)$.

Proof of claim: Since $F$ is convex and continuous, $C$ is closed convex bounded nonempty, and $X$ is uniformly smooth, hence reflexive, we have that $K\neq\emptyset$. Let $y\in K$ and $z\in C$. Then:

[TABLE]

so $h_{T}y\in K$. Since $K$ is a closed convex bounded nonempty subset of a uniformly smooth space, and it is invariant under the action of the nonexpansive mapping $h_{T}$, we have that there is a $p\in K\cap Fix(h_{T})$, so by Corollary 2.32.(iv), $p\in K\cap Fix(T)$. $\blacksquare$

We only sketch the remainder of the proof, since the details that will actually be used shall be given later. Let $\varepsilon>0$ and put $r:=x-p$. Using the continuity of $j$, let $\mu\in(0,1)$ be small enough such that for any $n$, $\langle r,j(x_{n}-p)\rangle\leq\varepsilon+\langle r,j(x_{n}-p-\mu r)\rangle$. (Note that $p+\mu r=(1-\mu)p+\mu x\in C$.) By Lemma 2.7, we have that $\|x_{n}-p-\mu r\|^{2}\leq\|x_{n}-p\|^{2}+2\langle-\mu r,j(x_{n}-p-\mu r)\rangle$. Summing up, we get that

[TABLE]

so by Lemma 3.2, $\liminf_{n\to\infty}\langle r,j(x_{n}-p)\rangle\leq\varepsilon$. Since $\varepsilon$ was chosen arbitrarily and $r=x-p$, we easily get that there is an $(n_{k})$, strictly increasing, such that $\limsup_{k\to\infty}\langle x-p,j(x_{n_{k}}-p)\rangle\leq 0$. We use that $T$ is a pseudocontraction to derive that for any $n$,

[TABLE]

so that $\langle x_{n}-x,j(x_{n}-p)\rangle\leq 0$, which we sum up with the previous inequality to get that $(x_{t_{n_{k}}})\to p$.

To obtain the convergence of $(x_{t_{n}})$ for any (suitable, from now on) sequence $(t_{n})$, it is clear that we need only to show that there is a $p$ such that for any $(t_{n})$ there is an $(n_{k})$ such that $(x_{t_{n_{k}}})\to p$. Fix a canonical sequence, say $s_{m}:=1-\frac{1}{m+1}$, for any $m$. By the previous argument, we have that there is an $(m_{l})$ and a $p\in Fix(T)$ such that $(x_{s_{m_{l}}})\to p$. Now consider a sequence $(t_{n})$. Again, by the above, there is an $(n_{k})$ and a $q\in Fix(T)$ such that $(x_{t_{n_{k}}})\to q$. What remains to be shown is that $p=q$. Let $\varepsilon>0$. Put, for all $k$, $x_{k}=x_{t_{n_{k}}}$. Let $k_{0}$ be big enough such that $\|x_{k_{0}}-q\|\leq\varepsilon^{2}/4b$ and that (again, using the continuity of $j$) $\langle x_{k_{0}}-x,j(q-p)-j(x_{k_{0}}-p)\rangle\leq\varepsilon^{2}/4$. Using arguments like before, we get that $\langle q-x,j(q-p)\rangle\leq\varepsilon^{2}/2$ and similarly $\langle p-x,j(p-q)\rangle\leq\varepsilon^{2}/2$, so $\|p-q\|\leq\varepsilon$. $\Box$

It is now clear that the least elementary principles are used in the Claim, where appeal is made to results of Banach space theory as established in a set-theoretic framework. From the point of a quantitative analysis the most difficult argument is the proof of $K\not=\emptyset$ using the reflexivity of $X.$ This can be avoided as follows. In the light of the conclusion of the theorem, it is immediate that the function $F$ has a unique minimizer, namely the limit of $(x_{t_{n}})$, so a viable idea would be to get to this uniqueness in an a priori way. This is where the additional hypothesis of uniform convexity helps us, through Proposition 2.4, which gives a modulus of uniform convexity for the squared norm – and thus also for $F$ – that acts as a modulus of minimizer uniqueness for $F$ which allows one to show the existence of an actual minimizer as the limit of approximate minimizers, with this modulus providing a rate of convergence. Let us see how these concepts come into play.

Second proof of the Claim. We divide this proof into a series of claims.

Claim 1. For all $\varepsilon>0$ there is a $y\in C$ such that for all $z\in C$:

• •

$\limsup\limits_{n\to\infty}\|x_{n}-y\|^{2}\leq\limsup\limits_{n\to\infty}\|x_{n}-z\|^{2}+\varepsilon$;

• •

$\limsup\limits_{n\to\infty}\|x_{n}-h_{T}y\|^{2}\leq\limsup\limits_{n\to\infty}\|x_{n}-z\|^{2}+\varepsilon$.

Proof of claim: As before, we have that $\lim_{n\to\infty}\|x_{n}-h_{T}x_{n}\|=0$. Suppose that for all $y\in C$ there is a $z\in C$ such that

[TABLE]

Let $\hat{y}\in C$ and put $K:=\left\lceil\frac{b}{\varepsilon}\right\rceil$. Put, then, $f_{1}:=\hat{y}$ and recursively for all $i\in\{1,\ldots,K\}$ put $f_{i+1}$ such that

[TABLE]

Therefore,

[TABLE]

which is a contradiction. Thus, there is a $y\in C$ such that for all $z\in C$

[TABLE]

Now, we have, again as before, that

[TABLE]

so, for all $z\in C$,

[TABLE]

$\blacksquare$

Claim 2. For all $\varepsilon>0$ there is a $u\in C$ such that:

• •

for all $z\in C$, $\limsup\limits_{n\to\infty}\|x_{n}-u\|^{2}\leq\limsup\limits_{n\to\infty}\|x_{n}-z\|^{2}+\varepsilon$;

• •

$\|u-Tu\|\leq\varepsilon$.

Proof of claim: Take $\eta_{1}:=\min\left(\varepsilon,\frac{1}{2}\psi_{b,\eta}(\tilde{\theta}(\varepsilon))\right)>0$. Apply Claim 1 for $(t_{n})$ and $\eta_{1}$ and put $u$ to be the resulting $y$. We have only to show that $\|u-h_{T}u\|\leq\tilde{\theta}(\varepsilon)$, since from that, using Corollary 2.32.(iii), it follows that $\|u-Tu\|\leq\varepsilon$. Suppose not. Then, for all $n$,

[TABLE]

so, for all $n$, by Proposition 2.4,

[TABLE]

Then, applying the defining property of $u$, we get that

[TABLE]

which is a contradiction, since $0<\eta_{1}\leq\frac{1}{2}\psi_{b,\eta}(\tilde{\theta}(\varepsilon))$. $\blacksquare$

Again, we only sketch the remainder of this proof. For any $m\in\mathbb{N}^{*}$, we fix a $u_{m}$ such that for all $z\in C$, $\limsup_{n\to\infty}\|x_{n}-u_{m}\|^{2}\leq\limsup_{n\to\infty}\|x_{n}-z\|^{2}+1/m$ and $\|u_{m}-Tu_{m}\|\leq 1/m$. We show that $(u_{m})$ is Cauchy. Let $\varepsilon>0$ and let $m$, $p\geq\lceil 2/\psi_{b,\eta}(\varepsilon)\rceil$. Assume that $\|u_{m}-u_{p}\|>\varepsilon$. Then, for all $n$, using Proposition 2.4 as before,

[TABLE]

which is a contradiction. It is then immediate that the limit of $(u_{m})$ satisfies our requirements. $\Box$

The next principles we can now remove from the proof are the ones that allowed us, for example, to pass to the limit in the argument above. What we do is to show that the approximate solutions obtained in Claim 2 are enough for the whole line of argument to go through, by essentially removing any ideal point that would appear in the course of the proof by an approximate one. This is made possible again by the use of Proposition 2.4, asserting that two $\delta$-infima of $F$, for sufficiently small $\delta$, must be $\varepsilon$-close. Also, it is now clear that the resulting proof does no longer use the existence of $F$ as a function but only the existence of the individual limsup’s in the form

[TABLE]

As a result of this, the proof may be formalized in a deductive system to which the logical bound extraction theorems, mentioned in the Introduction, apply – which is not clear if $F$ would be needed as an object (see also Remark 3.3 below).

Proof of the theorem using only the aforementioned principles. We presuppose the truth of Claim 2 in the previous proof, i.e. that for all $(t_{n})\subseteq(0,1)$ such that $\lim\limits_{n\to\infty}t_{n}=1$ and for all $\varepsilon>0$ there is a $u\in C$ such that:

• •

for all $z\in C$, $\limsup\limits_{n\to\infty}\|x_{t_{n}}-u\|^{2}\leq\limsup\limits_{n\to\infty}\|x_{t_{n}}-z\|^{2}+\varepsilon$;

• •

$\|u-Tu\|\leq\varepsilon$.

Thus, we shall start the numbering of claims at 3.

Claim 3. For all $(t_{n})\subseteq(0,1)$ such that $\lim\limits_{n\to\infty}t_{n}=1$ and for all $\varepsilon>0$ there is a $v\in C$ such that:

• •

for all $z\in C$, $\limsup\limits_{n\to\infty}\|x_{t_{n}}-v\|^{2}\leq\limsup\limits_{n\to\infty}\|x_{t_{n}}-z\|^{2}+\varepsilon$;

• •

for all $t\in(0,1)$, $\langle x_{t}-x,j(x_{t}-v)\rangle\leq\varepsilon$.

Proof of claim: Take $\eta_{2}:=\min\left(\varepsilon,\frac{1}{2}\psi_{b,\eta}\left(\omega_{\tau}\left(b,\frac{\varepsilon}{2b}\right)\right)\right).$

Apply Claim 2 for $(t_{n})$ and $\eta_{2}$ and put $v$ to be the resulting $u$.

We have to show that for all $t\in(0,1)$, $\langle x_{t}-x,j(x_{t}-v)\rangle\leq\varepsilon$. Let $t\in(0,1)$ and put $\delta:=\min\left(\eta_{2},\frac{\varepsilon(1-t)}{2b}\right)$. Apply Claim 2 for $(t_{n})$ and $\delta$ and put $v^{\prime}$ to be the resulting $u$, so in particular $\|v^{\prime}-Tv^{\prime}\|\leq\delta$. We then obtain that

[TABLE]

from which we get that

[TABLE]

Suppose that $\|v-v^{\prime}\|\geq\omega_{\tau}(b,\frac{\varepsilon}{2b})$, so, for all $n$,

[TABLE]

Then

[TABLE]

which is a contradiction. So $\|v-v^{\prime}\|\leq\omega_{\tau}(b,\frac{\varepsilon}{2b})$, i.e. $\|(x_{t}-v)-(x_{t}-v^{\prime})\|\leq\omega_{\tau}(b,\frac{\varepsilon}{2b})$. From that we obtain

[TABLE]

and

[TABLE]

From (3) and (4) we derive our conclusion. $\blacksquare$

Claim 4. For all $(t_{n})\subseteq(0,1)$ such that $\lim\limits_{n\to\infty}t_{n}=1$ and for all $\varepsilon>0$ there is a $w\in C$ such that:

• •

for all $t\in(0,1)$, $\langle x_{t}-x,j(x_{t}-w)\rangle\leq\varepsilon$;

• •

there exists $(n_{k})$, strictly increasing, such that $\limsup\limits_{k\to\infty}\|x_{t_{n_{k}}}-w\|^{2}\leq\varepsilon$.

Proof of claim: Put $\mu:=\min\left(\frac{\omega_{\tau}\left(b,\frac{\varepsilon}{3b}\right)}{b},\frac{1}{4}\right)$ and $\eta_{3}:=\min\left(\frac{\varepsilon}{3},2\mu\cdot\frac{\varepsilon}{3}\right).$

Apply Claim 3 for $(t_{n})$ and $\eta_{3}$ and put $w$ to be the resulting $v$. Denote, for all $n$, $x_{n}:=x_{t_{n}}$. We have that, for all $n$,

[TABLE]

Put $q:=x-w$. Since $\mu\in(0,1)$, $w+\mu q=(1-\mu)w+\mu x\in C$. By Lemma 2.7, we have that

[TABLE]

Since

[TABLE]

we have that

[TABLE]

and so that

[TABLE]

From (6) and (7) we get that

[TABLE]

Applying Lemma 3.2, we obtain that

[TABLE]

and therefore that there exists $(n_{k})$, strictly increasing, such that

[TABLE]

so in particular, noting also that $q=x-w$,

[TABLE]

Using (5), we derive $\limsup\limits_{k\to\infty}\|x_{n_{k}}-w\|^{2}\leq\varepsilon$, i.e. our conclusion. $\blacksquare$

Claim 5. For all $\varepsilon>0$ there is a $g\in C$ such that for all $(t_{n})\subseteq(0,1)$ with $\lim\limits_{n\to\infty}t_{n}=1$, there exists $(n_{k})$, strictly increasing, such that

[TABLE]

Proof of claim: Put

[TABLE]

and, for all $m$, $s_{m}:=1-\frac{1}{m+1}$.

Apply Claim 4 for $(s_{m})$ and $\eta_{4}$ and put $g$ to be the resulting $w$. In particular, there is $(m_{l})$, strictly increasing, such that $\limsup\limits_{l\to\infty}\|x_{s_{m_{l}}}-g\|^{2}\leq\eta_{4}$.

Let now $(t_{n})$ be chosen arbitrarily such that $\lim\limits_{n\to\infty}t_{n}=1$. Apply Claim 4 for $(t_{n})$ and $\eta_{4}$ and put $g^{\prime}$ to be the resulting $w$. In particular, there is $(n_{k})$, strictly increasing, such that $\limsup\limits_{k\to\infty}\|x_{t_{n_{k}}}-g^{\prime}\|^{2}\leq\eta_{4}$.

We have that for all $k$,

[TABLE]

Take a $k_{0}$ sufficiently large such that

[TABLE]

We have that

[TABLE]

and that

[TABLE]

so

[TABLE]

Therefore

[TABLE]

Similarly, we obtain that

[TABLE]

Summing up, we get that $\langle g-g^{\prime},j(g-g^{\prime})\rangle\leq\frac{\varepsilon^{2}}{4}$, so $\|g-g^{\prime}\|\leq\frac{\varepsilon}{2}$. Since $\limsup_{k\to\infty}\|x_{t_{n_{k}}}-g^{\prime}\|^{2}\leq\frac{\varepsilon^{2}}{24}\leq\frac{\varepsilon^{2}}{4}$, we have

[TABLE]

i.e. our conclusion. $\blacksquare$

Claim 6. For all $\varepsilon>0$ there is an $h\in C$ such that for all $(t_{n})\subseteq(0,1)$ with $\lim\limits_{n\to\infty}t_{n}=1$, we have that

[TABLE]

Proof of claim: Apply Claim 5 for $\varepsilon$ and put $h$ to be the resulting $g$. Let now $(t_{n})$ be chosen arbitrarily such that $\lim\limits_{n\to\infty}t_{n}=1$.

Suppose that $\limsup\limits_{n\to\infty}\|x_{t_{n}}-h\|>\varepsilon$. Then there is an $\eta>0$ such that for all $N$ there is an $n\geq N+1$ such that $\|x_{t_{n}}-h\|>\varepsilon+\eta$, so there is an $(n_{k})$, strictly increasing, such that for all $k$, $\|x_{t_{n_{k}}}-h\|>\varepsilon+\eta$. By the defining property of $h$, we get that there is a $(k_{l})$, strictly increasing, such that

[TABLE]

so there is an $L$ such that for all $l\geq L$,

[TABLE]

which contradicts the defining property of $(n_{k})$. $\blacksquare$

Claim 7. For all $(t_{n})\subseteq(0,1)$ with $\lim\limits_{n\to\infty}t_{n}=1$, we have that the sequence $(x_{t_{n}})$ is Cauchy.

Proof of claim: Denote, for all $n$, $x_{n}:=x_{t_{n}}$. We want to show that for all $\varepsilon>0$ there is an $N$ such that for all $m,n\geq N$, $\|x_{n}-x_{m}\|\leq\varepsilon$. Let $\varepsilon>0$. By applying Claim 6 for $\frac{\varepsilon}{4}$, we obtain an $h\in C$ having the property that there is an $N$ such that for all $n\geq N$,

[TABLE]

Take $n,m\geq N$. Then

[TABLE]

i.e. our conclusion. $\blacksquare$

This last claim is exactly our desired statement. $\Box$

Remark 3.3** (for logicians; we use the terminology from [40]).**

An inspection of the proof of the Cauchy property and hence of the metastability of $(x_{t_{n}})$ in this section shows that it can be carried out in the formal system WE-PA${}^{\omega}[X,\|\cdot\|,\eta,J_{X},\omega_{X},C]+$CAar where WE-PA${}^{\omega}[X,\|\cdot\|,\eta,J_{X},\omega_{X},C]$ is defined as in [40, (17.68)] and then augmented by the normalized duality mapping $J_{X}$ and the modulus of uniform smoothness $\omega_{X}$ as in [46]. CAar denotes the schema of arithmetic comprehension which is needed to show the existence of $\limsup\limits_{n\to\infty}\|x_{t_{n}}-y\|^{2}.$ From the logical metatheorems in [40, 46] and Theorems 11.11 and 11.13 in [40] it follows that one can extract a rate of metastability for the Cauchy property of $(x_{t_{n}})$ which is definable in Gödel’s calculus $T$ of primitive recursive functionals of finite type augmented by Spector’s bar recursion $B_{0,1}$ of lowest type. In the next section we will show that even the use of $B_{0,1}$ can be avoided.

4 The proof using approximate limsup’s

In this section we, in particular, show that the use of limsup’s can be replaced by that of $\varepsilon$-limsup’s whose existence can be established by induction (for logicians: $\Pi^{0}_{2}$-induction). As a result of this, the proof can even be formalized without arithmetic comprehension and so the extractability of a primitive recursive (in the sense of Gödel’s $T$) rate of metastability is guaranteed (see Remark 3.3). We also exhibit the finitary content of the actual use of approximate limsup’s made in the proof.

Remark 4.1**.**

The process of eliminating $\limsup$’s by an arithmetical principle in this section is in line with [36, Proposition 5.9] where such an arithmetization of the use of limsup’s to $T_{1}$ is shown to be possible in a certain restrictive deductive context and by [38, Theorem 6.1] it is optimal. In [40, Section 17.9], the approach is shown to work also within the framework of abstract spaces. In our context, however, we cannot directly apply these results as the limsup’s are used in the presence of e.g. inductions going beyond quantifier-free induction. However, as usual in the context of ordinary proofs, the arithmetization can nevertheless be carried out without problems and we suspect that this could be explained in terms of logical metatheorems by treating the inductions used as implicative assumptions and using that the method behind these arithmetizations works for arbitrary (arithmetical) formulas as long as certain monotonicity conditions are fulfilled (see [37]). Nevertheless, we leave this for future research to clarify.

4.1 The arithmetized version of limits superior

Definition 4.2**.**

Let $(a_{n})$ be a sequence of reals and $\varepsilon>0$. A number $a\in\mathbb{R}$ is called an $\varepsilon$-approximate limsup* (or simply an $\varepsilon$-limsup) for $(a_{n})$ if:*

• •

for all $n$ there is an $m$ such that $a_{n+m}\geq a-\varepsilon$;

• •

there is a $j$ such that for all $l$, $a_{j+l}\leq a+\varepsilon$.

What makes approximate limsup’s suitable for proof mining is that they admit an existence proof which uses only $\Pi^{0}_{2}$-induction.

Proposition 4.3** ($\Pi^{0}_{2}$-IA).**

For all $b,k\in\mathbb{N}$ and for all sequences of reals $(a_{n})$ contained in the interval $[0,b]$, there is a $p\in\mathbb{N}$ with $0\leq p\leq b\cdot(k+1)$ such that $\frac{p}{k+1}$ is a $\frac{1}{k+1}$-limsup of $(a_{n})$.

Proof.

Let $b$, $k$ and $(a_{n})$ be as in the statement.

Claim. There is a $p\in\mathbb{N}$ with $0\leq p\leq b\cdot(k+1)$ such that it is not the case that for all $j$ there is an $l$ with $a_{j+l}>\frac{p-1}{k+1}$ implies that for all $j$ there is an $l$ with $a_{j+l}>\frac{p}{k+1}$.

Proof of claim: Assume towards a contradiction that the opposite holds, i.e. for all natural numbers $p$ smaller or equal to $b\cdot(k+1)$, we have that $Q(p)$ implies $Q(p+1)$, where $Q(p)$ is the $\Pi^{0}_{2}$ statement that for all $j$ there is an $l$ such that $a_{j+l}>\frac{p-1}{k+1}$. Since $Q(0)$ holds trivially, we have by $\Pi^{0}_{2}$-induction that $Q(b\cdot(k+1)+1)$. But that states that for all $j$ there is an $l$ such that $a_{j+l}>b$, clearly false. $\blacksquare$

Take $p$ as in the Claim. Then $0\leq p\leq b\cdot(k+1)$ and:

1. (i)

for all $n$ there is an $m$ such that $a_{n+m}>\frac{p-1}{k+1}$, so $a_{n+m}\geq\frac{p}{k+1}-\frac{1}{k+1}$, 2. (ii)

there is a $j$ such that for all $l$, $a_{j+l}\leq\frac{p}{k+1}$, so $a_{j+l}\leq\frac{p}{k+1}+\frac{1}{k+1}$,

i.e. $\frac{p}{k+1}$ is a $\frac{1}{k+1}$-limsup of $(a_{n})$. ∎

Remark 4.4**.**

One can even show, as mentioned in the Introduction, that this statement is equivalent to $\Pi^{0}_{2}$-induction. To do that, we tweak the argument used in the proof of [38, Theorem 6.1], whose statement affirms that the existence of limsup’s (without function parameters) implies $\Pi^{0}_{2}$-induction, to also work with rational approximate limsup’s, i.e. in the form given in Proposition 4.3. The limsup hypothesis is used two times: once in Claims 1-3 and once when it yields $\Sigma^{0}_{1}$-induction as the first stage of a bootstrapping process. The second application does not pose any serious problems, while the first one is a bit more involved, since the statements of Claims 1-3 must be adjusted. Set, for any $k\in\mathbb{N}^{*}$, $L(k):=4k(k+1)>0$. One then requires in Claims 2 and 3 from $a$ to be a rational $\frac{1}{L(k)}$-limsup and a rational $\frac{1}{L(k+1)}$-limsup of $(q^{f}_{n})$, respectively, while the new Claim 1 states that for any $k,p\in\mathbb{N}^{*}$ with $p\leq k$ and for any rational $a\in[0,1]$ which is a $\frac{1}{L(k)}$-limsup of $(q^{f}_{n})$, the following are equivalent:

1. (i)

$a\geq\frac{1}{p}-\frac{1}{L(k)}$; 2. (ii)

$a>\frac{1}{p+1}+\frac{1}{L(k)}$; 3. (iii)

for all $n$ there is an $m\geq n$ with $f(m)<p$.

The proof then goes through.

It is not sufficient that one can prove the existence of approximate limsup’s, we must also show that they can play the role that is required of them. The following lemma is crucial in this regard, as it proves that one can extract specific sequence ranks that are needed in a later analysis of a proof, whereas the values of the approximate limsup’s may be discarded.

Lemma 4.5**.**

Let $\varepsilon>0$. Let $(a_{n})$, $(b_{n})$ and $(c_{n})$ be sequences of reals and $q$, $q^{\prime}$ and $r$ be $\frac{\varepsilon}{4}$-limsup’s of them, respectively. If $q\leq r+\frac{\varepsilon}{2}$ and $q^{\prime}\leq r+\frac{\varepsilon}{2}$, then for all $N$ there is a $k$ such that $a_{N+k}\leq c_{N+k}+\varepsilon$ and $b_{N+k}\leq c_{N+k}+\varepsilon$.

Proof.

By the definition of the approximate limsup, we have that:

• •

there is a $j$ such that for all $l$, $a_{j+l}\leq q+\frac{\varepsilon}{4}$;

• •

there is a $j^{\prime}$ such that for all $l$, $b_{j^{\prime}+l}\leq q^{\prime}+\frac{\varepsilon}{4}$;

• •

for all $n$ there is an $m$ such that $c_{n+m}\geq r-\frac{\varepsilon}{4}$, and in the following we denote this $m$ depending on $n$ as $m_{n}$.

Let $N\in\mathbb{N}$. We set $k:=j+j^{\prime}+m_{N+j+j^{\prime}}$. Then we have that

[TABLE]

and similarly, that $b_{N+k}\leq c_{N+k}+\varepsilon$. ∎

We will be using the following weaker forms of the above lemma.

Corollary 4.6**.**

Let $\varepsilon>0$. Let $(a_{n})$ and $(c_{n})$ be sequences of reals and $q$ and $r$ be $\frac{\varepsilon}{4}$-limsup’s of them, respectively. If $q\leq r+\frac{\varepsilon}{2}$, then for all $N$ there is a $k$ such that $a_{N+k}\leq c_{N+k}+\varepsilon$.

Corollary 4.7**.**

Let $\varepsilon>0$. Let $(a_{n})$, $(b_{n})$ and $(c_{n})$ be sequences of reals and $q$, $q^{\prime}$ and $r$ be $\frac{\varepsilon}{4}$-limsup’s of them, respectively. If $q\leq r+\frac{\varepsilon}{2}$ and $q^{\prime}\leq r+\frac{\varepsilon}{2}$, then there is a $k$ such that $a_{k}\leq c_{k}+\varepsilon$ and $b_{k}\leq c_{k}+\varepsilon$.

4.2 Replacing limsup’s by approximate limsup’s

We consider, in this section, $\alpha:\mathbb{N}\to\mathbb{N}$ and $\gamma:\mathbb{N}\to\mathbb{N}^{*}$ such that:

• •

for all $n$ and all $m\geq\alpha(n)$, $t_{m}\geq 1-\frac{1}{n+1}$;

• •

for all $n$, $t_{n}\leq 1-\frac{1}{\gamma(n)}$.

In the case that for all $n$, $t_{n}=1-\frac{1}{n+1}$, we may take, for all $n$, $\alpha(n):=n$ and $\gamma(n):=n+1$.

New proof of the theorem. Again, we divide the proof into a series of claims.

Claim I. Let $(s_{n})\subseteq(0,1)$ and $\varepsilon>0$. Then there is a $y\in C$ and a $q\in\mathbb{Q}$ such that $q$ is an $\frac{\varepsilon}{4}$-limsup of $(\|x_{s_{n}}-y\|^{2})$ and such that for all $z\in C$ and $r\in\mathbb{Q}$ with $r$ being an $\frac{\varepsilon}{4}$-limsup of $(\|x_{s_{n}}-z\|^{2})$, $q\leq r+\frac{\varepsilon}{2}$.

Proof of claim: Denote, for all $n$, $x_{n}:=x_{s_{n}}$. Assume towards a contradiction that for all $y\in C$ and $q\in\mathbb{Q}$ with $q$ being an $\frac{\varepsilon}{4}$-limsup of $(\|x_{n}-y\|^{2})$ there is a $z\in C$ and an $r\in\mathbb{Q}$ such that $r$ is an $\frac{\varepsilon}{4}$-limsup of $(\|x_{n}-z\|^{2})$ and $r<q-\frac{\varepsilon}{2}$. Let now $z_{1}\in C$ be arbitrary and $r_{1}$ be an $\frac{\varepsilon}{4}$-limsup of $(\|x_{n}-z_{1}\|^{2})$. Put, for all $n\leq\left\lceil\frac{2b^{2}}{\varepsilon}\right\rceil+2$, $z_{n+1}$ and $r_{n+1}$ be the $z$ and the $r$ obtained by applying the assumption to $z_{n}$ and $r_{n}$ playing the roles of $y$ and $q$, respectively. Then, since $r_{1}\leq b^{2}+\frac{\varepsilon}{2}$, and by the assumption, for each $n\leq\left\lceil\frac{2b^{2}}{\varepsilon}\right\rceil+2$, we have that $r_{n+1}<r_{n}-\frac{\varepsilon}{2}$, we get that for all $n\leq\left\lceil\frac{2b^{2}}{\varepsilon}\right\rceil+3$, $r_{n}\leq b^{2}-(n-2)\frac{\varepsilon}{2}$. If we choose $n:=\left\lceil\frac{2b^{2}}{\varepsilon}\right\rceil+3$, we obtain that $b^{2}-(n-2)\frac{\varepsilon}{2}\leq-\frac{\varepsilon}{2}$, contradicting the fact that $r_{n}$ is an $\frac{\varepsilon}{4}$-limsup of a sequence of nonnegative reals. $\blacksquare$

Denote, for all $n$, $x_{n}:=x_{t_{n}}$. We shall prove the Cauchyness of the sequence in its “metastable” formulation, namely: for all $\varepsilon>0$ and all $g:\mathbb{N}\to\mathbb{N}$ there is an $N$ such that $\|x_{N}-x_{N+g(N)}\|\leq\varepsilon$. Let, therefore, $\varepsilon>0$ and $g:\mathbb{N}\to\mathbb{N}$. From this point on, we shall use the following notations (where $n,c,d\in\mathbb{N}$ and $p\in C$):

[TABLE]

Claim II. There are $w$, $w^{\prime}$, $v$, $v^{\prime}\in C$ and $k$, $k^{\prime}$, $l$, $l^{\prime}$, $h$, $h^{\prime}\in\mathbb{N}$ such that:

• •

$\|x_{k}-w\|^{2}-\|x_{k}-w-\delta(\varepsilon)(x-w)\|^{2}$,

$\|x^{w}_{k^{\prime}}-w^{\prime}\|^{2}-\|x^{w}_{k^{\prime}}-w^{\prime}-\delta(\varepsilon)(x-w^{\prime})\|^{2}\leq\frac{2\nu_{4}(\varepsilon)\delta(\varepsilon)}{3}$;

• •

$\|x_{l}-w\|^{2}-\left\|x_{l}-\frac{v+w}{2}\right\|^{2}$, $\|x_{l}-v\|^{2}-\left\|x_{l}-\frac{v+w}{2}\right\|^{2}$,

$\|x_{l^{\prime}}-w^{\prime}\|^{2}-\left\|x_{l^{\prime}}-\frac{v^{\prime}+w^{\prime}}{2}\right\|^{2}$, $\|x_{l^{\prime}}-v^{\prime}\|^{2}-\left\|x_{l^{\prime}}-\frac{v^{\prime}+w^{\prime}}{2}\right\|^{2}\leq\nu_{2}(\varepsilon)$;

• •

$h,h^{\prime}\geq\alpha\left(\left\lceil\max\left\{\frac{2b}{\sqrt{\nu_{1}(w,k,k^{\prime},\varepsilon)}},\frac{8b^{2}}{\nu_{1}(w,k,k^{\prime},\varepsilon)}\right\}\right\rceil\right)$;

• •

$\|x_{h}-v\|^{2}-\left\|x_{h}-\frac{v+h_{T}v}{2}\right\|^{2}$, $\|x_{h^{\prime}}-v^{\prime}\|^{2}-\left\|x_{h^{\prime}}-\frac{v^{\prime}+h_{T}v^{\prime}}{2}\right\|^{2}\leq\frac{\nu_{1}(w,k,k^{\prime},\varepsilon)}{2}$.

Proof of claim:

1. A.

The construction of $w$ and $k$.

We apply Claim I for $(t_{n})$ and $u:=\min\left\{\frac{2\nu_{4}(\varepsilon)\delta(\varepsilon)}{3},\nu_{2}(\varepsilon)\right\}$. We obtain $w\in C$ and $q_{w}\in\mathbb{Q}$ such that $q_{w}$ is an $\frac{u}{4}$-limsup of $(\|x_{n}-w\|^{2})$ and for all $z\in C$ and $q_{z}\in\mathbb{Q}$ with $q_{z}$ being an $\frac{u}{4}$-limsup of $(\|x_{n}-z\|^{2})$ we have that $q_{w}\leq q_{z}+\frac{u}{2}$.

By the above applied to $z:=w+\delta(\varepsilon)(x-w)$ and $q_{z}$ an $\frac{u}{4}$-limsup of $(\|x_{n}-z\|^{2})$, we get after using Corollary 4.6 that there is a $k$ such that

[TABLE] 2. B.

The construction of $w^{\prime}$ and $k^{\prime}$.

We apply Claim I for $(t_{s_{w,g}(n)})$ and $u$. We obtain $w^{\prime}\in C$ and $q_{w^{\prime}}\in\mathbb{Q}$ such that $q_{w^{\prime}}$ is an $\frac{u}{4}$-limsup of $(\|x^{w}_{n}-w^{\prime}\|^{2})$ and for all $z\in C$ and $q_{z}\in\mathbb{Q}$ with $q_{z}$ being an $\frac{u}{4}$-limsup of $(\|x^{w}_{n}-z\|^{2})$ we have that $q_{w^{\prime}}\leq q_{z}+\frac{u}{2}$.

By the above applied to $z:=w^{\prime}+\delta(\varepsilon)(x-w^{\prime})$ and $q_{z}$ an $\frac{u}{4}$-limsup of $(\|x^{w}_{n}-z\|^{2})$, we get after using Corollary 4.6 that there is a $k^{\prime}$ such that

[TABLE] 3. C.

The construction of $v$ and $h$.

We apply Claim I for $(t_{n})$ and $u^{\prime}:=\min\left\{\frac{\nu_{1}(w,k,k^{\prime},\varepsilon)}{2},\nu_{2}(\varepsilon)\right\}$. We obtain $v\in C$ and $q_{v}\in\mathbb{Q}$ such that $q_{v}$ is an $\frac{u^{\prime}}{4}$-limsup of $(\|x_{n}-v\|^{2})$ and for all $z\in C$ and $q_{z}\in\mathbb{Q}$ with $q_{z}$ being an $\frac{u^{\prime}}{4}$-limsup of $(\|x_{n}-z\|^{2})$ we have that $q_{v}\leq q_{z}+\frac{u^{\prime}}{2}$.

By the above applied to $z:=\frac{v+h_{T}v}{2}$ and $q_{z}$ an $\frac{u^{\prime}}{4}$-limsup of $(\|x_{n}-z\|^{2})$, we get after using Corollary 4.6 that there is an $h\geq\alpha\left(\left\lceil\max\left\{\frac{2b}{\sqrt{\nu_{1}(w,k,k^{\prime},\varepsilon)}},\frac{8b^{2}}{\nu_{1}(w,k,k^{\prime},\varepsilon)}\right\}\right\rceil\right)$ such that

[TABLE] 4. D.

The construction of $l$.

Since $q_{w}$ is a $\frac{u}{4}$-limsup of $(\|x_{n}-w\|^{2})$, it is also a $\frac{\nu_{2}(\varepsilon)}{4}$-limsup of $(\|x_{n}-w\|^{2})$. Similarly, $q_{v}$ is a $\frac{\nu_{2}(\varepsilon)}{4}$-limsup of $(\|x_{n}-v\|^{2})$.

Put $z:=\frac{v+w}{2}$ and take $q_{z}$ to be a $\frac{\min\{u,u^{\prime}\}}{4}$-limsup of $(\|x_{n}-z\|^{2})$.

Since $q_{z}$ is also a $\frac{u}{4}$-limsup of $(\|x_{n}-z\|^{2})$,

[TABLE]

and similarly

[TABLE]

Also take note that $q_{z}$ is a $\frac{\nu_{2}(\varepsilon)}{4}$-limsup of $(\|x_{n}-z\|^{2})$. By Corollary 4.7, we get that there is an $l$ such that

[TABLE] 5. E.

The construction of $v^{\prime}$ and $h^{\prime}$.

We apply Claim I for $(t_{s_{w,g}(n)})$ and $u^{\prime}$. We obtain $v^{\prime}\in C$ and $q_{v^{\prime}}\in\mathbb{Q}$ such that $q_{v^{\prime}}$ is an $\frac{u^{\prime}}{4}$-limsup of $(\|x^{w}_{n}-v^{\prime}\|^{2})$ and for all $z\in C$ and $q_{z}\in\mathbb{Q}$ with $q_{z}$ being an $\frac{u^{\prime}}{4}$-limsup of $(\|x^{w}_{n}-z\|^{2})$ we have that $q_{v^{\prime}}\leq q_{z}+\frac{u^{\prime}}{2}$.

By the above applied to $z:=\frac{v^{\prime}+h_{T}v^{\prime}}{2}$ and $q_{z}$ an $\frac{u^{\prime}}{4}$-limsup of $(\|x^{w}_{n}-z\|^{2})$, we get after using Corollary 4.6 that there is an $h^{\prime}_{0}\geq\alpha\left(\left\lceil\max\left\{\frac{2b}{\sqrt{\nu_{1}(w,k,k^{\prime},\varepsilon)}},\frac{8b^{2}}{\nu_{1}(w,k,k^{\prime},\varepsilon)}\right\}\right\rceil\right)$ such that

[TABLE]

Put $h^{\prime}:=s_{w,g}(h^{\prime}_{0})\geq h^{\prime}_{0}\geq\alpha\left(\max\left\{\frac{2b}{\sqrt{\nu_{1}(w,k,k^{\prime},\varepsilon)}},\frac{8b^{2}}{\nu_{1}(w,k,k^{\prime},\varepsilon)}\right\}\right)$. Then

[TABLE] 6. F.

The construction of $l^{\prime}$.

Since $q_{w^{\prime}}$ is a $\frac{u}{4}$-limsup of $(\|x^{w}_{n}-w^{\prime}\|^{2})$, it is also a $\frac{\nu_{2}(\varepsilon)}{4}$-limsup of $(\|x^{w}_{n}-w^{\prime}\|^{2})$. Similarly, $q_{v^{\prime}}$ is a $\frac{\nu_{2}(\varepsilon)}{4}$-limsup of $(\|x^{w}_{n}-v^{\prime}\|^{2})$.

Put $z:=\frac{v^{\prime}+w^{\prime}}{2}$ and take $q_{z}$ to be a $\frac{\min\{u,u^{\prime}\}}{4}$-limsup of $(\|x^{w}_{n}-z\|^{2})$.

Since $q_{z}$ is also a $\frac{u}{4}$-limsup of $(\|x^{w}_{n}-z\|^{2})$,

[TABLE]

and similarly

[TABLE]

Also take note that $q_{z}$ is a $\frac{\nu_{2}(\varepsilon)}{4}$-limsup of $(\|x^{w}_{n}-z\|^{2})$. By Corollary 4.7, we get that there is an $l^{\prime}_{0}$ such that

[TABLE]

Put $l^{\prime}:=s_{w,g}(l^{\prime}_{0})$. Then

[TABLE]

We are now done. $\blacksquare$

Claim III. Let $w$, $w^{\prime}$, $v$, $v^{\prime}\in C$ and $k$, $k^{\prime}$, $l$, $l^{\prime}$, $h$, $h^{\prime}\in\mathbb{N}$ be as in Claim II. If we put $N:=k^{\prime}$, then $\|x_{N}-x_{N+g(N)}\|\leq\varepsilon$. (One notices here that the part of the proof corresponding to this claim will not need further inspection, as it is enough to obtain a value for $k^{\prime}$ in an analysis of Claim II.)

Proof of claim: We will further divide the proof of this claim into sub-claims.

Sub-claim 1. We have that:

• •

$\|x_{h}-v\|^{2}-\left\|x_{h}-\frac{v+h_{T}v}{2}\right\|^{2}$, $\|x_{h}-h_{T}v\|^{2}-\left\|x_{h}-\frac{v+h_{T}v}{2}\right\|^{2}$,

$\|x_{h^{\prime}}-v^{\prime}\|^{2}-\left\|x_{h^{\prime}}-\frac{v^{\prime}+h_{T}v^{\prime}}{2}\right\|^{2}$, $\|x_{h^{\prime}}-h_{T}v^{\prime}\|^{2}-\left\|x_{h^{\prime}}-\frac{v^{\prime}+h_{T}v^{\prime}}{2}\right\|^{2}\leq\nu_{1}(w,k,k^{\prime},\varepsilon)$.

Proof of sub-claim: First, we remark that:

[TABLE]

so, using Corollary 2.32.(ii),

[TABLE]

and, by Corollary 2.32.(i),

[TABLE]

Now we may write:

[TABLE]

Similarly, one may show that $\|x_{h^{\prime}}-h_{T}v^{\prime}\|^{2}-\left\|x_{h^{\prime}}-\frac{v^{\prime}+h_{T}v^{\prime}}{2}\right\|^{2}\leq\nu_{1}(w,k,k^{\prime},\varepsilon)$. $\blacksquare$

Sub-claim 2. We have that:

[TABLE]

Proof of sub-claim: Suppose that $\|h_{T}v-v\|\geq\tilde{\theta}(q(w,k,k^{\prime},\varepsilon))$. Then

[TABLE]

so

[TABLE]

which is a contradiction, since $\psi_{b,\eta}(\tilde{\theta}(q(w,k,k^{\prime},\varepsilon)))>0$.

Similarly, one shows that $\|h_{T}v^{\prime}-v^{\prime}\|\leq\tilde{\theta}(q(w,k,k^{\prime},\varepsilon))$. $\blacksquare$

Sub-claim 3. We have that:

• •

$\langle x_{k}-x,j(x_{k}-w)\rangle$, $\langle x^{w}_{k^{\prime}}-x,j(x^{w}_{k^{\prime}}-w^{\prime})\rangle\leq\frac{\nu_{4}(\varepsilon)}{3}$;

• •

$\langle x^{w}_{k^{\prime}}-x,j(x^{w}_{k^{\prime}}-w)\rangle$, $\langle x_{k}-x,j(x_{k}-w^{\prime})\rangle\leq\frac{\varepsilon^{2}}{96}$.

Proof of sub-claim: Since $\|h_{T}v-v\|\leq\tilde{\theta}(q(w,k,k^{\prime},\varepsilon))$, we have, using Corollary 2.32.(iii), that $\|Tv-v\|\leq q(w,k,k^{\prime},\varepsilon)$. We now compute:

[TABLE]

from which we obtain

[TABLE]

Suppose now that $\|w-v\|\geq\omega_{\tau}\left(b,\frac{p(\varepsilon)}{2b}\right)$. Then

[TABLE]

and so

[TABLE]

which is a contradiction, since $\psi_{b,\eta}\left(\omega_{\tau}\left(b,\frac{p(\varepsilon)}{2b}\right)\right)>0$.

Therefore

[TABLE]

so

[TABLE]

We have then

[TABLE]

Similarly, taking into account, when needed, that

[TABLE]

we obtain the other three inequalities. $\blacksquare$

Sub-claim 4. We have that:

[TABLE]

Proof of sub-claim: By Lemma 2.7, we have:

[TABLE]

Given that, as before, $\delta(\varepsilon)\in(0,1)$ and so $w+\delta(\varepsilon)(x-w)=(1-\delta(\varepsilon))w+\delta(\varepsilon)x\in C$, and that

[TABLE]

we get that

[TABLE]

Therefore (using the first item in Claim II),

[TABLE]

In a similar way, using the fact that $\langle x^{w}_{k^{\prime}}-x,j(x^{w}_{k^{\prime}}-w^{\prime})\rangle\leq\frac{\nu_{4}(\varepsilon)}{3}$, we obtain the other inequality to be proven. $\blacksquare$

Sub-claim 5. We have that $\|x^{w}_{N}-w\|\leq\frac{\varepsilon}{2}$.

Proof of sub-claim: We know that $\|x^{w}_{k^{\prime}}-w^{\prime}\|\leq\frac{\varepsilon^{2}}{96b}$. Since

[TABLE]

we have that

[TABLE]

and so

[TABLE]

Similarly, using $x_{k}$ as the “pivot”, we get that $\langle w-x,j(w-w^{\prime})\rangle\leq\frac{\varepsilon^{2}}{32}$, so

[TABLE]

i.e.

[TABLE]

We can now compute:

[TABLE]

which is what we wanted. $\blacksquare$

It follows immediately, by the definition of $x^{w}_{N}$, that $\max\{\|x_{N}-w\|,\|x_{N+g(N)}-w\|\}\leq\frac{\varepsilon}{2}$. To finish the proof of the claim, we see that

[TABLE]

which also finishes the proof of the theorem. $\blacksquare$

5 The extraction of the witness

5.1 The logical analysis of Claim I

The first proposition in this section, Proposition 5.1, is the (partial) functional interpretation of Proposition 4.3, i.e. of the existence of $\varepsilon$-limsup’s using only functionals definable in the fragment $T_{1}$ (which only contains the recursor constants $R_{0}$ and $R_{1}$) of Gödel’s $T$. This analysis was obtained with the crucial guidance of the functional interpretation of induction from [58].

We then give in Proposition 5.2 the (partial) functional interpretation of the proof of Claim I, i.e. the existence of $\varepsilon$-infima for approximate limsup’s, by functions definable in $T_{2}$ (as now also $R_{2}$ is used). Since the functional interpretation of the Claim II, which only uses the existence of approximate limsup’s and plain logic plus elementary arithmetic, can be interpreted already in $T_{1},$ this guarantees the extractability of a rate of metastability definable in $T_{2}.$

In the following we use, for any $n,m\in\mathbb{N}$, the notation n\mathbin{\vphantom{+}\text{\ooalign{\kern-1.50696pt\cr\smash{\cdot}$\cr\kern 1.50696pt\cr$-\cr}}}m to denote $n-m$ if $n\geq m$ and [math] otherwise. We also use the usual conventions when defining higher-order functionals and write e.g. ‘JUM(b\cdot(k+1)\mathbin{\vphantom{+}\text{\ooalign{\kern-1.50696pt\cr\smash{\cdot}$\cr\kern 1.50696pt\cr$-\cr}}}PUM)’ instead of ‘J(U,M,b\cdot(k+1)\mathbin{\vphantom{+}\text{\ooalign{\kern-1.50696pt\cr\smash{\cdot}$\cr\kern 1.50696pt\cr$-\cr}}}P(U,M))’. Occasionally, we also use the $\lambda$-notation $\lambda x_{1},\ldots,x_{n}.t[x_{1},\ldots,x_{n}]$ from functional programming, for a term $t[x_{1},\ldots,x_{n}]$ depending on the variables $x_{1},\ldots,x_{n},$ to denote the function: $(x_{1},\ldots,x_{n})\mapsto t[x_{1},\ldots,x_{n}].$

Proposition 5.1**.**

Let $b,k\in\mathbb{N}$ and $(a_{n})$ be a sequence of reals contained in the interval $[0,b]$. Define the following functionals:

[TABLE]

Then, for all $U,M:\mathbb{N}^{\mathbb{N}}\times\mathbb{N}\times\mathbb{N}\to\mathbb{N}$, we have that $0\leq PUM\leq b\cdot(k+1)$ and:

1. (i)

$a_{M(NUM,TUM,PUM)+(NUM)(M(NUM,TUM,PUM))}\geq\frac{PUM}{k+1}-\frac{1}{k+1}$; 2. (ii)

$a_{TUM+U(NUM,TUM,PUM)}\leq\frac{PUM}{k+1}+\frac{1}{k+1}$.

Proof.

We start with the following claim, analogous to the one in the proof of Proposition 4.3.

Claim. There is a $p\in\mathbb{N}$ with $0\leq p\leq b\cdot(k+1)$ such that it is not the case that

[TABLE]

implies that

[TABLE]

Proof of claim: Assume towards a contradiction that the opposite holds, i.e. for all natural numbers $p$ smaller or equal to $b\cdot(k+1)$, we have that $Q(p)$ implies $Q(p+1)$, where $Q(p)$ is the statement that

[TABLE]

Since $Q(0)$ holds trivially, we have by induction that $Q(b\cdot(k+1)+1)$. But that states that

[TABLE]

which clearly is false. $\blacksquare$

Take $p$ to be minimal with this property. Then $p=PUM$, by the definition of the latter, so clearly $0\leq PUM\leq b\cdot(k+1)$. We prove the remaining conclusions.

1. (i)

Since $PUM<b\cdot(k+1)+1$, we may write b\cdot(k+1)+1\mathbin{\vphantom{+}\text{\ooalign{\kern-1.50696pt\cr\smash{\cdot}$\cr\kern 1.50696pt\cr$-\cr}}}PUM=(b\cdot(k+1)\mathbin{\vphantom{+}\text{\ooalign{\kern-1.50696pt\cr\smash{\cdot}$\cr\kern 1.50696pt\cr$-\cr}}}PUM)+1, so

[TABLE]

and

[TABLE]

Thus,

[TABLE] 2. (ii)

Since

[TABLE]

and

[TABLE]

we have that

[TABLE]

The proof is finished. ∎

The following is a logical analysis of Claim I in the second proof (using approximate limsup’s) of Theorem 3.1 and uses as an ingredient the functional interpretation of the existence of approximate limsup’s. Here, and in the remainder of the paper, we shall frequently use numerical indices to refer to components of tuples.

Proposition 5.2**.**

Let $b\in\mathbb{N}^{*}$. Let $X$ be a Banach space, $C\subseteq X$ be a set of diameter at most $b$ and $(x_{n})\subseteq C$. Let $\varepsilon>0$. Let $z_{1}\in C$ be arbitrary. Define the following functionals (where any $\mathcal{O}$ denotes a constant zero function):

[TABLE]

In the above, $P$, $N$ and $T$ are the functionals defined in Proposition 5.1, customized by instantiating their free parameters with $b\mapsto b^{2}$, $k\mapsto\left\lceil\frac{4}{\varepsilon}\right\rceil$ and $(a_{n})\mapsto(\|x_{n}-z_{1}\|^{2})$. We continue to use in the following the notation $k:=\left\lceil\frac{4}{\varepsilon}\right\rceil$.

Then, for any $\Omega$ there is an $i<I$ such that if we denote

[TABLE]

and

[TABLE]

we have that

[TABLE]

and that if

[TABLE]

then

[TABLE]

In order to obtain a true realizer, we now put, for any $\Omega$, $i(\Omega)$ to be the least $i<I$ which realizes the above (in order to define it properly as a functional, we put it to be [math] in the “impossible” case that there isn’t one, as in the definition of $P$ in Proposition 5.1) and $\Psi(\Omega)$ to be ${\widetilde{\Psi}}(\Omega,i(\Omega))$.

Proof.

Assume towards a contradiction that the opposite holds, i.e. there is an $\Omega$ such that if we denote for all $x\leq I$,

[TABLE]

and

[TABLE]

then for all $x<I$, if

[TABLE]

then

[TABLE]

[TABLE]

[TABLE]

and

[TABLE]

Remark that for all $x\leq I$,

[TABLE]

In addition,

[TABLE]

We now derive that for all $x<I$,

[TABLE]

and

[TABLE]

together with the corresponding statement $\widetilde{N}_{I-x}(r_{I-x},z_{I-x},\widetilde{L}_{I-x},\widetilde{m}_{I-x})=n_{I-x-1}$. Therefore, what we know is that for all $x<I$, if

[TABLE]

then

[TABLE]

[TABLE]

[TABLE]

and

[TABLE]

We shall now prove by induction that for all $x\leq I$,

[TABLE]

It remains to show the base case ($x=0$): we apply Proposition 5.1 for $\overline{U}(\Omega)$ and $\overline{M}(\Omega)$. Using

[TABLE]

and - similarly -

[TABLE]

we see that what we obtain is that

[TABLE]

Using that $\frac{1}{k+1}\leq\frac{\varepsilon}{4}$, we obtain that

[TABLE]

i.e. what we wanted. The induction case follows immediately by our assumption. Therefore we have that for all $x<I$,

[TABLE]

so

[TABLE]

Since by construction $p_{I}\leq b^{2}\cdot(k+1)$ and $0\leq\frac{p_{0}}{k+1}$, what we obtain is

[TABLE]

contradicting the fact that $I=\left\lceil\frac{2b^{2}}{\varepsilon}\right\rceil$. ∎

5.2 The logical analysis of Claim II

In the sequel, we shall denote by (here $x$ stands for the sequence $(x_{n})$)

[TABLE]

the statement that (where we write $k:=\left\lceil\frac{4}{\delta}\right\rceil$)

[TABLE]

and that if

[TABLE]

then

[TABLE]

We will also make the parameters $(x_{n})$ and $\varepsilon>0$ (though not $b$) in the $\Psi$ from Proposition 5.2 explicit in what follows. Thus, Proposition 5.2 states that for any $(x_{n})\subseteq C$, $\varepsilon>0$, $g$ and $f$, if we put

[TABLE]

i.e., in particular, $\underline{w}$ is a 5-tuple – corresponding to $(\widetilde{U},\widetilde{N},p,y,L)$ in the above definition – whereas $k$ is a number (and also, we add for clarity, $g$ returns a 5-tuple – corresponding to $(r,z,\widetilde{L},\widetilde{m},u)$ – while $f$ returns a number), then

[TABLE]

5.2.1 Preparation

In the proposition below, the eight items correspond to the eight inequalities involving the sequence $(x_{n})$ that must be satisfied in Claim II.

Proposition 5.3**.**

Let $X$ be a Banach space, $b\in\mathbb{N}^{*}$ and $C\subseteq X$ be a set of diameter at most $b$. Let $(x_{n})\subseteq C$. Then there is a $\Phi$ such that for any $\Psi$ having the property that for any $(y_{n})\subseteq C$, $\delta>0$, $g$ and $f$, if we put

[TABLE]

then one has

[TABLE]

we have that for any $u$, $u^{\prime}$, $\underline{g}$, $\underline{g}^{\prime}$, $\underline{f}$, $\underline{f}^{\prime}$, $\iota$, and $\varphi$, if we put

[TABLE]

we have that

1. (i)

$A(x,u,\underline{w},g_{0}(\underline{w},k),k+f_{0}(\underline{w},k))$; 2. (ii)

$A(\varphi(\underline{w}),u,\underline{w}^{\prime},g^{\prime}_{0}(\underline{w},k,\underline{w}^{\prime},k^{\prime}),k^{\prime}+f^{\prime}_{0}(\underline{w},k,\underline{w}^{\prime},k^{\prime}))$; 3. (iii)

$A(x,u^{\prime}(\underline{w},k,\underline{w}^{\prime},k^{\prime}),\underline{v},g_{1}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},h),h+f_{1}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},h))$;

$h\geq\iota(\underline{w},k,\underline{w}^{\prime},k^{\prime})$; 4. (iv)

$A(x,u^{\prime}(\underline{w},k,\underline{w}^{\prime},k^{\prime}),\underline{v},g_{2}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},l),l+f_{2}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},l))$; 5. (v)

$A(x,u,\underline{w},g_{2}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},l),l+f_{2}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},l))$; 6. (vi)

$A(\varphi(\underline{w}),u^{\prime}(\underline{w},k,\underline{w}^{\prime},k^{\prime}),\underline{v}^{\prime},g^{\prime}_{1}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v}^{\prime},h^{\prime}),h^{\prime}+f^{\prime}_{1}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v}^{\prime},h^{\prime}))$;

$h^{\prime}\geq\iota(\underline{w},k,\underline{w}^{\prime},k^{\prime})$; 7. (vii)

$A(\varphi(\underline{w}),u^{\prime}(\underline{w},k,\underline{w}^{\prime},k^{\prime}),\underline{v}^{\prime},g^{\prime}_{2}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v}^{\prime},l^{\prime}),l^{\prime}+f^{\prime}_{2}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v}^{\prime},l^{\prime}))$; 8. (viii)

$A(\varphi(\underline{w}),u,\underline{w}^{\prime},g^{\prime}_{2}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v}^{\prime},l^{\prime}),l^{\prime}+f^{\prime}_{2}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v}^{\prime},l^{\prime}))$.

Take notice that:

By the discussion at the beginning of this subsection, we already have such a $\Psi$, but its form is not relevant for this proposition. 2. 2.

The exact form of the $\Phi$ will be given over the course of the proof.

Proof.

We shall first derive a purely qualitative version of the above. Namely, let $u$, $u^{\prime}$, $\underline{g}$, $\underline{g}^{\prime}$, $\underline{f}$, $\underline{f}^{\prime}$, $\iota$, $\varphi$ be given. We will show that there exist $\underline{w}$, $k$, $\underline{w}^{\prime}$, $k^{\prime}$, $\underline{v}$, $\underline{v}^{\prime}$, $l$, $l^{\prime}$, $h$, $h^{\prime}$ such that (i)-(viii) hold. It will then follow, by the functional interpretation, that these objects can be explicitly constructed. The first step will be to prove the “non-metastable” version of our hypothesis, which we do in the following claim.

Claim. For all $(y_{n})\subseteq C$ and $\delta>0$, there are $\underline{w}$ and $k$ such that for all $\underline{z}$ and $m$,

[TABLE]

Proof of claim: Suppose the opposite, so there are $(y_{n})\subseteq C$ and $\delta>0$ such that for all $\underline{w}$ and $k$ there are $\underline{z}$ and $m$, such that it is not the case that

[TABLE]

Put, for any $\underline{w}$ and $k$, $(g,f)(\underline{w},k)$ to be such a $\underline{z}$ and $m$. Then, for all $\underline{w}$ and $k$,

[TABLE]

If we now put $(\underline{w},k):=\Psi(y,\delta,g,f)$, we contradict our hypothesis. $\blacksquare$

If we apply the Claim to $(x,u)$, we get $\underline{w}$ and $k$ such that for all $\underline{z}$ and $m$,

[TABLE]

from which we get (i). Apply then the Claim to $(\varphi(\underline{w}),u)$ to get $\underline{w}^{\prime}$ and $k^{\prime}$ such that for all $\underline{z}$ and $m$,

[TABLE]

from which we get (ii). Now apply the Claim to $(x,u^{\prime}(\underline{w},k,\underline{w}^{\prime},k^{\prime}))$ to get $\underline{v}$ and $h_{0}$ such that for all $\underline{z}$ and $m$,

[TABLE]

Put $h:=h_{0}+\iota(\underline{w},k,\underline{w}^{\prime},k^{\prime})$. Then we have that for all $\underline{z}$ and $m$,

[TABLE]

and so we get (iii). Let $l:=k+h_{0}$. From (9), we have that for all $\underline{z}$ and $m$,

[TABLE]

from which we get (iv). Similarly, from (8), we have that for all $\underline{z}$ and $m$,

[TABLE]

from which we get (v). Afterwards, $\underline{v}^{\prime}$, $l^{\prime}$ and $h^{\prime}$ – and thus (vi), (vii) and (viii) – are obtained in a similar manner. $\blacksquare$

Now we proceed to the construction of $\Phi$. Since the above proof used only pure logic and the basic properties of the operation of addition, it follows by the soundness theorem of the functional interpretation that $\Phi$ can be constructed out of just $\lambda$-terms, $+$ and case distinction. When we shall majorize $\Phi$ to get our final bound, the case distinction will disappear, being replaced by the maximum. This is why we do not need to solve the case distinction further (which we could, by using suitable rational approximations, in order for the $\Phi$ to be fully constructive).

For conceptual clarity, we shall split the proof analysis into two distinct parts, the purely logical one and the “mathematical” one (which uses addition). Define the following functionals:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

Claim. There exist $\underline{w}$, $k$, $\underline{w}^{\prime}$, $k^{\prime}$, $\underline{v}$, $\tilde{h}$, $\underline{v}^{\prime}$, $\tilde{h}^{\prime}$ such that

1. (i’)

$A(x,u,\underline{w},g_{0}(\underline{w},k),k+f_{0}(\underline{w},k))$; 2. (ii’)

$A(\varphi(\underline{w}),u,\underline{w}^{\prime},g^{\prime}_{0}(\underline{w},k,\underline{w}^{\prime},k^{\prime}),k^{\prime}+f^{\prime}_{0}(\underline{w},k,\underline{w}^{\prime},k^{\prime}))$; 3. (iii’)

$A(x,u^{\prime}(\underline{w},k,\underline{w}^{\prime},k^{\prime}),\underline{v},\tilde{g}_{1}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},\tilde{h}),\tilde{h}+\tilde{f}_{1}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},\tilde{h}))$; 4. (iv’)

$A(x,u^{\prime}(\underline{w},k,\underline{w}^{\prime},k^{\prime}),\underline{v},\tilde{g}_{2}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},\tilde{h}),\tilde{h}+\tilde{f}_{2}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},\tilde{h}))$; 5. (v’)

$A(x,u,\underline{w},\tilde{g}_{3}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},\tilde{h}),k+\tilde{f}_{3}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},\tilde{h}))$; 6. (vi’)

$A(\varphi(\underline{w}),u^{\prime}(\underline{w},k,\underline{w}^{\prime},k^{\prime}),\underline{v}^{\prime},\tilde{g}^{\prime}_{1}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v}^{\prime},\tilde{h}^{\prime}),\tilde{h}^{\prime}+\tilde{f}^{\prime}_{1}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v}^{\prime},\tilde{h}^{\prime}))$; 7. (vii’)

$A(\varphi(\underline{w}),u^{\prime}(\underline{w},k,\underline{w}^{\prime},k^{\prime}),\underline{v}^{\prime},\tilde{g}^{\prime}_{2}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v}^{\prime},\tilde{h}^{\prime}),\tilde{h}^{\prime}+\tilde{f}^{\prime}_{2}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v}^{\prime},\tilde{h}^{\prime}))$; 8. (viii’)

$A(\varphi(\underline{w}),u,\underline{w}^{\prime},\tilde{g}^{\prime}_{3}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v}^{\prime},\tilde{h}^{\prime}),k^{\prime}+\tilde{f}^{\prime}_{3}(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v}^{\prime},\tilde{h}^{\prime}))$.

Proof of claim: Define $\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},\tilde{h},\underline{v}^{\prime},\tilde{h}^{\prime}$ in the following way:

[TABLE]

We first apply the hypothesis on $\Psi$ to $(x,u,(g_{w},f_{w}))$. Since $(\underline{w},k)=\Psi(x,u,(g_{w},f_{w}))$, we have that

[TABLE]

Suppose that it is not the case that

[TABLE]

Then, by the definition of $(g_{w},f_{w})$, we have that $(g_{w},f_{w})(\underline{w},k)=(g_{0},f_{0})(\underline{w},k)$, so, by (10), we have that (11) holds, which is a contradiction. Therefore (11) holds, so $(g_{w},f_{w})(\underline{w},k)=(\tilde{g}_{3},\tilde{f}_{3})(\underline{w},k,\underline{w}^{\prime},k^{\prime},\underline{v},\tilde{h})$ and

[TABLE]

We have thus proven the first and fifth item on our list. The other three pairs of items are proven in the same way, by applying the hypothesis on $\Psi$ to

[TABLE]

[TABLE]

and

[TABLE]

successively. $\blacksquare$

To finish the proof, we need only to use the $\underline{w}$, $k$, $\underline{w}^{\prime}$, $k^{\prime}$, $\underline{v}$, $\underline{v}^{\prime}$ already obtained in the claim and then to put

[TABLE]

[TABLE]

Then the items (i)-(viii) follow from the corresponding ones in the claim by a simple verification using the above definitions and the earlier ones of $\underline{\tilde{g}}$, $\underline{\tilde{g}}^{\prime}$, $\underline{\tilde{f}}$ and $\underline{\tilde{f}}^{\prime}$. ∎

Remark 5.4**.**

The case distinctions made in defining the various functions in the proof of the claim above (and also in some proofs below) serve to achieve that the value produced simultaneously satisfies two requirements. This is reminiscent of the treatment of the logical contraction axiom $A\to A\wedge A$ in Gödel’s functional (‘Dialectica’) interpretation [30]. In the end, when computing the bound we are interested in by a process of majorization (monotone functional interpretation, see [40]), we can always just take the maximum of the two values and so the case distinctions are not needed to be computed but serve to justify why the bound is correct. Alternatively, the correctness of taking the maximum can also be argued for by using the so-called bounded functional interpretation [24] which globally changes the whole interpretation whereas we prefer our local verification as this does not require to actually spell out the general interpretation.

Lemma 5.5**.**

Let $b\in\mathbb{N}^{*}$, $X$ be a Banach space, $C\subseteq X$ be a set of diameter at most $b$ and $(x_{n})\subseteq C$. Assume that there are suitable $\delta$, $\delta^{\prime}$, $\widetilde{\delta}$, $\underline{w}$, $\underline{w}^{\prime}$, $\underline{q}$, $m$, $n$, $z$, $N$, $T$, $P$, $k$, $U$, $M$ such that:

1. (i)

$A(x,\delta,\underline{w},\underline{q},m+n)$; $A(x,\delta^{\prime},\underline{w}^{\prime},\underline{q},m+n)$; 2. (ii)

$0<\delta\leq\widetilde{\delta}$; $0<\delta^{\prime}\leq\widetilde{\delta}$; 3. (iii)

$z=q_{2}$; 4. (iv)

$N$, $T$ and $P$ are the functionals defined in Proposition 5.1, customized by instantiating their free parameters with $b\mapsto b^{2}$, $k\mapsto\left\lceil\frac{4}{\min(\delta,\delta^{\prime})}\right\rceil$ and $(a_{n})\mapsto(\|x_{n}-z\|^{2})$; 5. (v)

$k=\left\lceil\frac{4}{\min(\delta,\delta^{\prime})}\right\rceil$; 6. (vi)

$(U,M)$, for an arbitrary argument $\underline{v}$, has the following value: if it is not the case that

[TABLE]

then $(v_{1}(m),m)$, else if it is not the case that

[TABLE]

and

[TABLE]

then $(w_{2},w_{1})(v_{3},z,v_{1},v_{2})$, else $(w^{\prime}_{2},w^{\prime}_{1})(v_{3},z,v_{1},v_{2})$; 7. (vii)

$(q_{1},q_{3},q_{4})=(P,N,T)(U,M)$; 8. (viii)

$q_{5}=0$; 9. (ix)

$n=NUM(m)$.

Then we have that

[TABLE]

Proof.

By the definition of $A$, we have that

[TABLE]

and that if

[TABLE]

and

[TABLE]

then

[TABLE]

The second instance of $A$ shows that

[TABLE]

and that if

[TABLE]

and

[TABLE]

then

[TABLE]

By Proposition 5.1 and the condition on $(N,T,P)$, we get that

[TABLE]

By the condition on $(U,M)$, if it is not the case that

[TABLE]

then $(U,M)(NUM,TUM,PUM)=(NUM(m),m)$. By (13), it follows that (14) holds, contradicting our assumption. Therefore, indeed, (14) holds. Suppose now that it is not the case that

[TABLE]

Then $(U,M)(NUM,TUM,PUM)=(w_{2},w_{1})(PUM,z,NUM,TUM)$. By (13), it follows that (15) holds, contradicting our assumption. Therefore, indeed, (15) holds. In particular, since $\frac{1}{k+1}\leq\frac{\delta}{4}$,

[TABLE]

and

[TABLE]

Thus, $(U,M)(NUM,TUM,PUM)=(w^{\prime}_{2},w^{\prime}_{1})(PUM,z,NUM,TUM)$. Yet again, by (13), it follows that

[TABLE]

and

[TABLE]

so, since $\frac{1}{k+1}\leq\frac{\delta^{\prime}}{4}$,

[TABLE]

and

[TABLE]

Therefore, we have that

[TABLE]

and

[TABLE]

We may now compute:

[TABLE]

and similarly we obtain

[TABLE]

so we are done. ∎

The following corollary is simply the instantiation of Lemma 5.5 above for $\delta^{\prime}:=\delta$, $\widetilde{\delta}:=\delta$ and $\underline{w}^{\prime}:=\underline{w}$.

Corollary 5.6**.**

Let $b\in\mathbb{N}^{*}$, $X$ be a Banach space, $C\subseteq X$ be a set of diameter at most $b$ and $(x_{n})\subseteq C$. Assume that there are suitable $\delta$, $\underline{w}$, $\underline{q}$, $m$, $n$, $z$, $N$, $T$, $P$, $k$, $U$, $M$ such that:

1. (i)

$A(x,\delta,\underline{w},\underline{q},m+n)$; 2. (ii)

$\delta>0$; 3. (iii)

$z=q_{2}$; 4. (iv)

$N$, $T$ and $P$ are the functionals defined in Proposition 5.1, customized by instantiating their free parameters with $b\mapsto b^{2}$, $k\mapsto\left\lceil\frac{4}{\delta}\right\rceil$ and $(a_{n})\mapsto(\|x_{n}-z\|^{2})$; 5. (v)

$k=\left\lceil\frac{4}{\delta}\right\rceil$; 6. (vi)

$(U,M)$, for an arbitrary argument $\underline{v}$, has the following value: if it is not the case that

[TABLE]

then $(v_{1}(m),m)$, else $(w_{2},w_{1})(v_{3},z,v_{1},v_{2})$; 7. (vii)

$(q_{1},q_{3},q_{4})=(P,N,T)(U,M)$; 8. (viii)

$q_{5}=0$; 9. (ix)

$n=NUM(m)$.

Then we have that

[TABLE]

5.2.2 The extraction of the quantities in Claim II

We will now show how to prove Claim II in the second proof of Theorem 3.1 (the one that uses approximate limsup’s). We use the notations introduced before the statement of that claim.

We will now define $u,u^{\prime},\underline{g},\underline{g}^{\prime},\underline{f},\underline{f}^{\prime},\iota,\varphi$.

1. I.

The definition of $u$ and $\varphi$.

These quantities are defined analogously to the corresponding ones in (the proof of) Claim II. First put

[TABLE]

For the $\varphi$, we just have to extract the point $w$ (i.e. the fourth component) from $\underline{w}$ and then form the sequence $(x^{w}_{n})$ as before. 2. II.

The definition of $g_{0}$ and $f_{0}$.

Consider some arbitrary $(\widetilde{U},\widetilde{N},p,y,L,m)$ for their arguments.

Let $z$ be $y+\delta(\varepsilon)(x-y)$ and $N$, $T$ and $P$ be the functionals defined in Proposition 5.1, customized by instantiating their free parameters with $b\mapsto b^{2}$, $k\mapsto\left\lceil\frac{4}{u}\right\rceil$ and $(a_{n})\mapsto(\|x_{n}-z\|^{2})$. We continue to use in the following the notation $k:=\left\lceil\frac{4}{u}\right\rceil$. We define $(U,M)$, for an arbitrary argument $\underline{v}$, in the following way: if it is not the case that

[TABLE]

then put their value as $(v_{1}(m),m)$, else put it as $(\widetilde{N},\widetilde{U})(v_{3},z,v_{1},v_{2})$. Finally, put the value of $g_{0}$ to be $(PUM,z,NUM,TUM,0)$ and the value of $f_{0}$ to be $(NUM)(m)$. 3. III.

The definition of $g^{\prime}_{0}$ and $f^{\prime}_{0}$.

Consider some arbitrary $(\widetilde{U},\widetilde{N},p,y,L,m,\widetilde{U}^{\prime},\widetilde{N}^{\prime},p^{\prime},y^{\prime},L^{\prime},m^{\prime})$ for their arguments.

Let $z$ be $y^{\prime}+\delta(\varepsilon)(x-y^{\prime})$ and $N$, $T$ and $P$ be the functionals defined in Proposition 5.1, customized by instantiating their free parameters with $b\mapsto b^{2}$, $k\mapsto\left\lceil\frac{4}{u}\right\rceil$ and $(a_{n})\mapsto(\|x^{y}_{n}-z\|^{2})$. We continue to use in the following the notation $k:=\left\lceil\frac{4}{u}\right\rceil$. We define $(U,M)$, for an arbitrary argument $\underline{v}$, in the following way: if it is not the case that

[TABLE]

then put their value as $(v_{1}(m^{\prime}),m^{\prime})$, else put it as $(\widetilde{N}^{\prime},\widetilde{U}^{\prime})(v_{3},z,v_{1},v_{2})$. Finally, put the value of $g^{\prime}_{0}$ to be $(PUM,z,NUM,TUM,0)$ and the value of $f^{\prime}_{0}$ to be $(NUM)(m^{\prime})$. 4. IV.

The definition of $u^{\prime}$ and $\iota$.

Consider some arbitrary $(\underline{w},k,\underline{w}^{\prime},k^{\prime})$ for their arguments.

Put

[TABLE]

Now put the value of $u^{\prime}$ to be

[TABLE]

and the one of $\iota$ to be

[TABLE] 5. V.

The definition of $g_{1}$ and $f_{1}$.

These are defined similarly to $(g_{0},f_{0})$ and $(g^{\prime}_{0},f^{\prime}_{0})$, with the caveat that we need access to $(\underline{w},k,\underline{w}^{\prime},k^{\prime})$ in order to work with the value $u^{\prime}(\underline{w},k,\underline{w}^{\prime},k^{\prime})$ when defining the corresponding $N$, $T$ and $P$. 6. VI.

The definition of $g_{2}$ and $f_{2}$.

These will play a role in the application of Lemma 5.5, so we step carefully through their definition.

Consider some arbitrary $(\widetilde{U},\widetilde{N},p,w,L,m,\widetilde{U}^{\prime},\widetilde{N}^{\prime},p^{\prime},w^{\prime},L^{\prime},m^{\prime},\widetilde{U}^{\prime\prime},\widetilde{N}^{\prime\prime},p^{\prime\prime},v,L^{\prime\prime},l)$ for their arguments.

Let $z$ be $\frac{v+w}{2}$ and $N$, $T$ and $P$ be the functionals defined in Proposition 5.1, customized by instantiating their free parameters with $b\mapsto b^{2}$, $k\mapsto\left\lceil\frac{4}{\min\{u,u^{\prime}(\underline{w},k,\underline{w}^{\prime},k^{\prime})\}}\right\rceil$ and $(a_{n})\mapsto(\|x_{n}-z\|^{2})$. We continue to use in the following the notation $k:=\left\lceil\frac{4}{\min\{u,u^{\prime}(\underline{w},k,\underline{w}^{\prime},k^{\prime})\}}\right\rceil$. We define $(U,M)$, for an arbitrary argument $\underline{v}$, in the following way: if it is not the case that

[TABLE]

then $(v_{1}(m),m)$, else if it is not the case that

[TABLE]

and

[TABLE]

then put their value as $(\widetilde{N},\widetilde{U})(v_{3},z,v_{1},v_{2})$, else put it as $(\widetilde{N}^{\prime\prime},\widetilde{U}^{\prime\prime})(v_{3},z,v_{1},v_{2})$. Finally, put the value of $g_{2}$ to be $(PUM,z,NUM,TUM,0)$ and the value of $f_{2}$ to be $(NUM)(m)$. 7. VII.

The definition of $g^{\prime}_{1}$ and $f^{\prime}_{1}$.

These are defined similarly to $(g_{1},f_{1})$. 8. VIII.

The definition of $g^{\prime}_{2}$ and $f^{\prime}_{2}$.

These are defined similarly to $(g_{2},f_{2})$.

Now that we have defined $u,u^{\prime},\underline{g},\underline{g}^{\prime},\underline{f},\underline{f}^{\prime},\iota,\varphi$, put

[TABLE]

and apply Proposition 5.3.

Claim II then follows by applying Corollary 5.6 four times and Lemma 5.5 two times, and then performing some simple computations similar to the ones in the original proof of the claim. The relevant fact here is that the $N$ that witnesses the metastability property is equal to

[TABLE]

6 The rate of metastability

When one has reached the end of the previous section, one can rightfully say that one is in the possession of a formula witnessing, for any $\varepsilon$ and $g$, the rank corresponding to the metastable reformulation of the Cauchy property (depending on additional parameters of the problem). It is however not an effective formula and not uniform at all as it depends on all the data of the problem. However by a process of majorization one easily obtains a bound (called a rate of metastability in the Introduction) which is both effective and highly uniform in the sense that it – in addition to $\varepsilon$ and $g$ – only depends on the norm bound $b$ and the moduli $\eta$, $\tau$, $\Theta$, $\alpha$, and $\gamma$ but not on $X$, $C$, $T$, or $(t_{n})$ themselves. In order to explain this approach, however, we need to first make a detour into the details of the calculus of functionals in which our final bound will be expressed.

The system $T$ of Hilbert-Gödel, mentioned in the Introduction, is a system of functionals of finite types. Those finite types are defined inductively in the following way: there is a primitive type of natural numbers, and if we have two types $\rho$ and $\tau$, we have a type denoted by $\rho\to\tau$ of functions from elements of type $\rho$ to elements of type $\tau$. Therefore, there is e.g. a type of functions $f:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}^{\left(\mathbb{N}^{\mathbb{N}}\right)}$. Product types are not built into the system, but they can be emulated by currying, i.e. the identification of $A^{B\times C}$ with $(A^{B})^{C}$. The functionals themselves are given by terms in this system, which are built up inductively by repeated application of variables and of constants for zero and successor, for basic combinatory operations, and lastly for recursion over natural numbers.

The crucial notion that we will make use of in the following is the one of majorization, introduced by Howard [35]. Majorization is a family of binary relations, i.e. on elements of each type $\rho$ one has a relation $\succeq_{\rho}$. It is defined inductively and, moreover, hereditarily: for two natural numbers $n$ and $m$ one has $n\succeq_{\mathbb{N}}m$ iff $n\geq m$ and if $f$ and $g$ are of type $\rho\to\tau$ then $f\succeq_{\rho\to\tau}g$ iff for all $m$, $n$ of type $\rho$ with $m\succeq_{\rho}n$ one has $f(m)\succeq_{\tau}g(n)$. For example, to any $f:\mathbb{N}\to\mathbb{N}$, we associate the function $f^{M}:\mathbb{N}\to\mathbb{N}$, defined for any $n\in\mathbb{N}$, by

[TABLE]

and it is immediate that $f^{M}\succeq_{\mathbb{N}^{\mathbb{N}}}f$ – we say of $f^{M}$ that it majorizes or is a majorant for $f$. Not all elements of higher types admit a majorant, but all the constants of $T$ do, and by heredity this extends to all terms (containing only variable of types $\mathbb{N},\mathbb{N}\to\mathbb{N}$) of $T$. As an illustrating example, if $f$ is defined recursively by a schema like the following (suppressing the type information and ignoring the definitions of $a$ and $g$):

[TABLE]

then if $a^{*}$ and $g^{*}$ are majorants for $a$ and $g$, respectively, it is easy to check that the function $f^{*}$ defined by

[TABLE]

majorizes $f$, where $\max$ for functionals is defined pointwise.

There is one further issue we need to take care of. In order to formalize arguments involving e.g. Banach spaces, one needs to extend (as was first done in [39]) the type system with a new primitive type $X$ corresponding to elements of such a space. To any such extended (‘abstract’) type $\rho$ one can then associate an ordinary type $\widehat{\rho}$ simply by replacing all the $X$’s with $\mathbb{N}$’s. Majorization is then defined in [27] on each abstract type $\rho$ as a binary relation between elements of type $\widehat{\rho}$ and those of type $\rho$, as follows: first we have that for any $x\in X$ and $n\in\mathbb{N}$, $n\succeq_{X}x$ iff $n\geq\|x\|$ and then one continues in the same hereditary manner as on the ordinary types.

As a consequence of all this, if one would majorize all the functionals that play a role into the definition of the witness obtained earlier, one would get a chance at finding a purely numerical (and thus uniform) rate of metastability in the sense defined above, after all the case distinctions are removed in favour of taking the corresponding maximum. This is what we will now proceed to do in a stepwise fashion.

First, we majorize the functionals introduced in Proposition 5.1. Those have three hidden parameters: the sequence itself, which is only used directly when defining $P$, and so it completely disappears by majorization, the $k$, which we show here explicitly, and the upper bound, which we instantiate with $b^{2}$, since that is the greatest possible bound on the sequences for which the approximate limsup’s are obtained. Since the $P$ is trivially majorized by $b^{2}\cdot(k^{*}+1)$, we omit it, since we can replace it by this value in its further appearances. Note that only the $N^{*}$ and the $T^{*}$ will play a role in further developments.

[TABLE]

We now do the same for the functionals in Proposition 5.2. Remark the added explicit parameter $l^{*}$. We specify that the variables $p^{*}$, $y^{*}$ and $m^{*}$ are of type $\mathbb{N}$, $L^{*}$ is in $\mathbb{N}^{\mathbb{N}}$ and the fifth and sixth components of $\Omega^{*}$ take values in $\mathbb{N}$ (this will be relevant for the calibration of the exact level of recursion that is needed to define these objects). Again, the only functional which we will use later is $\Psi^{*}$, the rest of them only serve to define it.

[TABLE]

where $\max$ for tuples is understood componentwise. Now we begin the most intricate portion of the majorization procedure, namely the treatment of the functions defined in the final part of the previous section. We make some remarks in order to convince the reader of the plausibility of the solution given below. First of all, since $\varphi$ yields a sequence which is bounded by $b$, it is trivially majorized, so we may omit it, like before with the $P$. In that same vein, we may omit some parameters if the majorant does not actually depend on them. For example, a majorant for $g^{\prime}_{0}$ will now no longer depend on $\underline{w}$, and moreover it can be replaced by the same majorant as for $g_{0}$, provided that $\underline{w}^{*}$ and $k^{*}$ are replaced in applications by $\underline{w}^{\prime*}$ and $k^{\prime*}$. A case distinction may be replaced by a (pointwise) maximum (the verification is as immediate as for the recursion example given before), whereas when majorizing small real numbers $\delta>0$ the maximum is, obviously, replaced by a minimum. For all undefined quantities below, see sub-section 5.2.2, as well as the notations introduced before the statement of Claim II in Section 4.

[TABLE]

[TABLE]

We now majorize the functionals appearing in the proof of Proposition 5.3. First, we treat the arithmetical shuffling stage.

[TABLE]

[TABLE]

[TABLE]

[TABLE]

Finally, we may treat the purely logical stage, where taking the maximum replaces the case distinctions. What we need to take care of is that the instance of $(g^{*}_{0},f^{*}_{0})$ majorizing $(g^{\prime}_{0},f^{\prime}_{0})$ is applied to its proper arguments, namely (here) $\underline{q}^{*}_{3-4}$.

[TABLE]

As before, one obtains the final bound of

[TABLE]

which, taking care of the dependencies in the formula just produced, we may denote as

[TABLE]

This, however, is not a rate of metastability in the sense that the notion was defined in the Introduction, but it may be easily converted into one. We remark that (suppressing the indices) $\Theta^{\prime}$ depends on the $g$ only via $g^{M}$ and, moreover, the only property of $g^{M}$ that is used is that it is a majorant for $g$. Therefore, for any $h$ such that for any $n$, $h(n)\leq g(n)$, since then $g^{M}$ is also a majorant for $h$, $\Theta^{\prime}(\varepsilon,g)$ is a bound on the (least) $N$ such that $\|x_{N}-x_{N+h(N)}\|\leq\varepsilon$. The uniformity of the bound having been already taken care of, we may allow the $h$ to depend on the sequence itself, and so

[TABLE]

is a valid choice (note that this $h$ can be made constructive by using suitable rational approximations). We may then simply put

[TABLE]

to obtain our main result, which is expressed as follows.

Theorem 6.1**.**

Let $X$ be a Banach space which is uniformly convex with modulus $\eta$ and uniformly smooth with modulus $\tau$. Let $C\subseteq X$ a closed, convex, nonempty subset. Let $b\in\mathbb{N}^{*}$ be such that for all $y\in C$, $\|y\|\leq b$ and the diameter of $C$ is bounded by $b$. Let $T:C\to C$ be a pseudocontraction that is uniformly continuous with modulus $\theta$ and $x\in C$. For all $t\in(0,1)$ put $x_{t}$ to be the unique point in $C$ such that $x_{t}=tTx_{t}+(1-t)x$. Let $(t_{n})\subseteq(0,1)$, $\alpha:\mathbb{N}\to\mathbb{N}$ and $\gamma:\mathbb{N}\to\mathbb{N}^{*}$ be such that:

• •

for all $n$ and all $m\geq\alpha(n)$, $t_{m}\geq 1-\frac{1}{n+1}$;

• •

for all $n$, $t_{n}\leq 1-\frac{1}{\gamma(n)}$.

Denote, for all $n$, $x_{n}:=x_{t_{n}}$. Then, for all $\varepsilon>0$ and $g:\mathbb{N}\to\mathbb{N}$ there is an $N\leq\Theta_{b,\eta,\tau,\theta,\alpha,\gamma}(\varepsilon,g)$ such that for all $m,n\in[N,N+g(N)]$, $\|x_{m}-x_{n}\|\leq\varepsilon.$

Thus, we have obtained a rate of metastability which is definable in the subsystem of $T$ containing at most type two recursion, which we denote by $T_{2}$. Note that in order for our bound to be properly said to be defined in that calculus, one must take care that only natural numbers and functionals thereof are used in the definition. The most prominent examples of this sort are that one cannot work with an $\varepsilon>0$ and must instead use a natural approximation $k$ standing for $\varepsilon:=\frac{1}{k+1}$, and also that the moduli of convexity, smoothness and continuity must also operate with and return natural numbers having this interpretation. This is straightforward to arrange (see also the metatheorems in [40, 46] which use the respective moduli in this form).

A closer look at the bound shows that type two recursion is only used in the definition of $(M^{*},U^{*})$ needed in defining $\Psi^{*}$ because of the argument $L^{*}$ which is in turn used by $\Omega^{*}$ . The concrete instances of $\Omega^{*}$ to which $\Psi^{*}$ is applied in the final stage, however, do not depend on that parameter, as it may be gleamed from a very careful examination. To see this, it is crucial to note that the functionals $(U^{*}_{i},M^{*}_{i})$ do not depend on the fifth components of $\underline{w}^{*},\underline{v}^{*}$ which play the role of $L^{*}.$ (That these functionals depend neither on the third nor the fourth component of $\underline{w}^{*},\underline{v}^{*}$ is not surprising since these can be easily majorized in terms of $b$ and $b/\varepsilon$ for the respective error $\varepsilon$ which corresponds to the definition of the first and second components of the $g^{*}_{i}$’s.) Therefore one may replace that recursion by a (simpler) type one recursion111On the other hand, in the applications of $\Psi$ that were used to obtain the actual realizer, the parameter $L$ played a nondisposable role in the case distinction, but one can also make the remark that $L$ cannot play another role because in the proof of Lemma 5.5, the corresponding ‘$\geq$’ statements within the $A$’s were never used.. Note also that the primitive recursion of ${\widetilde{\Psi}}^{*}$ actually only concerns the components 3-6 (the first two ones have constant values) which are of types $\mathbb{N}$, $\mathbb{N}$, $\mathbb{N}^{\mathbb{N}}$ and $\mathbb{N}$ – so that this is a recursion of type $\mathbb{N}^{\mathbb{N}}$. Actually, using again that the $\Omega^{*}_{1-4}$’s to which this recursion is applied do not depend on the type $\mathbb{N}^{\mathbb{N}}$ component $\tilde{\Psi}^{*}_{5}$ of $\tilde{\Psi}^{*}$, one can see that in the case at hand it reduces to a recursion of type $\mathbb{N}$. We also remark, that in the situation at hand, the functional $M^{*}$ (and hence $\overline{M}^{*}$) actually is constantly [math] since the respective $\Omega^{*}_{5}$ functionals, namely the fifth components of the $g^{*}_{i}$’s, are [math].

Corollary 6.2**.**

The bound $\Theta_{b,\eta,\tau,\theta,\alpha,\gamma}(1/(k+1),g),$ providing a rate of metastability for the resolvents of continuous pseudocontractive operators in Banach spaces which are uniformly convex and uniformly smooth, is definable in $T_{1}$ as a functional in the parameters $b$, $\eta$, $\tau$, $\theta$, $\alpha$, $\gamma$, $k$, $g$.

Remark 6.3**.**

A detailed analysis of the structure of our rate of metastability might actually reveal – in line with Lemma 4 in [57] – that the remaining type-1 recursions (to define $N^{*},T^{*}$ and $U^{*}$) are applied to type-2 functionals which are so simple (w.r.t. their dependence on the function argument) that our bound could be defined already in $T_{0}.$ We have to leave this for future research.

Remark 6.4**.**

In the special case where the mapping is nonexpansive and has a fixed point, we may trivially remove the boundedness condition as follows: let $G\subseteq X$ a closed, convex, nonempty subset. Let $U:G\to G$ be nonexpansive with a fixed point $p$ and $x\in G$. Let $b\in\mathbb{N}^{*}$ be such that $\|x-p\|\leq b/2$ and $\|p\|\leq b/2$. For all $t\in(0,1)$ put $x_{t}$ to be the unique point in $G$ such that $x_{t}=tUx_{t}+(1-t)x$. Let $(t_{n})$, $\alpha$, $\gamma$ be as before. Denote, for all $n$, $x_{n}:=x_{t_{n}}$. Then, for all $\varepsilon>0$ and $g:\mathbb{N}\to\mathbb{N}$ there is an $N\leq\Theta_{b,\eta,\tau,\text{\rm id},\alpha,\gamma}(\varepsilon,g)$ such that for all $m,n\in[N,N+g(N)]$, $\|x_{m}-x_{n}\|\leq\varepsilon.$ To see this, put $C$ to be the intersection of $G$ with the closed ball centred on $p$ with radius $b/2$. Clearly $C$ is closed, convex and nonempty. Set $T$ to be $U$ restricted to $C$, whose image is by nonexpansiveness also in $C$. Clearly, the diameter of $C$ is bounded by $b$, all elements of $C$ are bounded by $b$ and $x\in C$, so we may apply Theorem 6.1.

We now argue that the quantitative metastability of the sequence $(x_{t_{n}})$ is indeed a finitization in the sense of Tao of the following theorem (which is a somewhat restricted form of the main result in [60]).

Theorem 6.5** ([60]).**

Let $X$ be a Banach space which is uniformly convex and uniformly smooth, $C\subseteq X$ a closed, convex, bounded, nonempty subset, $T:C\to C$ be a uniformly continuous pseudocontraction and $x\in C$. For all $t\in(0,1)$ put $x_{t}$ to be the unique point in $C$ such that $x_{t}=tTx_{t}+(1-t)x$. Then for all $(t_{n})\subseteq(0,1)$ such that $\lim\limits_{n\to\infty}t_{n}=1$ we have that $(x_{t_{n}})$ converges to a fixed point of $T$, which we denote by $Qx$. In addition, the map $Q:C\to Fix(T)$ thus defined is a sunny nonexpansive retraction (and therefore the unique such one).

For this we now show that the metastability of $(x_{t_{n}})$ implies in an elementary way the above theorem: using just logic (and quantifier-free choice from $\mathbb{N}$ to $\mathbb{N}$) the metastability of $(x_{t_{n}})$ implies that $(x_{t_{n}})$ is Cauchy, and therefore, since $X$ is complete and $C$ is closed, it is convergent (in the context of reverse mathematics, the latter fact uses arithmetical comprehension – in fact a single use of $\Pi^{0}_{1}$-comprehension – to get a fast converging subsequence as required to obtain the actual limit). It is clear that the limit does not depend on the $(t_{n})$, so we can unambiguously dub it $Qx$. For the rest of the proof, we fix a $(t_{n})$ and denote, for all $n$, $x_{n}:=x_{t_{n}}$. That $Qx$ is a fixed point follows from the continuity of $T$ and the fact (proven already in the beginning off Section 3) that

[TABLE]

whose trivial proof we recall here:

[TABLE]

If $x$ is already a fixed point, then clearly for all $n$, $x_{n}=x$ and therefore $Qx=x$. We have thus shown that $Q$ is a retraction. To show that $Q$ is sunny and nonexpansive, we seek to apply Proposition 2.16. Let $p\in Fix(T)$. Then

[TABLE]

Now we reuse parts of the argument from Claim 3 in the last proof from Section 3. We have that

[TABLE]

so

[TABLE]

and therefore, using that $j$ is homogeneous,

[TABLE]

By passing to the limit, using the continuity of $j$, we get that

[TABLE]

which is what we needed to show.

Remark 6.6** (for logicians; we use the terminology from [40]).**

As mentioned already, the proof of the metastability of $(x_{t_{n}})$ in Section 4 shows that it can be carried out in the formal system WE-PA${}^{\omega}[X,\|\cdot\|,\eta,J_{X},\omega_{X},C].$ Note that the noneffective definition of the function $s_{p,g}$ can easily be avoided by using suitable rational approximations of $\|x_{n+g(n)}-p\|$ and $\|x_{n}-p\|.$ From this, the proof above of the convergence of $(x_{t_{n}})$ only requires classical logic, a fixed (in the parameters $T$, $x$, $(t_{n})$ needed to define $(\|x_{t_{n}}\|)$) sequence QF-AC${}^{0,0}_{-}$ of instances of QF-AC0,0 (in the terminology of reverse mathematics: $\Delta^{0}_{1}$-CA) and (a single use of) $\Pi^{0}_{1}$-CA. Both QF-AC0,0 and $\Pi^{0}_{1}$-CA can (with classical logic) be combined into $\Pi^{0}_{1}$-AC${}^{0,0}.$

Let us now specify the amount of classical logic needed when using the intuitionistically unproblematic principle AC${}^{0,0}.$ By applying negative translation to the above proof of the Cauchyness of $(x_{t_{n}})$ we obtain in WE-HA${}^{\omega}[X,\|\cdot\|,\eta,J_{X},\omega_{X},C]+$QF-AC${}^{0,0}_{-}+$M${}^{0}_{-}$

[TABLE]

(here M0 denotes the Markov principle for numbers). Hence,

[TABLE]

(which also covers M0) suffices. Using the closure of WE-HA${}^{\omega}[X,\|\cdot\|,\eta,J_{X},\omega_{X},C]+$AC${}^{0,0}+\Sigma^{0}_{1}$-LEM under the rule of $\Sigma^{0}_{2}$-DNE (proven similarly as in [47, Section 3]) one can conclude that even (a fixed – in the parameters mentioned – sequence $\Sigma^{0}_{1}$-LEM- of instances of)

[TABLE]

suffices (when added to WE-HA${}^{\omega}[X,\|\cdot\|,\eta,J_{X},\omega_{X},C]+$AC${}^{0,0}_{-}$) to prove the Cauchyness and – in turn – the convergence of $(x_{t_{n}})$ and the variational inequality (characterizing sunny nonexpansive retractions) from Proposition 2.16.

7 Applications

The convergence of the resolvents, which form an implicit iteration schema, plays a role in proving the strong convergence of some explicit iteration schemas designed to compute fixed points of some nonlinear operators.

One such schema is the Halpern iteration [33]. If $T:C\to C$ is a mapping, $x$, $u\in C$ and $(\lambda_{n})\subseteq(0,1)$, the Halpern iteration corresponding to this data is the sequence $(x_{n})$, defined by:

[TABLE]

The convergence of this sequence for nonexpansive self-mappings of closed convex bounded nonempty subsets $C$ of uniformly smooth Banach spaces was obtained by Shioji and Takahashi [62] under Wittmann’s [67] conditions on $(\lambda_{n})$ and analyzed from the point of view of proof mining by the first author and Leuştean [46], modulo the resolvent convergence. We are now in a position to complete this analysis under the additional hypothesis that $X$ is uniformly convex.

Theorem 7.1** (cf. [46, Theorem 3.2]).**

Let $X$ be a Banach space which is uniformly convex with modulus $\eta$ and uniformly smooth with modulus $\tau$. Let $C\subseteq X$ a closed, convex, nonempty subset. Let $b\in\mathbb{N}^{*}$ be such that for all $x\in C$, $\|x\|\leq b$ and the diameter of $C$ is bounded by $b$. Let $T:C\to C$ be a nonexpansive mapping and $x$, $u\in C$. Put $\theta:=\mathrm{id}_{\mathbb{N}}$ and put $\alpha$ and $\gamma$ to be the functions defined, for all $n$, by $\alpha(n):=n$ and $\gamma(n):=n+1$. Let $(\lambda_{n})\subseteq(0,1)$ be such that:

• •

$\sum_{n=0}^{\infty}\lambda_{n}=\infty$* with rate of divergence $\beta_{1}$;*

• •

$\lim_{n\to\infty}\lambda_{n}=0$* with rate of convergence $\beta_{2}$;*

• •

$\sum_{n=0}^{\infty}|\lambda_{n+1}-\lambda_{n}|<\infty$* with Cauchy modulus $\beta_{3}$.*

Denote by $(x_{n})$ the Halpern iteration corresponding to this data. Let $\Sigma$ be defined by [46, Theorem 3.2]. Then, for all $\varepsilon\in(0,2)$ and $g:\mathbb{N}\to\mathbb{N}$ there is an $N\leq\Sigma(\varepsilon,\omega_{\tau},g,b,\Theta_{b,\eta,\tau,\theta,\alpha,\gamma},\beta_{1},\beta_{2},\beta_{3})$ such that for all $m,n\in[N,N+g(N)]$, $\|x_{m}-x_{n}\|\leq\varepsilon.$

An explicit iteration schema that is in addition amenable to pseudocontractions is the Bruck iteration [15]. If $T:C\to C$ is a mapping, $x\in C$ and $(\lambda_{n})$, $(\theta_{n})\subseteq(0,1)$ such that for all $n$, $\lambda_{n}(1+\theta_{n})\leq 1$, the Bruck iteration corresponding to this data is the sequence $(x_{n})$, defined by:

[TABLE]

The convergence of this sequence in some general framework containing the case of Lipschitzian pseudocontractive self-mappings of closed convex bounded nonempty subsets $C$ of uniformly convex and smooth Banach spaces was obtained by Chidume and Zegeye [18] under some conditions on $(\lambda_{n})$ and $(\theta_{n})$ and then analyzed from the point of view of proof mining by Körnlein and the first author [49], again modulo the resolvent convergence. We now complete their analysis.

Theorem 7.2** (cf. [49, Corollary 2.10]).**

Let $X$ be a Banach space which is uniformly convex with modulus $\eta$ and uniformly smooth with modulus $\tau$. Let $C\subseteq X$ a closed, convex, nonempty subset. Let $b\in\mathbb{N}^{*}$ be such that for all $x\in C$, $\|x\|\leq b$ and the diameter of $C$ is bounded by $b$. Let $T:C\to C$ be a Lipschitzian pseudocontraction of constant $L$ and $x\in C$. Let $(\lambda_{n})$, $(\theta_{n})\subseteq(0,1)$ satisfy the Chidume-Zegeye conditions. Denote by $(x_{n})$ the Bruck iteration corresponding to this data. Let $\chi$, $h$, $g^{\prime}$ and $\Psi$ be defined as in [49]. Put $\theta$ to be multiplication by $L$ and for all $n$, $\gamma(n):=h(n)+1$. Then, for all $\varepsilon\in(0,2)$ and $g:\mathbb{N}\to\mathbb{N}$ there is an $N\leq\chi^{M}\left(\Theta_{b,\eta,\tau,\theta,\chi,\gamma}\left(\frac{\varepsilon}{2},g^{\prime}\right)\right)+\Psi(\varepsilon)+1$ such that for all $m,n\in[N,N+g(N)]$, $\|x_{m}-x_{n}\|\leq\varepsilon$ and for all $\l\geq N$, $\|x_{l}-Tx_{l}\|\leq\varepsilon$.

Proof.

The only issue that needs additional justification is that $\chi$ and $\gamma$ are the required moduli for the auxiliary sequence $t_{n}=1/(1+\theta_{n})$ used in the original relative metastability proof. This is shown in the first lines of the proof of [49, Theorem 2.8]. ∎

Another application of the rate of metastability extracted in this paper is given in [44], where it is used to construct a rate of metastability for the strongly convergent Halpern-type Proximal Point Algorithm in uniformly convex and uniformly smooth Banach spaces from [4].

8 Acknowledgements

The authors have been supported by the German Science Foundation (DFG Project KO 1737/6-1).