---

Step * of Lemma log-contraction-Taylor

∀[a,x:ℝ].  |log-contraction(a;x) - rlog(a)| ≤ ((r1/r(4)) * |x - rlog(a)|^3) supposing (r0 < a) ∧ (|x - rlog(a)| ≤ r1)
BY
{ (Auto
   THEN (Assert ∀x:ℝ. (r0 < (a + e^x)) BY
               (Auto THEN (RWW "rexp-positive<" 0 THENM nRNorm 0) THEN Auto))
   THEN (Assert ∀x:ℝ. ∀n:ℕ+.  (r0 < a + e^x^n) BY
               (Auto THEN BLemma `rnexp-positive` 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)
⊢ |log-contraction(a;x) - rlog(a)| ≤ ((r1/r(4)) * |x - rlog(a)|^3)

---

Latex:

---

Latex:
\mforall{}[a,x:\mBbbR{}].
    |log-contraction(a;x)  -  rlog(a)|  \mleq{}  ((r1/r(4))  *  |x  -  rlog(a)|\^{}3) 
    supposing  (r0  <  a)  \mwedge{}  (|x  -  rlog(a)|  \mleq{}  r1)


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}x:\mBbbR{}.  (r0  <  (a  +  e\^{}x))  BY
                          (Auto  THEN  (RWW  "rexp-positive<"  0  THENM  nRNorm  0)  THEN  Auto))
  THEN  (Assert  \mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (r0  <  a  +  e\^{}x\^{}n)  BY
                          (Auto  THEN  BLemma  `rnexp-positive`  THEN  Auto)))

---

Home Index