Constructive Brouwer Fixed Point Theorem

Add to your list(s) Download to your calendar using vCal

• Paul Taylor (Computer Science, University of Birmingham, honorary)
• Friday 12 July 2019, 11:00-12:00
• Computer Science, 245.

If you have a question about this talk, please contact Noam Zeilberger.

The classical intermediate value theorem on the real interval in general requires decidability of equality, but the result may be made constructive by requiring the function not to ``hover’’ or be ``locally constant’’.

We discuss the appropriate generalisation of this condition to prove L.E.J.~Brouwer’s fixed point theorem for R^{n constructively.}

The condition is that: in each contractible open subspace of Rn, the subspace of non-fixed points of the endofunction be (n-1)-connected.

(This is apparently stronger than “locally (n-1)-connected” but I don’t know whether the condition has a name.)

This condition is necessary for a computable result because of a counterexample due to G\”unter Baigger.

The proof is a modified form of a well known classical one using sub-division of simplices and Sperner’s Lemma.

References:

I don’t recall the details of the Baigger counterexample, but Petrus Potgieter sketched it for me when I went to Pretoria in 2006 and in the paper below:

G\”unter Baigger, Die Nichtkonstruktivit\”at des Brouwerschen Fixpunktsatzes, Arch. Math. Log., 1985

Petrus Potgieter, Computable counter-examples to the Brouwer fixed-point theorem, arxiv.org/abs/0804.3199

This 3-page lecture note by Jacob Fox (formerly of MIT , now Stanford) math.mit.edu/$\sim$fox/MAT307-lecture03.pdf contains - a neat combinatorial proof of Sperner’s Lemma and - its application to the classical Brouwer Fix Point Theorem: - but not actually the manner of sub-dividing simplices.

The construction of a regular subdivision of a simplex must be written up somewhere rigorously, but I don’t have a reference. My proof would be a modification of this in which the flat faces are replaced by wiggly ones that swerve to avoid fixed points.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, 245
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.