---

Step * of Lemma arcsine-contraction-Taylor

∀[a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} ]. ∀[x:ℝ].
  ∀c:ℝ
    |arcsine-contraction(a;x) - arcsine(a)| ≤ (c * |x - arcsine(a)|^3) 
    supposing (r0 ≤ a) ∧ (a ≤ c) ∧ (rsqrt(r1 - a * a) ≤ c)
BY
{ ((Auto THEN DSetVars THEN (Unhide THENA Auto))
   THEN ((Assert r0 ≤ (r1 - a * a) BY
                (nRAdd  ⌜a * a⌝ 0⋅
                 THEN RWW  "rnexp2< square-rleq-1-iff rabs-rleq-iff" 0
                 THEN Auto
                 THEN RWO "rminus-int" 0
                 THEN Auto))
         THEN Auto
         )
   THEN BLemma  `rleq-iff-all-rless`
   THEN Auto
   THEN (Assert (-(π/2), π/2) ⊆ (-∞, ∞)  BY
               ((D 0 THEN Reduce 0) THEN Auto))
   THEN (Assert d(rcos(x))/dx = λx.-(rsin(x)) on (-∞, ∞) BY
               Auto)
   THEN (Assert d(rsin(x))/dx = λx.rcos(x) on (-∞, ∞) BY
               Auto)
   THEN (Assert d(-(rsin(x)))/dx = λx.-(rcos(x)) on (-∞, ∞) BY
               (ProveDerivative THEN Auto))
   THEN (Assert d(-(rcos(x)))/dx = λx.rsin(x) on (-∞, ∞) BY
               (ProveDerivative THEN Auto))) }

1
1. a : ℝ
2. r(-1) < a
3. a < r1
4. x : ℝ
5. c : ℝ
6. r0 ≤ a
7. a ≤ c
8. rsqrt(r1 - a * a) ≤ c
9. r0 ≤ (r1 - a * a)
10. e : {e:ℝ| r0 < e} 
11. (-(π/2), π/2) ⊆ (-∞, ∞) 
12. d(rcos(x))/dx = λx.-(rsin(x)) on (-∞, ∞)
13. d(rsin(x))/dx = λx.rcos(x) on (-∞, ∞)
14. d(-(rsin(x)))/dx = λx.-(rcos(x)) on (-∞, ∞)
15. d(-(rcos(x)))/dx = λx.rsin(x) on (-∞, ∞)
⊢ |arcsine-contraction(a;x) - arcsine(a)| ≤ ((c * |x - arcsine(a)|^3) + e)

---

Latex:

---

Latex:
\mforall{}[a:\{a:\mBbbR{}|  (r(-1)  <  a)  \mwedge{}  (a  <  r1)\}  ].  \mforall{}[x:\mBbbR{}].
    \mforall{}c:\mBbbR{}
        |arcsine-contraction(a;x)  -  arcsine(a)|  \mleq{}  (c  *  |x  -  arcsine(a)|\^{}3) 
        supposing  (r0  \mleq{}  a)  \mwedge{}  (a  \mleq{}  c)  \mwedge{}  (rsqrt(r1  -  a  *  a)  \mleq{}  c)


By

---

Latex:
((Auto  THEN  DSetVars  THEN  (Unhide  THENA  Auto))
  THEN  ((Assert  r0  \mleq{}  (r1  -  a  *  a)  BY
                            (nRAdd    \mkleeneopen{}a  *  a\mkleeneclose{}  0\mcdot{}
                              THEN  RWW    "rnexp2<  square-rleq-1-iff  rabs-rleq-iff"  0
                              THEN  Auto
                              THEN  RWO  "rminus-int"  0
                              THEN  Auto))
              THEN  Auto
              )
  THEN  BLemma    `rleq-iff-all-rless`
  THEN  Auto
  THEN  (Assert  (-(\mpi{}/2),  \mpi{}/2)  \msubseteq{}  (-\minfty{},  \minfty{})    BY
                          ((D  0  THEN  Reduce  0)  THEN  Auto))
  THEN  (Assert  d(rcos(x))/dx  =  \mlambda{}x.-(rsin(x))  on  (-\minfty{},  \minfty{})  BY
                          Auto)
  THEN  (Assert  d(rsin(x))/dx  =  \mlambda{}x.rcos(x)  on  (-\minfty{},  \minfty{})  BY
                          Auto)
  THEN  (Assert  d(-(rsin(x)))/dx  =  \mlambda{}x.-(rcos(x))  on  (-\minfty{},  \minfty{})  BY
                          (ProveDerivative  THEN  Auto))
  THEN  (Assert  d(-(rcos(x)))/dx  =  \mlambda{}x.rsin(x)  on  (-\minfty{},  \minfty{})  BY
                          (ProveDerivative  THEN  Auto)))

---

Home Index