15 fixes x :: "'a::{comm_ring,monoid_mult}" |
15 fixes x :: "'a::{comm_ring,monoid_mult}" |
16 shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n" |
16 shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n" |
17 by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost) |
17 by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost) |
18 |
18 |
19 lemma setsum_gp0: |
19 lemma setsum_gp0: |
20 fixes x :: "'a::{comm_ring,division_ring_inverse_zero}" |
20 fixes x :: "'a::{comm_ring,division_ring}" |
21 shows "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))" |
21 shows "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))" |
22 using setsum_gp_basic[of x n] |
22 using setsum_gp_basic[of x n] |
23 by (simp add: real_of_nat_def mult.commute divide_simps) |
23 by (simp add: real_of_nat_def mult.commute divide_simps) |
24 |
24 |
25 lemma setsum_power_add: |
25 lemma setsum_power_add: |
53 by (simp add: algebra_simps) (metis le_add_diff_inverse power_add) |
53 by (simp add: algebra_simps) (metis le_add_diff_inverse power_add) |
54 finally show ?thesis . |
54 finally show ?thesis . |
55 qed |
55 qed |
56 |
56 |
57 lemma setsum_gp: |
57 lemma setsum_gp: |
58 fixes x :: "'a::{comm_ring,division_ring_inverse_zero}" |
58 fixes x :: "'a::{comm_ring,division_ring}" |
59 shows "(\<Sum>i=m..n. x^i) = |
59 shows "(\<Sum>i=m..n. x^i) = |
60 (if n < m then 0 |
60 (if n < m then 0 |
61 else if x = 1 then of_nat((n + 1) - m) |
61 else if x = 1 then of_nat((n + 1) - m) |
62 else (x^m - x^Suc n) / (1 - x))" |
62 else (x^m - x^Suc n) / (1 - x))" |
63 using setsum_gp_multiplied [of m n x] |
63 using setsum_gp_multiplied [of m n x] |
64 apply (auto simp: real_of_nat_def) |
64 apply (auto simp: real_of_nat_def) |
65 by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq) |
65 by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq) |
66 |
66 |
67 lemma setsum_gp_offset: |
67 lemma setsum_gp_offset: |
68 fixes x :: "'a::{comm_ring,division_ring_inverse_zero}" |
68 fixes x :: "'a::{comm_ring,division_ring}" |
69 shows "(\<Sum>i=m..m+n. x^i) = |
69 shows "(\<Sum>i=m..m+n. x^i) = |
70 (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" |
70 (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" |
71 using setsum_gp [of x m "m+n"] |
71 using setsum_gp [of x m "m+n"] |
72 by (auto simp: power_add algebra_simps) |
72 by (auto simp: power_add algebra_simps) |
73 |
73 |
74 lemma setsum_gp_strict: |
74 lemma setsum_gp_strict: |
75 fixes x :: "'a::{comm_ring,division_ring_inverse_zero}" |
75 fixes x :: "'a::{comm_ring,division_ring}" |
76 shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))" |
76 shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))" |
77 by (induct n) (auto simp: algebra_simps divide_simps) |
77 by (induct n) (auto simp: algebra_simps divide_simps) |
78 |
78 |
79 subsection{*Basics about polynomial functions: extremal behaviour and root counts.*} |
79 subsection{*Basics about polynomial functions: extremal behaviour and root counts.*} |
80 |
80 |