author  huffman 
Wed, 04 Mar 2009 17:12:23 0800  
changeset 30273  ecd6f0ca62ea 
parent 30082  43c5b7bfc791 
child 31017  2c227493ea56 
permissions  rwrr 
12196  1 
(* Title : Transcendental.thy 
2 
Author : Jacques D. Fleuriot 

3 
Copyright : 1998,1999 University of Cambridge 

13958
c1c67582c9b5
New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
12196
diff
changeset

4 
1999,2001 University of Edinburgh 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

5 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
12196  6 
*) 
7 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

8 
header{*Power Series, Transcendental Functions etc.*} 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

9 

15131  10 
theory Transcendental 
25600  11 
imports Fact Series Deriv NthRoot 
15131  12 
begin 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

13 

29164  14 
subsection {* Properties of Power Series *} 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

15 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

16 
lemma lemma_realpow_diff: 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

17 
fixes y :: "'a::recpower" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

18 
shows "p \<le> n \<Longrightarrow> y ^ (Suc n  p) = (y ^ (n  p)) * y" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

19 
proof  
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

20 
assume "p \<le> n" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

21 
hence "Suc n  p = Suc (n  p)" by (rule Suc_diff_le) 
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30082
diff
changeset

22 
thus ?thesis by (simp add: power_commutes) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

23 
qed 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

24 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

25 
lemma lemma_realpow_diff_sumr: 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

26 
fixes y :: "'a::{recpower,comm_semiring_0}" shows 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

27 
"(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n  p)) = 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

28 
y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n  p))" 
29163  29 
by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac 
30 
del: setsum_op_ivl_Suc cong: strong_setsum_cong) 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

31 

15229  32 
lemma lemma_realpow_diff_sumr2: 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

33 
fixes y :: "'a::{recpower,comm_ring}" shows 
15229  34 
"x ^ (Suc n)  y ^ (Suc n) = 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

35 
(x  y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n  p))" 
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30082
diff
changeset

36 
apply (induct n, simp) 
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30082
diff
changeset

37 
apply (simp del: setsum_op_ivl_Suc) 
15561  38 
apply (subst setsum_op_ivl_Suc) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

39 
apply (subst lemma_realpow_diff_sumr) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

40 
apply (simp add: right_distrib del: setsum_op_ivl_Suc) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

41 
apply (subst mult_left_commute [where a="x  y"]) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

42 
apply (erule subst) 
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30082
diff
changeset

43 
apply (simp add: algebra_simps) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

44 
done 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

45 

15229  46 
lemma lemma_realpow_rev_sumr: 
15539  47 
"(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n  p))) = 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

48 
(\<Sum>p=0..<Suc n. (x ^ (n  p)) * (y ^ p))" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

49 
apply (rule setsum_reindex_cong [where f="\<lambda>i. n  i"]) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

50 
apply (rule inj_onI, simp) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

51 
apply auto 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

52 
apply (rule_tac x="n  x" in image_eqI, simp, simp) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

53 
done 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

54 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

55 
text{*Power series has a `circle` of convergence, i.e. if it sums for @{term 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

56 
x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*} 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

57 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

58 
lemma powser_insidea: 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

59 
fixes x z :: "'a::{real_normed_field,banach,recpower}" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

60 
assumes 1: "summable (\<lambda>n. f n * x ^ n)" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

61 
assumes 2: "norm z < norm x" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

62 
shows "summable (\<lambda>n. norm (f n * z ^ n))" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

63 
proof  
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

64 
from 2 have x_neq_0: "x \<noteq> 0" by clarsimp 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

65 
from 1 have "(\<lambda>n. f n * x ^ n) > 0" 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

66 
by (rule summable_LIMSEQ_zero) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

67 
hence "convergent (\<lambda>n. f n * x ^ n)" 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

68 
by (rule convergentI) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

69 
hence "Cauchy (\<lambda>n. f n * x ^ n)" 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

70 
by (simp add: Cauchy_convergent_iff) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

71 
hence "Bseq (\<lambda>n. f n * x ^ n)" 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

72 
by (rule Cauchy_Bseq) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

73 
then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

74 
by (simp add: Bseq_def, safe) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

75 
have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le> 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

76 
K * norm (z ^ n) * inverse (norm (x ^ n))" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

77 
proof (intro exI allI impI) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

78 
fix n::nat assume "0 \<le> n" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

79 
have "norm (norm (f n * z ^ n)) * norm (x ^ n) = 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

80 
norm (f n * x ^ n) * norm (z ^ n)" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

81 
by (simp add: norm_mult abs_mult) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

82 
also have "\<dots> \<le> K * norm (z ^ n)" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

83 
by (simp only: mult_right_mono 4 norm_ge_zero) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

84 
also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

85 
by (simp add: x_neq_0) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

86 
also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

87 
by (simp only: mult_assoc) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

88 
finally show "norm (norm (f n * z ^ n)) \<le> 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

89 
K * norm (z ^ n) * inverse (norm (x ^ n))" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

90 
by (simp add: mult_le_cancel_right x_neq_0) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

91 
qed 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

92 
moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

93 
proof  
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

94 
from 2 have "norm (norm (z * inverse x)) < 1" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

95 
using x_neq_0 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

96 
by (simp add: nonzero_norm_divide divide_inverse [symmetric]) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

97 
hence "summable (\<lambda>n. norm (z * inverse x) ^ n)" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

98 
by (rule summable_geometric) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

99 
hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

100 
by (rule summable_mult) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

101 
thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

102 
using x_neq_0 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

103 
by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

104 
power_inverse norm_power mult_assoc) 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

105 
qed 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

106 
ultimately show "summable (\<lambda>n. norm (f n * z ^ n))" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

107 
by (rule summable_comparison_test) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

108 
qed 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

109 

15229  110 
lemma powser_inside: 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

111 
fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach,recpower}" shows 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

112 
"[ summable (%n. f(n) * (x ^ n)); norm z < norm x ] 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

113 
==> summable (%n. f(n) * (z ^ n))" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

114 
by (rule powser_insidea [THEN summable_norm_cancel]) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

115 

29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

116 
lemma sum_split_even_odd: fixes f :: "nat \<Rightarrow> real" shows 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

117 
"(\<Sum> i = 0 ..< 2 * n. if even i then f i else g i) = 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

118 
(\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1))" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

119 
proof (induct n) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

120 
case (Suc n) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

121 
have "(\<Sum> i = 0 ..< 2 * Suc n. if even i then f i else g i) = 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

122 
(\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))" 
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset

123 
using Suc.hyps unfolding One_nat_def by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

124 
also have "\<dots> = (\<Sum> i = 0 ..< Suc n. f (2 * i)) + (\<Sum> i = 0 ..< Suc n. g (2 * i + 1))" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

125 
finally show ?case . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

126 
qed auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

127 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

128 
lemma sums_if': fixes g :: "nat \<Rightarrow> real" assumes "g sums x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

129 
shows "(\<lambda> n. if even n then 0 else g ((n  1) div 2)) sums x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

130 
unfolding sums_def 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

131 
proof (rule LIMSEQ_I) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

132 
fix r :: real assume "0 < r" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

133 
from `g sums x`[unfolded sums_def, THEN LIMSEQ_D, OF this] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

134 
obtain no where no_eq: "\<And> n. n \<ge> no \<Longrightarrow> (norm (setsum g { 0..<n }  x) < r)" by blast 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

135 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

136 
let ?SUM = "\<lambda> m. \<Sum> i = 0 ..< m. if even i then 0 else g ((i  1) div 2)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

137 
{ fix m assume "m \<ge> 2 * no" hence "m div 2 \<ge> no" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

138 
have sum_eq: "?SUM (2 * (m div 2)) = setsum g { 0 ..< m div 2 }" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

139 
using sum_split_even_odd by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

140 
hence "(norm (?SUM (2 * (m div 2))  x) < r)" using no_eq unfolding sum_eq using `m div 2 \<ge> no` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

141 
moreover 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

142 
have "?SUM (2 * (m div 2)) = ?SUM m" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

143 
proof (cases "even m") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

144 
case True show ?thesis unfolding even_nat_div_two_times_two[OF True, unfolded numeral_2_eq_2[symmetric]] .. 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

145 
next 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

146 
case False hence "even (Suc m)" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

147 
from even_nat_div_two_times_two[OF this, unfolded numeral_2_eq_2[symmetric]] odd_nat_plus_one_div_two[OF False, unfolded numeral_2_eq_2[symmetric]] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

148 
have eq: "Suc (2 * (m div 2)) = m" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

149 
hence "even (2 * (m div 2))" using `odd m` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

150 
have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq .. 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

151 
also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

152 
finally show ?thesis by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

153 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

154 
ultimately have "(norm (?SUM m  x) < r)" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

155 
} 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

