---

Step * 1 of Lemma arcsine-contraction-Taylor


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)
BY
{ (InstLemma `Taylor-theorem`
    [⌜(-∞, ∞)⌝;⌜2⌝;⌜λ2i x.if (i =z 0) then arcsine-contraction(a;x)
                    if (i =z 1) then r1 + ((a * -(rsin(x))) - rsqrt(r1 - a * a) * rcos(x))
                    if (i =z 2) then r0 + ((a * -(rcos(x))) - rsqrt(r1 - a * a) * -(rsin(x)))
                    else r0 + ((a * -(-(rsin(x)))) - rsqrt(r1 - a * a) * -(rcos(x)))
                    fi ⌝;⌜arcsine(a)⌝;⌜x⌝;⌜e⌝]⋅
   THENA (Reduce 0 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 (-∞, ∞)
16. k : ℕ4
17. x1 : {a:ℝ| True} 
18. y : {a:ℝ| True} 
19. x1 = y
⊢ if (k =z 0) then arcsine-contraction(a;x1)
if (k =z 1) then r1 + ((a * -(rsin(x1))) - rsqrt(r1 - a * a) * rcos(x1))
if (k =z 2) then r0 + ((a * -(rcos(x1))) - rsqrt(r1 - a * a) * -(rsin(x1)))
else r0 + ((a * -(-(rsin(x1)))) - rsqrt(r1 - a * a) * -(rcos(x1)))
fi 
= if (k =z 0) then arcsine-contraction(a;y)
  if (k =z 1) then r1 + ((a * -(rsin(y))) - rsqrt(r1 - a * a) * rcos(y))
  if (k =z 2) then r0 + ((a * -(rcos(y))) - rsqrt(r1 - a * a) * -(rsin(y)))
  else r0 + ((a * -(-(rsin(y)))) - rsqrt(r1 - a * a) * -(rcos(y)))
  fi 

2
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 (-∞, ∞)
⊢ finite-deriv-seq((-∞, ∞);3;i,x.if (i =z 0) then arcsine-contraction(a;x)
if (i =z 1) then r1 + ((a * -(rsin(x))) - rsqrt(r1 - a * a) * rcos(x))
if (i =z 2) then r0 + ((a * -(rcos(x))) - rsqrt(r1 - a * a) * -(rsin(x)))
else r0 + ((a * -(-(rsin(x)))) - rsqrt(r1 - a * a) * -(rcos(x)))
fi )

3
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 (-∞, ∞)
16. ∃c:ℝ
     ((rmin(arcsine(a);x) ≤ c)
     ∧ (c ≤ rmax(arcsine(a);x))
     ∧ (|Taylor-remainder((-∞, ∞);2;x;arcsine(a);k,x.if (k =z 0) then arcsine-contraction(a;x)
       if (k =z 1) then r1 + ((a * -(rsin(x))) - rsqrt(r1 - a * a) * rcos(x))
       if (k =z 2) then r0 + ((a * -(rcos(x))) - rsqrt(r1 - a * a) * -(rsin(x)))
       else r0 + ((a * -(-(rsin(x)))) - rsqrt(r1 - a * a) * -(rcos(x)))
       fi ) - (x - c^2
       * (if (2 + 1 =z 0) then arcsine-contraction(a;c)
         if (2 + 1 =z 1) then r1 + ((a * -(rsin(c))) - rsqrt(r1 - a * a) * rcos(c))
         if (2 + 1 =z 2) then r0 + ((a * -(rcos(c))) - rsqrt(r1 - a * a) * -(rsin(c)))
         else r0 + ((a * -(-(rsin(c)))) - rsqrt(r1 - a * a) * -(rcos(c)))
         fi /r((2)!)))
       * (x - arcsine(a))| ≤ e))
⊢ |arcsine-contraction(a;x) - arcsine(a)| ≤ ((c * |x - arcsine(a)|^3) + e)

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  r(-1)  <  a
3.  a  <  r1
4.  x  :  \mBbbR{}
5.  c  :  \mBbbR{}
6.  r0  \mleq{}  a
7.  a  \mleq{}  c
8.  rsqrt(r1  -  a  *  a)  \mleq{}  c
9.  r0  \mleq{}  (r1  -  a  *  a)
10.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
11.  (-(\mpi{}/2),  \mpi{}/2)  \msubseteq{}  (-\minfty{},  \minfty{}) 
12.  d(rcos(x))/dx  =  \mlambda{}x.-(rsin(x))  on  (-\minfty{},  \minfty{})
13.  d(rsin(x))/dx  =  \mlambda{}x.rcos(x)  on  (-\minfty{},  \minfty{})
14.  d(-(rsin(x)))/dx  =  \mlambda{}x.-(rcos(x))  on  (-\minfty{},  \minfty{})
15.  d(-(rcos(x)))/dx  =  \mlambda{}x.rsin(x)  on  (-\minfty{},  \minfty{})
\mvdash{}  |arcsine-contraction(a;x)  -  arcsine(a)|  \mleq{}  ((c  *  |x  -  arcsine(a)|\^{}3)  +  e)


By

---

Latex:
(InstLemma  `Taylor-theorem`
    [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i  x.if  (i  =\msubz{}  0)  then  arcsine-contraction(a;x)
                                    if  (i  =\msubz{}  1)  then  r1  +  ((a  *  -(rsin(x)))  -  rsqrt(r1  -  a  *  a)  *  rcos(x))
                                    if  (i  =\msubz{}  2)  then  r0  +  ((a  *  -(rcos(x)))  -  rsqrt(r1  -  a  *  a)  *  -(rsin(x)))
                                    else  r0  +  ((a  *  -(-(rsin(x))))  -  rsqrt(r1  -  a  *  a)  *  -(rcos(x)))
                                    fi  \mkleeneclose{};\mkleeneopen{}arcsine(a)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
  THENA  (Reduce  0  THEN  Auto)
  )

---

Home Index