---

Step * of Lemma rlog-difference-bound

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

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

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

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

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

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

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `mean-value-for-bounded-derivative` 
              [\mkleeneopen{}[x,  y]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rlog(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(r1/x)\mkleeneclose{};\mkleeneopen{}(r1/x)\mkleeneclose{}]\mcdot{}
              THENA  Try  (Complete  ((Auto  THEN  RepUR  ``iproper``  0  THEN  Auto)))
              )
  )

---

Home Index