author  huffman 
Mon, 05 Sep 2011 18:06:02 0700  
changeset 44745  b068207a7400 
parent 44730  11a1290fd0ac 
child 44746  9e4f7d3b5376 
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 
12196  4 
*) 
5 

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

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

7 

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

11 

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

13 

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

14 
lemma lemma_realpow_diff: 
31017  15 
fixes y :: "'a::monoid_mult" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

16 
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

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

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

19 
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

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

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

22 

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

23 
lemma lemma_realpow_diff_sumr: 
31017  24 
fixes y :: "'a::{comm_semiring_0,monoid_mult}" shows 
41970  25 
"(\<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

26 
y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n  p))" 
29163  27 
by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac 
33549  28 
del: setsum_op_ivl_Suc) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

29 

15229  30 
lemma lemma_realpow_diff_sumr2: 
31017  31 
fixes y :: "'a::{comm_ring,monoid_mult}" shows 
41970  32 
"x ^ (Suc n)  y ^ (Suc n) = 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

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

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

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

39 
apply (subst mult_left_commute [of "x  y"]) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

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

43 

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

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

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

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

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

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

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

52 

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

53 
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

54 
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

55 

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

56 
lemma powser_insidea: 
44726  57 
fixes x z :: "'a::real_normed_field" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

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

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

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

62 
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

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

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

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

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

67 
hence "Cauchy (\<lambda>n. f n * x ^ n)" 
44726  68 
by (rule convergent_Cauchy) 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

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

71 
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

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

73 
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

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

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

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

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

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

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

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

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

82 
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

83 
by (simp add: x_neq_0) 
23082
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 only: mult_assoc) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

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

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

90 
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

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

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

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

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

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

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

97 
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

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

99 
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

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

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

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

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

104 
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

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

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

107 

15229  108 
lemma powser_inside: 
31017  109 
fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" shows 
41970  110 
"[ summable (%n. f(n) * (x ^ n)); norm z < norm x ] 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

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

113 

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

114 
lemma sum_split_even_odd: fixes f :: "nat \<Rightarrow> real" shows 
41970  115 
"(\<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

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

117 
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

118 
case (Suc n) 
41970  119 
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

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

121 
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

122 
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

123 
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

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

125 

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

126 
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

127 
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

128 
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

129 
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

130 
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

131 
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

132 
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

133 

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

134 
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

