On the reverse mathematics and Weihrauch complexity of moduli of regularity and uniqueness

Abstract

The notion of ‘modulus of regularity’, as recently studied in [Moduli of regularity and rates of convergence for Fejér monotone sequences, 2017, Preprint], unifies a number of different concepts used in convex optimization to establish rates of convergence for Fejér monotone iterative procedures. It generalizes the notion of ‘modulus of uniqueness’ to the nonunique case. In this paper, we investigate both notions in terms of reverse mathematics and calibrate their Weihrauch complexity.

Keywords

Moduli of regularity moduli of uniqueness reverse mathematics Weihrauch complexity convex optimization

1. Introduction

In [19], the concept of modulus of regularity is introduced as a central tool to construct rates of convergence for classes of Fejér monotone sequences which appear in fixed point theory, monotone operator theory and convex optimization. The concept of modulus of regularity gives a unified account of various notions such as metric subregularity [10,21,22], Hölder regularity [4], error bounds [21] and weak sharp minima [9] which play a prominent role in nonlinear optimization. It is general enough to cover many equilibrium, convex feasibility, fixed point and minimization problems involving set-valued operators.

In the case where the solution in question is unique, the concept coincides with the notion of modulus of uniqueness [13,18,19] and can be understood as its generalization to the nonunique case.

While most problems in nonlinear analysis deal with classes of abstract, in general not necessarily separable, metric or normed structures, we restrict ourselves in this paper to the compact metric case. In this situation a modulus of regularity always exists for continuous functions F ([19], Proposition 3.2) and the concept has been anticipated already in [1]. We calibrate the strength of its existence in the sense of reverse mathematics as well as its Weihrauch complexity and compare this with the case of a modulus of (uniform) uniqueness in the unique case. We also consider the weaker $\forall ε \exists δ$ -version of regularity (without stating the existence of a modulus function) and show that in this form, regularity is equivalent to ${WKL}_{0}$ while the existence of a modulus is equivalent to ${ACA}_{0}$ . This differs from the unique case where both the $\forall ε \exists δ$ -form as well as the modulus version of uniform uniqueness are equivalent to ${WKL}_{0}$ . The difference also shows up in the Weihrauch complexity: the many-valued modulus-of-uniqueness operator MUNI is computable while the many-valued modulus-of-regularity operator MREG is Weihrauch equivalent to $\hat{LPO}$ . Both phenomena are due to the fact that the proof for the $\forall ε \exists δ$ -form of regularity already makes substantial use of classical logic ( $Σ_{1}^{0} -LEM = Π_{1}^{0} -LEM + M$ , where M denotes the Markov principle) while in the unique case only M is used.1

¹
The latter is already implicit in [13] and [3] since to convert uniform uniqueness to prenex form as in [13], resp. reformulating it in the strong form stated on p. 714 in [3], just amounts to applying M.

2. Moduli of regularity and uniqueness

Definition 2.1 ([19]).

Let $(X, d)$ be a metric space and let be $F : X \to R$ a mapping. Let $zer F : = {x \in X : F (x) = 0} \neq \emptyset$ and $r > 0$ . We say that F is regular w.r.t. $zer F$ and $\overline{B} (z, r)$ for $z \in zer F$ if $\begin{matrix} \forall n \in N \exists k \in N \forall x \in \overline{B} (z, r) (| F (x) | < 2^{- k} \to \exists z^{'} \in zer F (d (x, z^{'}) < 2^{- n})) . \end{matrix}$ If this holds with ‘ $\forall x \in \overline{B} (z, r)$ ’ replaced by ‘ $\forall x \in X$ ’ we say that F is regular w.r.t. $zer F$ .

A function $f : N \to N$ providing given n a number $k = f (n)$ satisfying the above is called a modulus of regularity of F w.r.t. $zer F$ and $\overline{B} (z, r)$ resp. w.r.t. $zer F$ .

Remark 2.2.

In [19] the conclusion ‘ $\exists z^{'} \in zer F (d (x, z^{'}) < 2^{- n})$ ’ is conveniently written using the metric distance functions as ‘ $dist (x, zer F) < 2^{- n}$ ’ but, of course, the concept does not presuppose the existence of ‘dist’, i.e. the locatedness of $zer F$ .

Again for convenience and to follow the style used in analysis, the concept of a modulus of regularity in [19] is written in $ε / δ$ -form, i.e. as a function $: (0, \infty) \to (0, \infty)$ . All results can be, however, easily re-casted in terms of the modulus $f : N \to N$ as defined above which is more appropriate for the context of reverse mathematics and Weihrauch reducibility.

When $zer F$ is not a singleton set, effective moduli of regularity can only be expected to exist in rather restricted situations (due to their strong consequences on rates of convergence for numerous iterative procedures used in nonlinear analysis). However, [19] describes important cases where such moduli can be explicitly computed.

The concept of modulus of regularity generalizes that of a ‘modulus of uniqueness’ to the nonunique case:
Definition 2.3 ([13,18,19]).

Let $F : X \to R$ be such that $zer F = {z}$ .

We say that $zer F$ is uniformly unique w.r.t. $\overline{B} (z, r)$ if $\begin{matrix} \forall n \in N \exists k \in N \forall x \in \overline{B} (z, r) (| F (x) | < 2^{- k} \to d (x, z) < 2^{- n}) . \end{matrix}$ If this holds with ‘ $\forall x \in X$ ’ we say that $zer F$ is uniformly unique.

