author  nipkow 
Fri, 06 Jun 2014 12:36:06 +0200  
changeset 57180  74c81a5b5a34 
parent 57129  7edb7550663e 
child 57275  0ddb5b755cdc 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

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

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

3 
Author: Lawrence C Paulson 
51527  4 
Author: Jeremy Avigad 
12196  5 
*) 
6 

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

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

8 

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

12 

57025  13 
lemma root_test_convergence: 
14 
fixes f :: "nat \<Rightarrow> 'a::banach" 

15 
assumes f: "(\<lambda>n. root n (norm (f n))) > x"  "could be weakened to lim sup" 

16 
assumes "x < 1" 

17 
shows "summable f" 

18 
proof  

19 
have "0 \<le> x" 

20 
by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1]) 

21 
from `x < 1` obtain z where z: "x < z" "z < 1" 

22 
by (metis dense) 

23 
from f `x < z` 

24 
have "eventually (\<lambda>n. root n (norm (f n)) < z) sequentially" 

25 
by (rule order_tendstoD) 

26 
then have "eventually (\<lambda>n. norm (f n) \<le> z^n) sequentially" 

27 
using eventually_ge_at_top 

28 
proof eventually_elim 

29 
fix n assume less: "root n (norm (f n)) < z" and n: "1 \<le> n" 

30 
from power_strict_mono[OF less, of n] n 

31 
show "norm (f n) \<le> z ^ n" 

32 
by simp 

33 
qed 

34 
then show "summable f" 

35 
unfolding eventually_sequentially 

36 
using z `0 \<le> x` by (auto intro!: summable_comparison_test[OF _ summable_geometric]) 

37 
qed 

38 

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

40 

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

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

43 
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

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

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

46 
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

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

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

49 

15229  50 
lemma lemma_realpow_diff_sumr2: 
53079  51 
fixes y :: "'a::{comm_ring,monoid_mult}" 
52 
shows 

53 
"x ^ (Suc n)  y ^ (Suc n) = 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

54 
(x  y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n  p))" 
54573  55 
proof (induct n) 
56 
case (Suc n) 

57 
have "x ^ Suc (Suc n)  y ^ Suc (Suc n) = x * (x * x ^ n)  y * (y * y ^ n)" 

58 
by simp 

59 
also have "... = y * (x ^ (Suc n)  y ^ (Suc n)) + (x  y) * (x * x ^ n)" 

60 
by (simp add: algebra_simps) 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

61 
also have "... = y * ((x  y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n  p))) + (x  y) * (x * x ^ n)" 
54573  62 
by (simp only: Suc) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

63 
also have "... = (x  y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n  p))) + (x  y) * (x * x ^ n)" 
54573  64 
by (simp only: mult_left_commute) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

65 
also have "... = (x  y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n  p))" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

66 
by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib) 
54573  67 
finally show ?case . 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

69 

55832  70 
corollary power_diff_sumr2: {* @{text COMPLEX_POLYFUN} in HOL Light *} 
55734  71 
fixes x :: "'a::{comm_ring,monoid_mult}" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

72 
shows "x^n  y^n = (x  y) * (\<Sum>i<n. y^(n  Suc i) * x^i)" 
55734  73 
using lemma_realpow_diff_sumr2[of x "n  1" y] 
74 
by (cases "n = 0") (simp_all add: field_simps) 

75 

15229  76 
lemma lemma_realpow_rev_sumr: 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

77 
"(\<Sum>p<Suc n. (x ^ p) * (y ^ (n  p))) = 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

78 
(\<Sum>p<Suc n. (x ^ (n  p)) * (y ^ p))" 
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
57025
diff
changeset

79 
by (subst nat_diff_setsum_reindex[symmetric]) simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

80 

55719
cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

81 
lemma power_diff_1_eq: 
cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

82 
fixes x :: "'a::{comm_ring,monoid_mult}" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

83 
shows "n \<noteq> 0 \<Longrightarrow> x^n  1 = (x  1) * (\<Sum>i<n. (x^i))" 
55719
cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

84 
using lemma_realpow_diff_sumr2 [of x _ 1] 
cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

85 
by (cases n) auto 
cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

86 

cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

87 
lemma one_diff_power_eq': 
cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

88 
fixes x :: "'a::{comm_ring,monoid_mult}" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

89 
shows "n \<noteq> 0 \<Longrightarrow> 1  x^n = (1  x) * (\<Sum>i<n. x^(n  Suc i))" 
55719
cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

90 
using lemma_realpow_diff_sumr2 [of 1 _ x] 
cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

91 
by (cases n) auto 
cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

92 

cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

93 
lemma one_diff_power_eq: 
cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

94 
fixes x :: "'a::{comm_ring,monoid_mult}" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

95 
shows "n \<noteq> 0 \<Longrightarrow> 1  x^n = (1  x) * (\<Sum>i<n. x^i)" 
55719
cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

96 
by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex) 
cdddd073bff8
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents:
55417
diff
changeset

97 

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

98 
text{*Power series has a `circle` of convergence, i.e. if it sums for @{term 
53079  99 
x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*} 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

100 

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

101 
lemma powser_insidea: 
53599  102 
fixes x z :: "'a::real_normed_div_algebra" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

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

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

107 
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

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

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

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

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

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

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

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

116 
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

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

118 
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

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

120 
proof (intro exI allI impI) 
53079  121 
fix n::nat 
122 
assume "0 \<le> n" 

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

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

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

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

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

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

128 
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

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

130 
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

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

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

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

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

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

136 
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

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

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

139 
using x_neq_0 
53599  140 
by (simp add: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric]) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

143 
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

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

145 
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

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

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

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

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

150 
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

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

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

153 

15229  154 
lemma powser_inside: 
53599  155 
fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}" 
53079  156 
shows 
157 
"summable (\<lambda>n. f n * (x ^ n)) \<Longrightarrow> norm z < norm x \<Longrightarrow> 

158 
summable (\<lambda>n. f n * (z ^ n))" 

159 
by (rule powser_insidea [THEN summable_norm_cancel]) 

160 

161 
lemma sum_split_even_odd: 