156 
thus "\<exists> no. \<forall> m \<ge> no. norm (?SUM m  x) < r" by blast 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

157 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

158 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

159 
lemma sums_if: fixes g :: "nat \<Rightarrow> real" assumes "g sums x" and "f sums y" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

160 
shows "(\<lambda> n. if even n then f (n div 2) else g ((n  1) div 2)) sums (x + y)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

161 
proof  
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

162 
let ?s = "\<lambda> n. if even n then 0 else f ((n  1) div 2)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

163 
{ fix B T E have "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

164 
by (cases B) auto } note if_sum = this 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

165 
have g_sums: "(\<lambda> n. if even n then 0 else g ((n  1) div 2)) sums x" using sums_if'[OF `g sums x`] . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

166 
{ 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

167 
have "?s 0 = 0" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

168 
have Suc_m1: "\<And> n. Suc n  1 = n" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

169 
{ fix B T E have "(if \<not> B then T else E) = (if B then E else T)" by auto } note if_eq = this 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

170 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

171 
have "?s sums y" using sums_if'[OF `f sums y`] . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

172 
from this[unfolded sums_def, THEN LIMSEQ_Suc] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

173 
have "(\<lambda> n. if even n then f (n div 2) else 0) sums y" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

174 
unfolding sums_def setsum_shift_lb_Suc0_0_upt[where f="?s", OF `?s 0 = 0`, symmetric] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

175 
image_Suc_atLeastLessThan[symmetric] setsum_reindex[OF inj_Suc, unfolded comp_def] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

176 
even_nat_Suc Suc_m1 if_eq . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

177 
} from sums_add[OF g_sums this] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

178 
show ?thesis unfolding if_sum . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

179 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

180 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

181 
subsection {* Alternating series test / Leibniz formula *} 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

182 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

183 
lemma sums_alternating_upper_lower: 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

184 
fixes a :: "nat \<Rightarrow> real" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

185 
assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a > 0" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

186 
shows "\<exists>l. ((\<forall>n. (\<Sum>i=0..<2*n. 1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i=0..<2*n. 1^i*a i) > l) \<and> 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

187 
((\<forall>n. l \<le> (\<Sum>i=0..<2*n + 1. 1^i*a i)) \<and> (\<lambda> n. \<Sum>i=0..<2*n + 1. 1^i*a i) > l)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

188 
(is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

189 
proof  
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset

190 
have fg_diff: "\<And>n. ?f n  ?g n =  a (2 * n)" unfolding One_nat_def by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

191 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

192 
have "\<forall> n. ?f n \<le> ?f (Suc n)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

193 
proof fix n show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

194 
moreover 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

195 
have "\<forall> n. ?g (Suc n) \<le> ?g n" 
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset

196 
proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"] 
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset

197 
unfolding One_nat_def by auto qed 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

198 
moreover 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

199 
have "\<forall> n. ?f n \<le> ?g n" 
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset

200 
proof fix n show "?f n \<le> ?g n" using fg_diff a_pos 
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset

201 
unfolding One_nat_def by auto qed 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

202 
moreover 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

203 
have "(\<lambda> n. ?f n  ?g n) > 0" unfolding fg_diff 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

204 
proof (rule LIMSEQ_I) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

205 
fix r :: real assume "0 < r" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

206 
with `a > 0`[THEN LIMSEQ_D] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

207 
obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n  0) < r" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

208 
hence "\<forall> n \<ge> N. norm ( a (2 * n)  0) < r" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

209 
thus "\<exists> N. \<forall> n \<ge> N. norm ( a (2 * n)  0) < r" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

210 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

211 
ultimately 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

212 
show ?thesis by (rule lemma_nest_unique) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

213 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

214 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

215 
lemma summable_Leibniz': fixes a :: "nat \<Rightarrow> real" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

216 
assumes a_zero: "a > 0" and a_pos: "\<And> n. 0 \<le> a n" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

217 
and a_monotone: "\<And> n. a (Suc n) \<le> a n" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

218 
shows summable: "summable (\<lambda> n. (1)^n * a n)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

219 
and "\<And>n. (\<Sum>i=0..<2*n. (1)^i*a i) \<le> (\<Sum>i. (1)^i*a i)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

220 
and "(\<lambda>n. \<Sum>i=0..<2*n. (1)^i*a i) > (\<Sum>i. (1)^i*a i)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

221 
and "\<And>n. (\<Sum>i. (1)^i*a i) \<le> (\<Sum>i=0..<2*n+1. (1)^i*a i)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

222 
and "(\<lambda>n. \<Sum>i=0..<2*n+1. (1)^i*a i) > (\<Sum>i. (1)^i*a i)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

223 
proof  
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

224 
let "?S n" = "(1)^n * a n" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

225 
let "?P n" = "\<Sum>i=0..<n. ?S i" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

226 
let "?f n" = "?P (2 * n)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

227 
let "?g n" = "?P (2 * n + 1)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

228 
obtain l :: real where below_l: "\<forall> n. ?f n \<le> l" and "?f > l" and above_l: "\<forall> n. l \<le> ?g n" and "?g > l" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

229 
using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

230 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

231 
let ?Sa = "\<lambda> m. \<Sum> n = 0..<m. ?S n" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

232 
have "?Sa > l" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

233 
proof (rule LIMSEQ_I) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

234 
fix r :: real assume "0 < r" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

235 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

236 
with `?f > l`[THEN LIMSEQ_D] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

237 
obtain f_no where f: "\<And> n. n \<ge> f_no \<Longrightarrow> norm (?f n  l) < r" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

238 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

239 
from `0 < r` `?g > l`[THEN LIMSEQ_D] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

240 
obtain g_no where g: "\<And> n. n \<ge> g_no \<Longrightarrow> norm (?g n  l) < r" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

241 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

242 
{ fix n :: nat 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

243 
assume "n \<ge> (max (2 * f_no) (2 * g_no))" hence "n \<ge> 2 * f_no" and "n \<ge> 2 * g_no" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

244 
have "norm (?Sa n  l) < r" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

245 
proof (cases "even n") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

246 
case True from even_nat_div_two_times_two[OF this] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

247 
have n_eq: "2 * (n div 2) = n" unfolding numeral_2_eq_2[symmetric] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

248 
with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

249 
from f[OF this] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

250 
show ?thesis unfolding n_eq atLeastLessThanSuc_atLeastAtMost . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

251 
next 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

252 
case False hence "even (n  1)" using even_num_iff odd_pos by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

253 
from even_nat_div_two_times_two[OF this] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

254 
have n_eq: "2 * ((n  1) div 2) = n  1" unfolding numeral_2_eq_2[symmetric] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

255 
hence range_eq: "n  1 + 1 = n" using odd_pos[OF False] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

256 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

257 
from n_eq `n \<ge> 2 * g_no` have "(n  1) div 2 \<ge> g_no" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

258 
from g[OF this] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

259 
show ?thesis unfolding n_eq atLeastLessThanSuc_atLeastAtMost range_eq . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

260 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

261 
} 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

262 
thus "\<exists> no. \<forall> n \<ge> no. norm (?Sa n  l) < r" by blast 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

263 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

264 
hence sums_l: "(\<lambda>i. (1)^i * a i) sums l" unfolding sums_def atLeastLessThanSuc_atLeastAtMost[symmetric] . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

265 
thus "summable ?S" using summable_def by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

266 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

267 
have "l = suminf ?S" using sums_unique[OF sums_l] . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

268 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

269 
{ fix n show "suminf ?S \<le> ?g n" unfolding sums_unique[OF sums_l, symmetric] using above_l by auto } 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

270 
{ fix n show "?f n \<le> suminf ?S" unfolding sums_unique[OF sums_l, symmetric] using below_l by auto } 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

271 
show "?g > suminf ?S" using `?g > l` `l = suminf ?S` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

272 
show "?f > suminf ?S" using `?f > l` `l = suminf ?S` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

273 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

274 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

275 
theorem summable_Leibniz: fixes a :: "nat \<Rightarrow> real" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

276 
assumes a_zero: "a > 0" and "monoseq a" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

277 
shows "summable (\<lambda> n. (1)^n * a n)" (is "?summable") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

278 
and "0 < a 0 \<longrightarrow> (\<forall>n. (\<Sum>i. 1^i*a i) \<in> { \<Sum>i=0..<2*n. 1^i * a i .. \<Sum>i=0..<2*n+1. 1^i * a i})" (is "?pos") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

279 
and "a 0 < 0 \<longrightarrow> (\<forall>n. (\<Sum>i. 1^i*a i) \<in> { \<Sum>i=0..<2*n+1. 1^i * a i .. \<Sum>i=0..<2*n. 1^i * a i})" (is "?neg") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

280 
and "(\<lambda>n. \<Sum>i=0..<2*n. 1^i*a i) > (\<Sum>i. 1^i*a i)" (is "?f") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

