Prove2Me

lean_workbook_plus_32948

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

∣Dn−n⋅ln⁡2∣<n+1⇔n⋅ln⁡2−n−1<Dn<n⋅ln⁡2+n+1|D_n-n\cdot \ln 2|<\sqrt{n}+1\Leftrightarrow n\cdot \ln 2-\sqrt{n}-1<D_n<n\cdot \ln 2+\sqrt{n}+1

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_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

View graph