author  hoelzl 
Tue, 20 May 2014 19:24:39 +0200  
changeset 57025  e7fd64f82876 
parent 56952  efa2a83d548b 
child 57129  7edb7550663e 
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))" 
53079  79 
apply (rule setsum_reindex_cong [where f="\<lambda>i. n  i"]) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

80 
apply (auto simp: image_iff Bex_def intro!: inj_onI) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

81 
apply arith 
53079  82 
done 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

83 

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

84 
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

85 
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

86 
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

87 
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

88 
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

89 

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

90 
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

91 
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

92 
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

93 
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

94 
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

95 

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

96 
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

97 
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

98 
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

99 
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

100 

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

101 
text{*Power series has a `circle` of convergence, i.e. if it sums for @{term 
53079  102 
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

103 

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

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

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

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

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

110 
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

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

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

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

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

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

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

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

119 
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

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

121 
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

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

123 
proof (intro exI allI impI) 
53079  124 
fix n::nat 
125 
assume "0 \<le> n" 

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

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

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

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

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

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

131 
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

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

133 
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

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

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

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

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

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

139 
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

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

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

142 
using x_neq_0 
53599  143 
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

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

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

146 
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

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

148 
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

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

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

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

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

153 
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

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

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

156 

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

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

162 
by (rule powser_insidea [THEN summable_norm_cancel]) 

163 

164 
lemma sum_split_even_odd: 

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

166 
shows 

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

167 
"(\<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

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

169 
proof (induct n) 
53079  170 
case 0 
171 
then show ?case by simp 

172 
next 

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

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

174 
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

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

176 
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

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

179 
finally show ?case . 
53079  180 
qed 
181 

182 
lemma sums_if': 

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

184 
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

185 
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

186 
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

187 
proof (rule LIMSEQ_I) 
53079  188 
fix r :: real 
189 
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

190 
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

191 
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

192 

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

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

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

197 
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

198 
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

199 
using sum_split_even_odd by auto 
53079  200 
hence "(norm (?SUM (2 * (m div 2))  x) < r)" 
201 
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

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

203 
have "?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

204 
proof (cases "even m") 
53079  205 
case True 
206 
show ?thesis 

207 
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

208 
next 
53079  209 
case False 
210 
hence "even (Suc m)" by auto 

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

212 
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

213 
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

214 
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

215 
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

216 
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

217 
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

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

219 
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

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

221 
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

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

223 

53079  224 
lemma sums_if: 
225 
fixes g :: "nat \<Rightarrow> real" 

226 
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

227 
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

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

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

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

233 
by (cases B) auto 

234 
} note if_sum = this 

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

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

41970  237 
{ 
41550  238 
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

239 

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

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

242 
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

243 
by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum_reindex if_eq sums_def cong del: if_cong) 
53079  244 
} 
245 
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

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

247 

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

248 
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

249 

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

250 
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

251 
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

252 
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

253 
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

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

255 
(is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)") 
53079  256 
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

257 
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

258 

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

261 
fix n 

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

263 
qed 

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

265 
proof 

266 
fix n 

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

268 
unfolding One_nat_def by auto 

269 
qed 

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

271 
proof 

272 
fix n 

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

274 
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

275 
qed 
53079  276 
show "(\<lambda>n. ?f n  ?g n) > 0" unfolding fg_diff 
277 
proof (rule LIMSEQ_I) 

278 
fix r :: real 

279 
assume "0 < r" 

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

281 
by auto 

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

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

284 
qed 

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

286 

53079  287 
lemma summable_Leibniz': 
288 
fixes a :: "nat \<Rightarrow> real" 

289 
assumes a_zero: "a > 0" 

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

291 
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

292 
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

293 
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

294 
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

295 
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

296 
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

297 
proof  
53079  298 
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

299 
let ?P = "\<lambda>n. \<Sum>i<n. ?S i" 
53079  300 
let ?f = "\<lambda>n. ?P (2 * n)" 
301 
let ?g = "\<lambda>n. ?P (2 * n + 1)" 

302 
obtain l :: real 

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

304 
and "?f > l" 

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

306 
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

307 
using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast 
41970  308 

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

