--- a/src/HOL/Limits.thy Mon Feb 08 17:18:13 2016 +0100
+++ b/src/HOL/Limits.thy Mon Feb 08 19:53:49 2016 +0100
@@ -573,28 +573,64 @@
"((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> (0::real)) F \<longleftrightarrow> (f \<longlongrightarrow> 0) F"
by (fold real_norm_def, rule tendsto_norm_zero_iff)
-subsubsection \<open>Addition and subtraction\<close>
+subsection \<open>Topological Monoid\<close>
+
+class topological_monoid_add = topological_space + monoid_add +
+ assumes tendsto_add_Pair: "LIM x (nhds a \<times>\<^sub>F nhds b). fst x + snd x :> nhds (a + b)"
+
+class topological_comm_monoid_add = topological_monoid_add + comm_monoid_add
lemma tendsto_add [tendsto_intros]:
- fixes a b :: "'a::real_normed_vector"
- shows "\<lbrakk>(f \<longlongrightarrow> a) F; (g \<longlongrightarrow> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> a + b) F"
- by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
+ fixes a b :: "'a::topological_monoid_add"
+ shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> a + b) F"
+ using filterlim_compose[OF tendsto_add_Pair, of "\<lambda>x. (f x, g x)" a b F]
+ by (simp add: nhds_prod[symmetric] tendsto_Pair)
lemma continuous_add [continuous_intros]:
- fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add"
shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
unfolding continuous_def by (rule tendsto_add)
lemma continuous_on_add [continuous_intros]:
- fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add"
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
unfolding continuous_on_def by (auto intro: tendsto_add)
lemma tendsto_add_zero:
- fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add"
shows "\<lbrakk>(f \<longlongrightarrow> 0) F; (g \<longlongrightarrow> 0) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> 0) F"
by (drule (1) tendsto_add, simp)
+lemma tendsto_setsum [tendsto_intros]:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add"
+ assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
+ shows "((\<lambda>x. \<Sum>i\<in>S. f i x) \<longlongrightarrow> (\<Sum>i\<in>S. a i)) F"
+proof (cases "finite S")
+ assume "finite S" thus ?thesis using assms
+ by (induct, simp, simp add: tendsto_add)
+qed simp
+
+lemma continuous_setsum [continuous_intros]:
+ fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add"
+ shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
+ unfolding continuous_def by (rule tendsto_setsum)
+
+lemma continuous_on_setsum [continuous_intros]:
+ fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::topological_comm_monoid_add"
+ 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)"
+ unfolding continuous_on_def by (auto intro: tendsto_setsum)
+
+subsubsection \<open>Addition and subtraction\<close>
+
+instance real_normed_vector < topological_comm_monoid_add
+proof
+ fix a b :: 'a show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)"
+ unfolding tendsto_Zfun_iff add_diff_add
+ using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"]
+ by (intro Zfun_add)
+ (auto simp add: tendsto_Zfun_iff[symmetric] nhds_prod[symmetric] intro!: tendsto_fst)
+qed
+
lemma tendsto_minus [tendsto_intros]:
fixes a :: "'a::real_normed_vector"
shows "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. - f x) \<longlongrightarrow> - a) F"
@@ -638,25 +674,6 @@
lemma continuous_on_op_minus: "continuous_on (s::'a::real_normed_vector set) (op - x)"
by (rule continuous_intros | simp)+
-lemma tendsto_setsum [tendsto_intros]:
- fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
- assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
- shows "((\<lambda>x. \<Sum>i\<in>S. f i x) \<longlongrightarrow> (\<Sum>i\<in>S. a i)) F"
-proof (cases "finite S")
- assume "finite S" thus ?thesis using assms
- by (induct, simp, simp add: tendsto_add)
-qed simp
-
-lemma continuous_setsum [continuous_intros]:
- fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
- shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
- unfolding continuous_def by (rule tendsto_setsum)
-
-lemma continuous_on_setsum [continuous_intros]:
- fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::real_normed_vector"
- 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)"
- unfolding continuous_on_def by (auto intro: tendsto_setsum)
-
lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
subsubsection \<open>Linear operators and multiplication\<close>
@@ -1468,7 +1485,7 @@
subsection \<open>Limits of Sequences\<close>
-lemma [trans]: "X=Y ==> Y \<longlonglongrightarrow> z ==> X \<longlonglongrightarrow> z"
+lemma [trans]: "X = Y \<Longrightarrow> Y \<longlonglongrightarrow> z \<Longrightarrow> X \<longlonglongrightarrow> z"
by simp
lemma LIMSEQ_iff:
@@ -2042,7 +2059,7 @@
by (fact continuous_rabs)
lemma isCont_add [simp]:
- fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::topological_monoid_add"
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
by (fact continuous_add)
@@ -2081,7 +2098,7 @@
by (fact continuous_power)
lemma isCont_setsum [simp]:
- fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
+ fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add"
shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
by (auto intro: continuous_setsum)
@@ -2401,4 +2418,3 @@
using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp add: neq_iff)
end
-
--- a/src/HOL/Real_Vector_Spaces.thy Mon Feb 08 17:18:13 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Mon Feb 08 19:53:49 2016 +0100
@@ -2143,4 +2143,3 @@
qed
end
-
--- a/src/HOL/Series.thy Mon Feb 08 17:18:13 2016 +0100
+++ b/src/HOL/Series.thy Mon Feb 08 19:53:49 2016 +0100
@@ -271,12 +271,59 @@
by (auto intro: le_less_trans simp: eventually_sequentially) }
qed
+subsection \<open>Infinite summability on topological monoids\<close>
+
+lemma Zero_notin_Suc: "0 \<notin> Suc ` A"
+ by auto
+
+context
+ fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
+begin
+
+lemma sums_Suc:
+ assumes "(\<lambda>n. f (Suc n)) sums l" shows "f sums (l + f 0)"
+proof -
+ have "(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0"
+ using assms by (auto intro!: tendsto_add simp: sums_def)
+ moreover have "(\<Sum>i<n. f (Suc i)) + f 0 = (\<Sum>i<Suc n. f i)" for n
+ unfolding lessThan_Suc_eq_insert_0 by (simp add: Zero_notin_Suc ac_simps setsum.reindex)
+ ultimately show ?thesis
+ by (auto simp add: sums_def simp del: setsum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
+qed
+
+lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
+ unfolding sums_def by (simp add: setsum.distrib tendsto_add)
+
+lemma summable_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n + g n)"
+ unfolding summable_def by (auto intro: sums_add)
+
+lemma suminf_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f + suminf g = (\<Sum>n. f n + g n)"
+ by (intro sums_unique sums_add summable_sums)
+
+end
+
+context
+ fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{t2_space, topological_comm_monoid_add}" and I :: "'i set"
+begin
+
+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)"
+ by (induct I rule: infinite_finite_induct) (auto intro!: sums_add)
+
+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)"
+ using sums_unique[OF sums_setsum, OF summable_sums] by simp
+
+lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
+ using sums_summable[OF sums_setsum[OF summable_sums]] .
+
+end
subsection \<open>Infinite summability on real normed vector spaces\<close>
-lemma sums_Suc_iff:
+context
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
- shows "(\<lambda>n. f (Suc n)) sums s \<longleftrightarrow> f sums (s + f 0)"
+begin
+
+lemma sums_Suc_iff: "(\<lambda>n. f (Suc n)) sums s \<longleftrightarrow> f sums (s + f 0)"
proof -
have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) \<longlonglongrightarrow> s + f 0"
by (subst LIMSEQ_Suc_iff) (simp add: sums_def)
@@ -292,7 +339,7 @@
finally show ?thesis ..
qed
-lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n) :: 'a :: real_normed_vector) = summable f"
+lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n)) = summable f"
proof
assume "summable f"
hence "f sums suminf f" by (rule summable_sums)
@@ -300,19 +347,12 @@
thus "summable (\<lambda>n. f (Suc n))" unfolding summable_def by blast
qed (auto simp: sums_Suc_iff summable_def)
+end
+
context
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
begin
-lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
- unfolding sums_def by (simp add: setsum.distrib tendsto_add)
-
-lemma summable_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n + g n)"
- unfolding summable_def by (auto intro: sums_add)
-
-lemma suminf_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f + suminf g = (\<Sum>n. f n + g n)"
- by (intro sums_unique sums_add summable_sums)
-
lemma sums_diff: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n - g n) sums (a - b)"
unfolding sums_def by (simp add: setsum_subtractf tendsto_diff)
@@ -331,9 +371,6 @@
lemma suminf_minus: "summable f \<Longrightarrow> (\<Sum>n. - f n) = - (\<Sum>n. f n)"
by (intro sums_unique [symmetric] sums_minus summable_sums)
-lemma sums_Suc: "(\<lambda> n. f (Suc n)) sums l \<Longrightarrow> f sums (l + f 0)"
- by (simp add: sums_Suc_iff)
-
lemma sums_iff_shift: "(\<lambda>i. f (i + n)) sums s \<longleftrightarrow> f sums (s + (\<Sum>i<n. f i))"
proof (induct n arbitrary: s)
case (Suc n)
@@ -381,12 +418,10 @@
apply (drule_tac x="n" in spec, simp)
done
-lemma summable_imp_convergent:
- "summable (f :: nat \<Rightarrow> 'a) \<Longrightarrow> convergent f"
+lemma summable_imp_convergent: "summable f \<Longrightarrow> convergent f"
by (force dest!: summable_LIMSEQ_zero simp: convergent_def)
-lemma summable_imp_Bseq:
- "summable f \<Longrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
+lemma summable_imp_Bseq: "summable f \<Longrightarrow> Bseq f"
by (simp add: convergent_imp_Bseq summable_imp_convergent)
end
@@ -396,22 +431,6 @@
shows "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
by (auto dest: summable_minus) \<comment>\<open>used two ways, hence must be outside the context above\<close>
-
-context
- fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_vector" and I :: "'i set"
-begin
-
-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)"
- by (induct I rule: infinite_finite_induct) (auto intro!: sums_add)
-
-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)"
- using sums_unique[OF sums_setsum, OF summable_sums] by simp
-
-lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
- using sums_summable[OF sums_setsum[OF summable_sums]] .
-
-end
-
lemma (in bounded_linear) sums: "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
unfolding sums_def by (drule tendsto, simp only: setsum)
@@ -923,7 +942,7 @@
fixes f :: "nat \<Rightarrow> real"
assumes "summable f"
and "inj g"
- and pos: "!!x. 0 \<le> f x"
+ and pos: "\<And>x. 0 \<le> f x"
shows summable_reindex: "summable (f o g)"
and suminf_reindex_mono: "suminf (f o g) \<le> suminf f"
and suminf_reindex: "(\<And>x. x \<notin> range g \<Longrightarrow> f x = 0) \<Longrightarrow> suminf (f \<circ> g) = suminf f"