# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1503766720 -7200
# Node ID 322120e880c592b244e4b152f7b36e5801a2ea2c
# Parent  4585bfd1907452582ea44e552f441ce6294e65e9
More material on infinite sums

diff -r 4585bfd19074 -r 322120e880c5 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Sun Aug 27 16:17:44 2017 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Sat Aug 26 18:58:40 2017 +0200
@@ -2697,6 +2697,75 @@
 
 subsubsection \<open>Integral form\<close>
 
+lemma integrable_on_powr_from_0':
+  assumes a: "a > (-1::real)" and c: "c \<ge> 0"
+  shows   "(\<lambda>x. x powr a) integrable_on {0<..c}"
+proof -
+  from c have *: "{0<..c} - {0..c} = {}" "{0..c} - {0<..c} = {0}" by auto
+  show ?thesis
+  by (rule integrable_spike_set [OF integrable_on_powr_from_0[OF a c]]) (simp_all add: *)
+qed
+
+lemma absolutely_integrable_Gamma_integral:
+  assumes "Re z > 0" "a > 0"
+  shows   "(\<lambda>t. complex_of_real t powr (z - 1) / of_real (exp (a * t))) 
+             absolutely_integrable_on {0<..}" (is "?f absolutely_integrable_on _")
+proof -
+  have "((\<lambda>x. (Re z - 1) * (ln x / x)) \<longlongrightarrow> (Re z - 1) * 0) at_top"
+    by (intro tendsto_intros ln_x_over_x_tendsto_0)
+  hence "((\<lambda>x. ((Re z - 1) * ln x) / x) \<longlongrightarrow> 0) at_top" by simp
+  from order_tendstoD(2)[OF this, of "a/2"] and \<open>a > 0\<close>
+    have "eventually (\<lambda>x. (Re z - 1) * ln x / x < a/2) at_top" by simp
+  from eventually_conj[OF this eventually_gt_at_top[of 0]]
+    obtain x0 where "\<forall>x\<ge>x0. (Re z - 1) * ln x / x < a/2 \<and> x > 0"
+      by (auto simp: eventually_at_top_linorder)
+  hence "x0 > 0" by simp
+  have "x powr (Re z - 1) / exp (a * x) < exp (-(a/2) * x)" if "x \<ge> x0" for x
+  proof -
+    from that and \<open>\<forall>x\<ge>x0. _\<close> have x: "(Re z - 1) * ln x / x < a / 2" "x > 0" by auto
+    have "x powr (Re z - 1) = exp ((Re z - 1) * ln x)"
+      using \<open>x > 0\<close> by (simp add: powr_def)
+    also from x have "(Re z - 1) * ln x < (a * x) / 2" by (simp add: field_simps)
+    finally show ?thesis by (simp add: field_simps exp_add [symmetric])
+  qed
+  note x0 = \<open>x0 > 0\<close> this
+
+  have "?f absolutely_integrable_on ({0<..x0} \<union> {x0..})"
+  proof (rule set_integrable_Un)
+    show "?f absolutely_integrable_on {0<..x0}"
+    proof (rule Bochner_Integration.integrable_bound [OF _ _ AE_I2])
+      show "set_integrable lebesgue {0<..x0} (\<lambda>x. x powr (Re z - 1))" using x0(1) assms
+        by (intro nonnegative_absolutely_integrable_1 integrable_on_powr_from_0') auto
+      show "set_borel_measurable lebesgue {0<..x0}
+              (\<lambda>x. complex_of_real x powr (z - 1) / complex_of_real (exp (a * x)))"
+        by (intro measurable_completion)
+           (auto intro!: borel_measurable_continuous_on_indicator continuous_intros)
+      fix x :: real 
+      have "x powr (Re z - 1) / exp (a * x) \<le> x powr (Re z - 1) / 1" if "x \<ge> 0"
+        using that assms by (intro divide_left_mono) auto
+      thus "norm (indicator {0<..x0} x *\<^sub>R ?f x) \<le> 
+               norm (indicator {0<..x0} x *\<^sub>R x powr (Re z - 1))"
+        by (simp_all add: norm_divide norm_powr_real_powr indicator_def)
+    qed
+  next
+    show "?f absolutely_integrable_on {x0..}"
+    proof (rule Bochner_Integration.integrable_bound [OF _ _ AE_I2])
+      show "set_integrable lebesgue {x0..} (\<lambda>x. exp (-(a/2) * x))" using assms
+        by (intro nonnegative_absolutely_integrable_1 integrable_on_exp_minus_to_infinity) auto
+      show "set_borel_measurable lebesgue {x0..}
+              (\<lambda>x. complex_of_real x powr (z - 1) / complex_of_real (exp (a * x)))" using x0(1)
+        by (intro measurable_completion)
+           (auto intro!: borel_measurable_continuous_on_indicator continuous_intros)
+      fix x :: real 
+      show "norm (indicator {x0..} x *\<^sub>R ?f x) \<le> 
+               norm (indicator {x0..} x *\<^sub>R exp (-(a/2) * x))" using x0
+        by (auto simp: norm_divide norm_powr_real_powr indicator_def less_imp_le)
+    qed
+  qed auto
+  also have "{0<..x0} \<union> {x0..} = {0<..}" using x0(1) by auto
+  finally show ?thesis .
+qed
+
 lemma integrable_Gamma_integral_bound:
   fixes a c :: real
   assumes a: "a > -1" and c: "c \<ge> 0"
@@ -2898,6 +2967,25 @@
   from has_integral_linear[OF this bounded_linear_Re] show ?thesis by (simp add: o_def)
 qed
 
+lemma absolutely_integrable_Gamma_integral':
+  assumes "Re z > 0"
+  shows   "(\<lambda>t. complex_of_real t powr (z - 1) / of_real (exp t)) absolutely_integrable_on {0<..}"
+  using absolutely_integrable_Gamma_integral [OF assms zero_less_one] by simp
+
+lemma Gamma_integral_complex':
+  assumes z: "Re z > 0"
+  shows   "((\<lambda>t. of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0<..}"
+proof -
+  have "((\<lambda>t. of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0..}"
+    by (rule Gamma_integral_complex) fact+
+  hence "((\<lambda>t. if t \<in> {0<..} then of_real t powr (z - 1) / of_real (exp t) else 0) 
+           has_integral Gamma z) {0..}"
+    by (rule has_integral_spike [of "{0}", rotated 2]) auto
+  also have "?this = ?thesis"
+    by (subst has_integral_restrict) auto
+  finally show ?thesis .
+qed
+
 
 
 subsection \<open>The Weierstraß product formula for the sine\<close>
