---

Step * of Lemma approx-iter-arcsine_wf

∀[a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} ]. ∀[n:ℕ]. ∀[k:ℕ+].
  (approx-iter-arcsine(a;k;n) ∈ {y:ℤ| |arcsine-contraction^n(a) - (r(y))/2 * k| ≤ (r(2)/r(k))} )
BY
{ (InductionOnNat THEN Auto THEN RecUnfold `approx-iter-arcsine` 0 THEN Reduce 0) }

1
1. a : {a:ℝ| (r(-1) < a) ∧ (a < r1)} 
2. n : ℤ
3. k : ℕ+
⊢ a k ∈ {y:ℤ| |arcsine-contraction^0(a) - (r(y))/2 * k| ≤ (r(2)/r(k))} 

2
1. a : {a:ℝ| (r(-1) < a) ∧ (a < r1)} 
2. n : ℤ
3. 0 < n
4. ∀[k:ℕ+]. (approx-iter-arcsine(a;k;n - 1) ∈ {y:ℤ| |arcsine-contraction^n - 1(a) - (r(y))/2 * k| ≤ (r(2)/r(k))} )
5. k : ℕ+
⊢ if (n =z 0)
  then a k
  else eval m = n - 1 in
       eval k6 = 6 * k in
       eval k12 = 2 * k6 in
       eval y = approx-iter-arcsine(a;k6;m) in
         arcsine-contraction(a;(r(y))/k12) k
  fi  ∈ {y:ℤ| |arcsine-contraction^n(a) - (r(y))/2 * k| ≤ (r(2)/r(k))} 

---

Latex:

---

Latex:
\mforall{}[a:\{a:\mBbbR{}|  (r(-1)  <  a)  \mwedge{}  (a  <  r1)\}  ].  \mforall{}[n:\mBbbN{}].  \mforall{}[k:\mBbbN{}\msupplus{}].
    (approx-iter-arcsine(a;k;n)  \mmember{}  \{y:\mBbbZ{}|  |arcsine-contraction\^{}n(a)  -  (r(y))/2  *  k|  \mleq{}  (r(2)/r(k))\}  )


By

---

Latex:
(InductionOnNat  THEN  Auto  THEN  RecUnfold  `approx-iter-arcsine`  0  THEN  Reduce  0)

---

Home Index