Bounds for the cached constants

piLevel_halfPi_spec, piLevel_twoOverPi_spec and ln2Fixed_spec prove that the integers of Constants.Runtime are lower bounds within two units of π/2, 2/π and log 2 times 2 ^ bits, for every bits. The proofs read the integers as the endpoints of the proved enclosures piQuarter and logSeries 2 (piQuarterBounds_eq, ln2Bounds_eq), bound the enclosure widths, and check that the series degrees make those widths small at every precision.

Shifting such a bound to fewer bits keeps it within two units (LowerApprox.shiftRight), so every read at any precision inherits the bound. The faithful read of log 2 is within one unit and its grid read encloses it. The cache returns the uncached values (piLevelAt_eq, ln2FixedAt_eq).

def FloatLib.Numerics.Enclosure.Constants.LowerApprox (c : ℝ) (bits value : ℕ) : Prop

value is a lower bound within two units of c * 2 ^ bits.

The cache

theorem FloatLib.Numerics.Enclosure.Constants.piLevelAt_eq (level : ℕ) : piLevelAt level = piLevel (levelBits level)

A cached piLevel is the uncached one.

theorem FloatLib.Numerics.Enclosure.Constants.ln2FixedAt_eq (level : ℕ) : ln2FixedAt level = ln2Fixed (levelBits level)

A cached ln2Fixed is the uncached one.

theorem FloatLib.Numerics.Enclosure.Constants.le_levelBits_levelFor (bits : ℕ) : bits ≤ levelBits (levelFor bits)

The level of bits has at least bits fractional bits.

theorem FloatLib.Numerics.Enclosure.Constants.levelFor_mono {bits bits' : ℕ} (h : bits ≤ bits') : levelFor bits ≤ levelFor bits'

More bits need the same or a higher level.

Shifted and rounded reads

theorem FloatLib.Numerics.Enclosure.Constants.LowerApprox.shiftRight {c : ℝ} {precision value : ℕ} (h : LowerApprox c precision value) {bits : ℕ} (hbits : bits ≤ precision) : LowerApprox c bits (value >>> (precision - bits))

Shifting a lower bound within two units to fewer bits keeps it within two units.

theorem FloatLib.Numerics.Enclosure.Constants.LowerApprox.abs_round_sub_lt {c : ℝ} {bits value : ℕ} (h : LowerApprox c (bits + 64) value) : |↑((value + 1 + 2 ^ 63) >>> 64) - c * 2 ^ bits| < 1

A lower bound within two units at 64 more bits, raised by one unit and rounded to bits, is within one unit.

Machin's enclosure of π/4

theorem FloatLib.Numerics.Enclosure.atanTaylor_eq_split (x : ℚ) (n : ℕ) : atanTaylor x n = x * (↑(Taylor.split (Taylor.atanStep x) 0 n).constantTerm / ↑(Taylor.split (Taylor.atanStep x) 0 n).denominator)

Binary splitting writes an arctangent partial sum as x times one unreduced fraction.

theorem FloatLib.Numerics.Enclosure.piQuarter_eq (degree : ℕ) : piQuarter degree = { lo := 4 * (atanTaylor (1 / 5) (degree + 1) - 1 / (120 * 25 ^ degree)) - (atanTaylor (1 / 239) (degree + 1) + 1 / (13651680 * 57121 ^ degree)), hi := 4 * (atanTaylor (1 / 5) (degree + 1) + 1 / (120 * 25 ^ degree)) - (atanTaylor (1 / 239) (degree + 1) - 1 / (13651680 * 57121 ^ degree)) }

Machin's enclosure of π/4, with the radii of its two arctangent enclosures written out.

theorem FloatLib.Numerics.Enclosure.piQuarter_width_le (degree : ℕ) : (piQuarter degree).hi - (piQuarter degree).lo ≤ 1 / (12 * 25 ^ degree)

Machin's enclosure of π/4 has width at most 1 / (12 * 25 ^ degree).

theorem FloatLib.Numerics.Enclosure.piQuarter_bounds (degree : ℕ) : ↑(piQuarter degree).lo ≤ Real.pi / 4 ∧ Real.pi / 4 ≤ ↑(piQuarter degree).hi ∧ ↑(piQuarter degree).hi - ↑(piQuarter degree).lo ≤ 1 / (12 * 25 ^ degree)

Machin's enclosure contains π/4 and has width at most 1 / (12 * 25 ^ degree).

theorem FloatLib.Numerics.Enclosure.two_thirds_lt_piQuarter_lo (degree : ℕ) : 2 / 3 < (piQuarter degree).lo

The lower endpoint of Machin's enclosure exceeds two thirds.

