Exponential enclosures for interval_dyadic_real #

This file defines an inclusion operation for the interval_dyadic_real inclusion family that encloses Real.exp of an interval.

Implementation notes #

The exp of the endpoints is constructed by evaluating the Taylor partial sum up to the required precision level. The exponent is rewritten as exp x = exp (x / m) ^ m, where m is an integer chosen so that |x / m| < 1 / 32, so that the Taylor series converges faster.

This file is opt-in so that dyadic_interval doesn't import unnecessary theories.

TODO #

For larger exponents, we would eventually want to implement another optimisation that shifts the exp exponent by multiples of log 2 (which only shifts the exponent of the dyadic result). This is deferred since it requires a certified computation of log 2 to arbitrary precision, which is a separate from the main instance.

source

def Inclusion.IntervalDyadicReal.expPartialSumNum (a : ℤ) (b n : ℕ) :

ℤ

The numerator of the partial Taylor sum ∑ m ∈ range n, (a / b) ^ m / m! as an unreduced fraction over the common denominator b ^ n * n!.

Equations

Inclusion.IntervalDyadicReal.expPartialSumNum a b 0 = 0
Inclusion.IntervalDyadicReal.expPartialSumNum a b n_2.succ = (Inclusion.IntervalDyadicReal.expPartialSumNum a b n_2 + a ^ n_2) * ↑(b * (n_2 + 1))

Instances For

source

theorem Inclusion.IntervalDyadicReal.expPartialSumNum_div (a : ℤ) {b : ℕ} (hb : b ≠ 0) (n : ℕ) :

↑(expPartialSumNum a b n) / (↑b ^ n * ↑n.factorial) = ∑ m ∈ Finset.range n, (↑a / ↑b) ^ m / ↑m.factorial

source

def Inclusion.IntervalDyadicReal.expRatTaylor (a : ℤ) (b n prec : ℕ) :

Interval Dyadic

An enclosure of exp (a / b) by the first n terms of its Taylor series and the remainder bound of Real.exp_bound, rounded outward to precision prec. This is only intended for use when | a / b | ≤ 1.

Equations

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

Instances For

source

theorem Inclusion.IntervalDyadicReal.expRatTaylor_mem (a : ℤ) {b : ℕ} (hb : b ≠ 0) (hab : a.natAbs ≤ b) {n : ℕ} (hn : 0 < n) (prec : ℕ) :

Real.exp (↑a / ↑b) ∈ expRatTaylor a b n prec

source

def Inclusion.IntervalDyadicReal.expPoint (x : Dyadic) (prec : ℕ) :

Interval Dyadic

An enclosure of exp x by rewriting as exp (x / m) ^ m so that |x / m| < 1 / 32 to make the Taylor series converge quickly. The interval is rounded outward after the power to drop the redundant bits for the consumers.

Some relevant precision constants are chosen as follows:

m = 16 (⌊2 |x|⌋ + 1) to shrink the exponent below 1/32.
precTaylor is the precision of exp (x / m) requested. The power turns an absolute error δ on exp (x / m) into about m * exp x * δ on exp x, since its derivative is m * exp (x / m) ^ (m - 1). So precTaylor adds three amounts to prec.
- powerBits is at least ⌈ log₂ m ⌉.
- sizeBits = ⌊ 1.5x ⌋ + 1 (1.5 > log₂ e) which bounds the number of bits above 1 for exp x.
- a constant (8 here) so that the powered interval is narrower than the requested precision, to make it more likely that the resulting interval has width 2^{-prec}.
taylorTerms terms bring the Taylor remainder below 2 ^{-precTaylor}. Each term shrinks the remainder by at least 5 bits due to the 1/32 bound on the exponent, with further shrinking from the factorial. It's sufficient for the number of terms n to satisfy 5n + log₂ (n!) ≥ precTaylor + 1, and we take a very crude bound here using log₂(n!) ≥ n - 1.