Prove2Me

Upper_Bound_of_Natural_Logarithm

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysisinequalitieslogarithmproofwiki

For all y > 0: ln(y) <= y - 1.

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic

theorem Upper_Bound_of_Natural_Logarithm (y : ℝ) (hy : 0 < y) : Real.log y ≤ y - 1 := by sorry
Source
https://proofwiki.org/wiki/Upper_Bound_of_Natural_Logarithm

View graph