author  noschinl 
Sat, 25 May 2013 13:59:08 +0200  
changeset 52139  40fe6b80b481 
parent 51641  cd05e9fcc63d 
child 53015  a1119cf551e8 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

1 
(* Title: HOL/Transcendental.thy 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

2 
Author: Jacques D. Fleuriot, University of Cambridge, University of Edinburgh 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

3 
Author: Lawrence C Paulson 
51527  4 
Author: Jeremy Avigad 
5 

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: 
31017  17 
fixes y :: "'a::monoid_mult" 
23082
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: 
31017  26 
fixes y :: "'a::{comm_semiring_0,monoid_mult}" shows 
41970  27 
"(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n  p)) = 
23082
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 
33549  30 
del: setsum_op_ivl_Suc) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

31 

15229  32 
lemma lemma_realpow_diff_sumr2: 
31017  33 
fixes y :: "'a::{comm_ring,monoid_mult}" shows 
41970  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) 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47489
diff
changeset

40 
apply (simp add: distrib_left del: setsum_op_ivl_Suc) 
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
33667
diff
changeset

41 
apply (subst mult_left_commute [of "x  y"]) 
23082
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: 
41970  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: 
44726  59 
fixes x z :: "'a::real_normed_field" 
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)" 
44726  70 
by (rule convergent_Cauchy) 
20849
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: 
31017  111 
fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" shows 
41970  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 
41970  117 
"(\<Sum> i = 0 ..< 2 * n. if even i then f i else g i) = 
29803
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) 
41970  121 
have "(\<Sum> i = 0 ..< 2 * Suc n. if even i then f i else g i) = 
29803
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 
41970  138 
have sum_eq: "?SUM (2 * (m div 2)) = setsum g { 0 ..< m div 2 }" 
29803
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`] . 
41970  166 
{ 
29803
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 
41550  169 
have if_eq: "\<And>B T E. (if \<not> B then T else E) = (if B then E else T)" 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

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`] . 
41970  172 
from this[unfolded sums_def, THEN LIMSEQ_Suc] 
29803
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] 
31148  176 
even_Suc Suc_m1 if_eq . 
29803
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" 
41970  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> 
29803
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 
41970  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" 
41970  206 
with `a > 0`[THEN LIMSEQ_D] 
29803
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 
51477
2990382dc066
clean up lemma_nest_unique and renamed to nested_sequence_unique
hoelzl
parents:
50347
diff
changeset

212 
show ?thesis by (rule nested_sequence_unique) 
41970  213 
qed 
29803
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 
41970  230 

29803
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 

41970  236 
with `?f > l`[THEN LIMSEQ_D] 
29803
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 

41970  239 
from `0 < r` `?g > l`[THEN LIMSEQ_D] 
29803
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") 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

246 
case True from even_nat_div_two_times_two[OF this] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

247 
have n_eq: "2 * (n div 2) = n" unfolding numeral_2_eq_2[symmetric] by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

248 
with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no" by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

249 
from f[OF this] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

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

251 
next 
35213  252 
case False hence "even (n  1)" by simp 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

253 
from even_nat_div_two_times_two[OF this] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

254 
have n_eq: "2 * ((n  1) div 2) = n  1" unfolding numeral_2_eq_2[symmetric] by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

255 
hence range_eq: "n  1 + 1 = n" using odd_pos[OF False] by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

256 

69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

257 
from n_eq `n \<ge> 2 * g_no` have "(n  1) div 2 \<ge> g_no" by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

258 
from g[OF this] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

259 
show ?thesis unfolding n_eq atLeastLessThanSuc_atLeastAtMost range_eq . 
29803
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 
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44319
diff
changeset

299 
note leibniz = summable_Leibniz'[OF _ ge0, of "\<lambda>x. x", OF tendsto_minus[OF `a > 0`, unfolded minus_zero] monotone] 
29803
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 
41970  307 

29803
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 
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44319
diff
changeset

313 
moreover have ?f and ?g using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel] 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

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: 
41970  341 
fixes x :: "'a::{real_normed_vector, ring_1}" 
342 
shows "summable (%n. (diffs c)(n) * (x ^ n)) ==> 