281 
and "(\<lambda>n. \<Sum>i=0..<2*n+1. 1^i*a i) > (\<Sum>i. 1^i*a i)" (is "?g") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

282 
proof  
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

283 
have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

284 
proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

285 
case True 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

286 
hence ord: "\<And>n m. m \<le> n \<Longrightarrow> a n \<le> a m" and ge0: "\<And> n. 0 \<le> a n" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

287 
{ fix n have "a (Suc n) \<le> a n" using ord[where n="Suc n" and m=n] by auto } 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

288 
note leibniz = summable_Leibniz'[OF `a > 0` ge0] and mono = this 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

289 
from leibniz[OF mono] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

290 
show ?thesis using `0 \<le> a 0` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

291 
next 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

292 
let ?a = "\<lambda> n.  a n" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

293 
case False 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

294 
with monoseq_le[OF `monoseq a` `a > 0`] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

295 
have "(\<forall> n. a n \<le> 0) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

296 
hence ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

297 
{ fix n have "?a (Suc n) \<le> ?a n" using ord[where n="Suc n" and m=n] by auto } 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

298 
note monotone = this 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

299 
note leibniz = summable_Leibniz'[OF _ ge0, of "\<lambda>x. x", OF LIMSEQ_minus[OF `a > 0`, unfolded minus_zero] monotone] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

300 
have "summable (\<lambda> n. (1)^n * ?a n)" using leibniz(1) by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

301 
then obtain l where "(\<lambda> n. (1)^n * ?a n) sums l" unfolding summable_def by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

302 
from this[THEN sums_minus] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

303 
have "(\<lambda> n. (1)^n * a n) sums l" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

304 
hence ?summable unfolding summable_def by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

305 
moreover 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

306 
have "\<And> a b :: real. \<bar>  a   b \<bar> = \<bar>a  b\<bar>" unfolding minus_diff_minus by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

307 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

308 
from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

309 
have move_minus: "(\<Sum>n.  (1 ^ n * a n)) =  (\<Sum>n. 1 ^ n * a n)" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

310 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

311 
have ?pos using `0 \<le> ?a 0` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

312 
moreover have ?neg using leibniz(2,4) unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

313 
moreover have ?f and ?g using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN LIMSEQ_minus_cancel] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

314 
ultimately show ?thesis by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

315 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

316 
from this[THEN conjunct1] this[THEN conjunct2, THEN conjunct1] this[THEN conjunct2, THEN conjunct2, THEN conjunct1] this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct1] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

317 
this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct2] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

318 
show ?summable and ?pos and ?neg and ?f and ?g . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

319 
qed 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

320 

29164  321 
subsection {* TermbyTerm Differentiability of Power Series *} 
23043  322 

323 
definition 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

324 
diffs :: "(nat => 'a::ring_1) => nat => 'a" where 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

325 
"diffs c = (%n. of_nat (Suc n) * c(Suc n))" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

326 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

327 
text{*Lemma about distributing negation over it*} 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

328 
lemma diffs_minus: "diffs (%n.  c n) = (%n.  diffs c n)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

329 
by (simp add: diffs_def) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

330 

29163  331 
lemma sums_Suc_imp: 
332 
assumes f: "f 0 = 0" 

333 
shows "(\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s" 

334 
unfolding sums_def 

335 
apply (rule LIMSEQ_imp_Suc) 

336 
apply (subst setsum_shift_lb_Suc0_0_upt [where f=f, OF f, symmetric]) 

337 
apply (simp only: setsum_shift_bounds_Suc_ivl) 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

338 
done 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

339 

15229  340 
lemma diffs_equiv: 
341 
"summable (%n. (diffs c)(n) * (x ^ n)) ==> 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

342 
(%n. of_nat n * c(n) * (x ^ (n  Suc 0))) sums 
15546  343 
(\<Sum>n. (diffs c)(n) * (x ^ n))" 
29163  344 
unfolding diffs_def 
345 
apply (drule summable_sums) 

346 
apply (rule sums_Suc_imp, simp_all) 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

347 
done 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

348 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

349 
lemma lemma_termdiff1: 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

350 
fixes z :: "'a :: {recpower,comm_ring}" shows 
15539  351 
"(\<Sum>p=0..<m. (((z + h) ^ (m  p)) * (z ^ p))  (z ^ m)) = 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

352 
(\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m  p))  (z ^ (m  p))))" 
29667  353 
by(auto simp add: algebra_simps power_add [symmetric] cong: strong_setsum_cong) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

354 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

355 
lemma sumr_diff_mult_const2: 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

356 
"setsum f {0..<n}  of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i  r)" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

357 
by (simp add: setsum_subtractf) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

358 

15229  359 
lemma lemma_termdiff2: 
23112
2bc882fbe51c
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents:
23097
diff
changeset

360 
fixes h :: "'a :: {recpower,field}" 
20860  361 
assumes h: "h \<noteq> 0" shows 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

362 
"((z + h) ^ n  z ^ n) / h  of_nat n * z ^ (n  Suc 0) = 
20860  363 
h * (\<Sum>p=0..< n  Suc 0. \<Sum>q=0..< n  Suc 0  p. 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

364 
(z + h) ^ q * z ^ (n  2  q))" (is "?lhs = ?rhs") 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

365 
apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h) 
20860  366 
apply (simp add: right_diff_distrib diff_divide_distrib h) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

367 
apply (simp add: mult_assoc [symmetric]) 
20860  368 
apply (cases "n", simp) 
369 
apply (simp add: lemma_realpow_diff_sumr2 h 

370 
right_diff_distrib [symmetric] mult_assoc 

30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30082
diff
changeset

371 
del: power_Suc setsum_op_ivl_Suc of_nat_Suc) 
20860  372 
apply (subst lemma_realpow_rev_sumr) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

373 
apply (subst sumr_diff_mult_const2) 
20860  374 
apply simp 
375 
apply (simp only: lemma_termdiff1 setsum_right_distrib) 

376 
apply (rule setsum_cong [OF refl]) 

15539  377 
apply (simp add: diff_minus [symmetric] less_iff_Suc_add) 
20860  378 
apply (clarify) 
379 
apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac 

30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30082
diff
changeset

380 
del: setsum_op_ivl_Suc power_Suc) 
20860  381 
apply (subst mult_assoc [symmetric], subst power_add [symmetric]) 
382 
apply (simp add: mult_ac) 

383 
done 

384 

385 
lemma real_setsum_nat_ivl_bounded2: 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

386 
fixes K :: "'a::ordered_semidom" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

387 
assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

388 
assumes K: "0 \<le> K" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

389 
shows "setsum f {0..<nk} \<le> of_nat n * K" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

390 
apply (rule order_trans [OF setsum_mono]) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

391 
apply (rule f, simp) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

392 
apply (simp add: mult_right_mono K) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

393 
done 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

394 

15229  395 
lemma lemma_termdiff3: 
23112
2bc882fbe51c
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents:
23097
diff
changeset

396 
fixes h z :: "'a::{real_normed_field,recpower}" 
20860  397 
assumes 1: "h \<noteq> 0" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

398 
assumes 2: "norm z \<le> K" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

399 
assumes 3: "norm (z + h) \<le> K" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

400 
shows "norm (((z + h) ^ n  z ^ n) / h  of_nat n * z ^ (n  Suc 0)) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

401 
\<le> of_nat n * of_nat (n  Suc 0) * K ^ (n  2) * norm h" 
20860  402 
proof  
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

403 
have "norm (((z + h) ^ n  z ^ n) / h  of_nat n * z ^ (n  Suc 0)) = 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

404 
norm (\<Sum>p = 0..<n  Suc 0. \<Sum>q = 0..<n  Suc 0  p. 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

405 
(z + h) ^ q * z ^ (n  2  q)) * norm h" 
20860  406 
apply (subst lemma_termdiff2 [OF 1]) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

407 
apply (subst norm_mult) 
20860  408 
apply (rule mult_commute) 
409 
done 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

410 
also have "\<dots> \<le> of_nat n * (of_nat (n  Suc 0) * K ^ (n  2)) * norm h" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

411 
proof (rule mult_right_mono [OF _ norm_ge_zero]) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

412 
from norm_ge_zero 2 have K: "0 \<le> K" by (rule order_trans) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

413 
have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n" 
20860  414 
apply (erule subst) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

415 
apply (simp only: norm_mult norm_power power_add) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

416 
apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K) 
20860  417 
done 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

418 
show "norm (\<Sum>p = 0..<n  Suc 0. \<Sum>q = 0..<n  Suc 0  p. 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

419 
(z + h) ^ q * z ^ (n  2  q)) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

