---

Step * 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 ∈ ℝ
⊢ (((r(32) * a^2) * b^2) + ((r(-8) * a^3) * b) + ((r(-8) * b^3) * a)) ≤ a + b^4
BY
{ nRAdd ⌜((r(8) * a^3) * b) + ((r(8) * b^3) * a)⌝ 0⋅ }

1
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 ∈ ℝ
⊢ (r(32) * a^2 * b^2) ≤ (a + b^4 + (r(8) * a^3 * b) + (r(8) * b^3 * a))

---

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
\mvdash{}  (((r(32)  *  a\^{}2)  *  b\^{}2)  +  ((r(-8)  *  a\^{}3)  *  b)  +  ((r(-8)  *  b\^{}3)  *  a))  \mleq{}  a  +  b\^{}4


By

---

Latex:
nRAdd  \mkleeneopen{}((r(8)  *  a\^{}3)  *  b)  +  ((r(8)  *  b\^{}3)  *  a)\mkleeneclose{}  0\mcdot{}

---

Home Index