$ω : N \to N$ is a modulus of uniqueness for F w.r.t. $zer F$ and $\overline{B} (z, r)$ for $z \in zer F$ if $\begin{matrix} \forall n \in N \forall x \in \overline{B} (z, r) (| F (x) | < 2^{- ω (n)} \to d (x, z) < 2^{- n}) . \end{matrix}$ If this holds with ‘ $\forall x \in X$ ’ we say that ω is a modulus of uniqueness for F w.r.t. $zer F$ .

The concept of modulus of uniqueness can also be considered without assuming that $zer F \neq \emptyset$ in the form $\begin{matrix} (*) & \forall n \in N \forall x, y \in X (| F (x) |, | F (y) | < 2^{- ω (n)} \to d (x, y) < 2^{- n}) . \end{matrix}$ Clearly, if $zer F = {z}$ , then any ω with (∗) is a modulus of uniqueness in the sense of definition 2.3 and conversely, if ω is a modulus of uniqueness, then $ω^{'} (n) : = ω (n + 1)$ satisfies (∗). Suppose that one has an algorithmic way $(x_{n})$ to construct $2^{- n}$ -approximate zeros $x_{n}$ , i.e. $| F (x_{n}) | < 2^{- n}$ of F and ω satisfies (∗), then $(x_{ω (2^{- n})})$ is a $2^{- n}$ -Cauchy sequence whose limit (for complete X and continuous F) is a zero of F. In this way, moduli of uniqueness give rates of convergence for algorithms computing approximate solutions towards the actual solution and have been used in fixed point theory to prove even new existence results (see [7] and the literature cited there). As shown in [13] (for the case of compact metric spaces), explicit moduli of uniqueness can be extracted by proof-theoretic methods from given, even nonconstructive, proofs for the uniqueness of the zero of F. This has been carried out in the context of best Chebycheff approximation in [13 ,14] and best $L^{1}$ -approximation in [20] (see [18] for a comprehensive treatment of all this). Using the logical bound extraction theorems for abstract metric and normed structures (without separability or compactness assumptions) from [12,17] such extractions of moduli of uniqueness are also possible for abstract spaces in the absence of compactness (see [18], pp. 377–381) and have been used in metric fixed point theory e.g. in [7,11].

While the existence of a modulus of uniqueness is a uniform quantitative version of the plain uniqueness property $\begin{matrix} (1) & F (x) = 0 = F (z) \to x = z \end{matrix}$ and can be extracted from a given proof of the latter, the existence of a modulus of regularity is a uniform quantitative version of the following trivially true (but logically more complex than (1)) property: $\begin{matrix} (2) & F (x) = 0 \to \forall ε > 0 \exists z \in zer F (d (x, z) < ε) . \end{matrix}$ So in this generality, there is no meaningful property such that from a proof of this property a modulus of regularity can be extracted. Thus unless one is in the unique case (where the concept of a modulus of regularity coincides with that of modulus of uniqueness), one has to exploit rather specific features of the situation at hand in order to get an effective modulus of regularity (see also the comments in the introduction and [19]).

3. Reverse mathematics

In the following, ${RCA}_{0}$ is the usual base system used in reverse mathematics, i.e. the fragment of second order arithmetic with recursive $(Δ_{1}^{0})$ comprehension and $Σ_{1}^{0}$ -induction only. ${WKL}_{0}$ and ${ACA}_{0}$ are its extension by the weak König’s lemma WKL for $0 / 1$ -trees and the schema of arithmetic comprehension ACA, respectively. For details we refer to [25].

We refer to the definition of compact metric spaces X as used in reverse mathematics ([25], Definition III.2.3), where X is given as the completion $\hat{A}$ of a countable pseudometric space A which, additionally, possesses a sequence of finite ε-nets. We recall some crucial results from [25]:

Theorem 3.1 ([25], Theorem IV.1.6).

The following is provable in ${WKL}_{0}$ . Let X be a compact metric space. Let $⟨ ⟨ U_{n, k} : k \in N ⟩ : n \in N ⟩$ be a sequence of coverings of X by open sets. Then there exists a sequence of finite subcoverings $⟨ ⟨ U_{n, k} : k ⩽ l_{n} ⟩ : n \in N ⟩$ .

Theorem 3.2 ([25], Theorem IV.1.7).

The following is provable in ${WKL}_{0}$ . Let X be a compact metric space. Let C be a code for a closed subset in X. Then the nonemptyness of C can be expressed by a $Π_{1}^{0}$ -formula.

Proposition 3.3 ([25], Exercise II.6.9, [8], Lemma 1.24).

The following is provable in ${RCA}_{0}$ . Let X, Y be complete separable metric spaces and $Φ : X \to Y$ a continuous function. Let $V \subseteq Y$ be (a code of) an open set, then $Φ^{- 1} (V)$ is open (with a code computable from a code for V).

Corollary 3.4.
The following is probable in ${WKL}_{0}$ . Let X be a compact space and $F : X \to R$ be continuous, then the property that F has a zero on X can be expressed by a $Π_{1}^{0}$ -formula.
Proof.
Clearly, ${RCA}_{0}$ proves that $R ∖ {0}$ is open. Hence by Proposition 3.3, ${x \in X : F (x) \neq 0}$ has a code as an open set and so $zer F = {x \in X : F (x) = 0}$ has a code as a closed set. So by Theorem 3.2, provably in ${WKL}_{0}$ , the nonemptyness of $zer F$ can be expressed by a $Π_{1}^{0}$ -formula. □
Remark 3.5.
The proofs of the results above establish that even if we have sequences $⟨ Φ_{n} : n \in N ⟩$ and $⟨ F_{n} : n \in N ⟩$ uniformly given as sequences of codes that then ${RCA}_{0}$ proves that $⟨ Φ_{n}^{- 1} (V) : n \in N ⟩$ is a sequence of open sets and ${WKL}_{0}$ proves that the nonemptyness of $zer F_{n}$ can expressed as a $Π_{1}^{0}$ -formula with n as parameter. The latter is particularly easy to see in our instances below, where the functions $Φ_{n}$ are defined in terms of a single function Φ and any modulus of uniform continuity for Φ can be modified into one for all $Φ_{n}$ uniformly in n (see also the explicit construction of the $Π_{1}^{0}$ -formula in the proof of Lemma 5.5 below).

4. Reverse mathematics of moduli of uniqueness and regularity

Theorem 4.1.

${WKL}_{0}$ proves that for every compact metric space $X = \hat{A}$ any continuous mapping $F : X \to R$ having at most one zero has a modulus ω such that $\begin{matrix} \forall n \in N \forall x, y \in X (| F (x) |, | F (y) | < 2^{- ω (n)} \to d (x, y) < 2^{- n}) . \end{matrix}$ Obviously, if $zer F = {z}$ , then ω is a modulus of uniqueness of F w.r.t. $zer F$ .

Already for Lipschitz continuous functions $F : [0, 1] \to R$ which have exactly one zero, the uniform uniqueness of the zero implies ${WKL}_{0}$ over ${RCA}_{0}$ .

Proof.
1) Let F possess at most one zero and define $\begin{matrix} U_{n, k} : = {(x, y) \in X \times X : | F (x) |, | F (y) | ⩽ 2^{- k} \to d (x, y) < 2^{- n}} . \end{matrix}$ $⟨ ⟨ U_{n, k} : k \in N ⟩ : n \in N ⟩$ is a sequence of coverings of $X \times X$ (w.r.t. the product metric, [25], Example II.5.4) by open sets. Here one uses Proposition 3.3 and the fact that for the continuous functions $\begin{matrix} G_{n, k} (x, y) : = max {max {| F (x) |, | F (y) |} - 2^{- k}, 2^{- n} - d (x, y), 0} \end{matrix}$ one has $\begin{matrix} (x, y) \in U_{n, k} \leftrightarrow (x, y) \notin {(G_{n, k})}^{- 1} ({0}) . \end{matrix}$ By Theorem 3.1 it follows that, provably in ${WKL}_{0}$ , there is a sequence $⟨ ⟨ U_{n, k} : k ⩽ α (n) ⟩ : n \in N ⟩$ of finite subcoverings. Clearly, $α : N \to N$ is a modulus of uniqueness.

