Proof mining in L1-approximation Original Research Article

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 Kohlenbach (Logic: from Foundations to Applications, European Logic Colloquium (Keele, 1993), Oxford University Press, Oxford, 1996, pp. 225–260) to analyze Cheneyʹs simplification (Math. Mag. 38 (1965) 189) of Jacksonʹs original proof (Trans. Amer. Math. Soc. 22 (1921) 320) of the uniqueness of the best L1-approximation of continuous functions f∈C[0,1] by polynomials p∈Pn 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 View the MathML source (binary Königʹs lemma). The result of our analysis provides the first effective (in all parameters) 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ó (Acta Math. Acad. Sci. Hungar. 32 (1978) 331). The paper also describes how the uniform modulus of uniqueness can be used to compute the best L1-approximations of a fixed f∈C[0,1] with arbitrary precision. The second author uses this result to give a complexity upper bound on the computation of the best L1-approximation in Oliva (Math. Logic Quart., 48 (S1) (2002) 66–77).