Zulip Chat Archive

Stream: maths

Topic: 2 <= 3 log 2


Patrick Stevens (Jun 20 2021 at 12:02):

Can anyone think of an easy maths proof of 2 <= 3 log 2 in the reals, preferably one that is also easy in mathlib? The inequality is only just true, and my usual answer would be "evaluate some decimal places" but log is noncomputable. That means my usual answer would become "evaluate some terms of the series expansion, and use that the error of an alternating series truncation is at most the first omitted term", but that is a lot of machinery.

Kevin Buzzard (Jun 20 2021 at 12:03):

Take exp of both sides (exp is monotonic) and now you have to prove e^2 <= 8, which is feasible because we have good bounds for e.

Patrick Stevens (Jun 20 2021 at 12:03):

Ah, I didn't look very hard for bounds, but now I know they're there I'm sure I can find them - thanks

Patrick Stevens (Jun 20 2021 at 12:06):

Ah, data.complex.exponential_bounds - thanks!

Bhavik Mehta (Jun 20 2021 at 13:11):

There's also some bounds on log 2 itself which could help do it directly!


Last updated: Dec 20 2023 at 11:08 UTC