309 
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

310 
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

311 
proof (rule LIMSEQ_I) 
53079  312 
fix r :: real 
313 
assume "0 < r" 

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

315 
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

316 

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

318 
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

319 

53079  320 
{ 
321 
fix n :: nat 

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

323 
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

324 
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

325 
proof (cases "even n") 
53079  326 
case True 
327 
from even_nat_div_two_times_two[OF this] 

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

329 
unfolding numeral_2_eq_2[symmetric] by auto 

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

331 
by auto 

332 
from f[OF this] show ?thesis 

333 
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

334 
next 
53079  335 
case False 
336 
hence "even (n  1)" by simp 

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

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

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

341 
using odd_pos[OF False] by auto 

342 

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

344 
by auto 

345 
from g[OF this] show ?thesis 

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

346 
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

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

348 
} 
53079  349 
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

350 
qed 
53079  351 
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

352 
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

353 
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

354 

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

355 
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

356 

53079  357 
fix n 
358 
show "suminf ?S \<le> ?g n" 

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

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

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

362 
show "?g > suminf ?S" 

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

364 
show "?f > suminf ?S" 

365 
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

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

367 

53079  368 
theorem summable_Leibniz: 
369 
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

370 
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

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

373 
(\<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  374 
and "a 0 < 0 \<longrightarrow> 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

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

376 
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

377 
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

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

379 
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

380 
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

381 
case True 
53079  382 
hence ord: "\<And>n m. m \<le> n \<Longrightarrow> a n \<le> a m" and ge0: "\<And> n. 0 \<le> a n" 
383 
by auto 

384 
{ 

385 
fix n 

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

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

388 
} note mono = this 

389 
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

390 
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

391 
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

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

393 
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

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

395 
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

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

399 
{ 

400 
fix n 

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

402 
by auto 

403 
} note monotone = this 

404 
note leibniz = 

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

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

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

408 
using leibniz(1) by auto 

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

410 
unfolding summable_def by auto 

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

412 
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

413 
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

414 
moreover 
53079  415 
have "\<And>a b :: real. \<bar> a   b\<bar> = \<bar>a  b\<bar>" 
416 
unfolding minus_diff_minus by auto 

41970  417 

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

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

421 

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

422 
have ?pos using `0 \<le> ?a 0` by auto 
53079  423 
moreover have ?neg 
424 
using leibniz(2,4) 

425 
unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le 

426 
by auto 

427 
moreover have ?f and ?g 

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

429 
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

430 
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

431 
qed 
54576  432 
then show ?summable and ?pos and ?neg and ?f and ?g 
54573  433 
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

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

435 

29164  436 
subsection {* TermbyTerm Differentiability of Power Series *} 
23043  437 

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

438 
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

439 
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

440 

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

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

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

444 

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

446 
"(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

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

448 

15229  449 
lemma diffs_equiv: 
41970  450 
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

451 
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

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

455 

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

456 
lemma lemma_termdiff1: 
31017  457 
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

458 
"(\<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

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

461 

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

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

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

465 

15229  466 
lemma lemma_termdiff2: 
31017  467 
fixes h :: "'a :: {field}" 
53079  468 
assumes h: "h \<noteq> 0" 
469 
shows 

470 
"((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

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

474 
apply (simp add: right_diff_distrib diff_divide_distrib h) 

475 
apply (simp add: mult_assoc [symmetric]) 

476 
apply (cases "n", simp) 

477 
apply (simp add: lemma_realpow_diff_sumr2 h 

478 
right_diff_distrib [symmetric] mult_assoc 

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

479 
del: power_Suc setsum_lessThan_Suc of_nat_Suc) 
53079  480 
apply (subst lemma_realpow_rev_sumr) 
481 
apply (subst sumr_diff_mult_const2) 

482 
apply simp 

483 
apply (simp only: lemma_termdiff1 setsum_right_distrib) 

484 
apply (rule setsum_cong [OF refl]) 

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

485 
apply (simp add: less_iff_Suc_add) 
53079  486 
apply (clarify) 
487 
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

488 
del: setsum_lessThan_Suc power_Suc) 
53079  489 
apply (subst mult_assoc [symmetric], subst power_add [symmetric]) 
490 
apply (simp add: mult_ac) 

