BRICS RS-01-14 Kohlenbach & Oliva: Effective Bounds on Strong Unicity in L_{1}-Approximation BRICS

Basic Research in Computer Science

Effective Bounds on Strong Unicity in L_{1}-Approximation

Ulrich Kohlenbach Paulo B. Oliva BRICS Report Series RS-01-14 ISSN 0909-0878 May 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Ulrich Kohlenbach & Paulo B. Oliva.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/01/14/

Effective bounds on strong unicity in L_{1}-approximation

Ulrich Kohlenbach  Paulo Oliva

May, 2001 BRICS^{∗} Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C, Denmark

Abstract

In this paper we present another case study in the general project of Proof Mining which means the logical analysis of prima facie non-effective proofs with the aim of extracting new computationally relevant data. We use techniques based on monotone functional interpretation (developed in [17]) to analyze Cheney’s simplification [6] of Jackson’s original proof [9] from 1921 of the uniqueness of the best L_{1}-approximation of continuous functions f ∈ C[0, 1] by polynomials p ∈ P_{n} of degree ≤ n. Cheney’s proof is non-effective in the sense that it is based on classical logic and on the non-computational principle WKL (binary König lemma). The result of our analysis provides the first effective (in all parameters f, n and ε) uniform modulus of uniqueness (a concept which generalizes ‘strong uniqueness’ studied extensively in approximation theory). Moreover, the extracted modulus has the optimal ε-dependency as follows from Kroó [20]. The paper also describes how the uniform modulus of uniqueness can be used to compute the best L_{1}-approximations of a fixed f ∈ C[0, 1] with arbitrary precision, and includes some remarks on the case of best Chebycheff approximation.

1 Introduction

This paper is another case study in the general project of proof mining which means the logical analysis of prima facie non-effective proofs with the aim of extracting new computationally relevant data.^{1} At the same time we obtain new results in approximation theory. More specifically, we analyze a non-effective proof of the uniqueness of best approximations of continuous functions f ∈ C[0, 1] by polynomials p ∈ P_{n} of degree ≤ n with respect to the L_{1}-norm^{2}

∗Basic Research in Computer Science, funded by the Danish National Research Foundation.

1See [15], [16], [19] and [12] for other case studies as well as more information on Proof Mining in general.

∥f∥_{1} := ∫_{0}^{1} |f(x)|dx.

In [15], the first author showed how a quite general class of (non-effective) proofs of uniqueness theorems in analysis can be analyzed such that an effective so-called modulus of uniqueness can be extracted which generalises the concept of ‘strong unicity’.^{3} In [15] and [16] this technique has been applied to the case of best Chebycheff approximation yielding new uniform bounds on constants of strong unicity and a new quantitative version of the alternation theorem. In this paper we apply this logical approach to investigate the quantitative rate of strong unicity for the quite different case of best L_{1}-approximation. Like Chebycheff approximation, L_{1}-approximation, also called ‘approximation in the mean’, is a classical topic in numerical mathematics and was considered already by Chebycheff in 1859 and has been investigated ever since (see [24] for a comprehensive survey). The uniqueness of the best L_{1}-approximation of f ∈ C[0, 1] by polynomials of degree ≤ n was first proved in [9]. This proof uses measure theoretic arguments. A new uniqueness proof which avoids this and only uses the Riemann integral instead was given in 1965 by Cheney (see [6],[7]). Because of this feature, Cheney called his proof ‘elementary’. From a logical point of view, however, it is highly non-constructive relying both on classical logic and non-computational analytical principles which correspond – in logical terminology – to the so-called binary (‘weak’) König’s lemma, a principle which has received considerable attention in various parts of logic in recent years (see [25]). In this paper we carry out a complete logical analysis of Cheney’s proof and show how the explicit modulus mentioned above can be extracted from this seemingly hopelessly non-constructive proof. Consequently, our result, like Cheney’s proof, does not require any measure theory.

The main result of the present paper is the following effective strong uniqueness theorem:

Main result (Theorem 4.3) Let

Φ(ω, n, ε) := min\{\frac{c_{n}ε}{3^{n+2}(n+1)^{n+1}} , \frac{c_{n}ε}{2}ω_{n}(\frac{c_{n}ε}{2})\}, where
c_{n} := \frac{⌊n/2⌋!⌈n/2⌉!}{2^{n+3}3^{n^{2}+2n}(n+1)^{n^{2}+2n+1}} and
ω_{n}(ε) := min\{ω(\frac{ε}{4}), _{\frac{ε}{40(n+1)^{4}⌈ \frac{1}{ω(1)} ⌉}}\}.

2For f ∈ L_{1} uniqueness in general fails.

3The term ‘strong unicity’ was introduced by Newman and Shapiro [23] in 1963 and has been studied extensively in approximation theory. See e.g. the introduction in [2] and the references given there for a discussion of the crucial importance of estimates of strong unicity for the convergence analysis of iterative algorithms and for stability analysis.

The functional Φ is a uniform modulus of uniqueness for the best L_{1}-approximation of any function f in C[0, 1] having modulus of uniform continuity ω from P_{n}, i.e.

∀n ∈ IN; p_{1}, p_{2} ∈ P_{n}; ε ∈ Q_{+}^{∗}( ⋀_{i=1}^{2}(∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < Φ(ω, n, ε)) → ∥p_{1} − p_{2}∥_{1} ≤ ε),

where dist_{1}(f, P_{n}) := inf_{p∈P_{n}} ∥f − p∥_{1} and ω : Q_{+}^{∗} → Q_{+}^{∗} is a modulus of uniform continuity for f ∈ C[0, 1] if ^{4}

∀x, y ∈ [0, 1]; ε ∈ Q_{+}^{∗}(|x − y| < ω(ε) → |f(x) − f(y)| < ε).

Moreover, this theorem can be proved in Heyting Arithmetic HA^{ω} in all finite types (and consequently holds in constructive mathematics in the sense of Bishop).

The technical details of this analysis are mainly due to the second author who is using the results in a subsequent paper to determine a complexity upper bound for the sequence (p_{b,n})_{n∈IN} of best approximating polynomials for poly-time computable functions f ∈ C[0, 1] (in the sense of [10],[11]). Before going into the details of the analysis we need to recall some general logical background from [15].^{5} First we introduce a little amount of logical terminology: Let A^{ω} be a (sub-)system of arithmetic in all finite types (like E-PA^{ω} from [26] or Feferman’s fragment E-PRA^{ω} with quantifier-free induction and primitive recursion on the type 0 only [8]). Let A_{∗}^{ω} denote the extension of A^{ω} by the schema

QF-AC : ∀f^{1}∃x^{0}A_{qf}(f, x) → ∃F^{2}∀f^{1}A_{qf}(f, F (f))

of quantifier-free choice from functions to numbers (where A_{qf} is quantifier-free) plus certain analytical principles Γ which – described in analytical terms – correspond to applications of Heine-Borel compactness of e.g. [0, 1]^{d}. In logical terms, these principles correspond to the so-called binary (‘weak’) König’s lemma WKL which suffices to derive a substantial amount of mathematics relative to weak fragments of arithmetic (see [25]).^{6} In this paper the only genuine analytical tool Γ (which goes beyond E-PA^{ω}+QF-AC) is the attainment of the minimum of f ∈ C[0, 1]

(∗) ∀f ∈ C[0, 1]∃x ∈ [0, 1](f(x) = inf_{y∈[0,1]} f(y)).

4Note that this notion – used also in constructive mathematics and computable and feasible analysis – differs from the concept of modulus of continuity used in numerical analysis which we will discuss further below.

5Readers only interested in the numerical results but not in the general process of proof mining might skip this passage.

6E-PRA^{ω}+QF-AC+WKL is a finite type extension of the system WKL_{0} used in reverse mathematics and is (like the latter) Π_{2}^{0}-conservative over primitive recursive arithmetic PRA (see [14],[1]).

(∗) is known to fail in computable analysis and even for poly-time computable f there will be in general no computable x ∈ [0, 1] satisfying (∗). ^{7} Now, let X be a Polish space, K a compact Polish space and F : X × K → IR a continuous function (moreover all these objects have to be explicitly representable in A^{ω}) and assume that we can prove in A_{∗}^{ω} that for every f ∈ X, F (f, ·) has at most one root in K, i.e.^{8}

(1) ∀f ∈ X∀x_{1}, x_{2} ∈ K( ⋀_{i=1}^{2} F (f, x_{i}) = 0 → x_{1} = x_{2}).

Then by a general logical meta-theorem proved in [15] (theorem 4.3) one can extract from such a proof an explicit bound Φ(f, k) (given by a closed term of the underlying arithmetical system A^{ω}) such that

(2) ∀f ∈ X∀k ∈ IN∀x_{1}, x_{2} ∈ K( ⋀_{i=1}^{2}(|F (f, x_{i})| < 2^{−Φ(f,k)}) → d_{K}(x_{1}, x_{2}) < 2^{−k}),

where d_{K} denotes the metric on K. Moreover, (2) can be proved without using WKL and even in the intuitionistic variant A_{i}^{ω} of A^{ω} (and hence in constructive analysis in the sense of Bishop). The proof of this meta-theorem provides an algorithm for actually extracting Φ. This algorithm is based on the proof-theoretic technique of monotone functional interpretation [17]. It is important to note that Φ(f, k) does not depend on x_{1}, x_{2} ∈ K. Because of this fact, Φ(f, k) – which we call a modulus of uniqueness – can be used to compute the unique root (if existent) from any algorithm Ψ(f, k) computing approximate so-called ε(= 2^{−k})-roots of F (f, ·):

(3) ∀f ∈ X∀k ∈ IN(Ψ(f, n) ∈ K ∧ |F (f, Ψ(f, k))| < 2^{−k}).

One easily verifies that (2) and (3) imply that Ψ(f, Φ(f, k)) is a Cauchy sequence in K which converges with rate of convergence 2^{−k} to the unique root x ∈ K of F (f, ·). So x = lim_{k→∞} Ψ(f, Φ(f, k)) can be computed with arbitrarily prescribed precision (which can

also be proved in A_{i}^{ω}, see [15], theorem 4.4) and the computational complexity of x can be estimated in terms of the complexities of Φ and Ψ.

Remark 1.1 (Important!) As usual in computable analysis (see [27]), Φ(f, k) and Ψ(f, k) will depend not only on f ∈ X in the set theoretic sense but on a (computationally meaningful) representation of f. In the case of f ∈ C[0, 1], the representation of C[0, 1] as a Polish space (C[0, 1], ∥ · ∥_{∞}) in A^{ω} requires that f is endowed with a modulus of uniform continuity ω_{f}. So when we write Φ(f, k) we tacitly understand that f is given as a pair (f, ω_{f}). Actually, it now suffices to use the restriction f_{r} of f to the rational numbers in [0, 1] (which can be enumerated so that f_{r} can be represented as a number theoretic function), since f can be reconstructed from f_{r} with the help of ω_{f}. In this way, the representation (f_{r}, ω_{f}) of f can be viewed as an object of type 1 so that computability on f reduces to the well-known type-2 notion of computability (see again [27] for more information on this).

7(∗) is known to be equivalent to WKL over systems like E-PRA^{ω} even when f is given together with a modulus of uniform continuity, see [25].

8We may even have functions F : X × Y → IR, where X, Y are general Polish spaces and can allow constructively definable families (K_{f})_{f∈X} of compact subspaces of Y which are parametrised by f ∈ X instead of a fixed K. See [15] for details.

Let us now move to the case of best L_{1}-approximation treated in the present paper. The uniqueness of the best approximation can be written as follows

(4) ∀n ∈ IN∀f ∈ C[0, 1]∀p_{1}, p_{2} ∈ P_{n}( ⋀_{i=1}^{2}(∥f − p_{i}∥_{1} = dist_{1}(f, P_{n})) → p_{1} = p_{2}).

Note that in (4) we can without loss of generality replace the non-compact subspace P_{n} of C[0, 1] with the compact one K̃_{f,n} := {p ∈ P_{n} : ∥p∥_{1} ≤ 2∥f∥_{1}} since any best approximation p_{b} has to satisfy ∥f − p_{b}∥_{1} ≤ ∥f∥_{1} because otherwise the zero polynomial would be a better approximation. As a consequence of this, dist_{1}(f, P_{n}) = dist_{1}(f, K̃_{f,n}) can easily be seen to be computable (uniformly in f as represented above and n). We use the slightly larger space K_{f,n} := \{p ∈ P_{n} : ∥p∥_{1} ≤ \frac{5}{2}∥f∥_{1}\} in (4) for technical reasons.

In this paper we analyze the above mentioned proof of Cheney for (4) as given in [6],[7]^{9} which uses the non-computational principle (∗) (together with classical logic) but which can be formalized in A_{∗}^{ω} (as was shown in [13]). So the above mentioned result on the extractability of a modulus of uniqueness is applicable, i.e. the extractability of a (primitive recursive in the sense of Gödel’s T) functional Φ satisfying