diff -r 4585bfd19074 -r 322120e880c5 src/HOL/Analysis/Infinite_Set_Sum.thy
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Sun Aug 27 16:17:44 2017 +0100
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Sat Aug 26 18:58:40 2017 +0200
@@ -108,6 +108,15 @@
   "\<Sum>\<^sub>ai\<in>A. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) A"
 
 syntax (ASCII)
+  "_uinfsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
+  ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
+syntax
+  "_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
+  ("(2\<Sum>\<^sub>a_./ _)" [0, 10] 10)
+translations \<comment> \<open>Beware of argument permutation!\<close>
+  "\<Sum>\<^sub>ai. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) (CONST UNIV)"
+
+syntax (ASCII)
   "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
   ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10)
 syntax
@@ -159,6 +168,31 @@
   "A \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> set_integrable (count_space B) A f"
   by (subst abs_summable_on_restrict[of _ B]) (auto simp: abs_summable_on_def)
 
+lemma abs_summable_on_norm_iff [simp]: 
+  "(\<lambda>x. norm (f x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"
+  by (simp add: abs_summable_on_def integrable_norm_iff)
+
+lemma abs_summable_on_normI: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. norm (f x)) abs_summable_on A"
+  by simp
+
+lemma abs_summable_on_comparison_test:
+  assumes "g abs_summable_on A"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> norm (g x)"
+  shows   "f abs_summable_on A"
+  using assms Bochner_Integration.integrable_bound[of "count_space A" g f] 
+  unfolding abs_summable_on_def by (auto simp: AE_count_space)  
+
+lemma abs_summable_on_comparison_test':
+  assumes "g abs_summable_on A"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> g x"
+  shows   "f abs_summable_on A"
+proof (rule abs_summable_on_comparison_test[OF assms(1), of f])
+  fix x assume "x \<in> A"
+  with assms(2) have "norm (f x) \<le> g x" .
+  also have "\<dots> \<le> norm (g x)" by simp
+  finally show "norm (f x) \<le> norm (g x)" .
+qed
+
 lemma abs_summable_on_cong [cong]:
   "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> (f abs_summable_on A) \<longleftrightarrow> (g abs_summable_on B)"
   unfolding abs_summable_on_def by (intro integrable_cong) auto
