- POWDIFF_LEMMA
-
|- ∀n x y.
sum (0,SUC n) (λp. x pow p * y pow (SUC n − p)) =
y * sum (0,SUC n) (λp. x pow p * y pow (n − p))
- POWDIFF
-
|- ∀n x y.
x pow SUC n − y pow SUC n =
(x − y) * sum (0,SUC n) (λp. x pow p * y pow (n − p))
- POWREV
-
|- ∀n x y.
sum (0,SUC n) (λp. x pow p * y pow (n − p)) =
sum (0,SUC n) (λp. x pow (n − p) * y pow p)
- POWSER_INSIDEA
-
|- ∀f x z.
summable (λn. f n * x pow n) ∧ abs z < abs x ⇒
summable (λn. abs (f n) * z pow n)
- POWSER_INSIDE
-
|- ∀f x z.
summable (λn. f n * x pow n) ∧ abs z < abs x ⇒
summable (λn. f n * z pow n)
- DIFFS_NEG
-
|- ∀c. diffs (λn. -c n) = (λn. -diffs c n)
- DIFFS_LEMMA
-
|- ∀n c x.
sum (0,n) (λn. diffs c n * x pow n) =
sum (0,n) (λn. &n * (c n * x pow (n − 1))) + &n * (c n * x pow (n − 1))
- DIFFS_LEMMA2
-
|- ∀n c x.
sum (0,n) (λn. &n * (c n * x pow (n − 1))) =
sum (0,n) (λn. diffs c n * x pow n) − &n * (c n * x pow (n − 1))
- DIFFS_EQUIV
-
|- ∀c x.
summable (λn. diffs c n * x pow n) ⇒
(λn. &n * (c n * x pow (n − 1))) sums suminf (λn. diffs c n * x pow n)
- TERMDIFF_LEMMA1
-
|- ∀m z h.
sum (0,m) (λp. (z + h) pow (m − p) * z pow p − z pow m) =
sum (0,m) (λp. z pow p * ((z + h) pow (m − p) − z pow (m − p)))
- TERMDIFF_LEMMA2
-
|- ∀z h n.
h ≠ 0 ⇒
(((z + h) pow n − z pow n) / h − &n * z pow (n − 1) =
h *
sum (0,n − 1)
(λp.
z pow p *
sum (0,n − 1 − p) (λq. (z + h) pow q * z pow (n − 2 − p − q))))
- TERMDIFF_LEMMA3
-
|- ∀z h n k'.
h ≠ 0 ∧ abs z ≤ k' ∧ abs (z + h) ≤ k' ⇒
abs (((z + h) pow n − z pow n) / h − &n * z pow (n − 1)) ≤
&n * (&(n − 1) * (k' pow (n − 2) * abs h))
- TERMDIFF_LEMMA4
-
|- ∀f k' k.
0 < k ∧ (∀h. 0 < abs h ∧ abs h < k ⇒ abs (f h) ≤ k' * abs h) ⇒ (f -> 0) 0
- TERMDIFF_LEMMA5
-
|- ∀f g k.
0 < k ∧ summable f ∧
(∀h. 0 < abs h ∧ abs h < k ⇒ ∀n. abs (g h n) ≤ f n * abs h) ⇒
((λh. suminf (g h)) -> 0) 0
- TERMDIFF
-
|- ∀c k' x.
summable (λn. c n * k' pow n) ∧ summable (λn. diffs c n * k' pow n) ∧
summable (λn. diffs (diffs c) n * k' pow n) ∧ abs x < abs k' ⇒
((λx. suminf (λn. c n * x pow n)) diffl suminf (λn. diffs c n * x pow n))
x