Correctness of Payne-Hanek reduction

reduceWindow_spec proves that every window of at least two bits reduces m * 2 ^ e, for m > 0: x * 2/π = 4 j + quadrant + (fraction + η) / 2 ^ scale with 0 ≤ η < 2 m (QuarterTurns.Reduces). The proof splits the cached T ≤ 2/π * 2 ^ N < T + 2 into its bits above, inside and below the window: the bits above contribute a multiple of four, the window gives the fraction, and the bits below together with the error of T give η. The fraction has magnitude at most half a quarter turn (abs_fraction_reduceWindow_le).

An accepted reduction has the sign of the true remainder and relative error at most 2 ^ -bits (QuarterTurns.Reduces.exists_remainder). With r the reduced argument in radians, the sine and cosine of x are those of r rotated by the quadrant (QuarterTurns.Reduces.exists_sin_cos_eq_rotate). The computed argument q.argumentNumerator precision / 2 ^ (scale + precision) is within error / 2 ^ scale * π/2 + |fraction| / 2 ^ scale * 2 ^ (1 - precision) of r (QuarterTurns.abs_argument_sub_le), and its rotated sine and cosine are within the same bound of those of x (QuarterTurns.Reduces.abs_sin_sub_rotate_le and its cosine form).

reduce returns the reduction of one of its attempts (exists_reduce_eq_reduceWindow), so it reduces its argument too (reduce_spec), with error 2 m and a fraction of at most half a quarter turn. It returns an accepted reduction when some attempt within its fuel is accepted (accepts_reduce). fuelWithin? keeps every attempt within its level limit (fuelWithin?_spec) and gives no fuel exactly when the first window exceeds that limit (fuelWithin?_eq_none_iff).

def FloatLib.Numerics.Enclosure.ArgumentReduction.QuarterTurns.Reduces (q : QuarterTurns) (x : ℝ) : Prop

q reduces x: x * 2/π = 4 j + quadrant + (fraction + η) / 2 ^ scale for an integer j and some η with 0 ≤ η < error.

The window

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.le_levelBits_windowLevel (e : ℤ) (window : ℕ) : e + ↑window + 6 ≤ ↑(Constants.levelBits (windowLevel e window))

The level of a window holds at least e + window + 6 bits of 2/π.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.reduceWindow_spec {m : ℕ} (hm : 0 < m) (e : ℤ) {window : ℕ} (hwindow : 2 ≤ window) : (reduceWindow m e window).Reduces (↑m * 2 ^ e)

Every window of at least two bits reduces m * 2 ^ e, for m > 0.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.abs_fraction_reduceWindow_le (m : ℕ) (e : ℤ) {window : ℕ} (hwindow : 3 ≤ window) : |(reduceWindow m e window).fraction| ≤ 2 ^ (window - 3)

The fraction of a window of at least three bits is at most half a quarter turn.

Accepted reductions

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.QuarterTurns.accepts_spec {q : QuarterTurns} {bits : ℕ} (h : accepts bits q = true) {η : ℝ} (hη : 0 ≤ η) (hηlt : η < ↑q.error) : q.fraction ≠ 0 ∧ (0 < q.fraction ↔ 0 < ↑q.fraction + η) ∧ η * (2 ^ (bits + 1) - 1) ≤ |↑q.fraction + η|

An accepted reduction has a nonzero fraction that keeps its sign: for 0 ≤ η < error, fraction + η has the sign of fraction, and η * (2 ^ (bits + 1) - 1) ≤ |fraction + η|.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.QuarterTurns.Reduces.exists_remainder {q : QuarterTurns} {x : ℝ} (hq : q.Reduces x) {bits : ℕ} (h : accepts bits q = true) : ∃ (j : ℤ) (f : ℝ), x * (2 / Real.pi) = 4 * ↑j + ↑↑q.quadrant + f / 2 ^ q.scale ∧ |f - ↑q.fraction| ≤ |f| / 2 ^ bits ∧ (0 < q.fraction ↔ 0 < f) ∧ q.fraction ≠ 0

An accepted reduction gives the remainder f of x * 2/π, in units of 2 ^ -scale quarter turns, to a relative error of 2 ^ -bits and with its sign.

Quadrants

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.sin_cos_add_quarterTurns (r : ℝ) (j : ℤ) (quadrant : Fin 4) : (Real.sin (r + (4 * ↑j + ↑↑quadrant) * (Real.pi / 2)), Real.cos (r + (4 * ↑j + ↑↑quadrant) * (Real.pi / 2))) = rotate quadrant (Real.sin r) (Real.cos r)

The sine and cosine after whole quarter turns are the rotated sine and cosine.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.QuarterTurns.Reduces.exists_sin_cos_eq_rotate {q : QuarterTurns} {x : ℝ} (hq : q.Reduces x) : ∃ (η : ℝ), 0 ≤ η ∧ η < ↑q.error ∧ (Real.sin x, Real.cos x) = rotate q.quadrant (Real.sin ((↑q.fraction + η) / 2 ^ q.scale * (Real.pi / 2))) (Real.cos ((↑q.fraction + η) / 2 ^ q.scale * (Real.pi / 2)))

With r = (fraction + η) / 2 ^ scale * π/2 the reduced argument, the sine and cosine of x are those of r rotated by the quadrant.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.abs_rotate_fst_sub_le (quadrant : Fin 4) (a b : ℝ) : |(rotate quadrant (Real.sin a) (Real.cos a)).1 - (rotate quadrant (Real.sin b) (Real.cos b)).1| ≤ |a - b|

