Exact Taylor sums by binary splitting

Each Horner step is an affine map with integer coefficients and a positive common denominator. Composing adjacent blocks uses only integer arithmetic. Binary splitting balances the sizes of the multiplication operands, and rational normalization happens once, at the end.

The resulting exponential, logarithm and arctangent polynomials agree with their finite sums for every rational argument and every number of terms, without convergence assumptions.

structure FloatLib.Numerics.Enclosure.Taylor.Block : Type

The affine map tail ↦ (constantTerm + coefficient * tail) / denominator.

• constantTerm : ℤ

  Integer constant in the numerator.

• coefficient : ℤ

  Integer multiplier of the remaining polynomial tail.

• denominator : ℕ

  Common denominator of the affine expression.

• denominator_pos : 0 < self.denominator

  A positive denominator keeps every block evaluation defined.

def FloatLib.Numerics.Enclosure.Taylor.Block.eval (block : Block) (tail : ℚ) : ℚ

Apply a Horner block to the unevaluated tail of the polynomial.

def FloatLib.Numerics.Enclosure.Taylor.Block.identity : Block

An empty block leaves the tail unchanged.

def FloatLib.Numerics.Enclosure.Taylor.Block.comp (left right : Block) : Block

Compose consecutive Horner blocks without reducing either fraction.

theorem FloatLib.Numerics.Enclosure.Taylor.Block.eval_identity (tail : ℚ) : identity.eval tail = tail

Evaluating the identity block preserves the tail.

theorem FloatLib.Numerics.Enclosure.Taylor.Block.eval_comp (left right : Block) (tail : ℚ) : (left.comp right).eval tail = left.eval (right.eval tail)

Evaluating a composite block agrees with evaluating its two blocks in order.

def FloatLib.Numerics.Enclosure.Taylor.horner (term : ℕ → Block) (start : ℕ) : ℕ → ℚ → ℚ

Sequential Horner evaluation, used to specify the composition of a block.

theorem FloatLib.Numerics.Enclosure.Taylor.horner_add (term : ℕ → Block) (start m n : ℕ) (tail : ℚ) : horner term start (m + n) tail = horner term start m (horner term (start + m) n tail)

Horner evaluation over adjacent ranges is the composition of their evaluations.

@[irreducible, specialize #[]]

def FloatLib.Numerics.Enclosure.Taylor.split (term : ℕ → Block) (start length : ℕ) : Block

Compose a range of Horner steps by splitting it into halves.

theorem FloatLib.Numerics.Enclosure.Taylor.eval_split (term : ℕ → Block) (start length : ℕ) (tail : ℚ) : (split term start length).eval tail = horner term start length tail

Binary splitting gives the same affine map as sequential Horner evaluation.

def FloatLib.Numerics.Enclosure.Taylor.expStep (x : ℚ) (k : ℕ) : Block

The exponential Horner step tail ↦ 1 + x * tail / (k + 1).

theorem FloatLib.Numerics.Enclosure.Taylor.eval_expStep (x : ℚ) (k : ℕ) (tail : ℚ) : (expStep x k).eval tail = 1 + x / (↑k + 1) * tail

An exponential block evaluates to 1 + x / (k + 1) * tail.

theorem FloatLib.Numerics.Enclosure.Taylor.horner_expStep (x : ℚ) (start n : ℕ) : horner (expStep x) start n 0 = ∑ i ∈ Finset.range n, x ^ i / ↑((start + 1).ascFactorial i)

Exponential Horner steps expand into a sum with rising factorial denominators.

def FloatLib.Numerics.Enclosure.Taylor.logStep (x : ℚ) (k : ℕ) : Block

The logarithm Horner step tail ↦ x / (k + 1) + x * tail.

theorem FloatLib.Numerics.Enclosure.Taylor.eval_logStep (x : ℚ) (k : ℕ) (tail : ℚ) : (logStep x k).eval tail = x / (↑k + 1) + x * tail

A logarithm block evaluates to x / (k + 1) + x * tail.

theorem FloatLib.Numerics.Enclosure.Taylor.horner_logStep (x : ℚ) (start n : ℕ) : horner (logStep x) start n 0 = ∑ i ∈ Finset.range n, x ^ (i + 1) / ↑(start + i + 1)

Logarithm Horner steps expand into a sum with consecutive integer denominators.

def FloatLib.Numerics.Enclosure.Taylor.atanStep (x : ℚ) (k : ℕ) : Block

The arctangent Horner step tail ↦ 1 / (2k + 1) - x ^ 2 * tail.

theorem FloatLib.Numerics.Enclosure.Taylor.eval_atanStep (x : ℚ) (k : ℕ) (tail : ℚ) : (atanStep x k).eval tail = 1 / (2 * ↑k + 1) - x ^ 2 * tail

An arctangent block evaluates to 1 / (2k + 1) - x ^ 2 * tail.

theorem FloatLib.Numerics.Enclosure.Taylor.horner_atanStep (x : ℚ) (start n : ℕ) : horner (atanStep x) start n 0 = ∑ i ∈ Finset.range n, (-x ^ 2) ^ i / ↑(2 * (start + i) + 1)

Arctangent Horner steps expand into a sum of powers of -x ^ 2 over odd denominators.

def FloatLib.Numerics.Enclosure.Taylor.exp (x : ℚ) (n : ℕ) : ℚ

Sum of the first n exponential terms, with one final rational normalization.

def FloatLib.Numerics.Enclosure.Taylor.logOneSub (x : ℚ) (n : ℕ) : ℚ

Sum of the first n terms of -log (1 - x), with one final rational normalization.

def FloatLib.Numerics.Enclosure.Taylor.atan (x : ℚ) (n : ℕ) : ℚ

Sum of the first n arctangent terms, with one final rational normalization.

theorem FloatLib.Numerics.Enclosure.Taylor.exp_eq_sum (x : ℚ) (n : ℕ) : exp x n = ∑ i ∈ Finset.range n, x ^ i / ↑i.factorial

exp x n is the sum of the first n terms of the exponential series.

theorem FloatLib.Numerics.Enclosure.Taylor.logOneSub_eq_sum (x : ℚ) (n : ℕ) : logOneSub x n = ∑ i ∈ Finset.range n, x ^ (i + 1) / ↑(i + 1)

logOneSub x n is the sum of the first n terms of the series for -log (1 - x).

theorem FloatLib.Numerics.Enclosure.Taylor.atan_eq_sum (x : ℚ) (n : ℕ) : atan x n = ∑ i ∈ Finset.range n, (-1) ^ i * x ^ (2 * i + 1) / ↑(2 * i + 1)

atan x n is the sum of the first n terms of the arctangent series.