(5) \{ \begin{matrix}∀n, k ∈ IN∀f ∈ C[0, 1]∀p_{1}, p_{2} ∈ K_{f,n} \\ ( ⋀_{i=1}^{2}(∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < 2^{−Φ(f,n,k)}) → ∥p_{1} − p_{2}∥_{1} < 2^{−k}) \end{matrix}

is guaranteed. Moreover, a simple trick (used also in [15] in the Chebycheff case) allows to replace K_{f,n} with P_{n} so that

(6) \{ \begin{matrix}∀n, k ∈ IN∀f ∈ C[0, 1]∀p_{1}, p_{2} ∈ P_{n} \\ ( ⋀_{i=1}^{2}(∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < 2^{−Φ(f,n,k)}) → ∥p_{1} − p_{2}∥_{1} < 2^{−k}). \end{matrix}

9This result was first proved in [9] and is also called Jackson’s theorem. Cheney’s proof (which applies to arbitrary Chebycheff systems) is a simplification of Jackson’s proof.

Remark 1.2 Since ∥p_{1} −p_{2}∥_{∞} ≤ 2(n+1)^{2}∥p_{1} −p_{2}∥_{1} any upper bound on ∥p_{1} −p_{2}∥_{1} gives an bound on ∥p_{1}−p_{2}∥_{∞} and we can use this to get a bound on the coefficients of p_{1}−p_{2}. Namely, if p_{1}(x) − p_{2}(x) := a_{n}x^{n} + … + a_{1}x + a_{0} and ∥p_{1} − p_{2}∥_{1} < M then |a_{i}| ≤ \frac{(2(n+1)^{2})^{i+1}}{i!} M. The proof of this fact is given in section 3.5.

The importance of the modulus of uniqueness Φ(f, k) can also be illustrated by the fact that Φ + 1 is automatically a modulus of pointwise continuity for the operator which maps f ∈ X to its unique best approximation f_{b} ∈ E ⊂ X (see [15]). For the special cases of Chebycheff resp. L_{1}-approximation this was shown first in [7] resp. [3]. Therefore,

(7)∀n, k ∈ IN∀f, f̃ ∈ C[0, 1](∥f − f̃∥_{1} < 2^{−Φ(f,n,k)−1} → ∥P(f, n) − P(f̃, n)∥_{1} < 2^{−k}),

where P(f, n) is the unique best L_{1}-approximation of f ∈ C[0, 1] from P_{n}.

Since (C[0, 1], ∥ · ∥_{1}) is not a Polish space we have to represent C[0, 1] as the space (C[0, 1], ∥ · ∥_{∞}) to apply the logical meta-theorem mentioned above. As we discussed already, this amounts to enriching the input f by a modulus of uniform continuity ω_{f} so that Φ will also depend on ω_{f}.

Note that if C[0, 1] is replaced by the (pre-)compact (w.r.t. ∥ · ∥_{∞}) set K_{ω,M} of all functions f ∈ C[0, 1] which have the common modulus of uniform continuity ω and the common bound ∥f∥_{∞} ≤ M, then the same logical meta-theorem guarantees the extractability of a modulus of uniqueness Φ which only depends on K_{ω,M} i.e. on ω, M (in addition to n, k). Moreover, even the M-dependency can be eliminated as the approximation problem for f can be reduced to that for f̃(x) := f(x) − f(0) so that only a bound N ≥ sup_{x∈[0,1]} |f(x) − f(0)| is required, which can easily be computed from ω (e.g take N := ⌈\frac{1}{ω(1)}⌉). Therefore, from the logical meta-theorem and the fact that Cheney’s proof can be formalized in E-PA^{ω}+WKL we obtain already the extractability of a primitive recursive (in the sense of Gödel’s T) modulus of uniqueness Φ which only depends on ω_{f}, n and k: a-priori information. Of course, only the actual extraction of Φ by applying the algorithm provided by the logical meta-theorem gives the detailed mathematical form of Φ as presented above: a-posteriori information. It is interesting to note that although the proof we analyze here was published in 1965 (by Cheney) only in 1975 Björnestål proved the existence of a modulus of uniform uniqueness for the best L_{1}-approximation having the form c_{f,n}ε ω_{f}(c_{f,n}ε) where the constant c_{f,n} depends only on f (and its modulus of continuity) and n, but no explicit constant was presented. In 1978 Kroó improved such a result (using some amount of measure theory) proving the existence of a constant C_{ω_{f} ,n} which was independent of any particular value of f (i.e. the modulus of uniqueness would depend on f only through its modulus of continuity) doing the same job but as Björnestål he did not present any constant. In the same paper Kroó (using the method of Björnestål) also proved that the dependency on ε, i.e. ε ω_{f}(ε), is optimal (even for the modulus of pointwise continuity for the projection, see theorem 4.5). Therefore it is quite amazing that the a-priori information - the dependencies of the modulus of uniqueness - we obtain immediately by showing that Cheney’s proof can be formalized in the system A_{∗}^{ω} (which in some sense means that this information was already implicit in Cheney’s proof) was obtained without the use of logic only long after the proof was given. Moreover, the a-posteriori information – the actual modulus of uniform uniqueness – presents explicitly the dependencies on ω, n and ε, and the dependency on ε is optimal (as shown by Kroó).

2 Analysing proofs in analysis

The algorithm to be used for proof mining applied in cases like Cheney’s proof of Jackson’s theorem (as treated in this paper) is based on the proof theoretic technique of monotone functional interpretation combined with negative translation as developed in [17]. Whereas the technical details of this process are of importance to establish general meta-theorems on proof mining, this is not necessary for applications to specific proofs since here all numerical data will explicitly be exhibited and verified. This is because monotone functional interpretation explicitly transforms a given proof into another numerically enriched proof (in the normal mathematical sense). It is the strategy to find that proof (and to guarantee its existence) which is provided by the logical technique.

To approach the problem of proof mining applied to a logically involved proof as Cheney’s, one starts off by splitting the proof into small pieces which are analyzed separately. As a consequence of the modularity of monotone functional interpretation one can easily combine the results obtained from the analysis of the pieces into a global result (this only requires functional application and λ-abstraction). Applications of monotone functional interpretation to the lemmas in the given proof at hand consist mostly of two steps,

1) transforming a given lemma L into a variant L^{∗} which has the form

(∗∗) ∀n ∈ IN∀x ∈ X∀y ∈ K∃kA_{1}(n, x, y, k),

where X is a Polish space, K a compact Polish space and A_{1} ∈ Σ_{1}^{0}, and

2) extracting a bound Φ(n, x) for k which is independent of y.

Because of this it is worthwhile to formulate the case of lemmas having the form (∗∗) as a special meta-theorem (2.1 below) which allows us to avoid having to go into the details of the underlying mechanism of functional interpretation each time. Although in the following we perform the transformation L ↦ L^{∗} “by hand” one should note that this transformation is also usually automatically provided by functional interpretation. Only in the case of ‘lemma 1’ below, we first simplify the lemma to achieve this.

Theorem 2.1 ([15], theorem 4.1) Let X, K be A^{ω}-definable Polish spaces, K compact and consider a sentence which can be written (when formalized in the language of A^{ω}) in the form

A := ∀n ∈ IN∀x ∈ X∀y ∈ K∃k ∈ IN A_{1}(n, x, y, k),

where A_{1} is a purely existential. Then the following rule holds:^{10}

A_{∗}^{ω} ⊢ ∀n ∈ IN∀x ∈ X∀y ∈ K∃k ∈ IN A_{1}(n, x, y, k)

then one can extract an A^{ω}-definable functional Φ s.t.

A_{i}^{ω} ⊢ ∀n ∈ IN∀x ∈ X∀y ∈ K∃k ≤ Φ(n, x) A_{1}(n, x, y, k).

In particular, if

A_{i}^{ω} ⊢ (k ≤ k̃ ∧ A_{1}(n, x, y, k)) → A_{1}(n, x, y, k̃)

then

A_{i}^{ω} ⊢ ∀n ∈ IN∀x ∈ X∀y ∈ K A_{1}(n, x, y, Φ(n, x)).

Again it is important to note that Φ does not depend on y ∈ K.^{11}

In the following we try to avoid too much reference to logic in the main text and only insert various ‘logical remarks’ to explain to those readers interested in the process of proof mining in general how the various steps in our concrete ‘mining’ correspond to steps in the monotone functional interpretation (as used in the general meta-theorems). Readers only interested in the numerical results can skip these remarks.

3 Analysis of Cheney’s proof of Jackson’s theorem

3.1 Logical preliminaries on Cheney’s proof

In this section we sketch how a slight modification of Cheney’s proof can be seen to be formalizable in basic arithmetic like A^{ω} :=E-PA^{ω} plus the already mentioned analytical principle (∗), i.e. WKL. The only part of the proof which cannot be directly formalized in A^{ω} is the so-called ‘lemma 1’ (see [7], p. 219) which reads as follows

Lemma 3.1 (Lemma 1) Let f, h ∈ C[0, 1]. If f has at most finitely many roots and if ∫_{0}^{1} h sgn(f) ≠ 0, then for some λ ∈ IR, ∫_{0}^{1} |f − λh| < ∫_{0}^{1} |f|, where

10As the theorem shows the conclusion can be proved already in A_{i}^{ω} instead of A_{∗}^{ω}. This, however, is not important for the applied aspect of the present paper where only the construction of Φ matters.

11As discussed in the previous section, Φ(n, x) will depend on the representation of x ∈ X.

sgn(f)(x) =_{0} \{ \begin{matrix}1, if f(x) >_{IR} 0 \\ 0, if f(x) =_{IR} 0 \\ −1, if f(x) <_{IR} 0. \end{matrix}

In the context of the Cheney’s proof of Jackson’s theorem, h will be a polynomial in P_{n}. Moreover, it will be shown that if f (for the particular f at hand) has only less than n + 1 roots one can construct an h such that ∫_{0}^{1} h sgn(f) ≠ 0. So we only need the lemma with the stronger assumption that f has fewer than n + 1 roots. The existence of sgn(f) relies on the existence of the characteristic function χ_{=_{IR}} for equality between reals which in turn is equivalent to the existence of Feferman’s ([8]) non-constructive μ-operator (see [18]) and hence to a strong form of arithmetical comprehension which is not available in A_{∗}^{ω} := A^{ω}+WKL. However, the use of sgn can be eliminated as follows: if f has less than n + 1 roots then there exist points x_{0} < … < x_{n+1} in [0, 1] (where x_{0} = 0 and x_{n+1} = 1) which contain all the roots of f. By classical logic and induction one shows in A^{ω} the existence of a vector (σ_{1}, …, σ_{n+1}) ∈ {−1, 1}^{n+1} such that

σ_{i} =_{0} \{ \begin{matrix}1, if f is positive on (x_{i−1}, x_{i}), \\ −1, if f is negative on (x_{i−1}, x_{i}) \end{matrix}

for i = 1, …, n + 1. Using this vector, ∫_{0}^{1} h sgn(f) can be written as ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h. It will turn out below that it is the precise logical form of this reformulation of lemma 1 which will play a crucial role in the analysis of Cheney’s proof. Monotone functional interpretation of (the negative translation of) our version of lemma 1 will automatically introduce the main notion needed for the quantitative analysis of the proof namely the concept of so-called ‘rclusters of δ-roots’. This concept, furthermore, is the key for the elimination of the use of (∗) (i.e. WKL) on which Cheney’s proof of lemma 1 relies.^{12}

3.2 Analysing the structure of the proof

The main goal of the paper is to extract from Cheney’s proof [7] of Jackson’s theorem [9] an effective modulus of uniqueness which can be used, as it will be shown in section 4.2, to compute the best L_{1}-approximation, p_{b}, from P_{n} of a given function f ∈ C[0, 1] with arbitrary precision.^{13} In order to carry out the analysis we need to formalize Cheney’s proof. The first step we take in this direction is to list the main formulas used in the proof and to show how they are combined into lemmas. As mentioned before, each lemma will be analyzed separately. The functional interpretation of the lemma shows which functionals can be extracted from the proof of the lemma. But not all the functionals need to be presented, since some of them will disappear in the analysis of the proof (see the treatment of modus pones in the soundness of functional interpretation, e.g. in [17]). By analyzing the structure of the whole proof we can see which functionals are relevant and need to be extracted in order to obtain the final result. Then we construct such functionals and prove that they realize the lemma. In section 4 we show how the final modulus Φ is obtained by combining these functionals.

12It is the argument that ‘δ’, in the middle of page 219 in [7], is strictly positive which uses (∗). See section 3.10 and Remark 3.10.3 for more information.

13P_{n} is a Haar subspace of C[0, 1] of dimension n + 1.

In the propositions A – K below we omitted the parameters f, n, p_{1} and p_{2}, therefore, instead of A one should read A(f, n, p_{1}, p_{2}), where n ranges over IN, f ∈ C[0, 1] and p_{1}, p_{2} ∈ P_{n}, and the same holds for all the others propositions. We also use here and for the rest of this paper the defined functions p(x) := \frac{p_{1}(x)+p_{2}(x)}{2} and f_{0}(x) := f(x) − p(x) as shorthand notation. In the formulas and in the sketch of the proof presented below we use \overline{x} := x_{1}, …, x_{n} and \overline{σ} := σ_{1}, …, σ_{n+1}. The following formulas are used in Cheney’s proof:

A := ⋀_{i=1}^{2}(∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) = 0), i.e.

p_{1} and p_{2} are best L_{1}-approximations of f from P_{n}.

B := ∥f − p∥_{1} − dist_{1}(f, P_{n}) = 0, i.e. p is a best L_{1}-approximation of f.

C := ∥f_{0}∥ = \frac{1}{2}∥f − p_{1}∥ + \frac{1}{2}∥f − p_{2}∥.

C_{1} := ∀ε ∈ Q_{+}^{∗}∃δ ∈ Q_{+}^{∗}∀x, y ∈ [0, 1](|x − y| < δ → |g(x) − g(y)| < ε), where g(x) := |f_{0}(x)| − \frac{1}{2}|f(x) − p_{1}(x)| − \frac{1}{2}|f(x) − p_{2}(x)|. The formula C_{1} states that g is uniformly continuous.

D := ∀x ∈ [0, 1](|f_{0}(x)| = \frac{1}{2}(|f(x) − p_{1}(x)| + |f(x) − p_{2}(x)|)).

E := ∃x_{0}, …, x_{n} ∈ [0, 1]( ⋀_{i=0}^{n} f_{0}(x_{i}) = 0 ∧ ⋀_{i=1}^{n} x_{i−1} < x_{i}), i.e. f_{0} has at least n + 1 distinct roots.

F := ∃x_{0}, …, x_{n} ∈ [0, 1]( ⋀_{i=0}^{n} p_{1}(x_{i}) = p_{2}(x_{i}) ∧ ⋀_{i=1}^{n} x_{i−1} < x_{i}), i.e. p_{1} − p_{2} has at least n + 1 distinct roots.

G := ∀x ∈ [0, 1](p_{1}(x) = p_{2}(x)), alternatively, ∥p_{1} − p_{2}∥_{1} = 0 or p_{1} = p_{2}.

H(h) := ∥f_{0} − h∥_{1} ≥ ∥f_{0}∥_{1}.

I(\overline{x}, \overline{σ}, h) := ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x)dx > 0, where x_{0} := 0 and x_{n+1} := 1.

J(\overline{x}) := ∃y ∈ [0, 1](f_{0}(y) = 0 ∧ ⋀_{i=0}^{n+1} x_{i} ≠ y), where x_{0} := 0 and x_{n+1} := 1.

K := ∀x ∈ [0, 1](f_{0}(x) = 0 → p_{1}(x) = p_{2}(x)). The first part of the proof (which we call derivation D_{1}) is very simple and derives K from the assumption A,

{{{{{[A] {[A] A → B \atop B} \atop A ∧ B} A ∧ B → C \atop C} C_{1} \atop C ∧ C_{1}} C ∧ C_{1} → D \atop D} D → K \atop K}