491 
done 

20860  492 

493 
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

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

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

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

500 
apply (simp add: mult_right_mono K) 

501 
done 

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

502 

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

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

508 
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

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

511 
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

512 
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

513 
(z + h) ^ q * z ^ (n  2  q)) * norm h" 
54573  514 
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

515 
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

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

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

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

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

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

524 
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

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

527 
order_trans [OF norm_setsum] 
20860  528 
real_setsum_nat_ivl_bounded2 
529 
mult_nonneg_nonneg 

47489  530 
of_nat_0_le_iff 
20860  531 
zero_le_power K) 
532 
apply (rule le_Kn, simp) 

533 
done 

534 
qed 

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

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

538 
qed 

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

539 

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

547 
proof (rule real_tendsto_sandwich) 

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

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

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

553 
by (rule tendsto_const) 

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

555 
by (intro tendsto_intros) 

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

557 
by simp 

20860  558 
qed 
559 
qed 

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

560 

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

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

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

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

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

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

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

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

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

578 
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

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

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

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

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

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

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

589 

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

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

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

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

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

598 
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

599 
from norm_ge_zero r1 have r: "0 < r" 
20860  600 
by (rule order_le_less_trans) 
601 
hence r_neq_0: "r \<noteq> 0" by simp 

602 
show ?thesis 

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

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

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

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

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

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

609 
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

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

611 
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

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

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

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

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

619 
done 
41970  620 
finally have "summable 
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) * r ^ (n  Suc 0))" 
20860  622 
by (rule diffs_equiv [THEN sums_summable]) 
623 
also have 

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

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

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

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

628 
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

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

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

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

632 
done 
53079  633 
finally 
634 
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

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

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

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

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

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

642 
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

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

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

645 
apply (rule mult_left_mono [OF _ norm_ge_zero]) 
54575  646 
apply (simp add: mult_assoc [symmetric]) 
647 
apply (metis h lemma_termdiff3 less_eq_real_def r1 xh) 

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

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

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

651 

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

657 
and 4: "norm x < norm K" 

20860  658 
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

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

663 
proof (rule LIM_equal2) 

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

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

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

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

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

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

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

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

675 
then have "((\<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  c n * x ^ n) / h  of_nat n * c n * x ^ (n  Suc 0))" 

677 
by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums) 

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

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

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

20860  684 
qed 
685 
qed 

686 

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

687 

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

688 
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

689 

53079  690 
lemma DERIV_series': 
691 
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

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

695 
and "summable L" 

696 
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

697 
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

698 
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

699 
proof (rule LIM_I) 
53079  700 
fix r :: real 
701 
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

702 

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

704 
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

705 

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

707 
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

708 

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

709 
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

710 
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

711 
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

712 

53079  713 
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

714 

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

715 
let ?r = "r / (3 * real ?N)" 
56541  716 
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

717 

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

718 
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

719 
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

720 

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

721 
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

722 
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

723 
show "\<forall>x \<in> (?s ` {..< ?N }). 0 < x" 
53079  724 
proof 
725 
fix x 

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

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

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

732 
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

733 
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

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

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

736 

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

737 
def S \<equiv> "min (min (x0  a) (b  x0)) S'" 
53079  738 
hence "0 < S" and S_a: "S \<le> x0  a" and S_b: "S \<le> b  x0" 
739 
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

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

741 

53079  742 
{ 
743 
fix x 

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

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

746 
using S_a S_b by auto 

41970  747 

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

748 
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

749 
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

750 
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

751 
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

752 
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

753 
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

754 
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

755 

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

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

760 
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

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

762 
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

763 
then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))" 
56213  764 
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

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

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

768 
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

769 
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

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

772 
assume "n \<in> {..< ?N}" 
53079  773 
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

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

776 
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

777 
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

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

779 
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

780 
qed auto 
53079  781 
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

782 

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

783 
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

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

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

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

791 
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

792 
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

793 
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

794 

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

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

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

799 
using suminf_divide[OF diff_smbl, symmetric] by auto 

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

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

802 
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

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