420 
\<le> of_nat n * (of_nat (n  Suc 0) * K ^ (n  2))" 
20860  421 
apply (intro 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

422 
order_trans [OF norm_setsum] 
20860  423 
real_setsum_nat_ivl_bounded2 
424 
mult_nonneg_nonneg 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

425 
zero_le_imp_of_nat 
20860  426 
zero_le_power K) 
427 
apply (rule le_Kn, simp) 

428 
done 

429 
qed 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

430 
also have "\<dots> = of_nat n * of_nat (n  Suc 0) * K ^ (n  2) * norm h" 
20860  431 
by (simp only: mult_assoc) 
432 
finally show ?thesis . 

433 
qed 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

434 

20860  435 
lemma lemma_termdiff4: 
23112
2bc882fbe51c
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents:
23097
diff
changeset

436 
fixes f :: "'a::{real_normed_field,recpower} \<Rightarrow> 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

437 
'b::real_normed_vector" 
20860  438 
assumes k: "0 < (k::real)" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

439 
assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h" 
20860  440 
shows "f  0 > 0" 
29163  441 
unfolding LIM_def diff_0_right 
442 
proof (safe) 

443 
let ?h = "of_real (k / 2)::'a" 

444 
have "?h \<noteq> 0" and "norm ?h < k" using k by simp_all 

445 
hence "norm (f ?h) \<le> K * norm ?h" by (rule le) 

446 
hence "0 \<le> K * norm ?h" by (rule order_trans [OF norm_ge_zero]) 

447 
hence zero_le_K: "0 \<le> K" using k by (simp add: zero_le_mult_iff) 

448 

20860  449 
fix r::real assume r: "0 < r" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

450 
show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" 
20860  451 
proof (cases) 
452 
assume "K = 0" 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

453 
with k r le have "0 < k \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < k \<longrightarrow> norm (f x) < r)" 
20860  454 
by simp 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

455 
thus "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" .. 
20860  456 
next 
457 
assume K_neq_zero: "K \<noteq> 0" 

458 
with zero_le_K have K: "0 < K" by simp 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

459 
show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" 
20860  460 
proof (rule exI, safe) 
461 
from k r K show "0 < min k (r * inverse K / 2)" 

462 
by (simp add: mult_pos_pos positive_imp_inverse_positive) 

463 
next 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

464 
fix x::'a 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

465 
assume x1: "x \<noteq> 0" and x2: "norm x < min k (r * inverse K / 2)" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

466 
from x2 have x3: "norm x < k" and x4: "norm x < r * inverse K / 2" 
20860  467 
by simp_all 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

468 
from x1 x3 le have "norm (f x) \<le> K * norm x" by simp 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

469 
also from x4 K have "K * norm x < K * (r * inverse K / 2)" 
20860  470 
by (rule mult_strict_left_mono) 
471 
also have "\<dots> = r / 2" 

472 
using K_neq_zero by simp 

473 
also have "r / 2 < r" 

474 
using r by simp 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

475 
finally show "norm (f x) < r" . 
20860  476 
qed 
477 
qed 

478 
qed 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

479 

15229  480 
lemma lemma_termdiff5: 
23112
2bc882fbe51c
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents:
23097
diff
changeset

481 
fixes g :: "'a::{recpower,real_normed_field} \<Rightarrow> 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

482 
nat \<Rightarrow> 'b::banach" 
20860  483 
assumes k: "0 < (k::real)" 
484 
assumes f: "summable f" 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

485 
assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h" 
20860  486 
shows "(\<lambda>h. suminf (g h))  0 > 0" 
487 
proof (rule lemma_termdiff4 [OF k]) 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

488 
fix h::'a assume "h \<noteq> 0" and "norm h < k" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

489 
hence A: "\<forall>n. norm (g h n) \<le> f n * norm h" 
20860  490 
by (simp add: le) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

491 
hence "\<exists>N. \<forall>n\<ge>N. norm (norm (g h n)) \<le> f n * norm h" 
20860  492 
by simp 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

493 
moreover from f have B: "summable (\<lambda>n. f n * norm h)" 
20860  494 
by (rule summable_mult2) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

495 
ultimately have C: "summable (\<lambda>n. norm (g h n))" 
20860  496 
by (rule summable_comparison_test) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

497 
hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

498 
by (rule summable_norm) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

499 
also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)" 
20860  500 
by (rule summable_le) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

501 
also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h" 
20860  502 
by (rule suminf_mult2 [symmetric]) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

503 
finally show "norm (suminf (g h)) \<le> suminf f * norm h" . 
20860  504 
qed 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

505 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

506 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

507 
text{* FIXME: Long proofs*} 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

508 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

509 
lemma termdiffs_aux: 
23112
2bc882fbe51c
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents:
23097
diff
changeset

510 
fixes x :: "'a::{recpower,real_normed_field,banach}" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

511 
assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

512 
assumes 2: "norm x < norm K" 
20860  513 
shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n  x ^ n) / h 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

514 
 of_nat n * x ^ (n  Suc 0)))  0 > 0" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

515 
proof  
20860  516 
from dense [OF 2] 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

517 
obtain r where r1: "norm x < r" and r2: "r < norm K" by fast 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

518 
from norm_ge_zero r1 have r: "0 < r" 
20860  519 
by (rule order_le_less_trans) 
520 
hence r_neq_0: "r \<noteq> 0" by simp 

521 
show ?thesis 

20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

522 
proof (rule lemma_termdiff5) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

523 
show "0 < r  norm x" using r1 by simp 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

524 
next 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

525 
from r r2 have "norm (of_real r::'a) < norm K" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

526 
by simp 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

527 
with 1 have "summable (\<lambda>n. norm (diffs (diffs c) n * (of_real r ^ n)))" 
20860  528 
by (rule powser_insidea) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

529 
hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. norm (c n))) n * r ^ n)" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

530 
using r 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

531 
by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

532 
hence "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n  Suc 0))" 
20860  533 
by (rule diffs_equiv [THEN sums_summable]) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

534 
also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n  Suc 0)) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

535 
= (\<lambda>n. diffs (%m. of_nat (m  Suc 0) * norm (c m) * inverse r) n * (r ^ n))" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

536 
apply (rule ext) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

537 
apply (simp add: diffs_def) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

538 
apply (case_tac n, simp_all add: r_neq_0) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

539 
done 
20860  540 
finally have "summable 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

541 
(\<lambda>n. of_nat n * (of_nat (n  Suc 0) * norm (c n) * inverse r) * r ^ (n  Suc 0))" 
20860  542 
by (rule diffs_equiv [THEN sums_summable]) 
543 
also have 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

544 
"(\<lambda>n. of_nat n * (of_nat (n  Suc 0) * norm (c n) * inverse r) * 
20860  545 
r ^ (n  Suc 0)) = 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

546 
(\<lambda>n. norm (c n) * of_nat n * of_nat (n  Suc 0) * r ^ (n  2))" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

547 
apply (rule ext) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

548 
apply (case_tac "n", simp) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

549 
apply (case_tac "nat", simp) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

550 
apply (simp add: r_neq_0) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

551 
done 
20860  552 
finally show 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

553 
"summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n  Suc 0) * r ^ (n  2))" . 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

554 
next 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

555 
fix h::'a and n::nat 
20860  556 
assume h: "h \<noteq> 0" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

557 
assume "norm h < r  norm x" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

558 
hence "norm x + norm h < r" by simp 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

559 
with norm_triangle_ineq have xh: "norm (x + h) < r" 
20860  560 
by (rule order_le_less_trans) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

561 
show "norm (c n * (((x + h) ^ n  x ^ n) / h  of_nat n * x ^ (n  Suc 0))) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

562 
\<le> norm (c n) * of_nat n * of_nat (n  Suc 0) * r ^ (n  2) * norm h" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

563 
apply (simp only: norm_mult mult_assoc) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

564 
apply (rule mult_left_mono [OF _ norm_ge_zero]) 
20860  565 
apply (simp (no_asm) add: mult_assoc [symmetric]) 
566 
apply (rule lemma_termdiff3) 

567 
apply (rule h) 

568 
apply (rule r1 [THEN order_less_imp_le]) 

569 
apply (rule xh [THEN order_less_imp_le]) 

570 
done 

20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

571 
qed 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

572 
qed 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset

573 

20860  574 
lemma termdiffs: 
23112
2bc882fbe51c
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents:
23097
diff
changeset

575 
fixes K x :: "'a::{recpower,real_normed_field,banach}" 
20860  576 
assumes 1: "summable (\<lambda>n. c n * K ^ n)" 
577 
assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)" 

578 
assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)" 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

579 
assumes 4: "norm x < norm K" 
20860  580 
shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)" 
29163  581 
unfolding deriv_def 
582 
proof (rule LIM_zero_cancel) 