162 
fixes f :: "nat \<Rightarrow> real" 

163 
shows 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

164 
"(\<Sum>i<2 * n. if even i then f i else g i) = 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

166 
proof (induct n) 
53079  167 
case 0 
168 
then show ?case by simp 

169 
next 

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

170 
case (Suc n) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

171 
have "(\<Sum>i<2 * Suc n. if even i then f i else g i) = 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

172 
(\<Sum>i<n. f (2 * i)) + (\<Sum>i<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

173 
using Suc.hyps unfolding One_nat_def by auto 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

174 
also have "\<dots> = (\<Sum>i<Suc n. f (2 * i)) + (\<Sum>i<Suc n. g (2 * i + 1))" 
53079  175 
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

176 
finally show ?case . 
53079  177 
qed 
178 

179 
lemma sums_if': 

180 
fixes g :: "nat \<Rightarrow> real" 

181 
assumes "g sums x" 

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

182 
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

183 
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

184 
proof (rule LIMSEQ_I) 
53079  185 
fix r :: real 
186 
assume "0 < r" 

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

187 
from `g sums x`[unfolded sums_def, THEN LIMSEQ_D, OF this] 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

188 
obtain no where no_eq: "\<And> n. n \<ge> no \<Longrightarrow> (norm (setsum g {..<n}  x) < r)" by blast 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

189 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

190 
let ?SUM = "\<lambda> m. \<Sum>i<m. if even i then 0 else g ((i  1) div 2)" 
53079  191 
{ 
192 
fix m 

193 
assume "m \<ge> 2 * no" 

194 
hence "m div 2 \<ge> no" by auto 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

195 
have sum_eq: "?SUM (2 * (m div 2)) = setsum g {..< 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

196 
using sum_split_even_odd by auto 
53079  197 
hence "(norm (?SUM (2 * (m div 2))  x) < r)" 
198 
using no_eq unfolding sum_eq using `m div 2 \<ge> no` 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

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

200 
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

201 
proof (cases "even m") 
53079  202 
case True 
203 
show ?thesis 

204 
unfolding even_nat_div_two_times_two[OF True, unfolded numeral_2_eq_2[symmetric]] .. 

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

205 
next 
53079  206 
case False 
207 
hence "even (Suc m)" by auto 

208 
from even_nat_div_two_times_two[OF this, unfolded numeral_2_eq_2[symmetric]] 

209 
odd_nat_plus_one_div_two[OF False, unfolded numeral_2_eq_2[symmetric]] 

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

210 
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

211 
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

212 
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

213 
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

214 
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

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

216 
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

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

218 
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

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

220 

53079  221 
lemma sums_if: 
222 
fixes g :: "nat \<Rightarrow> real" 

223 
assumes "g sums x" and "f sums y" 

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

224 
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

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

226 
let ?s = "\<lambda> n. if even n then 0 else f ((n  1) div 2)" 
53079  227 
{ 
228 
fix B T E 

229 
have "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)" 

230 
by (cases B) auto 

231 
} note if_sum = this 

232 
have g_sums: "(\<lambda> n. if even n then 0 else g ((n  1) div 2)) sums x" 

233 
using sums_if'[OF `g sums x`] . 

41970  234 
{ 
41550  235 
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

236 

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

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

239 
have "(\<lambda> n. if even n then f (n div 2) else 0) sums y" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

240 
by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum_reindex if_eq sums_def cong del: if_cong) 
53079  241 
} 
242 
from sums_add[OF g_sums this] show ?thesis unfolding if_sum . 

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

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

244 

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

245 
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

246 

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

247 
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

248 
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

249 
assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a > 0" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

250 
shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. 1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. 1^i*a i) > l) \<and> 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

252 
(is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)") 
53079  253 
proof (rule nested_sequence_unique) 
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset

254 
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

255 

53079  256 
show "\<forall>n. ?f n \<le> ?f (Suc n)" 
257 
proof 

258 
fix n 

259 
show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto 

260 
qed 

261 
show "\<forall>n. ?g (Suc n) \<le> ?g n" 

262 
proof 

263 
fix n 

264 
show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"] 

265 
unfolding One_nat_def by auto 

266 
qed 

267 
show "\<forall>n. ?f n \<le> ?g n" 

268 
proof 

269 
fix n 

270 
show "?f n \<le> ?g n" using fg_diff a_pos 

271 
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

272 
qed 
53079  273 
show "(\<lambda>n. ?f n  ?g n) > 0" unfolding fg_diff 
274 
proof (rule LIMSEQ_I) 

275 
fix r :: real 

276 
assume "0 < r" 

277 
with `a > 0`[THEN LIMSEQ_D] obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n  0) < r" 

278 
by auto 

279 
hence "\<forall>n \<ge> N. norm ( a (2 * n)  0) < r" by auto 

280 
thus "\<exists>N. \<forall>n \<ge> N. norm ( a (2 * n)  0) < r" by auto 

281 
qed 

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

283 

53079  284 
lemma summable_Leibniz': 
285 
fixes a :: "nat \<Rightarrow> real" 

286 
assumes a_zero: "a > 0" 

287 
and a_pos: "\<And> n. 0 \<le> a n" 

288 
and a_monotone: "\<And> n. a (Suc n) \<le> a n" 

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

289 
shows summable: "summable (\<lambda> n. (1)^n * a n)" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

290 
and "\<And>n. (\<Sum>i<2*n. (1)^i*a i) \<le> (\<Sum>i. (1)^i*a i)" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

291 
and "(\<lambda>n. \<Sum>i<2*n. (1)^i*a i) > (\<Sum>i. (1)^i*a i)" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

292 
and "\<And>n. (\<Sum>i. (1)^i*a i) \<le> (\<Sum>i<2*n+1. (1)^i*a i)" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

294 
proof  
53079  295 
let ?S = "\<lambda>n. (1)^n * a n" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

296 
let ?P = "\<lambda>n. \<Sum>i<n. ?S i" 
53079  297 
let ?f = "\<lambda>n. ?P (2 * n)" 
298 
let ?g = "\<lambda>n. ?P (2 * n + 1)" 

