---

Step * of Lemma derivative-log-contraction-bound

∀a:{a:ℝ| r0 < a} . ∀[x:ℝ]. (|(a - e^x/a + e^x)^2| ≤ r1)
BY
{ ((D 0 THENA Auto)
   THEN (Assert ∀x:ℝ. (r0 < (a + e^x)) BY
               (Auto THEN (RWO "rexp-positive<" 0 THENM nRNorm 0) THEN Auto))
   THEN Auto) }

1
1. a : {a:ℝ| r0 < a} 
2. ∀x:ℝ. (r0 < (a + e^x))
3. x : ℝ
⊢ |(a - e^x/a + e^x)^2| ≤ r1

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbR{}|  r0  <  a\}  .  \mforall{}[x:\mBbbR{}].  (|(a  -  e\^{}x/a  +  e\^{}x)\^{}2|  \mleq{}  r1)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  \mforall{}x:\mBbbR{}.  (r0  <  (a  +  e\^{}x))  BY
                          (Auto  THEN  (RWO  "rexp-positive<"  0  THENM  nRNorm  0)  THEN  Auto))
  THEN  Auto)

---

Home Index