2) Assume ¬-WKL. Then there exists an infinite $0 / 1$ -tree T with no path. Consider the subtrees $T_{0}$ and $T_{1}$ of T consisting of all finite $0 / 1$ -sequences in T which start with 0 or which start with 1 resp. One of those subtrees must be infinite as well. W.l.o.g. assume that $T_{0}$ is infinite. Define $T [1]$ as $T_{0}$ augmented by the constant-1 path. With this $T [1]$ (playing the role of T) now define as in [25] (p. 129) a sequence $⟨ I_{n} = (r_{n}, s_{n}) : n \in N ⟩$ of nonempty open intervals with rational endpoints. Adapting the reasoning there to our situation (using that $b_{s}^{'} ⩽ 2 / 3$ for $s \in 2^{< N}$ with $lh (s) ⩾ 1$ and $s (0) = 0$ ) one gets $\begin{matrix} (i) \forall x \in [0, 1) \exists n \in N (x \in I_{n}), (ii) \forall k \in N \exists x \in [0, 2 / 3] \forall i ⩽ k (x \notin I_{i}), (iii) \forall n \in N (1 \notin I_{n}) . \end{matrix}$ Now we define (see [28], p.309): $\begin{matrix} F : [0, 1] \to [0, 1], F (x) : = \sum_{n = 0}^{\infty} 2^{- n - 1} F_{n} (x), \end{matrix}$ where $\begin{matrix} F_{n} (x) : = max {0, \frac{1}{2} (s_{n} - r_{n}) - | x - \frac{1}{2} (r_{n} + s_{n}) |} . \end{matrix}$ Then, clearly, $\forall x \in [0, 1)$ ( $F (x) > 0$ ) by (i), ${inf}_{x \in [0, 2 / 3]} F (x) = 0$ by (ii), and $F (1) = 0$ by (iii). F is nonexpansive but obviously is not uniformly unique w.r.t. $zer F = {1}$ .2
²
Alternatively, we could have modified the mapping $Φ_{5}$ in the proof of Theorem IV.2.3.5 in [25] by using ‘ $1 - 3^{- lh (u)}$ ’ instead of ‘ $1 - 2^{- lh (u)}$ ’ to achieve the Lipschitz property. However, we find the construction above more elementary. One can also adapt Specker’s [27] construction or the Lipschitz functions defined in [2].

□
Theorem 4.2.

${WKL}_{0}$ proves that for every compact metric space $X = \hat{A}$ any continuous mapping $F : X \to R$ having a zero is regular w.r.t. $zer F$ .

Already for Lipschitz continuous functions $F : [0, 1] \to R$ with $zer F \neq \emptyset$ , the regularity of F w.r.t. $zer F$ implies ${WKL}_{0}$ over ${RCA}_{0}$ .

Proof.
1) Take $k \in N$ and consider the finite cover of X by closed balls $\overline{B} (a_{1}, 2^{- k - 1}), \dots, \overline{B} (a_{n_{k}}, 2^{- k - 1})$ provided by the representation of X as a compact metric space (in the sense of [25], Definition III.2.3), where $a_{1}, \dots, a_{n_{k}}$ are in the countable set A whose completion $\hat{A}$ the space X is defined to be. Using ${WKL}_{0}$ , the predicate $\begin{matrix} P (i) : \equiv \exists x \in X (d (a_{i}, x) ⩽ 2^{- k - 1} \land F (x) = 0) (1 ⩽ i ⩽ n_{k}) \end{matrix}$ is in $Π_{1}^{0}$ . Here we use that $P (i)$ can be written as $\exists x \in X (G_{i} (x) = 0)$ for the continuous function $G_{i} : X \to R$ defined by $\begin{matrix} G_{i} (x) : = max {| F (x) |, max {2^{- k - 1}, d (a_{i}, x)} - 2^{- k - 1}} ⩾ 0 \end{matrix}$ and Corollary 3.4. Hence by bounded $Π_{1}^{0}$ -comprehension (provable in ${RCA}_{0}$ , see [24], Theorem 1, or [25], Theorems II.3.9 and II.2.5) one gets the existence of a code σ of a finite $0 / 1$ -sequence of length $n_{k}$ such that $\begin{matrix} \forall i (1 ⩽ i ⩽ n_{k} \to ({(σ)}_{i - 1} = 0 \leftrightarrow P (i))) . \end{matrix}$ Consider now an i with $\neg P (i)$ . Then, again by ${WKL}_{0}$ and using [25], Theorem IV.2.2, one gets the existence of an $l_{i} \in N$ with $\begin{matrix} inf {G_{i} (x) : x \in X} > 2^{- l_{i}} \end{matrix}$ and hence $\begin{matrix} \forall x \in \overline{B} (a_{i}, 2^{- k - 1}) (| F (x) | > 2^{- l_{i}}) . \end{matrix}$ In ${WKL}_{0}$ (needed to show the existence of a modulus of uniform continuity for F and hence for $G_{i}$ ) one can show that the sequence $(a_{i})$ with $a_{i} : = inf {| G_{i} (x) | : x \in X}$ exists. So by $Σ_{1}^{0}$ -bounded collection (provable in ${RCA}_{0}$ ) we can prove $\begin{matrix} \exists l \in N \forall i (1 ⩽ i ⩽ n_{k} \land {(σ)}_{i - 1} = 1 \to inf {G_{i} (x) : x \in X} > 2^{- l}) . \end{matrix}$ Now assume that $| F (x) | ⩽ 2^{- l}$ for some $x \in X$ . Then, by the definition of l, x must be in one of the balls $\overline{B} (a_{i}, 2^{- k - 1})$ (with $1 ⩽ i ⩽ n_{k}$ ) for which ${(σ)}_{i - 1} = 0$ , i.e. which contains a zero z of F. Since $d (x, z) ⩽ 2^{- k}$ , the conclusion follows.

2) is an immediate corollary to Theorem 4.1(2) as in the unique case the concepts of regularity and uniform uniqueness coincide. □
Remark 4.3.
The proof of Theorem 4.2(1) uses classical logic in the form of $Π_{1}^{0}$ -LEM (implicit in the bounded $Π_{1}^{0}$ -CA and M (implicit in concluding $\forall x \in \overline{B} (a_{i}, 2^{- k - 1}) \exists l \in N (G_{i} (x) > 2^{- l})$ from $\neg \exists x \in \overline{B} (a_{i}, 2^{- k - 1}) (G_{i} (x) = 0)$ .
Theorem 4.4.

${ACA}_{0}$ proves that if $X = \hat{A}$ is a compact metric space and $F : X \to R$ is continuous and has a zero, then F possesses a modulus of regularity w.r.t. $zer F$ .

Over ${RCA}_{0}$ , the statement that every Lipschitz continuous function $F : [0, 1] \to R$ with a zero has a modulus of regularity implies ${ACA}_{0}$ .

Proof.
1) Let $S : = zer F$ . By Theorem 4.2(1), already ${WKL}_{0}$ suffices to prove: $\begin{matrix} (3) & \forall n \in N \exists k \in N \forall l \in N (| F (a_{l}) | < 2^{- k} \to \exists p \in S (d (a_{l}, p) ⩽ 2^{- n})) . \end{matrix}$ We now show (in ${WKL}_{0}$ ) that $\begin{matrix} (4) & P (n, k, l) : \equiv (| F (a_{l}) | < 2^{- k} \to \exists p \in S (d (a_{l}, p) ⩽ 2^{- n})) \in Π_{1}^{0} . \end{matrix}$ Define (uniformly in n, l) continuous functions $G_{n, l} : X \to R$ by $\begin{matrix} G_{n, l} (x) : = max {| F (x) |, max {2^{- n}, d (a_{l}, x)} - 2^{- n}} . \end{matrix}$ Then $\begin{matrix} P (n, k, l) \leftrightarrow (| F (a_{l}) | < 2^{- k} \to \exists p \in X (G_{n, l} (p) = 0)) . \end{matrix}$ Hence, by Corollary 3.4, ${WKL}_{0}$ proves (see also the proof of Lemma 5.5) that $P (n, k, l) \in (Σ_{1}^{0} \to Π_{1}^{0}) = Π_{1}^{0}$ .

(3) and (4) imply that $\begin{matrix} \forall n \in N \exists k \in N \forall l \in N P (n, k, l) with \forall l \in N P (n, k, l) \in Π_{1}^{0} \end{matrix}$ and so by (a single use of) $Π_{1}^{0} {-AC}^{N, N}$ , and thus, in particular, in ${ACA}_{0}$ , we get $\begin{matrix} \exists f : N \to N \forall n, l \in N (| F (a_{l}) | < 2^{- f (n)} \to \exists p \in S (d (a_{l}, p) ⩽ 2^{- n})) . \end{matrix}$ Using the continuity of F and that ${a_{l} : l \in N}$ is dense in X we get $\begin{matrix} \exists f : N \to N \forall n \in N \forall x \in X (| F (x) | < 2^{- f (n)} \to \exists p \in S (d (x, p) < 2^{- n + 1})) \end{matrix}$ and so $g (n) : = f (n + 1)$ is a modulus of regularity for F w.r.t. $zer F$ .

2) We use a construction from the proofs of Remarks 4.9 and 4.10 in [19] which in turn adapt a construction due to [23]. Let $(a_{n})$ be a nondecreasing sequence of rational numbers in $[0, 1]$ and define $\begin{array}{l} f_{n} : [0, 1] \to [0, 1], f_{n} (x) : = max {x, a_{n}}, \\ T : [0, 1] \to [0, 1], T (x) : = \frac{1}{2} (x + f (x)), where f (x) : = \sum_{n = 0}^{\infty} 2^{- n - 1} f_{n} (x) . \end{array}$ f is nonexpansive and, therefore, T is nonexpansive too (even firmly nonexpansive) and 1 is a fixed point of T. By primitive recursion one can easily show in ${RCA}_{0}$ that the sequence $(x_{n})$ defined by $x_{n} : = T^{n} 0$ exists. By the comment after Corollary 1 in [16], $α (n) : = n + 3$ is a rate of asymptotic regularity for $(x_{n})$ , i.e. $\begin{matrix} \forall n \in N \forall k ⩾ n + 3 (| x_{k} - T x_{k} | < 2^{- n}) . \end{matrix}$ All this can easily be established in ${RCA}_{0}$ . Suppose now that the 2-Lipschitz function $F : [0, 1] \to R$ , $F (x) : = | x - T x |$ has a modulus of regularity $g : N \to N$ (note that $1 \in zer F \neq \emptyset$ ) Then (reasoning as in the proof of Theorem 4.1 in [19]; note that $(x_{n})$ obviously is Fejér monotone w.r.t. $zer F = Fix (T)$ since T is nonexpansive) one can easily show in ${RCA}_{0}$ that $ρ (n) : = α (g (n + 1)) = g (n + 1) + 3$ is a rate of convergence for $(x_{n})$ . So $z : = {lim}_{n \to \infty} x_{n}$ can be shown in ${RCA}_{0}$ to exist and is a fixed point of T, i.e. a zero of F. Since $f (z) = z$ , it is clear that $\forall n \in N (a_{n} ⩽ z)$ . Suppose that there would exist a $k \in N$ with $a_{n} + 2^{- k} ⩽ z$ for all $n \in N$ . Then by $Π_{1}^{0}$ -induction (and hence in ${RCA}_{0}$ ) also $x_{n} ⩽ z - 2^{- k}$ for all $n \in N$ in contradiction to $lim x_{n} = z$ : clearly $x_{0} = 0 ⩽ a_{n} ⩽ z - 2^{- k}$ . Assume that $x_{n} ⩽ z - 2^{- k}$ . Then $\begin{array}{rcl} x_{n + 1} & = & \frac{1}{2} (x_{n} + f (x_{n})) = \frac{1}{2} (x_{n} + \sum_{l = 0}^{\infty} 2^{- l - 1} max {x_{n}, a_{l}}) \\ \overset{I.H., assumption}{⩽} & \frac{1}{2} (z - 2^{- k} + \sum_{l = 0}^{\infty} 2^{- l - 1} (z - 2^{- k})) = z - 2^{- k} . \end{array}$ Hence $z = lim a_{n}$ . The claim now follows from the well-known fact that the convergence of increasing sequences of rational numbers in $[0, 1]$ is equivalent to ${ACA}_{0}$ over ${RCA}_{0}$ ([25], Theorem III.2.2, and note that the sequence $(c_{n})$ constructed in the relevant part of the proof of this theorem is an increasing sequence of rational numbers in $[0, 2]$ so that we may take $a_{n} : = c_{n} / 2$ ; alternatively one can also adapt Specker’s [26] construction). □
5. Weihrauch complexity of moduli of uniqueness and regularity

