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