135 
{ fix m assume "m \<ge> 2 * no" hence "m div 2 \<ge> no" by auto 
41970  136 
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

137 
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

138 
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

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

140 
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

141 
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

142 
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

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

144 
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

145 
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

146 
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

147 
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

148 
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

149 
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

150 
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

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

152 
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

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

154 
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

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

156 

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

157 
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

158 
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

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

160 
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

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

162 
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

163 
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  164 
{ 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

165 
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

166 
have Suc_m1: "\<And> n. Suc n  1 = n" by auto 
41550  167 
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

168 

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

169 
have "?s sums y" using sums_if'[OF `f sums y`] . 
41970  170 
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

171 
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

172 
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

173 
image_Suc_atLeastLessThan[symmetric] setsum_reindex[OF inj_Suc, unfolded comp_def] 
31148  174 
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

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

176 
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

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

178 

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

179 
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

180 

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

181 
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

182 
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

183 
assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a > 0" 
41970  184 
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

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

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

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

188 
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

189 

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

190 
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

191 
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

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

193 
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

194 
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

195 
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

196 
moreover 
41970  197 
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

198 
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

199 
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

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

201 
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

202 
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

203 
fix r :: real assume "0 < r" 
41970  204 
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

205 
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

206 
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

207 
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

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

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

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

212 

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

213 
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

214 
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

215 
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

216 
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

217 
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

218 
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

219 
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

220 
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

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

222 
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

223 
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

224 
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

225 
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

226 
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

227 
using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast 
41970  228 

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

229 
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

230 
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

231 
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

232 
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

233 

41970  234 
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

235 
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

236 

41970  237 
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

238 
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

239 

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

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

241 
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

242 
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

243 
proof (cases "even n") 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

244 
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

245 
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

246 
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

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

248 
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

249 
next 
35213  250 
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

251 
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

252 
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

253 
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

254 

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

255 
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

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

257 
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

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

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

260 
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

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

262 
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

263 
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

264 

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

265 
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

266 

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

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

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

269 
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

270 
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

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

272 

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

273 
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

274 
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

275 
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

276 
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

277 
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

278 
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

279 
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

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

281 
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

282 
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

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

284 
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

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

286 
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

287 
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

288 
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

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

290 
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

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

292 
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

293 
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

294 
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

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

296 
note monotone = this 
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44319
diff
changeset

297 
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

298 
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

299 
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

300 
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

301 
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

302 
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

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

304 
have "\<And> a b :: real. \<bar>  a   b \<bar> = \<bar>a  b\<bar>" unfolding minus_diff_minus by auto 
41970  305 

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

306 
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

307 
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

308 

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

309 
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

310 
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

311 
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

312 
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

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

314 
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

315 
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

316 
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

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

318 

29164  319 
subsection {* TermbyTerm Differentiability of Power Series *} 
23043  320 

321 
definition 

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

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

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

324 

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

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

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

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

328 

29163  329 
lemma sums_Suc_imp: 
330 
assumes f: "f 0 = 0" 

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

332 
unfolding sums_def 

333 
apply (rule LIMSEQ_imp_Suc) 

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

335 
apply (simp only: setsum_shift_bounds_Suc_ivl) 

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

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

337 

15229  338 
lemma diffs_equiv: 
41970  339 
fixes x :: "'a::{real_normed_vector, ring_1}" 
340 
shows "summable (%n. (diffs c)(n) * (x ^ n)) ==> 

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

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

345 
apply (rule sums_Suc_imp, simp_all) 

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

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

347 

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

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

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

353 

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

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

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

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

357 

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

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

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

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

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

369 
right_diff_distrib [symmetric] mult_assoc 

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

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

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

375 
apply (rule setsum_cong [OF refl]) 

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

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

382 
done 

383 

384 
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

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

386 
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

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

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

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

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

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

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

393 

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

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

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

399 
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

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

402 
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

403 
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

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

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

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

409 
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

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

411 
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

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

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

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

417 
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

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

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

421 
order_trans [OF norm_setsum] 
20860  422 
real_setsum_nat_ivl_bounded2 
423 
mult_nonneg_nonneg 

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

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

427 
done 

428 
qed 

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

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

432 
qed 

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

433 

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

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

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

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

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

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

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

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

447 

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

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

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

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

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

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

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

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

461 
by (simp add: mult_pos_pos positive_imp_inverse_positive) 

462 
next 

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

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

464 
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

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

467 
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

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

471 
using K_neq_zero by simp 

472 
also have "r / 2 < r" 

473 
using r by simp 

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

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

477 
qed 

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

478 

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

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

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

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

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

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

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

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

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

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

496 
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

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

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

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

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

504 

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

505 

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

506 
text{* FIXME: Long proofs*} 
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 
lemma termdiffs_aux: 
31017  509 
fixes x :: "'a::{real_normed_field,banach}" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

510 
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

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

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

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

516 
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

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

520 
show ?thesis 

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

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

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

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

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

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

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

528 
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

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

530 
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

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

533 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

560 
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

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

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

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

566 
apply (rule h) 

567 
apply (rule r1 [THEN order_less_imp_le]) 

568 
apply (rule xh [THEN order_less_imp_le]) 

569 
done 

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

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

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

572 

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

577 
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

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

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

584 
proof (rule LIM_equal2) 

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

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

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

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

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

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

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

596 
by (rule powser_inside [OF 1 5]) 

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

598 
by (rule powser_inside [OF 2 4]) 

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

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

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

604 
apply (subst suminf_divide [symmetric]) 

605 
apply (rule summable_diff [OF B A]) 

606 
apply (subst suminf_diff) 

607 
apply (rule summable_divide) 

608 
apply (rule summable_diff [OF B A]) 

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

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

614 
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

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

618 
qed 

619 

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

620 

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

621 
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

622 

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

623 
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

624 
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

625 
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

626 
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

627 
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

628 
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

629 
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

630 
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

631 
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

632 

41970  633 
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

634 
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

635 

41970  636 
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

637 
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

638 

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

639 
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

640 
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

641 
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

642 

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

643 
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

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

646 
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

647 
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

648 
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

649 

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

650 
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

651 
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

652 

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

653 
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

654 
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

655 
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

656 
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

657 
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

658 
then obtain n where "x = ?s n" and "n \<in> {0..<?N}" using image_iff[THEN iffD1] by blast 
41970  659 
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

660 
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

661 
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

662 
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

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

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

665 

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

666 
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

667 
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

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

669 

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

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

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

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

673 
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

674 
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

675 
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

676 
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

677 
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

678 
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

679 
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

680 

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

681 
{ fix n 
41970  682 
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

683 
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

684 
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

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

686 
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

687 
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

688 
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

689 

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

690 
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

691 
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

692 
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

693 
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

694 
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

695 
also have "S \<le> S'" using `S \<le> S'` . 
41970  696 
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

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

698 
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

699 
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

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

701 
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

702 

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

703 
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

704 
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

705 
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

706 
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

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

708 
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

709 
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

710 
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

711 
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

712 

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

713 
from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]] 
41970  714 
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

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

716 
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

717 
also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part" using abs_triangle_ineq4 by auto 
41970  718 
also have "\<dots> < r /3 + r/3 + r/3" 
36842  719 
using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3` 
720 
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

721 
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

722 
by auto 
41970  723 
} 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

724 
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

725 
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

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

727 

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

728 
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

729 
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

730 
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

731 
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

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

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

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

735 
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

736 
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

737 
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

738 
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

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

740 
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

741 
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

742 
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

743 
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

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

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

746 
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

747 
proof  
41970  748 
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

749 
unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult by auto 
41970  750 
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

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

752 
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

753 
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

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

755 
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

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

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

758 
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

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

760 
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

761 
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

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

763 
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

764 
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

765 
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

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

767 
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

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

769 
qed } 
31881  770 
{ 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

771 
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

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

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

774 
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

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

776 
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

777 
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

778 
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

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

780 
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

781 
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

782 
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

783 
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

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

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

786 
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

787 
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

788 
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

789 
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

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

791 
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

792 
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

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

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

795 
have " ?R < 0" using assms by auto 
41970  796 
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

797 
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

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

799 
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

800 
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

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

802 
qed 
29695  803 

29164  804 
subsection {* Exponential Function *} 
23043  805 

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

806 
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

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

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

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

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

813 
proof  
25062  814 
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

815 
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

816 
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

817 
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

818 
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

819 
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

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

821 
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

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

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

824 
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

825 
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

826 
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

827 
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

828 
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

829 
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

830 
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

831 
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

832 
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

833 
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

834 
thus "norm (S (Suc n)) \<le> r * norm (S n)" 
35216  835 
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

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

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

838 

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

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

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

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

845 
next 
25062  846 
fix n show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)" 
35216  847 
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

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

849 

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

851 
by (insert summable_exp_generic [where x=x], simp) 
23043  852 

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

854 
unfolding exp_def by (rule summable_exp_generic [THEN summable_sums]) 
23043  855 

856 

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

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

859 
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

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

861 

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

862 
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

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

864 

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

865 
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

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

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

868 
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

869 
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

870 
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

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

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

873 

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

876 

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

878 
by (rule isCont_o2 [OF _ isCont_exp]) 

879 

880 
lemma tendsto_exp [tendsto_intros]: 

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

882 
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

883 

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

884 

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

886 

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

890 
proof  
23278  891 
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

892 
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

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

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

895 

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

898 

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

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

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

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

903 

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

904 
lemma exp_series_add: 
31017  905 
fixes x y :: "'a::{real_field}" 
25062  906 
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

907 
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

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

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

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

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

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

913 
case (Suc n) 
25062  914 
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

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

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

918 

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

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

921 
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

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

923 
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

924 
+ 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

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

926 
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

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

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

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

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

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

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

941 
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

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

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

946 
"S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n  i))" 
35216  947 
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

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

949 

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

950 
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

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

952 
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

953 

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

956 

23241  957 
lemma exp_of_real: "exp (of_real x) = of_real (exp x)" 
958 
unfolding exp_def 

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

959 
apply (subst suminf_of_real) 
23241  960 
apply (rule summable_exp_generic) 
961 
apply (simp add: scaleR_conv_of_real) 

962 
done 

963 

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

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

967 
also assume "exp x = 0" 

968 
finally show "False" by simp 

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

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

970 

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

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

973 

29170  974 
lemma exp_diff: "exp (x  y) = exp x / exp y" 
975 
unfolding diff_minus divide_inverse 

976 
by (simp add: exp_add exp_minus) 

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

977 

29167  978 

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

980 

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

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

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

985 
proof  

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

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

988 
qed 

989 

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

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

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

992 

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

995 

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

997 
by (simp add: not_le) 

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

998 

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

999 
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

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

1001 

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

1002 
lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" 
15251  1003 
apply (induct "n") 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

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

1006 

29170  1007 
text {* Strict monotonicity of exponential. *} 
1008 

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

1010 
apply (drule order_le_imp_less_or_eq, auto) 

1011 
apply (simp add: exp_def) 

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

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

1015 
done 

1016 

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

1018 
proof  

1019 
assume x: "0 < x" 

1020 
hence "1 < 1 + x" by simp 

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

1022 
by (simp add: exp_ge_add_one_self_aux) 

1023 
finally show ?thesis . 

1024 
qed 

1025 

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

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

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

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

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

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

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

1032 
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

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

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

1035 

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

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

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

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

1040 

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

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

1043 

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

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

1046 

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

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

1049 

29170  1050 
text {* Comparisons of @{term "exp x"} with one. *} 
1051 

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

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

1054 

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

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

1057 

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

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

1060 

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

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

1063 

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

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

1066 

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

1067 
lemma lemma_exp_total: "1 \<le> y ==> \<exists>x. 0 \<le> x & x \<le> y  1 & exp(x::real) = y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1068 
apply (rule IVT) 
23045
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

1069 
apply (auto intro: isCont_exp simp add: le_diff_eq) 
41970  1070 
apply (subgoal_tac "1 + (y  1) \<le> exp (y  1)") 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1071 
apply simp 
17014
ad5ceb90877d
renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
avigad
parents:
16924
diff
changeset

1072 
apply (rule exp_ge_add_one_self_aux, simp) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1074 

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

1075 
lemma exp_total: "0 < (y::real) ==> \<exists>x. exp x = y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1076 
apply (rule_tac x = 1 and y = y in linorder_cases) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1077 
apply (drule order_less_imp_le [THEN lemma_exp_total]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1078 
apply (rule_tac [2] x = 0 in exI) 
36776
c137ae7673d3
remove a couple of redundant lemmas; simplify some proofs
huffman
parents:
35216
diff
changeset

1079 
apply (frule_tac [3] one_less_inverse) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1080 
apply (drule_tac [4] order_less_imp_le [THEN lemma_exp_total], auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1081 
apply (rule_tac x = "x" in exI) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

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

1084 

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

1085 

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

1087 

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

1088 
definition ln :: "real \<Rightarrow> real" where 
23043  1089 
"ln x = (THE u. exp u = x)" 
1090 

1091 
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

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

1093 

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

1094 
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

1095 
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

1096 

29171  1097 
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

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

1099 

29171  1100 
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

1101 
by (erule subst, rule ln_exp) 
29171  1102 

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

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

1104 
by (rule ln_unique, simp) 
29171  1105 

1106 
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

1107 
by (rule ln_unique, simp add: exp_add) 
29171  1108 

1109 
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

1110 
by (rule ln_unique, simp add: exp_minus) 
29171  1111 

1112 
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

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

1114 

29171  1115 
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

1116 
by (rule ln_unique, simp add: exp_real_of_nat_mult) 
29171  1117 

1118 
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

1119 
by (subst exp_less_cancel_iff [symmetric], simp) 
29171  1120 

1121 
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

1122 
by (simp add: linorder_not_less [symmetric]) 
29171  1123 

1124 
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

1125 
by (simp add: order_eq_iff) 
29171  1126 

1127 
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

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

1129 
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

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

1131 

29171  1132 
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

1133 
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

1134 

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

1135 
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

1136 
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

1137 

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

1138 
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

1139 
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

1140 

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

1141 
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

1142 
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

1143 

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

1144 
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

1145 
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

1146 

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

1147 
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

1148 
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

1149 

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

1150 
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

1151 
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

1152 

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

1153 
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

1154 
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

1155 

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

1156 
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

1157 
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

1158 

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

1159 
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

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

1161 

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

1162 
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

1163 
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

1164 
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

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

1166 

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

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

1168 
apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"]) 
44317
b7e9fa025f15
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
huffman
parents:
44316
diff
changeset

1169 
apply (erule DERIV_cong [OF DERIV_exp exp_ln]) 
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

1170 
apply (simp_all add: abs_if isCont_ln) 
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset

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

1172 

33667  1173 
lemma DERIV_ln_divide: "0 < x ==> DERIV ln x :> 1 / x" 
1174 
by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse) 

1175 

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

1176 
lemma ln_series: assumes "0 < x" and "x < 2" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1177 
shows "ln x = (\<Sum> n. (1)^n * (1 / real (n + 1)) * (x  1)^(Suc n))" (is "ln x = suminf (?f (x  1))") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

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

1180 

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

1181 
have "ln x  suminf (?f (x  1)) = ln 1  suminf (?f (1  1))" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1182 
proof (rule DERIV_isconst3[where x=x]) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1183 
fix x :: real assume "x \<in> {0 <..< 2}" hence "0 < x" and "x < 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

1184 
have "norm (1  x) < 1" using `0 < x` and `x < 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

1185 
have "1 / x = 1 / (1  (1  x))" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1186 
also have "\<dots> = (\<Sum> n. (1  x)^n)" using geometric_sums[OF `norm (1  x) < 1`] by (rule sums_unique) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1187 
also have "\<dots> = suminf (?f' x)" unfolding power_mult_distrib[symmetric] by (rule arg_cong[where f=suminf], rule arg_cong[where f="op ^"], auto) 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36776
diff
changeset

1188 
finally have "DERIV ln x :> suminf (?f' x)" using DERIV_ln[OF `0 < x`] unfolding divide_inverse 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

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

1190 
have repos: "\<And> h x :: real. h  1 + x = h + x  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

1191 
have "DERIV (\<lambda>x. suminf (?f x)) (x  1) :> (\<Sum>n. (1)^n * (1 / real (n + 1)) * real (Suc n) * (x  1) ^ n)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

1193 
show "x  1 \<in> { 1<..<1}" and "(0 :: real) < 1" using `0 < x` `x < 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

1194 
{ fix x :: real assume "x \<in> { 1<..<1}" hence "norm (x) < 1" by auto 
32960
69916a850301
eliminated hard tabulators, guessing at each author' 