Brouwer's Fixed Point Theorem (BFPT) is not provable in Bishop-style constructive mathematics (BISH). For quick orientation, BISH is obtained from classical mathematics by removing the Law of Excluded Middle (LEM) and replacing the full Axiom of Choice by the Axiom of Dependent Choice.
Standard classical proofs of BFPT either rely on LEM or the Bolzano-Weierstrass Theorem, which is equivalent to the Limited Principle of Omniscience, a constructively inadmissible weakening of LEM. BFPT itself is equivalent to Weak König's Lemma in BISH, and thus to the Lesser Limited Principle of Omniscience, another constructively inadmissible weakening of LEM.
However, the following approximate version of BFPT is known to be provable in BISH.
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$.
Here's my proof attempt:
The proof in BISH proceeds via Sperner's Lemma. Recall that $$\Delta^n=\bigg\{(x_0,...,x_n)\mid\sum_{i=0}^{n}\leq1\bigg\}.$$
Consider a uniformly continuous function $f$ from $\Delta^n$ into itself. Fix $m,k\in\mathbb{N}$ such that $2^{-k}+2^{-k-2}+2^{-k-3}<2^{-m}$ and $$d(x,y)<2^{-k}+2^{-k-2}\Longrightarrow d(f(x),f(y))<2^{-m},$$ where $d$ is the Euclidian metric.
Consider a simplical subdivision $\mathcal{S}$ of $\Delta^2$ with grid size $2^{-k}$. Specify a labeling as follows. A vertex $x$ of a simplex in $\mathcal{S}$ gets assigned the label $i$ if, and only if, $f(x)_i<x_i$ or $f(x)_i<x_i+2^{-k-3}$. This is constructively well-defined by the Approximate Splitting Principle and constitutes a feasible labeling in the sense of Sperner's Lemma. Thus, $\mathcal{S}$ contains a fully labeled subsimplex $S$. We must now show that for a vertex $s$ of $S$, $d(f(s),s)<(n-1)2^{-m}$ holds (cf. Scarf, 1967; van Dalen, 2011).
This is where I got stuck.
Suppose $s$ is labeled by $1$. I just can't figure out how to infer $d(f(s),s)<(n-1)2^{-m}$ from the fact that $f(s)_1<s_1+<2^{-k-3}$ and uniform continuity of $f$ alone.
I'm sure the argument is fairly easy, but I just can't see it. A "visual" argument for $\Delta^2$ is in the paper by van Dalen referenced above. While it helps me see that the conclusion is true for $\Delta^1$ and $\Delta^2$, I am still unable to derive it formally, let alone generalize it to $\Delta^n$.
Any help would be greatly appreciated.
Thank you in advance!
PS: I am not a mathematician, so bear with me.
from Hot Weekly Questions - Mathematics Stack Exchange
Post a Comment