Lean-Workbook Plus 56810: Logarithmic inequality

Proved

WorkbookRestored.plus_56810

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

lean-workbookrestored-importssource-checked

For pairwise distinct positive real $a,b,c$ , $\log_{cb^2}a+\log_{ac^2}b+\log_{ba^2}c=\frac{\log a}{2\log b+\log c}+\frac{\log b}{2\log c+\log a}+\frac{\log c}{2\log a+\log b}$ . Base logarithms and division use Lean’s total convention.

Source: Lean-Workbook row lean_workbook_plus_56810 (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_56810  (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hab : a ≠ b) (hbc : b ≠ c) (hca : a ≠ c) :
  Real.logb (c * b^2) a + Real.logb (a * c^2) b + Real.logb (b * a^2) c =
    Real.log a / (2 * Real.log b + Real.log c) + Real.log b / (2 * Real.log c + Real.log a) +
      Real.log c / (2 * Real.log a + Real.log b)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_56810; immutable original Prove2Me node 05f6954c-e839-43f4-b045-f5d838cb50f1

View graph