299 
obtain l :: real 

300 
where below_l: "\<forall> n. ?f n \<le> l" 

301 
and "?f > l" 

302 
and above_l: "\<forall> n. l \<le> ?g n" 

303 
and "?g > l" 

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

304 
using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast 
41970  305 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

307 
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

308 
proof (rule LIMSEQ_I) 
53079  309 
fix r :: real 
310 
assume "0 < r" 

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

312 
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

313 

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

315 
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

316 

53079  317 
{ 
318 
fix n :: nat 

319 
assume "n \<ge> (max (2 * f_no) (2 * g_no))" 

320 
hence "n \<ge> 2 * f_no" and "n \<ge> 2 * g_no" 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

321 
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

322 
proof (cases "even n") 
53079  323 
case True 
324 
from even_nat_div_two_times_two[OF this] 

325 
have n_eq: "2 * (n div 2) = n" 

326 
unfolding numeral_2_eq_2[symmetric] by auto 

327 
with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no" 

328 
by auto 

329 
from f[OF this] show ?thesis 

330 
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

331 
next 
53079  332 
case False 
333 
hence "even (n  1)" by simp 

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

334 
from even_nat_div_two_times_two[OF this] 
53079  335 
have n_eq: "2 * ((n  1) div 2) = n  1" 
336 
unfolding numeral_2_eq_2[symmetric] by auto 

337 
hence range_eq: "n  1 + 1 = n" 

338 
using odd_pos[OF False] by auto 

339 

340 
from n_eq `n \<ge> 2 * g_no` have "(n  1) div 2 \<ge> g_no" 

341 
by auto 

342 
from g[OF this] show ?thesis 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

343 
unfolding n_eq 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

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

345 
} 
53079  346 
thus "\<exists>no. \<forall>n \<ge> no. norm (?Sa n  l) < r" 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

347 
qed 
53079  348 
hence sums_l: "(\<lambda>i. (1)^i * a i) sums l" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

350 
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

351 

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

352 
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

353 

53079  354 
fix n 
355 
show "suminf ?S \<le> ?g n" 

356 
unfolding sums_unique[OF sums_l, symmetric] using above_l by auto 

357 
show "?f n \<le> suminf ?S" 

358 
unfolding sums_unique[OF sums_l, symmetric] using below_l by auto 

359 
show "?g > suminf ?S" 

360 
using `?g > l` `l = suminf ?S` by auto 

361 
show "?f > suminf ?S" 

362 
using `?f > l` `l = suminf ?S` 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

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

364 

53079  365 
theorem summable_Leibniz: 
366 
fixes a :: "nat \<Rightarrow> real" 

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

367 
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

368 
shows "summable (\<lambda> n. (1)^n * a n)" (is "?summable") 
53079  369 
and "0 < a 0 \<longrightarrow> 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

370 
(\<forall>n. (\<Sum>i. 1^i*a i) \<in> { \<Sum>i<2*n. 1^i * a i .. \<Sum>i<2*n+1. 1^i * a i})" (is "?pos") 
53079  371 
and "a 0 < 0 \<longrightarrow> 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

372 
(\<forall>n. (\<Sum>i. 1^i*a i) \<in> { \<Sum>i<2*n+1. 1^i * a i .. \<Sum>i<2*n. 1^i * a i})" (is "?neg") 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

373 
and "(\<lambda>n. \<Sum>i<2*n. 1^i*a i) > (\<Sum>i. 1^i*a i)" (is "?f") 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

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

376 
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

377 
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

378 
case True 
53079  379 
hence ord: "\<And>n m. m \<le> n \<Longrightarrow> a n \<le> a m" and ge0: "\<And> n. 0 \<le> a n" 
380 
by auto 

381 
{ 

382 
fix n 

383 
have "a (Suc n) \<le> a n" 

384 
using ord[where n="Suc n" and m=n] by auto 

385 
} note mono = this 

386 
note leibniz = summable_Leibniz'[OF `a > 0` ge0] 

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

387 
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

388 
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

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

390 
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

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

392 
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

393 
have "(\<forall> n. a n \<le> 0) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)" by auto 
53079  394 
hence ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n" 
395 
by auto 

396 
{ 

397 
fix n 

398 
have "?a (Suc n) \<le> ?a n" using ord[where n="Suc n" and m=n] 

399 
by auto 

400 
} note monotone = this 

401 
note leibniz = 

402 
summable_Leibniz'[OF _ ge0, of "\<lambda>x. x", 

403 
OF tendsto_minus[OF `a > 0`, unfolded minus_zero] monotone] 

404 
have "summable (\<lambda> n. (1)^n * ?a n)" 

405 
using leibniz(1) by auto 

406 
then obtain l where "(\<lambda> n. (1)^n * ?a n) sums l" 

407 
unfolding summable_def by auto 

408 
from this[THEN sums_minus] have "(\<lambda> n. (1)^n * a n) sums l" 

409 
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

410 
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

411 
moreover 
53079  412 
have "\<And>a b :: real. \<bar> a   b\<bar> = \<bar>a  b\<bar>" 
413 
unfolding minus_diff_minus by auto 

41970  414 

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

415 
from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus] 
53079  416 
have move_minus: "(\<Sum>n.  (1 ^ n * a n)) =  (\<Sum>n. 1 ^ n * a n)" 
417 
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

418 

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

419 
have ?pos using `0 \<le> ?a 0` by auto 
53079  420 
moreover have ?neg 
421 
using leibniz(2,4) 

422 
unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le 

423 
by auto 

424 
moreover have ?f and ?g 

425 
using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel] 

426 
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

427 
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

428 
qed 
54576  429 
then show ?summable and ?pos and ?neg and ?f and ?g 
54573  430 
by safe 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

432 

29164  433 
subsection {* TermbyTerm Differentiability of Power Series *} 
23043  434 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

435 
definition diffs :: "(nat \<Rightarrow> 'a::ring_1) \<Rightarrow> nat \<Rightarrow> 'a" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

436 
where "diffs c = (\<lambda>n. of_nat (Suc n) * c (Suc n))" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

437 

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

