Theory "powser"

Signature

Definitions

diffs

⊢ ∀c. diffs c = (λn. &SUC n * c (SUC n))

Theorems

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_LEMMA4

⊢ ∀f k' k.
      0 < k ∧ (∀h. 0 < abs h ∧ abs h < k ⇒ abs (f h) ≤ k' * abs h) ⇒
      (f -> 0) 0

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_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_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

⊢ ∀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

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)

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)

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))

DIFFS_NEG

⊢ ∀c. diffs (λn. -c n) = (λn. -diffs c n)

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_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_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)