@@ -210,6 +244,18 @@
   shows   "f abs_summable_on (A \<union> B)"
   using assms unfolding abs_summable_on_altdef by (intro set_integrable_Un) auto
 
+lemma abs_summable_on_insert_iff [simp]:
+  "f abs_summable_on insert x A \<longleftrightarrow> f abs_summable_on A"
+proof safe
+  assume "f abs_summable_on insert x A"
+  thus "f abs_summable_on A"
+    by (rule abs_summable_on_subset) auto
+next
+  assume "f abs_summable_on A"
+  from abs_summable_on_union[OF this, of "{x}"]
+    show "f abs_summable_on insert x A" by simp
+qed
+
 lemma abs_summable_on_reindex_bij_betw:
   assumes "bij_betw g A B"
   shows   "(\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on B"
@@ -235,11 +281,11 @@
   finally show ?thesis .
 qed
 
-lemma abs_summable_reindex_iff: 
+lemma abs_summable_on_reindex_iff: 
   "inj_on g A \<Longrightarrow> (\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on (g ` A)"
   by (intro abs_summable_on_reindex_bij_betw inj_on_imp_bij_betw)
 
-lemma abs_summable_on_Sigma_project:
+lemma abs_summable_on_Sigma_project2:
   fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
   assumes "f abs_summable_on (Sigma A B)" "x \<in> A"
   shows   "(\<lambda>y. f (x, y)) abs_summable_on (B x)"
@@ -425,6 +471,46 @@
   by (intro Bochner_Integration.integral_cong refl)
      (auto simp: indicator_def split: if_splits)
 
+lemma infsetsum_mono_neutral:
+  fixes f g :: "'a \<Rightarrow> real"
+  assumes "f abs_summable_on A" and "g abs_summable_on B"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+  assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x \<le> 0"
+  assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x \<ge> 0"
+  shows   "infsetsum f A \<le> infsetsum g B"
+  using assms unfolding infsetsum_altdef abs_summable_on_altdef
+  by (intro Bochner_Integration.integral_mono) (auto simp: indicator_def)
+
+lemma infsetsum_mono_neutral_left:
+  fixes f g :: "'a \<Rightarrow> real"
+  assumes "f abs_summable_on A" and "g abs_summable_on B"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+  assumes "A \<subseteq> B"
+  assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x \<ge> 0"
+  shows   "infsetsum f A \<le> infsetsum g B"
+  using \<open>A \<subseteq> B\<close> by (intro infsetsum_mono_neutral assms) auto
+
+lemma infsetsum_mono_neutral_right:
+  fixes f g :: "'a \<Rightarrow> real"
+  assumes "f abs_summable_on A" and "g abs_summable_on B"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+  assumes "B \<subseteq> A"
+  assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x \<le> 0"
+  shows   "infsetsum f A \<le> infsetsum g B"
+  using \<open>B \<subseteq> A\<close> by (intro infsetsum_mono_neutral assms) auto
+
+lemma infsetsum_mono:
+  fixes f g :: "'a \<Rightarrow> real"
+  assumes "f abs_summable_on A" and "g abs_summable_on A"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+  shows   "infsetsum f A \<le> infsetsum g A"
+  by (intro infsetsum_mono_neutral assms) auto
+
+lemma norm_infsetsum_bound:
+  "norm (infsetsum f A) \<le> infsetsum (\<lambda>x. norm (f x)) A"
+  unfolding abs_summable_on_def infsetsum_def
+  by (rule Bochner_Integration.integral_norm_bound)
+
 lemma infsetsum_Sigma:
   fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
   assumes [simp]: "countable A" and "\<And>i. countable (B i)"
