Prove2Me

Lean-Workbook Plus 41428: Logarithmic inequality

Proved
WorkbookRestored.plus_41428

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For natural nn and 0≤x≤10\le x\le1, log⁡(1+nx/(n+1))≤log⁡(1+n/(n+1))\log(1+nx/(n+1))\le\log(1+n/(n+1)).

Source: Lean-Workbook row lean_workbook_plus_41428 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real
Formal statement
theorem WorkbookRestored.plus_41428 (n : ℕ) (x : ℝ) (hx : 0 ≤ x ∧ x ≤ 1) :
  Real.log (1 + n * x / (n + 1)) ≤ Real.log (1 + n / (n + 1))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_41428; immutable original Prove2Me node bcc380cb-81d8-4e97-badf-cb0ec84bb71c

View graph