2 <= 3 log 2

Stream: maths

[Patrick Stevens]

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]

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]

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]

Ah, data.complex.exponential_bounds - thanks!

[Bhavik Mehta]

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