author  paulson <lp15@cam.ac.uk> 
Tue, 21 Apr 2015 17:19:00 +0100  
changeset 60141  833adf7db7d8 
parent 60036  218fcc645d22 
child 60150  bd773c47ad0b 
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 

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

8 

15131  9 
theory Transcendental 
59669
de7792ea4090
renaming HOL/Fact.thy > Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

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

12 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

13 
lemma of_real_fact [simp]: "of_real (fact n) = fact n" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

14 
by (metis of_nat_fact of_real_of_nat_eq) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

15 

b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

16 
lemma real_fact_nat [simp]: "real (fact n :: nat) = fact n" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

17 
by (simp add: real_of_nat_def) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

18 

59731  19 
lemma real_fact_int [simp]: "real (fact n :: int) = fact n" 
20 
by (metis of_int_of_nat_eq of_nat_fact real_of_int_def) 

21 

57025  22 
lemma root_test_convergence: 
23 
fixes f :: "nat \<Rightarrow> 'a::banach" 

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

25 
assumes "x < 1" 

26 
shows "summable f" 

27 
proof  

28 
have "0 \<le> x" 

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

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

31 
by (metis dense) 

32 
from f `x < z` 

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

34 
by (rule order_tendstoD) 

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

36 
using eventually_ge_at_top 

37 
proof eventually_elim 

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

39 
from power_strict_mono[OF less, of n] n 

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

41 
by simp 

42 
qed 

43 
then show "summable f" 

44 
unfolding eventually_sequentially 

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

46 
qed 

47 

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

49 

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

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

52 
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

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

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

55 
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

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

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

58 

15229  59 
lemma lemma_realpow_diff_sumr2: 
53079  60 
fixes y :: "'a::{comm_ring,monoid_mult}" 
61 
shows 

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

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

63 
(x  y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n  p))" 
54573  64 
proof (induct n) 
65 
case (Suc n) 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

66 
have "x ^ Suc (Suc n)  y ^ Suc (Suc n) = x * (x * x^n)  y * (y * y ^ n)" 
54573  67 
by simp 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

68 
also have "... = y * (x ^ (Suc n)  y ^ (Suc n)) + (x  y) * (x * x^n)" 
54573  69 
by (simp add: algebra_simps) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

70 
also have "... = y * ((x  y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n  p))) + (x  y) * (x * x^n)" 
54573  71 
by (simp only: Suc) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

72 
also have "... = (x  y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n  p))) + (x  y) * (x * x^n)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

73 
by (simp only: mult.left_commute) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

74 
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

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

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

78 

55832  79 
corollary power_diff_sumr2: {* @{text COMPLEX_POLYFUN} in HOL Light *} 
55734  80 
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

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

84 

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

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

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

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

89 

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

90 
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

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> x^n  1 = (x  1) * (\<Sum>i<n. (x^i))" 
59669
de7792ea4090
renaming HOL/Fact.thy > Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

93 
using lemma_realpow_diff_sumr2 [of x _ 1] 
55719
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^(n  Suc i))" 
59669
de7792ea4090
renaming HOL/Fact.thy > Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

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

100 
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

101 

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

102 
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

103 
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

104 
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

105 
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

106 

60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

107 
lemma powser_zero: 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

108 
fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra_1" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

109 
shows "(\<Sum>n. f n * 0 ^ n) = f 0" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

110 
proof  
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

111 
have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

112 
by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

113 
thus ?thesis unfolding One_nat_def by simp 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

114 
qed 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

115 

833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

116 
lemma powser_sums_zero: 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

117 
fixes a :: "nat \<Rightarrow> 'a::real_normed_div_algebra" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

118 
shows "(\<lambda>n. a n * 0^n) sums a 0" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

119 
using sums_finite [of "{0}" "\<lambda>n. a n * 0 ^ n"] 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

120 
by simp 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

121 

833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

