add type class for topological monoids
authorhoelzl
Mon Feb 08 19:53:49 2016 +0100 (2016-02-08)
changeset 62368106569399cd6
parent 62367 d2bc8a7e5fec
child 62369 acfc4ad7b76a
add type class for topological monoids
src/HOL/Limits.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Series.thy
     1.1 --- a/src/HOL/Limits.thy	Mon Feb 08 17:18:13 2016 +0100
     1.2 +++ b/src/HOL/Limits.thy	Mon Feb 08 19:53:49 2016 +0100
     1.3 @@ -573,28 +573,64 @@
     1.4    "((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> (0::real)) F \<longleftrightarrow> (f \<longlongrightarrow> 0) F"
     1.5    by (fold real_norm_def, rule tendsto_norm_zero_iff)
     1.6  
     1.7 -subsubsection \<open>Addition and subtraction\<close>
     1.8 +subsection \<open>Topological Monoid\<close>
     1.9 +
    1.10 +class topological_monoid_add = topological_space + monoid_add +
    1.11 +  assumes tendsto_add_Pair: "LIM x (nhds a \<times>\<^sub>F nhds b). fst x + snd x :> nhds (a + b)"
    1.12 +
    1.13 +class topological_comm_monoid_add = topological_monoid_add + comm_monoid_add
    1.14  
    1.15  lemma tendsto_add [tendsto_intros]:
    1.16 -  fixes a b :: "'a::real_normed_vector"
    1.17 -  shows "\<lbrakk>(f \<longlongrightarrow> a) F; (g \<longlongrightarrow> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> a + b) F"
    1.18 -  by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
    1.19 +  fixes a b :: "'a::topological_monoid_add"
    1.20 +  shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> a + b) F"
    1.21 +  using filterlim_compose[OF tendsto_add_Pair, of "\<lambda>x. (f x, g x)" a b F]
    1.22 +  by (simp add: nhds_prod[symmetric] tendsto_Pair)
    1.23  
    1.24  lemma continuous_add [continuous_intros]:
    1.25 -  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    1.26 +  fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add"
    1.27    shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
    1.28    unfolding continuous_def by (rule tendsto_add)
    1.29  
    1.30  lemma continuous_on_add [continuous_intros]:
    1.31 -  fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
    1.32 +  fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add"
    1.33    shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
    1.34    unfolding continuous_on_def by (auto intro: tendsto_add)
    1.35  
    1.36  lemma tendsto_add_zero:
    1.37 -  fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
    1.38 +  fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add"
    1.39    shows "\<lbrakk>(f \<longlongrightarrow> 0) F; (g \<longlongrightarrow> 0) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> 0) F"
    1.40    by (drule (1) tendsto_add, simp)
    1.41  
    1.42 +lemma tendsto_setsum [tendsto_intros]:
    1.43 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add"
    1.44 +  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
    1.45 +  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) \<longlongrightarrow> (\<Sum>i\<in>S. a i)) F"
    1.46 +proof (cases "finite S")
    1.47 +  assume "finite S" thus ?thesis using assms
    1.48 +    by (induct, simp, simp add: tendsto_add)
    1.49 +qed simp
    1.50 +
    1.51 +lemma continuous_setsum [continuous_intros]:
    1.52 +  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add"
    1.53 +  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
    1.54 +  unfolding continuous_def by (rule tendsto_setsum)
    1.55 +
    1.56 +lemma continuous_on_setsum [continuous_intros]:
    1.57 +  fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::topological_comm_monoid_add"
    1.58 +  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Sum>i\<in>S. f i x)"
    1.59 +  unfolding continuous_on_def by (auto intro: tendsto_setsum)
    1.60 +
    1.61 +subsubsection \<open>Addition and subtraction\<close>
    1.62 +
    1.63 +instance real_normed_vector < topological_comm_monoid_add
    1.64 +proof
    1.65 +  fix a b :: 'a show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)"
    1.66 +    unfolding tendsto_Zfun_iff add_diff_add
    1.67 +    using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"]
    1.68 +    by (intro Zfun_add)
    1.69 +       (auto simp add: tendsto_Zfun_iff[symmetric] nhds_prod[symmetric] intro!: tendsto_fst)
    1.70 +qed
    1.71 +
    1.72  lemma tendsto_minus [tendsto_intros]:
    1.73    fixes a :: "'a::real_normed_vector"
    1.74    shows "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. - f x) \<longlongrightarrow> - a) F"
    1.75 @@ -638,25 +674,6 @@
    1.76  lemma continuous_on_op_minus: "continuous_on (s::'a::real_normed_vector set) (op - x)"
    1.77    by (rule continuous_intros | simp)+
    1.78  
    1.79 -lemma tendsto_setsum [tendsto_intros]:
    1.80 -  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
    1.81 -  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
    1.82 -  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) \<longlongrightarrow> (\<Sum>i\<in>S. a i)) F"
    1.83 -proof (cases "finite S")
    1.84 -  assume "finite S" thus ?thesis using assms
    1.85 -    by (induct, simp, simp add: tendsto_add)
    1.86 -qed simp
    1.87 -
    1.88 -lemma continuous_setsum [continuous_intros]:
    1.89 -  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
    1.90 -  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
    1.91 -  unfolding continuous_def by (rule tendsto_setsum)
    1.92 -
    1.93 -lemma continuous_on_setsum [continuous_intros]:
    1.94 -  fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::real_normed_vector"
    1.95 -  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Sum>i\<in>S. f i x)"
    1.96 -  unfolding continuous_on_def by (auto intro: tendsto_setsum)
    1.97 -
    1.98  lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
    1.99  
   1.100  subsubsection \<open>Linear operators and multiplication\<close>
   1.101 @@ -1468,7 +1485,7 @@
   1.102  
   1.103  subsection \<open>Limits of Sequences\<close>
   1.104  
   1.105 -lemma [trans]: "X=Y ==> Y \<longlonglongrightarrow> z ==> X \<longlonglongrightarrow> z"
   1.106 +lemma [trans]: "X = Y \<Longrightarrow> Y \<longlonglongrightarrow> z \<Longrightarrow> X \<longlonglongrightarrow> z"
   1.107    by simp
   1.108  
   1.109  lemma LIMSEQ_iff:
   1.110 @@ -2042,7 +2059,7 @@
   1.111    by (fact continuous_rabs)
   1.112  
   1.113  lemma isCont_add [simp]:
   1.114 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   1.115 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::topological_monoid_add"
   1.116    shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
   1.117    by (fact continuous_add)
   1.118  
   1.119 @@ -2081,7 +2098,7 @@
   1.120    by (fact continuous_power)
   1.121  
   1.122  lemma isCont_setsum [simp]:
   1.123 -  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
   1.124 +  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add"
   1.125    shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   1.126    by (auto intro: continuous_setsum)
   1.127  
   1.128 @@ -2401,4 +2418,3 @@
   1.129    using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp add: neq_iff)
   1.130  
   1.131  end
   1.132 -
     2.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Feb 08 17:18:13 2016 +0100
     2.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Feb 08 19:53:49 2016 +0100
     2.3 @@ -2143,4 +2143,3 @@
     2.4  qed
     2.5  
     2.6  end
     2.7 -
     3.1 --- a/src/HOL/Series.thy	Mon Feb 08 17:18:13 2016 +0100
     3.2 +++ b/src/HOL/Series.thy	Mon Feb 08 19:53:49 2016 +0100
     3.3 @@ -271,12 +271,59 @@
     3.4        by (auto intro: le_less_trans simp: eventually_sequentially) }
     3.5  qed
     3.6  
     3.7 +subsection \<open>Infinite summability on topological monoids\<close>
     3.8 +
     3.9 +lemma Zero_notin_Suc: "0 \<notin> Suc ` A"
    3.10 +  by auto
    3.11 +
    3.12 +context
    3.13 +  fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
    3.14 +begin
    3.15 +
    3.16 +lemma sums_Suc:
    3.17 +  assumes "(\<lambda>n. f (Suc n)) sums l" shows "f sums (l + f 0)"
    3.18 +proof  -
    3.19 +  have "(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0"
    3.20 +    using assms by (auto intro!: tendsto_add simp: sums_def)
    3.21 +  moreover have "(\<Sum>i<n. f (Suc i)) + f 0 = (\<Sum>i<Suc n. f i)" for n
    3.22 +    unfolding lessThan_Suc_eq_insert_0 by (simp add: Zero_notin_Suc ac_simps setsum.reindex)
    3.23 +  ultimately show ?thesis
    3.24 +    by (auto simp add: sums_def simp del: setsum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
    3.25 +qed
    3.26 +
    3.27 +lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
    3.28 +  unfolding sums_def by (simp add: setsum.distrib tendsto_add)
    3.29 +
    3.30 +lemma summable_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n + g n)"
    3.31 +  unfolding summable_def by (auto intro: sums_add)
    3.32 +
    3.33 +lemma suminf_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f + suminf g = (\<Sum>n. f n + g n)"
    3.34 +  by (intro sums_unique sums_add summable_sums)
    3.35 +
    3.36 +end
    3.37 +
    3.38 +context
    3.39 +  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{t2_space, topological_comm_monoid_add}" and I :: "'i set"
    3.40 +begin
    3.41 +
    3.42 +lemma sums_setsum: "(\<And>i. i \<in> I \<Longrightarrow> (f i) sums (x i)) \<Longrightarrow> (\<lambda>n. \<Sum>i\<in>I. f i n) sums (\<Sum>i\<in>I. x i)"
    3.43 +  by (induct I rule: infinite_finite_induct) (auto intro!: sums_add)
    3.44 +
    3.45 +lemma suminf_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> (\<Sum>n. \<Sum>i\<in>I. f i n) = (\<Sum>i\<in>I. \<Sum>n. f i n)"
    3.46 +  using sums_unique[OF sums_setsum, OF summable_sums] by simp
    3.47 +
    3.48 +lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
    3.49 +  using sums_summable[OF sums_setsum[OF summable_sums]] .
    3.50 +
    3.51 +end
    3.52  
    3.53  subsection \<open>Infinite summability on real normed vector spaces\<close>
    3.54  
    3.55 -lemma sums_Suc_iff:
    3.56 +context
    3.57    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    3.58 -  shows "(\<lambda>n. f (Suc n)) sums s \<longleftrightarrow> f sums (s + f 0)"
    3.59 +begin
    3.60 +
    3.61 +lemma sums_Suc_iff: "(\<lambda>n. f (Suc n)) sums s \<longleftrightarrow> f sums (s + f 0)"
    3.62  proof -
    3.63    have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) \<longlonglongrightarrow> s + f 0"
    3.64      by (subst LIMSEQ_Suc_iff) (simp add: sums_def)
    3.65 @@ -292,7 +339,7 @@
    3.66    finally show ?thesis ..
    3.67  qed
    3.68  
    3.69 -lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n) :: 'a :: real_normed_vector) = summable f"
    3.70 +lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n)) = summable f"
    3.71  proof
    3.72    assume "summable f"
    3.73    hence "f sums suminf f" by (rule summable_sums)
    3.74 @@ -300,19 +347,12 @@
    3.75    thus "summable (\<lambda>n. f (Suc n))" unfolding summable_def by blast
    3.76  qed (auto simp: sums_Suc_iff summable_def)
    3.77  
    3.78 +end
    3.79 +
    3.80  context
    3.81    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    3.82  begin
    3.83  
    3.84 -lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
    3.85 -  unfolding sums_def by (simp add: setsum.distrib tendsto_add)
    3.86 -
    3.87 -lemma summable_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n + g n)"
    3.88 -  unfolding summable_def by (auto intro: sums_add)
    3.89 -
    3.90 -lemma suminf_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f + suminf g = (\<Sum>n. f n + g n)"
    3.91 -  by (intro sums_unique sums_add summable_sums)
    3.92 -
    3.93  lemma sums_diff: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n - g n) sums (a - b)"
    3.94    unfolding sums_def by (simp add: setsum_subtractf tendsto_diff)
    3.95  
    3.96 @@ -331,9 +371,6 @@
    3.97  lemma suminf_minus: "summable f \<Longrightarrow> (\<Sum>n. - f n) = - (\<Sum>n. f n)"
    3.98    by (intro sums_unique [symmetric] sums_minus summable_sums)
    3.99  
   3.100 -lemma sums_Suc: "(\<lambda> n. f (Suc n)) sums l \<Longrightarrow> f sums (l + f 0)"
   3.101 -  by (simp add: sums_Suc_iff)
   3.102 -
   3.103  lemma sums_iff_shift: "(\<lambda>i. f (i + n)) sums s \<longleftrightarrow> f sums (s + (\<Sum>i<n. f i))"
   3.104  proof (induct n arbitrary: s)
   3.105    case (Suc n)
   3.106 @@ -381,12 +418,10 @@
   3.107    apply (drule_tac x="n" in spec, simp)
   3.108    done
   3.109  
   3.110 -lemma summable_imp_convergent:
   3.111 -  "summable (f :: nat \<Rightarrow> 'a) \<Longrightarrow> convergent f"
   3.112 +lemma summable_imp_convergent: "summable f \<Longrightarrow> convergent f"
   3.113    by (force dest!: summable_LIMSEQ_zero simp: convergent_def)
   3.114  
   3.115 -lemma summable_imp_Bseq:
   3.116 -  "summable f \<Longrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
   3.117 +lemma summable_imp_Bseq: "summable f \<Longrightarrow> Bseq f"
   3.118    by (simp add: convergent_imp_Bseq summable_imp_convergent)
   3.119  
   3.120  end
   3.121 @@ -396,22 +431,6 @@
   3.122    shows "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
   3.123    by (auto dest: summable_minus) \<comment>\<open>used two ways, hence must be outside the context above\<close>
   3.124  
   3.125 -
   3.126 -context
   3.127 -  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_vector" and I :: "'i set"
   3.128 -begin
   3.129 -
   3.130 -lemma sums_setsum: "(\<And>i. i \<in> I \<Longrightarrow> (f i) sums (x i)) \<Longrightarrow> (\<lambda>n. \<Sum>i\<in>I. f i n) sums (\<Sum>i\<in>I. x i)"
   3.131 -  by (induct I rule: infinite_finite_induct) (auto intro!: sums_add)
   3.132 -
   3.133 -lemma suminf_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> (\<Sum>n. \<Sum>i\<in>I. f i n) = (\<Sum>i\<in>I. \<Sum>n. f i n)"
   3.134 -  using sums_unique[OF sums_setsum, OF summable_sums] by simp
   3.135 -
   3.136 -lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
   3.137 -  using sums_summable[OF sums_setsum[OF summable_sums]] .
   3.138 -
   3.139 -end
   3.140 -
   3.141  lemma (in bounded_linear) sums: "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
   3.142    unfolding sums_def by (drule tendsto, simp only: setsum)
   3.143  
   3.144 @@ -923,7 +942,7 @@
   3.145     fixes f :: "nat \<Rightarrow> real"
   3.146     assumes "summable f"
   3.147     and "inj g"
   3.148 -   and pos: "!!x. 0 \<le> f x"
   3.149 +   and pos: "\<And>x. 0 \<le> f x"
   3.150     shows summable_reindex: "summable (f o g)"
   3.151     and suminf_reindex_mono: "suminf (f o g) \<le> suminf f"
   3.152     and suminf_reindex: "(\<And>x. x \<notin> range g \<Longrightarrow> f x = 0) \<Longrightarrow> suminf (f \<circ> g) = suminf f"