806 
using abs_triangle_ineq4 by auto 

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

53079  810 
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

811 
by auto 
53079  812 
} 
813 
thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x  0) < s \<longrightarrow> 

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

815 
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

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

817 

53079  818 
lemma DERIV_power_series': 
819 
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

820 
assumes converges: "\<And> x. x \<in> {R <..< R} \<Longrightarrow> summable (\<lambda> n. f n * real (Suc n) * x^n)" 
53079  821 
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

822 
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

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

824 
proof  
53079  825 
{ 
826 
fix R' 

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

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

829 
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

830 
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

831 
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

832 
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

833 
proof  
53079  834 
have "(R' + R) / 2 < R" and "0 < (R' + R) / 2" 
835 
using `0 < R'` `0 < R` `R' < R` by auto 

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

837 
using `R' < R` by auto 

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

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

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

841 
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

842 
qed 
53079  843 
{ 
844 
fix n x y 

845 
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

846 
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

847 
proof  
53079  848 
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

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

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

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

854 
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  855 
by (rule setsum_abs) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

856 
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

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

859 
assume "p \<in> {..<Suc n}" 
53079  860 
hence "p \<le> n" by auto 
861 
{ 

862 
fix n 

863 
fix x :: real 

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

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

865 
hence "\<bar>x\<bar> \<le> R'" by auto 
53079  866 
hence "\<bar>x^n\<bar> \<le> R'^n" 
867 
unfolding power_abs by (rule power_mono, auto) 

868 
} 

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

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

871 
unfolding abs_mult by auto 

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

873 
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

874 
qed 
53079  875 
also have "\<dots> = real (Suc n) * R' ^ n" 
876 
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

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

880 
unfolding abs_mult[symmetric] by auto 

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

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

884 
finally show ?thesis . 
53079  885 
qed 
886 
} 

887 
{ 

888 
fix n 

889 
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

890 
by (auto intro!: derivative_eq_intros simp del: power_Suc simp: real_of_nat_def) 
53079  891 
} 
892 
{ 

893 
fix x 

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

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

896 
using assms `R' < R` by auto 

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

897 
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

898 
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

899 
fix n 
53079  900 
have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)" 
901 
by (rule mult_left_mono) auto 

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

902 
show "norm (f n * x ^ n) \<le> norm (f n * real (Suc n) * x ^ n)" 
53079  903 
unfolding real_norm_def abs_mult 
904 
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

905 
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

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

909 
show "summable (?f' x0)" 

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

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

912 
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

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

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

915 
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

916 
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

917 
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

918 
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

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

920 
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

921 
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

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

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

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

926 
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

927 
qed 
53079  928 
hence "0 < ?R" "?R < R" " ?R < x0" and "x0 < ?R" 
929 
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

930 
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

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

932 
qed 
29695  933 

53079  934 

29164  935 
subsection {* Exponential Function *} 
23043  936 

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

23043  939 

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

940 
lemma summable_exp_generic: 
31017  941 
fixes x :: "'a::{real_normed_algebra_1,banach}" 
25062  942 
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

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

944 
proof  
25062  945 
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

946 
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

947 
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

948 
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

949 
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

950 
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

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

952 
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

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

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

955 
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

956 
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

957 
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

958 
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

959 
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

960 
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

961 
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

962 
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

963 
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

964 
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

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

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

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

969 

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

970 
lemma summable_norm_exp: 
31017  971 
fixes x :: "'a::{real_normed_algebra_1,banach}" 
25062  972 
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

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

975 
by (rule summable_exp_generic) 
53079  976 
fix n 
977 
show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)" 

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

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

980 

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

23043  983 

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

987 

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

991 
del: mult_Suc of_nat_Suc) 

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

992 

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

993 
lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))" 
53079  994 
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

995 

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

996 
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" 
53079  997 
unfolding exp_def scaleR_conv_of_real 
998 
apply (rule DERIV_cong) 

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

1000 
apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs) 

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

1002 
apply (simp del: of_real_add) 

1003 
done 

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

1004 

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

1005 
declare DERIV_exp[THEN DERIV_chain2, derivative_intros] 
51527  1006 

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

