---

Step * of Lemma second-derivative-log-contraction

∀a:{a:ℝ| r0 < a} . d((a - e^x/a + e^x)^2)/dx = λx.(((r(-4) * a) * e^x) * (a - e^x)/a + e^x^3) on (-∞, ∞)
BY
{ ((Auto
    THEN (Assert a + e^x≠r0 for x ∈ (-∞, ∞) BY
                ((D 0 THENA Auto)
                 THEN D 0 With ⌜a⌝ 
                 THEN Auto
                 THEN (RWO "rabs-of-nonneg" 0 THEN Auto)
                 THEN RWO "rexp-positive<" 0
                 THEN Auto))
    )
   THEN Assert ⌜d((a - e^x/a + e^x))/dx = λx.((r(-2) * a) * e^x/a + e^x^2) on (-∞, ∞)⌝⋅
   ) }

1
.....assertion..... 
1. a : {a:ℝ| r0 < a} 
2. a + e^x≠r0 for x ∈ (-∞, ∞)
⊢ d((a - e^x/a + e^x))/dx = λx.((r(-2) * a) * e^x/a + e^x^2) on (-∞, ∞)

2
1. a : {a:ℝ| r0 < a} 
2. a + e^x≠r0 for x ∈ (-∞, ∞)
3. d((a - e^x/a + e^x))/dx = λx.((r(-2) * a) * e^x/a + e^x^2) on (-∞, ∞)
⊢ d((a - e^x/a + e^x)^2)/dx = λx.(((r(-4) * a) * e^x) * (a - e^x)/a + e^x^3) on (-∞, ∞)

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbR{}|  r0  <  a\} 
    d((a  -  e\^{}x/a  +  e\^{}x)\^{}2)/dx  =  \mlambda{}x.(((r(-4)  *  a)  *  e\^{}x)  *  (a  -  e\^{}x)/a  +  e\^{}x\^{}3)  on  (-\minfty{},  \minfty{})


By

---

Latex:
((Auto
    THEN  (Assert  a  +  e\^{}x\mneq{}r0  for  x  \mmember{}  (-\minfty{},  \minfty{})  BY
                            ((D  0  THENA  Auto)
                              THEN  D  0  With  \mkleeneopen{}a\mkleeneclose{} 
                              THEN  Auto
                              THEN  (RWO  "rabs-of-nonneg"  0  THEN  Auto)
                              THEN  RWO  "rexp-positive<"  0
                              THEN  Auto))
    )
  THEN  Assert  \mkleeneopen{}d((a  -  e\^{}x/a  +  e\^{}x))/dx  =  \mlambda{}x.((r(-2)  *  a)  *  e\^{}x/a  +  e\^{}x\^{}2)  on  (-\minfty{},  \minfty{})\mkleeneclose{}\mcdot{}
  )

---

Home Index