theorem FloatLib.Numerics.Enclosure.piQuarter_lo_pos (degree : ℕ) : 0 < (piQuarter degree).lo

The lower endpoint of Machin's enclosure is positive.

theorem FloatLib.Numerics.Enclosure.Constants.piQuarterBounds_eq (degree : ℕ) : ↑(piQuarterBounds degree).lower / ↑(piQuarterBounds degree).denominator = (piQuarter degree).lo ∧ ↑(piQuarterBounds degree).upper / ↑(piQuarterBounds degree).denominator = (piQuarter degree).hi

piQuarterBounds degree denotes the endpoints of piQuarter degree.

π/2 and 2/π

theorem FloatLib.Numerics.Enclosure.Constants.LowerApprox.of_div {c lo hi : ℝ} {bits numerator denominator : ℕ} (hdenominator : 0 < denominator) (hvalue : ↑numerator / ↑denominator = lo * 2 ^ bits) (hlo : lo ≤ c) (hhi : c ≤ hi) (hwidth : (hi - lo) * 2 ^ bits ≤ 1) : LowerApprox c bits (numerator / denominator)

A floor quotient is a lower bound within two units of c * 2 ^ bits when the exact quotient is lo * 2 ^ bits for an enclosure [lo, hi] of c of width at most 2 ^ -bits.

theorem FloatLib.Numerics.Enclosure.Constants.piLevel_halfPi_spec (bits : ℕ) : LowerApprox (Real.pi / 2) bits (piLevel bits).halfPi

piLevel bits holds π / 2 * 2 ^ bits to within two units below.

theorem FloatLib.Numerics.Enclosure.Constants.piLevel_twoOverPi_spec (bits : ℕ) : LowerApprox (2 / Real.pi) bits (piLevel bits).twoOverPi

piLevel bits holds 2 / π * 2 ^ bits to within two units below.

log 2

theorem FloatLib.Numerics.Enclosure.logOneSubTaylor_eq_split (x : ℚ) (n : ℕ) : logOneSubTaylor x n = ↑(Taylor.split (Taylor.logStep x) 0 n).constantTerm / ↑(Taylor.split (Taylor.logStep x) 0 n).denominator

Binary splitting writes a partial sum of -log (1 - x) as one unreduced fraction.

theorem FloatLib.Numerics.Enclosure.logSeries_two_eq (degree : ℕ) : logSeries 2 degree = { lo := logOneSubTaylor (1 / 3) degree - logOneSubTaylor (-1 / 3) degree - 1 / 3 ^ degree, hi := logOneSubTaylor (1 / 3) degree - logOneSubTaylor (-1 / 3) degree + 1 / 3 ^ degree }

Endpoints of logSeries 2, with the radii of both series in 1/3 written out.

theorem FloatLib.Numerics.Enclosure.Constants.ln2Bounds_eq (degree : ℕ) : ↑(ln2Bounds degree).lower / ↑(ln2Bounds degree).denominator = (logSeries 2 degree).lo ∧ ↑(ln2Bounds degree).upper / ↑(ln2Bounds degree).denominator = (logSeries 2 degree).hi

ln2Bounds degree denotes the endpoints of logSeries 2 degree.

theorem FloatLib.Numerics.Enclosure.Constants.ln2Fixed_spec (bits : ℕ) : LowerApprox (Real.log 2) bits (ln2Fixed bits)

ln2Fixed bits is within two units below log 2 * 2 ^ bits.

Reads at any precision

theorem FloatLib.Numerics.Enclosure.Constants.halfPiLower_spec (bits : ℕ) : LowerApprox (Real.pi / 2) bits (halfPiLower bits)

halfPiLower bits is within two units below π / 2 * 2 ^ bits.

theorem FloatLib.Numerics.Enclosure.Constants.twoOverPiLower_spec (bits : ℕ) : LowerApprox (2 / Real.pi) bits (twoOverPiLower bits)

twoOverPiLower bits is within two units below 2 / π * 2 ^ bits.

theorem FloatLib.Numerics.Enclosure.Constants.ln2Lower_spec (bits : ℕ) : LowerApprox (Real.log 2) bits (ln2Lower bits)

ln2Lower bits is within two units below log 2 * 2 ^ bits.

theorem FloatLib.Numerics.Enclosure.Constants.abs_ln2Faithful_sub_lt_one (bits : ℕ) : |↑(ln2Faithful bits) - Real.log 2 * 2 ^ bits| < 1

ln2Faithful bits is within one unit of log 2 * 2 ^ bits.

theorem FloatLib.Numerics.Enclosure.Constants.containsReal_ln2Grid (precision : ℕ) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (ln2Grid precision) (Real.log 2)

The grid read of log 2 encloses log 2.