1009 

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

1011 
by (rule isCont_o2 [OF _ isCont_exp]) 

1012 

1013 
lemma tendsto_exp [tendsto_intros]: 

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

1015 
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

1016 

53079  1017 
lemma continuous_exp [continuous_intros]: 
1018 
"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

1019 
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

1020 

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

1021 
lemma continuous_on_exp [continuous_intros]: 
53079  1022 
"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

1023 
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

1024 

53079  1025 

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

1027 

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

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

1032 
have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)" 
56213  1033 
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

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

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

1036 

23278  1037 
lemma exp_zero [simp]: "exp 0 = 1" 
53079  1038 
unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero) 
23278  1039 

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

1040 
lemma exp_series_add: 
31017  1041 
fixes x y :: "'a::{real_field}" 
25062  1042 
defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)" 
56213  1043 
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

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

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

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

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

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

1049 
case (Suc n) 
25062  1050 
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

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

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

1054 

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

1056 
by (simp only: times_S) 
56213  1057 
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

1058 
by (simp only: Suc) 
56213  1059 
also have "\<dots> = x * (\<Sum>i\<le>n. S x i * S y (ni)) 
1060 
+ 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

1061 
by (rule distrib_right) 
56213  1062 
also have "\<dots> = (\<Sum>i\<le>n. (x * S x i) * S y (ni)) 
1063 
+ (\<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

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

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

1070 
by (subst setsum_atMost_Suc_shift) simp 

1071 
also have "(\<Sum>i\<le>n. real (Suc ni) *\<^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 
by simp 

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

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

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

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

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

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

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

1085 

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

1086 
lemma exp_add: "exp (x + y) = exp x * exp y" 
53079  1087 
unfolding exp_def 
1088 
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

1089 

29170  1090 
lemma mult_exp_exp: "exp x * exp y = exp (x + y)" 
53079  1091 
by (rule exp_add [symmetric]) 
29170  1092 

23241  1093 
lemma exp_of_real: "exp (of_real x) = of_real (exp x)" 
53079  1094 
unfolding exp_def 
1095 
apply (subst suminf_of_real) 

1096 
apply (rule summable_exp_generic) 

1097 
apply (simp add: scaleR_conv_of_real) 

1098 
done 

23241  1099 

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

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

1103 
also assume "exp x = 0" 

1104 
finally show "False" by simp 

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

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

1106 

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

1109 

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

1111 
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

1112 

29167  1113 

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

1115 

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

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

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

1120 
proof  

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

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

1123 
qed 

1124 

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

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

1127 

29170  1128 
lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0" 
53079  1129 
by (simp add: not_less) 
29170  1130 

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

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

1133 

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

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

1136 

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

1137 
lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" 
53079  1138 
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

1139 

29170  1140 
text {* Strict monotonicity of exponential. *} 
1141 

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

1144 
using order_le_imp_less_or_eq [OF assms] 

1145 
proof 

1146 
assume "0 < x" 

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

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

56213  1150 
apply (rule setsum_le_suminf [OF summable_exp]) 
54575  1151 
using `0 < x` 
1152 
apply (auto simp add: zero_le_mult_iff) 

1153 
done 

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

1155 
by (simp add: exp_def) 

1156 
next 

1157 
assume "0 = x" 

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

1159 
by auto 

1160 
qed 

29170  1161 

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

1163 
proof  

1164 
assume x: "0 < x" 

1165 
hence "1 < 1 + x" by simp 

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

1167 
by (simp add: exp_ge_add_one_self_aux) 

1168 
finally show ?thesis . 

1169 
qed 

1170 

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

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

1172 
fixes x y :: real 
53079  1173 
assumes "x < y" 
1174 
shows "exp x < exp y" 

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

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

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

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

1178 
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

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

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

1181 

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

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

1185 

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

1188 

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

1191 

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

1194 

29170  1195 
text {* Comparisons of @{term "exp x"} with one. *} 
1196 

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

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

1199 

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

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

1202 

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

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

1205 

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

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

1208 

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

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

1211 

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

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

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

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

1218 
qed (simp_all add: le_diff_eq) 

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

1219 

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

44755 