Definition of Nat.nthRoot

In this file we define Nat.nthRoot n a to be the floor of the nth root of a. The function is defined in terms of natural numbers with no dependencies outside of prelude.

def Nat.nthRoot : Nat → Nat → Nat

Nat.nthRoot n a = ⌊(a : ℝ) ^ (1 / n : ℝ)⌋₊ defined in terms of natural numbers.

We use Newton's method to find a root of $x^n = a$, so it converges superexponentially fast.

Equations

• Nat.nthRoot 0 x✝ = 1
• Nat.nthRoot 1 x✝ = x✝
• n.succ.succ.nthRoot x✝ = Nat.nthRoot.go n x✝ x✝ x✝

def Nat.nthRoot.go (n a : Nat) : Nat → Nat → Nat

Auxiliary definition for Nat.nthRoot.

Given natural numbers n, a, fuel, guess such that ⌊(a : ℝ) ^ (1 / (n + 2) : ℝ)⌋₊ ≤ guess ≤ fuel, returns ⌊(a : ℝ) ^ (1 / (n + 2) : ℝ)⌋₊.

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 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 fuelth step of Newton's method.

Equations

• Nat.nthRoot.go n a 0 x✝ = x✝
• Nat.nthRoot.go n a fuel.succ x✝ = if (a / x✝ ^ (n + 1) + (n + 1) * x✝) / (n + 2) < x✝ then Nat.nthRoot.go n a fuel ((a / x✝ ^ (n + 1) + (n + 1) * x✝) / (n + 2)) else x✝