Prove2Me

Lean-Workbook Plus 79397: Logarithmic inequality

Proved
WorkbookRestored.plus_79397

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

lean-workbookrestored-importssource-checked

For 0<x<y0<x<y, 2x+log⁡x/log⁡2<2y+log⁡y/log⁡22^x+\log x/\log2<2^y+\log y/\log2, with real exponentiation.

Source: Lean-Workbook row lean_workbook_plus_79397 (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.Base
open Real
Formal statement
theorem WorkbookRestored.plus_79397 (x y : ℝ) (hxy : x < y) (hx : 0 < x) (hy : 0 < y) : (2:ℝ)^x + (Real.log x) / (Real.log 2) < (2:ℝ)^y + (Real.log y) / (Real.log 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_79397; immutable original Prove2Me node 92faa752-736c-430f-97f9-eea0ca3fb813

View graph