8.1. Introduction
HexPoly multiplies polynomials by the schoolbook method,
divides them by long division and computes their gcd by Euclid's algorithm.
All three take a number of coefficient operations quadratic in the degree. HexPolyFast implements the
classical faster algorithms for the same type DensePoly R: Karatsuba
multiplication, division by Newton iteration, the half-gcd algorithm, product
and remainder trees for evaluating and interpolating at many points, and Padé
approximation. Each operation that HexPoly already has comes with a theorem
saying that the fast version returns exactly the same polynomial, and each new
operation comes with a theorem saying what its answer is.
A Padé approximant of a power series is a rational function p / q whose own
power series agrees with it to a given order. If a sequence satisfies a linear
recurrence of order n, its generating function is a rational function whose
denominator has degree at most n, and a Padé approximant recovers it from the
first 2n terms. The numbers of ways to tile a 3 × 2k rectangle with
dominoes are 1, 3, 11, 41, 153, 571, 2131, 7953, …. Asking for a numerator
of degree at most 1 and a denominator of degree at most 2 finds their
generating function:
open Hex Hex.DensePoly
namespace HexPolyFastChapter
def tilings : TSeries Rat 8 :=
TSeries.ofFn fun i =>
[1, 3, 11, 41, 153, 571, 2131, 7953].getD i 0
#eval (pade? (karatsubaPlan 32) tilings 1 2).map
fun a => (a.p, a.q)
A polynomial prints as the list of its coefficients, constant term first, so
the generating function is (1 - x) / (1 - 4x + x²), and the tilings satisfy
aₖ = 4aₖ₋₁ - aₖ₋₂. The approximant was computed from the first four terms.
Multiplying all eight terms by the denominator, and keeping the coefficients
of 1, x, …, x⁷, gives back the numerator, so the other four terms satisfy
the recurrence too:
#guard mulLow (karatsubaPlan 32) 8 #p[1, -4, 1]
(polyOfSeries tilings) = #p[1, -1]
The first argument of both calls, karatsubaPlan 32, says how to multiply:
by Karatsuba's method, switching to the schoolbook method for factors with
at most 32 coefficients. Hex.DensePoly.pade? runs the half-gcd algorithm, which
does its work in such products. Multiplication, the half-gcd algorithm and
Padé approximation each have a section below.
HexPolyFast does not depend on Mathlib, and has no theory companion of its
own: its theorems are stated in terms of HexPoly and
HexTruncatedSeries operations, which their
companions relate to Mathlib's polynomials and power series.
Proofs and Mathlib shows how to use them.