Bound on ln (natural log)

Stream: Is there code for X?

[Colin McDonagh]

Hi, newb here. Looking through mathlib I can't tell if there's code for the bound on the natural logarithm (ln, not a logarithm with a base number which is a natural number):
ln x < x - 1

[Rémy Degenne]

docs#Real.log_le_sub_one_of_pos

[Colin McDonagh]

Thank you!

[Scott Morrison]

@Colin McDonagh, a general strategy here is:

import Mathlib

example : Real.log x ≤ x - 1 := by apply?

which prints as the third result:

Try this: refine Real.log_le_sub_one_of_pos ?hx
Remaining subgoals:
⊢ 0 < x

and if you change the example to

example (h : 0 < x) : Real.log x ≤ x - 1 := by apply?

you just get a single result:

Try this: exact Real.log_le_sub_one_of_pos h

[Colin McDonagh]

Excellent, thanks for the lesson