The most involved part of the proof (which includes the application of lemma 1) is when we want to prove that f_{0} has n + 1 distinct roots. In the derivation below we use \overline{σ}′ := σ′_{1}, …, σ′_{n+1}, where σ′_{i} := sgn (f_{0})(\frac{x_{i−1}+x_{i}}{2} ). Moreover, ∀\overline{x} := ∀x_{1} ≤ … ≤ x_{n}, where ∀x_{1} ≤ … ≤ x_{n} Q(\overline{x}) is an abreviation for ∀x_{1}, …, x_{n} (x_{1} ≤ … ≤ x_{n} → Q(\overline{x})).

\begin{aligned}{{[A] A → B \atop B} B → ∀h H(h) \atop ∀h H(h)} & {∀\overline{x}, \overline{σ}∃h I(\overline{x}, \overline{σ}, h) ∀\overline{x}, h (∀λH(λh) ∧ I(\overline{x}, \overline{σ}′, h) → J(\overline{x})) \atop ∀λH(λh̃) → ∀\overline{x}J(\overline{x})} \\ & ∀\overline{x} J(\overline{x}) \end{aligned}

We call this derivation D_{2}. An outline of the whole proof in the form of an informal natural deduction derivation is presented below,

{{\begin{aligned}{D_{1} \atop K} & {{D_{2} \atop ∀\overline{x} J(\overline{x})} ∀\overline{x} J(\overline{x}) → E \atop E} \\ & K ∧ E \end{aligned} K ∧ E → F \atop F} F → G \atop G}

\overline{[A]}
A → G

Remark 3.2 We assume that real numbers are represented as Cauchy sequences (a_{n})_{n∈IN} of rational number with fixed rate of convergence (say 2^{−n}) i.e. ∀k, k̃ ≥ n(|(a)_{k} − (a)k̃| ≤ 2^{−n}). In this way, equality =_{IR} (similarly ≤_{IR} and ≥_{IR}) between real numbers is a ∀-statement (for any point k in the Cauchy sequence the approximants are close by 2^{−k}) and strict inequality <_{IR} is a ∃-statement (there exists a point k + 1 in the sequence such that the approximants are distant by 2^{−k}). We call those: ‘hidden quantifiers’. For example, let a, b ∈ IR, then a <_{IR} b is an abreviation for ∃k ∈ IN((a)_{k+1} + 2^{−k} <Q (b)_{k+1}). In the analysis below we avoid going into the representation of the real numbers by observing that a <_{IR} b can be written either as ∃r ∈ Q_{+}^{∗}(a <_{IR} b + r) or ∃r ∈ Q_{+}^{∗}(a ≤_{IR} b + r). The idea is that, if a <_{IR} b occurs positively we write it as ∃r ∈ Q_{+}^{∗}(a <_{IR} b + r) and if it occurs negatively we write it as ∃r ∈ Q_{+}^{∗}(a ≤_{IR} b + r), in this way after prenexing these quantifiers the matrix is purely existential and (given the prenexed quantifiers have a ∀∃ form as described in theorem 2.1) we can apply our meta-theorem 2.1. In the beginning of the analysis of each lemma we present the hidden quantifiers that are relevant for the final modulus.

Remark 3.3 In general we can only apply our meta-theorem 2.1 if P_{n} is replaced by K_{f,n}. As it happened, only in section 3.5 this limitation really matters. Nonetheless, as we discussed already, at the end we show that the final result actually holds for P_{n}.

3.3 Lemma A → B [Triangle inequality]

The first lemma states,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}( ⋀_{i=1}^{2} ∥f − p_{i}∥_{1} = dist_{1}(f, P_{n}) → ∥f − p∥_{1} = dist_{1}(f, P_{n})).

As described in the previous section, the first step is to present the hidden quantifiers,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n} (∀δ ∈ Q_{+}^{∗}(⋀_{i=1}^{2} ∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) ≤ δ) → ∀ε ∈ Q_{+}^{∗}(∥f − p∥_{1} − dist_{1}(f, P_{n}) < ε)).

Then we look at the functional interpretation of the lemma,

(1) ∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; ε ∈ Q_{+}^{∗}∃δ ∈ Q_{+}^{∗}

( ⋀_{i=1}^{2} ∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) ≤ δ → ∥f − p∥_{1} − dist_{1}(f, P_{n}) < ε).

We see now that (1) has the same structure as the formula A in theorem 2.1. Therefore, we are sure to find a functional Φ_{1}, depending at most on n, f and ε, such that,^{14} (2) ∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; ε ∈ Q_{+}^{∗}∃δ ≥ Φ_{1}(f, n, ε)

14Since in theorem 2.1 we used 2^{−k} (with k ∈ IN) instead of δ ∈ Q_{+}^{∗}, the upper bound on k guaranteed by the meta-theorem gives a lower bound on δ.

( ⋀_{i=1}^{2}(∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < δ) → ∥f − p∥_{1} − dist_{1}(f, P_{n}) < ε).

Since we have monotonicity in δ the functional Φ_{1} actually realizes δ. The same phenomenon will happen in all the following lemmas, i.e. the lower bounds will always be realizing functionals for the variables they bound. Here, it is obvious how to construct Φ_{1},

Claim 3.4 The functional Φ_{1}(f, n, ε) := Φ_{1}(ε) := ε does the job.^{15}

Proof: Suppose (1) ∥f − p_{1}∥_{1} − dist_{1}(f, P_{n}) < ε and (2) ∥f − p_{2}∥_{1} − dist_{1}(f, P_{n}) < ε. Multiplying (1) and (2) by 1/2 and adding them together we get 1/2(∥f − p_{1}∥_{1} + ∥f − p_{2}∥_{1}) − dist_{1}(f, P_{n}) < ε. By the triangle inequality for the L_{1}-norm, 1/2(∥2f − p_{1} − p_{2}∥_{1}) − dist_{1}(f, P_{n}) < ε, i.e. ∥f − p∥_{1} − dist_{1}(f, P_{n}) < ε. □

Remark 3.5 The reader may have noticed that from (1) to (2) we changed from ≤ to < in the premise of the implication. The reason we wrote ≤ first was just to show that the lemma could be written in the form of A (from theorem 2.1) and that a functional realizing δ was guaranteed by our meta-theorem. Since a ≤ b/2 implies a < b (and the reverse implication holds without the factor 1/2) we normally write the relation that yields the optimal bound. When analysing the following lemmas we often claim that some sentence is an instance of our meta-theorem 2.1 without bothering to write it explicitly in the form of A. We hope the reader can see that through the implications mentioned above these lemmas could in fact be written in the form of A.

3.4 Lemma A ∧ B → C [Definition of L_{1}-norm]

The lemma states,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n} ( ⋀_{i=1}^{2}(∥f − p_{i}∥_{1} = dist_{1}(f, P_{n})) → ∥f − p∥_{1} − 1/2∥f − p_{1}∥_{1} − 1/2∥f − p_{2}∥_{1} = 0).

After presenting the hidden quantifiers and performing the functional interpretation we come again to the same logical structure of the formula in theorem 2.1, and again we know that there must exist a functional Φ_{2} depending at most on n, f and ε such that,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; ε ∈ Q_{+}^{∗}

( ⋀_{i=1}^{2}(∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < Φ_{2}(f, n, ε)) → | ∥f − p∥_{1} − 1/2∥f − p_{1}∥_{1} − 1/2∥f − p_{2}∥_{1} | < ε).

Again, the choice of Φ_{2} is simple, Claim 3.6 The functional Φ_{2}(f, n, ε) := Φ_{2}(ε) := ε does the job. Proof: Suppose (1) ∥f − p_{1}∥_{1} − dist_{1}(f, P_{n}) < ε and (2) ∥f − p_{2}∥_{1} − dist_{1}(f, P_{n}) < ε. By previous lemma we have (3) ∥f − p∥_{1} − dist_{1}(f, P_{n}) < ε. And \frac{(1)+(2)}{2} gives (4) 1/2(∥f − p_{1}∥_{1} + ∥f − p_{2}∥_{1}) − dist_{1}(f, P_{n}) < ε. From (3) and (4), we have, | ∥f − p∥_{1} − 1/2∥f − p_{1}∥_{1} − 1/2∥f − p_{2}∥_{1} | < ε – we used a ∈ [0, m) and b ∈ [0, m) then |a − b| ∈ [0, m). □

15Note that in fact Φ_{1} is independent of n and f. We adopt the convention that parameters not used in the definition of the functionals will be dropped.

3.5 Lemma C_{1} [Continuity of g(x)]

Let g(x) := |f_{0}(x)| − \frac{1}{2}|f(x) − p_{1}(x)| − \frac{1}{2}|f(x) − p_{2}(x)|. Based on the continuity of f, p_{1} and p_{2} we derive that g is continuous,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; ε ∈ Q_{+}^{∗}; x, y ∈ [0, 1]∃δ ∈ Q_{+}^{∗}

(|x − y| ≤ δ → |g(x) − g(y)| < ε).

Note that here we can again apply the meta-theorem 2.1 and we are sure to find a function Δ depending only f, n and ε such that,^{16}

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; ε ∈ Q_{+}^{∗}; x, y ∈ [0, 1]

(|x − y| < Δ(f, n, ε) → |g(x) − g(y)| < ε).

We write Δ(f, n, ε) as ω_{f,n}(ε). In this section we show how the modulus of continuity ω_{f,n}(ε) can be computed using only n, the modulus of continuity of f, ω_{f}, and an upper bound M_{f} ≥ ∥f∥_{∞} (in section 4 we show that we just need M_{f} ≥ sup_{x∈[0,1]} |f(x) − f(0)|, for instance ⌈\frac{1}{ω_{f} (1)}⌉, so that the final result only depends on ω_{f}). 3.5.1 Modulus of the sum Given the moduli of continuity ω_{f} and ω_{g} for the functions f and g respectively, we find the modulus of continuity for f + g, ω_{f+g}, in the following way. We have,

|x − y| < ω_{f}(ε/2) → |f(x) − f(y)| < ε/2.

|x − y| < ω_{g}(ε/2) → |g(x) − g(y)| < ε/2. Therefore, |x − y| < min{ω_{f}(ε/2), ω_{g}(ε/2)} → (|f(x) − f(y)| < ε/2 ∧ |g(x) − g(y)| < ε/2). |x − y| < min{ω_{f}(ε/2), ω_{g}(ε/2)} → |f(x) + g(x) − f(y) − g(y)| < ε.

16Here it is fundamental that p_{1} and p_{2} live in the compact space K_{f,n} otherwise the modulus of continuity for g would depend also on these elements and we would be unable to get a uniform modulus of uniqueness at the end.

Hence, ω_{f+g}(ε) = min{ω_{f}(ε/2), ω_{g}(ε/2)}.

3.5.2 Modulus of a constant times a function We show that ω_{af}(ε) = ω_{f}(\frac{ε}{a}), for all a ∈ Q_{+}^{∗},

|x − y| < ω_{f}(\frac{ε}{a}) → |f(x) − f(y)| < \frac{ε}{a},

|x − y| < ω_{f}(\frac{ε}{a}) → |af(x) − af(y)| < ε,

|x − y| < ω_{af}(ε) → |af(x) − af(y)| < ε. 3.5.3 Modulus of p_{1} and p_{2} Let p_{i} ∈ K_{f,n}. Then ∥p_{i}∥_{1} ≤ \frac{5}{2}∥f∥_{1} ≤ \frac{5}{2}∥f∥_{∞}. If p_{i}(x) = a_{n}x^{n} + … + a_{1}x + a_{0} and p_{i}^{∗}(x) = \frac{a_{n}x^{n+1}}{n+1} + … + \frac{a_{1}x^{2}}{2} + a_{0}x then for all x ∈ [0, 1] we have,

|p_{i}^{∗}(x)| = | ∫_{0}^{x} p_{i}(x)dx| ≤ ∫_{0}^{x} |p_{i}(x)|dx ≤ ∥p_{i}∥_{1} ≤ \frac{5}{2}∥f∥_{∞}. By Markov’s inequality (see e.g. [7]),

∥p_{i}∥_{∞} = ∥(p_{i}^{∗})′∥_{∞} ≤ 2(n + 1)^{2}(\frac{5}{2}∥f∥_{∞}) = 5(n + 1)^{2}∥f∥_{∞}. If we apply Markov’s inequality once more we get,

∥p′_{i}∥_{∞} ≤ 2n^{2}5(n + 1)^{2}∥f∥_{∞} < 10(n + 1)^{4}∥f∥_{∞}. By the mean value theorem this implies that p_{i} has Lipschitz constant 10(n + 1)^{4}∥f∥_{∞} on [0, 1], i.e. \frac{ε}{10(n+1)^{4}∥f∥_{∞}} is a modulus of uniform continuity for p_{i} on [0, 1]. Given an upper bound M_{f} on ∥f∥_{∞} we have,^{17}

ω_{p_{i}}(ε) := \frac{ε}{10(n + 1)^{4}M_{f}} .

Remark 3.7 Here we present how one gets a bound on the coefficients of p given ∥p∥_{1} (or some bound on ∥p∥_{1}). Let p^{i} denote the i-th derivative of p. Above we have shown that ∥p∥_{∞} ≤ 2(n + 1)^{2}∥p∥_{1} which by Markov’s inequality yields (1) ∥p^{i}∥_{∞} ≤ (2(n + 1)^{2})^{i+1}∥p∥_{1}. Since p^{i}(x) = \frac{n!}{(n−i)!}a_{n}x^{n−i} + … + i!a_{i}, from (1) we get |i! a_{i}| ≤ (2(n + 1)^{2})^{i+1}∥p∥_{1} which implies |a_{i}| ≤ \frac{(2(n+1)^{2})^{i+1}}{i!} ∥p∥_{1}. 3.5.4 The modulus of continuity ω_{f,n} Now we can present ω_{f,n} as a function of ω_{f} and n (note that we can take ω_{|f|} := ω_{f}),

17It should be clear that given f together with its modulus of continuity, ω_{f}, there is a simple algorithm to compute M_{f}, just take for instance M_{f} := max\{|f(i.ω_{f} (1))| : 0 ≤ i ≤ ⌊ \frac{1}{ω_{f} (1)} ⌋\} + 1.

ω_{f,n}(ε) = min{ω_{|f−p|}(ε/2), ω_{1/2|f−p_{1}|}(ε/4), ω_{1/2|f−p_{2}|}(ε/4)}
= min{ω_{f−p}(ε/2), ω_{f−p_{1}}(ε/2), ω_{f−p_{2}}(ε/2)}
= min{ω_{f}(ε/4), ω_{p_{1}}(ε/4), ω_{p_{2}}(ε/4)}
= min\{ω_{f}(\frac{ε}{4}), \frac{ε}{40(n + 1)^{4}M_{f}} \}.

