more infinite product theorems
authorpaulson <lp15@cam.ac.uk>
Wed May 09 14:07:19 2018 +0100 (14 months ago)
changeset 68127137d5d0112bb
parent 68125 2e5b737810a6
child 68128 4646124e683e
more infinite product theorems
src/HOL/Analysis/Infinite_Products.thy
src/HOL/Series.thy
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Wed May 09 07:48:54 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Wed May 09 14:07:19 2018 +0100
     1.3 @@ -688,4 +688,31 @@
     1.4      by (simp add: convergent_prod_def)
     1.5  qed
     1.6  
     1.7 +lemma has_prod_If_finite_set:
     1.8 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
     1.9 +  shows "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 1) has_prod (\<Prod>r\<in>A. f r)"
    1.10 +  using has_prod_finite[of A "(\<lambda>r. if r \<in> A then f r else 1)"]
    1.11 +  by simp
    1.12 +
    1.13 +lemma has_prod_If_finite:
    1.14 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    1.15 +  shows "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 1) has_prod (\<Prod>r | P r. f r)"
    1.16 +  using has_prod_If_finite_set[of "{r. P r}"] by simp
    1.17 +
    1.18 +lemma convergent_prod_If_finite_set[simp, intro]:
    1.19 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    1.20 +  shows "finite A \<Longrightarrow> convergent_prod (\<lambda>r. if r \<in> A then f r else 1)"
    1.21 +  by (simp add: convergent_prod_finite)
    1.22 +
    1.23 +lemma convergent_prod_If_finite[simp, intro]:
    1.24 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    1.25 +  shows "finite {r. P r} \<Longrightarrow> convergent_prod (\<lambda>r. if P r then f r else 1)"
    1.26 +  using convergent_prod_def has_prod_If_finite has_prod_def by fastforce
    1.27 +
    1.28 +lemma has_prod_single:
    1.29 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    1.30 +  shows "(\<lambda>r. if r = i then f r else 1) has_prod f i"
    1.31 +  using has_prod_If_finite[of "\<lambda>r. r = i"] by simp
    1.32 +
    1.33 +
    1.34  end
     2.1 --- a/src/HOL/Series.thy	Wed May 09 07:48:54 2018 +0200
     2.2 +++ b/src/HOL/Series.thy	Wed May 09 14:07:19 2018 +0100
     2.3 @@ -115,24 +115,11 @@
     2.4    shows "f sums (\<Sum>n\<in>N. f n)"
     2.5  proof -
     2.6    have eq: "sum f {..<n + Suc (Max N)} = sum f N" for n
     2.7 -  proof (cases "N = {}")
     2.8 -    case True
     2.9 -    with f have "f = (\<lambda>x. 0)" by auto
    2.10 -    then show ?thesis by simp
    2.11 -  next
    2.12 -    case [simp]: False
    2.13 -    show ?thesis
    2.14 -    proof (safe intro!: sum.mono_neutral_right f)
    2.15 -      fix i
    2.16 -      assume "i \<in> N"
    2.17 -      then have "i \<le> Max N" by simp
    2.18 -      then show "i < n + Suc (Max N)" by simp
    2.19 -    qed
    2.20 -  qed
    2.21 +    by (rule sum.mono_neutral_right) (auto simp: add_increasing less_Suc_eq_le f)
    2.22    show ?thesis
    2.23      unfolding sums_def
    2.24      by (rule LIMSEQ_offset[of _ "Suc (Max N)"])
    2.25 -       (simp add: eq atLeast0LessThan del: add_Suc_right)
    2.26 +      (simp add: eq atLeast0LessThan del: add_Suc_right)
    2.27  qed
    2.28  
    2.29  corollary sums_0: "(\<And>n. f n = 0) \<Longrightarrow> (f sums 0)"