Step
*
1
3
1
1
1
1
1
of Lemma
log-contraction-Taylor
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)
7. e : {e:ℝ| r0 < e}
8. c : ℝ
9. rmin(rlog(a);x) ≤ c
10. c ≤ rmax(rlog(a);x)
11. |Taylor-remainder((-∞, ∞);2;x;rlog(a);k,x.if (k =z 0) then log-contraction(a;x)
if (k =z 1) then (a - e^x/a + e^x)^2
if (k =z 2) then (((r(-4) * a) * e^x) * (a - e^x)/a + e^x^3)
else (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)/a + e^x^4)
fi ) - (x - c^2 * ((((r(16) * a^2) * e^c^2) + ((r(-4) * a^3) * e^c) + ((r(-4) * a) * e^c^3)/a + e^c^4)/r((2)!)))
* (x - rlog(a))| ≤ e
12. v : ℝ
13. (a - e^rlog(a)) = v ∈ ℝ
14. v1 : ℝ
15. a + e^rlog(a)^4 = v1 ∈ ℝ
16. v2 : ℝ
17. a + e^rlog(a)^3 = v2 ∈ ℝ
18. v3 : ℝ
19. (((r(16) * a^2) * e^rlog(a)^2) + ((r(-4) * a^3) * e^rlog(a)) + ((r(-4) * a) * e^rlog(a)^3)) = v3 ∈ ℝ
20. r0 < (a + e^rlog(a))
21. r0 < v2
22. r0 < v1
23. v = r0
⊢ (log-contraction(a;x) - Σ{(if (k =z 0) then log-contraction(a;rlog(a))
if (k =z 1) then (v/a + e^rlog(a))^2
if (k =z 2) then (((r(-4) * a) * e^rlog(a)) * v/v2)
else (v3/v1)
fi /r((k)!))
* x - rlog(a)^k | 0≤k≤2})
= (log-contraction(a;x) - rlog(a))
BY
{ (RepUR ``rsum`` 0 THEN RepeatFor 4 ((RecUnfold `from-upto` 0 THEN Reduce 0))) }
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)
7. e : {e:ℝ| r0 < e}
8. c : ℝ
9. rmin(rlog(a);x) ≤ c
10. c ≤ rmax(rlog(a);x)
11. |Taylor-remainder((-∞, ∞);2;x;rlog(a);k,x.if (k =z 0) then log-contraction(a;x)
if (k =z 1) then (a - e^x/a + e^x)^2
if (k =z 2) then (((r(-4) * a) * e^x) * (a - e^x)/a + e^x^3)
else (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)/a + e^x^4)
fi ) - (x - c^2 * ((((r(16) * a^2) * e^c^2) + ((r(-4) * a^3) * e^c) + ((r(-4) * a) * e^c^3)/a + e^c^4)/r((2)!)))
* (x - rlog(a))| ≤ e
12. v : ℝ
13. (a - e^rlog(a)) = v ∈ ℝ
14. v1 : ℝ
15. a + e^rlog(a)^4 = v1 ∈ ℝ
16. v2 : ℝ
17. a + e^rlog(a)^3 = v2 ∈ ℝ
18. v3 : ℝ
19. (((r(16) * a^2) * e^rlog(a)^2) + ((r(-4) * a^3) * e^rlog(a)) + ((r(-4) * a) * e^rlog(a)^3)) = v3 ∈ ℝ
20. r0 < (a + e^rlog(a))
21. r0 < v2
22. r0 < v1
23. v = r0
⊢ (log-contraction(a;x) - let xs ⟵ [(log-contraction(a;rlog(a))/r1) * r1;
((v/a + e^rlog(a))^2/r((1)!)) * x - rlog(a)^1;
((((r(-4) * a) * e^rlog(a)) * v/v2)/r((2)!)) * x - rlog(a)^2]
in radd-list(xs))
= (log-contraction(a;x) - rlog(a))
Latex:
Latex:
1. a : \mBbbR{}
2. x : \mBbbR{}
3. r0 < a
4. |x - rlog(a)| \mleq{} r1
5. \mforall{}x:\mBbbR{}. (r0 < (a + e\^{}x))
6. \mforall{}x:\mBbbR{}. \mforall{}n:\mBbbN{}\msupplus{}. (r0 < a + e\^{}x\^{}n)
7. e : \{e:\mBbbR{}| r0 < e\}
8. c : \mBbbR{}
9. rmin(rlog(a);x) \mleq{} c
10. c \mleq{} rmax(rlog(a);x)
11. |Taylor-remainder((-\minfty{}, \minfty{});2;x;rlog(a);k,x.if (k =\msubz{} 0) then log-contraction(a;x)
if (k =\msubz{} 1) then (a - e\^{}x/a + e\^{}x)\^{}2
if (k =\msubz{} 2) then (((r(-4) * a) * e\^{}x) * (a - e\^{}x)/a + e\^{}x\^{}3)
else (((r(16) * a\^{}2) * e\^{}x\^{}2) + ((r(-4) * a\^{}3) * e\^{}x) + ((r(-4) * a) * e\^{}x\^{}3)/a + e\^{}x\^{}4)
fi ) - (x - c\^{}2
* ((((r(16) * a\^{}2) * e\^{}c\^{}2) + ((r(-4) * a\^{}3) * e\^{}c) + ((r(-4) * a) * e\^{}c\^{}3)/a + e\^{}c\^{}4)/r((2)!)))
* (x - rlog(a))| \mleq{} e
12. v : \mBbbR{}
13. (a - e\^{}rlog(a)) = v
14. v1 : \mBbbR{}
15. a + e\^{}rlog(a)\^{}4 = v1
16. v2 : \mBbbR{}
17. a + e\^{}rlog(a)\^{}3 = v2
18. v3 : \mBbbR{}
19. (((r(16) * a\^{}2) * e\^{}rlog(a)\^{}2) + ((r(-4) * a\^{}3) * e\^{}rlog(a)) + ((r(-4) * a) * e\^{}rlog(a)\^{}3)) = v3
20. r0 < (a + e\^{}rlog(a))
21. r0 < v2
22. r0 < v1
23. v = r0
\mvdash{} (log-contraction(a;x) - \mSigma{}\{(if (k =\msubz{} 0) then log-contraction(a;rlog(a))
if (k =\msubz{} 1) then (v/a + e\^{}rlog(a))\^{}2
if (k =\msubz{} 2) then (((r(-4) * a) * e\^{}rlog(a)) * v/v2)
else (v3/v1)
fi /r((k)!))
* x - rlog(a)\^{}k | 0\mleq{}k\mleq{}2\})
= (log-contraction(a;x) - rlog(a))
By
Latex:
(RepUR ``rsum`` 0 THEN RepeatFor 4 ((RecUnfold `from-upto` 0 THEN Reduce 0)))
Home
Index