Equivalence between the existence of an approximate equilibrium in a competitive economy and Sperner's lemma: a constructive analysis (Q420181)

Summary: Brouwer's fixed point theorem cannot be constructively proved, so the existence of an equilibrium in a competitive economy also cannot be constructively proved. On the other hand, Sperner's lemma which is used to prove Brouwer's theorem is constructively proved. Some authors have presented a constructive (or an approximate) version of Brouwer's fixed point theorem using Sperner's lemma. In this paper, I prove the existence of an approximate equilibrium in a competitive economy directly by Sperner's lemma. Also I show that the existence of an approximate equilibrium leads to Sperner's lemma. I follow the Bishop style constructive mathematics according to \textit{E. Bishop} and \textit{D. Bridges} [Constructive analysis. Grundlehren der Mathematischen Wissenschaften, 279. Berlin etc.: Springer-Verlag (1985; Zbl 0656.03042)], \textit{D. Bridges} and \textit{F. Richman} [Varieties of constructive mathematics. London Mathematical Society Lecture Note Series, 97. Cambridge etc.: Cambridge University Press. (1987; Zbl 0618.03032)], and \textit{D.S. Bridges} and \textit{L. S. Vîţă} [Techniques of constructive analysis. Universitext. New York, NY: Springer (2006; Zbl 1107.03065)].