122 
text{*Power series has a circle or radius of convergence: if it sums for @{term 
53079  123 
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

124 

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

125 
lemma powser_insidea: 
53599  126 
fixes x z :: "'a::real_normed_div_algebra" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

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

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

131 
from 2 have x_neq_0: "x \<noteq> 0" by clarsimp 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

133 
by (rule summable_LIMSEQ_zero) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

135 
by (rule convergentI) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

136 
hence "Cauchy (\<lambda>n. f n * x^n)" 
44726  137 
by (rule convergent_Cauchy) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

139 
by (rule Cauchy_Bseq) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

140 
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

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

142 
have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le> 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

144 
proof (intro exI allI impI) 
53079  145 
fix n::nat 
146 
assume "0 \<le> n" 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

147 
have "norm (norm (f n * z ^ n)) * norm (x^n) = 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

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

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

151 
by (simp only: mult_right_mono 4 norm_ge_zero) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

152 
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

153 
by (simp add: x_neq_0) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

154 
also have "\<dots> = K * norm (z ^ n) * inverse (norm (x^n)) * norm (x^n)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

155 
by (simp only: mult.assoc) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

156 
finally show "norm (norm (f n * z ^ n)) \<le> 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

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

159 
qed 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

160 
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

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

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

163 
using x_neq_0 
53599  164 
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

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

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

167 
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

168 
by (rule summable_mult) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

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

171 
by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

172 
power_inverse norm_power mult.assoc) 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

174 
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

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

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

177 

15229  178 
lemma powser_inside: 
53599  179 
fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}" 
53079  180 
shows 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

181 
"summable (\<lambda>n. f n * (x^n)) \<Longrightarrow> norm z < norm x \<Longrightarrow> 
53079  182 
summable (\<lambda>n. f n * (z ^ n))" 
183 
by (rule powser_insidea [THEN summable_norm_cancel]) 

184 

60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

185 
lemma powser_times_n_limit_0: 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

186 
fixes x :: "'a::{real_normed_div_algebra,banach}" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

187 
assumes "norm x < 1" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

188 
shows "(\<lambda>n. of_nat n * x ^ n) > 0" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

189 
proof  
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

190 
have "norm x / (1  norm x) \<ge> 0" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

191 
using assms 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

192 
by (auto simp: divide_simps) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

193 
moreover obtain N where N: "norm x / (1  norm x) < of_int N" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

194 
using ex_le_of_int 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

195 
by (meson ex_less_of_int) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

196 
ultimately have N0: "N>0" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

197 
by auto 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

198 
then have *: "real (N + 1) * norm x / real N < 1" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

199 
using N assms 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

200 
by (auto simp: field_simps) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

201 
{ fix n::nat 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

202 
assume "N \<le> int n" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

203 
then have "real N * real_of_nat (Suc n) \<le> real_of_nat n * real (1 + N)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

204 
by (simp add: algebra_simps) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

205 
then have "(real N * real_of_nat (Suc n)) * (norm x * norm (x ^ n)) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

206 
\<le> (real_of_nat n * real (1 + N)) * (norm x * norm (x ^ n))" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

207 
using N0 mult_mono by fastforce 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

208 
then have "real N * (norm x * (real_of_nat (Suc n) * norm (x ^ n))) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

209 
\<le> real_of_nat n * (norm x * (real (1 + N) * norm (x ^ n)))" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

210 
by (simp add: algebra_simps) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

211 
} note ** = this 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

212 
show ?thesis using * 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

213 
apply (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

214 
apply (simp add: N0 norm_mult nat_le_iff field_simps power_Suc ** 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

215 
del: of_nat_Suc real_of_int_add) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

216 
done 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

217 
qed 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

218 

833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

219 
corollary lim_n_over_pown: 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

220 
fixes x :: "'a::{real_normed_field,banach}" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

221 
shows "1 < norm x \<Longrightarrow> ((\<lambda>n. of_nat n / x^n) > 0) sequentially" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

222 
using powser_times_n_limit_0 [of "inverse x"] 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

223 
by (simp add: norm_divide divide_simps) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

224 

53079  225 
lemma sum_split_even_odd: 
226 
fixes f :: "nat \<Rightarrow> real" 

227 
shows 

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

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

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

230 
proof (induct n) 
53079  231 
case 0 
232 
then show ?case by simp 

233 
next 

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

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

235 
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

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

237 
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

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

240 
finally show ?case . 
53079  241 
qed 
242 

243 
lemma sums_if': 

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

245 
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

246 
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

247 
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

248 
proof (rule LIMSEQ_I) 
53079  249 
fix r :: real 
250 
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

251 
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

252 
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

253 

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

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

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

258 
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

259 
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

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

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

264 
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

265 
proof (cases "even m") 
53079  266 
case True 
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset

267 
then show ?thesis by (auto simp add: even_two_times_div_two) 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

268 
next 
53079  269 
case False 
58834  270 
then have eq: "Suc (2 * (m div 2)) = m" 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

271 
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

272 
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

273 
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

274 
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

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

276 
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

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

278 
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

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

280 

53079  281 
lemma sums_if: 
282 
fixes g :: "nat \<Rightarrow> real" 

283 
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

284 
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

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

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

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

290 
by (cases B) auto 

291 
} note if_sum = this 

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

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