3.6 Lemma C ∧ C_{1} → D [Integrand is ≤ 0 and continuous]

Let g(x) := |f(x) − p(x)| − 1/2|f(x) − p_{1}(x)| − 1/2|f(x) − p_{2}(x)|. The lemma says,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}( ∫_{0}^{1} g(x)dx = 0 → ∀x ∈ [0, 1](g(x) = 0)). After presenting the hidden quantifiers and applying functional interpretation we observe that again we can apply theorem 2.1, and we are guaranteed to find a functional Φ_{3}(f, n, ε) such that,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; ε ∈ Q_{+}^{∗}(| ∫_{0}^{1} g(x)dx| ≤ Φ_{3}(f, n, ε) → ∥g∥_{∞} ≤ ε). Let ω_{f,n}(ε) : Q_{+}^{∗} → Q_{+}^{∗} denote the modulus of uniform continuity of the function g ∈ C[0, 1], proved to exist in the analysis of lemma C_{1} (section 3.5).

Claim 3.8 The functional Φ_{3}(f, n, ε) := Φ_{3}(ω_{f,n}, ε) := \frac{ε}{2}. min\{\frac{1}{2}, ω_{f,n}(\frac{ε}{2})\} does the job.

Proof: Assume ∥g∥_{∞} > ε, since ∀x ∈ [0, 1]g(x) ≤ 0 we conclude ∃x_{0} ∈ [0, 1]g(x_{0}) < −ε. By the continuity of g we also have,

∀x ∈ [0, 1](|x − x_{0}| < ω_{f,n}(ε/2) → g(x) < −ε/2).

If x_{0} < 1/2 then,

| ∫_{0}^{1} g(x)dx| > | ∫_{x_{0}}^{min\{1,x_{0}+ω_{f,n}(ε/2)\}} −ε/2 dx| = \frac{ε}{2} min\{\frac{1}{2}, ω_{f,n}(\frac{ε}{2})\},

otherwise (x_{0} ≥ 1/2),

| ∫_{0}^{1} g(x)dx| > | ∫_{max\{0,x_{0}−ω_{f,n}(ε/2)\}}^{x_{0}} −ε/2 dx| = \frac{ε}{2} min\{\frac{1}{2}, ω_{f,n}(\frac{ε}{2})\}.

From this we conclude,

| ∫_{0}^{1} g(x)dx| > \frac{ε}{2} min\{\frac{1}{2}, ω_{f,n}(\frac{ε}{2})\}. □

3.7 Lemma D → K [If f_{0}(x) = 0 then p_{1}(x) = p_{2}(x)]

Let f_{1}(x) := 1/2(|f(x) − p_{1}(x)| + |f(x) − p_{2}(x)|), the lemma says,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; x ∈ [0, 1]

(∥ |f_{0}| − f_{1}∥_{∞} = 0 → (|f_{0}(x)| = 0 → p_{1}(x) = p_{2}(x))).

Again we are sure to find functionals Φ_{4}(f, n, ε) and Φ_{5}(f, n, ε) such that,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; x ∈ [0, 1]; ε ∈ Q_{+}^{∗} (∥ |f_{0}| − f_{1}∥_{∞} ≤ Φ_{4}(f, n, ε) → (|f_{0}(x)| ≤ Φ_{5}(f, n, ε) → |p_{1}(x) − p_{2}(x)| ≤ ε)).

Claim 3.9 The functionals Φ_{4}(f, n, ε) := Φ_{4}(ε) := ε/8 and Φ_{5}(f, n, ε) := Φ_{5}(ε) := ε/8 do

the job. Proof: Trivial. □

3.8 Lemma F → G [If p has n + 1 roots then p = 0]

The lemma states that if p_{1}(x) − p_{2}(x) has n + 1 distinct roots then ∀x ∈ [0, 1]p_{1}(x) = p_{2}(x),

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}∀x_{0}, …, x_{n} ∈ [0, 1]

( ⋀_{i=1}^{n}(x_{i} < x_{i+1}) ∧ ⋀_{i=0}^{n}(p_{1}(x_{i}) = p_{2}(x_{i})) → ∥p_{1} − p_{2}∥_{∞} = 0)

Then we present the hidden quantifiers and apply functional interpretation,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; r, ε ∈ Q_{+}^{∗}; x_{0}, …, x_{n} ∈ [0, 1]∃δ ∈ Q_{+}^{∗}

( ⋀_{i=1}^{n}(x_{i−1} + r ≤ x_{i}) ∧ ⋀_{i=0}^{n}(|p_{1}(x_{i}) − p_{2}(x_{i})| ≤ δ) → ∥p_{1} − p_{2}∥_{∞} ≤ ε)

By theorem 2.1 we are sure to find a functional Φ_{6} realizing δ.

Claim 3.10 The functional Φ_{6}(f, n, r, ε) := Φ_{6}(n, r, ε) := \frac{⌊n/2⌋!⌈n/2⌉!r^{n}}{(n+1)} ε does the job.

Proof: See [15], pages 82–83. □

Remark 3.11 In fact, the functional Φ_{6} does the job for p_{1}, p_{2} ∈ P_{n} (not only for p_{1}, p_{2} ∈ K_{f,n}).

3.9 Lemma B → ∀h H(h) [Definition of best L_{1}-approximation]

This lemma is a trivial consequence of the definition of dist_{1},

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}(∥f_{0}∥_{1} = dist_{1}(f, P_{n}) → ∀h ∈ P_{n}(∥f_{0} − h∥_{1} ≥ ∥f_{0}∥_{1})).

We can easily find a functional Φ_{7}(f, n, ε) s.t.,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; ε ∈ Q_{+}^{∗} (∥f_{0}∥_{1} − dist_{1}(f, P_{n}) ≤ Φ_{7}(f, n, ε) → ∀h ∈ P_{n}(∥f_{0} − h∥_{1} + ε ≥ ∥f_{0}∥_{1})).

Claim 3.12 The functional Φ_{7}(f, n, ε) := Φ_{7}(ε) := ε does the job.

Proof: Assume (1) ∥f_{0}∥_{1} − dist_{1}(f, P_{n}) ≤ ε. By the definition of dist_{1} we have for any h ∈ P_{n} (2) ∥f_{0} − h∥_{1} ≥ dist_{1}(f, P_{n}). From (1) and (2) we have ∥f_{0} − h∥_{1} + ε ≥ ∥f_{0}∥_{1}. □

3.10 Lemma ∀\overline{x}, h (∀λH(λh) ∧ I(\overline{x}, \overline{σ}′, h) → J(\overline{x})) [lemma 1]

This is the most intricate lemma used in the proof and therefore we analyze it in greater detail. We first rewrite the lemma in order to show how it is used in the proof of Jackson’s theorem in [7].

Lemma 1 Let f ∈ C[0, 1] and h, p_{1}, p_{2} ∈ P_{n}. If f_{0} has at most n roots then either ∫_{0}^{1}(h(x) sgn(f_{0})(x))dx = 0 or there exists a λ ∈ IR such that ∫_{0}^{1} |f_{0}(x) − λh(x)|dx < ∫_{0}^{1} |f_{0}(x)|dx.

Proof: Assume that all the roots of f_{0} are among 0 = x_{0} ≤ x_{1} ≤ … ≤ x_{n+1} = 1 and w.l.g. assume that ∫_{0}^{1}(h(x) sgn(f_{0})(x))dx > 0. Let B′ := ⋃_{i=0}^{n+1}(x_{i} − r, x_{i} + r) and B := B′ ⋂[0, 1]. Let A := [0, 1]\B. Make r small enough so that ∫_{A}(h(x) sgn(f_{0})(x))dx > ∫_{B} |h(x)|dx. Note that A is a finite union of closed intervals which contain no roots of f_{0}, therefore δ := min{|f_{0}(x)| : x ∈ A} is positive. Hence we can find a λ such that 0 < λ∥h∥_{∞} < δ, and for points x ∈ A, sgn(f_{0} − λh)(x) = sgn(f_{0})(x), which implies (see [7] or the proof of claim 3.13 for details) that ∫_{0}^{1} |f_{0}(x) − λh(x)|dx < ∫_{0}^{1} |f_{0}(x)|dx. □

The contraposition of the above stated lemma is then used in the proof. Now we analyze the logical structure of the lemma in order to discover which functionals can be extracted and what their dependencies are:

3.10.1 Logical analysis

First we replace P_{n} with K_{f,n} in the statement of lemma 1. Then we rewrite the integral of h sgn(f_{0}) over the interval [0, 1] as a sum of integrals over smaller intervals (which are guaranteed by the premise to contain no root of f_{0}) as described in section 3.1. In this way lemma 1 can be formally written as,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; x_{1} ≤ … ≤ x_{n} ∈ [0, 1]; h ∈ P_{n} (∀y ∈ [0, 1](f_{0}(y) = 0 → ⋁_{i=0}^{n+1} x_{i} = y) →

∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x)dx = 0 ∨ ∃λ ∈ IR(∥f_{0} − λh∥_{1} < ∥f_{0}∥_{1}))

where σ_{i} := sgn(f_{0})(\frac{x_{i−1}+x_{i}}{2} ), x_{0} := 0 and x_{n+1} := 1. The above formula implies^{18} (relative to E-PA^{ω}),

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; x_{1} ≤ … ≤ x_{n} ∈ [0, 1]; h ∈ P_{n}; η, δ ∈ Q_{+}^{∗}

∃r, l ∈ Q_{+}^{∗}(∀y ∈ [0, 1](|f_{0}(y)| < δ → ⋁_{i=0}^{n+1} |x_{i} − y| ≤ r) →

| ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x)dx| < η ∨ ∃λ ∈ IR(∥f_{0} − λh∥_{1} + l < ∥f_{0}∥_{1}))

Here we notice that η can be eliminated since h/η ∈ P_{n},

(∗) \{ \begin{matrix}∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; x_{1} ≤ … ≤ x_{n} ∈ [0, 1]; h ∈ P_{n}; δ ∈ Q_{+}^{∗} \\ ∃r, l ∈ Q_{+}^{∗}(∀y ∈ [0, 1](|f_{0}(y)| < δ → ⋁_{i=0}^{n+1} |x_{i} − y| ≤ r) → \\ | ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x)dx| < 1 ∨ ∃λ ∈ IR(∥f_{0} − λh∥_{1} + l < ∥f_{0}∥_{1})) \end{matrix}

3.10.2 Functionals realizing lemma 1

By observing that (∗) has (relative to E-PA^{ω}) the same logical form as the formula A in the meta-theorem 2.1 we are sure to find functionals Φ_{8}(f, n, δ, h) and Φ_{9}(f, n, δ, h) such that,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; x_{1} ≤ … ≤ x_{n} ∈ [0, 1]; h ∈ P_{n}; δ ∈ Q_{+}^{∗}

(∀y ∈ [0, 1](|f_{0}(y)| < δ → ⋁_{i=0}^{n+1} |x_{i} − y| ≤ Φ_{9}(f, n, δ, h)) →

| ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x)dx| < 1 ∨ ∃λ ∈ IR(∥f_{0} − λh∥_{1} + Φ_{8}(f, n, δ, h) < ∥f_{0}∥_{1})).

18In fact the formula we obtain below is a weakening of lemma 1. It will turn out in the course of the extraction that it is sufficient to consider this weakened form to get the final result.

Claim 3.13 The functionals Φ_{8}(f, n, δ, h) := Φ_{8}(n, δ, h) := \frac{δ}{3∥h∥_{∞}} and

Φ_{9}(f, n, δ, h) := Φ_{9}(n, h) := \frac{1}{6(n+1)∥h∥_{∞}} do the job.^{19}

Proof: We have to prove that,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; x_{1} ≤ … ≤ x_{n} ∈ [0, 1]; h ∈ P_{n}; δ ∈ Q_{+}^{∗}

(∀y ∈ [0, 1](|f_{0}(y)| < δ → ⋁_{i=0}^{n+1} |x_{i} − y| ≤ \frac{1}{6(n+1)∥h∥_{∞}}) → | ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x)dx| ≤ 1 ∨ ∃λ ∈ IR(∥f_{0} − λh∥_{1} + \frac{δ}{3∥h∥_{∞}} < ∥f_{0}∥_{1})).

For simplicity we define r := \frac{1}{6(n+1)∥h∥_{∞}}. Note that now we do not require y (in the above formula) to be a root of f_{0} but a δ-root (i.e. |f_{0}(y)| < δ). As a consequence y will not necessarily be equal to one of the x_{i}’s but only ‘r-close’ to some x_{i}, we say that y belongs to the (x_{i}, r)-cluster.^{20} Now we follow the original proof. Take n points, x_{1}, …, x_{n}, such that (1) 0 = x_{0} ≤ x_{1} ≤ … ≤ x_{n+1} = 1 and suppose that (2) all δroots of f_{0} belong to at least one of the (x_{i}, r)- clusters. Moreover, suppose w.l.g. that (3) ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x)dx > 1. Let B′ := ⋃_{i=0}^{n+1}(x_{i} − r, x_{i} + r), B := [0, 1] ⋂ B′ and A := [0, 1]\B. Note that A can be written as the union of smaller (possibly containing a single point) intervals A_{i} := [x_{i−1} + min\{r, \frac{x_{i}−x_{i−1}}{2} \}, x_{i} − min\{r, \frac{x_{i}−x_{i−1}}{2} \}], for 1 ≤ i ≤ n + 1. Therefore by assumption (2) we have sgn(f_{0})(x) = σ_{i}, for x ∈ A_{i}, where σ_{i} = sgn(f_{0})(\frac{x_{i−1}+x_{i}}{2} ), and then ∑_{i=1}^{n+1} σ_{i} ∫_{A_{i}} h(x) dx = ∫_{A}(h(x) sgn(f_{0})(x)) dx. Following the original proof we would have to shrink B until ∫_{B} |h(x)|dx ≤ 1/3, but ∫_{B} |h(x)|dx ≤ |B| · ∥h∥_{∞} ≤ (n + 1)\frac{1}{3(n+1)∥h∥_{∞}} ∥h∥_{∞} = 1/3. Then by (3) we get (4) ∫_{A}(h(x) sgn(f_{0})(x))dx > 1/3 + ∫_{B} |h(x)|dx. And by the definition of A and (2) we have min\{|f_{0}(x)| : x ∈ A\} ≥ δ, therefore taking λ := \frac{δ}{∥h∥_{∞}} we have (5) sgn(f_{0} − λh)(x) = sgn(f_{0})(x), for x ∈ A. Hence,

