3
$\begingroup$

The approximate Brouwer Fixed Point Theorem (aBFPT) for the standard $n$-simplex is:

Let $f$ be a uniformly continuous function from $\Delta^n$ into itself. Then for each $\varepsilon>0$ there exists $x\in\Delta^n$ such that $d(f(x),x)<\varepsilon$.

Does anyone know a reference for a full proof of aBFPT via Sperner's Lemma in Bishop-style constructive mathematics (BISH)?

A constructive proof of aBFPT via Gale's Hex Theorem is in Hendtlass's PhD thesis. A constructive proof for the $2$-simplex is in this paper by van Dalen. That's all I could find.

If you don't know a reference but have a proof handy I'd very much like to see that as well.

Thank you in advance!

Note: The status of BFPT in constructive mathematics has been discussed in this MO post. For quick orientation: aBFPT may be viewed as constituting the constructive core of the full classical BFPT. The latter implies LLPO and is thus inherently nonconstructive (indeed, the two are equivalent over BISH since both are equivalent to WKL in the presence of countable choice). Classically, BFPT can be retrieved from aBFPT by a simple application of the Bolzano-Weierstrass theorem, which is equivalent to LPO over BISH and thus constructively inadmissible.

Improve this question
$\endgroup$
5
  • $\begingroup$ I don't know the answer, but you might want to look in the computational complexity literature. Approximate Brouwer is an exemplar of a complexity class that has turned out to be interesting, called PPAD. $\endgroup$
    – arsmath
    Commented May 29, 2020 at 10:19
  • $\begingroup$ I am not proficient at all in this topic. But I do know about two papers of Orevkov that might be relevant here ( mathnet.ru/php/… and mathnet.ru/php/… ). As far as I understand, he studied Brower's Fixed Point theorem in the context of Russian constructive mathematics. In particular, Theorem 7.1 from the second paper is aBFPT. Unfortunately, both the papers are in Russian and they seems not to be translated in English. $\endgroup$
    – Fedor Pakhomov
    Commented May 29, 2020 at 13:49
  • $\begingroup$ I just found out that actually there exist an English translation of the second paper. It is in the volume "Problems in the Constructive Trend in Mathematics, IV" that were translated in English. $\endgroup$
    – Fedor Pakhomov
    Commented May 29, 2020 at 14:02
  • $\begingroup$ All van Dalen does is taking the usual argument based on Sperner's lemma and getting rid of having to decide ordering relations by adding some additional slack. The same method works for the usual arguments and does not depend on the dimension being 2. $\endgroup$
    – Michael Greinecker
    Commented May 29, 2020 at 14:04
  • $\begingroup$ There are also seems to be an explicit prove for the general case in link.springer.com/chapter/10.1007/978-1-4020-8926-8_14 $\endgroup$
    – Michael Greinecker
    Commented May 29, 2020 at 14:05

0

Reset to default

You must log in to answer this question.