---

Step * 1 1 of Lemma log-contraction-Taylor


1. a : ℝ
2. x : ℝ
3. r0 < a
4. |x - rlog(a)| ≤ r1
5. ∀x:ℝ. (r0 < (a + e^x))
6. ∀x:ℝ. ∀n:ℕ+.  (r0 < a + e^x^n)
7. e : {e:ℝ| r0 < e} 
8. k : ℕ4
9. x1 : {a:ℝ| True} 
10. y : {a:ℝ| True} 
11. x1 = y
⊢ if (k =z 0) then log-contraction(a;x1)
if (k =z 1) then (a - e^x1/a + e^x1)^2
if (k =z 2) then (((r(-4) * a) * e^x1) * (a - e^x1)/a + e^x1^3)
else (((r(16) * a^2) * e^x1^2) + ((r(-4) * a^3) * e^x1) + ((r(-4) * a) * e^x1^3)/a + e^x1^4)
fi 
= if (k =z 0) then log-contraction(a;y)
  if (k =z 1) then (a - e^y/a + e^y)^2
  if (k =z 2) then (((r(-4) * a) * e^y) * (a - e^y)/a + e^y^3)
  else (((r(16) * a^2) * e^y^2) + ((r(-4) * a^3) * e^y) + ((r(-4) * a) * e^y^3)/a + e^y^4)
  fi 
BY
{ (IntSegCases (-4) THEN Reduce 0 THEN Auto THEN Try ((RWO  "-2" 0 THEN Auto))) }

1
1. a : ℝ
2. x : ℝ
3. r0 < a
4. |x - rlog(a)| ≤ r1
5. ∀x:ℝ. (r0 < (a + e^x))
6. ∀x:ℝ. ∀n:ℕ+.  (r0 < a + e^x^n)
7. e : {e:ℝ| r0 < e} 
8. k : ℤ
9. x1 : {a:ℝ| True} 
10. y : {a:ℝ| True} 
11. x1 = y
12. k = 0 ∈ ℤ
⊢ log-contraction(a;x1) = log-contraction(a;y)

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  x  :  \mBbbR{}
3.  r0  <  a
4.  |x  -  rlog(a)|  \mleq{}  r1
5.  \mforall{}x:\mBbbR{}.  (r0  <  (a  +  e\^{}x))
6.  \mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (r0  <  a  +  e\^{}x\^{}n)
7.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
8.  k  :  \mBbbN{}4
9.  x1  :  \{a:\mBbbR{}|  True\} 
10.  y  :  \{a:\mBbbR{}|  True\} 
11.  x1  =  y
\mvdash{}  if  (k  =\msubz{}  0)  then  log-contraction(a;x1)
if  (k  =\msubz{}  1)  then  (a  -  e\^{}x1/a  +  e\^{}x1)\^{}2
if  (k  =\msubz{}  2)  then  (((r(-4)  *  a)  *  e\^{}x1)  *  (a  -  e\^{}x1)/a  +  e\^{}x1\^{}3)
else  (((r(16)  *  a\^{}2)  *  e\^{}x1\^{}2)  +  ((r(-4)  *  a\^{}3)  *  e\^{}x1)  +  ((r(-4)  *  a)  *  e\^{}x1\^{}3)/a  +  e\^{}x1\^{}4)
fi 
=  if  (k  =\msubz{}  0)  then  log-contraction(a;y)
    if  (k  =\msubz{}  1)  then  (a  -  e\^{}y/a  +  e\^{}y)\^{}2
    if  (k  =\msubz{}  2)  then  (((r(-4)  *  a)  *  e\^{}y)  *  (a  -  e\^{}y)/a  +  e\^{}y\^{}3)
    else  (((r(16)  *  a\^{}2)  *  e\^{}y\^{}2)  +  ((r(-4)  *  a\^{}3)  *  e\^{}y)  +  ((r(-4)  *  a)  *  e\^{}y\^{}3)/a  +  e\^{}y\^{}4)
    fi 


By

---

Latex:
(IntSegCases  (-4)  THEN  Reduce  0  THEN  Auto  THEN  Try  ((RWO    "-2"  0  THEN  Auto)))

---

Home Index