|
===A proof in a weak logical system===
In [[reverse mathematics]], Brouwer's theorem can be proved in the system [[Weak König's lemma|WKL<sub>0</sub>]], and conversely over the base system [[reverse mathematics|RCA<sub>0</sub>]] Brouwer's theorem for a square implies the [[weak König's lemma]], so this gives a precise description of the strength of Brouwer's theorem.
== Computing a fixed point ==
The first algorithm to approximate a fixed point was proposed by [[Herbert Scarf]] in 1967.<ref>{{Cite journal |last=Scarf |first=Herbert |date=1967-09-01 |title=The Approximation of Fixed Points of a Continuous Mapping |url=http://epubs.siam.org/doi/10.1137/0115116 |journal=SIAM Journal on Applied Mathematics |language=en |volume=15 |issue=5 |pages=1328–1343 |doi=10.1137/0115116 |issn=0036-1399}}</ref><ref>H. Scarf found the first algorithmic proof: {{SpringerEOM|title=Brouwer theorem|first=M.I.|last=Voitsekhovskii|isbn=1-4020-0609-8}}.</ref> A subtle aspect of Scarf's algorithm is that it finds a point that is {{em|almost fixed}} by a function ''f'', but in general cannot find a point that is close to an actual fixed point. In mathematical language, if {{mvar|ε}} is chosen to be very small, Scarf's algorithm can be used to find a point ''x'' such that ''f''(''x'') is very close to ''x'', i.e., <math>d(f(x),x) < \varepsilon </math>. But Scarf's algorithm cannot be used to find a point ''x'' such that ''x'' is very close to a fixed point: we cannot guarantee <math>d(x,y) < \varepsilon,</math> where <math>f(y)=y.</math> Often this latter condition is what is meant by the informal phrase "approximating a fixed point"{{Citation needed|date=August 2019}}.
Other algorithms for computing a fixed point were developed by Kuhn (1968), Eaves (1972), Merrill (1972) and others.<ref name=":0">{{Cite journal |last=Hirsch |first=Michael D |last2=Papadimitriou |first2=Christos H |last3=Vavasis |first3=Stephen A |date=1989-12-01 |title=Exponential lower bounds for finding Brouwer fix points |url=https://www.sciencedirect.com/science/article/pii/0885064X89900174 |journal=Journal of Complexity |language=en |volume=5 |issue=4 |pages=379–416 |doi=10.1016/0885-064X(89)90017-4 |issn=0885-064X}}</ref> A book by Michael Todd<ref>{{Cite book |url=https://link.springer.com/book/10.1007/978-3-642-50327-6 |title=The Computation of Fixed Points and Applications |language=en |doi=10.1007/978-3-642-50327-6}}</ref> surveys various algorithms developed until 1976. These algorithms are based on ''function evaluations'': they receive as an input a black-box that, for any ''x'', returns the value of ''f''(''x''). In the worst case, the number of evaluations required by these algorithms is exponential. Hirsch, [[Christos Papadimitriou|Papadimitriou]] and Vavasis proved that<ref name=":0" /> ''any'' algorithm based on function evaluations, that finds a fixed point with ''p'' decimal digits, requires <math>\Omega(2^p)</math> evaluations in the worst case. Equivalently, finding a point at a distance at most <math>\epsilon</math> from a fixed point requires <math>\Omega(1/\epsilon)</math> evaluations. This holds even when the function is two-dimensional (from the unit-disk to itself).
==Generalizations==
==See also==
* [[Banach fixed-point theorem]]
* [[Fixed-point computation]]
* [[Infinite compositions of analytic functions]]
* [[Nash equilibrium#Alternate proof using the Brouwer fixed-point theorem|Nash equilibrium]]
| 