University of Birmingham > Talks@bham > Theoretical computer science seminar > Constructive Brouwer Fixed Point Theorem

Constructive Brouwer Fixed Point Theorem

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

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 Rn 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.


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,

This 3-page lecture note by Jacob Fox (formerly of MIT , now Stanford)$\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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.