---

Step * of Lemma cosine-approx-for-small-ext

∀a:{2...}. ∀N:ℕ+. ∀x:{x:ℝ| |x| ≤ (r1/r(a))} .  (∃z:ℤ [(|cosine(x) - (r(z)/r(2 * N))| ≤ (r(2)/r(N)))])
BY
{ Extract of Obid: cosine-approx-for-small
  not unfolding  exp cosine-approx genfact-inv
  finishing with Auto
  normalizes to:
  
  λa,N,x. cosine-approx(x;eval aa = a * a in genfact-inv(N;2 * aa;k.aa * ((2 * k) + 2) * ((2 * k) + 1));N) }

---

Latex:

---

Latex:
\mforall{}a:\{2...\}.  \mforall{}N:\mBbbN{}\msupplus{}.  \mforall{}x:\{x:\mBbbR{}|  |x|  \mleq{}  (r1/r(a))\}  .    (\mexists{}z:\mBbbZ{}  [(|cosine(x)  -  (r(z)/r(2  *  N))|  \mleq{}  (r(2)/r(N)))]\000C)


By

---

Latex:
Extract  of  Obid:  cosine-approx-for-small
not  unfolding    exp  cosine-approx  genfact-inv
finishing  with  Auto
normalizes  to:

\mlambda{}a,N,x.  cosine-approx(x;eval  aa  =  a  *  a  in
                                                genfact-inv(N;2  *  aa;k.aa  *  ((2  *  k)  +  2)  *  ((2  *  k)  +  1));N)

---

Home Index