src/HOL/Analysis/Infinite_Set_Sum.thy
changeset 67167 88d1c9d86f48
parent 66568 52b5cf533fd6
child 67268 bdf25939a550
     1.1 --- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Mon Dec 11 17:28:32 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Tue Dec 12 10:01:14 2017 +0100
     1.3 @@ -256,6 +256,27 @@
     1.4      show "f abs_summable_on insert x A" by simp
     1.5  qed
     1.6  
     1.7 +lemma abs_summable_sum: 
     1.8 +  assumes "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B"
     1.9 +  shows   "(\<lambda>y. \<Sum>x\<in>A. f x y) abs_summable_on B"
    1.10 +  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_sum)
    1.11 +
    1.12 +lemma abs_summable_Re: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. Re (f x)) abs_summable_on A"
    1.13 +  by (simp add: abs_summable_on_def)
    1.14 +
    1.15 +lemma abs_summable_Im: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. Im (f x)) abs_summable_on A"
    1.16 +  by (simp add: abs_summable_on_def)
    1.17 +
    1.18 +lemma abs_summable_on_finite_diff:
    1.19 +  assumes "f abs_summable_on A" "A \<subseteq> B" "finite (B - A)"
    1.20 +  shows   "f abs_summable_on B"
    1.21 +proof -
    1.22 +  have "f abs_summable_on (A \<union> (B - A))"
    1.23 +    by (intro abs_summable_on_union assms abs_summable_on_finite)
    1.24 +  also from assms have "A \<union> (B - A) = B" by blast
    1.25 +  finally show ?thesis .
    1.26 +qed
    1.27 +
    1.28  lemma abs_summable_on_reindex_bij_betw:
    1.29    assumes "bij_betw g A B"
    1.30    shows   "(\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on B"
    1.31 @@ -407,6 +428,27 @@
    1.32  lemma infsetsum_all_0: "(\<And>x. x \<in> A \<Longrightarrow> f x = 0) \<Longrightarrow> infsetsum f A = 0"
    1.33    by simp
    1.34  
    1.35 +lemma infsetsum_nonneg: "(\<And>x. x \<in> A \<Longrightarrow> f x \<ge> (0::real)) \<Longrightarrow> infsetsum f A \<ge> 0"
    1.36 +  unfolding infsetsum_def by (rule Bochner_Integration.integral_nonneg) auto
    1.37 +
    1.38 +lemma sum_infsetsum:
    1.39 +  assumes "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B"
    1.40 +  shows   "(\<Sum>x\<in>A. \<Sum>\<^sub>ay\<in>B. f x y) = (\<Sum>\<^sub>ay\<in>B. \<Sum>x\<in>A. f x y)"
    1.41 +  using assms by (simp add: infsetsum_def abs_summable_on_def Bochner_Integration.integral_sum)
    1.42 +
    1.43 +lemma Re_infsetsum: "f abs_summable_on A \<Longrightarrow> Re (infsetsum f A) = (\<Sum>\<^sub>ax\<in>A. Re (f x))"
    1.44 +  by (simp add: infsetsum_def abs_summable_on_def)
    1.45 +
    1.46 +lemma Im_infsetsum: "f abs_summable_on A \<Longrightarrow> Im (infsetsum f A) = (\<Sum>\<^sub>ax\<in>A. Im (f x))"
    1.47 +  by (simp add: infsetsum_def abs_summable_on_def)
    1.48 +
    1.49 +lemma infsetsum_of_real: 
    1.50 +  shows "infsetsum (\<lambda>x. of_real (f x) 
    1.51 +           :: 'a :: {real_normed_algebra_1,banach,second_countable_topology,real_inner}) A = 
    1.52 +             of_real (infsetsum f A)"
    1.53 +  unfolding infsetsum_def
    1.54 +  by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_inner_left[of 1]]) auto
    1.55 +
    1.56  lemma infsetsum_finite [simp]: "finite A \<Longrightarrow> infsetsum f A = (\<Sum>x\<in>A. f x)"
    1.57    by (simp add: infsetsum_def lebesgue_integral_count_space_finite)
    1.58