Lemmas about Nat.nthRoot

In this file we prove that Nat.nthRoot n a is indeed the floor of ⁿ√a.

TODO

Rewrite the proof of Nat.nthRoot.lt_pow_go_succ_aux to avoid dependencies on real numbers, so that we can move this file to Mathlib/Data/Nat/NthRoot, then to Batteries.

@[simp]

theorem Nat.nthRoot_zero_left (a : ℕ) : nthRoot 0 a = 1

@[simp]

theorem Nat.nthRoot_one_left : nthRoot 1 = id

@[simp]

theorem Nat.nthRoot_zero_right {n : ℕ} (h : n ≠ 0) : n.nthRoot 0 = 0

@[simp]

theorem Nat.nthRoot_one_right {n : ℕ} : n.nthRoot 1 = 1

@[simp]

theorem Nat.pow_nthRoot_le_iff {n a : ℕ} : n.nthRoot a ^ n ≤ a ↔ n ≠ 0 ∨ a ≠ 0

nthRoot n a ^ n ≤ a unless both n and a are zeros.

theorem Nat.pow_nthRoot_le {n a : ℕ} : n ≠ 0 ∨ a ≠ 0 → n.nthRoot a ^ n ≤ a

Alias of the reverse direction of Nat.pow_nthRoot_le_iff.

---

nthRoot n a ^ n ≤ a unless both n and a are zeros.

theorem Nat.nthRoot.lt_pow_go_succ_aux {n a b : ℕ} (hb : b ≠ 0) : a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)

An auxiliary lemma saying that if b ≠ 0, then (a / b ^ n + n * b) / (n + 1) + 1 is a strict upper estimate on √[n + 1] a.

Currently, the proof relies on the weighted AM-GM inequality, which increases the dependency closure of this file by a lot.

A PR proving this inequality by more elementary means is very welcome.

theorem Nat.lt_pow_nthRoot_add_one {n : ℕ} (hn : n ≠ 0) (a : ℕ) : a < (n.nthRoot a + 1) ^ n

@[simp]

theorem Nat.le_nthRoot_iff {n a b : ℕ} (hn : n ≠ 0) : a ≤ n.nthRoot b ↔ a ^ n ≤ b

@[simp]

theorem Nat.nthRoot_lt_iff {n a b : ℕ} (hn : n ≠ 0) : n.nthRoot a < b ↔ a < b ^ n

@[simp]

theorem Nat.nthRoot_pow {n : ℕ} (hn : n ≠ 0) (a : ℕ) : n.nthRoot (a ^ n) = a

theorem Nat.nthRoot_eq_of_le_of_lt {n a b : ℕ} (h₁ : a ^ n ≤ b) (h₂ : b < (a + 1) ^ n) : n.nthRoot b = a

If a ^ n ≤ b < (a + 1) ^ n, then n root of b equals a.

theorem Nat.exists_pow_eq_iff' {n a : ℕ} (hn : n ≠ 0) : (∃ (x : ℕ), x ^ n = a) ↔ n.nthRoot a ^ n = a

theorem Nat.exists_pow_eq_iff {n a : ℕ} : (∃ (x : ℕ), x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a

instance Nat.instDecidableExistsPowEq {n a : ℕ} : Decidable (∃ (x : ℕ), x ^ n = a)

Equations

• Nat.instDecidableExistsPowEq = decidable_of_iff' (n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a) ⋯