Cached constants: π/2, 2/π and log 2 at any precision

piLevel bits holds π/2 and 2/π, and ln2Fixed bits holds log 2, each as a natural number T with T ≤ c * 2 ^ bits < T + 2. Binary splitting sums Machin's formula π/4 = 4 atan (1/5) - atan (1/239) and the series of log 2 = log (4/3) - log (2/3) into unreduced integer fractions, so each constant costs one integer division and no rational normalization. The fractions are the lower and upper endpoints of piQuarter (piDegree bits) and logSeries 2 (ln2Degree bits), the rational enclosures of Trigonometric.Runtime and Elementary.Runtime, and Constants.Proof proves the two-unit bounds at every precision.

Level k holds the constants at 64 * 2 ^ k fractional bits. The first forty levels are cached. Each is computed at most once per process, on first use, and then shared. Higher levels are computed on each call. A read at bits shifts the first level with at least bits bits down to bits, which keeps the two-unit bound. The faithful read of log 2 takes 64 more bits and is within one unit, and the grid read returns an enclosure on a binary grid.

The cache is read by the binary sine and cosine reduction, the exponential reduction, generated transcendental configurations, the certified binary power and Model.pi. Two computations do not read it. The rational enclosures behind the exact comparators compute their own π/4 with piQuarter, and BinaryGrid.log, behind the certified binary and decimal logarithms and the logarithm comparator ElementaryComparison.compareLog, computes its own log 2.

Module initialization only allocates the cells. The cache definitions disable closed-term extraction, and every read goes through Internal.forceCache, which is never inlined or extracted.

@[never_extract, noinline]

def FloatLib.Numerics.Internal.forceCache {α : Type} (cache : Thunk α) : α

Read a cached value. The read is kept out of line and out of closed-term extraction, so it stays a first-use computation whatever the caller's compiler settings.

π/2 and 2/π

def FloatLib.Numerics.Enclosure.Constants.piDegree (bits : ℕ) : ℕ

The Machin series degree for bits fractional bits. Each term of atan (1/5) gains log₂ 25 bits, so a quarter of bits terms and four more leave a truncation error far below 2 ^ -bits.

structure FloatLib.Numerics.Enclosure.Constants.FractionBounds : Type

Endpoints of a rational enclosure, as unreduced fractions over one positive denominator.

• lower : ℤ

  Numerator of the lower endpoint.

• upper : ℤ

  Numerator of the upper endpoint.

• denominator : ℕ

  Common denominator of both endpoints.

• denominator_pos : 0 < self.denominator

  A positive denominator keeps both endpoints defined.

@[instance_reducible]

instance FloatLib.Numerics.Enclosure.Constants.instReprFractionBounds : Repr FractionBounds

def FloatLib.Numerics.Enclosure.Constants.instReprFractionBounds.repr : FractionBounds → ℕ → Std.Format

def FloatLib.Numerics.Enclosure.Constants.piQuarterBounds (degree : ℕ) : FractionBounds

The endpoints of piQuarter degree, from the integers of binary splitting.

With the first degree + 1 arctangent terms written as c / (5 b) for 1/5 and c' / (239 b') for 1/239, and the radii 1 / (120 * 25 ^ degree) and 1 / (13651680 * 57121 ^ degree) of atanRadius, the endpoints are 4 (c / (5 b) ∓ r) - (c' / (239 b') ± r').

structure FloatLib.Numerics.Enclosure.Constants.PiLevel : Type

2/π and π/2 at one precision, as lower bounds in units of 2 ^ -bits.

• twoOverPi : ℕ

  A lower bound within two units of 2 / π * 2 ^ bits.

• halfPi : ℕ

  A lower bound within two units of π / 2 * 2 ^ bits.

def FloatLib.Numerics.Enclosure.Constants.instReprPiLevel.repr : PiLevel → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.Enclosure.Constants.instReprPiLevel : Repr PiLevel

def FloatLib.Numerics.Enclosure.Constants.instDecidableEqPiLevel.decEq (x✝ x✝¹ : PiLevel) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.Enclosure.Constants.instDecidableEqPiLevel : DecidableEq PiLevel

def FloatLib.Numerics.Enclosure.Constants.piLevel (bits : ℕ) : PiLevel

2/π and π/2 at bits fractional bits from one Machin enclosure [lo, hi] of π/4: the floors of 2 ^ bits / (2 hi) and of 2 ^ (bits + 1) * lo, each one integer division.

log 2

def FloatLib.Numerics.Enclosure.Constants.ln2Degree (bits : ℕ) : ℕ

The degree of logSeries 2 for bits fractional bits. The series runs in 1/3, and its width 2 / 3 ^ degree is far below 2 ^ -bits at two thirds of bits terms and eight more.

def FloatLib.Numerics.Enclosure.Constants.ln2Bounds (degree : ℕ) : FractionBounds

The endpoints c / b - c' / b' ∓ 1 / 3 ^ degree of logSeries 2 degree, where c / b and c' / b' are the series of -log (2/3) and -log (4/3) from binary splitting.

def FloatLib.Numerics.Enclosure.Constants.ln2Fixed (bits : ℕ) : ℕ

A lower bound within two units of log 2 * 2 ^ bits: the floor of 2 ^ bits times the lower endpoint of logSeries 2 (ln2Degree bits), one integer division.

The cache

def FloatLib.Numerics.Enclosure.Constants.Internal.cacheLevels : ℕ

Number of cached levels.

def FloatLib.Numerics.Enclosure.Constants.levelBits (level : ℕ) : ℕ

Fractional bits of level level: 64 at level zero, doubling at each level.

def FloatLib.Numerics.Enclosure.Constants.levelFor (bits : ℕ) : ℕ

First cache level with at least bits fractional bits.

def FloatLib.Numerics.Enclosure.Constants.Internal.piCache : Array (Thunk PiLevel)

piLevel at every cached level, each computed on first use and then shared.

def FloatLib.Numerics.Enclosure.Constants.Internal.ln2Cache : Array (Thunk ℕ)

ln2Fixed at every cached level, each computed on first use and then shared.

def FloatLib.Numerics.Enclosure.Constants.piLevelAt (level : ℕ) : PiLevel

piLevel at a level: cached below Internal.cacheLevels, computed on each call above.

def FloatLib.Numerics.Enclosure.Constants.ln2FixedAt (level : ℕ) : ℕ

ln2Fixed at a level: cached below Internal.cacheLevels, computed on each call above.

Reads at any precision

def FloatLib.Numerics.Enclosure.Constants.halfPiLower (bits : ℕ) : ℕ

A lower bound within two units of π / 2 * 2 ^ bits, shifted down from its level.

def FloatLib.Numerics.Enclosure.Constants.twoOverPiLower (bits : ℕ) : ℕ

A lower bound within two units of 2 / π * 2 ^ bits, shifted down from its level.

def FloatLib.Numerics.Enclosure.Constants.ln2Lower (bits : ℕ) : ℕ

A lower bound within two units of log 2 * 2 ^ bits, shifted down from its level.

def FloatLib.Numerics.Enclosure.Constants.ln2Faithful (bits : ℕ) : ℕ

log 2 * 2 ^ bits within one unit, rounded from a lower bound with 64 more bits. It is the nearest integer unless the constant lies within 2 ^ -63 of a rounding midpoint.

def FloatLib.Numerics.Enclosure.Constants.ln2Grid (precision : ℕ) : Interval ℤ

An enclosure of log 2 on the grid of precision fractional bits, from a lower bound with 64 more bits. It usually spans one grid unit.