20860  583 
show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n)  suminf (\<lambda>n. c n * x ^ n)) / h 
584 
 suminf (\<lambda>n. diffs c n * x ^ n))  0 > 0" 

585 
proof (rule LIM_equal2) 

29163  586 
show "0 < norm K  norm x" using 4 by (simp add: less_diff_eq) 
20860  587 
next 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

588 
fix h :: 'a 
20860  589 
assume "h \<noteq> 0" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

590 
assume "norm (h  0) < norm K  norm x" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

591 
hence "norm x + norm h < norm K" by simp 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

592 
hence 5: "norm (x + h) < norm K" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

593 
by (rule norm_triangle_ineq [THEN order_le_less_trans]) 
20860  594 
have A: "summable (\<lambda>n. c n * x ^ n)" 
595 
by (rule powser_inside [OF 1 4]) 

596 
have B: "summable (\<lambda>n. c n * (x + h) ^ n)" 

597 
by (rule powser_inside [OF 1 5]) 

598 
have C: "summable (\<lambda>n. diffs c n * x ^ n)" 

599 
by (rule powser_inside [OF 2 4]) 

600 
show "((\<Sum>n. c n * (x + h) ^ n)  (\<Sum>n. c n * x ^ n)) / h 

601 
 (\<Sum>n. diffs c n * x ^ n) = 

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

602 
(\<Sum>n. c n * (((x + h) ^ n  x ^ n) / h  of_nat n * x ^ (n  Suc 0)))" 
20860  603 
apply (subst sums_unique [OF diffs_equiv [OF C]]) 
604 
apply (subst suminf_diff [OF B A]) 

605 
apply (subst suminf_divide [symmetric]) 

606 
apply (rule summable_diff [OF B A]) 

607 
apply (subst suminf_diff) 

608 
apply (rule summable_divide) 

609 
apply (rule summable_diff [OF B A]) 

610 
apply (rule sums_summable [OF diffs_equiv [OF C]]) 

29163  611 
apply (rule arg_cong [where f="suminf"], rule ext) 
29667  612 
apply (simp add: algebra_simps) 
20860  613 
done 
614 
next 

615 
show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n  x ^ n) / h  

23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

616 
of_nat n * x ^ (n  Suc 0)))  0 > 0" 
20860  617 
by (rule termdiffs_aux [OF 3 4]) 
618 
qed 

619 
qed 

620 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

621 

29695  622 
subsection{* Some properties of factorials *} 
623 

624 
lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0" 

625 
by auto 

626 

627 
lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)" 

628 
by auto 

629 

630 
lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)" 

631 
by simp 

632 

633 
lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))" 

634 
by (auto simp add: positive_imp_inverse_positive) 

635 

636 
lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))" 

637 
by (auto intro: order_less_imp_le) 

638 

29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

639 
subsection {* Derivability of power series *} 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

640 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

641 
lemma DERIV_series': fixes f :: "real \<Rightarrow> nat \<Rightarrow> real" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

642 
assumes DERIV_f: "\<And> n. DERIV (\<lambda> x. f x n) x0 :> (f' x0 n)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

643 
and allf_summable: "\<And> x. x \<in> {a <..< b} \<Longrightarrow> summable (f x)" and x0_in_I: "x0 \<in> {a <..< b}" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

644 
and "summable (f' x0)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

645 
and "summable L" and L_def: "\<And> n x y. \<lbrakk> x \<in> { a <..< b} ; y \<in> { a <..< b} \<rbrakk> \<Longrightarrow> \<bar> f x n  f y n \<bar> \<le> L n * \<bar> x  y \<bar>" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

646 
shows "DERIV (\<lambda> x. suminf (f x)) x0 :> (suminf (f' x0))" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

647 
unfolding deriv_def 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

648 
proof (rule LIM_I) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

649 
fix r :: real assume "0 < r" hence "0 < r/3" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

650 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

651 
obtain N_L where N_L: "\<And> n. N_L \<le> n \<Longrightarrow> \<bar> \<Sum> i. L (i + n) \<bar> < r/3" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

652 
using suminf_exist_split[OF `0 < r/3` `summable L`] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

653 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

654 
obtain N_f' where N_f': "\<And> n. N_f' \<le> n \<Longrightarrow> \<bar> \<Sum> i. f' x0 (i + n) \<bar> < r/3" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

655 
using suminf_exist_split[OF `0 < r/3` `summable (f' x0)`] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

656 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

657 
let ?N = "Suc (max N_L N_f')" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

658 
have "\<bar> \<Sum> i. f' x0 (i + ?N) \<bar> < r/3" (is "?f'_part < r/3") and 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

659 
L_estimate: "\<bar> \<Sum> i. L (i + ?N) \<bar> < r/3" using N_L[of "?N"] and N_f' [of "?N"] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

660 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

661 
let "?diff i x" = "(f (x0 + x) i  f x0 i) / x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

662 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

663 
let ?r = "r / (3 * real ?N)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

664 
have "0 < 3 * real ?N" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

665 
from divide_pos_pos[OF `0 < r` this] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

666 
have "0 < ?r" . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

667 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

668 
let "?s n" = "SOME s. 0 < s \<and> (\<forall> x. x \<noteq> 0 \<and> \<bar> x \<bar> < s \<longrightarrow> \<bar> ?diff n x  f' x0 n \<bar> < ?r)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

669 
def S' \<equiv> "Min (?s ` { 0 ..< ?N })" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

670 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

671 
have "0 < S'" unfolding S'_def 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

672 
proof (rule iffD2[OF Min_gr_iff]) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

673 
show "\<forall> x \<in> (?s ` { 0 ..< ?N }). 0 < x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

674 
proof (rule ballI) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

675 
fix x assume "x \<in> ?s ` {0..<?N}" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

676 
then obtain n where "x = ?s n" and "n \<in> {0..<?N}" using image_iff[THEN iffD1] by blast 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

677 
from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

678 
obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x  f' x0 n\<bar> < ?r)" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

679 
have "0 < ?s n" by (rule someI2[where a=s], auto simp add: s_bound) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

680 
thus "0 < x" unfolding `x = ?s n` . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

681 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

682 
qed auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

683 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

684 
def S \<equiv> "min (min (x0  a) (b  x0)) S'" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

685 
hence "0 < S" and S_a: "S \<le> x0  a" and S_b: "S \<le> b  x0" and "S \<le> S'" using x0_in_I and `0 < S'` 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

686 
by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

687 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

688 
{ fix x assume "x \<noteq> 0" and "\<bar> x \<bar> < S" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

689 
hence x_in_I: "x0 + x \<in> { a <..< b }" using S_a S_b by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

690 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

691 
note diff_smbl = summable_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

692 
note div_smbl = summable_divide[OF diff_smbl] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

693 
note all_smbl = summable_diff[OF div_smbl `summable (f' x0)`] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

694 
note ign = summable_ignore_initial_segment[where k="?N"] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

695 
note diff_shft_smbl = summable_diff[OF ign[OF allf_summable[OF x_in_I]] ign[OF allf_summable[OF x0_in_I]]] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

696 
note div_shft_smbl = summable_divide[OF diff_shft_smbl] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

697 
note all_shft_smbl = summable_diff[OF div_smbl ign[OF `summable (f' x0)`]] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

698 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

699 
{ fix n 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

700 
have "\<bar> ?diff (n + ?N) x \<bar> \<le> L (n + ?N) * \<bar> (x0 + x)  x0 \<bar> / \<bar> x \<bar>" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

701 
using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero] unfolding abs_divide . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

702 
hence "\<bar> ( \<bar> ?diff (n + ?N) x \<bar>) \<bar> \<le> L (n + ?N)" using `x \<noteq> 0` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

703 
} note L_ge = summable_le2[OF allI[OF this] ign[OF `summable L`]] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

704 
from order_trans[OF summable_rabs[OF conjunct1[OF L_ge]] L_ge[THEN conjunct2]] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

705 
have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))" . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

706 
hence "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3") using L_estimate by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

707 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

708 
have "\<bar>\<Sum>n \<in> { 0 ..< ?N}. ?diff n x  f' x0 n \<bar> \<le> (\<Sum>n \<in> { 0 ..< ?N}. \<bar>?diff n x  f' x0 n \<bar>)" .. 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

709 
also have "\<dots> < (\<Sum>n \<in> { 0 ..< ?N}. ?r)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

710 
proof (rule setsum_strict_mono) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

711 
fix n assume "n \<in> { 0 ..< ?N}" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

712 
have "\<bar> x \<bar> < S" using `\<bar> x \<bar> < S` . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

713 
also have "S \<le> S'" using `S \<le> S'` . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

714 
also have "S' \<le> ?s n" unfolding S'_def 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

715 
proof (rule Min_le_iff[THEN iffD2]) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

716 
have "?s n \<in> (?s ` {0..<?N}) \<and> ?s n \<le> ?s n" using `n \<in> { 0 ..< ?N}` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

