Prove2Me

Lean-Workbook Plus 32948: Logarithmic inequality

Proved
WorkbookRestored.plus_32948

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

lean-workbookrestored-importssource-checked

For natural nn and real DD, ∣D−nlog⁡2∣<n+1|D-n\log2|<\sqrt n+1 if and only if nlog⁡2−n−1<D<nlog⁡2+n+1n\log2-\sqrt n-1<D<n\log2+\sqrt n+1.

Source: Lean-Workbook row lean_workbook_plus_32948 (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_32948 (n : ℕ) (D : ℝ) : |D - n * Real.log 2| < Real.sqrt n + 1 ↔ n * Real.log 2 - Real.sqrt n - 1 < D ∧ D < n * Real.log 2 + Real.sqrt n + 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_32948; immutable original Prove2Me node dcd945c8-7248-4664-8cad-f8b09c2aba26

View graph