---

Step * of Lemma near-arcsine-exists-ext

∀a:{a:ℝ| a ∈ (r(-1), r1)} . ∀N:ℕ+.  (∃y:ℝ [(|y - arcsine(a)| ≤ (r1/r(N)))])
BY
{ Extract of Obid: near-arcsine-exists
  not unfolding  arcsine-approx rational-approx halfpi rsqrt rmul radd rdiv rminus rsub int-rdiv int-to-real
  finishing with (Reduce 0
                  THEN (Subst' (r(73))/100 400 ~ 584 0 THENA Computation)
                  THEN (Subst' r0 4000 ~ 0 0 THENA Computation)
                  THEN Reduce 0
                  THEN Auto)
  normalizes to:
  
  λa,N. eval b = a 4000 in
        if (4) < (b)
           then eval b = a 400 in
                if (588) < (b)
                   then (π/2 within 1/2 * N) - arcsine-approx(rsqrt(r1 - a * a);2 * N)
                   else if (b + 4) < (584)  then arcsine-approx(a;N)  else arcsine-approx(a;N)
           else if (b + 4) < (0)
                   then -(eval b = -(a) 400 in
                          if (588) < (b)
                             then (π/2 within 1/2 * N) - arcsine-approx(rsqrt(r1 - -(a) * -(a));2 * N)
                             else if (b + 4) < (584)  then arcsine-approx(-(a);N)  else arcsine-approx(-(a);N))
                   else eval m = 4 * (N + 1) in
                        eval a@0 = r0 m in
                        eval b = a m in
                          if (a@0 + 4) < (b)
                             then eval b = a 400 in
                                  if (588) < (b)
                                     then (π/2 within 1/2 * N) - arcsine-approx(rsqrt(r1 - a * a);2 * N)
                                     else if (b + 4) < (584)  then arcsine-approx(a;N)  else arcsine-approx(a;N)
                             else if (b + 4) < (a@0)
                                     then -(eval b = -(a) 400 in
                                            if (588) < (b)
                                               then (π/2 within 1/2 * N) - arcsine-approx(rsqrt(r1 - -(a) * -(a));2 * N)
                                               else if (b + 4) < (584)
                                                       then arcsine-approx(-(a);N)
                                                       else arcsine-approx(-(a);N))
                                     else r0 }

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbR{}|  a  \mmember{}  (r(-1),  r1)\}  .  \mforall{}N:\mBbbN{}\msupplus{}.    (\mexists{}y:\mBbbR{}  [(|y  -  arcsine(a)|  \mleq{}  (r1/r(N)))])


By

---

Latex:
...

---

Home Index