equal
deleted
inserted
replaced
1533 |
1533 |
1534 definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f $ (n + 1))" |
1534 definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f $ (n + 1))" |
1535 |
1535 |
1536 lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n + 1)" |
1536 lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n + 1)" |
1537 by (simp add: fps_deriv_def) |
1537 by (simp add: fps_deriv_def) |
|
1538 |
|
1539 lemma fps_0th_higher_deriv: |
|
1540 "(fps_deriv ^^ n) f $ 0 = (fact n * f $ n :: 'a :: {comm_ring_1, semiring_char_0})" |
|
1541 by (induction n arbitrary: f) (simp_all del: funpow.simps add: funpow_Suc_right algebra_simps) |
1538 |
1542 |
1539 lemma fps_deriv_linear[simp]: |
1543 lemma fps_deriv_linear[simp]: |
1540 "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = |
1544 "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = |
1541 fps_const a * fps_deriv f + fps_const b * fps_deriv g" |
1545 fps_const a * fps_deriv f + fps_const b * fps_deriv g" |
1542 unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: field_simps) |
1546 unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: field_simps) |