Timeline for Does the Brouwer fixed point theorem admit a constructive proof?
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 15, 2015 at 11:25 | vote | accept | coudy | ||
| Apr 14, 2015 at 18:38 | comment | added | Arno | @TonyK While being positive is not decidable, it is semidecidable. So we try for all rationals within the current bounds to find a proof that the function is positive/negative there. If the function is not constant 0, we'll find one eventually, and replace the appropriate current interval bound with it. | |
| Apr 14, 2015 at 18:31 | comment | added | TonyK | @Arno: How can we compute such an interval, when we can't even decide whether a computable number is positive or negative? | |
| Apr 14, 2015 at 17:32 | comment | added | Arno | @TonyK: Using a modified bisection algorithm, we can compute an interval (as a closed set, ie approximated from the outside) on which the function is zero. Now comes the non-constructive case distinction: If the interval contains a single point, we can compute this. If not, it contains some rational (and rationals are computable). | |
| Apr 14, 2015 at 15:54 | comment | added | TonyK | "Any computable function [...] has a computable root": I'm surprised by that. I'm pretty sure that not every such computable function has a constructively computable root. | |
| Apr 14, 2015 at 0:28 | comment | added | Arno | Yes, Orevkov was first. Baigger's work is built on Orevkov's construction and filling in some more details. | |
| Apr 14, 2015 at 0:20 | comment | added | Timothy Chow | Was Baigger the first? I thought it was Orevkov in 1963? | |
| Apr 13, 2015 at 19:56 | history | answered | Arno | CC BY-SA 3.0 |