diff -r d201a838d0f7 -r c56a5571f60a src/HOL/Lim.thy
--- a/src/HOL/Lim.thy Wed Feb 04 18:10:07 2009 +0100
+++ b/src/HOL/Lim.thy Thu Feb 05 11:34:42 2009 +0100
@@ -532,6 +532,44 @@
lemma isCont_abs [simp]: "isCont abs (a::real)"
by (rule isCont_rabs [OF isCont_ident])
+lemma isCont_setsum: fixes A :: "nat set" assumes "finite A"
+ shows "\ i \ A. isCont (f i) x \ isCont (\ x. \ i \ A. f i x) x"
+ using `finite A`
+proof induct
+ case (insert a F) show "isCont (\ x. \ i \ (insert a F). f i x) x"
+ unfolding setsum_insert[OF `finite F` `a \ F`] by (rule isCont_add, auto simp add: insert)
+qed auto
+
+lemma LIM_less_bound: fixes f :: "real \ real" assumes "b < x"
+ and all_le: "\ x' \ { b <..< x}. 0 \ f x'" and isCont: "isCont f x"
+ shows "0 \ f x"
+proof (rule ccontr)
+ assume "\ 0 \ f x" hence "f x < 0" by auto
+ hence "0 < - f x / 2" by auto
+ from isCont[unfolded isCont_def, THEN LIM_D, OF this]
+ obtain s where "s > 0" and s_D: "\x'. \ x' \ x ; \ x' - x \ < s \ \ \ f x' - f x \ < - f x / 2" by auto
+
+ let ?x = "x - min (s / 2) ((x - b) / 2)"
+ have "?x < x" and "\ ?x - x \ < s"
+ using `b < x` and `0 < s` by auto
+ have "b < ?x"
+ proof (cases "s < x - b")
+ case True thus ?thesis using `0 < s` by auto
+ next
+ case False hence "s / 2 \ (x - b) / 2" by auto
+ from inf_absorb2[OF this, unfolded inf_real_def]
+ have "?x = (x + b) / 2" by auto
+ thus ?thesis using `b < x` by auto
+ qed
+ hence "0 \ f ?x" using all_le `?x < x` by auto
+ moreover have "\f ?x - f x\ < - f x / 2"
+ using s_D[OF _ `\ ?x - x \ < s`] `?x < x` by auto
+ hence "f ?x - f x < - f x / 2" by auto
+ hence "f ?x < f x / 2" by auto
+ hence "f ?x < 0" using `f x < 0` by auto
+ thus False using `0 \ f ?x` by auto
+qed
+
subsection {* Uniform Continuity *}