19In order to be precise we should have written max{1, ∥h∥_{∞}} instead of ∥h∥_{∞} in the definition of Φ_{8} and Φ_{9}, so that they are always defined. This can be seen to be not necessary because we only apply these functionals to an h with uniform norm different from zero (see section 3.12). For another comment on the norm of the function h see remark 3.14.

20This weakening is fundamental to the elimination of the WKL, as mentioned in section 3.1. We discuss this point in more details in section 3.10.3.

∥f_{0} − λh∥_{1} = ∫_{A} |f_{0} − λh| − ∫_{B} |f_{0} − λh|
=^{(5)} ∫_{A}(f_{0} − λh) sgn(f_{0}) + ∫_{B} |f_{0} − λh|
= ∫_{A} f_{0} sgn(f_{0}) − λ ∫_{A} h sgn(f_{0}) + ∫_{B} |f_{0} − λh|
≤ ∫_{A} f_{0} sgn(f_{0}) − λ ∫_{A} h sgn(f_{0}) + ∫_{B} |f_{0}| + λ ∫_{B} |h|
= ∫_{A} |f_{0}| + ∫_{B} |f_{0}| + λ ∫_{B} |h| − λ ∫_{A} h sgn(f_{0})

= ∫_{0}^{1} |f_{0}| + λ ∫_{B} |h| − λ ∫_{A} h sgn(f_{0}).

Now we can add \frac{δ}{3∥h∥_{∞}} on both sides of the inequality and put λ = \frac{δ}{∥h∥_{∞}} in evidence to get,

∥f_{0} − λh∥_{1} + \frac{δ}{3∥h∥_{∞}} ≤ ∥f_{0}∥_{1} + \frac{δ}{∥h∥_{∞}} (1/3 + ∫_{B} |h| − ∫_{A} h sgn(f_{0}))
<^{(4)} ∥f_{0}∥_{1}. □

As we mentioned, the lemma is going to be used in the contrapositive form,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; x_{1} ≤ … ≤ x_{n} ∈ [0, 1]; h ∈ P_{n}; δ ∈ Q_{+}^{∗}

(∀λ ∈ IR(∥f_{0} − λh∥_{1} + \frac{δ}{3∥h∥_{∞}} ≥ ∥f_{0}∥_{1}) ∧ ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x)dx > 1 →

∃y ∈ [0, 1](|f_{0}(y)| < δ ∧ ⋀_{i=0}^{n+1} |x_{i} − y| > \frac{1}{6(n+1)∥h∥_{∞}})).

Remark 3.14 The functionals Φ_{8} and Φ_{9} should range over Q_{+}^{∗}, but ∥h∥_{∞} ∈ IR_{+}. Therefore, we should have written ∥h∥_{∞,Q} instead of ∥h∥_{∞} in the definition of Φ_{8} and Φ_{9}, where ∥h∥_{∞,Q} is a rational upper bound on ∥h∥_{∞}.

3.10.3 Elimination of WKL

As we discussed already in the introduction, the logical method of monotone functional interpretation on which the proof of the general logical meta-theorem is based upon not only provides an algorithm for the extraction of the modulus of uniqueness Φ but also a constructive verification of Φ which can be formalized in intuitionistic arithmetic in all finite types HA^{ω}. In particular, we get from this that Jackson’s theorem is provable in HA^{ω} despite the fact that Cheney’s proof heavily relies on classical logic and the non-computational binary König’s lemma WKL. We will not carry out the details of this intuitionistic verification since we focus in this paper on the applied aspect of constructing Φ. However, in 3.10.2 above we can see already how the constructivisation of Cheney’s proof comes out of our analysis: as said before, WKL is used in the equivalent (see [25])^{21} form of

(+) ∀f ∈ C[0, 1]∀a, b ∈ [0, 1](a < b → ∃x_{0} ∈ [a, b](f(x_{0}) = inf_{x_{0}∈[a,b]} f(x)))

to conclude

∀x ∈ [x_{i} + r, x_{i+1} − r](f(x) > 0) → inf_{x∈[x_{i}+r,x_{i+1}−r]} f(x) > 0.

After our replacement of ‘roots x_{i}’ by ‘r-clusters of δ-roots’ this transforms into

∀x ∈ [x_{i} + r, x_{i+1} − r](f(x) > δ) → inf_{x∈[x_{i}+r,x_{i+1}−r]} f(x) ≥ δ

which follows from the constructively valid ‘ε-weakening’

(+)_{ε} \{ \begin{matrix}∀f ∈ C[0, 1]∀a, b ∈ [0, 1] \\ (a < b → ∀ε > 0∃x_{0} ∈ [a, b](f(x_{0}) − inf_{x_{0}∈[a,b]} f(x) < ε)) \end{matrix}

version of (+) which eliminates the use of WKL. Also the use of classical logic to find σ_{i} such that

σ_{i} =_{0} 0 ↔ f(\frac{x_{i} + x_{i+1}}{2} ) ≥_{IR} 0

is no longer necessary since we now have that

f(\frac{x_{i} + x_{i+1}}{2} ) ≥_{IR} δ ∨ f(\frac{x_{i} + x_{i+1}}{2} ) ≤_{IR} −δ

which can easily be decided since δ ∈ Q_{+}^{∗}.

3.11 Lemma ∀\overline{x}, \overline{σ}∃h I(\overline{x}, \overline{σ}, h)

In the second part of Cheney’s proof he considers the case where f_{0} has less than n + 1 roots, from this assumption he arrives at a contradiction (using lemma 1) when assuming that for any h ∈ P_{n}, ∫ h sgn(f_{0}) = 0. Here we show that for any given n points x_{1} ≤ … ≤ x_{n} in the interval [0, 1] and for any σ_{1}, …, σ_{n+1} ∈ {−1, 1} (where σ_{i} will denote the sign of the function f_{0} in the interval [x_{i−1}, x_{i}]) it is possible to find a function h ∈ P_{n} such that ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h > 0, where x_{0} = 0 and x_{n+1} = 1. Formally,

21Note that f ∈ C[0, 1] is given together with a modulus of uniform continuity ω_{f}.

∀n ∈ IN; x_{1} ≤ … ≤ x_{n} ∈ [0, 1]; σ_{1}, …, σ_{n+1} ∈ {−1, 1}∃h ∈ P_{n}( ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h > 0).

In the same way as we did in section 3.10.1 we present the hidden quantifier η in the inequality and since h/η ∈ P_{n} we have,

∀n ∈ IN; x_{1} ≤ … ≤ x_{n} ∈ [0, 1]; σ_{1}, …, σ_{n+1} ∈ {−1, 1}∃h ∈ P_{n}( ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h > 1).

The sentence above states the existence of a function h ∈ P_{n}, therefore there exists also a k ∈ Q_{+}^{∗} such that, in the interval [0, 1], k ≥ ∥h∥_{∞}. Here we can again apply our meta-theorem 2.1 and we are sure to find a function Φ_{10} depending only on n such that,^{22}

∀n ∈ IN; x_{1} ≤ … ≤ x_{n} ∈ [0, 1]; σ_{1}, …, σ_{n+1} ∈ {−1, 1}∃h ∈ P_{n} ( ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h > 1 ∧ Φ_{10}(n) ≥ ∥h∥_{∞}).

Claim 3.15 The function Φ_{10}(n) := 3^{n+1}(n + 1)^{n+1} does the job.

Before we give the proof for Claim 3.15 we need,

Claim 3.16 Let y_{1}, …, y_{m} be points in [0, 1] such that y_{1} < y_{2} < … < y_{m}. Define h(x) := a(x − y_{1}) … (x − y_{m}). For any a ∈ IR^{∗} and any two points x_{0} < x_{1} in [0, 1] such that h has no roots inside [x_{0}, x_{1}],

∫_{x_{0}}^{x_{1}} |h(x)|dx > \frac{x_{1} − x_{0}}{3} min\{|h(x_{0} + \frac{x_{1} − x_{0}}{3} )|, |h(x_{1} − \frac{x_{1} − x_{0}}{3} )|\}.

Proof: It is sufficient to show that for any x ∈ (x_{0} + \frac{x_{1}−x_{0}}{3} , x_{1} − \frac{x_{1}−x_{0}}{3} ),

|h(x)| ≥ min\{|h(x_{0} + \frac{x_{1} − x_{0}}{3} )|, |h(x_{1} − \frac{x_{1} − x_{0}}{3} )|\}.

Let y_{0} = 0 and y_{m+1} = 1. First note that y_{i} ≤ x_{0} < x_{1} ≤ y_{i+1} for some 0 ≤ i < m, where at least one of y_{i} and y_{i+1} is a root of h (w.l.g. say that y_{i} is a root of h). Now suppose that there is an x^{∗} ∈ (x_{0} + \frac{x_{1}−x_{0}}{3} , x_{1} − \frac{x_{1}−x_{0}}{3} ) such that |h(x^{∗})| < min\{|h(x_{0} + \frac{x_{1}−x_{0}}{3} )|, |h(x_{1} − \frac{x_{1}−x_{0}}{3} )|\}. Then clearly h has a local minimum inside the interval (x_{0} + \frac{x_{1}−x_{0}}{3} , x_{1} − \frac{x_{1}−x_{0}}{3} ). On the other hand since |h(y_{i})| ≤ |h(x_{0} + \frac{x_{1}−x_{0}}{3} )| and |h(x^{∗})| ≤ |h(x_{0} + \frac{x_{1}−x_{0}}{3} )| (and y_{i} < x_{0} + \frac{x_{1}−x_{0}}{3} < x^{∗}) the polynomial h has a local maximum in the interval (y_{i}, x^{∗}). But we know in advance that h has at least one local extremum in each interval (y_{i}, y_{i+1}), 1 ≤ i < m. Since we have m − 1 intervals we have found already m local extrema, a contradiction since the derivative of h has degree m − 1. □

22Note that Φ_{10} does not depend on the points x_{1}, …, x_{n} neither on the σ’s since they are elements from compact spaces.

Proof of Claim 3.15: The claim states that for any given points 0 = x_{0} ≤ x_{1} ≤ … ≤ x_{n+1} = 1 and for any σ_{1}, …, σ_{n+1} ∈ {−1, 1} there exists an h ∈ P_{n} such that ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x)dx > 1, and ∥h∥_{∞} ≤ 3^{n+1}(n + 1)^{n+1}. Let 0 = x_{0} ≤ x_{1} ≤ … ≤ x_{n+1} = 1 and σ_{1}, …, σ_{n+1} ∈ {−1, 1} be given. Ignore all the points x_{j} such that x_{i} = x_{j} and i < j. We are left with ñ+1 points 0 = x_{a_{0}} < x_{a_{1}} < … < x_{a_{ñ+1}} = 1 where a_{i−1} < a_{i}, a_{i} ∈ {0, …, n+1} and ñ ≤ n. Let x̃_{i} := x_{a_{i}} and σ̃_{i} := σ_{a_{i}}. Since we have eliminated just empty intervals we

have for any function h ∈ P_{n}, ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x) dx = ∑_{i=1}^{ñ+1} σ̃_{i} ∫ x̃_{i} ; x̃_{i−1} h(x) dx. Among the

points x̃_{1}, …, x̃ñ pick only the points x̃_{i} for which σ̃_{i} ≠ σ̃_{i+1}. Finally, we are left with m + 1 points 0 = x̃_{b_{0}} < x̃_{b_{1}} < … < x̃_{b_{m+1}} = 1 where b_{i−1} < b_{i}, b_{i} ∈ {0, …, ñ + 1} and m ≤ ñ. Let

y_{i} := x̃_{b_{i}} and σ_{i}^{∗} := σ̃_{b_{i}}. Again we have ∑_{i=1}^{ñ+1} σ̃_{i} ∫ x̃_{i} ; x̃_{i−1} h(x)dx = ∑_{i=1}^{m+1} σ_{i}^{∗} ∫_{y_{i−1}}^{y_{i}} h(x)dx, for

any h ∈ P_{n}. Then we define h(x) := a(x − y_{1}) … (x − y_{m}) and choose the sgn(a) = (−1)^{j} (j ∈ {0, 1}) so that ∑_{i=1}^{m+1} σ_{i}^{∗} ∫_{y_{i−1}}^{y_{i}} h(x)dx = ∑_{i=1}^{m+1} ∫_{y_{i−1}}^{y_{i}} |h(x)|dx. Therefore, for this specific h we have (1) ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x)dx = ∑_{i=1}^{m+1} ∫_{y_{i−1}}^{y_{i}} |h(x)|dx = ∫_{0}^{1} |h(x)|dx.

By the pigeon hole principle for some i ∈ \{1, …, n + 1\} we have x_{i} − x_{i−1} ≥ \frac{1}{n+1}. Let i_{0} ∈ \{1, …, n + 1\} be such that x_{i_{0}} − x_{i_{0}−1} ≥ \frac{1}{n+1}. Then,

∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x)dx  =^{(1)}  ∫_{0}^{1} |h(x)|dx
≥  ∫_{x_{i_{0}}−1}^{x_{i_{0}}} |h(x)|dx
>^{Claim 3.16} \frac{x_{i_{0}} − x_{i_{0}−1}}{3} min\{|h(x_{i_{0}−1} + \frac{(x_{i_{0}} − x_{i_{0}−1})}{3})|,

|h(x_{i_{0}} − \frac{(x_{i_{0}} − x_{i_{0}−1})}{3})|\}

≥  \frac{1}{3(n + 1)} \frac{|a|}{3^{n}(n + 1)^{n}} = \frac{|a|}{3^{n+1}(n + 1)^{n+1}} .

Therefore, by choosing j ∈ {0, 1} appropriately and taking a := (−1)^{j}3^{n+1}(n+1)^{n+1} we have ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h(x)dx > 1 and ∥h∥_{∞} ≤ 3^{n+1}(n + 1)^{n+1}. □

3.12 Eliminating the function h in lemma 1

We have just shown that,

(1) ∀x_{1} ≤ … ≤ x_{n} ∈ [0, 1]; σ_{1}, …, σ_{n+1} ∈ {−1, 1}∃h ∈ P_{n} ( ∑_{i=1}^{n+1} σ_{i} ∫_{x_{i−1}}^{x_{i}} h > 1 ∧ Φ_{10}(n) ≥ ∥h∥_{∞}).

Let f ∈ C[0, 1], n ∈ IN, p_{1}, p_{2} ∈ K_{f,n} and x_{1} ≤ … ≤ x_{n} ∈ [0, 1] be fixed, and let h̃ be the function from (1) when σ_{i} := f_{0}(\frac{x_{i−1}+x_{i}}{2} ), where x_{0} := 0 and x_{n+1} := 1. Applying lemma 1 to h̃ we get,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; x_{1} ≤ … ≤ x_{n} ∈ [0, 1]; δ ∈ Q_{+}^{∗}

