src/HOL/Lim.thy
 changeset 29803 c56a5571f60a parent 29667 53103fc8ffa3 child 29885 379e43e513c2
```     1.1 --- a/src/HOL/Lim.thy	Wed Feb 04 18:10:07 2009 +0100
1.2 +++ b/src/HOL/Lim.thy	Thu Feb 05 11:34:42 2009 +0100
1.3 @@ -532,6 +532,44 @@
1.4  lemma isCont_abs [simp]: "isCont abs (a::real)"
1.5  by (rule isCont_rabs [OF isCont_ident])
1.6
1.7 +lemma isCont_setsum: fixes A :: "nat set" assumes "finite A"
1.8 +  shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x"
1.9 +  using `finite A`
1.10 +proof induct
1.11 +  case (insert a F) show "isCont (\<lambda> x. \<Sum> i \<in> (insert a F). f i x) x"
1.12 +    unfolding setsum_insert[OF `finite F` `a \<notin> F`] by (rule isCont_add, auto simp add: insert)
1.13 +qed auto
1.14 +
1.15 +lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
1.16 +  and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
1.17 +  shows "0 \<le> f x"
1.18 +proof (rule ccontr)
1.19 +  assume "\<not> 0 \<le> f x" hence "f x < 0" by auto
1.20 +  hence "0 < - f x / 2" by auto
1.21 +  from isCont[unfolded isCont_def, THEN LIM_D, OF this]
1.22 +  obtain s where "s > 0" and s_D: "\<And>x'. \<lbrakk> x' \<noteq> x ; \<bar> x' - x \<bar> < s \<rbrakk> \<Longrightarrow> \<bar> f x' - f x \<bar> < - f x / 2" by auto
1.23 +
1.24 +  let ?x = "x - min (s / 2) ((x - b) / 2)"
1.25 +  have "?x < x" and "\<bar> ?x - x \<bar> < s"
1.26 +    using `b < x` and `0 < s` by auto
1.27 +  have "b < ?x"
1.28 +  proof (cases "s < x - b")
1.29 +    case True thus ?thesis using `0 < s` by auto
1.30 +  next
1.31 +    case False hence "s / 2 \<ge> (x - b) / 2" by auto
1.32 +    from inf_absorb2[OF this, unfolded inf_real_def]
1.33 +    have "?x = (x + b) / 2" by auto
1.34 +    thus ?thesis using `b < x` by auto
1.35 +  qed
1.36 +  hence "0 \<le> f ?x" using all_le `?x < x` by auto
1.37 +  moreover have "\<bar>f ?x - f x\<bar> < - f x / 2"
1.38 +    using s_D[OF _ `\<bar> ?x - x \<bar> < s`] `?x < x` by auto
1.39 +  hence "f ?x - f x < - f x / 2" by auto
1.40 +  hence "f ?x < f x / 2" by auto
1.41 +  hence "f ?x < 0" using `f x < 0` by auto
1.42 +  thus False using `0 \<le> f ?x` by auto
1.43 +qed
1.44 +
1.45
1.46  subsection {* Uniform Continuity *}
1.47
```