1 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University2 Department of Computer Science, Queen Mary, University of London3 Technische Universität Darmstadt4 University of Edinburgh
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&unknown;C[0,1] by polynomials p&unknown;Pn of degree = -dependency as follows from Kroo (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&unknown;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).
Proceedings of the 3rd International Workshop on Implicit Computational Complexity: Icc-01, 2001, p. 117-122