343 
(%n. of_nat n * c(n) * (x ^ (n  Suc 0))) sums 

15546  344 
(\<Sum>n. (diffs c)(n) * (x ^ n))" 
29163  345 
unfolding diffs_def 
346 
apply (drule summable_sums) 

347 
apply (rule sums_Suc_imp, simp_all) 

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

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

349 

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

350 
lemma lemma_termdiff1: 
31017  351 
fixes z :: "'a :: {monoid_mult,comm_ring}" shows 
41970  352 
"(\<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

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

355 

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

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

357 
"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

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

359 

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

363 
"((z + h) ^ n  z ^ n) / h  of_nat n * z ^ (n  Suc 0) = 
20860  364 
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

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

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

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

371 
right_diff_distrib [symmetric] mult_assoc 

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

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

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

377 
apply (rule setsum_cong [OF refl]) 

15539  378 
apply (simp add: diff_minus [symmetric] less_iff_Suc_add) 
20860  379 
apply (clarify) 
380 
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

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

384 
done 

385 

386 
lemma real_setsum_nat_ivl_bounded2: 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

387 
fixes K :: "'a::linordered_semidom" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

388 
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

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

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

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

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

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

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

395 

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

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

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

401 
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

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

404 
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

405 
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

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

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

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

411 
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

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

413 
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

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

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

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

419 
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

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

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

423 
order_trans [OF norm_setsum] 
20860  424 
real_setsum_nat_ivl_bounded2 
425 
mult_nonneg_nonneg 

47489  426 
of_nat_0_le_iff 
20860  427 
zero_le_power K) 
428 
apply (rule le_Kn, simp) 

429 
done 

430 
qed 

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

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

434 
qed 

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

435 

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

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

440 
assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h" 
20860  441 
shows "f  0 > 0" 
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31271
diff
changeset

442 
unfolding LIM_eq diff_0_right 
29163  443 
proof (safe) 
444 
let ?h = "of_real (k / 2)::'a" 

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

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

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

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

449 

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

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

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

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

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

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

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

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

463 
by (simp add: mult_pos_pos positive_imp_inverse_positive) 

464 
next 

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

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

466 
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

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

469 
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

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

473 
using K_neq_zero by simp 

474 
also have "r / 2 < r" 

475 
using r by simp 

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

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

479 
qed 

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

480 

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

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

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

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

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

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

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

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

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

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

498 
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

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

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

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

504 
finally show "norm (suminf (g h)) \<le> suminf f * norm h" . 
20860  505 
qed 
15077
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 

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

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

509 

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

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

512 
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

513 
assumes 2: "norm x < norm K" 
20860  514 
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

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

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

518 
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

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

522 
show ?thesis 

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

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

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

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

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

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

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

530 
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

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

532 
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

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

535 
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