We recall the standard concepts used in the notion of Weihrauch reducibility which can be found e.g. in [5].

Definition 5.1.

A represented space is a pair $(X, δ_{X})$ , where X is a set and $δ_{X} : \subseteq N^{N} \to X$ is a partial surjective function.

Definition 5.2.

Let $(X, δ_{X}), (Y, δ_{Y})$ be represented spaces and let $f : \subseteq X ⇉ Y$ be a multi-valued function. Then $F : \subseteq N^{N} \to N^{N}$ is a realizer of f if $\begin{matrix} \forall p \in dom (f δ_{X}) (δ_{Y} (F (p)) \in f (δ_{X} (p))) . \end{matrix}$

Definition 5.3.

Let f, g be multi-functions on represented spaces. Then f is said to be Weihrauch reducible to g, in symbols $f ⩽_{W} g$ , if there are computable functions $H, K : \subseteq N^{N} \to N^{N}$ such that $H ⟨ i d, G K ⟩$ is a realizer of f whenever G is a realizer of g. We say that f and g are Weihrauch equivalent, in symbols $f \equiv_{W} g$ , if both $f ⩽_{W} g$ and $g ⩽_{W} f$ .

The parallelization $\hat{LPO}$ of the ‘omniscience principle’ LPO (i.e. $Σ_{1}^{0}$ -LEM) is defined as3