717 
thus "\<exists> a \<in> (?s ` {0..<?N}). a \<le> ?s n" by blast 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

718 
qed auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

719 
finally have "\<bar> x \<bar> < ?s n" . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

720 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

721 
from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def diff_0_right, unfolded some_eq_ex[symmetric], THEN conjunct2] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

722 
have "\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < ?s n \<longrightarrow> \<bar>?diff n x  f' x0 n\<bar> < ?r" . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

723 
with `x \<noteq> 0` and `\<bar>x\<bar> < ?s n` 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

724 
show "\<bar>?diff n x  f' x0 n\<bar> < ?r" by blast 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

725 
qed auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

726 
also have "\<dots> = of_nat (card {0 ..< ?N}) * ?r" by (rule setsum_constant) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

727 
also have "\<dots> = real ?N * ?r" unfolding real_eq_of_nat by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

728 
also have "\<dots> = r/3" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

729 
finally have "\<bar>\<Sum>n \<in> { 0 ..< ?N}. ?diff n x  f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

730 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

731 
from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

732 
have "\<bar> (suminf (f (x0 + x))  (suminf (f x0))) / x  suminf (f' x0) \<bar> = 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

733 
\<bar> \<Sum>n. ?diff n x  f' x0 n \<bar>" unfolding suminf_diff[OF div_smbl `summable (f' x0)`, symmetric] using suminf_divide[OF diff_smbl, symmetric] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

734 
also have "\<dots> \<le> ?diff_part + \<bar> (\<Sum>n. ?diff (n + ?N) x)  (\<Sum> n. f' x0 (n + ?N)) \<bar>" unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"] unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]] by (rule abs_triangle_ineq) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

735 
also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part" using abs_triangle_ineq4 by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

736 
also have "\<dots> < r /3 + r/3 + r/3" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

737 
using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

738 
finally have "\<bar> (suminf (f (x0 + x))  (suminf (f x0))) / x  suminf (f' x0) \<bar> < r" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

739 
by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

740 
} thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x  0) < s \<longrightarrow> 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

741 
norm (((\<Sum>n. f (x0 + x) n)  (\<Sum>n. f x0 n)) / x  (\<Sum>n. f' x0 n)) < r" using `0 < S` 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

742 
unfolding real_norm_def diff_0_right by blast 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

743 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

744 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

745 
lemma DERIV_power_series': fixes f :: "nat \<Rightarrow> real" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

746 
assumes converges: "\<And> x. x \<in> {R <..< R} \<Longrightarrow> summable (\<lambda> n. f n * real (Suc n) * x^n)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

747 
and x0_in_I: "x0 \<in> {R <..< R}" and "0 < R" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

748 
shows "DERIV (\<lambda> x. (\<Sum> n. f n * x^(Suc n))) x0 :> (\<Sum> n. f n * real (Suc n) * x0^n)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

749 
(is "DERIV (\<lambda> x. (suminf (?f x))) x0 :> (suminf (?f' x0))") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

750 
proof  
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

751 
{ fix R' assume "0 < R'" and "R' < R" and "R' < x0" and "x0 < R'" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

752 
hence "x0 \<in> {R' <..< R'}" and "R' \<in> {R <..< R}" and "x0 \<in> {R <..< R}" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

753 
have "DERIV (\<lambda> x. (suminf (?f x))) x0 :> (suminf (?f' x0))" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

754 
proof (rule DERIV_series') 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

755 
show "summable (\<lambda> n. \<bar>f n * real (Suc n) * R'^n\<bar>)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

756 
proof  
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

757 
have "(R' + R) / 2 < R" and "0 < (R' + R) / 2" using `0 < R'` `0 < R` `R' < R` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

758 
hence in_Rball: "(R' + R) / 2 \<in> {R <..< R}" using `R' < R` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

759 
have "norm R' < norm ((R' + R) / 2)" using `0 < R'` `0 < R` `R' < R` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

760 
from powser_insidea[OF converges[OF in_Rball] this] show ?thesis by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

761 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

762 
{ fix n x y assume "x \<in> {R' <..< R'}" and "y \<in> {R' <..< R'}" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

763 
show "\<bar>?f x n  ?f y n\<bar> \<le> \<bar>f n * real (Suc n) * R'^n\<bar> * \<bar>xy\<bar>" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

764 
proof  
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

765 
have "\<bar>f n * x ^ (Suc n)  f n * y ^ (Suc n)\<bar> = (\<bar>f n\<bar> * \<bar>xy\<bar>) * \<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n  p)\<bar>" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

766 
unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

767 
also have "\<dots> \<le> (\<bar>f n\<bar> * \<bar>xy\<bar>) * (\<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

768 
proof (rule mult_left_mono) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

769 
have "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n  p)\<bar> \<le> (\<Sum>p = 0..<Suc n. \<bar>x ^ p * y ^ (n  p)\<bar>)" by (rule setsum_abs) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

770 
also have "\<dots> \<le> (\<Sum>p = 0..<Suc n. R' ^ n)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

771 
proof (rule setsum_mono) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

772 
fix p assume "p \<in> {0..<Suc n}" hence "p \<le> n" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

773 
{ fix n fix x :: real assume "x \<in> {R'<..<R'}" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

774 
hence "\<bar>x\<bar> \<le> R'" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

775 
hence "\<bar>x^n\<bar> \<le> R'^n" unfolding power_abs by (rule power_mono, auto) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

776 
} from mult_mono[OF this[OF `x \<in> {R'<..<R'}`, of p] this[OF `y \<in> {R'<..<R'}`, of "np"]] `0 < R'` 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

777 
have "\<bar>x^p * y^(np)\<bar> \<le> R'^p * R'^(np)" unfolding abs_mult by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

778 
thus "\<bar>x^p * y^(np)\<bar> \<le> R'^n" unfolding power_add[symmetric] using `p \<le> n` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

779 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

780 
also have "\<dots> = real (Suc n) * R' ^ n" unfolding setsum_constant card_atLeastLessThan real_of_nat_def by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

781 
finally show "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n  p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>" unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

782 
show "0 \<le> \<bar>f n\<bar> * \<bar>x  y\<bar>" unfolding abs_mult[symmetric] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

783 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

784 
also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x  y\<bar>" unfolding abs_mult real_mult_assoc[symmetric] by algebra 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

785 
finally show ?thesis . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

786 
qed } 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

787 
{ fix n 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

788 
from DERIV_pow[of "Suc n" x0, THEN DERIV_cmult[where c="f n"]] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

789 
show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)" unfolding real_mult_assoc by auto } 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

790 
{ fix x assume "x \<in> {R' <..< R'}" hence "R' \<in> {R <..< R}" and "norm x < norm R'" using assms `R' < R` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

791 
have "summable (\<lambda> n. f n * x^n)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

792 
proof (rule summable_le2[THEN conjunct1, OF _ powser_insidea[OF converges[OF `R' \<in> {R <..< R}`] `norm x < norm R'`]], rule allI) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

793 
fix n 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

794 
have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)" by (rule mult_left_mono, auto) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

795 
show "\<bar>f n * x ^ n\<bar> \<le> norm (f n * real (Suc n) * x ^ n)" unfolding real_norm_def abs_mult 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

796 
by (rule mult_right_mono, auto simp add: le[unfolded mult_1_right]) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

797 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

798 
from this[THEN summable_mult2[where c=x], unfolded real_mult_assoc, unfolded real_mult_commute] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

799 
show "summable (?f x)" by auto } 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

800 
show "summable (?f' x0)" using converges[OF `x0 \<in> {R <..< R}`] . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

801 
show "x0 \<in> {R' <..< R'}" using `x0 \<in> {R' <..< R'}` . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

802 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

803 
} note for_subinterval = this 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

804 
let ?R = "(R + \<bar>x0\<bar>) / 2" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

805 
have "\<bar>x0\<bar> < ?R" using assms by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

806 
hence " ?R < x0" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

807 
proof (cases "x0 < 0") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

808 
case True 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

809 
hence " x0 < ?R" using `\<bar>x0\<bar> < ?R` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

810 
thus ?thesis unfolding neg_less_iff_less[symmetric, of " x0"] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

811 
next 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

812 
case False 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

813 
have " ?R < 0" using assms by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

814 
also have "\<dots> \<le> x0" using False by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

815 
finally show ?thesis . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

816 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

817 
hence "0 < ?R" "?R < R" " ?R < x0" and "x0 < ?R" using assms by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

818 
from for_subinterval[OF this] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

819 
show ?thesis . 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

820 
qed 
29695  821 

29164  822 
subsection {* Exponential Function *} 
23043  823 

824 
definition 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

825 
exp :: "'a \<Rightarrow> 'a::{recpower,real_normed_field,banach}" where 
25062  826 
"exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))" 
23043  827 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

