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