---

Step * of Lemma arcsine-contraction-difference

∀[a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} ]. ∀[x,y:ℝ].
  (|arcsine-contraction(a;x) - arcsine-contraction(a;y)| ≤ (r(3) * |x - y|))
BY
{ (Auto
   THEN D 1
   THEN Unhide
   THEN 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 (InstLemma `mean-value-for-bounded-derivative` [⌜(-∞, ∞)⌝;⌜λ2x.arcsine-contraction(a;x)⌝;⌜λ2x.r1
                                                                                                  + ((a * -(rsin(x))) 
                                                                                                    - rsqrt(r1 - a * a)
                                                                                                    * rcos(x))⌝]⋅
         THENA (Auto THEN Unfold `arcsine-contraction` 0 THEN ProveDerivative THEN Auto)
         )) }

1
1. a : ℝ
2. r(-1) < a
3. a < r1
4. x : ℝ
5. y : ℝ
6. r0 ≤ (r1 - a * a)
7. ∀c:ℝ
     ((∀x:{x:ℝ| x ∈ (-∞, ∞)} . (|r1 + ((a * -(rsin(x))) - rsqrt(r1 - a * a) * rcos(x))| ≤ c))
     ⇒ (∀x,y:{x:ℝ| x ∈ (-∞, ∞)} .  (|arcsine-contraction(a;x) - arcsine-contraction(a;y)| ≤ (c * |x - y|))))
⊢ |arcsine-contraction(a;x) - arcsine-contraction(a;y)| ≤ (r(3) * |x - y|)

---

Latex:

---

Latex:
\mforall{}[a:\{a:\mBbbR{}|  (r(-1)  <  a)  \mwedge{}  (a  <  r1)\}  ].  \mforall{}[x,y:\mBbbR{}].
    (|arcsine-contraction(a;x)  -  arcsine-contraction(a;y)|  \mleq{}  (r(3)  *  |x  -  y|))


By

---

Latex:
(Auto
  THEN  D  1
  THEN  Unhide
  THEN  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  (InstLemma  `mean-value-for-bounded-derivative`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.arcsine-contraction(a;x)\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}x.r1  +  ((a  *  -(rsin(x)))  -  rsqrt(r1  -  a  *  a)  *  rcos(x))\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Unfold  `arcsine-contraction`  0  THEN  ProveDerivative  THEN  Auto)
              ))

---

Home Index