Documentation

Cayley.Soundness.TrigTable

The checker's trigonometric tables #

cos(2πk/15) and sin(2πk/15) are within 2⁻⁷¹ of cosTab and sinTab: the case k = 1 comes from Cayley.Soundness.Trig, and the multiples follow by complex multiplication with the error tracked step by step.

source
def Cayley.cosM :
ℕ → ℤ
Equations
Instances For
    source
    def Cayley.sinM :
    ℕ → ℤ
    Equations
    Instances For
      source
      theorem Cayley.cosTab_eq (k : ℕ) (hk : k < 15) :
      cosTab[k]! = d80 (cosM k)
      source
      theorem Cayley.sinTab_eq (k : ℕ) (hk : k < 15) :
      sinTab[k]! = d80 (sinM k)
      source
      noncomputable def Cayley.zc (k : ℕ) :
      ℂ

      The exact point e^(ikθ₁).

      Equations
      Instances For
        source
        noncomputable def Cayley.zt (k : ℕ) :
        ℂ

        The table point.

        Equations
        Instances For
          source
          theorem Cayley.zc_succ (k : ℕ) :
          zc (k + 1) = zc k * zc 1
          source
          theorem Cayley.norm_zc (k : ℕ) :
          ‖zc k‖ = 1
          source
          theorem Cayley.norm_le_re_im (z : ℂ) :
          ‖z‖ ≤ |z.re| + |z.im|
          source
          theorem Cayley.zc_one_err :
          ‖zc 1 - zt 1‖ ≤ 1 / 2 ^ 79
          source
          theorem Cayley.step_err (k : ℕ) (E : ℝ) (hk : ‖zc k - zt k‖ ≤ E) :
          ‖zc (k + 1) - zt (k + 1)‖ ≤ E + (|(zt k).re| + |(zt k).im|) * (1 / 2 ^ 79) + (|(zt k * zt 1 - zt (k + 1)).re| + |(zt k * zt 1 - zt (k + 1)).im|)

          The computable step error of the recurrence.

          source
          theorem Cayley.step_small (k : ℕ) (hk : k < 14) :
          (|(zt k).re| + |(zt k).im|) * (1 / 2 ^ 79) + (|(zt k * zt 1 - zt (k + 1)).re| + |(zt k * zt 1 - zt (k + 1)).im|) ≤ 1 / 2 ^ 75

          The numerical side condition of each step.

          source
          theorem Cayley.trig_err (k : ℕ) (hk : k < 15) :
          ‖zc k - zt k‖ ≤ ↑k / 2 ^ 75
          source
          theorem Cayley.cos_tab_err (k : ℕ) (hk : k < 15) :
          |Real.cos (2 * Real.pi * ↑k / 15) - D cosTab[k]!| ≤ 1 / 2 ^ 71
          source
          theorem Cayley.sin_tab_err (k : ℕ) (hk : k < 15) :
          |Real.sin (2 * Real.pi * ↑k / 15) - D sinTab[k]!| ≤ 1 / 2 ^ 71