@@ -460,6 +546,13 @@
   finally show ?thesis ..
 qed
 
+lemma infsetsum_Sigma':
+  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+  assumes [simp]: "countable A" and "\<And>i. countable (B i)"
+  assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on (Sigma A B)"
+  shows   "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) (B x)) A = infsetsum (\<lambda>(x,y). f x y) (Sigma A B)"
+  using assms by (subst infsetsum_Sigma) auto
+
 lemma infsetsum_Times:
   fixes A :: "'a set" and B :: "'b set"
   assumes [simp]: "countable A" and "countable B"
@@ -496,6 +589,95 @@
   finally show ?thesis .
 qed
 
+lemma abs_summable_on_Sigma_iff:
+  assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
+  shows   "f abs_summable_on Sigma A B \<longleftrightarrow> 
+             (\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x) \<and>
+             ((\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A)"
+proof safe
+  define B' where "B' = (\<Union>x\<in>A. B x)"
+  have [simp]: "countable B'" 
+    unfolding B'_def using assms by auto
+  interpret pair_sigma_finite "count_space A" "count_space B'"
+    by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
+
+  {
+    assume *: "f abs_summable_on Sigma A B"
+    thus "(\<lambda>y. f (x, y)) abs_summable_on B x" if "x \<in> A" for x
+      using that by (rule abs_summable_on_Sigma_project2)
+
+    have "set_integrable (count_space (A \<times> B')) (Sigma A B) (\<lambda>z. norm (f z))"
+      using abs_summable_on_normI[OF *]
+      by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
+    also have "count_space (A \<times> B') = count_space A \<Otimes>\<^sub>M count_space B'"
+      by (simp add: pair_measure_countable)
+    finally have "integrable (count_space A) 
+                    (\<lambda>x. lebesgue_integral (count_space B') 
+                      (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y))))"
+      by (rule integrable_fst')
+    also have "?this \<longleftrightarrow> integrable (count_space A)
+                    (\<lambda>x. lebesgue_integral (count_space B') 
+                      (\<lambda>y. indicator (B x) y *\<^sub>R norm (f (x, y))))"
+      by (intro integrable_cong refl) (simp_all add: indicator_def)
+    also have "\<dots> \<longleftrightarrow> integrable (count_space A) (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x))"
+      by (intro integrable_cong refl infsetsum_altdef' [symmetric]) (auto simp: B'_def)
+    also have "\<dots> \<longleftrightarrow> (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A"
+      by (simp add: abs_summable_on_def)
+    finally show \<dots> .
+  }
+
+  {
+    assume *: "\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x"
+    assume "(\<lambda>x. \<Sum>\<^sub>ay\<in>B x. norm (f (x, y))) abs_summable_on A"
+    also have "?this \<longleftrightarrow> (\<lambda>x. \<integral>y\<in>B x. norm (f (x, y)) \<partial>count_space B') abs_summable_on A"
+      by (intro abs_summable_on_cong refl infsetsum_altdef') (auto simp: B'_def)
+    also have "\<dots> \<longleftrightarrow> (\<lambda>x. \<integral>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y)) \<partial>count_space B')
+                        abs_summable_on A" (is "_ \<longleftrightarrow> ?h abs_summable_on _")
+      by (intro abs_summable_on_cong) (auto simp: indicator_def)
+    also have "\<dots> \<longleftrightarrow> integrable (count_space A) ?h"
+      by (simp add: abs_summable_on_def)
+    finally have **: \<dots> .
+
+    have "integrable (count_space A \<Otimes>\<^sub>M count_space B') (\<lambda>z. indicator (Sigma A B) z *\<^sub>R f z)"
+    proof (rule Fubini_integrable, goal_cases)
+      case 3
+      {
+        fix x assume x: "x \<in> A"
+        with * have "(\<lambda>y. f (x, y)) abs_summable_on B x"
+          by blast
+        also have "?this \<longleftrightarrow> integrable (count_space B') 
+                      (\<lambda>y. indicator (B x) y *\<^sub>R f (x, y))"
+          using x by (intro abs_summable_on_altdef') (auto simp: B'_def)
+        also have "(\<lambda>y. indicator (B x) y *\<^sub>R f (x, y)) = 
+                     (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))"
+          using x by (auto simp: indicator_def)
+        finally have "integrable (count_space B')
+                        (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))" .
+      }
+      thus ?case by (auto simp: AE_count_space)
+    qed (insert **, auto simp: pair_measure_countable)
+    also have "count_space A \<Otimes>\<^sub>M count_space B' = count_space (A \<times> B')"
+      by (simp add: pair_measure_countable)
+    also have "set_integrable (count_space (A \<times> B')) (Sigma A B) f \<longleftrightarrow>
+                 f abs_summable_on Sigma A B"
+      by (rule abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
+    finally show \<dots> .
+  }
+qed
+
+lemma abs_summable_on_Sigma_project1:
+  assumes "(\<lambda>(x,y). f x y) abs_summable_on Sigma A B"
+  assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
+  shows   "(\<lambda>x. infsetsum (\<lambda>y. norm (f x y)) (B x)) abs_summable_on A"
+  using assms by (subst (asm) abs_summable_on_Sigma_iff) auto
+
+lemma abs_summable_on_Sigma_project1':
+  assumes "(\<lambda>(x,y). f x y) abs_summable_on Sigma A B"
+  assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
+  shows   "(\<lambda>x. infsetsum (\<lambda>y. f x y) (B x)) abs_summable_on A"
+  by (intro abs_summable_on_comparison_test' [OF abs_summable_on_Sigma_project1[OF assms]]
+        norm_infsetsum_bound)
+
 lemma infsetsum_prod_PiE:
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
   assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
@@ -565,6 +747,29 @@
   using assms unfolding infsetsum_def abs_summable_on_def 
   by (rule Bochner_Integration.integral_mult_right)
 
+lemma infsetsum_cdiv:
+  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_field, second_countable_topology}"
+  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
+  shows   "infsetsum (\<lambda>x. f x / c) A = infsetsum f A / c"
+  using assms unfolding infsetsum_def abs_summable_on_def by auto
+
+
 (* TODO Generalise with bounded_linear *)
 
+lemma
+  fixes f :: "'a \<Rightarrow> 'c :: {banach, real_normed_field, second_countable_topology}"
+  assumes [simp]: "countable A" and [simp]: "countable B"
+  assumes "f abs_summable_on A" and "g abs_summable_on B"
+  shows   abs_summable_on_product: "(\<lambda>(x,y). f x * g y) abs_summable_on A \<times> B"
+    and   infsetsum_product: "infsetsum (\<lambda>(x,y). f x * g y) (A \<times> B) =
+                                infsetsum f A * infsetsum g B"
+proof -
+  from assms show "(\<lambda>(x,y). f x * g y) abs_summable_on A \<times> B"
+    by (subst abs_summable_on_Sigma_iff)
+       (auto intro!: abs_summable_on_cmult_right simp: norm_mult infsetsum_cmult_right)
+  with assms show "infsetsum (\<lambda>(x,y). f x * g y) (A \<times> B) = infsetsum f A * infsetsum g B"
+    by (subst infsetsum_Sigma)
+       (auto simp: infsetsum_cmult_left infsetsum_cmult_right)
+qed
+
 end