438 
text{*Lemma about distributing negation over it*} 
53079  439 
lemma diffs_minus: "diffs (\<lambda>n.  c n) = (\<lambda>n.  diffs c n)" 
440 
by (simp add: diffs_def) 

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

441 

29163  442 
lemma sums_Suc_imp: 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

443 
"(f::nat \<Rightarrow> 'a::real_normed_vector) 0 = 0 \<Longrightarrow> (\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

444 
using sums_Suc_iff[of f] by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

445 

15229  446 
lemma diffs_equiv: 
41970  447 
fixes x :: "'a::{real_normed_vector, ring_1}" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

448 
shows "summable (\<lambda>n. diffs c n * x^n) \<Longrightarrow> 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

449 
(\<lambda>n. of_nat n * c n * x^(n  Suc 0)) sums (\<Sum>n. diffs c n * x^n)" 
53079  450 
unfolding diffs_def 
54573  451 
by (simp add: summable_sums sums_Suc_imp) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

452 

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

453 
lemma lemma_termdiff1: 
31017  454 
fixes z :: "'a :: {monoid_mult,comm_ring}" shows 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

455 
"(\<Sum>p<m. (((z + h) ^ (m  p)) * (z ^ p))  (z ^ m)) = 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

458 

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

459 
lemma sumr_diff_mult_const2: 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

460 
"setsum f {..<n}  of_nat n * (r::'a::ring_1) = (\<Sum>i<n. f i  r)" 
53079  461 
by (simp add: setsum_subtractf) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

462 

15229  463 
lemma lemma_termdiff2: 
31017  464 
fixes h :: "'a :: {field}" 
53079  465 
assumes h: "h \<noteq> 0" 
466 
shows 

467 
"((z + h) ^ n  z ^ n) / h  of_nat n * z ^ (n  Suc 0) = 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

468 
h * (\<Sum>p< n  Suc 0. \<Sum>q< n  Suc 0  p. 
53079  469 
(z + h) ^ q * z ^ (n  2  q))" (is "?lhs = ?rhs") 
470 
apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h) 

471 
apply (simp add: right_diff_distrib diff_divide_distrib h) 

472 
apply (simp add: mult_assoc [symmetric]) 

473 
apply (cases "n", simp) 

474 
apply (simp add: lemma_realpow_diff_sumr2 h 

475 
right_diff_distrib [symmetric] mult_assoc 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

476 
del: power_Suc setsum_lessThan_Suc of_nat_Suc) 
53079  477 
apply (subst lemma_realpow_rev_sumr) 
478 
apply (subst sumr_diff_mult_const2) 

479 
apply simp 

480 
apply (simp only: lemma_termdiff1 setsum_right_distrib) 

481 
apply (rule setsum_cong [OF refl]) 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset

482 
apply (simp add: less_iff_Suc_add) 
53079  483 
apply (clarify) 
484 
apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

485 
del: setsum_lessThan_Suc power_Suc) 
53079  486 
apply (subst mult_assoc [symmetric], subst power_add [symmetric]) 
487 
apply (simp add: mult_ac) 

488 
done 

20860  489 

490 
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

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

492 
assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K" 
53079  493 
and K: "0 \<le> K" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

494 
shows "setsum f {..<nk} \<le> of_nat n * K" 
53079  495 
apply (rule order_trans [OF setsum_mono]) 
496 
apply (rule f, simp) 

497 
apply (simp add: mult_right_mono K) 

498 
done 

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

499 

15229  500 
lemma lemma_termdiff3: 
31017  501 
fixes h z :: "'a::{real_normed_field}" 
20860  502 
assumes 1: "h \<noteq> 0" 
53079  503 
and 2: "norm z \<le> K" 
504 
and 3: "norm (z + h) \<le> K" 

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

505 
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

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

508 
have "norm (((z + h) ^ n  z ^ n) / h  of_nat n * z ^ (n  Suc 0)) = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

510 
(z + h) ^ q * z ^ (n  2  q)) * norm h" 
54573  511 
by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult_commute norm_mult) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

512 
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

513 
proof (rule mult_right_mono [OF _ norm_ge_zero]) 
53079  514 
from norm_ge_zero 2 have K: "0 \<le> K" 
515 
by (rule order_trans) 

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

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

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

519 
apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K) 
20860  520 
done 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

521 
show "norm (\<Sum>p<n  Suc 0. \<Sum>q<n  Suc 0  p. (z + h) ^ q * z ^ (n  2  q)) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

524 
order_trans [OF norm_setsum] 
20860  525 
real_setsum_nat_ivl_bounded2 
526 
mult_nonneg_nonneg 

47489  527 
of_nat_0_le_iff 
20860  528 
zero_le_power K) 
529 
apply (rule le_Kn, simp) 

530 
done 

531 
qed 

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

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

535 
qed 

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

536 

20860  537 
lemma lemma_termdiff4: 
56167  538 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
20860  539 
assumes k: "0 < (k::real)" 
53079  540 
and le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h" 
20860  541 
shows "f  0 > 0" 
56167  542 
proof (rule tendsto_norm_zero_cancel) 
543 
show "(\<lambda>h. norm (f h))  0 > 0" 

544 
proof (rule real_tendsto_sandwich) 

545 
show "eventually (\<lambda>h. 0 \<le> norm (f h)) (at 0)" 

20860  546 
by simp 
56167  547 
show "eventually (\<lambda>h. norm (f h) \<le> K * norm h) (at 0)" 
548 
using k by (auto simp add: eventually_at dist_norm le) 

549 
show "(\<lambda>h. 0)  (0::'a) > (0::real)" 

550 
by (rule tendsto_const) 

551 
have "(\<lambda>h. K * norm h)  (0::'a) > K * norm (0::'a)" 

552 
by (intro tendsto_intros) 

553 
then show "(\<lambda>h. K * norm h)  (0::'a) > 0" 

554 
by simp 

20860  555 
qed 
556 
qed 

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

557 

15229  558 
lemma lemma_termdiff5: 
56167  559 
fixes g :: "'a::real_normed_vector \<Rightarrow> nat \<Rightarrow> 'b::banach" 
20860  560 
assumes k: "0 < (k::real)" 
561 
assumes f: "summable f" 

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

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

