infinite product material
authorpaulson <lp15@cam.ac.uk>
Sun Jun 03 15:22:30 2018 +0100 (13 months ago)
changeset 6836120375f232f3b
parent 68360 0f19c98fa7be
child 68363 23b2fad1729a
child 68371 17c3b22a9575
infinite product material
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Infinite_Products.thy
src/HOL/Groups_Big.thy
src/HOL/Set_Interval.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sat Jun 02 22:57:44 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Jun 03 15:22:30 2018 +0100
     1.3 @@ -40,9 +40,7 @@
     1.4  
     1.5  lemmas swap_apply1 = swap_apply(1)
     1.6  lemmas swap_apply2 = swap_apply(2)
     1.7 -lemmas lessThan_empty_iff = Iio_eq_empty_iff_nat
     1.8  lemmas Zero_notin_Suc = zero_notin_Suc_image
     1.9 -lemmas atMost_Suc_eq_insert_0 = Iic_Suc_eq_insert_0
    1.10  
    1.11  lemma pointwise_minimal_pointwise_maximal:
    1.12    fixes s :: "(nat \<Rightarrow> nat) set"
     2.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Jun 02 22:57:44 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Jun 03 15:22:30 2018 +0100
     2.3 @@ -3925,55 +3925,42 @@
     2.4  subsection \<open>Stronger form with finite number of exceptional points\<close>
     2.5  
     2.6  lemma fundamental_theorem_of_calculus_interior_strong:
     2.7 -  fixes f :: "real \<Rightarrow> 'a::banach"
     2.8 -  assumes "finite s"
     2.9 -    and "a \<le> b"
    2.10 -    and "continuous_on {a..b} f"
    2.11 -    and "\<forall>x\<in>{a <..< b} - s. (f has_vector_derivative f'(x)) (at x)"
    2.12 -  shows "(f' has_integral (f b - f a)) {a..b}"
    2.13 + fixes f :: "real \<Rightarrow> 'a::banach"
    2.14 + assumes "finite S"
    2.15 +   and "a \<le> b" "\<And>x. x \<in> {a <..< b} - S \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)"
    2.16 +   and "continuous_on {a .. b} f"
    2.17 + shows "(f' has_integral (f b - f a)) {a .. b}"
    2.18    using assms
    2.19 -proof (induct "card s" arbitrary: s a b)
    2.20 -  case 0
    2.21 +proof (induction arbitrary: a b)
    2.22 +case empty
    2.23    then show ?case
    2.24 -    by (force simp add: intro: fundamental_theorem_of_calculus_interior)
    2.25 +    using fundamental_theorem_of_calculus_interior by force
    2.26  next
    2.27 -  case (Suc n)
    2.28 -  then obtain c s' where cs: "s = insert c s'" and n: "n = card s'"
    2.29 -    by (metis card_eq_SucD)
    2.30 -  then have "finite s'"
    2.31 -    using \<open>finite s\<close> by force
    2.32 +case (insert x S)
    2.33    show ?case
    2.34 -  proof (cases "c \<in> box a b")
    2.35 -    case False
    2.36 -    with \<open>finite s'\<close> show ?thesis
    2.37 -      using cs n Suc
    2.38 -      by (metis Diff_iff box_real(1) insert_iff)
    2.39 +  proof (cases "x \<in> {a<..<b}")
    2.40 +    case False then show ?thesis
    2.41 +      using insert by blast
    2.42    next
    2.43 -    let ?P = "\<lambda>i j. \<forall>x\<in>{i <..< j} - s'. (f has_vector_derivative f' x) (at x)"
    2.44 -    case True
    2.45 -    then have "a \<le> c" "c \<le> b"
    2.46 -      by (auto simp: mem_box)
    2.47 -    moreover have "?P a c" "?P c b"
    2.48 -      using Suc.prems(4) True \<open>a \<le> c\<close> cs(1) by auto
    2.49 -    moreover have "continuous_on {a..c} f" "continuous_on {c..b} f"
    2.50 -      using \<open>continuous_on {a..b} f\<close> \<open>a \<le> c\<close> \<open>c \<le> b\<close> continuous_on_subset by fastforce+
    2.51 -    ultimately have "(f' has_integral f c - f a + (f b - f c)) {a..b}"
    2.52 -      using Suc.hyps(1) \<open>finite s'\<close> \<open>n = card s'\<close> by (blast intro: has_integral_combine)
    2.53 -      then show ?thesis
    2.54 -        by auto
    2.55 +    case True then have "a < x" "x < b"
    2.56 +      by auto
    2.57 +    have "(f' has_integral f x - f a) {a..x}" "(f' has_integral f b - f x) {x..b}"
    2.58 +      using \<open>continuous_on {a..b} f\<close> \<open>a < x\<close> \<open>x < b\<close> continuous_on_subset by (force simp: intro!: insert)+
    2.59 +    then have "(f' has_integral f x - f a + (f b - f x)) {a..b}"
    2.60 +      using \<open>a < x\<close> \<open>x < b\<close> has_integral_combine less_imp_le by blast
    2.61 +    then show ?thesis
    2.62 +      by simp
    2.63    qed
    2.64  qed
    2.65  
    2.66  corollary fundamental_theorem_of_calculus_strong:
    2.67    fixes f :: "real \<Rightarrow> 'a::banach"
    2.68 -  assumes "finite s"
    2.69 +  assumes "finite S"
    2.70      and "a \<le> b"
    2.71 +    and vec: "\<And>x. x \<in> {a..b} - S \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)"
    2.72      and "continuous_on {a..b} f"
    2.73 -    and vec: "\<forall>x\<in>{a..b} - s. (f has_vector_derivative f'(x)) (at x)"
    2.74    shows "(f' has_integral (f b - f a)) {a..b}"
    2.75 -  apply (rule fundamental_theorem_of_calculus_interior_strong[OF assms(1-3), of f'])
    2.76 -  using vec apply (auto simp: mem_box)
    2.77 -  done
    2.78 +  by (rule fundamental_theorem_of_calculus_interior_strong [OF \<open>finite S\<close>]) (force simp: assms)+
    2.79  
    2.80  proposition indefinite_integral_continuous_left:
    2.81    fixes f:: "real \<Rightarrow> 'a::banach"
    2.82 @@ -7242,7 +7229,6 @@
    2.83    define f where "f = (\<lambda>k x. if x \<in> {inverse (of_nat (Suc k))..c} then x powr a else 0)"
    2.84    define F where "F = (\<lambda>k. if inverse (of_nat (Suc k)) \<le> c then
    2.85                               c powr (a+1)/(a+1) - inverse (real (Suc k)) powr (a+1)/(a+1) else 0)"
    2.86 -
    2.87    {
    2.88      fix k :: nat
    2.89      have "(f k has_integral F k) {0..c}"
    2.90 @@ -7448,8 +7434,8 @@
    2.91  
    2.92  lemma integrable_on_subinterval:
    2.93    fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
    2.94 -  assumes "f integrable_on s" "{a..b} \<subseteq> s"
    2.95 +  assumes "f integrable_on S" "{a..b} \<subseteq> S"
    2.96    shows "f integrable_on {a..b}"
    2.97 -  using integrable_on_subcbox[of f s a b] assms by (simp add: cbox_interval)
    2.98 +  using integrable_on_subcbox[of f S a b] assms by (simp add: cbox_interval)
    2.99  
   2.100  end
     3.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Sat Jun 02 22:57:44 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Sun Jun 03 15:22:30 2018 +0100
     3.3 @@ -50,21 +50,21 @@
     3.4      by (rule tendsto_eq_intros refl | simp)+
     3.5  qed auto
     3.6  
     3.7 -definition gen_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool" 
     3.8 -  where "gen_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
     3.9 +definition raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool" 
    3.10 +  where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
    3.11  
    3.12  text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close>
    3.13  definition has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
    3.14 -  where "f has_prod p \<equiv> gen_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> gen_has_prod f (Suc i) q)"
    3.15 +  where "f has_prod p \<equiv> raw_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> raw_has_prod f (Suc i) q)"
    3.16  
    3.17  definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where
    3.18 -  "convergent_prod f \<equiv> \<exists>M p. gen_has_prod f M p"
    3.19 +  "convergent_prod f \<equiv> \<exists>M p. raw_has_prod f M p"
    3.20  
    3.21  definition prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a"
    3.22      (binder "\<Prod>" 10)
    3.23    where "prodinf f = (THE p. f has_prod p)"
    3.24  
    3.25 -lemmas prod_defs = gen_has_prod_def has_prod_def convergent_prod_def prodinf_def
    3.26 +lemmas prod_defs = raw_has_prod_def has_prod_def convergent_prod_def prodinf_def
    3.27  
    3.28  lemma has_prod_subst[trans]: "f = g \<Longrightarrow> g has_prod z \<Longrightarrow> f has_prod z"
    3.29    by simp
    3.30 @@ -72,34 +72,39 @@
    3.31  lemma has_prod_cong: "(\<And>n. f n = g n) \<Longrightarrow> f has_prod c \<longleftrightarrow> g has_prod c"
    3.32    by presburger
    3.33  
    3.34 -lemma gen_has_prod_nonzero [simp]: "\<not> gen_has_prod f M 0"
    3.35 -  by (simp add: gen_has_prod_def)
    3.36 +lemma raw_has_prod_nonzero [simp]: "\<not> raw_has_prod f M 0"
    3.37 +  by (simp add: raw_has_prod_def)
    3.38  
    3.39 -lemma gen_has_prod_eq_0:
    3.40 -  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    3.41 -  assumes p: "gen_has_prod f m p" and i: "f i = 0" "i \<ge> m"
    3.42 +lemma raw_has_prod_eq_0:
    3.43 +  fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"
    3.44 +  assumes p: "raw_has_prod f m p" and i: "f i = 0" "i \<ge> m"
    3.45    shows "p = 0"
    3.46  proof -
    3.47    have eq0: "(\<Prod>k\<le>n. f (k+m)) = 0" if "i - m \<le> n" for n
    3.48 -    by (metis i that atMost_atLeast0 atMost_iff diff_add finite_atLeastAtMost prod_zero_iff)
    3.49 +  proof -
    3.50 +    have "\<exists>k\<le>n. f (k + m) = 0"
    3.51 +      using i that by auto
    3.52 +    then show ?thesis
    3.53 +      by auto
    3.54 +  qed
    3.55    have "(\<lambda>n. \<Prod>i\<le>n. f (i + m)) \<longlonglongrightarrow> 0"
    3.56      by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0)
    3.57      with p show ?thesis
    3.58 -      unfolding gen_has_prod_def
    3.59 +      unfolding raw_has_prod_def
    3.60      using LIMSEQ_unique by blast
    3.61  qed
    3.62  
    3.63 -lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. gen_has_prod f (Suc i) p))"
    3.64 +lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. raw_has_prod f (Suc i) p))"
    3.65    by (simp add: has_prod_def)
    3.66        
    3.67  lemma has_prod_unique2: 
    3.68 -  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    3.69 +  fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"
    3.70    assumes "f has_prod a" "f has_prod b" shows "a = b"
    3.71    using assms
    3.72 -  by (auto simp: has_prod_def gen_has_prod_eq_0) (meson gen_has_prod_def sequentially_bot tendsto_unique)
    3.73 +  by (auto simp: has_prod_def raw_has_prod_eq_0) (meson raw_has_prod_def sequentially_bot tendsto_unique)
    3.74  
    3.75  lemma has_prod_unique:
    3.76 -  fixes f :: "nat \<Rightarrow> 'a :: {idom,t2_space}"
    3.77 +  fixes f :: "nat \<Rightarrow> 'a :: {semidom,t2_space}"
    3.78    shows "f has_prod s \<Longrightarrow> s = prodinf f"
    3.79    by (simp add: has_prod_unique2 prodinf_def the_equality)
    3.80  
    3.81 @@ -378,42 +383,55 @@
    3.82    shows   "abs_convergent_prod f"
    3.83    using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset)
    3.84  
    3.85 -lemma convergent_prod_ignore_initial_segment:
    3.86 -  fixes f :: "nat \<Rightarrow> 'a :: {real_normed_field}"
    3.87 -  assumes "convergent_prod f"
    3.88 -  shows   "convergent_prod (\<lambda>n. f (n + m))"
    3.89 +lemma raw_has_prod_ignore_initial_segment:
    3.90 +  fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
    3.91 +  assumes "raw_has_prod f M p" "N \<ge> M"
    3.92 +  obtains q where  "raw_has_prod f N q"
    3.93  proof -
    3.94 -  from assms obtain M L 
    3.95 -    where L: "(\<lambda>n. \<Prod>k\<le>n. f (k + M)) \<longlonglongrightarrow> L" "L \<noteq> 0" and nz: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0"
    3.96 -    by (auto simp: convergent_prod_altdef)
    3.97 -  define C where "C = (\<Prod>k<m. f (k + M))"
    3.98 +  have p: "(\<lambda>n. \<Prod>k\<le>n. f (k + M)) \<longlonglongrightarrow> p" and "p \<noteq> 0" 
    3.99 +    using assms by (auto simp: raw_has_prod_def)
   3.100 +  then have nz: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0"
   3.101 +    using assms by (auto simp: raw_has_prod_eq_0)
   3.102 +  define C where "C = (\<Prod>k<N-M. f (k + M))"
   3.103    from nz have [simp]: "C \<noteq> 0" 
   3.104      by (auto simp: C_def)
   3.105  
   3.106 -  from L(1) have "(\<lambda>n. \<Prod>k\<le>n+m. f (k + M)) \<longlonglongrightarrow> L" 
   3.107 +  from p have "(\<lambda>i. \<Prod>k\<le>i + (N-M). f (k + M)) \<longlonglongrightarrow> p" 
   3.108      by (rule LIMSEQ_ignore_initial_segment)
   3.109 -  also have "(\<lambda>n. \<Prod>k\<le>n+m. f (k + M)) = (\<lambda>n. C * (\<Prod>k\<le>n. f (k + M + m)))"
   3.110 +  also have "(\<lambda>i. \<Prod>k\<le>i + (N-M). f (k + M)) = (\<lambda>n. C * (\<Prod>k\<le>n. f (k + N)))"
   3.111    proof (rule ext, goal_cases)
   3.112      case (1 n)
   3.113 -    have "{..n+m} = {..<m} \<union> {m..n+m}" by auto
   3.114 -    also have "(\<Prod>k\<in>\<dots>. f (k + M)) = C * (\<Prod>k=m..n+m. f (k + M))"
   3.115 +    have "{..n+(N-M)} = {..<(N-M)} \<union> {(N-M)..n+(N-M)}" by auto
   3.116 +    also have "(\<Prod>k\<in>\<dots>. f (k + M)) = C * (\<Prod>k=(N-M)..n+(N-M). f (k + M))"
   3.117        unfolding C_def by (rule prod.union_disjoint) auto
   3.118 -    also have "(\<Prod>k=m..n+m. f (k + M)) = (\<Prod>k\<le>n. f (k + m + M))"
   3.119 -      by (intro ext prod.reindex_bij_witness[of _ "\<lambda>k. k + m" "\<lambda>k. k - m"]) auto
   3.120 -    finally show ?case by (simp add: add_ac)
   3.121 +    also have "(\<Prod>k=(N-M)..n+(N-M). f (k + M)) = (\<Prod>k\<le>n. f (k + (N-M) + M))"
   3.122 +      by (intro ext prod.reindex_bij_witness[of _ "\<lambda>k. k + (N-M)" "\<lambda>k. k - (N-M)"]) auto
   3.123 +    finally show ?case
   3.124 +      using \<open>N \<ge> M\<close> by (simp add: add_ac)
   3.125    qed
   3.126 -  finally have "(\<lambda>n. C * (\<Prod>k\<le>n. f (k + M + m)) / C) \<longlonglongrightarrow> L / C"
   3.127 +  finally have "(\<lambda>n. C * (\<Prod>k\<le>n. f (k + N)) / C) \<longlonglongrightarrow> p / C"
   3.128      by (intro tendsto_divide tendsto_const) auto
   3.129 -  hence "(\<lambda>n. \<Prod>k\<le>n. f (k + M + m)) \<longlonglongrightarrow> L / C" by simp
   3.130 -  moreover from \<open>L \<noteq> 0\<close> have "L / C \<noteq> 0" by simp
   3.131 -  ultimately show ?thesis 
   3.132 -    unfolding prod_defs by blast
   3.133 +  hence "(\<lambda>n. \<Prod>k\<le>n. f (k + N)) \<longlonglongrightarrow> p / C" by simp
   3.134 +  moreover from \<open>p \<noteq> 0\<close> have "p / C \<noteq> 0" by simp
   3.135 +  ultimately show ?thesis
   3.136 +    using raw_has_prod_def that by blast 
   3.137  qed
   3.138  
   3.139 +corollary convergent_prod_ignore_initial_segment:
   3.140 +  fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
   3.141 +  assumes "convergent_prod f"
   3.142 +  shows   "convergent_prod (\<lambda>n. f (n + m))"
   3.143 +  using assms
   3.144 +  unfolding convergent_prod_def 
   3.145 +  apply clarify
   3.146 +  apply (erule_tac N="M+m" in raw_has_prod_ignore_initial_segment)
   3.147 +  apply (auto simp add: raw_has_prod_def add_ac)
   3.148 +  done
   3.149 +
   3.150  corollary convergent_prod_ignore_nonzero_segment:
   3.151    fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
   3.152    assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0"
   3.153 -  shows "\<exists>p. gen_has_prod f M p"
   3.154 +  shows "\<exists>p. raw_has_prod f M p"
   3.155    using convergent_prod_ignore_initial_segment [OF f]
   3.156    by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1))
   3.157  
   3.158 @@ -551,13 +569,13 @@
   3.159    with L show ?thesis by (auto simp: prod_defs)
   3.160  qed
   3.161  
   3.162 -lemma gen_has_prod_cases:
   3.163 +lemma raw_has_prod_cases:
   3.164    fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
   3.165 -  assumes "gen_has_prod f M p"
   3.166 -  obtains i where "i<M" "f i = 0" | p where "gen_has_prod f 0 p"
   3.167 +  assumes "raw_has_prod f M p"
   3.168 +  obtains i where "i<M" "f i = 0" | p where "raw_has_prod f 0 p"
   3.169  proof -
   3.170    have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0"
   3.171 -    using assms unfolding gen_has_prod_def by blast+
   3.172 +    using assms unfolding raw_has_prod_def by blast+
   3.173    then have "(\<lambda>n. prod f {..<M} * (\<Prod>i\<le>n. f (i + M))) \<longlonglongrightarrow> prod f {..<M} * p"
   3.174      by (metis tendsto_mult_left)
   3.175    moreover have "prod f {..<M} * (\<Prod>i\<le>n. f (i + M)) = prod f {..n+M}" for n
   3.176 @@ -572,8 +590,8 @@
   3.177    qed
   3.178    ultimately have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * p"
   3.179      by (auto intro: LIMSEQ_offset [where k=M])
   3.180 -  then have "gen_has_prod f 0 (prod f {..<M} * p)" if "\<forall>i<M. f i \<noteq> 0"
   3.181 -    using \<open>p \<noteq> 0\<close> assms that by (auto simp: gen_has_prod_def)
   3.182 +  then have "raw_has_prod f 0 (prod f {..<M} * p)" if "\<forall>i<M. f i \<noteq> 0"
   3.183 +    using \<open>p \<noteq> 0\<close> assms that by (auto simp: raw_has_prod_def)
   3.184    then show thesis
   3.185      using that by blast
   3.186  qed
   3.187 @@ -581,8 +599,8 @@
   3.188  corollary convergent_prod_offset_0:
   3.189    fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
   3.190    assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
   3.191 -  shows "\<exists>p. gen_has_prod f 0 p"
   3.192 -  using assms convergent_prod_def gen_has_prod_cases by blast
   3.193 +  shows "\<exists>p. raw_has_prod f 0 p"
   3.194 +  using assms convergent_prod_def raw_has_prod_cases by blast
   3.195  
   3.196  lemma prodinf_eq_lim:
   3.197    fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
   3.198 @@ -648,7 +666,7 @@
   3.199  qed
   3.200  
   3.201  lemma has_prod_finite:
   3.202 -  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
   3.203 +  fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"
   3.204    assumes [simp]: "finite N"
   3.205      and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"
   3.206    shows "f has_prod (\<Prod>n\<in>N. f n)"
   3.207 @@ -668,7 +686,7 @@
   3.208      moreover have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f N"
   3.209        by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) (simp add: eq atLeast0LessThan del: add_Suc_right)
   3.210      ultimately show ?thesis
   3.211 -      by (simp add: gen_has_prod_def has_prod_def)
   3.212 +      by (simp add: raw_has_prod_def has_prod_def)
   3.213    next
   3.214      case False
   3.215      then obtain k where "k \<in> N" "f k = 0"
   3.216 @@ -692,8 +710,8 @@
   3.217             (use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>)
   3.218        finally show ?thesis .
   3.219      qed
   3.220 -    have q: "gen_has_prod f (Suc (Max ?Z)) ?q"
   3.221 -    proof (simp add: gen_has_prod_def)
   3.222 +    have q: "raw_has_prod f (Suc (Max ?Z)) ?q"
   3.223 +    proof (simp add: raw_has_prod_def)
   3.224        show "(\<lambda>n. \<Prod>i\<le>n. f (Suc (i + Max ?Z))) \<longlonglongrightarrow> ?q"
   3.225          by (rule LIMSEQ_offset[of _ "(Max N)"]) (simp add: eq)
   3.226      qed
   3.227 @@ -709,17 +727,20 @@
   3.228  qed
   3.229  
   3.230  corollary has_prod_0:
   3.231 -  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
   3.232 +  fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"
   3.233    assumes "\<And>n. f n = 1"
   3.234    shows "f has_prod 1"
   3.235    by (simp add: assms has_prod_cong)
   3.236  
   3.237 +lemma prodinf_zero[simp]: "prodinf (\<lambda>n. 1::'a::real_normed_field) = 1"
   3.238 +  using has_prod_unique by force
   3.239 +
   3.240  lemma convergent_prod_finite:
   3.241    fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
   3.242    assumes "finite N" "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"
   3.243    shows "convergent_prod f"
   3.244  proof -
   3.245 -  have "\<exists>n p. gen_has_prod f n p"
   3.246 +  have "\<exists>n p. raw_has_prod f n p"
   3.247      using assms has_prod_def has_prod_finite by blast
   3.248    then show ?thesis
   3.249      by (simp add: convergent_prod_def)
   3.250 @@ -759,12 +780,12 @@
   3.251    assumes "convergent_prod f"
   3.252    shows "\<exists>p. f has_prod p"
   3.253  proof -
   3.254 -  obtain M p where p: "gen_has_prod f M p"
   3.255 +  obtain M p where p: "raw_has_prod f M p"
   3.256      using assms convergent_prod_def by blast
   3.257    then have "p \<noteq> 0"
   3.258 -    using gen_has_prod_nonzero by blast
   3.259 +    using raw_has_prod_nonzero by blast
   3.260    with p have fnz: "f i \<noteq> 0" if "i \<ge> M" for i
   3.261 -    using gen_has_prod_eq_0 that by blast
   3.262 +    using raw_has_prod_eq_0 that by blast
   3.263    define C where "C = (\<Prod>n<M. f n)"
   3.264    show ?thesis
   3.265    proof (cases "\<forall>n\<le>M. f n \<noteq> 0")
   3.266 @@ -781,7 +802,7 @@
   3.267        by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear)
   3.268      have "f i \<noteq> 0" if "i > ?N" for i
   3.269        by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that)
   3.270 -    then have "\<exists>p. gen_has_prod f (Suc ?N) p"
   3.271 +    then have "\<exists>p. raw_has_prod f (Suc ?N) p"
   3.272        using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment)
   3.273      then show ?thesis
   3.274        unfolding has_prod_def using 0 by blast
   3.275 @@ -796,7 +817,7 @@
   3.276  lemma convergent_prod_LIMSEQ:
   3.277    shows "convergent_prod f \<Longrightarrow> (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> prodinf f"
   3.278    by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent 
   3.279 -      convergent_prod_to_zero_iff gen_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le)
   3.280 +      convergent_prod_to_zero_iff raw_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le)
   3.281  
   3.282  lemma has_prod_iff: "f has_prod x \<longleftrightarrow> convergent_prod f \<and> prodinf f = x"
   3.283  proof
   3.284 @@ -818,4 +839,494 @@
   3.285  
   3.286  end
   3.287  
   3.288 +subsection \<open>Infinite products on ordered, topological monoids\<close>
   3.289 +
   3.290 +lemma LIMSEQ_prod_0: 
   3.291 +  fixes f :: "nat \<Rightarrow> 'a::{semidom,topological_space}"
   3.292 +  assumes "f i = 0"
   3.293 +  shows "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0"
   3.294 +proof (subst tendsto_cong)
   3.295 +  show "\<forall>\<^sub>F n in sequentially. prod f {..n} = 0"
   3.296 +  proof
   3.297 +    show "prod f {..n} = 0" if "n \<ge> i" for n
   3.298 +      using that assms by auto
   3.299 +  qed
   3.300 +qed auto
   3.301 +
   3.302 +lemma LIMSEQ_prod_nonneg: 
   3.303 +  fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}"
   3.304 +  assumes 0: "\<And>n. 0 \<le> f n" and a: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> a"
   3.305 +  shows "a \<ge> 0"
   3.306 +  by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a])
   3.307 +
   3.308 +
   3.309 +context
   3.310 +  fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}"
   3.311 +begin
   3.312 +
   3.313 +lemma has_prod_le:
   3.314 +  assumes f: "f has_prod a" and g: "g has_prod b" and le: "\<And>n. 0 \<le> f n \<and> f n \<le> g n"
   3.315 +  shows "a \<le> b"
   3.316 +proof (cases "a=0 \<or> b=0")
   3.317 +  case True
   3.318 +  then show ?thesis
   3.319 +  proof
   3.320 +    assume [simp]: "a=0"
   3.321 +    have "b \<ge> 0"
   3.322 +    proof (rule LIMSEQ_prod_nonneg)
   3.323 +      show "(\<lambda>n. prod g {..n}) \<longlonglongrightarrow> b"
   3.324 +        using g by (auto simp: has_prod_def raw_has_prod_def LIMSEQ_prod_0)
   3.325 +    qed (use le order_trans in auto)
   3.326 +    then show ?thesis
   3.327 +      by auto
   3.328 +  next
   3.329 +    assume [simp]: "b=0"
   3.330 +    then obtain i where "g i = 0"    
   3.331 +      using g by (auto simp: prod_defs)
   3.332 +    then have "f i = 0"
   3.333 +      using antisym le by force
   3.334 +    then have "a=0"
   3.335 +      using f by (auto simp: prod_defs LIMSEQ_prod_0 LIMSEQ_unique)
   3.336 +    then show ?thesis
   3.337 +      by auto
   3.338 +  qed
   3.339 +next
   3.340 +  case False
   3.341 +  then show ?thesis
   3.342 +    using assms
   3.343 +    unfolding has_prod_def raw_has_prod_def
   3.344 +    by (force simp: LIMSEQ_prod_0 intro!: LIMSEQ_le prod_mono)
   3.345 +qed
   3.346 +
   3.347 +lemma prodinf_le: 
   3.348 +  assumes f: "f has_prod a" and g: "g has_prod b" and le: "\<And>n. 0 \<le> f n \<and> f n \<le> g n"
   3.349 +  shows "prodinf f \<le> prodinf g"
   3.350 +  using has_prod_le [OF assms] has_prod_unique f g  by blast
   3.351 +
   3.352  end
   3.353 +
   3.354 +
   3.355 +lemma prod_le_prodinf: 
   3.356 +  fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}"
   3.357 +  assumes "f has_prod a" "\<And>i. 0 \<le> f i" "\<And>i. i\<ge>n \<Longrightarrow> 1 \<le> f i"
   3.358 +  shows "prod f {..<n} \<le> prodinf f"
   3.359 +  by(rule has_prod_le[OF has_prod_If_finite_set]) (use assms has_prod_unique in auto)
   3.360 +
   3.361 +lemma prodinf_nonneg:
   3.362 +  fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}"
   3.363 +  assumes "f has_prod a" "\<And>i. 1 \<le> f i" 
   3.364 +  shows "1 \<le> prodinf f"
   3.365 +  using prod_le_prodinf[of f a 0] assms
   3.366 +  by (metis order_trans prod_ge_1 zero_le_one)
   3.367 +
   3.368 +lemma prodinf_le_const:
   3.369 +  fixes f :: "nat \<Rightarrow> real"
   3.370 +  assumes "convergent_prod f" "\<And>n. prod f {..<n} \<le> x" 
   3.371 +  shows "prodinf f \<le> x"
   3.372 +  by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2)
   3.373 +
   3.374 +lemma prodinf_eq_one_iff: 
   3.375 +  fixes f :: "nat \<Rightarrow> real"
   3.376 +  assumes f: "convergent_prod f" and ge1: "\<And>n. 1 \<le> f n"
   3.377 +  shows "prodinf f = 1 \<longleftrightarrow> (\<forall>n. f n = 1)"
   3.378 +proof
   3.379 +  assume "prodinf f = 1" 
   3.380 +  then have "(\<lambda>n. \<Prod>i<n. f i) \<longlonglongrightarrow> 1"
   3.381 +    using convergent_prod_LIMSEQ[of f] assms by (simp add: LIMSEQ_lessThan_iff_atMost)
   3.382 +  then have "\<And>i. (\<Prod>n\<in>{i}. f n) \<le> 1"
   3.383 +  proof (rule LIMSEQ_le_const)
   3.384 +    have "1 \<le> prod f n" for n
   3.385 +      by (simp add: ge1 prod_ge_1)
   3.386 +    have "prod f {..<n} = 1" for n
   3.387 +      by (metis \<open>\<And>n. 1 \<le> prod f n\<close> \<open>prodinf f = 1\<close> antisym f convergent_prod_has_prod ge1 order_trans prod_le_prodinf zero_le_one)
   3.388 +    then have "(\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" if "n \<ge> Suc i" for i n
   3.389 +      by (metis mult.left_neutral order_refl prod.cong prod.neutral_const prod_lessThan_Suc)
   3.390 +    then show "\<exists>N. \<forall>n\<ge>N. (\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" for i
   3.391 +      by blast      
   3.392 +  qed
   3.393 +  with ge1 show "\<forall>n. f n = 1"
   3.394 +    by (auto intro!: antisym)
   3.395 +qed (metis prodinf_zero fun_eq_iff)
   3.396 +
   3.397 +lemma prodinf_pos_iff:
   3.398 +  fixes f :: "nat \<Rightarrow> real"
   3.399 +  assumes "convergent_prod f" "\<And>n. 1 \<le> f n"
   3.400 +  shows "1 < prodinf f \<longleftrightarrow> (\<exists>i. 1 < f i)"
   3.401 +  using prod_le_prodinf[of f 1] prodinf_eq_one_iff
   3.402 +  by (metis convergent_prod_has_prod assms less_le prodinf_nonneg)
   3.403 +
   3.404 +lemma less_1_prodinf2:
   3.405 +  fixes f :: "nat \<Rightarrow> real"
   3.406 +  assumes "convergent_prod f" "\<And>n. 1 \<le> f n" "1 < f i"
   3.407 +  shows "1 < prodinf f"
   3.408 +proof -
   3.409 +  have "1 < (\<Prod>n<Suc i. f n)"
   3.410 +    using assms  by (intro less_1_prod2[where i=i]) auto
   3.411 +  also have "\<dots> \<le> prodinf f"
   3.412 +    by (intro prod_le_prodinf) (use assms order_trans zero_le_one in \<open>blast+\<close>)
   3.413 +  finally show ?thesis .
   3.414 +qed
   3.415 +
   3.416 +lemma less_1_prodinf:
   3.417 +  fixes f :: "nat \<Rightarrow> real"
   3.418 +  shows "\<lbrakk>convergent_prod f; \<And>n. 1 < f n\<rbrakk> \<Longrightarrow> 1 < prodinf f"
   3.419 +  by (intro less_1_prodinf2[where i=1]) (auto intro: less_imp_le)
   3.420 +
   3.421 +lemma prodinf_nonzero:
   3.422 +  fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
   3.423 +  assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
   3.424 +  shows "prodinf f \<noteq> 0"
   3.425 +  by (metis assms convergent_prod_offset_0 has_prod_unique raw_has_prod_def has_prod_def)
   3.426 +
   3.427 +lemma less_0_prodinf:
   3.428 +  fixes f :: "nat \<Rightarrow> real"
   3.429 +  assumes f: "convergent_prod f" and 0: "\<And>i. f i > 0"
   3.430 +  shows "0 < prodinf f"
   3.431 +proof -
   3.432 +  have "prodinf f \<noteq> 0"
   3.433 +    by (metis assms less_irrefl prodinf_nonzero)
   3.434 +  moreover have "0 < (\<Prod>n<i. f n)" for i
   3.435 +    by (simp add: 0 prod_pos)
   3.436 +  then have "prodinf f \<ge> 0"
   3.437 +    using convergent_prod_LIMSEQ [OF f] LIMSEQ_prod_nonneg 0 less_le by blast
   3.438 +  ultimately show ?thesis
   3.439 +    by auto
   3.440 +qed
   3.441 +
   3.442 +lemma prod_less_prodinf2:
   3.443 +  fixes f :: "nat \<Rightarrow> real"
   3.444 +  assumes f: "convergent_prod f" and 1: "\<And>m. m\<ge>n \<Longrightarrow> 1 \<le> f m" and 0: "\<And>m. 0 < f m" and i: "n \<le> i" "1 < f i"
   3.445 +  shows "prod f {..<n} < prodinf f"
   3.446 +proof -
   3.447 +  have "prod f {..<n} \<le> prod f {..<i}"
   3.448 +    by (rule prod_mono2) (use assms less_le in auto)
   3.449 +  then have "prod f {..<n} < f i * prod f {..<i}"
   3.450 +    using mult_less_le_imp_less[of 1 "f i" "prod f {..<n}" "prod f {..<i}"] assms
   3.451 +    by (simp add: prod_pos)
   3.452 +  moreover have "prod f {..<Suc i} \<le> prodinf f"
   3.453 +    using prod_le_prodinf[of f _ "Suc i"]
   3.454 +    by (meson "0" "1" Suc_leD convergent_prod_has_prod f \<open>n \<le> i\<close> le_trans less_eq_real_def)
   3.455 +  ultimately show ?thesis
   3.456 +    by (metis le_less_trans mult.commute not_le prod_lessThan_Suc)
   3.457 +qed
   3.458 +
   3.459 +lemma prod_less_prodinf:
   3.460 +  fixes f :: "nat \<Rightarrow> real"
   3.461 +  assumes f: "convergent_prod f" and 1: "\<And>m. m\<ge>n \<Longrightarrow> 1 < f m" and 0: "\<And>m. 0 < f m" 
   3.462 +  shows "prod f {..<n} < prodinf f"
   3.463 +  by (meson "0" "1" f le_less prod_less_prodinf2)
   3.464 +
   3.465 +lemma raw_has_prodI_bounded:
   3.466 +  fixes f :: "nat \<Rightarrow> real"
   3.467 +  assumes pos: "\<And>n. 1 \<le> f n"
   3.468 +    and le: "\<And>n. (\<Prod>i<n. f i) \<le> x"
   3.469 +  shows "\<exists>p. raw_has_prod f 0 p"
   3.470 +  unfolding raw_has_prod_def add_0_right
   3.471 +proof (rule exI LIMSEQ_incseq_SUP conjI)+
   3.472 +  show "bdd_above (range (\<lambda>n. prod f {..n}))"
   3.473 +    by (metis bdd_aboveI2 le lessThan_Suc_atMost)
   3.474 +  then have "(SUP i. prod f {..i}) > 0"
   3.475 +    by (metis UNIV_I cSUP_upper less_le_trans pos prod_pos zero_less_one)
   3.476 +  then show "(SUP i. prod f {..i}) \<noteq> 0"
   3.477 +    by auto
   3.478 +  show "incseq (\<lambda>n. prod f {..n})"
   3.479 +    using pos order_trans [OF zero_le_one] by (auto simp: mono_def intro!: prod_mono2)
   3.480 +qed
   3.481 +
   3.482 +lemma convergent_prodI_nonneg_bounded:
   3.483 +  fixes f :: "nat \<Rightarrow> real"
   3.484 +  assumes "\<And>n. 1 \<le> f n" "\<And>n. (\<Prod>i<n. f i) \<le> x"
   3.485 +  shows "convergent_prod f"
   3.486 +  using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast
   3.487 +
   3.488 +
   3.489 +subsection \<open>Infinite products on topological monoids\<close>
   3.490 +
   3.491 +context
   3.492 +  fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_semigroup_mult,idom}"
   3.493 +begin
   3.494 +
   3.495 +lemma raw_has_prod_mult: "\<lbrakk>raw_has_prod f M a; raw_has_prod g M b\<rbrakk> \<Longrightarrow> raw_has_prod (\<lambda>n. f n * g n) M (a * b)"
   3.496 +  by (force simp add: prod.distrib tendsto_mult raw_has_prod_def)
   3.497 +
   3.498 +lemma has_prod_mult_nz: "\<lbrakk>f has_prod a; g has_prod b; a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. f n * g n) has_prod (a * b)"
   3.499 +  by (simp add: raw_has_prod_mult has_prod_def)
   3.500 +
   3.501 +end
   3.502 +
   3.503 +
   3.504 +context
   3.505 +  fixes f g :: "nat \<Rightarrow> 'a::real_normed_field"
   3.506 +begin
   3.507 +
   3.508 +lemma has_prod_mult:
   3.509 +  assumes f: "f has_prod a" and g: "g has_prod b"
   3.510 +  shows "(\<lambda>n. f n * g n) has_prod (a * b)"
   3.511 +  using f [unfolded has_prod_def]
   3.512 +proof (elim disjE exE conjE)
   3.513 +  assume f0: "raw_has_prod f 0 a"
   3.514 +  show ?thesis
   3.515 +    using g [unfolded has_prod_def]
   3.516 +  proof (elim disjE exE conjE)
   3.517 +    assume g0: "raw_has_prod g 0 b"
   3.518 +    with f0 show ?thesis
   3.519 +      by (force simp add: has_prod_def prod.distrib tendsto_mult raw_has_prod_def)
   3.520 +  next
   3.521 +    fix j q
   3.522 +    assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q"
   3.523 +    obtain p where p: "raw_has_prod f (Suc j) p"
   3.524 +      using f0 raw_has_prod_ignore_initial_segment by blast
   3.525 +    then have "Ex (raw_has_prod (\<lambda>n. f n * g n) (Suc j))"
   3.526 +      using q raw_has_prod_mult by blast
   3.527 +    then show ?thesis
   3.528 +      using \<open>b = 0\<close> \<open>g j = 0\<close> has_prod_0_iff by fastforce
   3.529 +  qed
   3.530 +next
   3.531 +  fix i p
   3.532 +  assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p"
   3.533 +  show ?thesis
   3.534 +    using g [unfolded has_prod_def]
   3.535 +  proof (elim disjE exE conjE)
   3.536 +    assume g0: "raw_has_prod g 0 b"
   3.537 +    obtain q where q: "raw_has_prod g (Suc i) q"
   3.538 +      using g0 raw_has_prod_ignore_initial_segment by blast
   3.539 +    then have "Ex (raw_has_prod (\<lambda>n. f n * g n) (Suc i))"
   3.540 +      using raw_has_prod_mult p by blast
   3.541 +    then show ?thesis
   3.542 +      using \<open>a = 0\<close> \<open>f i = 0\<close> has_prod_0_iff by fastforce
   3.543 +  next
   3.544 +    fix j q
   3.545 +    assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q"
   3.546 +    obtain p' where p': "raw_has_prod f (Suc (max i j)) p'"
   3.547 +      by (metis raw_has_prod_ignore_initial_segment max_Suc_Suc max_def p)
   3.548 +    moreover
   3.549 +    obtain q' where q': "raw_has_prod g (Suc (max i j)) q'"
   3.550 +      by (metis raw_has_prod_ignore_initial_segment max.cobounded2 max_Suc_Suc q)
   3.551 +    ultimately show ?thesis
   3.552 +      using \<open>b = 0\<close> by (simp add: has_prod_def) (metis \<open>f i = 0\<close> \<open>g j = 0\<close> raw_has_prod_mult max_def)
   3.553 +  qed
   3.554 +qed
   3.555 +
   3.556 +lemma convergent_prod_mult:
   3.557 +  assumes f: "convergent_prod f" and g: "convergent_prod g"
   3.558 +  shows "convergent_prod (\<lambda>n. f n * g n)"
   3.559 +  unfolding convergent_prod_def
   3.560 +proof -
   3.561 +  obtain M p N q where p: "raw_has_prod f M p" and q: "raw_has_prod g N q"
   3.562 +    using convergent_prod_def f g by blast+
   3.563 +  then obtain p' q' where p': "raw_has_prod f (max M N) p'" and q': "raw_has_prod g (max M N) q'"
   3.564 +    by (meson raw_has_prod_ignore_initial_segment max.cobounded1 max.cobounded2)
   3.565 +  then show "\<exists>M p. raw_has_prod (\<lambda>n. f n * g n) M p"
   3.566 +    using raw_has_prod_mult by blast
   3.567 +qed
   3.568 +
   3.569 +lemma prodinf_mult: "convergent_prod f \<Longrightarrow> convergent_prod g \<Longrightarrow> prodinf f * prodinf g = (\<Prod>n. f n * g n)"
   3.570 +  by (intro has_prod_unique has_prod_mult convergent_prod_has_prod)
   3.571 +
   3.572 +end
   3.573 +
   3.574 +context
   3.575 +  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_field"
   3.576 +    and I :: "'i set"
   3.577 +begin
   3.578 +
   3.579 +lemma has_prod_prod: "(\<And>i. i \<in> I \<Longrightarrow> (f i) has_prod (x i)) \<Longrightarrow> (\<lambda>n. \<Prod>i\<in>I. f i n) has_prod (\<Prod>i\<in>I. x i)"
   3.580 +  by (induct I rule: infinite_finite_induct) (auto intro!: has_prod_mult)
   3.581 +
   3.582 +lemma prodinf_prod: "(\<And>i. i \<in> I \<Longrightarrow> convergent_prod (f i)) \<Longrightarrow> (\<Prod>n. \<Prod>i\<in>I. f i n) = (\<Prod>i\<in>I. \<Prod>n. f i n)"
   3.583 +  using has_prod_unique[OF has_prod_prod, OF convergent_prod_has_prod] by simp
   3.584 +
   3.585 +lemma convergent_prod_prod: "(\<And>i. i \<in> I \<Longrightarrow> convergent_prod (f i)) \<Longrightarrow> convergent_prod (\<lambda>n. \<Prod>i\<in>I. f i n)"
   3.586 +  using convergent_prod_has_prod_iff has_prod_prod prodinf_prod by force
   3.587 +
   3.588 +end
   3.589 +
   3.590 +subsection \<open>Infinite summability on real normed vector spaces\<close>
   3.591 +
   3.592 +context
   3.593 +  fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
   3.594 +begin
   3.595 +
   3.596 +lemma raw_has_prod_Suc_iff: "raw_has_prod f M (a * f M) \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0"
   3.597 +proof -
   3.598 +  have "raw_has_prod f M (a * f M) \<longleftrightarrow> (\<lambda>i. \<Prod>j\<le>Suc i. f (j+M)) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0"
   3.599 +    by (subst LIMSEQ_Suc_iff) (simp add: raw_has_prod_def)
   3.600 +  also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0"
   3.601 +    by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod_atLeast1_atMost_eq lessThan_Suc_atMost)
   3.602 +  also have "\<dots> \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0"
   3.603 +  proof safe
   3.604 +    assume tends: "(\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M" and 0: "a * f M \<noteq> 0"
   3.605 +    with tendsto_divide[OF tends tendsto_const, of "f M"]    
   3.606 +    show "raw_has_prod (\<lambda>n. f (Suc n)) M a"
   3.607 +      by (simp add: raw_has_prod_def)
   3.608 +  qed (auto intro: tendsto_mult_right simp:  raw_has_prod_def)
   3.609 +  finally show ?thesis .
   3.610 +qed
   3.611 +
   3.612 +lemma has_prod_Suc_iff:
   3.613 +  assumes "f 0 \<noteq> 0" shows "(\<lambda>n. f (Suc n)) has_prod a \<longleftrightarrow> f has_prod (a * f 0)"
   3.614 +proof (cases "a = 0")
   3.615 +  case True
   3.616 +  then show ?thesis
   3.617 +  proof (simp add: has_prod_def, safe)
   3.618 +    fix i x
   3.619 +    assume "f (Suc i) = 0" and "raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) x"
   3.620 +    then obtain y where "raw_has_prod f (Suc (Suc i)) y"
   3.621 +      by (metis (no_types) raw_has_prod_eq_0 Suc_n_not_le_n raw_has_prod_Suc_iff raw_has_prod_ignore_initial_segment raw_has_prod_nonzero linear)
   3.622 +    then show "\<exists>i. f i = 0 \<and> Ex (raw_has_prod f (Suc i))"
   3.623 +      using \<open>f (Suc i) = 0\<close> by blast
   3.624 +  next
   3.625 +    fix i x
   3.626 +    assume "f i = 0" and x: "raw_has_prod f (Suc i) x"
   3.627 +    then obtain j where j: "i = Suc j"
   3.628 +      by (metis assms not0_implies_Suc)
   3.629 +    moreover have "\<exists> y. raw_has_prod (\<lambda>n. f (Suc n)) i y"
   3.630 +      using x by (auto simp: raw_has_prod_def)
   3.631 +    then show "\<exists>i. f (Suc i) = 0 \<and> Ex (raw_has_prod (\<lambda>n. f (Suc n)) (Suc i))"
   3.632 +      using \<open>f i = 0\<close> j by blast
   3.633 +  qed
   3.634 +next
   3.635 +  case False
   3.636 +  then show ?thesis
   3.637 +    by (auto simp: has_prod_def raw_has_prod_Suc_iff assms)
   3.638 +qed
   3.639 +
   3.640 +lemma convergent_prod_Suc_iff:
   3.641 +  assumes "\<And>k. f k \<noteq> 0" shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f"
   3.642 +proof
   3.643 +  assume "convergent_prod f"
   3.644 +  then have "f has_prod prodinf f"
   3.645 +    by (rule convergent_prod_has_prod)
   3.646 +  moreover have "prodinf f \<noteq> 0"
   3.647 +    by (simp add: \<open>convergent_prod f\<close> assms prodinf_nonzero)
   3.648 +  ultimately have "(\<lambda>n. f (Suc n)) has_prod (prodinf f * inverse (f 0))"
   3.649 +    by (simp add: has_prod_Suc_iff inverse_eq_divide assms)
   3.650 +  then show "convergent_prod (\<lambda>n. f (Suc n))"
   3.651 +    using has_prod_iff by blast
   3.652 +next
   3.653 +  assume "convergent_prod (\<lambda>n. f (Suc n))"
   3.654 +  then show "convergent_prod f"
   3.655 +    using assms convergent_prod_def raw_has_prod_Suc_iff by blast
   3.656 +qed
   3.657 +
   3.658 +lemma raw_has_prod_inverse: 
   3.659 +  assumes "raw_has_prod f M a" shows "raw_has_prod (\<lambda>n. inverse (f n)) M (inverse a)"
   3.660 +  using assms unfolding raw_has_prod_def by (auto dest: tendsto_inverse simp: prod_inversef [symmetric])
   3.661 +
   3.662 +lemma has_prod_inverse: 
   3.663 +  assumes "f has_prod a" shows "(\<lambda>n. inverse (f n)) has_prod (inverse a)"
   3.664 +using assms raw_has_prod_inverse unfolding has_prod_def by auto 
   3.665 +
   3.666 +lemma convergent_prod_inverse:
   3.667 +  assumes "convergent_prod f" 
   3.668 +  shows "convergent_prod (\<lambda>n. inverse (f n))"
   3.669 +  using assms unfolding convergent_prod_def  by (blast intro: raw_has_prod_inverse elim: )
   3.670 +
   3.671 +end
   3.672 +
   3.673 +context (* Separate contexts are necessary to allow general use of the results above, here. *)
   3.674 +  fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
   3.675 +begin
   3.676 +
   3.677 +lemma raw_has_prod_Suc_iff': "raw_has_prod f M a \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M (a / f M) \<and> f M \<noteq> 0"
   3.678 +  by (metis raw_has_prod_eq_0 add.commute add.left_neutral raw_has_prod_Suc_iff raw_has_prod_nonzero le_add1 nonzero_mult_div_cancel_right times_divide_eq_left)
   3.679 +
   3.680 +lemma has_prod_divide: "f has_prod a \<Longrightarrow> g has_prod b \<Longrightarrow> (\<lambda>n. f n / g n) has_prod (a / b)"
   3.681 +  unfolding divide_inverse by (intro has_prod_inverse has_prod_mult)
   3.682 +
   3.683 +lemma convergent_prod_divide:
   3.684 +  assumes f: "convergent_prod f" and g: "convergent_prod g"
   3.685 +  shows "convergent_prod (\<lambda>n. f n / g n)"
   3.686 +  using f g has_prod_divide has_prod_iff by blast
   3.687 +
   3.688 +lemma prodinf_divide: "convergent_prod f \<Longrightarrow> convergent_prod g \<Longrightarrow> prodinf f / prodinf g = (\<Prod>n. f n / g n)"
   3.689 +  by (intro has_prod_unique has_prod_divide convergent_prod_has_prod)
   3.690 +
   3.691 +lemma prodinf_inverse: "convergent_prod f \<Longrightarrow> (\<Prod>n. inverse (f n)) = inverse (\<Prod>n. f n)"
   3.692 +  by (intro has_prod_unique [symmetric] has_prod_inverse convergent_prod_has_prod)
   3.693 +
   3.694 +lemma has_prod_iff_shift: 
   3.695 +  assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
   3.696 +  shows "(\<lambda>i. f (i + n)) has_prod a \<longleftrightarrow> f has_prod (a * (\<Prod>i<n. f i))"
   3.697 +  using assms
   3.698 +proof (induct n arbitrary: a)
   3.699 +  case 0
   3.700 +  then show ?case by simp
   3.701 +next
   3.702 +  case (Suc n)
   3.703 +  then have "(\<lambda>i. f (Suc i + n)) has_prod a \<longleftrightarrow> (\<lambda>i. f (i + n)) has_prod (a * f n)"
   3.704 +    by (subst has_prod_Suc_iff) auto
   3.705 +  with Suc show ?case
   3.706 +    by (simp add: ac_simps)
   3.707 +qed
   3.708 +
   3.709 +corollary has_prod_iff_shift':
   3.710 +  assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
   3.711 +  shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i)) \<longleftrightarrow> f has_prod a"
   3.712 +  by (simp add: assms has_prod_iff_shift)
   3.713 +
   3.714 +lemma has_prod_one_iff_shift:
   3.715 +  assumes "\<And>i. i < n \<Longrightarrow> f i = 1"
   3.716 +  shows "(\<lambda>i. f (i+n)) has_prod a \<longleftrightarrow> (\<lambda>i. f i) has_prod a"
   3.717 +  by (simp add: assms has_prod_iff_shift)
   3.718 +
   3.719 +lemma convergent_prod_iff_shift:
   3.720 +  shows "convergent_prod (\<lambda>i. f (i + n)) \<longleftrightarrow> convergent_prod f"
   3.721 +  apply safe
   3.722 +  using convergent_prod_offset apply blast
   3.723 +  using convergent_prod_ignore_initial_segment convergent_prod_def by blast
   3.724 +
   3.725 +lemma has_prod_split_initial_segment:
   3.726 +  assumes "f has_prod a" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
   3.727 +  shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i))"
   3.728 +  using assms has_prod_iff_shift' by blast
   3.729 +
   3.730 +lemma prodinf_divide_initial_segment:
   3.731 +  assumes "convergent_prod f" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
   3.732 +  shows "(\<Prod>i. f (i + n)) = (\<Prod>i. f i) / (\<Prod>i<n. f i)"
   3.733 +  by (rule has_prod_unique[symmetric]) (auto simp: assms has_prod_iff_shift)
   3.734 +
   3.735 +lemma prodinf_split_initial_segment:
   3.736 +  assumes "convergent_prod f" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
   3.737 +  shows "prodinf f = (\<Prod>i. f (i + n)) * (\<Prod>i<n. f i)"
   3.738 +  by (auto simp add: assms prodinf_divide_initial_segment)
   3.739 +
   3.740 +lemma prodinf_split_head:
   3.741 +  assumes "convergent_prod f" "f 0 \<noteq> 0"
   3.742 +  shows "(\<Prod>n. f (Suc n)) = prodinf f / f 0"
   3.743 +  using prodinf_split_initial_segment[of 1] assms by simp
   3.744 +
   3.745 +end
   3.746 +
   3.747 +context (* Separate contexts are necessary to allow general use of the results above, here. *)
   3.748 +  fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
   3.749 +begin
   3.750 +
   3.751 +lemma convergent_prod_inverse_iff: "convergent_prod (\<lambda>n. inverse (f n)) \<longleftrightarrow> convergent_prod f"
   3.752 +  by (auto dest: convergent_prod_inverse)
   3.753 +
   3.754 +lemma convergent_prod_const_iff:
   3.755 +  fixes c :: "'a :: {real_normed_field}"
   3.756 +  shows "convergent_prod (\<lambda>_. c) \<longleftrightarrow> c = 1"
   3.757 +proof
   3.758 +  assume "convergent_prod (\<lambda>_. c)"
   3.759 +  then show "c = 1"
   3.760 +    using convergent_prod_imp_LIMSEQ LIMSEQ_unique by blast 
   3.761 +next
   3.762 +  assume "c = 1"
   3.763 +  then show "convergent_prod (\<lambda>_. c)"
   3.764 +    by auto
   3.765 +qed
   3.766 +
   3.767 +lemma has_prod_power: "f has_prod a \<Longrightarrow> (\<lambda>i. f i ^ n) has_prod (a ^ n)"
   3.768 +  by (induction n) (auto simp: has_prod_mult)
   3.769 +
   3.770 +lemma convergent_prod_power: "convergent_prod f \<Longrightarrow> convergent_prod (\<lambda>i. f i ^ n)"
   3.771 +  by (induction n) (auto simp: convergent_prod_mult)
   3.772 +
   3.773 +lemma prodinf_power: "convergent_prod f \<Longrightarrow> prodinf (\<lambda>i. f i ^ n) = prodinf f ^ n"
   3.774 +  by (metis has_prod_unique convergent_prod_imp_has_prod has_prod_power)
   3.775 +
   3.776 +end
   3.777 +
   3.778 +end
     4.1 --- a/src/HOL/Groups_Big.thy	Sat Jun 02 22:57:44 2018 +0100
     4.2 +++ b/src/HOL/Groups_Big.thy	Sun Jun 03 15:22:30 2018 +0100
     4.3 @@ -1302,17 +1302,20 @@
     4.4      by simp
     4.5  qed
     4.6  
     4.7 -lemma (in linordered_semidom) prod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A"
     4.8 +context linordered_semidom
     4.9 +begin
    4.10 +
    4.11 +lemma prod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A"
    4.12    by (induct A rule: infinite_finite_induct) simp_all
    4.13  
    4.14 -lemma (in linordered_semidom) prod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < prod f A"
    4.15 +lemma prod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < prod f A"
    4.16    by (induct A rule: infinite_finite_induct) simp_all
    4.17  
    4.18 -lemma (in linordered_semidom) prod_mono:
    4.19 +lemma prod_mono:
    4.20    "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i \<le> g i) \<Longrightarrow> prod f A \<le> prod g A"
    4.21    by (induct A rule: infinite_finite_induct) (force intro!: prod_nonneg mult_mono)+
    4.22  
    4.23 -lemma (in linordered_semidom) prod_mono_strict:
    4.24 +lemma prod_mono_strict:
    4.25    assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
    4.26    shows "prod f A < prod g A"
    4.27    using assms
    4.28 @@ -1324,6 +1327,42 @@
    4.29    then show ?case by (force intro: mult_strict_mono' prod_nonneg)
    4.30  qed
    4.31  
    4.32 +end
    4.33 +
    4.34 +lemma prod_mono2:
    4.35 +  fixes f :: "'a \<Rightarrow> 'b :: linordered_idom"
    4.36 +  assumes fin: "finite B"
    4.37 +    and sub: "A \<subseteq> B"
    4.38 +    and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 1 \<le> f b"
    4.39 +    and A: "\<And>a. a \<in> A \<Longrightarrow> 0 \<le> f a"
    4.40 +  shows "prod f A \<le> prod f B"
    4.41 +proof -
    4.42 +  have "prod f A \<le> prod f A * prod f (B-A)"
    4.43 +    by (metis prod_ge_1 A mult_le_cancel_left1 nn not_less prod_nonneg)
    4.44 +  also from fin finite_subset[OF sub fin] have "\<dots> = prod f (A \<union> (B-A))"
    4.45 +    by (simp add: prod.union_disjoint del: Un_Diff_cancel)
    4.46 +  also from sub have "A \<union> (B-A) = B" by blast
    4.47 +  finally show ?thesis .
    4.48 +qed
    4.49 +
    4.50 +lemma less_1_prod:
    4.51 +  fixes f :: "'a \<Rightarrow> 'b::linordered_idom"
    4.52 +  shows "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 1 < f i) \<Longrightarrow> 1 < prod f I"
    4.53 +  by (induct I rule: finite_ne_induct) (auto intro: less_1_mult)
    4.54 +
    4.55 +lemma less_1_prod2:
    4.56 +  fixes f :: "'a \<Rightarrow> 'b::linordered_idom"
    4.57 +  assumes I: "finite I" "i \<in> I" "1 < f i" "\<And>i. i \<in> I \<Longrightarrow> 1 \<le> f i"
    4.58 +  shows "1 < prod f I"
    4.59 +proof -
    4.60 +  have "1 < f i * prod f (I - {i})"
    4.61 +    using assms
    4.62 +    by (meson DiffD1 leI less_1_mult less_le_trans mult_le_cancel_left1 prod_ge_1)
    4.63 +  also have "\<dots> = prod f I"
    4.64 +    using assms by (simp add: prod.remove)
    4.65 +  finally show ?thesis .
    4.66 +qed
    4.67 +
    4.68  lemma (in linordered_field) abs_prod: "\<bar>prod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
    4.69    by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
    4.70  
     5.1 --- a/src/HOL/Set_Interval.thy	Sat Jun 02 22:57:44 2018 +0100
     5.2 +++ b/src/HOL/Set_Interval.thy	Sun Jun 03 15:22:30 2018 +0100
     5.3 @@ -507,7 +507,7 @@
     5.4  lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \<longleftrightarrow> n = bot"
     5.5    by (auto simp: set_eq_iff not_less le_bot)
     5.6  
     5.7 -lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
     5.8 +lemma lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
     5.9    by (simp add: Iio_eq_empty_iff bot_nat_def)
    5.10  
    5.11  lemma mono_image_least:
    5.12 @@ -709,7 +709,7 @@
    5.13  lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
    5.14  by (simp add: lessThan_def atMost_def less_Suc_eq_le)
    5.15  
    5.16 -lemma Iic_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})"
    5.17 +lemma atMost_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})"
    5.18    unfolding lessThan_Suc_atMost[symmetric] lessThan_Suc_eq_insert_0[of "Suc n"] ..
    5.19  
    5.20  lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
    5.21 @@ -803,7 +803,7 @@
    5.22  
    5.23  lemma atLeast0_atMost_Suc_eq_insert_0:
    5.24    "{0..Suc n} = insert 0 (Suc ` {0..n})"
    5.25 -  by (simp add: atLeast0AtMost Iic_Suc_eq_insert_0)
    5.26 +  by (simp add: atLeast0AtMost atMost_Suc_eq_insert_0)
    5.27  
    5.28  
    5.29  subsubsection \<open>Intervals of nats with @{term Suc}\<close>
    5.30 @@ -2408,6 +2408,16 @@
    5.31    "\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..n}"
    5.32    "\<Prod>i<n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..<n}"
    5.33  
    5.34 +lemma prod_atLeast1_atMost_eq:
    5.35 +  "prod f {Suc 0..n} = (\<Prod>k<n. f (Suc k))"
    5.36 +proof -
    5.37 +  have "prod f {Suc 0..n} = prod f (Suc ` {..<n})"
    5.38 +    by (simp add: image_Suc_lessThan)
    5.39 +  also have "\<dots> = (\<Prod>k<n. f (Suc k))"
    5.40 +    by (simp add: prod.reindex)
    5.41 +  finally show ?thesis .
    5.42 +qed
    5.43 +
    5.44  lemma prod_int_plus_eq: "prod int {i..i+j} =  \<Prod>{int i..int (i+j)}"
    5.45    by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)
    5.46  
    5.47 @@ -2441,7 +2451,7 @@
    5.48    "prod f {Suc m..<Suc n} = prod (%i. f(Suc i)){m..<n}"
    5.49  by (simp add:prod_shift_bounds_nat_ivl[where k="Suc 0", simplified])
    5.50  
    5.51 -lemma prod_lessThan_Suc: "prod f {..<Suc n} = prod f {..<n} * f n"
    5.52 +lemma prod_lessThan_Suc [simp]: "prod f {..<Suc n} = prod f {..<n} * f n"
    5.53    by (simp add: lessThan_Suc mult.commute)
    5.54  
    5.55  lemma prod_lessThan_Suc_shift:"(\<Prod>i<Suc n. f i) = f 0 * (\<Prod>i<n. f (Suc i))"
     6.1 --- a/src/HOL/Topological_Spaces.thy	Sat Jun 02 22:57:44 2018 +0100
     6.2 +++ b/src/HOL/Topological_Spaces.thy	Sun Jun 03 15:22:30 2018 +0100
     6.3 @@ -1353,6 +1353,12 @@
     6.4  lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l = f \<longlonglongrightarrow> l"
     6.5    by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
     6.6  
     6.7 +lemma LIMSEQ_lessThan_iff_atMost:
     6.8 +  shows "(\<lambda>n. f {..<n}) \<longlonglongrightarrow> x \<longleftrightarrow> (\<lambda>n. f {..n}) \<longlonglongrightarrow> x"
     6.9 +  apply (subst LIMSEQ_Suc_iff [symmetric])
    6.10 +  apply (simp only: lessThan_Suc_atMost)
    6.11 +  done
    6.12 +
    6.13  lemma LIMSEQ_unique: "X \<longlonglongrightarrow> a \<Longrightarrow> X \<longlonglongrightarrow> b \<Longrightarrow> a = b"
    6.14    for a b :: "'a::t2_space"
    6.15    using trivial_limit_sequentially by (rule tendsto_unique)