tuned proofs
authorhuffman
Sun Mar 16 13:34:35 2014 -0700 (2014-03-16)
changeset 56167ac8098b0e458
parent 56166 9a241bc276cd
child 56168 088b64497a61
tuned proofs
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Transcendental.thy	Sun Mar 16 18:09:04 2014 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Sun Mar 16 13:34:35 2014 -0700
     1.3 @@ -533,54 +533,28 @@
     1.4  qed
     1.5  
     1.6  lemma lemma_termdiff4:
     1.7 -  fixes f :: "'a::{real_normed_field} \<Rightarrow>
     1.8 -              'b::real_normed_vector"
     1.9 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    1.10    assumes k: "0 < (k::real)"
    1.11      and le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
    1.12    shows "f -- 0 --> 0"
    1.13 -  unfolding LIM_eq diff_0_right
    1.14 -proof safe
    1.15 -  let ?h = "of_real (k / 2)::'a"
    1.16 -  have "?h \<noteq> 0" and "norm ?h < k" using k by simp_all
    1.17 -  hence "norm (f ?h) \<le> K * norm ?h" by (rule le)
    1.18 -  hence "0 \<le> K * norm ?h" by (rule order_trans [OF norm_ge_zero])
    1.19 -  hence zero_le_K: "0 \<le> K" using k by (simp add: zero_le_mult_iff)
    1.20 -
    1.21 -  fix r::real
    1.22 -  assume r: "0 < r"
    1.23 -  show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)"
    1.24 -  proof cases
    1.25 -    assume "K = 0"
    1.26 -    with k r le have "0 < k \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < k \<longrightarrow> norm (f x) < r)"
    1.27 +proof (rule tendsto_norm_zero_cancel)
    1.28 +  show "(\<lambda>h. norm (f h)) -- 0 --> 0"
    1.29 +  proof (rule real_tendsto_sandwich)
    1.30 +    show "eventually (\<lambda>h. 0 \<le> norm (f h)) (at 0)"
    1.31        by simp
    1.32 -    thus "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" ..
    1.33 -  next
    1.34 -    assume K_neq_zero: "K \<noteq> 0"
    1.35 -    with zero_le_K have K: "0 < K" by simp
    1.36 -    show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)"
    1.37 -    proof (rule exI, safe)
    1.38 -      from k r K
    1.39 -      show "0 < min k (r * inverse K / 2)"
    1.40 -        by (simp add: mult_pos_pos positive_imp_inverse_positive)
    1.41 -    next
    1.42 -      fix x::'a
    1.43 -      assume x1: "x \<noteq> 0" and x2: "norm x < min k (r * inverse K / 2)"
    1.44 -      from x2 have x3: "norm x < k" and x4: "norm x < r * inverse K / 2"
    1.45 -        by simp_all
    1.46 -      from x1 x3 le have "norm (f x) \<le> K * norm x" by simp
    1.47 -      also from x4 K have "K * norm x < K * (r * inverse K / 2)"
    1.48 -        by (rule mult_strict_left_mono)
    1.49 -      also have "\<dots> = r / 2"
    1.50 -        using K_neq_zero by simp
    1.51 -      also have "r / 2 < r"
    1.52 -        using r by simp
    1.53 -      finally show "norm (f x) < r" .
    1.54 -    qed
    1.55 +    show "eventually (\<lambda>h. norm (f h) \<le> K * norm h) (at 0)"
    1.56 +      using k by (auto simp add: eventually_at dist_norm le)
    1.57 +    show "(\<lambda>h. 0) -- (0::'a) --> (0::real)"
    1.58 +      by (rule tendsto_const)
    1.59 +    have "(\<lambda>h. K * norm h) -- (0::'a) --> K * norm (0::'a)"
    1.60 +      by (intro tendsto_intros)
    1.61 +    then show "(\<lambda>h. K * norm h) -- (0::'a) --> 0"
    1.62 +      by simp
    1.63    qed
    1.64  qed
    1.65  
    1.66  lemma lemma_termdiff5:
    1.67 -  fixes g :: "'a::real_normed_field \<Rightarrow> nat \<Rightarrow> 'b::banach"
    1.68 +  fixes g :: "'a::real_normed_vector \<Rightarrow> nat \<Rightarrow> 'b::banach"
    1.69    assumes k: "0 < (k::real)"
    1.70    assumes f: "summable f"
    1.71    assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h"
    1.72 @@ -685,34 +659,20 @@
    1.73      show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
    1.74    next
    1.75      fix h :: 'a
    1.76 -    assume "h \<noteq> 0"
    1.77      assume "norm (h - 0) < norm K - norm x"
    1.78      hence "norm x + norm h < norm K" by simp
    1.79      hence 5: "norm (x + h) < norm K"
    1.80        by (rule norm_triangle_ineq [THEN order_le_less_trans])
    1.81 -    have A: "summable (\<lambda>n. c n * x ^ n)"
    1.82 -      by (rule powser_inside [OF 1 4])
    1.83 -    have B: "summable (\<lambda>n. c n * (x + h) ^ n)"
    1.84 -      by (rule powser_inside [OF 1 5])
    1.85 -    have C: "summable (\<lambda>n. diffs c n * x ^ n)"
    1.86 -      by (rule powser_inside [OF 2 4])
    1.87 -    let ?dp = "(\<Sum>n. of_nat n * c n * x ^ (n - Suc 0))"
    1.88 -    have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
    1.89 -          ((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - ?dp"  
    1.90 -      by (metis sums_unique [OF diffs_equiv [OF C]])
    1.91 -    also have "... = (\<Sum>n. c n * (x + h) ^ n - c n * x ^ n) / h - ?dp"  
    1.92 -      by (metis suminf_diff [OF B A])
    1.93 -    also have "... = (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h)  - ?dp"
    1.94 -      by (metis suminf_divide [OF summable_diff [OF B A]] )  
    1.95 -    also have "... = (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h - of_nat n * c n * x ^ (n - Suc 0))"
    1.96 -      apply (subst suminf_diff)
    1.97 -      apply (auto intro: summable_divide summable_diff [OF B A] sums_summable [OF diffs_equiv [OF C]])
    1.98 -      done
    1.99 -    also have "... = (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
   1.100 +    have "summable (\<lambda>n. c n * x ^ n)"
   1.101 +      and "summable (\<lambda>n. c n * (x + h) ^ n)"
   1.102 +      and "summable (\<lambda>n. diffs c n * x ^ n)"
   1.103 +      using 1 2 4 5 by (auto elim: powser_inside)
   1.104 +    then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
   1.105 +          (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h - of_nat n * c n * x ^ (n - Suc 0))"
   1.106 +      by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums)
   1.107 +    then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
   1.108 +          (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
   1.109        by (simp add: algebra_simps)
   1.110 -    finally show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h
   1.111 -                   - (\<Sum>n. diffs c n * x ^ n) =
   1.112 -                  (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))" . 
   1.113    next
   1.114      show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   1.115        by (rule termdiffs_aux [OF 3 4])