41970  294 
{ 
41550  295 
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

296 

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

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

299 
have "(\<lambda> n. if even n then f (n div 2) else 0) sums y" 
57418  300 
by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum.reindex if_eq sums_def cong del: if_cong) 
53079  301 
} 
302 
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

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

304 

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

305 
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

306 

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

307 
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

308 
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

309 
assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a > 0" 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57514
diff
changeset

310 
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> 
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57514
diff
changeset

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

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

314 
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

315 

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

318 
fix n 

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

320 
qed 

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

322 
proof 

323 
fix n 

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

325 
unfolding One_nat_def by auto 

326 
qed 

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

328 
proof 

329 
fix n 

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

331 
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

332 
qed 
53079  333 
show "(\<lambda>n. ?f n  ?g n) > 0" unfolding fg_diff 
334 
proof (rule LIMSEQ_I) 

335 
fix r :: real 

336 
assume "0 < r" 

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

338 
by auto 

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

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

341 
qed 

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

343 

53079  344 
lemma summable_Leibniz': 
345 
fixes a :: "nat \<Rightarrow> real" 

346 
assumes a_zero: "a > 0" 

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

348 
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

349 
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

350 
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

351 
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

352 
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

353 
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

354 
proof  
53079  355 
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

356 
let ?P = "\<lambda>n. \<Sum>i<n. ?S i" 
53079  357 
let ?f = "\<lambda>n. ?P (2 * n)" 
358 
let ?g = "\<lambda>n. ?P (2 * n + 1)" 

359 
obtain l :: real 

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

361 
and "?f > l" 

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

363 
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

364 
using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast 
41970  365 

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

366 
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

367 
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

368 
proof (rule LIMSEQ_I) 
53079  369 
fix r :: real 
370 
assume "0 < r" 

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

372 
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

373 

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

375 
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

376 

53079  377 
{ 
378 
fix n :: nat 

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

380 
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

381 
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

382 
proof (cases "even n") 
53079  383 
case True 
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset

384 
then have n_eq: "2 * (n div 2) = n" by (simp add: even_two_times_div_two) 
53079  385 
with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no" 
386 
by auto 

387 
from f[OF this] show ?thesis 

388 
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

389 
next 
53079  390 
case False 
391 
hence "even (n  1)" by simp 

58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset

392 
then have n_eq: "2 * ((n  1) div 2) = n  1" 
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset

393 
by (simp add: even_two_times_div_two) 
53079  394 
hence range_eq: "n  1 + 1 = n" 
395 
using odd_pos[OF False] by auto 

396 

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

398 
by auto 

399 
from g[OF this] show ?thesis 

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

400 
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

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

402 
} 
53079  403 
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

404 
qed 
53079  405 
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

406 
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

407 
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

408 

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

409 
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

410 

53079  411 
fix n 
412 
show "suminf ?S \<le> ?g n" 

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

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

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

416 
show "?g > suminf ?S" 

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

418 
show "?f > suminf ?S" 

419 
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

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

421 

53079  422 
theorem summable_Leibniz: 
423 
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

424 
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

425 
shows "summable (\<lambda> n. (1)^n * a n)" (is "?summable") 
53079  426 
and "0 < a 0 \<longrightarrow> 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57514
diff
changeset