536 
= (\<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

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

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

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

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

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

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

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

547 
(\<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

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

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

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

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

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

554 
"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

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

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

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

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

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

562 
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

563 
\<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

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

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

568 
apply (rule h) 

569 
apply (rule r1 [THEN order_less_imp_le]) 

570 
apply (rule xh [THEN order_less_imp_le]) 

571 
done 

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

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

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

574 

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

579 
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

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

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

586 
proof (rule LIM_equal2) 

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

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

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

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

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

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

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

598 
by (rule powser_inside [OF 1 5]) 

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

600 
by (rule powser_inside [OF 2 4]) 

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

41970  602 
 (\<Sum>n. diffs c n * x ^ n) = 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

606 
apply (subst suminf_divide [symmetric]) 

607 
apply (rule summable_diff [OF B A]) 

608 
apply (subst suminf_diff) 

609 
apply (rule summable_divide) 

610 
apply (rule summable_diff [OF B A]) 

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

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

616 
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

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

620 
qed 

621 

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

622 

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

623 
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

624 

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

625 
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

626 
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

627 
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

628 
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

629 
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

630 
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

631 
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

632 
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

633 
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

634 

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

636 
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

637 

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

639 
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

640 

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

641 
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

642 
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

643 
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

644 

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

645 
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

646 

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

647 
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

648 
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

649 
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

650 
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

651 

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

652 
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

653 
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

654 

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

655 
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

656 
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

657 
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

658 
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

659 
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

660 
then obtain n where "x = ?s n" and "n \<in> {0..<?N}" using image_iff[THEN iffD1] by blast 
41970  661 
from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def] 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

662 
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

663 
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

664 
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

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

666 
qed auto 
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 
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

669 
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

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

671 

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

672 
{ 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

673 
hence x_in_I: "x0 + x \<in> { a <..< b }" using S_a S_b by auto 
41970  674 

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

675 
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

676 
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

677 
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

678 
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

679 
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

680 
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

681 
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

682 

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

683 
{ fix n 
41970  684 
have "\<bar> ?diff (n + ?N) x \<bar> \<le> L (n + ?N) * \<bar> (x0 + x)  x0 \<bar> / \<bar> x \<bar>" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

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

686 
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

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

688 
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

689 
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

690 
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

691 

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

692 
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

693 
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

694 
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

695 
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

696 
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

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

699 
proof (rule Min_le_iff[THEN iffD2]) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

700 
have "?s n \<in> (?s ` {0..<?N}) \<and> ?s n \<le> ?s n" using `n \<in> { 0 ..< ?N}` by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

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

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

703 
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

704 

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

705 
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

706 
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

707 
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

708 
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

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

710 
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

711 
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

712 
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

713 
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

714 

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

715 
from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]] 
41970  716 
have "\<bar> (suminf (f (x0 + x))  (suminf (f x0))) / x  suminf (f' x0) \<bar> = 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

717 
\<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

718 
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

719 
also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part" using abs_triangle_ineq4 by auto 
41970  720 
also have "\<dots> < r /3 + r/3 + r/3" 
36842  721 
using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3` 
722 
by (rule add_strict_mono [OF add_less_le_mono]) 

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

723 
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

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

726 
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

727 
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

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

729 

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

730 
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

731 
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

732 
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

733 
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

734 
(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

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

736 
{ 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

737 
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

738 
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

739 
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

740 
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

741 
proof  
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

742 
have "(R' + R) / 2 < R" and "0 < (R' + R) / 2" using `0 < R'` `0 < R` `R' < R` by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

743 
hence in_Rball: "(R' + R) / 2 \<in> {R <..< R}" using `R' < R` by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

744 
have "norm R' < norm ((R' + R) / 2)" using `0 < R'` `0 < R` `R' < R` by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

745 
from powser_insidea[OF converges[OF in_Rball] this] show ?thesis 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

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

747 
{ fix n x y assume "x \<in> {R' <..< R'}" and "y \<in> {R' <..< R'}" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

748 
show "\<bar>?f x n  ?f y n\<bar> \<le> \<bar>f n * real (Suc n) * R'^n\<bar> * \<bar>xy\<bar>" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

749 
proof  
41970  750 
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>" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

751 
unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult by auto 
41970  752 
also have "\<dots> \<le> (\<bar>f n\<bar> * \<bar>xy\<bar>) * (\<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>)" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

753 
proof (rule mult_left_mono) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

754 
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) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

755 
also have "\<dots> \<le> (\<Sum>p = 0..<Suc n. R' ^ n)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

756 
proof (rule setsum_mono) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

757 
fix p assume "p \<in> {0..<Suc n}" hence "p \<le> n" by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

758 
{ fix n fix x :: real assume "x \<in> {R'<..<R'}" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

759 
hence "\<bar>x\<bar> \<le> R'" by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

760 
hence "\<bar>x^n\<bar> \<le> R'^n" unfolding power_abs by (rule power_mono, auto) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

761 
} from mult_mono[OF this[OF `x \<in> {R'<..<R'}`, of p] this[OF `y \<in> {R'<..<R'}`, of "np"]] `0 < R'` 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

762 
have "\<bar>x^p * y^(np)\<bar> \<le> R'^p * R'^(np)" unfolding abs_mult by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

763 
thus "\<bar>x^p * y^(np)\<bar> \<le> R'^n" unfolding power_add[symmetric] using `p \<le> n` by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

764 
qed 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

765 
also have "\<dots> = real (Suc n) * R' ^ n" unfolding setsum_constant card_atLeastLessThan real_of_nat_def by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

766 
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'`]]] . 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

767 
show "0 \<le> \<bar>f n\<bar> * \<bar>x  y\<bar>" unfolding abs_mult[symmetric] by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

768 
qed 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36776
diff
changeset

769 
also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x  y\<bar>" unfolding abs_mult mult_assoc[symmetric] by algebra 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

770 
finally show ?thesis . 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

771 
qed } 
31881  772 
{ fix n show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

773 
by (auto intro!: DERIV_intros simp del: power_Suc) } 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

