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 *}