(∀λ ∈ IR(∥f_{0} − λh̃∥_{1} + Φ_{8}(n, δ, h̃) ≥ ∥f_{0}∥_{1}) →

∃y ∈ [0, 1](|f_{0}(y)| < δ ∧ ⋀_{i=0}^{n+1} |x_{i} − y| > Φ_{9}(n, h̃))).

We have ∥h̃∥_{∞} ≤ 3^{n+1}(n+1)^{n+1}. Let Φ̃_{8}(n, δ) := \frac{δ}{3^{n+2}(n+1)^{n+1}} and Φ̃_{9}(n) := \frac{1}{2·3^{n+2}(n+1)^{n+2}} .

By the monotonicity of the functionals Φ_{8} and Φ_{9} in ∥h∥_{∞} we have, Φ̃_{8}(n, δ) ≤ Φ_{8}(n, δ, h̃) and Φ̃_{9}(n) ≤ Φ_{9}(n, h̃). Then,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; x_{1} ≤ … ≤ x_{n} ∈ [0, 1]; δ ∈ Q_{+}^{∗}

(∀λ ∈ IR(∥f_{0} − λh̃∥_{1} + Φ̃_{8}(n, δ) ≥ ∥f_{0}∥_{1}) →

∃y ∈ [0, 1](|f_{0}(y)| < δ ∧ ⋀_{i=0}^{n+1} |x_{i} − y| > Φ̃_{9}(n))).

And we can conclude,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; δ ∈ Q_{+}^{∗}

(∀h ∈ P_{n}(∥f_{0} − h∥_{1} + Φ̃_{8}(n, δ) ≥ ∥f_{0}∥_{1}) →

∀x_{1} ≤ … ≤ x_{n} ∈ [0, 1]∃y ∈ [0, 1](|f_{0}(y)| < δ ∧ ⋀_{i=0}^{n+1} |x_{i} − y| > Φ̃_{9}(n))).

We can actually replace the conclusion of the implication above with the actual existence of n + 1 roots in the following way (lemma ∀\overline{x}J(\overline{x}) → E): Assume

(1) ∀x_{1} ≤ … ≤ x_{n} ∈ [0, 1]∃y ∈ [0, 1](|f_{0}(y)| < δ ∧ ⋀_{i=0}^{n+1} |x_{i} − y| > Φ̃_{9}(n))). If m < n + 1 is the biggest number of δ-roots of f_{0} which are pairwise apart from each other by at least Φ̃_{9}(n) then by (1) we have a contradiction. Hence,

∃x_{0}, …, x_{n} ∈ [0, 1](⋀_{i=0}^{n} |f_{0}(x_{i})| < δ ∧ ⋀_{i=1}^{n}(x_{i−1} + Φ̃_{9}(n) < x_{i})). Therefore, we have,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; δ ∈ Q_{+}^{∗}

(∀h ∈ P_{n}(∥f_{0} − h∥_{1} + Φ̃_{8}(n, δ) ≥ ∥f_{0}∥_{1}) → ∃x_{0}, …, x_{n} ∈ [0, 1](⋀_{i=0}^{n} |f_{0}(x_{i})| < δ ∧ ⋀_{i=1}^{n} x_{i−1} + Φ̃_{9}(n) < x_{i})).

4 The uniform modulus of uniqueness for

L_{1}-approximation

In this section we show how the computed functionals are combined in order to obtain the uniform modulus of uniqueness. Let f ∈ C[0, 1], n ∈ IN, p_{1}, p_{2} ∈ K_{f,n} and ε ∈ Q_{+}^{∗} be fixed. Assume (i ∈ {1, 2}),

(1) ∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < min{Φ_{1}(Φ_{7}(Φ̃_{8}(n, Φ_{5}(Φ_{6}(n, Φ̃_{9}(n), ε))))),

Φ_{1}(Φ_{2}(Φ_{3}(ω_{f,n}, Φ_{4}(Φ_{6}(n, Φ̃_{9}(n), ε)))))}.

By section 3.3 we have, (where f_{0}(x) = f(x) − \frac{p_{1}(x)+p_{2}(x)}{2})

∥f_{0}∥_{1} − dist_{1}(f, P_{n}) < Φ_{2}(Φ_{3}(ω_{f,n}, Φ_{4}(Φ_{6}(n, Φ̃_{9}(n), ε)))).

By section 3.4 (and since Φ_{1} is the identity),

| ∥f_{0}∥_{1} − 1/2∥f − p_{1}∥_{1} − 1/2∥f − p_{2}∥_{1} | < Φ_{3}(ω_{f,n}, Φ_{4}(Φ_{6}(n, Φ̃_{9}(n), ε))).

By section 3.6 (since ∫ |f_{0}| − \frac{1}{2}|f − p_{1}| − \frac{1}{2}|f − p_{2}| = ∥f_{0}∥_{1} − \frac{1}{2}∥f − p_{1}∥_{1} − \frac{1}{2}∥f − p_{2}∥_{1}),

∥ |f_{0}| − 1/2|f − p_{1}| − 1/2|f − p_{2}| ∥_{∞} ≤ Φ_{4}(Φ_{6}(n, Φ̃_{9}(n), ε)).

Hence, by section 3.7,

(2) ∀x ∈ [0, 1](|f_{0}(x)| ≤ Φ_{5}(Φ_{6}(n, Φ̃_{9}(n), ε)) → |p_{1}(x) − p_{2}(x)| ≤ Φ_{6}(n, Φ̃_{9}(n), ε)). By the same assumption (1) and section 3.3 we also have,

∥f_{0}∥_{1} − dist_{1}(f, P_{n}) < Φ_{7}(Φ̃_{8}(n, Φ_{5}(Φ_{6}(n, Φ̃_{9}(n), ε)))).

And by section 3.9,

∀h ∈ P_{n}(∥f_{0} − h∥_{1} + Φ̃_{8}(n, Φ_{5}(Φ_{6}(n, Φ̃_{9}(n), ε))) ≥ ∥f_{0}∥_{1}).

Hence, by section 3.12 (taking δ = Φ_{5}(Φ_{6}(n, Φ̃_{9}(n), ε))),

∃x_{0}, …, x_{n} ∈ [0, 1](⋀_{i=0}^{n} |f_{0}(x_{i})| < Φ_{5}(Φ_{6}(n, Φ̃_{9}(n), ε)) ∧ ⋀_{i=1}^{n} x_{i−1} + Φ̃_{9}(n) ≤ x_{i}). And by (2), ∃x_{0}, …, x_{n} ∈ [0, 1](⋀_{i=0}^{n} |p_{1}(x_{i}) − p_{2}(x_{i})| ≤ Φ_{6}(n, Φ̃_{9}(n), ε) ∧ ⋀_{i=1}^{n} x_{i−1} + Φ̃_{9}(n) ≤ x_{i}). Therefore, by section 3.8 (taking r = Φ̃_{9}(n)) we conclude,

(3) ∥p_{1} − p_{2}∥_{∞} ≤ ε.

If we substitute the linear functionals, Φ_{1}, Φ_{2}, Φ_{4}, Φ_{5} and Φ_{7}, to make the conclusion more legible, we have (1) → (3), ∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < min\{Φ̃_{8}(n, \frac{Φ_{6}(n,Φ̃_{9}(n),ε)}{8}), Φ_{3}(ω_{f,n}, \frac{Φ_{6}(n,Φ̃_{9}(n),ε)}{8})\} → ∥p_{1} − p_{2}∥_{∞} ≤ ε. After applying Φ̃_{8} and Φ̃_{9} we get,

∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < min\{^{\frac{Φ_{6}(n, \frac{1}{2.3^{n+2}(n+1)^{n+2}} ,ε)}{8·3^{n+2}(n+1)^{n+1}}}, Φ_{3}(ω_{f,n}, ^{\frac{Φ_{6}(n, \frac{1}{2·3^{n+2}(n+1)^{n+2}} ,ε)}{8}})\} →

∥p_{1} − p_{2}∥_{∞} ≤ ε.

Then we apply Φ_{6},

∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < min\{^{\frac{\frac{⌊n/2⌋!⌈n/2⌉!ε}{2^{n+3}3^{n^{2}+2n}(n+1)^{n^{2}+2n+1}}}{3^{n+2}(n+1)^{n+1}}} , Φ_{3}(ω_{f,n}, \frac{⌊n/2⌋!⌈n/2⌉!ε}{2^{n+3}3^{n^{2}+2n}(n+1)^{n^{2}+2n+1}} )\} →

∥p_{1} − p_{2}∥_{∞} ≤ ε.

Let c_{n} := \frac{⌊n/2⌋!⌈n/2⌉!}{2^{n+3}3^{n^{2}+2n}(n+1)^{n^{2}+2n+1}} then we can rewrite the above formula as,

∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < min\{\frac{c_{n}ε}{3^{n+2}(n+1)^{n+1}} , Φ_{3}(ω_{f,n}, c_{n}ε)\} → ∥p_{1} − p_{2}∥_{∞} ≤ ε. And finally we apply the definition of Φ_{3},

∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < min\{\frac{c_{n}ε}{3^{n+2}(n+1)^{n+1}} , \frac{c_{n}ε}{2}ω_{f,n}(\frac{c_{n}ε}{2})\} → ∥p_{1} − p_{2}∥_{∞} ≤ ε. Let Φ̃(f, n, ε) = min\{\frac{c_{n}ε}{3^{n+2}(n+1)^{n+1}} , \frac{c_{n}ε}{2}ω_{f,n}(\frac{c_{n}ε}{2})\}, where ω_{f,n} := min\{ω_{f}(\frac{ε}{4}), \frac{ε}{40(n+1)^{4}M_{f}} \} and M_{f} ≥ ∥f∥_{∞}. We have shown that,

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}

( ⋀_{i=1}^{2}(∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < Φ̃(f, n, ε)) → ∥p_{1} − p_{2}∥_{∞} ≤ ε).

Proposition 4.1 The functional Φ̃(f, n, ε) is a uniform modulus of uniqueness for the best L_{1}-approximation of C[0, 1] from K_{f,n}, i.e.

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ K_{f,n}; ε ∈ Q_{+}^{∗}

( ⋀_{i=1}^{2}(∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < Φ̃(f, n, ε)) → ∥p_{1} − p_{2}∥_{1} ≤ ε).

Proof: Above, plus the fact that ∥p_{1} − p_{2}∥_{1} ≤ ∥p_{1} − p_{2}∥_{∞}. □ Claim 4.2 Φ̃(f, n, ε) ≤ \frac{ε}{8} Proof: Trivial. □

Now we show that Proposition 4.1 can be generalised to the whole space P_{n} (i.e. we can replace K_{f,n} with P_{n}). Moreover, we notice that the dependency on particular values of the function f can be eliminated so that the modulus of uniqueness depends on f only through its modulus of continuity.

Theorem 4.3 Let Φ(ω, n, ε) = min\{\frac{c_{n}ε}{3^{n+2}(n+1)^{n+1}} , \frac{c_{n}ε}{2}ω_{n}(\frac{c_{n}ε}{2})\}, where the constant c_{n} :=

\frac{⌊n/2⌋!⌈n/2⌉!}{2^{n+3}3^{n^{2}+2n}(n+1)^{n^{2}+2n+1}} , ω_{n}(ε) := min\{ω(\frac{ε}{4}), _{\frac{ε}{40(n+1)^{4}⌈ \frac{1}{ω(1)} ⌉}}\}. For all f ∈ C[0, 1] with modu-

lus of continuity ω

∀n ∈ IN; p_{1}, p_{2} ∈ P_{n}; ε ∈ Q_{+}^{∗}( ⋀_{i=1}^{2}(∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < Φ(ω, n, ε)) → ∥p_{1} − p_{2}∥_{1} ≤ ε).

Proof: Actually, we prove the stronger version of the theorem where instead of ⌈\frac{1}{ω(1)}⌉ in the definition of ω_{n} we have any upper bound on sup_{x∈[0,1]} |f(x) − f(0)|. First we show that in Proposition 4.1 we can replace K_{f,n} with P_{n}. Suppose without loss of generality that p_{1} ∈ P_{n}\K_{f,n}. Then ∥p_{1}∥_{1} > \frac{5}{2}∥f∥_{1} and hence ∥f − p_{1}∥_{1} > \frac{3}{2}∥f∥_{1} ≥ \frac{3}{2}dist_{1}(f, P_{n}). Assume that ∥f − p_{i}∥_{1} < dist_{1}(f, P_{n}) + Φ̃(f, n, ε). By Claim 4.2, ∥f − p_{i}∥_{1} < dist_{1}(f, P_{n}) + \frac{ε}{8}. Then, \frac{ε}{8} > \frac{1}{2}dist_{1}(f, P_{n}), i.e. dist_{1}(f, P_{n}) < \frac{ε}{4}. Therefore ∥f − p_{i}∥_{1} < dist_{1}(f, P_{n}) + \frac{ε}{8} < \frac{ε}{2} and we have ∥p_{1} − p_{2}∥_{1} ≤ ε. The second point is that some upper bound M_{f} ≥ ∥f∥_{∞} is used to define ω_{f,n} in Proposition 4.1. We claim that an upper bound N_{f} ≥ sup_{x∈[0,1]} |f(x) − f(0)| is sufficient. For any function f ∈ C[0, 1] and polynomials p_{1}, p_{2} ∈ P_{n} let f̃, p̃_{1} and p̃_{2} be the functions obtained by the transposition of f, p_{1} and p_{2} respectively by f(0) (i.e. f̃(x) := f(x) − f(0) and p̃_{i}(x) := p_{i}(x)−f(0)). It is clear that (1) ∥f −p_{i}∥_{1} = ∥f̃−p̃_{i}∥_{1}, (2) dist_{1}(f, P_{n}) = dist_{1}(f̃, P_{n}) and (3) ∥p_{1} − p_{2}∥_{1} = ∥p̃_{1} − p̃_{2}∥_{1}. Let ω be the modulus of continuity for f and assume,

∥f − p_{i}∥_{1} < dist(f, P_{n}) + Φ(ω, n, ε),

by (1) and (2) we have, ∥f̃ − p̃_{i}∥_{1} < dist(f̃, P_{n}) + Φ(ω, n, ε). Since ω is also a modulus of continuity for f̃ and ∥f̃∥_{∞} = sup_{x∈[0,1]} |f(x) − f(0)| ≤ N_{f} we have Φ̃(f̃, n, ε) = Φ(ω, n, ε), therefore,

∥f̃− p̃_{i}∥_{1} < dist(f̃, P_{n}) + Φ̃(f̃, n, ε),