774 
{ fix x assume "x \<in> {R' <..< R'}" hence "R' \<in> {R <..< R}" and "norm x < norm R'" using assms `R' < R` by auto 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

775 
have "summable (\<lambda> n. f n * x^n)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

776 
proof (rule summable_le2[THEN conjunct1, OF _ powser_insidea[OF converges[OF `R' \<in> {R <..< R}`] `norm x < norm R'`]], rule allI) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

777 
fix n 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

778 
have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)" by (rule mult_left_mono, auto) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

779 
show "\<bar>f n * x ^ n\<bar> \<le> norm (f n * real (Suc n) * x ^ n)" unfolding real_norm_def abs_mult 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

780 
by (rule mult_right_mono, auto simp add: le[unfolded mult_1_right]) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

781 
qed 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36776
diff
changeset

782 
from this[THEN summable_mult2[where c=x], unfolded mult_assoc, unfolded mult_commute] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

783 
show "summable (?f x)" 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

784 
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

785 
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

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

788 
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

789 
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

790 
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

791 
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

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

793 
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

794 
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

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

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

797 
have " ?R < 0" using assms by auto 
41970  798 
also have "\<dots> \<le> x0" using False 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

799 
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

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

801 
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

802 
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

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

804 
qed 
29695  805 

29164  806 
subsection {* Exponential Function *} 
23043  807 

44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

808 
definition exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

809 
"exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))" 
23043  810 

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

811 
lemma summable_exp_generic: 
31017  812 
fixes x :: "'a::{real_normed_algebra_1,banach}" 
25062  813 
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

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

815 
proof  
25062  816 
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

817 
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

818 
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

819 
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

820 
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

821 
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

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

823 
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

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

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

826 
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

827 
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

828 
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

829 
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

830 
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

831 
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

832 
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

833 
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

834 
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

835 
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

836 
thus "norm (S (Suc n)) \<le> r * norm (S n)" 
35216  837 
by (simp add: S_Suc inverse_eq_divide) 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

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

840 

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

841 
lemma summable_norm_exp: 
31017  842 
fixes x :: "'a::{real_normed_algebra_1,banach}" 
25062  843 
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

844 
proof (rule summable_norm_comparison_test [OF exI, rule_format]) 
25062  845 
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

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

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

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

851 

23043  852 
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

853 
by (insert summable_exp_generic [where x=x], simp) 
23043  854 

25062  855 
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

856 
unfolding exp_def by (rule summable_exp_generic [THEN summable_sums]) 
23043  857 

858 

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

860 
"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

861 
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

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

863 

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

864 
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

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

866 

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

867 
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" 
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

868 
unfolding exp_def scaleR_conv_of_real 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

869 
apply (rule DERIV_cong) 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

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

871 
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

872 
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

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

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

875 

51527  876 
declare DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] 
877 

44311  878 
lemma isCont_exp: "isCont exp x" 
879 
by (rule DERIV_exp [THEN DERIV_isCont]) 

880 

881 
lemma isCont_exp' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a" 

882 
by (rule isCont_o2 [OF _ isCont_exp]) 

883 

884 
lemma tendsto_exp [tendsto_intros]: 

885 
"(f > a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) > exp a) F" 

886 
by (rule isCont_tendsto_compose [OF isCont_exp]) 

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

887 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