53079  565 
fix h::'a 
566 
assume "h \<noteq> 0" and "norm h < k" 

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

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

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

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

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

575 
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

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

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

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

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

583 

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

584 

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

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

586 

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

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

589 
assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)" 
53079  590 
and 2: "norm x < norm K" 
20860  591 
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

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

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

595 
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

596 
from norm_ge_zero r1 have r: "0 < r" 
20860  597 
by (rule order_le_less_trans) 
598 
hence r_neq_0: "r \<noteq> 0" by simp 

599 
show ?thesis 

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

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

601 
show "0 < r  norm x" using r1 by simp 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

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

606 
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

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

608 
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

609 
hence "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n  Suc 0))" 
20860  610 
by (rule diffs_equiv [THEN sums_summable]) 
53079  611 
also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n  Suc 0)) = 
612 
(\<lambda>n. diffs (\<lambda>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

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

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

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

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

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

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

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

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

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

625 
apply (case_tac "n", simp) 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
54576
diff
changeset

626 
apply (rename_tac nat) 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

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

629 
done 
53079  630 
finally 
631 
show "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

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

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

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

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

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

639 
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

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

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

642 
apply (rule mult_left_mono [OF _ norm_ge_zero]) 
54575  643 
apply (simp add: mult_assoc [symmetric]) 
644 
apply (metis h lemma_termdiff3 less_eq_real_def r1 xh) 

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

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

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

648 

20860  649 
lemma termdiffs: 
31017  650 
fixes K x :: "'a::{real_normed_field,banach}" 
20860  651 
assumes 1: "summable (\<lambda>n. c n * K ^ n)" 
54575  652 
and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)" 
653 
and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)" 

654 
and 4: "norm x < norm K" 

20860  655 
shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)" 
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

656 
unfolding DERIV_def 
29163  657 
proof (rule LIM_zero_cancel) 
20860  658 
show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n)  suminf (\<lambda>n. c n * x ^ n)) / h 
659 
 suminf (\<lambda>n. diffs c n * x ^ n))  0 > 0" 

660 
proof (rule LIM_equal2) 

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

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

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

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

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

667 
by (rule norm_triangle_ineq [THEN order_le_less_trans]) 
56167  668 
have "summable (\<lambda>n. c n * x ^ n)" 
669 
and "summable (\<lambda>n. c n * (x + h) ^ n)" 

670 
and "summable (\<lambda>n. diffs c n * x ^ n)" 

671 
using 1 2 4 5 by (auto elim: powser_inside) 

672 
then have "((\<Sum>n. c n * (x + h) ^ n)  (\<Sum>n. c n * x ^ n)) / h  (\<Sum>n. diffs c n * x ^ n) = 

673 
(\<Sum>n. (c n * (x + h) ^ n  c n * x ^ n) / h  of_nat n * c n * x ^ (n  Suc 0))" 

674 
by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums) 

675 
then show "((\<Sum>n. c n * (x + h) ^ n)  (\<Sum>n. c n * x ^ n)) / h  (\<Sum>n. diffs c n * x ^ n) = 

676 
(\<Sum>n. c n * (((x + h) ^ n  x ^ n) / h  of_nat n * x ^ (n  Suc 0)))" 

54575  677 
by (simp add: algebra_simps) 
20860  678 
next 
53079  679 
show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n  x ^ n) / h  of_nat n * x ^ (n  Suc 0)))  0 > 0" 
680 
by (rule termdiffs_aux [OF 3 4]) 

20860  681 
qed 
682 
qed 

683 

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

684 

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

685 
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

686 

53079  687 
lemma DERIV_series': 
688 
fixes f :: "real \<Rightarrow> nat \<Rightarrow> real" 

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

689 
assumes DERIV_f: "\<And> n. DERIV (\<lambda> x. f x n) x0 :> (f' x0 n)" 
53079  690 
and allf_summable: "\<And> x. x \<in> {a <..< b} \<Longrightarrow> summable (f x)" and x0_in_I: "x0 \<in> {a <..< b}" 
691 
and "summable (f' x0)" 

692 
and "summable L" 

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

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

694 
shows "DERIV (\<lambda> x. suminf (f x)) x0 :> (suminf (f' x0))" 
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

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

696 
proof (rule LIM_I) 
53079  697 
fix r :: real 
698 
assume "0 < r" hence "0 < r/3" 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

699 

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

701 
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

702 

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

704 
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

705 

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

706 
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

707 
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

708 
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

709 

53079  710 
let ?diff = "\<lambda>i x. (f (x0 + x) i  f x0 i) / x" 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

711 

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

712 
let ?r = "r / (3 * real ?N)" 
56541  713 
from `0 < r` have "0 < ?r" by simp 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

714 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

715 
let ?s = "\<lambda>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)" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

717 

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

718 
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

719 
proof (rule iffD2[OF Min_gr_iff]) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

720 
show "\<forall>x \<in> (?s ` {..< ?N }). 0 < x" 
53079  721 
proof 
722 
fix x 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

723 
assume "x \<in> ?s ` {..<?N}" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

724 
then obtain n where "x = ?s n" and "n \<in> {..<?N}" 
53079  725 
using image_iff[THEN iffD1] by blast 
41970  726 
from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def] 
53079  727 
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)" 
728 
by auto 

729 
have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound) 

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

730 
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

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

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

733 

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

734 
def S \<equiv> "min (min (x0  a) (b  x0)) S'" 
53079  735 
hence "0 < S" and S_a: "S \<le> x0  a" and S_b: "S \<le> b  x0" 
736 
and "S \<le> S'" using x0_in_I and `0 < S'` 

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

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

738 

53079  739 
{ 
740 
fix x 

741 
assume "x \<noteq> 0" and "\<bar> x \<bar> < S" 

742 
hence x_in_I: "x0 + x \<in> { a <..< b }" 

743 
using S_a S_b by auto 

41970  744 

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

745 
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

746 
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

747 
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

748 
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

749 
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

750 
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

751 
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

752 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

753 
{ fix n 
41970  754 
have "\<bar> ?diff (n + ?N) x \<bar> \<le> L (n + ?N) * \<bar> (x0 + x)  x0 \<bar> / \<bar> x \<bar>" 
53079  755 
using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero] 
756 
unfolding abs_divide . 

757 
hence "\<bar> (\<bar>?diff (n + ?N) x \<bar>) \<bar> \<le> L (n + ?N)" 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

758 
using `x \<noteq> 0` by auto } 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

759 
note 1 = this and 2 = summable_rabs_comparison_test[OF _ ign[OF `summable L`]] 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

760 
then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))" 
56213  761 
by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] suminf_le[OF _ 2 ign[OF `summable L`]]]) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

762 
then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3") 
53079  763 
using L_estimate by auto 
764 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

765 
have "\<bar>\<Sum>n<?N. ?diff n x  f' x0 n \<bar> \<le> (\<Sum>n<?N. \<bar>?diff n x  f' x0 n \<bar>)" .. 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

767 
proof (rule setsum_strict_mono) 
53079  768 
fix n 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

769 
assume "n \<in> {..< ?N}" 
53079  770 
have "\<bar>x\<bar> < S" using `\<bar>x\<bar> < S` . 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

773 
proof (rule Min_le_iff[THEN iffD2]) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

774 
have "?s n \<in> (?s ` {..<?N}) \<and> ?s n \<le> ?s n" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

775 
using `n \<in> {..< ?N}` by auto 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

776 
thus "\<exists> a \<in> (?s ` {..<?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

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

779 

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

780 
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

781 
have "\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < ?s n \<longrightarrow> \<bar>?diff n x  f' x0 n\<bar> < ?r" . 
53079  782 
with `x \<noteq> 0` and `\<bar>x\<bar> < ?s n` show "\<bar>?diff n x  f' x0 n\<bar> < ?r" 
783 
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

784 
qed auto 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

785 
also have "\<dots> = of_nat (card {..<?N}) * ?r" 
53079  786 
by (rule setsum_constant) 
787 
also have "\<dots> = real ?N * ?r" 

788 
unfolding real_eq_of_nat 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

789 
also have "\<dots> = r/3" by auto 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

790 
finally have "\<bar>\<Sum>n<?N. ?diff n x  f' x0 n \<bar> < r / 3" (is "?diff_part < 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

791 

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

792 
from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]] 
53079  793 
have "\<bar>(suminf (f (x0 + x))  (suminf (f x0))) / x  suminf (f' x0)\<bar> = 
794 
\<bar>\<Sum>n. ?diff n x  f' x0 n\<bar>" 

795 
unfolding suminf_diff[OF div_smbl `summable (f' x0)`, symmetric] 

796 
using suminf_divide[OF diff_smbl, symmetric] by auto 

797 
also have "\<dots> \<le> ?diff_part + \<bar> (\<Sum>n. ?diff (n + ?N) x)  (\<Sum> n. f' x0 (n + ?N)) \<bar>" 

798 
unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"] 

799 
unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]] 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

800 
apply (subst (5) add_commute) 
53079  801 
by (rule abs_triangle_ineq) 
802 
also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part" 

803 
using abs_triangle_ineq4 by auto 

41970  804 
also have "\<dots> < r /3 + r/3 + r/3" 
36842  805 
using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3` 
806 
by (rule add_strict_mono [OF add_less_le_mono]) 

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

808 
by auto 
53079  809 
} 
810 
thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x  0) < s \<longrightarrow> 

811 
norm (((\<Sum>n. f (x0 + x) n)  (\<Sum>n. f x0 n)) / x  (\<Sum>n. f' x0 n)) < r" 

812 
using `0 < S` unfolding real_norm_def diff_0_right 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

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

814 

53079  815 
lemma DERIV_power_series': 
816 
fixes f :: "nat \<Rightarrow> real" 

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

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

819 
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

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

821 
proof  
53079  822 
{ 
823 
fix R' 

824 
assume "0 < R'" and "R' < R" and "R' < x0" and "x0 < R'" 

825 
hence "x0 \<in> {R' <..< R'}" and "R' \<in> {R <..< R}" and "x0 \<in> {R <..< R}" 

826 
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

827 
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

828 
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

829 
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

830 
proof  
53079  831 
have "(R' + R) / 2 < R" and "0 < (R' + R) / 2" 
832 
using `0 < R'` `0 < R` `R' < R` by auto 

833 
hence in_Rball: "(R' + R) / 2 \<in> {R <..< R}" 

834 
using `R' < R` by auto 

835 
have "norm R' < norm ((R' + R) / 2)" 

836 
using `0 < R'` `0 < R` `R' < R` by auto 

837 
from powser_insidea[OF converges[OF in_Rball] this] show ?thesis 

838 
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

839 
qed 
53079  840 
{ 
841 
fix n x y 

842 
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

843 
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

844 
proof  
53079  845 
have "\<bar>f n * x ^ (Suc n)  f n * y ^ (Suc n)\<bar> = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

846 
(\<bar>f n\<bar> * \<bar>xy\<bar>) * \<bar>\<Sum>p<Suc n. x ^ p * y ^ (n  p)\<bar>" 
53079  847 
unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult 
848 
by auto 

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

850 
proof (rule mult_left_mono) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

851 
have "\<bar>\<Sum>p<Suc n. x ^ p * y ^ (n  p)\<bar> \<le> (\<Sum>p<Suc n. \<bar>x ^ p * y ^ (n  p)\<bar>)" 
53079  852 
by (rule setsum_abs) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

854 
proof (rule setsum_mono) 
53079  855 
fix p 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

856 
assume "p \<in> {..<Suc n}" 
53079  857 
hence "p \<le> n" by auto 
858 
{ 

859 
fix n 

860 
fix x :: real 

861 
assume "x \<in> {R'<..<R'}" 

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

862 
hence "\<bar>x\<bar> \<le> R'" by auto 
53079  863 
hence "\<bar>x^n\<bar> \<le> R'^n" 
864 
unfolding power_abs by (rule power_mono, auto) 

865 
} 

866 
from mult_mono[OF this[OF `x \<in> {R'<..<R'}`, of p] this[OF `y \<in> {R'<..<R'}`, of "np"]] `0 < R'` 

867 
have "\<bar>x^p * y^(np)\<bar> \<le> R'^p * R'^(np)" 

868 
unfolding abs_mult by auto 

869 
thus "\<bar>x^p * y^(np)\<bar> \<le> R'^n" 

870 
unfolding power_add[symmetric] using `p \<le> n` by auto 

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

871 
qed 
53079  872 
also have "\<dots> = real (Suc n) * R' ^ n" 
873 
unfolding setsum_constant card_atLeastLessThan real_of_nat_def by auto 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

874 
finally show "\<bar>\<Sum>p<Suc n. x ^ p * y ^ (n  p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>" 
53079  875 
unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] . 
876 
show "0 \<le> \<bar>f n\<bar> * \<bar>x  y\<bar>" 

877 
unfolding abs_mult[symmetric] by auto 

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

878 
qed 
53079  879 
also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x  y\<bar>" 
880 
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

881 
finally show ?thesis . 
53079  882 
qed 
883 
} 

884 
{ 

885 
fix n 

886 
show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)" 

56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

887 
by (auto intro!: derivative_eq_intros simp del: power_Suc simp: real_of_nat_def) 
53079  888 
} 
889 
{ 

890 
fix x 

891 
assume "x \<in> {R' <..< R'}" 

892 
hence "R' \<in> {R <..< R}" and "norm x < norm R'" 

893 
using assms `R' < R` by auto 

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

894 
have "summable (\<lambda> n. f n * x^n)" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

895 
proof (rule summable_comparison_test, intro exI allI impI) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

896 
fix n 
53079  897 
have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)" 
898 
by (rule mult_left_mono) auto 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

899 
show "norm (f n * x ^ n) \<le> norm (f n * real (Suc n) * x ^ n)" 
53079  900 
unfolding real_norm_def abs_mult 
901 
by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right]) 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

902 
qed (rule powser_insidea[OF converges[OF `R' \<in> {R <..< R}`] `norm x < norm R'`]) 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36776
diff
changeset

903 
from this[THEN summable_mult2[where c=x], unfolded mult_assoc, unfolded mult_commute] 
53079  904 
show "summable (?f x)" by auto 
905 
} 

906 
show "summable (?f' x0)" 

907 
using converges[OF `x0 \<in> {R <..< R}`] . 

908 
show "x0 \<in> {R' <..< R'}" 

909 
using `x0 \<in> {R' <..< R'}` . 

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

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

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

912 
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

913 
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

914 
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

915 
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

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

917 
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

918 
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

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

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

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

923 
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

924 
qed 
53079  925 
hence "0 < ?R" "?R < R" " ?R < x0" and "x0 < ?R" 
926 
using assms 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

927 
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

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

929 
qed 
29695  930 

53079  931 

29164  932 
subsection {* Exponential Function *} 
23043  933 

53079  934 
definition exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" 
935 
where "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))" 

23043  936 

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

937 
lemma summable_exp_generic: 
31017  938 
fixes x :: "'a::{real_normed_algebra_1,banach}" 
25062  939 
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

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

941 
proof  
25062  942 
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

943 
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

944 
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

945 
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

946 
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

947 
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

948 
from r1 show ?thesis 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

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

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

952 
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

953 
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

954 
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

955 
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

956 
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

957 
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

958 
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

959 
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

960 
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

961 
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

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

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

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

966 

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

967 
lemma summable_norm_exp: 
31017  968 
fixes x :: "'a::{real_normed_algebra_1,banach}" 
25062  969 
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

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

972 
by (rule summable_exp_generic) 
53079  973 
fix n 
974 
show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)" 

35216  975 
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

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

977 

53079  978 
lemma summable_exp: "summable (\<lambda>n. inverse (real (fact n)) * x ^ n)" 
979 
using summable_exp_generic [where x=x] by simp 

23043  980 

25062  981 
lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x" 
53079  982 
unfolding exp_def by (rule summable_exp_generic [THEN summable_sums]) 
23043  983 

984 

41970  985 
lemma exp_fdiffs: 
53079  986 
"diffs (\<lambda>n. inverse(real (fact n))) = (\<lambda>n. inverse(real (fact n)))" 
987 
by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def of_nat_mult 

988 
del: mult_Suc of_nat_Suc) 

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

989 

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

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

992 

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

993 
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" 
53079  994 
unfolding exp_def scaleR_conv_of_real 
995 
apply (rule DERIV_cong) 

996 
apply (rule termdiffs [where K="of_real (1 + norm x)"]) 

997 
apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs) 

998 
apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+ 

999 
apply (simp del: of_real_add) 

1000 
done 

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

1001 

56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

1002 
declare DERIV_exp[THEN DERIV_chain2, derivative_intros] 
51527  1003 

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

1006 

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

1008 
by (rule isCont_o2 [OF _ isCont_exp]) 

1009 

1010 
lemma tendsto_exp [tendsto_intros]: 

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

1012 
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

1013 

53079  1014 
lemma continuous_exp [continuous_intros]: 
1015 
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))" 

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

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

1017 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56261
diff
changeset

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

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

1021 

53079  1022 

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

1024 

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

1028 
proof  
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

1029 
have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)" 
56213  1030 
by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left) 
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset

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

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

1033 

23278  1034 
lemma exp_zero [simp]: "exp 0 = 1" 
53079  1035 
unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero) 
23278  1036 

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

1037 
lemma exp_series_add: 
31017  1038 
fixes x y :: "'a::{real_field}" 
25062  1039 
defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)" 
56213  1040 
shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n  i))" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

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

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

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

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

1046 
case (Suc n) 
25062  1047 
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

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

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

1051 

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

1053 
by (simp only: times_S) 
56213  1054 
also have "\<dots> = (x + y) * (\<Sum>i\<le>n. S x i * S y (ni))" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

1055 
by (simp only: Suc) 
56213  1056 
also have "\<dots> = x * (\<Sum>i\<le>n. S x i * S y (ni)) 
1057 
+ y * (\<Sum>i\<le>n. S x i * S y (ni))" 

49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47489
diff
changeset

1058 
by (rule distrib_right) 
56213  1059 
also have "\<dots> = (\<Sum>i\<le>n. (x * S x i) * S y (ni)) 
1060 
+ (\<Sum>i\<le>n. S x i * (y * S y (ni)))" 

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

1061 
by (simp only: setsum_right_distrib mult_ac) 
56213  1062 
also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (ni))) 
1063 
+ (\<Sum>i\<le>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

1064 
by (simp add: times_S Suc_diff_le) 
56213  1065 
also have "(\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (ni))) = 
1066 
(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc ni)))" 

1067 
by (subst setsum_atMost_Suc_shift) simp 

1068 
also have "(\<Sum>i\<le>n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni))) = 

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

1070 
by simp 

1071 
also have "(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc ni))) + 

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

1073 
(\<Sum>i\<le>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

1074 
by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric] 
56213  1075 
real_of_nat_add [symmetric]) simp 
1076 
also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i\<le>Suc n. S x i * S y (Suc ni))" 

23127  1077 
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

1078 
finally show 
56213  1079 
"S (x + y) (Suc n) = (\<Sum>i\<le>Suc n. S x i * S y (Suc n  i))" 
35216  1080 
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

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

1082 

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

1083 
lemma exp_add: "exp (x + y) = exp x * exp y" 
53079  1084 
unfolding exp_def 
1085 
by (simp only: Cauchy_product summable_norm_exp exp_series_add) 

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

1086 

29170  1087 
lemma mult_exp_exp: "exp x * exp y = exp (x + y)" 
53079  1088 
by (rule exp_add [symmetric]) 
29170  1089 

23241  1090 
lemma exp_of_real: "exp (of_real x) = of_real (exp x)" 
53079  1091 
unfolding exp_def 
1092 
apply (subst suminf_of_real) 

1093 
apply (rule summable_exp_generic) 

1094 
apply (simp add: scaleR_conv_of_real) 

1095 
done 

23241  1096 

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

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

1100 
also assume "exp x = 0" 

1101 
finally show "False" by simp 

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

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

1103 

29170  1104 
lemma exp_minus: "exp ( x) = inverse (exp x)" 
53079  1105 
by (rule inverse_unique [symmetric], simp add: mult_exp_exp) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1106 

29170  1107 
lemma exp_diff: "exp (x  y) = exp x / exp y" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset

1108 
using exp_add [of x " y"] by (simp add: exp_minus divide_inverse) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1109 

29167  1110 

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

1112 

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

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

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

1117 
proof  

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

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

1120 
qed 

1121 

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

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

1124 

29170  1125 
lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0" 
53079  1126 
by (simp add: not_less) 
29170  1127 

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

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

1130 

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

1131 
lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x" 
53079  1132 
by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1133 

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

1134 
lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" 
53079  1135 
by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult_commute) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1136 

29170  1137 
text {* Strict monotonicity of exponential. *} 
1138 

54575  1139 
lemma exp_ge_add_one_self_aux: 
1140 
assumes "0 \<le> (x::real)" shows "1+x \<le> exp(x)" 

1141 
using order_le_imp_less_or_eq [OF assms] 

1142 
proof 

1143 
assume "0 < x" 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

1144 
have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)" 
54575  1145 
by (auto simp add: numeral_2_eq_2) 
1146 
also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)" 

56213  1147 
apply (rule setsum_le_suminf [OF summable_exp]) 
54575  1148 
using `0 < x` 
1149 
apply (auto simp add: zero_le_mult_iff) 

1150 
done 

1151 
finally show "1+x \<le> exp x" 

1152 
by (simp add: exp_def) 

1153 
next 

1154 
assume "0 = x" 

1155 
then show "1 + x \<le> exp x" 

1156 
by auto 

1157 
qed 

29170  1158 

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

1160 
proof  

1161 
assume x: "0 < x" 

1162 
hence "1 < 1 + x" by simp 

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

1164 
by (simp add: exp_ge_add_one_self_aux) 

1165 
finally show ?thesis . 

1166 
qed 

1167 

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

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

1169 
fixes x y :: real 
53079  1170 
assumes "x < y" 
1171 
shows "exp x < exp y" 

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

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

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

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

1175 
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

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

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

1178 

53079  1179 
lemma exp_less_cancel: "exp (x::real) < exp y \<Longrightarrow> x < y" 
54575  1180 
unfolding linorder_not_le [symmetric] 
1181 
by (auto simp add: order_le_less exp_less_mono) 

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

1182 

29170  1183 
lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y" 
53079  1184 
by (auto intro: exp_less_mono exp_less_cancel) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1185 

29170  1186 
lemma exp_le_cancel_iff [iff]: "exp (x::real) \<le> exp y \<longleftrightarrow> x \<le> y" 
53079  1187 
by (auto simp add: linorder_not_less [symmetric]) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1188 

29170  1189 
lemma exp_inj_iff [iff]: "exp (x::real) = exp y \<longleftrightarrow> x = y" 
53079  1190 
by (simp add: order_eq_iff) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1191 

29170  1192 
text {* Comparisons of @{term "exp x"} with one. *} 
1193 

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

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

1196 

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

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

1199 

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

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

1202 

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

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

1205 

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

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

1208 

53079  1209 
lemma lemma_exp_total: "1 \<le> y \<Longrightarrow> \<exists>x. 0 \<le> x & x \<le> y  1 & exp(x::real) = y" 
44755  1210 
proof (rule IVT) 
1211 
assume "1 \<le> y" 

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

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

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

1215 
qed (simp_all add: le_diff_eq) 

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

1216 

53079  1217 
lemma exp_total: "0 < (y::real) \<Longrightarrow> \<exists>x. exp x = y" 
44755  1218 
proof (rule linorder_le_cases [of 1 y]) 
53079  1219 
assume "1 \<le> y" 
1220 
thus "\<exists>x. exp x = y" by (fast dest: lemma_exp_total) 

44755  1221 
next 
1222 
assume "0 < y" and "y \<le> 1" 

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

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