A quarter-turn rotation keeps the Lipschitz bound of sine.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.abs_rotate_snd_sub_le (quadrant : Fin 4) (a b : ℝ) : |(rotate quadrant (Real.sin a) (Real.cos a)).2 - (rotate quadrant (Real.sin b) (Real.cos b)).2| ≤ |a - b|

A quarter-turn rotation keeps the Lipschitz bound of cosine.

Error of the computed argument

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.QuarterTurns.abs_argument_sub_le (q : QuarterTurns) (precision : ℕ) {η : ℝ} (hη : 0 ≤ η) (hηlt : η < ↑q.error) : |(↑q.fraction + η) / 2 ^ q.scale * (Real.pi / 2) - ↑(q.argumentNumerator precision) / 2 ^ (q.scale + precision)| ≤ ↑q.error / 2 ^ q.scale * (Real.pi / 2) + |↑q.fraction| / 2 ^ q.scale * (2 / 2 ^ precision)

The computed argument q.argumentNumerator precision / 2 ^ (scale + precision) is within error / 2 ^ scale * π/2 + |fraction| / 2 ^ scale * 2 / 2 ^ precision of the reduced argument (fraction + η) / 2 ^ scale * π/2, for 0 ≤ η < error.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.QuarterTurns.Reduces.abs_sin_sub_rotate_le {q : QuarterTurns} {x : ℝ} (hq : q.Reduces x) (precision : ℕ) : |Real.sin x - (rotate q.quadrant (Real.sin (↑(q.argumentNumerator precision) / 2 ^ (q.scale + precision))) (Real.cos (↑(q.argumentNumerator precision) / 2 ^ (q.scale + precision)))).1| ≤ ↑q.error / 2 ^ q.scale * (Real.pi / 2) + |↑q.fraction| / 2 ^ q.scale * (2 / 2 ^ precision)

The sine of a reduced x is within error / 2 ^ scale * π/2 + |fraction| / 2 ^ scale * 2 / 2 ^ precision of the rotated sine of the computed argument q.argumentNumerator precision / 2 ^ (scale + precision).

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.QuarterTurns.Reduces.abs_cos_sub_rotate_le {q : QuarterTurns} {x : ℝ} (hq : q.Reduces x) (precision : ℕ) : |Real.cos x - (rotate q.quadrant (Real.sin (↑(q.argumentNumerator precision) / 2 ^ (q.scale + precision))) (Real.cos (↑(q.argumentNumerator precision) / 2 ^ (q.scale + precision)))).2| ≤ ↑q.error / 2 ^ q.scale * (Real.pi / 2) + |↑q.fraction| / 2 ^ q.scale * (2 / 2 ^ precision)

The cosine form of QuarterTurns.Reduces.abs_sin_sub_rotate_le.

Attempts

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.twenty_le_attemptWindow (p bits attempt : ℕ) : 20 ≤ attemptWindow p bits attempt

Every attempt window has at least twenty bits.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.attemptWindow_mono (p bits : ℕ) {attempt attempt' : ℕ} (h : attempt ≤ attempt') : attemptWindow p bits attempt ≤ attemptWindow p bits attempt'

Later attempts have wider windows.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.windowLevel_mono (e : ℤ) {window window' : ℕ} (h : window ≤ window') : windowLevel e window ≤ windowLevel e window'

Wider windows read the same or a higher level.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.exists_reduce_eq_reduceWindow (m : ℕ) (e : ℤ) (p bits fuel : ℕ) : ∃ attempt ≤ fuel, reduce m e p bits fuel = reduceWindow m e (attemptWindow p bits attempt)

reduce returns the reduction of one of its attempts.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.reduce_spec {m : ℕ} (hm : 0 < m) (e : ℤ) (p bits fuel : ℕ) : (reduce m e p bits fuel).Reduces (↑m * 2 ^ e)

reduce reduces m * 2 ^ e, whichever attempt it returns.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.error_reduce (m : ℕ) (e : ℤ) (p bits fuel : ℕ) : (reduce m e p bits fuel).error = 2 * m

The error of reduce is 2 m units.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.abs_fraction_reduce_le (m : ℕ) (e : ℤ) (p bits fuel : ℕ) : |(reduce m e p bits fuel).fraction| ≤ 2 ^ ((reduce m e p bits fuel).scale - 1)

The fraction of reduce is at most half a quarter turn.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.accepts_reduce {m : ℕ} {e : ℤ} {p bits fuel attempt : ℕ} (hattempt : attempt ≤ fuel) (h : QuarterTurns.accepts bits (reduceWindow m e (attemptWindow p bits attempt)) = true) : QuarterTurns.accepts bits (reduce m e p bits fuel) = true

reduce returns an accepted reduction when some attempt within the fuel is accepted.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.fuelWithin?_spec {e : ℤ} {p bits limit fuel count : ℕ} (h : fuelWithin? e p bits limit fuel = some count) : count ≤ fuel ∧ ∀ attempt ≤ count, windowLevel e (attemptWindow p bits attempt) ≤ limit

fuelWithin? keeps every attempt within the level limit: a result count is at most fuel, and every attempt up to it reads a level of at most limit.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.fuelWithin?_eq_none_iff {e : ℤ} {p bits limit fuel : ℕ} : fuelWithin? e p bits limit fuel = none ↔ limit < windowLevel e (attemptWindow p bits 0)

fuelWithin? gives no fuel exactly when the first window reads a level above limit.