888 
lemma continuous_exp [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

889 
unfolding continuous_def by (rule tendsto_exp) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

890 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

891 
lemma continuous_on_exp [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

892 
unfolding continuous_on_def by (auto intro: tendsto_exp) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

893 

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

895 

23278  896 
lemma powser_zero: 
31017  897 
fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}" 
23278  898 
shows "(\<Sum>n. f n * 0 ^ n) = f 0" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

899 
proof  
23278  900 
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

901 
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

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

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

904 

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

907 

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

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

909 
"(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))" 
28069  910 
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

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

912 

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

913 
lemma exp_series_add: 
31017  914 
fixes x y :: "'a::{real_field}" 
25062  915 
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

916 
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

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

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

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

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

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

922 
case (Suc n) 
25062  923 
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

924 
unfolding S_def by (simp del: mult_Suc) 
25062  925 
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

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

927 

25062  928 
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

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

930 
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

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

932 
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

933 
+ y * (\<Sum>i=0..n. S x i * S y (ni))" 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47489
diff
changeset

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

935 
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

936 
+ (\<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

937 
by (simp only: setsum_right_distrib mult_ac) 
25062  938 
also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (ni))) 
939 
+ (\<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

940 
by (simp add: times_S Suc_diff_le) 
25062  941 
also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (ni))) = 
942 
(\<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

943 
by (subst setsum_cl_ivl_Suc2, simp) 
25062  944 
also have "(\<Sum>i=0..n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni))) = 
945 
(\<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

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

949 
(\<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

950 
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

951 
real_of_nat_add [symmetric], simp) 
25062  952 
also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc ni))" 
23127  953 
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

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

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

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

958 

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

959 
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

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

961 
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

962 

29170  963 
lemma mult_exp_exp: "exp x * exp y = exp (x + y)" 
964 
by (rule exp_add [symmetric]) 

965 

23241  966 
lemma exp_of_real: "exp (of_real x) = of_real (exp x)" 
967 
unfolding exp_def 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
43335
diff
changeset

968 
apply (subst suminf_of_real) 
23241  969 
apply (rule summable_exp_generic) 
970 
apply (simp add: scaleR_conv_of_real) 

971 
done 

972 

29170  973 
lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0" 
974 
proof 

975 
have "exp x * exp ( x) = 1" by (simp add: mult_exp_exp) 

976 
also assume "exp x = 0" 

977 
finally show "False" by simp 

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

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

979 

29170  980 
lemma exp_minus: "exp ( x) = inverse (exp x)" 
981 
by (rule inverse_unique [symmetric], simp add: mult_exp_exp) 

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

982 

29170  983 
lemma exp_diff: "exp (x  y) = exp x / exp y" 
984 
unfolding diff_minus divide_inverse 

985 
by (simp add: exp_add exp_minus) 

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

986 

29167  987 

988 
subsubsection {* Properties of the Exponential Function on Reals *} 

989 

29170  990 
text {* Comparisons of @{term "exp x"} with zero. *} 
29167  991 

992 
text{*Proof: because every exponential can be seen as a square.*} 

993 
lemma exp_ge_zero [simp]: "0 \<le> exp (x::real)" 

994 
proof  

995 
have "0 \<le> exp (x/2) * exp (x/2)" by simp 

996 
thus ?thesis by (simp add: exp_add [symmetric]) 

997 
qed 

998 

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

999 
lemma exp_gt_zero [simp]: "0 < exp (x::real)" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1001 

29170  1002 
lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0" 
1003 
by (simp add: not_less) 

1004 

1005 
lemma not_exp_le_zero [simp]: "\<not> exp (x::real) \<le> 0" 

1006 
by (simp add: not_le) 

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

1007 

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

1008 
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

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

1010 

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

1011 
lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" 
15251  1012 
apply (induct "n") 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47489
diff
changeset

1013 
apply (auto simp add: real_of_nat_Suc distrib_left exp_add mult_commute) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1015 

29170  1016 
text {* Strict monotonicity of exponential. *} 
1017 

1018 
lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) ==> (1 + x) \<le> exp(x)" 

1019 
apply (drule order_le_imp_less_or_eq, auto) 

1020 
apply (simp add: exp_def) 

36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36776
diff
changeset

1021 
apply (rule order_trans) 
29170  1022 
apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le) 
1023 
apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff) 

1024 
done 

1025 

1026 
lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x" 

1027 
proof  