828 
lemma summable_exp_generic: 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

829 
fixes x :: "'a::{real_normed_algebra_1,recpower,banach}" 
25062  830 
defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

831 
shows "summable S" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

832 
proof  
25062  833 
have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)" 
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30082
diff
changeset

834 
unfolding S_def by (simp del: mult_Suc) 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

835 
obtain r :: real where r0: "0 < r" and r1: "r < 1" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

836 
using dense [OF zero_less_one] by fast 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

837 
obtain N :: nat where N: "norm x < real N * r" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

838 
using reals_Archimedean3 [OF r0] by fast 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

839 
from r1 show ?thesis 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

840 
proof (rule ratio_test [rule_format]) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

841 
fix n :: nat 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

842 
assume n: "N \<le> n" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

843 
have "norm x \<le> real N * r" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

844 
using N by (rule order_less_imp_le) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

845 
also have "real N * r \<le> real (Suc n) * r" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

846 
using r0 n by (simp add: mult_right_mono) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

847 
finally have "norm x * norm (S n) \<le> real (Suc n) * r * norm (S n)" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

848 
using norm_ge_zero by (rule mult_right_mono) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

849 
hence "norm (x * S n) \<le> real (Suc n) * r * norm (S n)" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

850 
by (rule order_trans [OF norm_mult_ineq]) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

851 
hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

852 
by (simp add: pos_divide_le_eq mult_ac) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

853 
thus "norm (S (Suc n)) \<le> r * norm (S n)" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

854 
by (simp add: S_Suc norm_scaleR inverse_eq_divide) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

855 
qed 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

856 
qed 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

857 

4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

858 
lemma summable_norm_exp: 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

859 
fixes x :: "'a::{real_normed_algebra_1,recpower,banach}" 
25062  860 
shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

861 
proof (rule summable_norm_comparison_test [OF exI, rule_format]) 
25062  862 
show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

863 
by (rule summable_exp_generic) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

864 
next 
25062  865 
fix n show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

866 
by (simp add: norm_scaleR norm_power_ineq) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

867 
qed 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

868 

23043  869 
lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

870 
by (insert summable_exp_generic [where x=x], simp) 
23043  871 

25062  872 
lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

873 
unfolding exp_def by (rule summable_exp_generic [THEN summable_sums]) 
23043  874 

875 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

876 
lemma exp_fdiffs: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

877 
"diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))" 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23413
diff
changeset

878 
by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def of_nat_mult 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

879 
del: mult_Suc of_nat_Suc) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

880 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

881 
lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

882 
by (simp add: diffs_def) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

883 

25062  884 
lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

885 
by (auto intro!: ext simp add: exp_def) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

886 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

887 
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" 
15229  888 
apply (simp add: exp_def) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

889 
apply (subst lemma_exp_ext) 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

890 
apply (subgoal_tac "DERIV (\<lambda>u. \<Sum>n. of_real (inverse (real (fact n))) * u ^ n) x :> (\<Sum>n. diffs (\<lambda>n. of_real (inverse (real (fact n)))) n * x ^ n)") 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

891 
apply (rule_tac [2] K = "of_real (1 + norm x)" in termdiffs) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

892 
apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

893 
apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+ 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

894 
apply (simp del: of_real_add) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

895 
done 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

896 

23045
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

897 
lemma isCont_exp [simp]: "isCont exp x" 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

898 
by (rule DERIV_exp [THEN DERIV_isCont]) 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

899 

95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

900 

29167  901 
subsubsection {* Properties of the Exponential Function *} 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

902 

23278  903 
lemma powser_zero: 
904 
fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1,recpower}" 

905 
shows "(\<Sum>n. f n * 0 ^ n) = f 0" 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

906 
proof  
23278  907 
have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

908 
by (rule sums_unique [OF series_zero], simp add: power_0_left) 
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset

909 
thus ?thesis unfolding One_nat_def by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

910 
qed 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

911 

23278  912 
lemma exp_zero [simp]: "exp 0 = 1" 
913 
unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero) 

914 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

915 
lemma setsum_cl_ivl_Suc2: 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

916 
"(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))" 
28069  917 
by (simp add: setsum_head_Suc setsum_shift_bounds_cl_Suc_ivl 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

918 
del: setsum_cl_ivl_Suc) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

919 

4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

920 
lemma exp_series_add: 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

921 
fixes x y :: "'a::{real_field,recpower}" 
25062  922 
defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

923 
shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n  i))" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

924 
proof (induct n) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

925 
case 0 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

926 
show ?case 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

927 
unfolding S_def by simp 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

928 
next 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

929 
case (Suc n) 
25062  930 
have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)" 
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30082
diff
changeset

931 
unfolding S_def by (simp del: mult_Suc) 
25062  932 
hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

933 
by simp 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

934 

25062  935 
have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

936 
by (simp only: times_S) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

937 
also have "\<dots> = (x + y) * (\<Sum>i=0..n. S x i * S y (ni))" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

938 
by (simp only: Suc) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

939 
also have "\<dots> = x * (\<Sum>i=0..n. S x i * S y (ni)) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

940 
+ y * (\<Sum>i=0..n. S x i * S y (ni))" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

941 
by (rule left_distrib) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

942 
also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (ni)) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

943 
+ (\<Sum>i=0..n. S x i * (y * S y (ni)))" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

944 
by (simp only: setsum_right_distrib mult_ac) 
25062  945 
also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (ni))) 
946 
+ (\<Sum>i=0..n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni)))" 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

947 
by (simp add: times_S Suc_diff_le) 
25062  948 
also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (ni))) = 
949 
(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc ni)))" 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

950 
by (subst setsum_cl_ivl_Suc2, simp) 
25062  951 
also have "(\<Sum>i=0..n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni))) = 
952 
(\<Sum>i=0..Suc n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni)))" 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

953 
by (subst setsum_cl_ivl_Suc, simp) 
25062  954 
also have "(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc ni))) + 
955 
(\<Sum>i=0..Suc n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni))) = 

956 
(\<Sum>i=0..Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc ni)))" 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

957 
by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric] 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

958 
real_of_nat_add [symmetric], simp) 
25062  959 
also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc ni))" 
23127  960 
by (simp only: scaleR_right.setsum) 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

961 
finally show 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

962 
"S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n  i))" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

963 
by (simp add: scaleR_cancel_left del: setsum_cl_ivl_Suc) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

964 
qed 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

965 

4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

966 
lemma exp_add: "exp (x + y) = exp x * exp y" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

967 
unfolding exp_def 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

968 
by (simp only: Cauchy_product summable_norm_exp exp_series_add) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

969 

29170  970 
lemma mult_exp_exp: "exp x * exp y = exp (x + y)" 
971 
by (rule exp_add [symmetric]) 

972 

23241  973 
lemma exp_of_real: "exp (of_real x) = of_real (exp x)" 
974 
unfolding exp_def 

975 
apply (subst of_real.suminf) 

976 
apply (rule summable_exp_generic) 

977 
apply (simp add: scaleR_conv_of_real) 

978 
done 

979 

29170  980 
lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0" 
981 
proof 

982 
have "exp x * exp ( x) = 1" by (simp add: mult_exp_exp) 

983 
also assume "exp x = 0" 

984 
finally show "False" by simp 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

985 
qed 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

986 

29170  987 
lemma exp_minus: "exp ( x) = inverse (exp x)" 
988 
by (rule inverse_unique [symmetric], simp add: mult_exp_exp) 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

989 

29170  990 
lemma exp_diff: "exp (x  y) = exp x / exp y" 
991 
unfolding diff_minus divide_inverse 

992 
by (simp add: exp_add exp_minus) 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

993 

29167  994 

995 
subsubsection {* Properties of the Exponential Function on Reals *} 

996 

29170  997 
text {* Comparisons of @{term "exp x"} with zero. *} 
29167  998 

999 
text{*Proof: because every exponential can be seen as a square.*} 

1000 
lemma exp_ge_zero [simp]: "0 \<le> exp (x::real)" 

1001 
proof  

1002 
have "0 \<le> exp (x/2) * exp (x/2)" by simp 

1003 
thus ?thesis by (simp add: exp_add [symmetric]) 

1004 
qed 

1005 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

1006 
lemma exp_gt_zero [simp]: "0 < exp (x::real)" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1007 
by (simp add: order_less_le) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1008 

29170  1009 
lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0" 
1010 
by (simp add: not_less) 

1011 

1012 
lemma not_exp_le_zero [simp]: "\<not> exp (x::real) \<le> 0" 

1013 
by (simp add: not_le) 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1014 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

1015 
lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x" 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1016 
by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1017 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1018 
lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" 
15251  1019 
apply (induct "n") 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1020 
apply (auto simp add: real_of_nat_Suc right_distrib exp_add mult_commute) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1021 
done 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1022 