The official definition is slightly different but modulo Currying trivially equivalent to this, see [5], Lemma 6.3, where our formulation is called C.

\begin{matrix} \hat{LPO} : N^{N \times N} \to N^{N}, \hat{LPO} (q) (n) = \{\begin{matrix} 0, & if \exists k \in N (q (n, k) = 0), \\ 1, & otherwise . \end{matrix} \end{matrix}

The formulation of the convergence principle for bounded monotone sequences of reals is formulated in the framework of Weihrauch complexity as follows

\begin{matrix} MCT : \subseteq R^{N} \to R, (x_{n}) \mapsto sup_{n \in N} x_{n} \end{matrix}

with

dom (MCT) = {(x_{n}) : \forall n \in N (x_{n} ⩽ x_{n + 1}) and (x_{n}) bounded}

{MCT}_{Q \cap [0, 1]}

is the restriction of MCT to

{(r_{n}) \in Q^{N} : \forall n \in N (0 ⩽ r_{n} ⩽ r_{n + 1} ⩽ 1)}

It is well-known (see e.g. [6], Facts 3.5 and 11.26; the result essentially is also already in [15], Proposition 5.5) that $\begin{matrix} {MCT}_{Q \cap [0, 1]} \equiv_{W} MCT \equiv_{W} \hat{LPO} . \end{matrix}$ Let us define $\begin{matrix} {MREG}_{[0, 1]} : \subseteq C [0, 1] ⇉ N^{N}, F \mapsto {f \in N^{N} : f modulus of regularity of F w.r.t. zer F}, \end{matrix}$ with $dom ({MREG}_{[0, 1]}) : = {F \in C [0, 1] : zer F \neq \emptyset}$ , and $\begin{matrix} {MUNI}_{[0, 1]} : \subseteq C [0, 1] ⇉ N^{N}, F \mapsto {f \in N^{N} : f modulus of uniqueness (*) of F w.r.t. zer F}, \end{matrix}$ with $dom ({MUNI}_{[0, 1]}) : = {F \in C [0, 1] : F has at most one zero}$ .

We will show that ${MUNI}_{[0, 1]}$ is computable and so this a fortiori holds for its restriction to those F which have exactly one zero.

In the proofs below we refer to the standard representations of $R$ and $C [0, 1]$ but suppress explicitly mentioning them.

Lemma 5.4.

$MCT ⩽_{W} {MREG}_{[0, 1]}$ .

Proof.

By the comments above, it suffices to show that $\begin{matrix} {MCT}_{Q \cap [0, 1]} ⩽_{W} {MREG}_{[0, 1]} . \end{matrix}$ As the proof of Theorem 4.4(2) shows, uniformly in a given increasing sequence $(a_{n})$ of rational numbers in $[0, 1]$ one can compute a (2-Lipschitz) function $F : = K ((a_{n})) \in dom ({MREG}_{[0, 1]})$ such that if $g \in {MREG}_{[0, 1]} (F)$ , then $a : = lim a_{n} = sup a_{n}$ can be computed uniformly as a functional $H ((a_{n}), g)$ using that $g (n + 1) + 3$ is a rate of convergence for $(T^{n} 0)$ whose limit is a (note that in $(a_{n})$ , the mapping T, and hence the sequence $(T^{n} 0)$ , is computable). □

Lemma 5.5.

${MREG}_{[0, 1]} ⩽_{W} \hat{LPO}$ .

Proof.

Let $F \in C [0, 1]$ with $zer F \neq \emptyset$ . From a name of F in the usual standard representation of $C [0, 1]$ one can compute a modulus $ω : N \to N$ of uniform continuity for F, i.e. $\begin{matrix} \forall k \in N \forall x, y \in [0, 1] (| x - y | < 2^{- ω (k)} \to | F (x) - F (y) | < 2^{- k}), \end{matrix}$ and from this a (common) modulus $\tilde{ω} (k) : = max {ω (k), k}$ of uniform continuity for the function $G_{n, l}$ from the proof of Theorem 4.4(1) for all $n, l \in N$ . Using compactness (WKL) the statement $\begin{matrix} \exists p \in [0, 1] (G_{n, l} (p) = 0) \end{matrix}$ can be written equivalently as $\begin{matrix} \forall m \exists i ⩽ 2^{\tilde{ω} (m)} (| G_{n, l} (i / 2^{\tilde{ω} (m)}) (m) | <_{Q} 2^{- m + 1}) \in Π_{1}^{0}, \end{matrix}$ where for (a name of) $x \in R$ , ‘ $x (m)$ ’ denotes the $2^{- m}$ -rational approximation to x provided by that name. Note that WKL is only needed to verify the above equivalence but not to construct the $Π_{1}^{0}$ -formula from a name of F.

With $(a_{l})$ being some standard enumeration of the dyadic rational numbers in $[0, 1]$ , the property $\forall l \in N P (n, k, l)$ in the proof of Theorem 4.4(1) can now be written (coding three universal quantifiers into a single one) as $\begin{matrix} \forall l \in N (q (⟨ n, k ⟩, l) \neq 0) \end{matrix}$ for a function $q \in N^{N \times N}$ which can be uniformly computed as a function $q : = K (F)$ in (a name of) F. Now let $p = \hat{LPO} (q)$ . Then the statement $\begin{matrix} \forall n \in N \exists k \in N \forall l \in N P (n, k, l) \end{matrix}$ established in the proof of Theorem 4.4(1) has the form $\begin{matrix} \forall n \in N \exists k \in N (p (⟨ n, k ⟩) = 1) \end{matrix}$ so that an $f \in N^{N}$ with $\begin{matrix} \forall n \in N \forall l \in N P (n, f (n), l) \end{matrix}$ can be uniformly computed in p as $\begin{matrix} f : = H (p) : = λ n . min k [p (⟨ n, k ⟩) = 1] . \end{matrix}$ As in the proof of Theorem 4.4(1) it follows that $g (n) : = f (n + 1)$ is a modulus of regularity for F w.r.t. $zer F$ , i.e. $g \in {MREG}_{[0, 1]} (F)$ . □

Corollary 5.6.

$\begin{matrix} {MREG}_{[0, 1]} \equiv_{W} \hat{LPO} . \end{matrix}$

The above also holds for general computably compact computable Polish spaces instead of $[0, 1]$ .

In contrast to this, we have that ${MUNI}_{[0, 1]}$ is computable (again this holds for every computably compact computable Polish space K instead of $[0, 1]$ but for the sake of simplicity we treat here only the case $[0, 1]$ ):

Proposition 5.7.

${MUNI}_{[0, 1]}$ is computable.

Proof.

We use the representation of $[0, 1]$ from [18] (Chapter 4) by which

each $f \in N^{N}$ represents a unique element in $[0, 1]$ ,

primitive recursively in $f \in N^{N}$ one can define $\tilde{f} ⩽ N : = λ n . j (2^{n + 3}, 2^{n + 2} - 1)$ such that $\tilde{f}$ represents the same real in $[0, 1]$ as f does (here $f ⩽ g : \equiv \forall n \in N (f (n) ⩽ g (n))$ ).

On the level of names f, g for

x, y \in [0, 1]

and a given name

\hat{F} \in N^{N}

for

F \in C [0, 1]

one can express

\begin{matrix} (x, y) \in U_{n, k} : \equiv (| F (x) |, | F (y) | ⩽ 2^{- k} \to | x - y | < 2^{- n}) \end{matrix}

as a

Σ_{1}^{0}

-formula

\begin{matrix} \exists l \in N (Φ (\hat{F}, f, g, n, k, l) = 0), \end{matrix}

where Φ is a (primitive recursively) computable functional

: N^{N} \times N^{N} \times N^{N} \times N^{3} \to N

If F has at most one zero, then $\begin{matrix} \tilde{Ψ} (f, g, n) : = min m . [Φ (\hat{F}, f, g, n, {(m)}_{0}, {(m)}_{1}) = 0] \end{matrix}$ defines (computably in $\hat{F}$ ) a total function $: N^{N} \times N^{N} \times N \to N$ . With $\tilde{Ψ}$ also $Ψ (f, g, n) : = {(\tilde{Ψ} (f, g, n))}_{0}$ is computable in $\hat{F}$ . Hence the restriction of $λ f, g . Ψ (f, g, n)$ to functions $f, g ⩽ N$ has (uniformly in n) a modulus of uniform continuity $ω (n, k)$ which is computable in $\hat{F}$ , i.e. $\begin{array}{l} \forall f_{1}, f_{2}, g_{1}, g_{2} ⩽ N \forall k, n \in N \\ ({\overline{f}}_{1} (ω (n, k)) = {\overline{f}}_{2} (ω (n, k)) \land {\overline{g}}_{1} (ω (n, k)) = {\overline{g}}_{2} (ω (n, k)) \to Ψ (f_{1}, g_{1}, n) = Ψ (f_{2}, g_{2}, n)) . \end{array}$ Using ω one can compute (uniformly in $\hat{F}$ ) $\begin{matrix} α (n) : = sup {Ψ (f, g, n) : f, g ⩽ N} . \end{matrix}$ Clearly, α is a modulus of uniform uniqueness in the form (∗) for $zer F$ . □

The proof above uses an unbounded search which terminates by the assumption of the uniqueness of the solution but which does not provide any complexity information. This is in contrast to the situation where one has a proof (even if that is prima facie noneffective) for the uniqueness from which – as discussed briefly in Section 2 – one can then extract a modulus of uniqueness which reflects the numerical content of that uniqueness proof.

Footnotes

Acknowledgement

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

References

R.M.

Anderson , ‘Almost’ implies ‘Near’, Trans. Amer. Math. Soc.296 (1986), 229–237. doi:10.1090/S0002-9947-1986-0837809-3.

Beeson, Foundations of Constructive Mathematics, Springer Verlag, Berlin, Heidelberg, New York, 1985.

Berger,

Bridges and

Schuster, The fan theorem and unique existence of maxima, J. Symb. Logic71 (2006), 713–720. doi:10.2178/jsl/1146620167.

J.M.

Borwein,

Li and

M.K.

Tam, Convergence rate analysis for averaged fixed point iterations in common fixed point problems, SIAM J. Optim.27 (2017), 1–33. doi:10.1137/15M1045223.

Brattka and

Gherardi, Weihrauch degrees, omniscience principles and weak computability, J. Symb. Logic76 (2011), 143–176. doi:10.2178/jsl/1294170993.

Brattka,

Gherardi and

Marcone, The Bolzano–Weierstraß theorem is the jump of weak König’s lemma, Ann. Pure Appl. Logic163 (2012), 623–655. doi:10.1016/j.apal.2011.10.006.

E.M.

Briseid, Logical aspects of rates of convergence in metric spaces, J. Symb. Logic74 (2009), 1401–1428. doi:10.2178/jsl/1254748697.

D.K.

Brown, Functional analysis in weak subsystems of second order arithmetic, PhD thesis, Pennsylvania State University, 1987.

J.V.

Burke and

M.C.

Ferris, Weak sharp minima in mathematical programming, SIAM J. Control Optim.31 (1993), 1340–1359. doi:10.1137/0331063.

10.

Dontchev and

Rockafellar, Implicit Functions and Solution Mappings. A View from Variational Analysis, Springer Monographs in Mathematics, Springer, Dordrecht, 2009.

11.

Gerhardy, A quantitative version of Kirk’s fixed point theorem for asymptotic contractions, J. Math. Anal. Appl.316 (2006), 339–345. doi:10.1016/j.jmaa.2005.04.039.

12.

Gerhardy and

Kohlenbach, General logical metatheorems for functional analysis, Trans. Amer. Math. Soc.360 (2008), 2615–2660. doi:10.1090/S0002-9947-07-04429-7.

13.

Kohlenbach, Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin’s proof for Chebycheff approximation, Ann. Pure Appl. Logic64 (1993), 27–94. doi:10.1016/0168-0072(93)90213-W.

14.

Kohlenbach, New effective moduli of uniqueness and uniform a-priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory, Numer. Funct. Anal. Optim.14 (1993), 581–606. doi:10.1080/01630569308816541.

15.

Kohlenbach, Things that can and things that cannot be done in PRA, Ann. Pure Applied Logic102 (2000), 223–245. doi:10.1016/S0168-0072(99)00036-6.

16.

Kohlenbach, On the computational content of the Krasnoselski and Ishikawa fixed point theorems, in: Proceedings of the Fourth Workshop on Computability and Complexity in Analysis,

Blanck,

Brattka and

Hertling, eds, LNCS, Vol. 2064, Springer, 2001, pp. 119–145. doi:10.1007/3-540-45335-0_9.

17.

Kohlenbach, Some logical metatheorems with applications in functional analysis, Trans. Amer. Math. Soc.357(1) (2005), 89–128. doi:10.1090/S0002-9947-04-03515-9.

18.

Kohlenbach, Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Monographs in Mathematics, 2008, xx+536pp.

19.

Kohlenbach,

López-Acedo and

Nicolae, Moduli of regularity and rates of convergence for Fejér monotone sequences, Submitted, arXiv:1711.02130.

20.

Kohlenbach and

Oliva, Proof mining in

L_{1}

-approximation, Ann. Pure Appl. Logic121 (2003), 1–38. doi:10.1016/S0168-0072(02)00081-7.

21.

A.Y.

Kruger, Error bounds and metric subregularity, Optimization64 (2015), 49–79. doi:10.1080/02331934.2014.938074.

22.

Leventhal, Metric subregularity and the proximal point method, J. Math. Anal. Appl.360 (2009), 681–688. doi:10.1016/j.jmaa.2009.07.012.

23.

Neumann, Computational problems in metric fixed point theory and their Weihrauch degrees, Log. Method. Comput. Sci.11 (2015), 44pp.

24.

Parsons, On n-quantifier induction, J. Symbolic Logic37 (1972), 466–482. doi:10.2307/2272731.

25.

S.G.

Simpson, Subsystems of Second Order Arithmetic, 2nd edn, ASL Perspectives in Mathematical Logic, Cambridge University Press, 2009, xvi+444.

26.

Specker, Nicht konstruktiv beweisbare Sätze der Analysis, J. Symb. Logic14 (1949), 145–158. doi:10.2307/2267043.

27.

Specker, Der Satz vom Maximum in der rekursiven Analysis, in: Constructivity in Mathematics,

Heyting, ed., Proceedings of the Colloquium Held at Amsterdam 1957, North-Holland, 1959, pp. 254–265.

28.

A.S.

Troelstra and

van Dalen, Constructivism in Mathematics, Vol. I, North-Holland, Amsterdam, 1988.

On the reverse mathematics and Weihrauch complexity of moduli of regularity and uniqueness

Abstract

Keywords

1. Introduction

1 The latter is already implicit in [13] and [3] since to convert uniform uniqueness to prenex form as in [13], resp. reformulating it in the strong form stated on p. 714 in [3], just amounts to applying M.

Definition 2.1 ([19]).

3. Reverse mathematics

Theorem 3.1 ([25], Theorem IV.1.6).

Theorem 3.2 ([25], Theorem IV.1.7).

Proposition 3.3 ([25], Exercise II.6.9, [8], Lemma 1.24).

Footnotes

Acknowledgement

References

¹
The latter is already implicit in [13] and [3] since to convert uniform uniqueness to prenex form as in [13], resp. reformulating it in the strong form stated on p. 714 in [3], just amounts to applying M.