Lean-Workbook Plus 66332: Logarithmic inequality

Proved

WorkbookRestored.plus_66332

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

lean-workbookrestored-importssource-checked

For $a,b>0$ with $a,b\ne1$ and real $x\ne0$ , $\frac{x\log a+\log(1+1/a^x)}{x\log b+\log(1+1/b^x)}=\frac{\log a+(1/x)\log(1+1/a^x)}{\log b+(1/x)\log(1+1/b^x)}$ . Real exponentiation and Lean’s total division are used.

Source: Lean-Workbook row lean_workbook_plus_66332 (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_66332  (x a b : ℝ)
  (h₀ : a > 0 ∧ b > 0)
  (h₁ : a ≠ 1 ∧ b ≠ 1)
  (h₂ : x ≠ 0) :
  (x * Real.log a + Real.log (1 + 1 / a^x)) / (x * Real.log b + Real.log (1 + 1 / b^x))
    = (Real.log a + 1 / x * Real.log (1 + 1 / a^x)) / (Real.log b + 1 / x * Real.log (1 + 1 / b^x))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_66332; immutable original Prove2Me node 35afa6f2-364e-4034-8e5a-60940cb60066

View graph