which implies, by Proposition 4.1, the first part of this proof and (3), ∥p_{1} − p_{2}∥_{1} ≤ ε. Since ⌈\frac{1}{ω(1)}⌉ ≥ sup_{x∈[0,1]} |f(x) − f(0)| if ω is a modulus of uniform continuity for f the theorem follows. □ A function f ∈ C[0, 1] is said to be Lipschitz continuous with Lipschitz constant λ ∈ IR_{+}^{∗} if |f(x)−f(y)| ≤ λ|x−y| (i.e. \frac{ε}{λ} is a modulus of continuity for f) and is Lipschitz-α continuous with constant λ, 0 < α ≤ 1, if |f(x) − f(y)| ≤ λ|x − y|^{α} (equivalently, (\frac{ε}{λ})^{1/α} is a modulus of continuity in our sense for f).^{23} In this way, if a function f is Lipschitz continuous (or Lipschitz-α continuous) with constant λ then sup_{x∈[0,1]} |f(x) − f(0)| ≤ λ (and we can take λ

instead of ⌈\frac{1}{ω(1)}⌉ in Theorem 4.3). Hence, theorem 4.3 implies,

Corollary 4.4 For any f ∈ C[0, 1],

i) let Φ_{L}(λ, n, ε) = min\{\frac{c_{n}ε}{3^{n+2}(n+1)^{n+1}} , \frac{c_{n}^{2}ε^{2}}{160(n+1)^{4}λ}\}. If f is Lipschitz continuous with constant λ then the functional Φ_{L} is a modulus of uniqueness for f.

ii) let Φ_{L_{α}}(λ, α, n, ε) = min\{\frac{c_{n}ε}{3^{n+2}(n+1)^{n+1}} , \frac{c_{n}ε}{2}(\frac{c_{n}ε}{8λ})^{1/α}, \frac{c_{n}^{2}ε^{2}}{160(n+1)^{4}λ}\}. If f is Lipschitz-α continuous with constant λ then the functional Φ_{L_{α}} is a modulus of uniqueness for f.

And as a corollary of proposition 5.4 from [15] and theorem 4.3 above we get,

Theorem 4.5 Let P(f, n) denote the operator which assigns to any given function f ∈ C[0, 1] and any n ∈ IN the best L_{1}-approximation of f ∈ C[0, 1] from P_{n}. Then Φ_{P} (ω_{f}, n, ε) := \frac{Φ(ω_{f} ,n,ε)}{2}, Φ as defined in Theorem 4.3, is a modulus of pointwise continuity for the operator P(f, n), i.e.,

∀f, f̃ ∈ C[0, 1]; n ∈ IN; ε ∈ Q_{+}^{∗}(∥f − f̃∥_{1} < Φ_{P} (ω_{f}, n, ε) → ∥P(f, n) − P(f̃, n)∥_{1} ≤ ε).

Proof: For completeness we reproduce here the proof as given in [15]. One easily verifies that dist_{1}(f, P_{n}) is Lipschitz continuous in f (with respect to the L_{1}-norm) with λ = 1, i.e.

(∗) ∥f − f̃∥_{1} < ε → |dist_{1}(f, P_{n}) − dist_{1}(f̃, P_{n})| < ε.

Assume now that ∥f − f̃∥_{1} < Φ_{P} (ω_{f}, n, ε) = \frac{1}{2}Φ(ω_{f}, n, ε). Then,

∥f − P(f̃, n)∥_{1} ≤ ∥f̃− P(f̃, n)∥_{1} + ∥f − f̃∥_{1} = dist_{1}(f̃, P_{n}) + ∥f − f̃∥_{1}
<^{(∗)} dist_{1}(f, P_{n}) + \frac{1}{2}Φ(ω_{f}, n, ε) + ∥f − f̃∥_{1}
< dist_{1}(f, P_{n}) + Φ(ω_{f}, n, ε).

Since, furthermore, ∥f −P(f, n)∥_{1} = dist_{1}(f, P_{n}), we obtain from theorem 4.3 that ∥P(f, n)− P(f̃, n)∥_{1} ≤ ε. □

23In analysis the condition ‘|f(x) − f(y)| ≤ λ|x − y|^{α} for some λ’ is called Hölder condition with exponent α.

4.1 Related results

The first proof of the uniqueness of the best L_{1}-approximation was given in 1921 by Jackson, [9]. The proof we analysed was published by Cheney [6] in 1965 and reprinted in his book [7] from 1966. Only in 1975 Björnestål [3], by analyzing the qualitative (relative to the dependencies) aspect of the continuity of the projection operator for arbitrary normed linear spaces X into a closed linear subspace of X, obtained the following result,

Theorem 4.6 (Björnestål, 75) Let f ∈ C[0, 1] and Ω_{f} be a modulus of uniform continuity of f −p_{b}, where p_{b} is the best L_{1}-approximation of f from P_{n}. Then, for p ∈ P_{n}, ε sufficiently small and for some constant c depending on f and n,

∥p − p_{b}∥_{1} ≥ ε → ∥f − p∥_{1} − ∥f − p_{b}∥_{1} ≥ 2 ∫_{0}^{Ω_{f}^{−1}(c ε)} c ε − Ω_{f}(x) dx.

We want to show that our theorem 4.3 implies an effective version of Björnestål’s theorem. First we can rewrite his theorem in the form we have been working with,

(1) ∥f − p∥_{1} < dist_{1}(f, P_{n}) + 2 ∫_{0}^{Ω_{f}^{−1}(c ε)} c ε − Ω_{f}(x) dx → ∥p − p_{b}∥_{1} < ε.

The modulus of uniform continuity referred by Björnestål is defined as,

Ω_{f}(ε) = sup_{|x−y|<ε} |f(x) − p_{b}(x) − f(y) + p_{b}(y)|,

which means that Ω_{f}^{−1}(ε) (for ε small enough so that Ω_{f}^{−1}(ε) is defined) is the optimal modulus of continuity for f − p_{b} in our sense.

First we show that ∫_{0}^{Ω_{f}^{−1}(c ε)} c ε − Ω_{f}(x) dx can be written as c′ εΩ_{f}^{−1}(c′ ε), for some constant \frac{c}{2} ≤ c′ ≤ c. For that purpose note that,

∫_{0}^{Ω_{f}^{−1}(c ε)} c ε − Ω_{f}(x) dx ≤ ∫_{0}^{Ω_{f}^{−1}(c ε)} c ε dx = c εΩ_{f}^{−1}(c ε).

On the other hand we have,

∫_{0}^{Ω_{f}^{−1}(c ε)} c ε − Ω_{f}(x) dx ≥ ∫_{0}^{Ω_{f}^{−1}( \frac{c}{2} ε)} c ε − Ω_{f}(x) dx ≥ ∫_{0}^{Ω_{f}^{−1}( \frac{c}{2} ε)} \frac{c}{2} ε dx = \frac{c}{2} εΩ_{f}^{−1}(\frac{c}{2} ε).

Therefore, for some \frac{c}{2} ≤ c′ ≤ c, (1) is equivalent to,

∥f − p∥_{1} < dist_{1}(f, P_{n}) + 2c′ εΩ_{f}^{−1}(c′ ε) → ∥p − p_{b}∥_{1} < ε.

The constant c, however, is not presented by Björnestål and moreover the function Ω_{f}^{−1} is normally non-computable. We can give an effective modulus of continuity for f −p_{b} following section 3.5 (and taking M_{f} = ⌈\frac{1}{ω_{f} (1)}⌉ as suggested in the proof of 4.3),

ω_{f−p_{b}}(ε) ≥ min\{ω_{f}(\frac{ε}{2}), ω_{p_{b}}(\frac{ε}{2})\}
≥ min\{ω_{f}(\frac{ε}{2}), \frac{ε}{20(n + 1)^{4}⌈\frac{1}{ω_{f} (1)}⌉}\}

Therefore, let ω_{f−p_{b}}^{∗}(ε) := min\{ω_{f}(\frac{ε}{2}), _{\frac{ε}{20(n+1)^{4}⌈ \frac{1}{ω_{f} (1)} ⌉}}\}, we can restate our theorem 4.3 and

see how it relates to Björnestål’s result:

Corollary 4.7 Let f ∈ C[0, 1], ω_{f} be some modulus of uniform continuity of f, and p ∈ P_{n}. Then for ε ≤ 1,

∥f − p∥_{1} < dist_{1}(f, P_{n}) + c̃_{n} ε ω_{f−p_{b}}^{∗}(c̃_{n} ε) → ∥p − p_{b}∥_{1} ≤ ε,

where c̃_{n} := \frac{c_{n}}{3^{n+2}(n+1)^{n+1}} and c_{n} := \frac{⌊n/2⌋!⌈n/2⌉!}{2^{n+3}3^{n^{2}+2n}(n+1)^{n^{2}+2n+1}} .

Proof: From theorem 4.3 we have,

∥f − p∥_{1} < dist_{1}(f, P_{n}) + min\{\frac{c_{n}ε}{3^{n+2}(n + 1)^{n+1}} , \frac{c_{n}ε}{2}ω_{f−p_{b}}^{∗}(\frac{c_{n}ε}{4})\} → ∥p − p_{b}∥_{1} ≤ ε,

which implies,

∥f − p∥_{1} < dist_{1}(f, P_{n}) + min\{\frac{c_{n}ε}{3^{n+2}(n + 1)^{n+1}} , \frac{c_{n}ε}{3^{n+2}(n + 1)^{n+1}} ω_{f−p_{b}}^{∗}(\frac{c_{n}ε}{4})\} → ∥p − p_{b}∥_{1} ≤ ε.

For ε ≤ 1 we have ω_{f−p_{b}}^{∗}(\frac{c_{n}ε}{4}) ≤ 1. Hence,

∥f − p∥_{1} < dist_{1}(f, P_{n}) + \frac{c_{n}ε}{3^{n+2}(n + 1)^{n+1}} ω_{f−p_{b}}^{∗}(\frac{c_{n}ε}{4}) → ∥p − p_{b}∥_{1} ≤ ε.

Since 3^{n+2}(n + 1)^{n+1} > 4 we get our result. □

Some years later, in 1978, Kroó [20] showed that the constant c in Björnestål’s result needed not to depend on any particular point of the function f but only on its modulus of continuity. 24 We got an effective version of Björnestål’s result where our constant c is completely independent of the function f and only depends on the dimension of the space P_{n}.

24As in Björnestål [3], Kroó does not present the actual constant.

Remark 4.8 In Kroó [20] the problem of L_{1}-approximation of continuous functions is considered for arbitrary Haar subspaces of C[0, 1] containing the constant functions. Kroó [22] treats uniqueness subspaces of C[0, 1] but in that case the constant c also depends on values of the function f and not only on its modulus of continuity. Since Cheney’s proof which we analyzed works for arbitrary Haar subspaces we are also guaranteed to extract uniform moduli of uniqueness in the general setting. As done by Jackson [9] in his original proof, in the present work we focused on the specific Haar subspace P_{n} in order to get fully explicit results. One can observe that only section 3.8 (Lagrange interpolation formula used to show that P_{n} is a Haar space), section 3.5 (Markov inequality used to show that K_{f,n} is compact by constructing a common modulus of uniform continuity) and section 3.11 (the construction of a polynomial which changes sign in each x_{i}) made reference to the particular Haar space P_{n}. From results in [4](lemma 4.3), [5](lemma) and [13](after lemma 9.32) is follows that there exist effective and quantitative substitutes for each of these constructions for arbitrary (effectively given) Haar spaces. So it is clear that the analysis carried out in this paper can be extended to general Haar spaces H containing the constant functions^{25}. Details will be presented in a subsequent paper.

4.2 How p_{b} is computed

An operator B_{f,n}(ε) : Q_{+}^{∗} → P_{n} computes the unique best L_{1}-approximation, p_{b} ∈ P_{n}, of a function f ∈ C[0, 1] from P_{n} if for any given ε ∈ Q_{+}^{∗} it generates a polynomial of degree ≤ n with rational coefficients (i.e. a n + 1-vector of rational coefficients) B_{f,n}(ε) such that, ∥B_{f,n}(ε)−p_{b}∥_{1} ≤ ε. We show how this can be achieved using the uniform modulus of uniqueness, Φ(f, n, ε),

∀f ∈ C[0, 1]; n ∈ IN; p_{1}, p_{2} ∈ P_{n}; ε ∈ Q_{+}^{∗}

( ⋀_{i=1}^{2}(∥f − p_{i}∥_{1} − dist_{1}(f, P_{n}) < Φ(f, n, ε)) → ∥p_{1} − p_{2}∥_{1} ≤ ε).

First we substitute p for p_{1} and p_{b} for p_{2},

∀f ∈ C[0, 1]; n ∈ IN; p ∈ P_{n}; ε ∈ Q_{+}^{∗}(∥f − p∥_{1} − dist_{1}(f, P_{n}) < Φ(f, n, ε) → ∥p − p_{b}∥_{1} ≤ ε).

Now we just need to find a B_{f,n}(ε) such that, ∥f −B_{f,n}(ε)∥_{1} −dist_{1}(f, P_{n}) < Φ(f, n, ε). Note that now there is no explicit reference to p_{b}, only implicit in dist_{1}(f, P_{n}).

A set N := {p_{1}, p_{2}, …} ⊂ P_{n} is said to be an ε-net of P_{n} if ∀p ∈ P_{n}∃p_{i} ∈ N(∥p − p_{i}∥_{1} ≤ ε). The algorithm for computing p_{b} consists in evaluating ∥f −p_{i}∥_{1} for each p_{i} in some Φ(f, n, ε)- net of P_{n} and taking the p_{i} which gives the minimum value. This ε-net has a priori infinitely many elements, but since we know that the best L_{1}-approximation p_{b} of f lives in a compact subspace of P_{n}, namely p_{b} ∈ K_{f,n}, we have ∥p_{b}∥_{1} ≤ 5/2∥f∥_{1} which gives us a bound on the coefficients of p_{b} (see remark 3.7). In this way, we can restrict the search to the ε-net of K_{f,n}, chosen according to these bounds on the coefficients, which is finite. The complexity analysis of the whole algorithm will be carried out in a future work.

25We only need the constant functions to belong to H if we want to get rid of the f dependency in c, i.e.

obtain a constant c in the uniform modulus of uniqueness depending only on n and ω_{f}.

5 Concluding remarks on the extraction of Φ

