From 7a081b7ac4780c8424d479315ae6780a86892a37 Mon Sep 17 00:00:00 2001 From: Yury Kudryashov Date: Fri, 22 Aug 2025 07:12:05 +0000 Subject: [PATCH 01/10] feat(Data/Nat): define `Nat.nthRoot` Define `Nat.nthRoot n a` to be the `n`th root of a natural number `a`. --- Mathlib.lean | 2 + Mathlib/Data/Nat/NthRoot/Defs.lean | 27 +++++ Mathlib/Data/Nat/NthRoot/Lemmas.lean | 147 +++++++++++++++++++++++++++ 3 files changed, 176 insertions(+) create mode 100644 Mathlib/Data/Nat/NthRoot/Defs.lean create mode 100644 Mathlib/Data/Nat/NthRoot/Lemmas.lean diff --git a/Mathlib.lean b/Mathlib.lean index 8a8aa06d9efb58..4dc479120a9fd1 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3405,6 +3405,8 @@ import Mathlib.Data.Nat.ModEq import Mathlib.Data.Nat.Multiplicity import Mathlib.Data.Nat.Notation import Mathlib.Data.Nat.Nth +import Mathlib.Data.Nat.NthRoot.Defs +import Mathlib.Data.Nat.NthRoot.Lemmas import Mathlib.Data.Nat.Order.Lemmas import Mathlib.Data.Nat.PSub import Mathlib.Data.Nat.Pairing diff --git a/Mathlib/Data/Nat/NthRoot/Defs.lean b/Mathlib/Data/Nat/NthRoot/Defs.lean new file mode 100644 index 00000000000000..88e9cfb128676e --- /dev/null +++ b/Mathlib/Data/Nat/NthRoot/Defs.lean @@ -0,0 +1,27 @@ +/- +Copyright (c) 2025 Concordance Inc. dba Harmonic. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury Kudryashov +-/ + +/-! +# Definition of `Nat.nthRoot` + +In this file we define `Nat.nthRoot n a` to be the floor of the `n`th root of `a`. +The function is defined in terms of natural numbers with no dependencies outside of prelude. +-/ + +/-- `Nat.nthRoot n a = ⌊(a : ℝ) ^ (1 / n : ℝ)⌋₊` defined in terms of natural numbers. + +We use Lagrange's method to find a root of $x^n = a$, +so it converges superexponentially fast. -/ +def Nat.nthRoot : Nat → Nat → Nat + | 0, _ => 1 + | 1, a => a + | n + 2, a => + if a ≤ 1 then a else go n a a + where + /-- Auxiliary definition for `Nat.nthRoot`. -/ + go n a guess := + let next := (a / guess^(n + 1) + (n + 1) * guess) / (n + 2) + if next < guess then go n a next else guess diff --git a/Mathlib/Data/Nat/NthRoot/Lemmas.lean b/Mathlib/Data/Nat/NthRoot/Lemmas.lean new file mode 100644 index 00000000000000..fc74501bcb8730 --- /dev/null +++ b/Mathlib/Data/Nat/NthRoot/Lemmas.lean @@ -0,0 +1,147 @@ +/- +Copyright (c) 2025 Concordance Inc. dba Harmonic. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury Kudryashov +-/ +import Mathlib.Analysis.MeanInequalities +import Mathlib.Data.Nat.NthRoot.Defs +import Mathlib.Tactic.Rify + +/-! +# Lemmas about `Nat.nthRoot` + +In this file we prove that `Nat.nthRoot n a` is indeed the floor of `ⁿ√a`. + +## TODO + +Rewrite proofs to avoid dependencies on real numbers, +so that we can move this file to Batteries. +-/ + +namespace Nat + +@[simp] theorem nthRoot_zero_left (a : ℕ) : nthRoot 0 a = 1 := rfl + +@[simp] theorem nthRoot_one_left : nthRoot 1 = id := rfl + +theorem nthRoot.pow_go_le (n a b : ℕ) : (go n a b)^(n + 2) ≤ a := by + induction b using Nat.strongRecOn with + | ind b ihb => + rw [go] + split_ifs with h + case pos => + exact ihb _ h + case neg => + have : b ≤ a / b^(n + 1) := by linarith only [Nat.mul_le_of_le_div _ _ _ (not_lt.1 h)] + replace := Nat.mul_le_of_le_div _ _ _ this + rwa [← Nat.pow_succ'] at this + +variable {n a b : ℕ} + +theorem nthRoot.lt_pow_go_succ_aux (h : a < b ^ (n + 1)) : + a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by + rcases eq_or_ne b 0 with rfl | hb; · simp at h + rcases Nat.eq_zero_or_pos n with rfl | hn; · simp + rw [← Nat.add_mul_div_left a, Nat.div_div_eq_div_mul] <;> try positivity + rify + calc + (a : ℝ) = ((a / b^n) ^ (1 / (n + 1) : ℝ) * b^(n / (n + 1) : ℝ)) ^ (n + 1) := by + rw [mul_pow, ← Real.rpow_mul_natCast, ← Real.rpow_mul_natCast] <;> try positivity + field_simp + _ ≤ ((1 / (n + 1)) * (a / b^n) + (n / (n + 1)) * b) ^ (n + 1) := by + gcongr + apply Real.geom_mean_le_arith_mean2_weighted <;> try positivity + field_simp [add_comm] + _ = ((a + b^n * (n * b)) / (b^n * (n + 1))) ^ (n + 1) := by + congr 1 + field_simp + ring + _ < _ := by + gcongr ?_ ^ _ + convert lt_floor_add_one (R := ℝ) _ using 1 + norm_cast + rw [Nat.floor_div_natCast, Nat.floor_natCast] + +theorem nthRoot.lt_pow_go_succ (hb : a < (b + 1) ^ (n + 2)) : a < (go n a b + 1) ^ (n + 2) := by + induction b using Nat.strongRecOn with + | ind b ihb => + rw [go] + split_ifs with h + case pos => + rcases eq_or_ne b 0 with rfl | hb + · simp at * + apply ihb _ h + replace h : a < b^(n + 2) := by + rw [Nat.div_lt_iff_lt_mul (by positivity)] at h + replace h : a / b ^ (n + 1) < b := by linarith only [h] + rwa [Nat.div_lt_iff_lt_mul (by positivity), ← Nat.pow_succ'] at h + exact Nat.nthRoot.lt_pow_go_succ_aux h + case neg => + assumption + +theorem pow_nthRoot_le (hn : n ≠ 0) (a : ℕ) : (nthRoot n a)^n ≤ a := by + match n, hn with + | 1, _ => simp + | n + 2, _ => + simp only [nthRoot] + split_ifs with h + case pos => interval_cases a <;> simp + case neg => apply nthRoot.pow_go_le + +theorem lt_pow_nthRoot_add_one (hn : n ≠ 0) (a : ℕ) : a < (nthRoot n a + 1)^n := by + match n, hn with + | 1, _ => simp + | n + 2, hn => + simp only [nthRoot] + split_ifs with h + case pos => interval_cases a <;> simp + case neg => + apply nthRoot.lt_pow_go_succ + exact a.lt_succ_self.trans_le (Nat.le_self_pow hn _) + +@[simp] +theorem le_nthRoot_iff (hn : n ≠ 0) : a ≤ nthRoot n b ↔ a^n ≤ b := by + cases le_or_gt a (nthRoot n b) with + | inl hle => + simp only [hle, true_iff] + refine le_trans ?_ (pow_nthRoot_le hn b) + gcongr + | inr hlt => + simp only [hlt.not_ge, false_iff, not_le] + refine (lt_pow_nthRoot_add_one hn b).trans_le ?_ + gcongr + assumption + +@[simp] +theorem nthRoot_lt_iff (hn : n ≠ 0) : nthRoot n a < b ↔ a < b^n := by + simp only [← not_le, le_nthRoot_iff hn] + +@[simp] +theorem nthRoot_pow (hn : n ≠ 0) (a : ℕ) : nthRoot n (a ^ n) = a := by + refine eq_of_forall_le_iff fun b ↦ ?_ + rw [le_nthRoot_iff hn] + exact (Nat.pow_left_strictMono hn).le_iff_le + +theorem nthRoot_eq_of_le_of_lt (h₁ : a ^ n ≤ b) (h₂ : b < (a + 1) ^ n) : + nthRoot n b = a := by + rcases eq_or_ne n 0 with rfl | hn + · rw [pow_zero] at *; omega + simp only [← le_nthRoot_iff hn, ← nthRoot_lt_iff hn] at h₁ h₂ + omega + +theorem exists_pow_eq_iff' (hn : n ≠ 0) : (∃ x, x ^ n = a) ↔ (nthRoot n a) ^ n = a := by + constructor + · rintro ⟨x, rfl⟩ + rw [nthRoot_pow hn] + · exact fun h ↦ ⟨_, h⟩ + +theorem exists_pow_eq_iff : + (∃ x, x ^ n = a) ↔ ((n = 0 ∧ a = 1) ∨ (n ≠ 0 ∧ (nthRoot n a) ^ n = a)) := by + rcases eq_or_ne n 0 with rfl | hn + · simp [eq_comm] + · simp [exists_pow_eq_iff', hn] + +instance instDecidableExistsPowEq : Decidable (∃ x, x ^ n = a) := + decidable_of_iff' _ exists_pow_eq_iff + +end Nat From 5c26b942f9cca37937ff93188e97bee93a9d6af6 Mon Sep 17 00:00:00 2001 From: Yury Kudryashov <162619279+yury-harmonic@users.noreply.github.com> Date: Fri, 22 Aug 2025 14:55:04 -0500 Subject: [PATCH 02/10] Apply suggestions from code review Co-authored-by: Jireh Loreaux --- Mathlib/Data/Nat/NthRoot/Lemmas.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Mathlib/Data/Nat/NthRoot/Lemmas.lean b/Mathlib/Data/Nat/NthRoot/Lemmas.lean index fc74501bcb8730..f056f330f7977c 100644 --- a/Mathlib/Data/Nat/NthRoot/Lemmas.lean +++ b/Mathlib/Data/Nat/NthRoot/Lemmas.lean @@ -24,7 +24,7 @@ namespace Nat @[simp] theorem nthRoot_one_left : nthRoot 1 = id := rfl -theorem nthRoot.pow_go_le (n a b : ℕ) : (go n a b)^(n + 2) ≤ a := by +theorem nthRoot.pow_go_le (n a b : ℕ) : (go n a b) ^ (n + 2) ≤ a := by induction b using Nat.strongRecOn with | ind b ihb => rw [go] @@ -45,14 +45,14 @@ theorem nthRoot.lt_pow_go_succ_aux (h : a < b ^ (n + 1)) : rw [← Nat.add_mul_div_left a, Nat.div_div_eq_div_mul] <;> try positivity rify calc - (a : ℝ) = ((a / b^n) ^ (1 / (n + 1) : ℝ) * b^(n / (n + 1) : ℝ)) ^ (n + 1) := by + (a : ℝ) = ((a / b ^ n) ^ (1 / (n + 1) : ℝ) * b ^ (n / (n + 1) : ℝ)) ^ (n + 1) := by rw [mul_pow, ← Real.rpow_mul_natCast, ← Real.rpow_mul_natCast] <;> try positivity field_simp - _ ≤ ((1 / (n + 1)) * (a / b^n) + (n / (n + 1)) * b) ^ (n + 1) := by + _ ≤ ((1 / (n + 1)) * (a / b ^ n) + (n / (n + 1)) * b) ^ (n + 1) := by gcongr apply Real.geom_mean_le_arith_mean2_weighted <;> try positivity field_simp [add_comm] - _ = ((a + b^n * (n * b)) / (b^n * (n + 1))) ^ (n + 1) := by + _ = ((a + b ^ n * (n * b)) / (b ^ n * (n + 1))) ^ (n + 1) := by congr 1 field_simp ring @@ -71,7 +71,7 @@ theorem nthRoot.lt_pow_go_succ (hb : a < (b + 1) ^ (n + 2)) : a < (go n a b + 1) rcases eq_or_ne b 0 with rfl | hb · simp at * apply ihb _ h - replace h : a < b^(n + 2) := by + replace h : a < b ^ (n + 2) := by rw [Nat.div_lt_iff_lt_mul (by positivity)] at h replace h : a / b ^ (n + 1) < b := by linarith only [h] rwa [Nat.div_lt_iff_lt_mul (by positivity), ← Nat.pow_succ'] at h @@ -79,7 +79,7 @@ theorem nthRoot.lt_pow_go_succ (hb : a < (b + 1) ^ (n + 2)) : a < (go n a b + 1) case neg => assumption -theorem pow_nthRoot_le (hn : n ≠ 0) (a : ℕ) : (nthRoot n a)^n ≤ a := by +theorem pow_nthRoot_le (hn : n ≠ 0) (a : ℕ) : (nthRoot n a) ^ n ≤ a := by match n, hn with | 1, _ => simp | n + 2, _ => @@ -88,7 +88,7 @@ theorem pow_nthRoot_le (hn : n ≠ 0) (a : ℕ) : (nthRoot n a)^n ≤ a := by case pos => interval_cases a <;> simp case neg => apply nthRoot.pow_go_le -theorem lt_pow_nthRoot_add_one (hn : n ≠ 0) (a : ℕ) : a < (nthRoot n a + 1)^n := by +theorem lt_pow_nthRoot_add_one (hn : n ≠ 0) (a : ℕ) : a < (nthRoot n a + 1) ^ n := by match n, hn with | 1, _ => simp | n + 2, hn => @@ -100,7 +100,7 @@ theorem lt_pow_nthRoot_add_one (hn : n ≠ 0) (a : ℕ) : a < (nthRoot n a + 1)^ exact a.lt_succ_self.trans_le (Nat.le_self_pow hn _) @[simp] -theorem le_nthRoot_iff (hn : n ≠ 0) : a ≤ nthRoot n b ↔ a^n ≤ b := by +theorem le_nthRoot_iff (hn : n ≠ 0) : a ≤ nthRoot n b ↔ a ^ n ≤ b := by cases le_or_gt a (nthRoot n b) with | inl hle => simp only [hle, true_iff] @@ -113,7 +113,7 @@ theorem le_nthRoot_iff (hn : n ≠ 0) : a ≤ nthRoot n b ↔ a^n ≤ b := by assumption @[simp] -theorem nthRoot_lt_iff (hn : n ≠ 0) : nthRoot n a < b ↔ a < b^n := by +theorem nthRoot_lt_iff (hn : n ≠ 0) : nthRoot n a < b ↔ a < b ^ n := by simp only [← not_le, le_nthRoot_iff hn] @[simp] From e6676eaa4929c5ffde8da40c1ae4fa46c8b5f9e3 Mon Sep 17 00:00:00 2001 From: Yury Kudryashov Date: Sat, 23 Aug 2025 02:00:53 +0000 Subject: [PATCH 03/10] Redefine --- Mathlib/Data/Nat/NthRoot/Defs.lean | 26 +++++++++++++++++++++----- 1 file changed, 21 insertions(+), 5 deletions(-) diff --git a/Mathlib/Data/Nat/NthRoot/Defs.lean b/Mathlib/Data/Nat/NthRoot/Defs.lean index 88e9cfb128676e..0d826102ebcd9e 100644 --- a/Mathlib/Data/Nat/NthRoot/Defs.lean +++ b/Mathlib/Data/Nat/NthRoot/Defs.lean @@ -13,15 +13,31 @@ The function is defined in terms of natural numbers with no dependencies outside /-- `Nat.nthRoot n a = ⌊(a : ℝ) ^ (1 / n : ℝ)⌋₊` defined in terms of natural numbers. -We use Lagrange's method to find a root of $x^n = a$, +We use Newthon's method to find a root of $x^n = a$, so it converges superexponentially fast. -/ def Nat.nthRoot : Nat → Nat → Nat | 0, _ => 1 | 1, a => a | n + 2, a => - if a ≤ 1 then a else go n a a + if a ≤ 1 then a else go a n a a where - /-- Auxiliary definition for `Nat.nthRoot`. -/ - go n a guess := + /-- Auxiliary definition for `Nat.nthRoot`. + + Given natural numbers `fuel`, `n`, `a`, `guess` + such that `⌊(a : ℝ) ^ (1 / (n + 2) : ℝ)⌋₊ ≤ guess ≤ fuel`, + returns `⌊(a : ℝ) ^ (1 / (n + 2) : ℝ)⌋₊`. + + The auxiliary number `guess` is the current approximation in Newthon's method, + tracked in the arguments so that the definition uses a tail recursion + which is unfolded into a loop by the compiler. + + The auxiliary number `fuel` is an upper estimate on the number of steps in Newthon's method. + Any number `fuel ≥ guess` is guaranteed to work, but smaller numbers may work as well. + If `fuel` is too small, then `Nat.nthRoot.go` returns the result of the `fuel`th step + of Newthon's method. + -/ + go + | 0, _, _, guess => guess + | fuel + 1, n, a, guess => let next := (a / guess^(n + 1) + (n + 1) * guess) / (n + 2) - if next < guess then go n a next else guess + if next < guess then go fuel n a next else guess From 65d1045bc61e4b81ba69af3b1c6fd03a464213cf Mon Sep 17 00:00:00 2001 From: Yury Kudryashov Date: Sat, 23 Aug 2025 03:02:02 +0000 Subject: [PATCH 04/10] Fix --- Mathlib/Data/Nat/NthRoot/Defs.lean | 12 ++-- Mathlib/Data/Nat/NthRoot/Lemmas.lean | 84 ++++++++++++++++++---------- 2 files changed, 61 insertions(+), 35 deletions(-) diff --git a/Mathlib/Data/Nat/NthRoot/Defs.lean b/Mathlib/Data/Nat/NthRoot/Defs.lean index 0d826102ebcd9e..743fc3e6089f3f 100644 --- a/Mathlib/Data/Nat/NthRoot/Defs.lean +++ b/Mathlib/Data/Nat/NthRoot/Defs.lean @@ -19,11 +19,11 @@ def Nat.nthRoot : Nat → Nat → Nat | 0, _ => 1 | 1, a => a | n + 2, a => - if a ≤ 1 then a else go a n a a + go n a a a where /-- Auxiliary definition for `Nat.nthRoot`. - Given natural numbers `fuel`, `n`, `a`, `guess` + Given natural numbers `n`, `a`, `fuel`, `guess` such that `⌊(a : ℝ) ^ (1 / (n + 2) : ℝ)⌋₊ ≤ guess ≤ fuel`, returns `⌊(a : ℝ) ^ (1 / (n + 2) : ℝ)⌋₊`. @@ -36,8 +36,8 @@ def Nat.nthRoot : Nat → Nat → Nat If `fuel` is too small, then `Nat.nthRoot.go` returns the result of the `fuel`th step of Newthon's method. -/ - go - | 0, _, _, guess => guess - | fuel + 1, n, a, guess => + go (n a : Nat) + | 0, guess => guess + | fuel + 1, guess => let next := (a / guess^(n + 1) + (n + 1) * guess) / (n + 2) - if next < guess then go fuel n a next else guess + if next < guess then go n a fuel next else guess diff --git a/Mathlib/Data/Nat/NthRoot/Lemmas.lean b/Mathlib/Data/Nat/NthRoot/Lemmas.lean index f056f330f7977c..fd649117eb662e 100644 --- a/Mathlib/Data/Nat/NthRoot/Lemmas.lean +++ b/Mathlib/Data/Nat/NthRoot/Lemmas.lean @@ -14,30 +14,65 @@ In this file we prove that `Nat.nthRoot n a` is indeed the floor of `ⁿ√a`. ## TODO -Rewrite proofs to avoid dependencies on real numbers, +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 Batteries. -/ namespace Nat +variable {m n a b guess fuel : ℕ} + @[simp] theorem nthRoot_zero_left (a : ℕ) : nthRoot 0 a = 1 := rfl @[simp] theorem nthRoot_one_left : nthRoot 1 = id := rfl -theorem nthRoot.pow_go_le (n a b : ℕ) : (go n a b) ^ (n + 2) ≤ a := by - induction b using Nat.strongRecOn with - | ind b ihb => +@[simp] +theorem nthRoot_zero_right (h : n ≠ 0) : nthRoot n 0 = 0 := by + match n, h with + | 1, _ => simp + | n + 2, _ => simp [nthRoot, nthRoot.go] + +@[simp] +theorem nthRoot_one_right : nthRoot n 1 = 1 := by + rcases n with _|_|_ <;> simp [nthRoot, nthRoot.go, Nat.add_comm 1] + +private theorem nthRoot.pow_go_le (hle : guess ≤ fuel) (n a : ℕ) : + go n a fuel guess ^ (n + 2) ≤ a := by + induction fuel generalizing guess with + | zero => + obtain rfl : guess = 0 := by omega + simp [go] + | succ fuel ih => rw [go] split_ifs with h case pos => - exact ihb _ h + apply ih + omega case neg => - have : b ≤ a / b^(n + 1) := by linarith only [Nat.mul_le_of_le_div _ _ _ (not_lt.1 h)] + have : guess ≤ a / guess ^ (n + 1) := by + linarith only [Nat.mul_le_of_le_div _ _ _ (not_lt.1 h)] replace := Nat.mul_le_of_le_div _ _ _ this rwa [← Nat.pow_succ'] at this -variable {n a b : ℕ} +/-- `nthRoot n a ^ n ≤ a` unless both `n` and `a` are zeros. -/ +@[simp] +theorem pow_nthRoot_le_iff : nthRoot n a ^ n ≤ a ↔ n ≠ 0 ∨ a ≠ 0 := by + match n with + | 0 => simp [Nat.one_le_iff_ne_zero] + | 1 => simp + | n + 2 => simp [nthRoot, nthRoot.pow_go_le] + +alias ⟨_, pow_nthRoot_le⟩ := pow_nthRoot_le_iff + +/-- +An auxiliary lemma saying that if `b` is a strict upper estimate on `√[n + 1] a`, +then so is `(a / b ^ n + n * b) / (n + 1) + 1`. + +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 nthRoot.lt_pow_go_succ_aux (h : a < b ^ (n + 1)) : a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by rcases eq_or_ne b 0 with rfl | hb; · simp at h @@ -62,49 +97,39 @@ theorem nthRoot.lt_pow_go_succ_aux (h : a < b ^ (n + 1)) : norm_cast rw [Nat.floor_div_natCast, Nat.floor_natCast] -theorem nthRoot.lt_pow_go_succ (hb : a < (b + 1) ^ (n + 2)) : a < (go n a b + 1) ^ (n + 2) := by - induction b using Nat.strongRecOn with - | ind b ihb => +private theorem nthRoot.lt_pow_go_succ (hlt : a < (guess + 1) ^ (n + 2)) : + a < (go n a fuel guess + 1) ^ (n + 2) := by + induction fuel generalizing guess with + | zero => simpa [go] + | succ fuel ih => rw [go] split_ifs with h case pos => - rcases eq_or_ne b 0 with rfl | hb + rcases eq_or_ne guess 0 with rfl | hguess · simp at * - apply ihb _ h - replace h : a < b ^ (n + 2) := by + apply ih + replace h : a < guess ^ (n + 2) := by rw [Nat.div_lt_iff_lt_mul (by positivity)] at h - replace h : a / b ^ (n + 1) < b := by linarith only [h] + replace h : a / guess ^ (n + 1) < guess := by linarith only [h] rwa [Nat.div_lt_iff_lt_mul (by positivity), ← Nat.pow_succ'] at h exact Nat.nthRoot.lt_pow_go_succ_aux h case neg => assumption -theorem pow_nthRoot_le (hn : n ≠ 0) (a : ℕ) : (nthRoot n a) ^ n ≤ a := by - match n, hn with - | 1, _ => simp - | n + 2, _ => - simp only [nthRoot] - split_ifs with h - case pos => interval_cases a <;> simp - case neg => apply nthRoot.pow_go_le - theorem lt_pow_nthRoot_add_one (hn : n ≠ 0) (a : ℕ) : a < (nthRoot n a + 1) ^ n := by match n, hn with | 1, _ => simp | n + 2, hn => simp only [nthRoot] - split_ifs with h - case pos => interval_cases a <;> simp - case neg => - apply nthRoot.lt_pow_go_succ - exact a.lt_succ_self.trans_le (Nat.le_self_pow hn _) + apply nthRoot.lt_pow_go_succ + exact a.lt_succ_self.trans_le (Nat.le_self_pow hn _) @[simp] theorem le_nthRoot_iff (hn : n ≠ 0) : a ≤ nthRoot n b ↔ a ^ n ≤ b := by cases le_or_gt a (nthRoot n b) with | inl hle => simp only [hle, true_iff] - refine le_trans ?_ (pow_nthRoot_le hn b) + refine le_trans ?_ (pow_nthRoot_le (.inl hn)) gcongr | inr hlt => simp only [hlt.not_ge, false_iff, not_le] @@ -122,6 +147,7 @@ theorem nthRoot_pow (hn : n ≠ 0) (a : ℕ) : nthRoot n (a ^ n) = a := by rw [le_nthRoot_iff hn] exact (Nat.pow_left_strictMono hn).le_iff_le +/-- If `a ^ n ≤ b < (a + 1) ^ n`, then `n` root of `b` equals `a`. -/ theorem nthRoot_eq_of_le_of_lt (h₁ : a ^ n ≤ b) (h₂ : b < (a + 1) ^ n) : nthRoot n b = a := by rcases eq_or_ne n 0 with rfl | hn From f911978c734c7c560f9dc9f4dd4764b2b28f6ff1 Mon Sep 17 00:00:00 2001 From: Yury Kudryashov <162619279+yury-harmonic@users.noreply.github.com> Date: Mon, 6 Oct 2025 07:53:25 -0500 Subject: [PATCH 05/10] Apply suggestions from code review Co-authored-by: Yakov Pechersky --- Mathlib/Data/Nat/NthRoot/Lemmas.lean | 28 ++++++++++------------------ 1 file changed, 10 insertions(+), 18 deletions(-) diff --git a/Mathlib/Data/Nat/NthRoot/Lemmas.lean b/Mathlib/Data/Nat/NthRoot/Lemmas.lean index fd649117eb662e..a295847124ee33 100644 --- a/Mathlib/Data/Nat/NthRoot/Lemmas.lean +++ b/Mathlib/Data/Nat/NthRoot/Lemmas.lean @@ -28,9 +28,7 @@ variable {m n a b guess fuel : ℕ} @[simp] theorem nthRoot_zero_right (h : n ≠ 0) : nthRoot n 0 = 0 := by - match n, h with - | 1, _ => simp - | n + 2, _ => simp [nthRoot, nthRoot.go] + rcases n with _|_|_ <;> grind [nthRoot, nthRoot.go] @[simp] theorem nthRoot_one_right : nthRoot n 1 = 1 := by @@ -40,27 +38,23 @@ private theorem nthRoot.pow_go_le (hle : guess ≤ fuel) (n a : ℕ) : go n a fuel guess ^ (n + 2) ≤ a := by induction fuel generalizing guess with | zero => - obtain rfl : guess = 0 := by omega + obtain rfl : guess = 0 := by grind simp [go] | succ fuel ih => rw [go] split_ifs with h case pos => - apply ih - omega + grind case neg => have : guess ≤ a / guess ^ (n + 1) := by linarith only [Nat.mul_le_of_le_div _ _ _ (not_lt.1 h)] replace := Nat.mul_le_of_le_div _ _ _ this - rwa [← Nat.pow_succ'] at this + grind /-- `nthRoot n a ^ n ≤ a` unless both `n` and `a` are zeros. -/ @[simp] theorem pow_nthRoot_le_iff : nthRoot n a ^ n ≤ a ↔ n ≠ 0 ∨ a ≠ 0 := by - match n with - | 0 => simp [Nat.one_le_iff_ne_zero] - | 1 => simp - | n + 2 => simp [nthRoot, nthRoot.pow_go_le] + rcases n with _|_|_ <;> first | grind | simp [nthRoot, nthRoot.pow_go_le] alias ⟨_, pow_nthRoot_le⟩ := pow_nthRoot_le_iff @@ -106,7 +100,7 @@ private theorem nthRoot.lt_pow_go_succ (hlt : a < (guess + 1) ^ (n + 2)) : split_ifs with h case pos => rcases eq_or_ne guess 0 with rfl | hguess - · simp at * + · grind apply ih replace h : a < guess ^ (n + 2) := by rw [Nat.div_lt_iff_lt_mul (by positivity)] at h @@ -151,21 +145,19 @@ theorem nthRoot_pow (hn : n ≠ 0) (a : ℕ) : nthRoot n (a ^ n) = a := by theorem nthRoot_eq_of_le_of_lt (h₁ : a ^ n ≤ b) (h₂ : b < (a + 1) ^ n) : nthRoot n b = a := by rcases eq_or_ne n 0 with rfl | hn - · rw [pow_zero] at *; omega + · grind simp only [← le_nthRoot_iff hn, ← nthRoot_lt_iff hn] at h₁ h₂ - omega + grind theorem exists_pow_eq_iff' (hn : n ≠ 0) : (∃ x, x ^ n = a) ↔ (nthRoot n a) ^ n = a := by constructor · rintro ⟨x, rfl⟩ rw [nthRoot_pow hn] - · exact fun h ↦ ⟨_, h⟩ + · grind theorem exists_pow_eq_iff : (∃ x, x ^ n = a) ↔ ((n = 0 ∧ a = 1) ∨ (n ≠ 0 ∧ (nthRoot n a) ^ n = a)) := by - rcases eq_or_ne n 0 with rfl | hn - · simp [eq_comm] - · simp [exists_pow_eq_iff', hn] + rcases eq_or_ne n 0 with rfl | _ <;> grind [exists_pow_eq_iff'] instance instDecidableExistsPowEq : Decidable (∃ x, x ^ n = a) := decidable_of_iff' _ exists_pow_eq_iff From 79bec62df69e0cd1643388369a08e4a4f2d79409 Mon Sep 17 00:00:00 2001 From: Yury Kudryashov Date: Tue, 7 Oct 2025 15:43:14 +0000 Subject: [PATCH 06/10] Partially fix --- Mathlib/Data/Nat/NthRoot/Lemmas.lean | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/Mathlib/Data/Nat/NthRoot/Lemmas.lean b/Mathlib/Data/Nat/NthRoot/Lemmas.lean index a295847124ee33..303ca929fe4b73 100644 --- a/Mathlib/Data/Nat/NthRoot/Lemmas.lean +++ b/Mathlib/Data/Nat/NthRoot/Lemmas.lean @@ -3,6 +3,7 @@ Copyright (c) 2025 Concordance Inc. dba Harmonic. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury Kudryashov -/ +import Mathlib.Algebra.Order.Floor.Semifield import Mathlib.Analysis.MeanInequalities import Mathlib.Data.Nat.NthRoot.Defs import Mathlib.Tactic.Rify @@ -59,32 +60,30 @@ theorem pow_nthRoot_le_iff : nthRoot n a ^ n ≤ a ↔ n ≠ 0 ∨ a ≠ 0 := by alias ⟨_, pow_nthRoot_le⟩ := pow_nthRoot_le_iff /-- -An auxiliary lemma saying that if `b` is a strict upper estimate on `√[n + 1] a`, -then so is `(a / b ^ n + n * b) / (n + 1) + 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 nthRoot.lt_pow_go_succ_aux (h : a < b ^ (n + 1)) : +theorem nthRoot.lt_pow_go_succ_aux (hb : b ≠ 0) : a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by - rcases eq_or_ne b 0 with rfl | hb; · simp at h rcases Nat.eq_zero_or_pos n with rfl | hn; · simp rw [← Nat.add_mul_div_left a, Nat.div_div_eq_div_mul] <;> try positivity rify calc (a : ℝ) = ((a / b ^ n) ^ (1 / (n + 1) : ℝ) * b ^ (n / (n + 1) : ℝ)) ^ (n + 1) := by rw [mul_pow, ← Real.rpow_mul_natCast, ← Real.rpow_mul_natCast] <;> try positivity - field_simp + simp (disch := positivity) [div_mul_cancel₀] _ ≤ ((1 / (n + 1)) * (a / b ^ n) + (n / (n + 1)) * b) ^ (n + 1) := by gcongr apply Real.geom_mean_le_arith_mean2_weighted <;> try positivity - field_simp [add_comm] + simp [field, add_comm] _ = ((a + b ^ n * (n * b)) / (b ^ n * (n + 1))) ^ (n + 1) := by congr 1 field_simp - ring _ < _ := by gcongr ?_ ^ _ convert lt_floor_add_one (R := ℝ) _ using 1 @@ -101,12 +100,7 @@ private theorem nthRoot.lt_pow_go_succ (hlt : a < (guess + 1) ^ (n + 2)) : case pos => rcases eq_or_ne guess 0 with rfl | hguess · grind - apply ih - replace h : a < guess ^ (n + 2) := by - rw [Nat.div_lt_iff_lt_mul (by positivity)] at h - replace h : a / guess ^ (n + 1) < guess := by linarith only [h] - rwa [Nat.div_lt_iff_lt_mul (by positivity), ← Nat.pow_succ'] at h - exact Nat.nthRoot.lt_pow_go_succ_aux h + · exact ih <| Nat.nthRoot.lt_pow_go_succ_aux hguess case neg => assumption From d976e01fb092e845bc6cae0a5aa93bdf0f2bb5e9 Mon Sep 17 00:00:00 2001 From: Yury Kudryashov Date: Fri, 10 Oct 2025 21:54:55 +0000 Subject: [PATCH 07/10] Move a file --- Mathlib.lean | 2 +- .../SpecialFunctions/Pow/NthRootLemmas.lean} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename Mathlib/{Data/Nat/NthRoot/Lemmas.lean => Analysis/SpecialFunctions/Pow/NthRootLemmas.lean} (100%) diff --git a/Mathlib.lean b/Mathlib.lean index 03c8e7924c34c1..78fa3250955559 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1999,6 +1999,7 @@ import Mathlib.Analysis.SpecialFunctions.Pow.Continuity import Mathlib.Analysis.SpecialFunctions.Pow.Deriv import Mathlib.Analysis.SpecialFunctions.Pow.Integral import Mathlib.Analysis.SpecialFunctions.Pow.NNReal +import Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Analysis.SpecialFunctions.Sigmoid import Mathlib.Analysis.SpecialFunctions.SmoothTransition @@ -3526,7 +3527,6 @@ import Mathlib.Data.Nat.Multiplicity import Mathlib.Data.Nat.Notation import Mathlib.Data.Nat.Nth import Mathlib.Data.Nat.NthRoot.Defs -import Mathlib.Data.Nat.NthRoot.Lemmas import Mathlib.Data.Nat.Order.Lemmas import Mathlib.Data.Nat.PSub import Mathlib.Data.Nat.Pairing diff --git a/Mathlib/Data/Nat/NthRoot/Lemmas.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean similarity index 100% rename from Mathlib/Data/Nat/NthRoot/Lemmas.lean rename to Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean From 3dc663aa600c5fcc0845ac0e699defdf747aa9f2 Mon Sep 17 00:00:00 2001 From: Yury Kudryashov Date: Fri, 10 Oct 2025 21:56:24 +0000 Subject: [PATCH 08/10] Change TODO --- Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean index 303ca929fe4b73..50f882c2356563 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean @@ -16,7 +16,7 @@ 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 Batteries. +so that we can move this file to `Mathlib/Data/Nat/NthRoot`, then to Batteries. -/ namespace Nat From f7584e2210c401f6b3b2e338295b18a2e08c0aae Mon Sep 17 00:00:00 2001 From: Yury Kudryashov Date: Mon, 13 Oct 2025 15:05:54 +0000 Subject: [PATCH 09/10] Fix typos --- Mathlib/Data/Nat/NthRoot/Defs.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Data/Nat/NthRoot/Defs.lean b/Mathlib/Data/Nat/NthRoot/Defs.lean index 743fc3e6089f3f..13b52292e6dd18 100644 --- a/Mathlib/Data/Nat/NthRoot/Defs.lean +++ b/Mathlib/Data/Nat/NthRoot/Defs.lean @@ -13,7 +13,7 @@ The function is defined in terms of natural numbers with no dependencies outside /-- `Nat.nthRoot n a = ⌊(a : ℝ) ^ (1 / n : ℝ)⌋₊` defined in terms of natural numbers. -We use Newthon's method to find a root of $x^n = a$, +We use Newton's method to find a root of $x^n = a$, so it converges superexponentially fast. -/ def Nat.nthRoot : Nat → Nat → Nat | 0, _ => 1 @@ -27,14 +27,14 @@ def Nat.nthRoot : Nat → Nat → Nat such that `⌊(a : ℝ) ^ (1 / (n + 2) : ℝ)⌋₊ ≤ guess ≤ fuel`, returns `⌊(a : ℝ) ^ (1 / (n + 2) : ℝ)⌋₊`. - The auxiliary number `guess` is the current approximation in Newthon's method, + The auxiliary number `guess` is the current approximation in Newton's method, tracked in the arguments so that the definition uses a tail recursion which is unfolded into a loop by the compiler. - The auxiliary number `fuel` is an upper estimate on the number of steps in Newthon's method. + The auxiliary number `fuel` is an upper estimate on the number of steps in Newton's method. Any number `fuel ≥ guess` is guaranteed to work, but smaller numbers may work as well. If `fuel` is too small, then `Nat.nthRoot.go` returns the result of the `fuel`th step - of Newthon's method. + of Newton's method. -/ go (n a : Nat) | 0, guess => guess From 349f2fc23f90aedf91faaff49af2270ededaafda Mon Sep 17 00:00:00 2001 From: Yury Kudryashov Date: Thu, 16 Oct 2025 18:32:31 +0000 Subject: [PATCH 10/10] Import `Mathlib.Init` --- Mathlib/Data/Nat/NthRoot/Defs.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Data/Nat/NthRoot/Defs.lean b/Mathlib/Data/Nat/NthRoot/Defs.lean index 13b52292e6dd18..bf6a6e6d550563 100644 --- a/Mathlib/Data/Nat/NthRoot/Defs.lean +++ b/Mathlib/Data/Nat/NthRoot/Defs.lean @@ -3,6 +3,7 @@ Copyright (c) 2025 Concordance Inc. dba Harmonic. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury Kudryashov -/ +import Mathlib.Init /-! # Definition of `Nat.nthRoot`