Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation

DOI10.1016/0168-0072(93)90213-WzbMath0795.03086OpenAlexW2061466015MaRDI QIDQ688431

Ulrich Kohlenbach

Publication date: 1 September 1994

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(93)90213-w

zbMATH Keywords

Chebycheff approximationeffective modulus of uniquenessineffective uniqueness proofs of classical analysis

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Constructive real analysis (26E40)

Related Items (27)

Computational complexity of optimization and crude range testing: A new approach motivated by fuzzy optimization ⋮ Proof mining in \(L_{1}\)-approximation ⋮ A proof-theoretic bound extraction theorem for \(\mathrm{CAT}(\kappa)\)-spaces ⋮ Revisiting jointly firmly nonexpansive families of mappings ⋮ Some logical metatheorems with applications in functional analysis ⋮ Bounded functional interpretation and feasible analysis ⋮ Constructing local optima on a compact interval ⋮ On the computational content of convergence proofs via Banach limits ⋮ Eliminating disjunctions by disjunction elimination ⋮ Bounds on strong unicity for Chebyshev approximation with bounded coefficients ⋮ Logical metatheorems for abstract spaces axiomatized in positive bounded logic ⋮ Convexity and unique minimum points ⋮ Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Toward a clarity of the extreme value theorem ⋮ Bounded functional interpretation ⋮ A QUANTITATIVE VERSION OF A THEOREM DUE TO BORWEIN-REICH-SHAFRIR ⋮ Strongly uniform bounds from semi-constructive proofs ⋮ General logical metatheorems for functional analysis ⋮ Weihrauch degrees, omniscience principles and weak computability ⋮ The fan theorem and unique existence of maxima ⋮ Moduli of regularity and rates of convergence for Fejér monotone sequences ⋮ Logical aspects of rates of convergence in metric spaces ⋮ Continuity and Lipschitz constants for projections ⋮ Problems, solutions, and completions ⋮ Some conservation results on weak König's lemma ⋮ On preserving the computational content of mathematical proofs: toy examples for a formalising strategy

Cites Work

• Pointwise hereditary majorization and some applications
• Fixed point theory in weak second-order arithmetic
• Countable algebra and set existence axioms
• Representations of the real numbers and of the open subsets of the set of real numbers
• On the foundations of best approximation theory
• A constructive development of Chebyshev approximation theory
• Constructivism in mathematics. An introduction. Volume II
• Which set existence axioms are needed to prove the separable Hahn-Banach theorem?
• On the computational complexity of best Chebyshev approximations
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Uniform approximation by polynomials having bounded coefficients
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• Some theorems on Cebysev approximation
• Lipschitz Constants and Moduli of Continuity for the Chebyshev Projection
• Recursive Functionals and Quantifiers of Finite Types I
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Which set existence axioms are needed to prove the Cauchy/Peano theorem for ordinary differential equations?
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• Note on the fan theorem
• 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
• Approximation von Funktionen und ihre numerische Behandlung
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation