---

Step * of Lemma rabs-rlog-difference-bound

∀x,y:ℝ.  ((r0 < x) ⇒ (r0 < y) ⇒ (|rlog(y) - rlog(x)| ≤ (|y - x|/rmin(x;y))))
BY
{ ((Auto THEN (Assert r0 < rmin(x;y) BY EAuto 1))
   THEN (InstLemma `mean-value-for-bounded-derivative` 
         [⌜[rmin(x;y), ∞)⌝;⌜λ2x.rlog(x)⌝;⌜λ2x.(r1/x)⌝;⌜(r1/rmin(x;y))⌝]⋅
         THENA Try (Complete ((Auto THEN RepUR ``iproper i-finite`` 0 THEN Auto)))
         )
   ) }

1
.....wf..... 
1. x : ℝ
2. y : ℝ
3. r0 < x
4. r0 < y
5. r0 < rmin(x;y)
⊢ λx.rlog(x) ∈ [rmin(x;y), ∞) ⟶ℝ

2
.....wf..... 
1. x : ℝ
2. y : ℝ
3. r0 < x
4. r0 < y
5. r0 < rmin(x;y)
⊢ λx.(r1/x) ∈ [rmin(x;y), ∞) ⟶ℝ

3
.....antecedent..... 
1. x : ℝ
2. y : ℝ
3. r0 < x
4. r0 < y
5. r0 < rmin(x;y)
⊢ ∀x@0,y:{x@0:ℝ| x@0 ∈ [rmin(x;y), ∞)} .  ((x@0 = y) ⇒ ((r1/x@0) = (r1/y)))

4
.....antecedent..... 
1. x : ℝ
2. y : ℝ
3. r0 < x
4. r0 < y
5. r0 < rmin(x;y)
⊢ d(rlog(x))/dx = λx.(r1/x) on [rmin(x;y), ∞)

5
.....antecedent..... 
1. x : ℝ
2. y : ℝ
3. r0 < x
4. r0 < y
5. r0 < rmin(x;y)
⊢ ∀x@0:{x@0:ℝ| x@0 ∈ [rmin(x;y), ∞)} . (|(r1/x@0)| ≤ (r1/rmin(x;y)))

6
1. x : ℝ
2. y : ℝ
3. r0 < x
4. r0 < y
5. r0 < rmin(x;y)
6. ∀x@0,y@0:{x@0:ℝ| x@0 ∈ [rmin(x;y), ∞)} .  (|rlog(x@0) - rlog(y@0)| ≤ ((r1/rmin(x;y)) * |x@0 - y@0|))
⊢ |rlog(y) - rlog(x)| ≤ (|y - x|/rmin(x;y))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    ((r0  <  x)  {}\mRightarrow{}  (r0  <  y)  {}\mRightarrow{}  (|rlog(y)  -  rlog(x)|  \mleq{}  (|y  -  x|/rmin(x;y))))


By

---

Latex:
((Auto  THEN  (Assert  r0  <  rmin(x;y)  BY  EAuto  1))
  THEN  (InstLemma  `mean-value-for-bounded-derivative` 
              [\mkleeneopen{}[rmin(x;y),  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rlog(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(r1/x)\mkleeneclose{};\mkleeneopen{}(r1/rmin(x;y))\mkleeneclose{}]\mcdot{}
              THENA  Try  (Complete  ((Auto  THEN  RepUR  ``iproper  i-finite``  0  THEN  Auto)))
              )
  )

---

Home Index