---

Step * 1 1 1 1 1 1 of Lemma third-derivative-log-contraction-bound


1. a : {a:ℝ| r0 < a} 
2. x : ℝ
3. ∀x:ℝ. (r0 < (a + e^x))
4. ∀x:ℝ. ∀n:ℕ+.  (r0 < a + e^x^n)
5. b : ℝ
6. e^x = b ∈ ℝ
7. (a + b^2 * a + b^2) = a + b^4
8. a^3 = (a^2 * a)
9. b^3 = (b^2 * b)
⊢ ((((a + b) * (a + b)) * (a + b) * (a + b)) + (r(8) * ((a * a) * a) * b) + (r(8) * ((b * b) * b) * a))
= ((((a * a) * a * a) + ((b * b) * b * b))
  + (r(12) * ((a * a) * a) * b)
  + (r(12) * ((b * b) * b) * a)
  + (r(6) * (a * a) * b * b))
BY
{ (nRNorm 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbR{}|  r0  <  a\} 
2.  x  :  \mBbbR{}
3.  \mforall{}x:\mBbbR{}.  (r0  <  (a  +  e\^{}x))
4.  \mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (r0  <  a  +  e\^{}x\^{}n)
5.  b  :  \mBbbR{}
6.  e\^{}x  =  b
7.  (a  +  b\^{}2  *  a  +  b\^{}2)  =  a  +  b\^{}4
8.  a\^{}3  =  (a\^{}2  *  a)
9.  b\^{}3  =  (b\^{}2  *  b)
\mvdash{}  ((((a  +  b)  *  (a  +  b))  *  (a  +  b)  *  (a  +  b))
+  (r(8)  *  ((a  *  a)  *  a)  *  b)
+  (r(8)  *  ((b  *  b)  *  b)  *  a))
=  ((((a  *  a)  *  a  *  a)  +  ((b  *  b)  *  b  *  b))
    +  (r(12)  *  ((a  *  a)  *  a)  *  b)
    +  (r(12)  *  ((b  *  b)  *  b)  *  a)
    +  (r(6)  *  (a  *  a)  *  b  *  b))


By

---

Latex:
(nRNorm  0  THEN  Auto)

---

Home Index