Timeline for Proving a messy inequality
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 21, 2012 at 20:41 | vote | accept | VSJ | ||
| Apr 21, 2012 at 7:33 | answer | added | VSJ | timeline score: 5 | |
| Apr 11, 2012 at 23:54 | comment | added | VSJ | @David Speyer: Thank you, that was very helpful! I'll still try to prove it analytically, but knowing that there is something to fall back on is quite comforting. | |
| Apr 11, 2012 at 21:37 | comment | added | David E Speyer | My comment on this answer mathoverflow.net/questions/17189/… is an example of what Boris is talking about. | |
| Apr 11, 2012 at 20:46 | history | edited | VSJ | CC BY-SA 3.0 |
added progress
|
| Apr 7, 2012 at 1:40 | comment | added | VSJ | @Brendan : Ah, in that case I'll wait a bit. To be honest I'm amazed to hear that floating point arithmetic can be used to rigourously prove anything at all! I would really appreciate any references. This also raises the question if these brute force methods work, why doesn't everyone use them all the time? | |
| Apr 7, 2012 at 1:15 | comment | added | Brendan McKay | This can even be done in floating point to full rigor if interval arithmetic is used. But that would be a "desperate last hope" type of proof. | |
| Apr 6, 2012 at 18:06 | comment | added | VSJ | @boris-bukh :Thanks for the suggestion. Do you happen to know any such sample proofs which I can read and get a better idea of how these techniques work? | |
| Apr 6, 2012 at 16:39 | answer | added | Robert | timeline score: 1 | |
| Apr 6, 2012 at 11:42 | comment | added | Boris Bukh | If all else fails: with much work, a plot can be turned into a proof. Sample points at sufficiently fine grid, which given a crude upper bound on the derivative implies inequality nearby whenever the inequality is true with an epsilon to spare. Then check neighborhoods of the set where the equality holds. For those, compute the derivates around them, show that they point in the right direction, and bound the second derivative to show that one gets a control for big enough neighborhood of the equality case. This is a pain, but general Tarski's exponential function problem is still open. | |
| Apr 6, 2012 at 2:08 | history | asked | VSJ | CC BY-SA 3.0 |