1028 
assume x: "0 < x" 

1029 
hence "1 < 1 + x" by simp 

1030 
also from x have "1 + x \<le> exp x" 

1031 
by (simp add: exp_ge_add_one_self_aux) 

1032 
finally show ?thesis . 

1033 
qed 

1034 

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

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

1036 
fixes x y :: real 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1037 
assumes "x < y" shows "exp x < exp y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1038 
proof  
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1039 
from `x < y` have "0 < y  x" by simp 
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1040 
hence "1 < exp (y  x)" by (rule exp_gt_one) 
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1041 
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

1042 
thus "exp x < exp y" by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1044 

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

1045 
lemma exp_less_cancel: "exp (x::real) < exp y ==> x < y" 
29170  1046 
apply (simp add: linorder_not_le [symmetric]) 
1047 
apply (auto simp add: order_le_less exp_less_mono) 

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

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

1049 

29170  1050 
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

1051 
by (auto intro: exp_less_mono exp_less_cancel) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1052 

29170  1053 
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

1054 
by (auto simp add: linorder_not_less [symmetric]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1055 

29170  1056 
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

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

1058 

29170  1059 
text {* Comparisons of @{term "exp x"} with one. *} 
1060 

1061 
lemma one_less_exp_iff [simp]: "1 < exp (x::real) \<longleftrightarrow> 0 < x" 

1062 
using exp_less_cancel_iff [where x=0 and y=x] by simp 

1063 

1064 
lemma exp_less_one_iff [simp]: "exp (x::real) < 1 \<longleftrightarrow> x < 0" 

1065 
using exp_less_cancel_iff [where x=x and y=0] by simp 

1066 

1067 
lemma one_le_exp_iff [simp]: "1 \<le> exp (x::real) \<longleftrightarrow> 0 \<le> x" 

1068 
using exp_le_cancel_iff [where x=0 and y=x] by simp 

1069 

1070 
lemma exp_le_one_iff [simp]: "exp (x::real) \<le> 1 \<longleftrightarrow> x \<le> 0" 

1071 
using exp_le_cancel_iff [where x=x and y=0] by simp 

1072 

1073 
lemma exp_eq_one_iff [simp]: "exp (x::real) = 1 \<longleftrightarrow> x = 0" 

1074 
using exp_inj_iff [where x=x and y=0] by simp 

1075 

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

1076 
lemma lemma_exp_total: "1 \<le> y ==> \<exists>x. 0 \<le> x & x \<le> y  1 & exp(x::real) = y" 
44755  1077 
proof (rule IVT) 
1078 
assume "1 \<le> y" 

1079 
hence "0 \<le> y  1" by simp 

1080 
hence "1 + (y  1) \<le> exp (y  1)" by (rule exp_ge_add_one_self_aux) 

1081 
thus "y \<le> exp (y  1)" by simp 

1082 
qed (simp_all add: le_diff_eq) 

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

1083 

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

1084 
lemma exp_total: "0 < (y::real) ==> \<exists>x. exp x = y" 
44755  1085 
proof (rule linorder_le_cases [of 1 y]) 
1086 
assume "1 \<le> y" thus "\<exists>x. exp x = y" 

1087 
by (fast dest: lemma_exp_total) 

1088 
next 

1089 
assume "0 < y" and "y \<le> 1" 

1090 
hence "1 \<le> inverse y" by (simp add: one_le_inverse_iff) 

1091 
then obtain x where "exp x = inverse y" by (fast dest: lemma_exp_total) 

1092 
hence "exp ( x) = y" by (simp add: exp_minus) 

1093 
thus "\<exists>x. exp x = y" .. 

1094 
qed 

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

1095 

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

1096 

29164  1097 
subsection {* Natural Logarithm *} 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1098 

44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1099 
definition ln :: "real \<Rightarrow> real" where 
23043  1100 
"ln x = (THE u. exp u = x)" 
1101 

1102 
lemma ln_exp [simp]: "ln (exp x) = x" 

44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

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

1104 

22654
c2b6b5a9e136
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents:
22653
diff
changeset

1105 
lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x" 
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1106 
by (auto dest: exp_total) 
22654
c2b6b5a9e136
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents:
22653
diff
changeset

1107 

29171  1108 
lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x" 
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1109 
by (metis exp_gt_zero exp_ln) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1110 

29171  1111 
lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y" 
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1112 
by (erule subst, rule ln_exp) 
29171  1113 

1114 
lemma ln_one [simp]: "ln 1 = 0" 

44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1115 
by (rule ln_unique, simp) 
29171  1116 

1117 
lemma ln_mult: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x * y) = ln x + ln y" 