29170  1023 
text {* Strict monotonicity of exponential. *} 
1024 

1025 
lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) ==> (1 + x) \<le> exp(x)" 

1026 
apply (drule order_le_imp_less_or_eq, auto) 

1027 
apply (simp add: exp_def) 

1028 
apply (rule real_le_trans) 

1029 
apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le) 

1030 
apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff) 

1031 
done 

1032 

1033 
lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x" 

1034 
proof  

1035 
assume x: "0 < x" 

1036 
hence "1 < 1 + x" by simp 

1037 
also from x have "1 + x \<le> exp x" 

1038 
by (simp add: exp_ge_add_one_self_aux) 

1039 
finally show ?thesis . 

1040 
qed 

1041 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1042 
lemma exp_less_mono: 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

1043 
fixes x y :: real 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1044 
assumes "x < y" shows "exp x < exp y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1045 
proof  
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1046 
from `x < y` have "0 < y  x" by simp 
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1047 
hence "1 < exp (y  x)" by (rule exp_gt_one) 
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1048 
hence "1 < exp y / exp x" by (simp only: exp_diff) 
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1049 
thus "exp x < exp y" by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1050 
qed 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1051 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

1052 
lemma exp_less_cancel: "exp (x::real) < exp y ==> x < y" 
29170  1053 
apply (simp add: linorder_not_le [symmetric]) 
1054 
apply (auto simp add: order_le_less exp_less_mono) 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1055 
done 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1056 

29170  1057 
lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1058 
by (auto intro: exp_less_mono exp_less_cancel) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1059 

29170  1060 
lemma exp_le_cancel_iff [iff]: "exp (x::real) \<le> exp y \<longleftrightarrow> x \<le> y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1061 
by (auto simp add: linorder_not_less [symmetric]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1062 

29170  1063 
lemma exp_inj_iff [iff]: "exp (x::real) = exp y \<longleftrightarrow> x = y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1064 
by (simp add: order_eq_iff) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1065 

29170  1066 
text {* Comparisons of @{term "exp x"} with one. *} 
1067 

1068 
lemma one_less_exp_iff [simp]: "1 < exp (x::real) \<longleftrightarrow> 0 < x" 

1069 
using exp_less_cancel_iff [where x=0 and y=x] by simp 

1070 

1071 
lemma exp_less_one_iff [simp]: "exp (x::real) < 1 \<longleftrightarrow> x < 0" 

1072 
using exp_less_cancel_iff [where x=x and y=0] by simp 

1073 

1074 
lemma one_le_exp_iff [simp]: "1 \<le> exp (x::real) \<longleftrightarrow> 0 \<le> x" 

1075 
using exp_le_cancel_iff [where x=0 and y=x] by simp 

1076 

1077 
lemma exp_le_one_iff [simp]: "exp (x::real) \<le> 1 \<longleftrightarrow> x \<le> 0" 

1078 
using exp_le_cancel_iff [where x=x and y=0] by simp 

1079 

1080 
lemma exp_eq_one_iff [simp]: "exp (x::real) = 1 \<longleftrightarrow> x = 0" 

1081 
using exp_inj_iff [where x=x and y=0] by simp 

1082 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

1083 
lemma lemma_exp_total: "1 \<le> y ==> \<exists>x. 0 \<le> x & x \<le> y  1 & exp(x::real) = y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1084 
apply (rule IVT) 
23045
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

1085 
apply (auto intro: isCont_exp simp add: le_diff_eq) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1086 
apply (subgoal_tac "1 + (y  1) \<le> exp (y  1)") 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1087 
apply simp 
17014
ad5ceb90877d
renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad
parents:
16924
diff
changeset

1088 
apply (rule exp_ge_add_one_self_aux, simp) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1089 
done 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1090 

23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

1091 
lemma exp_total: "0 < (y::real) ==> \<exists>x. exp x = y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1092 
apply (rule_tac x = 1 and y = y in linorder_cases) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1093 
apply (drule order_less_imp_le [THEN lemma_exp_total]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1094 
apply (rule_tac [2] x = 0 in exI) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1095 
apply (frule_tac [3] real_inverse_gt_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1096 
apply (drule_tac [4] order_less_imp_le [THEN lemma_exp_total], auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1097 
apply (rule_tac x = "x" in exI) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1098 
apply (simp add: exp_minus) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1099 
done 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1100 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1101 

29164  1102 
subsection {* Natural Logarithm *} 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1103 

23043  1104 
definition 
1105 
ln :: "real => real" where 

1106 
"ln x = (THE u. exp u = x)" 

1107 

1108 
lemma ln_exp [simp]: "ln (exp x) = x" 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1109 
by (simp add: ln_def) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1110 

22654
c2b6b5a9e136
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents:
22653
diff
changeset

1111 
lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x" 
c2b6b5a9e136
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents:
22653
diff
changeset

1112 
by (auto dest: exp_total) 
c2b6b5a9e136
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents:
22653
diff
changeset

1113 

29171  1114 
lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x" 
1115 
apply (rule iffI) 

1116 
apply (erule subst, rule exp_gt_zero) 

1117 
apply (erule exp_ln) 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1118 
done 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1119 

29171  1120 
lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y" 
1121 
by (erule subst, rule ln_exp) 

1122 

1123 
lemma ln_one [simp]: "ln 1 = 0" 

1124 
by (rule ln_unique, simp) 

1125 

1126 
lemma ln_mult: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x * y) = ln x + ln y" 

1127 
by (rule ln_unique, simp add: exp_add) 

1128 

1129 
lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) =  ln x" 

1130 
by (rule ln_unique, simp add: exp_minus) 

1131 

1132 
lemma ln_div: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x / y) = ln x  ln y" 

1133 
by (rule ln_unique, simp add: exp_diff) 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1134 

29171  1135 
lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x" 
1136 
by (rule ln_unique, simp add: exp_real_of_nat_mult) 

1137 

1138 
lemma ln_less_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y" 

1139 
by (subst exp_less_cancel_iff [symmetric], simp) 

1140 

1141 
lemma ln_le_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y" 

1142 
by (simp add: linorder_not_less [symmetric]) 

1143 

1144 
lemma ln_inj_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y" 

1145 
by (simp add: order_eq_iff) 

1146 

1147 
lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x" 

1148 
apply (rule exp_le_cancel_iff [THEN iffD1]) 

1149 
apply (simp add: exp_ge_add_one_self_aux) 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1150 
done 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1151 

29171  1152 
lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x" 
1153 
by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1154 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1155 
lemma ln_ge_zero [simp]: 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1156 
assumes x: "1 \<le> x" shows "0 \<le> ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1157 
proof  
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1158 
have "0 < x" using x by arith 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1159 
hence "exp 0 \<le> exp (ln x)" 
22915  1160 
by (simp add: x) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1161 
thus ?thesis by (simp only: exp_le_cancel_iff) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1162 
qed 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1163 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1164 
lemma ln_ge_zero_imp_ge_one: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1165 
assumes ln: "0 \<le> ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1166 
and x: "0 < x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1167 
shows "1 \<le> x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1168 
proof  
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1169 
from ln have "ln 1 \<le> ln x" by simp 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1170 
thus ?thesis by (simp add: x del: ln_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1171 
qed 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1172 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1173 
lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1174 
by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1175 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1176 
lemma ln_less_zero_iff [simp]: "0 < x ==> (ln x < 0) = (x < 1)" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1177 
by (insert ln_ge_zero_iff [of x], arith) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1178 

15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1179 
lemma ln_gt_zero: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1180 
assumes x: "1 < x" shows "0 < ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1181 
proof  
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1182 
have "0 < x" using x by arith 
22915  1183 
hence "exp 0 < exp (ln x)" by (simp add: x) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1184 
thus ?thesis by (simp only: exp_less_cancel_iff) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1185 
qed 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1186 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1187 
lemma ln_gt_zero_imp_gt_one: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1188 
assumes ln: "0 < ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1189 
and x: "0 < x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1190 
shows "1 < x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1191 
proof  
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1192 
from ln have "ln 1 < ln x" by simp 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1193 
thus ?thesis by (simp add: x del: ln_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1194 
qed 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1195 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1196 
lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1197 
by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1198 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1199 
lemma ln_eq_zero_iff [simp]: "0 < x ==> (ln x = 0) = (x = 1)" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1200 
by (insert ln_less_zero_iff [of x] ln_gt_zero_iff [of x], arith) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1201 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1202 
lemma ln_less_zero: "[ 0 < x; x < 1 ] ==> ln x < 0" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

1203 
by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1204 

89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1205 
lemma exp_ln_eq: "exp u = x ==> ln x = u" 
89840837108e
converting Hyperreal/Transcendental to Isar script
