Prove2Me

Lean-Workbook Plus 48801: Logarithmic inequality

Proved
WorkbookRestored.plus_48801

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

lean-workbookrestored-importssource-checked

If real n,h>0n,h>0 and 0.9hn=0.5n0.9^h n=0.5n, then h=log⁡(0.5)/log⁡(0.9)h=\log(0.5)/\log(0.9).

Source: Lean-Workbook row lean_workbook_plus_48801 (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_48801  (n : ℝ)
  (h : ℝ)
  (h₀ : 0 < n)
  (h₁ : 0 < h)
  (h₂ : (0.9^h) * n = 0.5 * n) :
  h = Real.log 0.5 / Real.log 0.9   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_48801; immutable original Prove2Me node a7cd6071-5643-4298-b93f-3830ba876240

View graph