Skip to main content
MathOverflow

Timeline for Constructive proof of a rational version of Perron-Frobenius?

Current License: CC BY-SA 4.0

32 events
when toggle format what by license comment
May 11, 2018 at 7:47 comment added darij grinberg Okay, I will have to admit: I don't know nearly enough logic and analysis to get this, although I find the idea rather interesting; it's like Barr's theorem but without requiring the meta-theory to be classical. One thing I'm not totally sure about is what exactly the classical proofs of Perron-Frobenius require. You're implicitly assuming that constructivism differs from classical logic in LEM only, but I suspect the AC matters as well in Perron-Frobenius (it's real numbers after all), and I'm not even sure the logical foundations are the same.
May 11, 2018 at 7:18 history edited darij grinberg CC BY-SA 4.0
adapt to OP change
May 7, 2018 at 10:04 history edited Franka Waaldijk CC BY-SA 4.0
improved exposition
May 7, 2018 at 9:56 history edited Franka Waaldijk CC BY-SA 4.0
improved exposition
May 7, 2018 at 9:32 comment added Franka Waaldijk Matt F. pointed out that KG was proved in a paper by Michael Beeson, I've added the reference here in a fifth update.
May 7, 2018 at 9:30 history edited Franka Waaldijk CC BY-SA 4.0
lay-out
May 6, 2018 at 11:44 comment added Franka Waaldijk In essence then the eigenvector $v$ is positive, because a) we can find $v$ constructively, b) positivity is decidable for vectors in $(^r\mathbb{A})^n$, and c) it is impossible that $v$ is not positive, since that would contradict classical mathematics.
May 6, 2018 at 9:40 history edited Franka Waaldijk CC BY-SA 4.0
improved explanation
May 6, 2018 at 9:27 history edited Franka Waaldijk CC BY-SA 4.0
improved explanation
May 5, 2018 at 20:02 history edited Franka Waaldijk CC BY-SA 4.0
lay-out
May 5, 2018 at 19:56 history edited Franka Waaldijk CC BY-SA 4.0
corrected typo
May 5, 2018 at 19:14 comment added Franka Waaldijk I will explain the Kleene Getaway in a fourth update above, and mention where it is used in the proof that I gave.
May 5, 2018 at 19:13 comment added Franka Waaldijk The proof is there! But it uses a nifty and onorthodox shortcut, which you probably have not seen before. (I'm the only one as far as I know who regularly uses it. I remember it went against the constructive aesthetics of my PhD supervisor, who was also surprised by its effectiveness). I've been asking myself for some time now whether I should highlight this shortcut for a more general audience... I guess now is as good as ever. You see, I directly use the classical result, in a strictly constructive way, building in essence on Kleene's results. Let's call this shortcut the Kleene Getaway.
May 5, 2018 at 15:40 comment added darij grinberg I still don't see the proofs in your answer. Why is your eigenvector positive (or nonnegativr)?
May 5, 2018 at 7:35 comment added Franka Waaldijk To illustrate: in your first comment you wrote: '(And I'd be quite happy to have the theorem for positive matrices.)'. I gave you exactly that theorem...
May 5, 2018 at 7:32 history edited Franka Waaldijk CC BY-SA 4.0
improved explanation
May 5, 2018 at 7:24 comment added Franka Waaldijk I see that you have not accepted my answer as such... Perhaps you could explain why? Frankly, I feel I've given you a very clear and correct answer, much more than just some suggestions. So I would like to hear from you what you feel is missing.
May 5, 2018 at 2:56 comment added darij grinberg I believe I have now answered my question myself (using the theory of linear programming), though it will take me a while to write the answer up. Thanks for the suggestions and the interesting references!
May 4, 2018 at 17:20 history edited Franka Waaldijk CC BY-SA 4.0
typos
May 4, 2018 at 16:23 history edited Franka Waaldijk CC BY-SA 4.0
added explanatory comment
May 4, 2018 at 16:16 history edited Franka Waaldijk CC BY-SA 4.0
typos
May 4, 2018 at 16:10 history edited Franka Waaldijk CC BY-SA 4.0
added explanatory comment
May 4, 2018 at 16:04 history edited Franka Waaldijk CC BY-SA 4.0
added "third update"
May 4, 2018 at 6:12 history edited Franka Waaldijk CC BY-SA 4.0
corrected typo
May 4, 2018 at 6:00 comment added Franka Waaldijk But the argument, though correct, is brute force like I said. And like I suggested, there is a more elegant algebraic solution. This, through constructive logic, then directly covers the positivity of the eigenvector. I will update again to reflect this.
May 4, 2018 at 5:58 comment added Franka Waaldijk Compactness in constructive mathematics...very crucial. For those with more than a passing interest in constructive math, it would be useful to acquaint themselves with Constructive Analysis.
May 3, 2018 at 22:56 comment added darij grinberg Compactness in constructive logic? The main part of Perron-Frobenius is the positivity/nonnegativity of the eigenvector; I don't see how to get this algebraically from the splitting of a polynomial.
May 3, 2018 at 22:16 history edited Franka Waaldijk CC BY-SA 4.0
updated to incorporate the comments
May 3, 2018 at 22:04 comment added Franka Waaldijk I just read your comment, will update the answer to reflect this. In short: Perron-Frobenius for positive matrices follows more or less automatically from the splitting of $p(A)$ over $\mathbb{A}$, and the discreteness of $\mathbb{A}$. But I don't know how you derive your thms. 1. and 2. from Perron-Frobenius (and I'm terribly rusty on algebra), so I can't immediately help you further. If you provide some details on your classical derivation, that would help.
May 3, 2018 at 18:43 comment added darij grinberg (I suspect Basu/Pollack/Roy is another book that can be mined for useful tools.)
May 3, 2018 at 18:42 comment added darij grinberg It's not enough to build a constructive theory of algebraic reals; I also need to prove Perron-Frobenius in this theory! (And I'd be quite happy to have the theorem for positive matrices.)
May 3, 2018 at 16:39 history answered Franka Waaldijk CC BY-SA 4.0
toggle format