Effective asymptotic regularity for one-parameter nonexpansive semigroups (Q499259)

The paper under discussion contains a case study of ``proof mining'', an applied subfield of mathematical logic. The idea of proof mining was first suggested by G. Kreisel in the 1950s (under the name ``unwinding of proofs''; the current name is due to D. Scott) as a way to use the results of proof theory in order to extract new (primarily quantitative) information from concrete mathematical proofs. The current, mature incarnation of the field was developed by U. Kohlenbach (which is the first author of this paper) and his collaborators in the 1990s, but mainly in the 2000s, when significant results were obtained by applying proof-theoretical methods to diverse mathematical areas like nonlinear analysis and ergodic theory. Here, the two authors analyse the following result of \textit{T. Suzuki} [Bull. Lond. Math. Soc. 38, No. 6, 1009--1018 (2006; Zbl 1116.47050)]: if \(E\) is a Banach space, \(C\) is a subset of \(E\) and \((T_t)_{t \geq 0}\) is a nonexpansive semigroup on \(C\), then, for any \(\alpha\), \(\beta \in \mathbb{R}_+\) (with \(\beta \neq 0\)) such that \(\frac\alpha\beta\) is irrational, and any \(\lambda \in (0,1)\), we have that \[ \bigcap_{t \geq 0} \mathrm{Fix}(T(t)) = \mathrm{Fix}(\lambda T(\alpha) + (1-\lambda)T(\beta)), \] where for any \(U\), one denotes by \(\mathrm{Fix}(U)\) the fixed point set of \(U\). The left-to-right inclusion in the above is trivial; it is the right-to-left one that concerns the authors. Namely, this is because it may be written as: \[ \begin{aligned} \forall q \in C\;\forall m \in \mathbb{N}\;\forall t \geq 0\;\exists k \in \mathbb{N}\\ (\|(\lambda T(\alpha)+ (1-\lambda)T(\beta))q -q\| \leq 2^{-k} \to \|T(t)q-q\|<2^{-m}),\end{aligned} \] which is a \(\forall\exists\)-statement, and therefore is amenable to the techniques of proof mining with the goal of producing a witnessing function -- that is, a formula for the \(k\) in terms of \(m\) and perhaps some other parameters of the problem. The bulk of the paper focuses on finding and proving the validity of such a witnessing function. As it is generally done in proof mining, the resulting proof is obtained by applying a `proof interpretation' (usually a variant of Gödel's Dialectica) to the original one, while taking care along the way of the parameters that are seen to be necessary to the final witness. Here, the most significant one is the so-called `effective irrationality measure' of a positive irrational number \(\gamma\) (here, the ratio \(\alpha/\beta\)), i.e. a function \(f: \mathbb{N} \to \mathbb{N}\) such that for any \(p \in \mathbb{N}\) and \(q \in \mathbb{N}^*\), one has that \[ \left( \left| \gamma - \frac p q \right| \geq \frac1{f(q)} \right). \] It is of this special parameter, rather than on the numbers \(\alpha\) and \(\beta\) themselves, that the witnessing function to be constructed ultimately is shown to depend upon. The authors conclude their paper by presenting some immediate applications of their result, e.g. rates of asymptotic regularity.