427 
(\<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  428 
and "a 0 < 0 \<longrightarrow> 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57514
diff
changeset

429 
(\<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") 
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57514
diff
changeset

430 
and "(\<lambda>n. \<Sum>i<2*n. ( 1)^i*a i) > (\<Sum>i. ( 1)^i*a i)" (is "?f") 
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57514
diff
changeset

431 
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

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

433 
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

434 
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

435 
case True 
53079  436 
hence ord: "\<And>n m. m \<le> n \<Longrightarrow> a n \<le> a m" and ge0: "\<And> n. 0 \<le> a n" 
437 
by auto 

438 
{ 

439 
fix n 

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

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

442 
} note mono = this 

443 
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

444 
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

445 
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

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

447 
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

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

449 
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

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

453 
{ 

454 
fix n 

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

456 
by auto 

457 
} note monotone = this 

458 
note leibniz = 

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

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

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

462 
using leibniz(1) by auto 

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

464 
unfolding summable_def by auto 

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

466 
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

467 
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

468 
moreover 
53079  469 
have "\<And>a b :: real. \<bar> a   b\<bar> = \<bar>a  b\<bar>" 
470 
unfolding minus_diff_minus by auto 

41970  471 

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

472 
from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus] 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57514
diff
changeset

473 
have move_minus: "(\<Sum>n.  (( 1) ^ n * a n)) =  (\<Sum>n. ( 1) ^ n * a n)" 
53079  474 
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

475 

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

476 
have ?pos using `0 \<le> ?a 0` by auto 
53079  477 
moreover have ?neg 
478 
using leibniz(2,4) 

479 
unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le 

480 
by auto 

481 
moreover have ?f and ?g 

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

483 
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

484 
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

485 
qed 
59669
de7792ea4090
renaming HOL/Fact.thy > Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59658
diff
changeset

486 
then show ?summable and ?pos and ?neg and ?f and ?g 
54573  487 
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

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

489 

29164  490 
subsection {* TermbyTerm Differentiability of Power Series *} 
23043  491 

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

492 
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

493 
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

494 

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

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

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

498 

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

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

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

502 

15229  503 
lemma diffs_equiv: 
41970  504 
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

505 
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

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

509 

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

510 
lemma lemma_termdiff1: 
31017  511 
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

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

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

515 

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

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

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

519 

15229  520 
lemma lemma_termdiff2: 
31017  521 
fixes h :: "'a :: {field}" 
53079  522 
assumes h: "h \<noteq> 0" 
523 
shows 

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

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

528 
apply (simp add: right_diff_distrib diff_divide_distrib h) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

529 
apply (simp add: mult.assoc [symmetric]) 
53079  530 
apply (cases "n", simp) 
531 
apply (simp add: lemma_realpow_diff_sumr2 h 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

532 
right_diff_distrib [symmetric] mult.assoc 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

533 
del: power_Suc setsum_lessThan_Suc of_nat_Suc) 
53079  534 
apply (subst lemma_realpow_rev_sumr) 
535 
apply (subst sumr_diff_mult_const2) 

536 
apply simp 

537 
apply (simp only: lemma_termdiff1 setsum_right_distrib) 

57418  538 
apply (rule setsum.cong [OF refl]) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset

539 
apply (simp add: less_iff_Suc_add) 
53079  540 
apply (clarify) 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

541 
apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 ac_simps 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

542 
del: setsum_lessThan_Suc power_Suc) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

543 
apply (subst mult.assoc [symmetric], subst power_add [symmetric]) 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

544 
apply (simp add: ac_simps) 
53079  545 
done 
20860  546 

547 
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

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

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

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

554 
apply (simp add: mult_right_mono K) 

555 
done 

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

556 

15229  557 
lemma lemma_termdiff3: 
31017  558 
fixes h z :: "'a::{real_normed_field}" 
20860  559 
assumes 1: "h \<noteq> 0" 
53079  560 
and 2: "norm z \<le> K" 
561 
and 3: "norm (z + h) \<le> K" 

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

562 
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

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

565 
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

566 
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

567 
(z + h) ^ q * z ^ (n  2  q)) * norm h" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

568 
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

569 
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

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

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

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

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

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

578 
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

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

581 
order_trans [OF norm_setsum] 
20860  582 
real_setsum_nat_ivl_bounded2 
583 
mult_nonneg_nonneg 

47489  584 
of_nat_0_le_iff 
20860  585 
zero_le_power K) 
586 
apply (rule le_Kn, simp) 

587 
done 

588 
qed 

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

589 
also have "\<dots> = of_nat n * of_nat (n  Suc 0) * K ^ (n  2) * norm h" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

590 
by (simp only: mult.assoc) 
20860  591 
finally show ?thesis . 
592 
qed 

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

593 

20860  594 
lemma lemma_termdiff4: 
56167  595 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
20860  596 
assumes k: "0 < (k::real)" 
53079  597 
and le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h" 
20860  598 
shows "f  0 > 0" 
56167  599 
proof (rule tendsto_norm_zero_cancel) 
600 
show "(\<lambda>h. norm (f h))  0 > 0" 

601 
proof (rule real_tendsto_sandwich) 

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

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

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

607 
by (rule tendsto_const) 

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

609 
by (intro tendsto_intros) 

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