44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1118 
by (rule ln_unique, simp add: exp_add) 
29171  1119 

1120 
lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) =  ln x" 

44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1121 
by (rule ln_unique, simp add: exp_minus) 
29171  1122 

1123 
lemma ln_div: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x / y) = ln x  ln y" 

44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1124 
by (rule ln_unique, simp add: exp_diff) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1125 

29171  1126 
lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x" 
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1127 
by (rule ln_unique, simp add: exp_real_of_nat_mult) 
29171  1128 

1129 
lemma ln_less_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y" 

44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1130 
by (subst exp_less_cancel_iff [symmetric], simp) 
29171  1131 

1132 
lemma ln_le_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y" 

44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1133 
by (simp add: linorder_not_less [symmetric]) 
29171  1134 

1135 
lemma ln_inj_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y" 

44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1136 
by (simp add: order_eq_iff) 
29171  1137 

1138 
lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x" 

44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1139 
apply (rule exp_le_cancel_iff [THEN iffD1]) 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1140 
apply (simp add: exp_ge_add_one_self_aux) 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

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

1142 

29171  1143 
lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x" 
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1144 
by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1145 

d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1146 
lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x" 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1147 
using ln_le_cancel_iff [of 1 x] by simp 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1148 

d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1149 
lemma ln_ge_zero_imp_ge_one: "\<lbrakk>0 \<le> ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 \<le> x" 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1150 
using ln_le_cancel_iff [of 1 x] by simp 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1151 

d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1152 
lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> (0 \<le> ln x) = (1 \<le> x)" 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1153 
using ln_le_cancel_iff [of 1 x] by simp 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1154 

d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1155 
lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x < 0) = (x < 1)" 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1156 
using ln_less_cancel_iff [of x 1] by simp 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1157 

d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1158 
lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x" 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1159 
using ln_less_cancel_iff [of 1 x] by simp 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1160 

d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1161 
lemma ln_gt_zero_imp_gt_one: "\<lbrakk>0 < ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 < x" 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1162 
using ln_less_cancel_iff [of 1 x] by simp 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1163 

d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1164 
lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> (0 < ln x) = (1 < x)" 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1165 
using ln_less_cancel_iff [of 1 x] by simp 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1166 

d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1167 
lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x = 0) = (x = 1)" 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1168 
using ln_inj_iff [of x 1] by simp 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1169 

d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1170 
lemma ln_less_zero: "\<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ln x < 0" 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

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

1172 

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

1173 
lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x" 
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1174 
apply (subgoal_tac "isCont ln (exp (ln x))", simp) 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1175 
apply (rule isCont_inverse_function [where f=exp], simp_all) 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

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

1177 

45915  1178 
lemma tendsto_ln [tendsto_intros]: 
1179 
"\<lbrakk>(f > a) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. ln (f x)) > ln a) F" 

1180 
by (rule isCont_tendsto_compose [OF isCont_ln]) 

1181 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1182 
lemma continuous_ln: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1183 
"continuous F f \<Longrightarrow> 0 < f (Lim F (\<lambda>x. x)) \<Longrightarrow> continuous F (\<lambda>x. ln (f x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1184 
unfolding continuous_def by (rule tendsto_ln) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1185 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1186 
lemma isCont_ln' [continuous_intros]: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1187 
"continuous (at x) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1188 
unfolding continuous_at by (rule tendsto_ln) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1189 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1190 
lemma continuous_within_ln [continuous_intros]: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1191 
"continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1192 
unfolding continuous_within by (rule tendsto_ln) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1193 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1194 
lemma continuous_on_ln [continuous_on_intros]: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset

1195 
"continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; 