def Hex.PolyQuot.evalRatBall (f : DensePoly Rat) (s : DyadicSquare) (coeffPrec : Int) : DyadicComplexBall

Horner evaluation of a rational polynomial on the circumscribed disc of a dyadic square.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PolyQuot.coeffBits (f : DensePoly Rat) : Nat

Bit-length upper bound for the magnitudes of rational coefficients. Since every rational denominator is positive, the numerator magnitude alone is a valid upper bound.

Equations

• Hex.PolyQuot.coeffBits f = Array.foldl (fun (bits : Nat) (q : Rat) => bits.max (Hex.ceilLog2 (q.num.natAbs + 1))) 0 f.toArray

def Hex.PolyQuot.rootBits (s : DyadicSquare) : Nat

Bit-length upper bound for the magnitude of every point in a square's circumscribed disc. The bound is clamped at zero when the disc lies inside the unit circle.

Equations

• Hex.PolyQuot.rootBits s = (max 0 (Hex.Dyadic.ceilLog2 (s.center.hi + s.radiusHi))).toNat

def Hex.PolyQuot.approxGuardBits (s : DyadicSquare) (f : DensePoly Rat) : Nat

Guard bits sufficient for coefficient rounding and Horner amplification over the selected root's certified circumscribed disc.

Equations

• Hex.PolyQuot.approxGuardBits s f = 8 + Hex.ceilLog2 (f.size + 1) + Hex.PolyQuot.coeffBits f + f.size * (Hex.PolyQuot.rootBits s + 3)