611 
by simp 

20860  612 
qed 
613 
qed 

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

614 

15229  615 
lemma lemma_termdiff5: 
56167  616 
fixes g :: "'a::real_normed_vector \<Rightarrow> nat \<Rightarrow> 'b::banach" 
20860  617 
assumes k: "0 < (k::real)" 
618 
assumes f: "summable f" 

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

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

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

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

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

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

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

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

632 
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

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

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

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

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

640 

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

641 

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

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

643 

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

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

646 
assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)" 
53079  647 
and 2: "norm x < norm K" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

648 
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

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

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

652 
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

653 
from norm_ge_zero r1 have r: "0 < r" 
20860  654 
by (rule order_le_less_trans) 
655 
hence r_neq_0: "r \<noteq> 0" by simp 

656 
show ?thesis 

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

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

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

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

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

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

663 
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

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

665 
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

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

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

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

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

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

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

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

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

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

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

682 
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

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

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

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

686 
done 
53079  687 
finally 
688 
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

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

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

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

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

694 
with norm_triangle_ineq have xh: "norm (x + h) < r" 
20860  695 
by (rule order_le_less_trans) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

697 
\<le> norm (c n) * of_nat n * of_nat (n  Suc 0) * r ^ (n  2) * norm h" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

698 
apply (simp only: norm_mult mult.assoc) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

699 
apply (rule mult_left_mono [OF _ norm_ge_zero]) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

700 
apply (simp add: mult.assoc [symmetric]) 
54575  701 
apply (metis h lemma_termdiff3 less_eq_real_def r1 xh) 
20860  702 
done 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

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

705 

20860  706 
lemma termdiffs: 
31017  707 
fixes K x :: "'a::{real_normed_field,banach}" 
20860  708 
assumes 1: "summable (\<lambda>n. c n * K ^ n)" 
54575  709 
and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)" 
710 
and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)" 

711 
and 4: "norm x < norm K" 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

712 
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

713 
unfolding DERIV_def 
29163  714 
proof (rule LIM_zero_cancel) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

715 
show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n)  suminf (\<lambda>n. c n * x^n)) / h 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

716 
 suminf (\<lambda>n. diffs c n * x^n))  0 > 0" 
20860  717 
proof (rule LIM_equal2) 
29163  718 
show "0 < norm K  norm x" using 4 by (simp add: less_diff_eq) 
20860  719 
next 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

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

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

724 
by (rule norm_triangle_ineq [THEN order_le_less_trans]) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

725 
have "summable (\<lambda>n. c n * x^n)" 
56167  726 
and "summable (\<lambda>n. c n * (x + h) ^ n)" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

727 
and "summable (\<lambda>n. diffs c n * x^n)" 
56167  728 
using 1 2 4 5 by (auto elim: powser_inside) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

729 
then have "((\<Sum>n. c n * (x + h) ^ n)  (\<Sum>n. c n * x^n)) / h  (\<Sum>n. diffs c n * x^n) = 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

730 
(\<Sum>n. (c n * (x + h) ^ n  c n * x^n) / h  of_nat n * c n * x ^ (n  Suc 0))" 
56167  731 
by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

732 
then show "((\<Sum>n. c n * (x + h) ^ n)  (\<Sum>n. c n * x^n)) / h  (\<Sum>n. diffs c n * x^n) = 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

733 
(\<Sum>n. c n * (((x + h) ^ n  x^n) / h  of_nat n * x ^ (n  Suc 0)))" 
54575  734 
by (simp add: algebra_simps) 
20860  735 
next 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

736 
show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n  x^n) / h  of_nat n * x ^ (n  Suc 0)))  0 > 0" 
53079  737 
by (rule termdiffs_aux [OF 3 4]) 
20860  738 
qed 
739 
qed 

740 

60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

741 
subsection {* The Derivative of a Power Series Has the Same Radius of Convergence *} 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

742 

833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

743 
lemma termdiff_converges: 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

744 
fixes x :: "'a::{real_normed_field,banach}" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

745 
assumes K: "norm x < K" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

746 
and sm: "\<And>x. norm x < K \<Longrightarrow> summable(\<lambda>n. c n * x ^ n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

747 
shows "summable (\<lambda>n. diffs c n * x ^ n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

748 
proof (cases "x = 0") 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

749 
case True then show ?thesis 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

750 
using powser_sums_zero sums_summable by auto 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

751 
next 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