We emphasize again the two important roles played by logic in the extraction of the modulus of uniqueness for best L_{1}-approximation presented here. First, by showing that Cheney’s proof could be formalized in the system A_{∗}^{ω} (and by the logical meta-theorem 2.1) we were guaranteed that such a modulus Φ would exist and that it could be extracted from the mentioned proof. Moreover, the fact that Φ depends only on ω_{f}, n and ε (which was proved by Kroó years after Cheney’s proof) is obtained immediately from the meta-theorem 2.1. The second important role is that logic not only guaranteed the existence of the modulus but it went even further and supplied a procedure (monotone functional interpretation) to extract the modulus, which enabled us to provide for the first time an explicit dependency on n and ω_{f}. And, as it happened, the extracted modulus of uniqueness has the optimal ε-dependency established by Kroó.

We hope it is transparent that all the mathematical tools used in our analysis were already present in Cheney’s proof,^{26} which can be noticed for instance in the analysis of lemma 1 (section 3.10) where in order to prove that the functionals presented realized the lemma (see Claim 3.13) we followed line by line the original proof from [7], the only difference being that we considered the ε-version of the propositions. This visibly shows that the uniform modulus of uniqueness here extracted was really implicitly present in Cheney’s proof but could only be made explicit with the help of logic. The difficulty to extract ad hoc such information can be understood because Cheney’s proof (although very simple from the mathematical point of view and even called ‘elementary’ by the author) is logically very intricate due to the use of proof by contradiction and principles that fail in computable analysis.

6 Remarks on the case of Chebycheff approximation

In this section we recall some of the results obtained in [16] on effective moduli of uniqueness for the best Chebycheff approximation and show how they can be used to get moduli of uniqueness which – like our modulus for the L_{1}-approximation in theorem 4.3 – only depend on f ∈ C[0, 1] via a modulus of uniform continuity ω for f. [16] extracts from a classical proof (due to Young [28]) for the uniqueness of the best Chebycheff approximation uniform constants of strong unicity (see [23]) and moduli of uniqueness both for the polynomial case P_{n} and for general Haar spaces H. Whereas the constants of strong unicity depend on a positive lower bound for dist(f, P_{n}) (resp. dist(f, H)), this dependency can be removed (as shown in [16]) on the expense of losing the linearity of the modulus of uniqueness. In fact, in [16] non-linear moduli of uniqueness (and moduli of pointwise continuity for the Chebycheff projection) which only depend on the modulus of uniform continuity^{27} of f, the Haar space, ε and an upper bound for ∥f∥_{∞} are obtained. The following constructions are due to [4],[5]:

26Except Markov’s inequality which was used to show that the set K_{f,n} is compact and Lagrange interpolation formula used to prove that P_{n} is a Haar space. These tools, however, are standard in approximation theory.

Definition 6.1 Let ϕ := {ϕ_{1}, …, ϕ_{n}} be a Chebycheff system over [0, 1], \underline{ϕ}(x) := (ϕ_{1}(x), …, ϕ_{n}(x)) ∈ IR^{n}, ∥\underline{ϕ}∥ := sup_{x∈[0,1]} ∥\underline{ϕ}(x)∥_{2}, where ∥ · ∥_{2} denotes the Euclidean

norm on IR^{n}.

1) β, γ, κ : (0, \frac{1}{n}] → IR_{+}^{∗} are defined by

β(α) := \{ \begin{matrix}inf_{x∈[0,1]} |ϕ_{1}(x)|, if n = 1 \\ inf \{| det(ϕ_{j}(x_{i}))| : 0 ≤ x_{1}, …, x_{n} ≤ 1, ⋀_{i=1}^{n−1}(x_{i+1} − x_{i} ≥ α)\} , if n > 1 \end{matrix}

and

γ(α) := min (∥\underline{ϕ}∥, \frac{β(α)}{n^{\frac{1}{2}} (n − 1)! ∏_{i=1}^{n}(1 + ∥ϕ_{i}∥_{∞})}) , κ(α) := γ(α)^{−1} · ∥\underline{ϕ}∥

for α ∈ (0, \frac{1}{n}]. Since ϕ is a Chebycheff system it follows that β(α) > 0.

H :=Lin_{IR}(ϕ_{1}, …, ϕ_{n}).

2) Let M ∈ IR_{+}^{∗}, ω : IR_{+}^{∗} → IR_{+}^{∗} and let ω\underline{ϕ} be a modulus of uniform continuity for \underline{ϕ}. Then we define for ε ∈ IR_{+}^{∗}

ω_{M,H}(ε) := min (ω(\frac{ε}{2}), ω\underline{ϕ} (\frac{ε · β(\frac{1}{n})}{4Mn^{\frac{3}{2}} (n − 1)! ∏_{i=1}^{n}(1 + ∥ϕ_{i}∥_{∞})})) .

27Here we refer again to the notion as defined in the introduction and not to the concept of modulus of continuity as used in numerical analysis.

Theorem 6.2 ([16]) Let ϕ, H, β, γ, κ bas as in definition 6.1 and let A ⊂ C[0, 1] be a set of functions which have ω : IR_{+}^{∗} → IR_{+}^{∗} as a common modulus of uniform continuity and M ∈ IR_{+}^{∗} as a common upper bound M ≥ ∥f∥_{∞} for all f ∈ A.

1) Let l_{H,A} ∈ IR_{+}^{∗} such that l_{H,A} < inf_{f∈A} dist(f, H) and 0 < α ≤ min (\frac{1}{n}, ω_{M,H}(2 · l_{H,A})) .

Then \frac{γ(α)}{n·∥\underline{ϕ}∥} as a common constant of strong unicity for all f ∈ A, i.e.

∀f ∈ A, φ ∈ H(∥f − φ∥_{∞} ≥ ∥f − φ_{b}∥_{∞} + (\frac{γ(α)}{n · ∥\underline{ϕ}∥}) · ∥φ − φ_{b}∥_{∞}),

where φ_{b} is the best approximation of f in H. Furthermore 2n · κ(α) is a common Lipschitz constant for the Chebycheff projection for all points f ∈ A.

2)

Φ_{M,H}(ω, ε) := min (\frac{ε}{4}, \frac{ε}{2nκ( min (\frac{1}{n}, ω_{M,H}(\frac{ε}{2})))})

is a common modulus of uniqueness (and a common modulus of continuity for the Chebycheff projection in f) for all f ∈ A.

Remark 6.3 The bounds in the theorem improve numerically bounds obtained prior by D. Bridges ([4],[5], see [16] for a detailed discussion).

Using the transformation f ↦ f̃, with f̃(x) := f(x) − f(0), an argument similar to the one used in the proof of theorem 4.3 allows one to conclude: Theorem 6.4 Let {ϕ_{1}, …, ϕ_{n}} be a Chebycheff system s.t. 1 ∈ H :=Lin_{IR}(ϕ_{1}, …, ϕ_{n}) and let ω : IR_{+}^{∗} → IR_{+}^{∗} be any function. Then

Φ_{H}(ω, ε) := min (\frac{ε}{4}, \frac{ε}{2nκ( min (\frac{1}{n}, ω^{H}(\frac{ε}{2})))})

with

ω^{H}(ε) := min (ω(\frac{ε}{2}), ω\underline{ϕ} (\frac{ε · β(\frac{1}{n})}{4⌈\frac{1}{ω(1)}⌉n^{\frac{3}{2}} (n − 1)! ∏_{i=1}^{n}(1 + ∥ϕ_{i}∥_{∞})}))

is a common modulus of uniqueness (and a common modulus of continuity for the Chebycheff projection) for all functions f ∈ C[0, 1] which have ω as a modulus of uniform continuity.

For the polynomial case we get (see [16](cor.3.8))

Φ(ω, n, ε) := min (ε/4, \frac{⌊\frac{n}{2}⌋! ⌈\frac{n}{2}⌉!}{2(n + 1)} · (ω_{n}(ε/2))^{n} · ε),

with

ω_{n}(ε) := \{ \begin{matrix}min (ω (\frac{ε}{2}) , _{\frac{ε}{8n^{2}⌈ \frac{1}{ω(1)} ⌉}}) , if n ≥ 1 \\ 1 if n = 0 \end{matrix}

as such a common modulus.

As a corollary we obtain that for arbitrary Haar spaces having the constant function 1 the continuity behaviour of the Chebycheff projection is uniform for any class of equicontinuous functions which generalizes a result of [21] for the case of (trigonometric) polynomials.

References

[1] J. Avigad and S. Feferman. Gödel’s functional (”Dialectica”) interpretation. In S.R. Buss, editor, Handbook of proof theory, volume 137, pages 337–405. Elsevier, North-Holland, Amsterdam, 1998.

[2] M. Bartelt and W. Li. Error estimates and Lipschitz constants for best approximation in continuous function spaces. Computers and Mathematics with Application, 30(3-6):255– 268, 1995.

[3] B.O. Björnestål. Continuity of the metric projection operator i-iii. The preprint series of Department of Mathematics. Royal Institute of Technology. Stockholm, TRITA-MAT, 17, 1975.

[4] D.S. Bridges. A constructive development of Chebychev approximation theory. Journal of Approximation Theory, 30:99–120, 1980.

[5] D.S. Bridges. Lipschitz constants and moduli of continuity for the Chebychev projection. Proc. Amer. Math. Soc., 85:557–561, 1982.

[6] E.W. Cheney. An elementary proof of Jackson’s theorem on mean-approximation. Mathematics Magazine, 38:189–191, 1965.

[7] E.W. Cheney. Approximation Theory. AMS Chelsea Publishing, 1966.

[8] S. Feferman. Theories of finite type related to mathematical practice. In J. Barwise, editor, Handbook of Mathematical Logic, pages 913–972. North-Holland, Amsterdam, 1977.

[9] D. Jackson. Note on a class of polynomials of approximation. Transactions of the American Mathematical Society, 22:320–326, 1921.

[10] K.-I. Ko. On the computational complexity of best Chebycheff approximation. Journal of Complexity, 2:95–120, 1986.

[11] K.-I. Ko. Complexity theory of real functions. Birkhäuser, Boston-Basel-Berlin, 1991.

[12] U. Kohlenbach. A quantitative version of a theorem due to Borwein-Reich-Shafrir. To appear in: Numerical Functional Analysis and Optimization, 15 pages.

[13] U. Kohlenbach. Theory of majorizable and continuous functionals and their use for the extraction of bounds from non-constructive proofs: effective moduli of uniqueness for best approximations from ineffective proofs of uniqueness (german). PhD thesis, Frankfurt, pp. xxii+278, 1990.

[14] U. Kohlenbach. Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization. Journal of Symbolic Logic, 57:1239–1273, 1992.

[15] U. Kohlenbach. Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin’s proof for Chebycheff approximation. Annals of Pure and Applied Logic, 64:27–94, 1993.

[16] U. 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. Numerical Functional Analysis and Optimization, 14:581–606, 1993.

[17] U. Kohlenbach. Analysing proofs in Analysis. In W. Hodges, M. Hyland, C. Steinhorn, and J. Truss, editors, Logic: from Foundations to Applications, pages 225–260. European Logic Colloquium (Keele, 1993), Oxford University Press, 1996.

[18] U. Kohlenbach. Higher order reverse mathematics. Preprint, 14 pages, 2000.

[19] U. Kohlenbach. On the computational content of the Krasnoselski and Ishikawa fixed point theorems. In J. Blanck, V. Brattka, P. Hertling, and K. Weihrauch, editors, Computability and Complexity in Analysis, (CCA’2000), Lecture Notes in Computer Science. Springer LNCS, to appear.

[20] A. Kroó. On the continuity of best approximations in the space of integrable functions. Acta Mathematica Academiae Scientiarum Hungaricae, 32:331–348, 1978.

[21] A. Kroó. On the uniform modulus of continuity of the operator of best approximation in the space of periodic functions. Acta Math. Academiae Scientiarum Hungaricae, 34:185–203, 1979.

[22] A. Kroó. On strong unicity of L_{1}-approximation. Proceedings of the American Mathematical Society, 83(4), 1981.

[23] D. J. Newman and H. S Shapiro. Some theorems on Chebycheff approximation. Duke Mathematical Journal, 30:673–681, 1963.

[24] A. Pinkus. On L_{1}-Approximation, volume 93 of Cambridge Trats in Mathematics. Cambridge University Press, 1989.

[25] S.G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, 1999.

[26] A.S. Troelstra. Metamathematical investigation of intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, volume 344, pages 1–323. Springer Verlag, 1973.

[27] K. Weihrauch. Computable Analysis. Springer-Verlag, 2000.

[28] J.W. Young. General theory of approximnation by functions involving a given number of arbitrary parameters. Trans. Amer. Math. Soc., 8:331–344, 1907.

Recent BRICS Report Series Publications

RS-01-14 Ulrich Kohlenbach and Paulo B. Oliva. Effective Bounds on Strong Unicity in L_{1}-Approximation. May 2001. 38 pp.

RS-01-13 Federico Crazzolara and Glynn Winskel. Events in Security Protocols. April 2001. 30 pp.

RS-01-12 Torben Amtoft, Charles Consel, Olivier Danvy, and Karoline Malmkjær. The Abstraction and Instantiation of String-Matching Programs. April 2001.

RS-01-11 Alexandre David and M. Oliver Möller. From HUppaal to Uppaal: A Translation from Hierarchical Timed Automata to Flat Timed Automata. March 2001. 40 pp.

RS-01-10 Daniel Fridlender and Mia Indrika. Do we Need Dependent Types? March 2001. 6 pp. Appears in Journal of Functional Programming, 10(4):409–415, 2000. Superseeds BRICS Report RS-98-38.

RS-01-9 Claus Brabrand, Anders Møller, and Michael I. Schwartzbach. Static Validation of Dynamically Generated HTML. February 2001. 18 pp.

RS-01-8 Ulrik Frendrup and Jesper Nyholm Jensen. Checking for Open Bisimilarity in the π-Calculus. February 2001. 61 pp.

RS-01-7 Gregory Gutin, Khee Meng Koh, Eng Guan Tay, and Anders Yeo. On the Number of Quasi-Kernels in Digraphs. January 2001. 11 pp.

RS-01-6 Gregory Gutin, Anders Yeo, and Alexey Zverovich. Traveling Salesman Should not be Greedy: Domination Analysis of Greedy-Type Heuristics for the TSP. January 2001. 7 pp.

RS-01-5 Thomas S. Hune, Judi Romijn, Mariëlle Stoelinga, and Frits W. Vaandrager. Linear Parametric Model Checking of Timed Automata. January 2001. 44 pp. To appear in Margaria and Yi, editors, Tools and Algorithms for The Construction and Analysis of Systems: 7th International Conference, TACAS ’01 Proceedings, LNCS, 2001.