---

Step * of Lemma iter-arcsine-contraction-property2

∀a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} . ∀n:ℕ.  (|arcsine-contraction^n(a) - arcsine(a)| ≤ |a - arcsine(a)|^3^n)
BY
{ (Intro
   THEN (Assert r0 ≤ (r1 - a * a) BY
               ((D 1 THEN (Unhide THENA Auto))
                THEN 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 NatInd (-1)) }

1
.....basecase..... 
1. a : {a:ℝ| (r(-1) < a) ∧ (a < r1)} 
2. r0 ≤ (r1 - a * a)
3. n : ℤ
⊢ |arcsine-contraction^0(a) - arcsine(a)| ≤ |a - arcsine(a)|^3^0

2
.....upcase..... 
1. a : {a:ℝ| (r(-1) < a) ∧ (a < r1)} 
2. r0 ≤ (r1 - a * a)
3. n : ℤ
4. 0 < n
5. |arcsine-contraction^n - 1(a) - arcsine(a)| ≤ |a - arcsine(a)|^3^(n - 1)
⊢ |arcsine-contraction^n(a) - arcsine(a)| ≤ |a - arcsine(a)|^3^n

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbR{}|  (r(-1)  <  a)  \mwedge{}  (a  <  r1)\}  .  \mforall{}n:\mBbbN{}.
    (|arcsine-contraction\^{}n(a)  -  arcsine(a)|  \mleq{}  |a  -  arcsine(a)|\^{}3\^{}n)


By

---

Latex:
(Intro
  THEN  (Assert  r0  \mleq{}  (r1  -  a  *  a)  BY
                          ((D  1  THEN  (Unhide  THENA  Auto))
                            THEN  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  NatInd  (-1))

---

Home Index