752 
case False 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

753 
then have "K>0" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

754 
using K less_trans zero_less_norm_iff by blast 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

755 
then obtain r::real where r: "norm x < norm r" "norm r < K" "r>0" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

756 
using K False 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

757 
by (auto simp: abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

758 
have "(\<lambda>n. of_nat n * (x / of_real r) ^ n) > 0" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

759 
using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

760 
then obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> real_of_nat n * norm x ^ n < r ^ n" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

761 
using r unfolding LIMSEQ_iff 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

762 
apply (drule_tac x=1 in spec) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

763 
apply (auto simp: norm_divide norm_mult norm_power field_simps) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

764 
done 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

765 
have "summable (\<lambda>n. (of_nat n * c n) * x ^ n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

766 
apply (rule summable_comparison_test' [of "\<lambda>n. norm(c n * (of_real r) ^ n)" N]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

767 
apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

768 
using N r norm_of_real [of "r+K", where 'a = 'a] 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

769 
apply (auto simp add: norm_divide norm_mult norm_power ) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

770 
using less_eq_real_def by fastforce 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

771 
then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ Suc n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

772 
using summable_iff_shift [of "\<lambda>n. of_nat n * c n * x ^ n" 1] 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

773 
by simp 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

774 
then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

775 
using False summable_mult2 [of "\<lambda>n. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"] 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

776 
by (simp add: mult.assoc) (auto simp: power_Suc mult_ac) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

777 
then show ?thesis 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

778 
by (simp add: diffs_def) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

779 
qed 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

780 

833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

781 
lemma termdiff_converges_all: 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

782 
fixes x :: "'a::{real_normed_field,banach}" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

783 
assumes "\<And>x. summable (\<lambda>n. c n * x^n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

784 
shows "summable (\<lambda>n. diffs c n * x^n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

785 
apply (rule termdiff_converges [where K = "1 + norm x"]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

786 
using assms 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

787 
apply (auto simp: ) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

788 
done 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

789 

833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

790 
lemma termdiffs_strong: 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

791 
fixes K x :: "'a::{real_normed_field,banach}" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

792 
assumes sm: "summable (\<lambda>n. c n * K ^ n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

793 
and K: "norm x < norm K" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

794 
shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. diffs c n * x^n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

795 
proof  
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

796 
have [simp]: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

797 
using K 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

798 
apply (auto simp: norm_divide) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

799 
apply (rule le_less_trans [of _ "of_real (norm K) + of_real (norm x)"]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

800 
apply (auto simp: mult_2_right norm_triangle_mono) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

801 
done 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

802 
have "summable (\<lambda>n. c n * (of_real (norm x + norm K) / 2) ^ n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

803 
apply (rule summable_norm_cancel [OF powser_insidea [OF sm]]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

804 
using K 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

805 
apply (auto simp: algebra_simps) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

806 
done 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

807 
moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs c n * x ^ n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

808 
by (blast intro: sm termdiff_converges powser_inside) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

809 
moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs(diffs c) n * x ^ n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

810 
by (blast intro: sm termdiff_converges powser_inside) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

811 
ultimately show ?thesis 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

812 
apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

813 
apply (auto simp: algebra_simps) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

814 
using K 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

815 
apply (simp add: norm_divide) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

816 
apply (rule less_le_trans [of _ "of_real (norm K) + of_real (norm x)"]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

817 
apply (simp_all add: of_real_add [symmetric] del: of_real_add) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

818 
done 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

819 
qed 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

820 

833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

821 
lemma powser_limit_0: 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

822 
fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

823 
assumes s: "0 < s" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

824 
and sm: "\<And>x. norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

825 
shows "(f > a 0) (at 0)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

826 
proof  
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

827 
have "summable (\<lambda>n. a n * (of_real s / 2) ^ n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

828 
apply (rule sums_summable [where l = "f (of_real s / 2)", OF sm]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

829 
using s 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

830 
apply (auto simp: norm_divide) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

831 
done 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

832 
then have "((\<lambda>x. \<Sum>n. a n * x ^ n) has_field_derivative (\<Sum>n. diffs a n * 0 ^ n)) (at 0)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

833 
apply (rule termdiffs_strong) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

834 
using s 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

835 
apply (auto simp: norm_divide) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

836 
done 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

837 
then have "isCont (\<lambda>x. \<Sum>n. a n * x ^ n) 0" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

838 
by (blast intro: DERIV_continuous) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

839 
then have "((\<lambda>x. \<Sum>n. a n * x ^ n) > a 0) (at 0)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

840 
by (simp add: continuous_within powser_zero) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

841 
then show ?thesis 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

842 
apply (rule Lim_transform) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

843 
apply (auto simp add: LIM_eq) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

844 
apply (rule_tac x="s" in exI) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

845 
using s 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

846 
apply (auto simp: sm [THEN sums_unique]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

847 
done 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

848 
qed 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

849 

833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

850 
lemma powser_limit_0_strong: 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

851 
fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

852 
assumes s: "0 < s" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

853 
and sm: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

854 
shows "(f > a 0) (at 0)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

855 
proof  
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

856 
have *: "((\<lambda>x. if x = 0 then a 0 else f x) > a 0) (at 0)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

857 
apply (rule powser_limit_0 [OF s]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

858 
apply (case_tac "x=0") 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

859 
apply (auto simp add: powser_sums_zero sm) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

860 
done 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

861 
show ?thesis 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

862 
apply (subst LIM_equal [where g = "(\<lambda>x. if x = 0 then a 0 else f x)"]) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

863 
apply (simp_all add: *) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

864 
done 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

865 
qed 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

866 

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

867 

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

868 
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

869 

53079  870 
lemma DERIV_series': 
871 
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

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

875 
and "summable L" 

876 
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

877 
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

878 
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

879 
proof (rule LIM_I) 
53079  880 
fix r :: real 
881 
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

882 

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

884 
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

885 

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

887 
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

888 

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

889 
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

890 
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

891 
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

892 

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

894 

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

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

897 

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

898 
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

899 
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

900 

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

901 
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

902 
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

903 
show "\<forall>x \<in> (?s ` {..< ?N }). 0 < x" 
53079  904 
proof 
905 
fix x 

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

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

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

912 
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

913 
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

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

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

916 

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

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

920 
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 

53079  922 
{ 
923 
fix x 

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

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

926 
using S_a S_b by auto 

41970  927 

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

928 
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

929 
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

930 
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

931 
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

932 
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

933 
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

934 
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

935 

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

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

940 
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

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

942 
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

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

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

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

948 
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

949 
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

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

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

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

956 
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

957 
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

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

959 
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

960 
qed auto 
53079  961 
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

962 

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

963 
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

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

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

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

971 
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

972 
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

973 
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

974 

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

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

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

979 
using suminf_divide[OF diff_smbl, symmetric] by auto 

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

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

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

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

983 
apply (subst (5) add.commute) 
53079  984 
by (rule abs_triangle_ineq) 
985 
also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part" 

986 
using abs_triangle_ineq4 by auto 

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

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

991 
by auto 
53079  992 
} 
993 
thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x  0) < s \<longrightarrow> 

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

995 
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

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

997 

53079  998 
lemma DERIV_power_series': 
999 
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

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

1002 
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

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

1004 
proof  
53079  1005 
{ 
1006 
fix R' 

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

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

1009 
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

1010 
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

1011 
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

1012 
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

1013 
proof  
53079  1014 
have "(R' + R) / 2 < R" and "0 < (R' + R) / 2" 
1015 
using `0 < R'` `0 < R` `R' < R` by auto 

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

1017 
using `R' < R` by auto 

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

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

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

1021 
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

1022 
qed 
53079  1023 
{ 
1024 
fix n x y 

1025 
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

1026 
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

1027 
proof  
53079  1028 
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

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

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

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

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

1036 
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

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

1039 
assume "p \<in> {..<Suc n}" 
53079  1040 
hence "p \<le> n" by auto 
1041 
{ 

1042 
fix n 

1043 
fix x :: real 

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

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

1045 
hence "\<bar>x\<bar> \<le> R'" by auto 
53079  1046 
hence "\<bar>x^n\<bar> \<le> R'^n" 
1047 
unfolding power_abs by (rule power_mono, auto) 

1048 
} 

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

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

1051 
unfolding abs_mult by auto 

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

1053 
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

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

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

1060 
unfolding abs_mult[symmetric] by auto 

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

1061 
qed 
53079  1062 
also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x  y\<bar>" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

1063 
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

1064 
finally show ?thesis . 
53079  1065 
qed 
1066 
} 

1067 
{ 

1068 
fix n 

1069 
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

1070 
by (auto intro!: derivative_eq_intros simp del: power_Suc simp: real_of_nat_def) 
53079  1071 
} 
1072 
{ 

1073 
fix x 

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

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

1076 
using assms `R' < R` by auto 

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

1077 
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

1078 
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

1079 
fix n 
53079  1080 
have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)" 
1081 
by (rule mult_left_mono) auto 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

1085 
qed (rule powser_insidea[OF converges[OF `R' \<in> {R <..< R}`] `norm x < norm R'`]) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

1086 
from this[THEN summable_mult2[where c=x], unfolded mult.assoc, unfolded mult.commute] 
53079  1087 
show "summable (?f x)" by auto 
1088 
} 

1089 
show "summable (?f' x0)" 

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

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

1092 
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

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

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

1095 
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

1096 
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

1097 
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

1098 
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

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

1100 
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

1101 
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

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

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

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

1106 
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

1107 
qed 
53079  1108 
hence "0 < ?R" "?R < R" " ?R < x0" and "x0 < ?R" 
1109 
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

1110 
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

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

1112 
qed 
29695  1113 

53079  1114 

29164  1115 
subsection {* Exponential Function *} 
23043  1116 

58656  1117 
definition exp :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1118 
where "exp = (\<lambda>x. \<Sum>n. x^n /\<^sub>R fact n)" 
23043  1119 

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

1120 
lemma summable_exp_generic: 
31017  1121 
fixes x :: "'a::{real_normed_algebra_1,banach}" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1122 
defines S_def: "S \<equiv> \<lambda>n. x^n /\<^sub>R fact n" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

1124 
proof  
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

1126 
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

1127 
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

1128 
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

1129 
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

1130 
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

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

1132 
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

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

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

1135 
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

1136 
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

1137 
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

1138 
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

1139 
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

1140 
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

1141 
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

1142 
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

1143 
hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

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

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

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

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

1149 

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

1150 
lemma summable_norm_exp: 
31017  1151 
fixes x :: "'a::{real_normed_algebra_1,banach}" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1152 
shows "summable (\<lambda>n. norm (x^n /\<^sub>R fact n))" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

1153 
proof (rule summable_norm_comparison_test [OF exI, rule_format]) 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1154 
show "summable (\<lambda>n. norm x^n /\<^sub>R fact n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

1155 
by (rule summable_exp_generic) 
53079  1156 
fix n 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1157 
show "norm (x^n /\<^sub>R fact n) \<le> norm x^n /\<^sub>R fact n" 
35216  1158 
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

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

1160 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1161 
lemma summable_exp: 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1162 
fixes x :: "'a::{real_normed_field,banach}" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1163 
shows "summable (\<lambda>n. inverse (fact n) * x^n)" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1164 
using summable_exp_generic [where x=x] 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1165 
by (simp add: scaleR_conv_of_real nonzero_of_real_inverse) 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1166 

b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1167 
lemma exp_converges: "(\<lambda>n. x^n /\<^sub>R fact n) sums exp x" 
53079  1168 
unfolding exp_def by (rule summable_exp_generic [THEN summable_sums]) 
23043  1169 

41970  1170 
lemma exp_fdiffs: 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1171 
fixes XXX :: "'a::{real_normed_field,banach}" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1172 
shows "diffs (\<lambda>n. inverse (fact n)) = (\<lambda>n. inverse (fact n :: 'a))" 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1173 
by (simp add: diffs_def mult_ac nonzero_inverse_mult_distrib nonzero_of_real_inverse 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

1175 

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

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

1178 

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

1179 
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" 
53079  1180 
unfolding exp_def scaleR_conv_of_real 
1181 
apply (rule DERIV_cong) 

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

1183 
apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs) 

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

1185 
apply (simp del: of_real_add) 

1186 
done 

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

1187 

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

1188 
declare DERIV_exp[THEN DERIV_chain2, derivative_intros] 
51527  1189 

58656  1190 
lemma norm_exp: "norm (exp x) \<le> exp (norm x)" 
1191 
proof  

1192 
from summable_norm[OF summable_norm_exp, of x] 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

1193 
have "norm (exp x) \<le> (\<Sum>n. inverse (fact n) * norm (x^n))" 
58656  1194 
by (simp add: exp_def) 
1195 
also have "\<dots> \<le> exp (norm x)" 

1196 
using summable_exp_generic[of "norm x"] summable_norm_exp[of x] 

1197 
by (auto simp: exp_def intro!: suminf_le norm_power_ineq) 
