src/HOL/Limits.thy
changeset 62368 106569399cd6
parent 62101 26c0a70f78a3
child 62369 acfc4ad7b76a
     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 -