src/HOL/Set_Interval.thy
 changeset 65578 e4997c181cce parent 65273 917ae0ba03a2 child 66490 cc66ab2373ce
```     1.1 --- a/src/HOL/Set_Interval.thy	Tue Apr 25 08:38:23 2017 +0200
1.2 +++ b/src/HOL/Set_Interval.thy	Tue Apr 25 16:39:54 2017 +0100
1.3 @@ -1892,7 +1892,7 @@
1.4    by (induction m) (simp_all add: algebra_simps)
1.5
1.6
1.7 -subsubsection \<open>The formula for geometric sums\<close>
1.8 +subsection \<open>The formula for geometric sums\<close>
1.9
1.10  lemma geometric_sum:
1.11    assumes "x \<noteq> 1"
1.12 @@ -1947,6 +1947,71 @@
1.13    shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
1.14  by (metis one_diff_power_eq' [of n x] nat_diff_sum_reindex)
1.15
1.16 +lemma sum_gp_basic:
1.17 +  fixes x :: "'a::{comm_ring,monoid_mult}"
1.18 +  shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
1.19 +  by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
1.20 +
1.21 +lemma sum_power_shift:
1.22 +  fixes x :: "'a::{comm_ring,monoid_mult}"
1.23 +  assumes "m \<le> n"
1.24 +  shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
1.25 +proof -
1.26 +  have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
1.28 +  also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
1.29 +    using \<open>m \<le> n\<close> by (intro sum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto
1.30 +  finally show ?thesis .
1.31 +qed
1.32 +
1.33 +lemma sum_gp_multiplied:
1.34 +  fixes x :: "'a::{comm_ring,monoid_mult}"
1.35 +  assumes "m \<le> n"
1.36 +  shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
1.37 +proof -
1.38 +  have  "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
1.39 +    by (metis mult.assoc mult.commute assms sum_power_shift)
1.40 +  also have "... =x^m * (1 - x^Suc(n-m))"
1.41 +    by (metis mult.assoc sum_gp_basic)
1.42 +  also have "... = x^m - x^Suc n"
1.43 +    using assms
1.45 +  finally show ?thesis .
1.46 +qed
1.47 +
1.48 +lemma sum_gp:
1.49 +  fixes x :: "'a::{comm_ring,division_ring}"
1.50 +  shows   "(\<Sum>i=m..n. x^i) =
1.51 +               (if n < m then 0
1.52 +                else if x = 1 then of_nat((n + 1) - m)
1.53 +                else (x^m - x^Suc n) / (1 - x))"
1.54 +using sum_gp_multiplied [of m n x] apply auto
1.55 +by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
1.56 +
1.57 +subsection\<open>Geometric progressions\<close>
1.58 +
1.59 +lemma sum_gp0:
1.60 +  fixes x :: "'a::{comm_ring,division_ring}"
1.61 +  shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
1.62 +  using sum_gp_basic[of x n]
1.63 +  by (simp add: mult.commute divide_simps)
1.64 +
1.66 +  fixes x :: "'a::{comm_ring,monoid_mult}"
1.67 +  shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
1.69 +
1.70 +lemma sum_gp_offset:
1.71 +  fixes x :: "'a::{comm_ring,division_ring}"
1.72 +  shows   "(\<Sum>i=m..m+n. x^i) =
1.73 +       (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
1.74 +  using sum_gp [of x m "m+n"]
1.75 +  by (auto simp: power_add algebra_simps)
1.76 +
1.77 +lemma sum_gp_strict:
1.78 +  fixes x :: "'a::{comm_ring,division_ring}"
1.79 +  shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
1.80 +  by (induct n) (auto simp: algebra_simps divide_simps)
1.81
1.82  subsubsection \<open>The formula for arithmetic sums\<close>
1.83
```