BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Constructive Brouwer Fixed Point Theorem - Paul Ta
ylor (Computer Science\, University of Birmingham\
, honorary)
DTSTART:20190712T100000Z
DTEND:20190712T110000Z
UID:TALK3825AT
URL:/talk/index/3825
DESCRIPTION: The classical intermediate value theorem on the r
eal interval in general\nrequires decidability of
equality\, but the result may be made constructive
\nby requiring the function not to ``hover'' or be
``locally constant''.\n\nWe discuss the appropria
te generalisation of this condition to prove\nL.E.
J.~Brouwer's fixed point theorem for R^n construct
ively.\n\nThe condition is that: in each contracti
ble open subspace of R^n\,\nthe subspace of non-fi
xed points of the endofunction be (n-1)-connected.
\n\n(This is apparently stronger than "locally (n-
1)-connected"\nbut I don't know whether the condit
ion has a name.)\n\nThis condition is necessary fo
r a computable result\nbecause of a counterexample
due to G\\"unter Baigger.\n\nThe proof is a modif
ied form of a well known classical one\nusing sub-
division of simplices and Sperner's Lemma.\n\n\nRe
ferences:\n\nI don't recall the details of the Bai
gger counterexample\,\nbut Petrus Potgieter sketch
ed it for me when I went to\nPretoria in 2006 and
in the paper below:\n\nG\\"unter Baigger\,\nDie Ni
chtkonstruktivit\\"at des Brouwerschen Fixpunktsat
zes\,\nArch. Math. Log.\, 1985\n\nPetrus Potgieter
\,\nComputable counter-examples to the Brouwer fix
ed-point theorem\,\narxiv.org/abs/0804.3199\n\nThi
s 3-page lecture note by Jacob Fox (formerly of MI
T\, now\nStanford)\n math.mit.edu/$\\sim$fox/
MAT307-lecture03.pdf\ncontains\n- a neat combinato
rial proof of Sperner's Lemma and\n- its applicati
on to the classical Brouwer Fix Point Theorem:\n-
but not actually the manner of sub-dividing simpli
ces.\n\nThe construction of a regular subdivision
of a simplex must\nbe written up somewhere rigorou
sly\, but I don't have a\nreference. My proof wo
uld be a modification of this in\nwhich the flat f
aces are replaced by wiggly ones that\nswerve to a
void fixed points.
LOCATION:Computer Science\, 245
CONTACT:Noam Zeilberger
END:VEVENT
END:VCALENDAR