Proof mining in L1-approximation

AbstractIn 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 WKL (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)