src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
 changeset 59000 6eb0725503fc parent 58877 262572d90bc6 child 59425 c5e79df8cc21
```     1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Nov 13 14:40:06 2014 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Nov 13 17:19:52 2014 +0100
1.3 @@ -774,120 +774,6 @@
1.4
1.5  subsection {* Sums *}
1.6
1.7 -lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
1.8 -proof (cases "finite A")
1.9 -  case True
1.10 -  then show ?thesis by induct auto
1.11 -next
1.12 -  case False
1.13 -  then show ?thesis by simp
1.14 -qed
1.15 -
1.16 -lemma setsum_Pinfty:
1.17 -  fixes f :: "'a \<Rightarrow> ereal"
1.18 -  shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)"
1.19 -proof safe
1.20 -  assume *: "setsum f P = \<infinity>"
1.21 -  show "finite P"
1.22 -  proof (rule ccontr)
1.23 -    assume "infinite P"
1.24 -    with * show False
1.25 -      by auto
1.26 -  qed
1.27 -  show "\<exists>i\<in>P. f i = \<infinity>"
1.28 -  proof (rule ccontr)
1.29 -    assume "\<not> ?thesis"
1.30 -    then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>"
1.31 -      by auto
1.32 -    with `finite P` have "setsum f P \<noteq> \<infinity>"
1.33 -      by induct auto
1.34 -    with * show False
1.35 -      by auto
1.36 -  qed
1.37 -next
1.38 -  fix i
1.39 -  assume "finite P" and "i \<in> P" and "f i = \<infinity>"
1.40 -  then show "setsum f P = \<infinity>"
1.41 -  proof induct
1.42 -    case (insert x A)
1.43 -    show ?case using insert by (cases "x = i") auto
1.44 -  qed simp
1.45 -qed
1.46 -
1.47 -lemma setsum_Inf:
1.48 -  fixes f :: "'a \<Rightarrow> ereal"
1.49 -  shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
1.50 -proof
1.51 -  assume *: "\<bar>setsum f A\<bar> = \<infinity>"
1.52 -  have "finite A"
1.53 -    by (rule ccontr) (insert *, auto)
1.54 -  moreover have "\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>"
1.55 -  proof (rule ccontr)
1.56 -    assume "\<not> ?thesis"
1.57 -    then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
1.58 -      by auto
1.59 -    from bchoice[OF this] obtain r where "\<forall>x\<in>A. f x = ereal (r x)" ..
1.60 -    with * show False
1.61 -      by auto
1.62 -  qed
1.63 -  ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
1.64 -    by auto
1.65 -next
1.66 -  assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
1.67 -  then obtain i where "finite A" "i \<in> A" and "\<bar>f i\<bar> = \<infinity>"
1.68 -    by auto
1.69 -  then show "\<bar>setsum f A\<bar> = \<infinity>"
1.70 -  proof induct
1.71 -    case (insert j A)
1.72 -    then show ?case
1.73 -      by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto
1.74 -  qed simp
1.75 -qed
1.76 -
1.77 -lemma setsum_real_of_ereal:
1.78 -  fixes f :: "'i \<Rightarrow> ereal"
1.79 -  assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
1.80 -  shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
1.81 -proof -
1.82 -  have "\<forall>x\<in>S. \<exists>r. f x = ereal r"
1.83 -  proof
1.84 -    fix x
1.85 -    assume "x \<in> S"
1.86 -    from assms[OF this] show "\<exists>r. f x = ereal r"
1.87 -      by (cases "f x") auto
1.88 -  qed
1.89 -  from bchoice[OF this] obtain r where "\<forall>x\<in>S. f x = ereal (r x)" ..
1.90 -  then show ?thesis
1.91 -    by simp
1.92 -qed
1.93 -
1.94 -lemma setsum_ereal_0:
1.95 -  fixes f :: "'a \<Rightarrow> ereal"
1.96 -  assumes "finite A"
1.97 -    and "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
1.98 -  shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
1.99 -proof
1.100 -  assume *: "(\<Sum>x\<in>A. f x) = 0"
1.101 -  then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>"
1.102 -    by auto
1.103 -  then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>"
1.104 -    using assms by (force simp: setsum_Pinfty)
1.105 -  then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
1.106 -    by auto
1.107 -  from bchoice[OF this] * assms show "\<forall>i\<in>A. f i = 0"
1.108 -    using setsum_nonneg_eq_0_iff[of A "\<lambda>i. real (f i)"] by auto
1.109 -qed (rule setsum.neutral)
1.110 -
1.111 -lemma setsum_ereal_right_distrib:
1.112 -  fixes f :: "'a \<Rightarrow> ereal"
1.113 -  assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
1.114 -  shows "r * setsum f A = (\<Sum>n\<in>A. r * f n)"
1.115 -proof cases
1.116 -  assume "finite A"
1.117 -  then show ?thesis using assms
1.118 -    by induct (auto simp: ereal_right_distrib setsum_nonneg)
1.119 -qed simp
1.120 -
1.121  lemma sums_ereal_positive:
1.122    fixes f :: "nat \<Rightarrow> ereal"
1.123    assumes "\<And>i. 0 \<le> f i"
1.124 @@ -1463,6 +1349,9 @@
1.125
1.126  subsection "Relate extended reals and the indicator function"
1.127
1.128 +lemma ereal_indicator_le_0: "(indicator S x::ereal) \<le> 0 \<longleftrightarrow> x \<notin> S"
1.129 +  by (auto split: split_indicator simp: one_ereal_def)
1.130 +
1.131  lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
1.132    by (auto simp: indicator_def one_ereal_def)
1.133
```