author paulson Wed May 09 14:07:19 2018 +0100 (14 months ago) changeset 68127 137d5d0112bb parent 68125 2e5b737810a6 child 68128 4646124e683e
more infinite product theorems
 src/HOL/Analysis/Infinite_Products.thy file | annotate | diff | revisions src/HOL/Series.thy file | annotate | diff | revisions
```     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.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)"])