Prove2Me

lean_workbook_plus_16402

Proved

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

If an≥12n,a_n \ge \frac{1}{2^n}, then an1−1/n≤2an.a_n ^{1-1/n} \le 2 a_n. If an<12n,a_n < \frac{1}{2^n}, then an1−1/n<2an+12n−1.a_n ^{1-1/n} < 2a_n + \frac{1}{2^{n-1}}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16402 (a n : ℕ) : (a : ℝ) ≥ 1 / 2 ^ n → (a : ℝ) ^ (1 - 1 / n) ≤ 2 * a ∧ (a : ℝ) < 1 / 2 ^ n → (a : ℝ) ^ (1 - 1 / n) < 2 * a + 1 / 2 ^ (n - 1)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph