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.27 +    by (simp add: sum_distrib_left power_add [symmetric])
    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.44 +    by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
    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.65 +lemma sum_power_add:
    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.68 +  by (simp add: sum_distrib_left power_add)
    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