--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon May 23 19:21:05 2011 +0200
@@ -805,6 +805,21 @@
} ultimately show ?thesis by auto
qed
+lemma liminf_extreal_cminus:
+ fixes f :: "nat \<Rightarrow> extreal" assumes "c \<noteq> -\<infinity>"
+ shows "liminf (\<lambda>x. c - f x) = c - limsup f"
+proof (cases c)
+ case PInf then show ?thesis by (simp add: Liminf_const)
+next
+ case (real r) then show ?thesis
+ unfolding liminf_SUPR_INFI limsup_INFI_SUPR
+ apply (subst INFI_extreal_cminus)
+ apply auto
+ apply (subst SUPR_extreal_cminus)
+ apply auto
+ done
+qed (insert `c \<noteq> -\<infinity>`, simp)
+
subsubsection {* Continuity *}
lemma continuous_imp_tendsto:
@@ -1259,4 +1274,20 @@
finally show "\<exists>r. (\<lambda>i. real (f i)) sums r" by (auto simp: sums_extreal)
qed
+lemma suminf_SUP_eq:
+ fixes f :: "nat \<Rightarrow> nat \<Rightarrow> extreal"
+ assumes "\<And>i. incseq (\<lambda>n. f n i)" "\<And>n i. 0 \<le> f n i"
+ shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
+proof -
+ { fix n :: nat
+ have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
+ using assms by (auto intro!: SUPR_extreal_setsum[symmetric]) }
+ note * = this
+ show ?thesis using assms
+ apply (subst (1 2) suminf_extreal_eq_SUPR)
+ unfolding *
+ apply (auto intro!: le_SUPI2)
+ apply (subst SUP_commute) ..
+qed
+
end
\ No newline at end of file