author  chaieb 
Fri, 30 Jan 2009 12:48:57 +0000  
changeset 29695  171146a93106 
parent 29667  53103fc8ffa3 
child 29803  c56a5571f60a 
permissions  rwrr 
12196  1 
(* Title : Transcendental.thy 
2 
Author : Jacques D. Fleuriot 

3 
Copyright : 1998,1999 University of Cambridge 

13958
c1c67582c9b5
New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
12196
diff
changeset

4 
1999,2001 University of Edinburgh 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

5 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
12196  6 
*) 
7 

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

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

9 

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

13 

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

15 

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

16 
lemma lemma_realpow_diff: 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

17 
fixes y :: "'a::recpower" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

18 
shows "p \<le> n \<Longrightarrow> y ^ (Suc n  p) = (y ^ (n  p)) * y" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

21 
hence "Suc n  p = Suc (n  p)" by (rule Suc_diff_le) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

24 

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

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

26 
fixes y :: "'a::{recpower,comm_semiring_0}" shows 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

28 
y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n  p))" 
29163  29 
by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac 
30 
del: setsum_op_ivl_Suc cong: strong_setsum_cong) 

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

31 

15229  32 
lemma lemma_realpow_diff_sumr2: 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

33 
fixes y :: "'a::{recpower,comm_ring}" shows 
15229  34 
"x ^ (Suc n)  y ^ (Suc n) = 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

35 
(x  y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n  p))" 
25153  36 
apply (induct n, simp add: power_Suc) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

37 
apply (simp add: power_Suc del: setsum_op_ivl_Suc) 
15561  38 
apply (subst setsum_op_ivl_Suc) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

40 
apply (simp add: right_distrib del: setsum_op_ivl_Suc) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

41 
apply (subst mult_left_commute [where a="x  y"]) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

42 
apply (erule subst) 
29667  43 
apply (simp add: power_Suc algebra_simps) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

45 

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

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

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

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

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

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

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

54 

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

55 
text{*Power series has a `circle` of convergence, i.e. if it sums for @{term 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

56 
x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*} 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

57 

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

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

59 
fixes x z :: "'a::{real_normed_field,banach,recpower}" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

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

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

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

64 
from 2 have x_neq_0: "x \<noteq> 0" by clarsimp 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

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

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

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

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

70 
by (simp add: Cauchy_convergent_iff) 
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

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

73 
then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

75 
have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le> 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

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

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

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

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

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

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

84 
also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

86 
also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

109 

15229  110 
lemma powser_inside: 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

111 
fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach,recpower}" shows 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

112 
"[ summable (%n. f(n) * (x ^ n)); norm z < norm x ] 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

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

115 

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

116 

29164  117 
subsection {* TermbyTerm Differentiability of Power Series *} 
23043  118 

119 
definition 

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

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

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

122 

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

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

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

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

126 

29163  127 
lemma sums_Suc_imp: 
128 
assumes f: "f 0 = 0" 

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

130 
unfolding sums_def 

131 
apply (rule LIMSEQ_imp_Suc) 

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

133 
apply (simp only: setsum_shift_bounds_Suc_ivl) 

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

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

135 

15229  136 
lemma diffs_equiv: 
137 
"summable (%n. (diffs c)(n) * (x ^ n)) ==> 

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

138 
(%n. of_nat n * c(n) * (x ^ (n  Suc 0))) sums 
15546  139 
(\<Sum>n. (diffs c)(n) * (x ^ n))" 
29163  140 
unfolding diffs_def 
141 
apply (drule summable_sums) 

142 
apply (rule sums_Suc_imp, simp_all) 

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

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

144 

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

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

146 
fixes z :: "'a :: {recpower,comm_ring}" shows 
15539  147 
"(\<Sum>p=0..<m. (((z + h) ^ (m  p)) * (z ^ p))  (z ^ m)) = 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

150 

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

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

152 
"setsum f {0..<n}  of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i  r)" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

154 

15229  155 
lemma lemma_termdiff2: 
23112
2bc882fbe51c
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents:
23097
diff
changeset

156 
fixes h :: "'a :: {recpower,field}" 
20860  157 
assumes h: "h \<noteq> 0" shows 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

158 
"((z + h) ^ n  z ^ n) / h  of_nat n * z ^ (n  Suc 0) = 
20860  159 
h * (\<Sum>p=0..< n  Suc 0. \<Sum>q=0..< n  Suc 0  p. 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

163 
apply (simp add: mult_assoc [symmetric]) 
20860  164 
apply (cases "n", simp) 
165 
apply (simp add: lemma_realpow_diff_sumr2 h 

166 
right_diff_distrib [symmetric] mult_assoc 

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

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

169 
apply (subst sumr_diff_mult_const2) 
20860  170 
apply simp 
171 
apply (simp only: lemma_termdiff1 setsum_right_distrib) 

172 
apply (rule setsum_cong [OF refl]) 

15539  173 
apply (simp add: diff_minus [symmetric] less_iff_Suc_add) 
20860  174 
apply (clarify) 
175 
apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac 

176 
del: setsum_op_ivl_Suc realpow_Suc) 

177 
apply (subst mult_assoc [symmetric], subst power_add [symmetric]) 

178 
apply (simp add: mult_ac) 

179 
done 

180 

181 
lemma real_setsum_nat_ivl_bounded2: 

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

182 
fixes K :: "'a::ordered_semidom" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

183 
assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

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

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

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

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

190 

15229  191 
lemma lemma_termdiff3: 
23112
2bc882fbe51c
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents:
23097
diff
changeset

192 
fixes h z :: "'a::{real_normed_field,recpower}" 
20860  193 
assumes 1: "h \<noteq> 0" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

196 
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

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

199 
have "norm (((z + h) ^ n  z ^ n) / h  of_nat n * z ^ (n  Suc 0)) = 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

203 
apply (subst norm_mult) 
20860  204 
apply (rule mult_commute) 
205 
done 

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

206 
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

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

208 
from norm_ge_zero 2 have K: "0 \<le> K" by (rule order_trans) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

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

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

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

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

218 
order_trans [OF norm_setsum] 
20860  219 
real_setsum_nat_ivl_bounded2 
220 
mult_nonneg_nonneg 

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

221 
zero_le_imp_of_nat 
20860  222 
zero_le_power K) 
223 
apply (rule le_Kn, simp) 

224 
done 

225 
qed 

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

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

229 
qed 

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

230 

20860  231 
lemma lemma_termdiff4: 
23112
2bc882fbe51c
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents:
23097
diff
changeset

232 
fixes f :: "'a::{real_normed_field,recpower} \<Rightarrow> 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

235 
assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h" 
20860  236 
shows "f  0 > 0" 
29163  237 
unfolding LIM_def diff_0_right 
238 
proof (safe) 

239 
let ?h = "of_real (k / 2)::'a" 

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

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

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

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

244 

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

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

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

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

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

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

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

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

258 
by (simp add: mult_pos_pos positive_imp_inverse_positive) 

259 
next 

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

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

261 
assume x1: "x \<noteq> 0" and x2: "norm x < min k (r * inverse K / 2)" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

264 
from x1 x3 le have "norm (f x) \<le> K * norm x" by simp 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

268 
using K_neq_zero by simp 

269 
also have "r / 2 < r" 

270 
using r by simp 

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

271 
finally show "norm (f x) < r" . 
20860  272 
qed 
273 
qed 

274 
qed 

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

275 

15229  276 
lemma lemma_termdiff5: 
23112
2bc882fbe51c
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents:
23097
diff
changeset

277 
fixes g :: "'a::{recpower,real_normed_field} \<Rightarrow> 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

278 
nat \<Rightarrow> 'b::banach" 
20860  279 
assumes k: "0 < (k::real)" 
280 
assumes f: "summable f" 

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

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

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

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

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

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

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

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

293 
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

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

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

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

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

301 

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

302 

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

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

304 

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

305 
lemma termdiffs_aux: 
23112
2bc882fbe51c
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents:
23097
diff
changeset

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

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

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

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

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

313 
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

314 
from norm_ge_zero r1 have r: "0 < r" 
20860  315 
by (rule order_le_less_trans) 
316 
hence r_neq_0: "r \<noteq> 0" by simp 

317 
show ?thesis 

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

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

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

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

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

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

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

325 
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

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

327 
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

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

330 
also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n  Suc 0)) 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

331 
= (\<lambda>n. diffs (%m. of_nat (m  Suc 0) * norm (c m) * inverse r) n * (r ^ n))" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

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

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

335 
done 
20860  336 
finally have "summable 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

358 
\<le> norm (c n) * of_nat n * of_nat (n  Suc 0) * r ^ (n  2) * norm h" 
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

360 
apply (rule mult_left_mono [OF _ norm_ge_zero]) 
20860  361 
apply (simp (no_asm) add: mult_assoc [symmetric]) 
362 
apply (rule lemma_termdiff3) 

363 
apply (rule h) 

364 
apply (rule r1 [THEN order_less_imp_le]) 

365 
apply (rule xh [THEN order_less_imp_le]) 

366 
done 

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

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

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

369 

20860  370 
lemma termdiffs: 
23112
2bc882fbe51c
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
huffman
parents:
23097
diff
changeset

371 
fixes K x :: "'a::{recpower,real_normed_field,banach}" 
20860  372 
assumes 1: "summable (\<lambda>n. c n * K ^ n)" 
373 
assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)" 

374 
assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)" 

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

375 
assumes 4: "norm x < norm K" 
20860  376 
shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)" 
29163  377 
unfolding deriv_def 
378 
proof (rule LIM_zero_cancel) 

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

381 
proof (rule LIM_equal2) 

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

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

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

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

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

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

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

393 
by (rule powser_inside [OF 1 5]) 

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

395 
by (rule powser_inside [OF 2 4]) 

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

397 
 (\<Sum>n. diffs c n * x ^ n) = 

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

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

401 
apply (subst suminf_divide [symmetric]) 

402 
apply (rule summable_diff [OF B A]) 

403 
apply (subst suminf_diff) 

404 
apply (rule summable_divide) 

405 
apply (rule summable_diff [OF B A]) 

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

29163  407 
apply (rule arg_cong [where f="suminf"], rule ext) 
29667  408 
apply (simp add: algebra_simps) 
20860  409 
done 
410 
next 

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

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

412 
of_nat n * x ^ (n  Suc 0)))  0 > 0" 
20860  413 
by (rule termdiffs_aux [OF 3 4]) 
414 
qed 

415 
qed 

416 

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

417 

29695  418 
subsection{* Some properties of factorials *} 
419 

420 
lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0" 

421 
by auto 

422 

423 
lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)" 

424 
by auto 

425 

426 
lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)" 

427 
by simp 

428 

429 
lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))" 

430 
by (auto simp add: positive_imp_inverse_positive) 

431 

432 
lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))" 

433 
by (auto intro: order_less_imp_le) 

434 

435 

29164  436 
subsection {* Exponential Function *} 
23043  437 

438 
definition 

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

439 
exp :: "'a \<Rightarrow> 'a::{recpower,real_normed_field,banach}" where 
25062  440 
"exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))" 
23043  441 

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

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

443 
fixes x :: "'a::{real_normed_algebra_1,recpower,banach}" 
25062  444 
defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

446 
proof  
25062  447 
have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

448 
unfolding S_def by (simp add: power_Suc del: mult_Suc) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

449 
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

450 
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

451 
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

452 
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

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

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

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

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

457 
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

458 
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

459 
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

460 
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

461 
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

462 
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

463 
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

464 
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

465 
hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

467 
thus "norm (S (Suc n)) \<le> r * norm (S n)" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

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

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

471 

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

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

473 
fixes x :: "'a::{real_normed_algebra_1,recpower,banach}" 
25062  474 
shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

475 
proof (rule summable_norm_comparison_test [OF exI, rule_format]) 
25062  476 
show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

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

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

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

482 

23043  483 
lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

484 
by (insert summable_exp_generic [where x=x], simp) 
23043  485 

25062  486 
lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

487 
unfolding exp_def by (rule summable_exp_generic [THEN summable_sums]) 
23043  488 

489 

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

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

491 
"diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))" 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23413
diff
changeset

492 
by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def of_nat_mult 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

494 

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

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

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

497 

25062  498 
lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

499 
by (auto intro!: ext simp add: exp_def) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

500 

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

501 
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" 
15229  502 
apply (simp add: exp_def) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

503 
apply (subst lemma_exp_ext) 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

504 
apply (subgoal_tac "DERIV (\<lambda>u. \<Sum>n. of_real (inverse (real (fact n))) * u ^ n) x :> (\<Sum>n. diffs (\<lambda>n. of_real (inverse (real (fact n)))) n * x ^ n)") 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

506 
apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

507 
apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+ 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

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

510 

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

511 
lemma isCont_exp [simp]: "isCont exp x" 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

512 
by (rule DERIV_exp [THEN DERIV_isCont]) 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

513 

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

514 

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

516 

23278  517 
lemma powser_zero: 
518 
fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1,recpower}" 

519 
shows "(\<Sum>n. f n * 0 ^ n) = f 0" 

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

520 
proof  
23278  521 
have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

522 
by (rule sums_unique [OF series_zero], simp add: power_0_left) 
23278  523 
thus ?thesis by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

525 

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

528 

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

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

530 
"(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))" 
28069  531 
by (simp add: setsum_head_Suc setsum_shift_bounds_cl_Suc_ivl 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

533 

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

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

535 
fixes x y :: "'a::{real_field,recpower}" 
25062  536 
defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

537 
shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n  i))" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

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

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

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

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

543 
case (Suc n) 
25062  544 
have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

545 
unfolding S_def by (simp add: power_Suc del: mult_Suc) 
25062  546 
hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

548 

25062  549 
have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n" 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

551 
also have "\<dots> = (x + y) * (\<Sum>i=0..n. S x i * S y (ni))" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

553 
also have "\<dots> = x * (\<Sum>i=0..n. S x i * S y (ni)) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

554 
+ y * (\<Sum>i=0..n. S x i * S y (ni))" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

556 
also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (ni)) 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

557 
+ (\<Sum>i=0..n. S x i * (y * S y (ni)))" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

558 
by (simp only: setsum_right_distrib mult_ac) 
25062  559 
also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (ni))) 
560 
+ (\<Sum>i=0..n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni)))" 

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

561 
by (simp add: times_S Suc_diff_le) 
25062  562 
also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (ni))) = 
563 
(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc ni)))" 

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

564 
by (subst setsum_cl_ivl_Suc2, simp) 
25062  565 
also have "(\<Sum>i=0..n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni))) = 
566 
(\<Sum>i=0..Suc n. real (Suc ni) *\<^sub>R (S x i * S y (Suc ni)))" 

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

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

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

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

571 
by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric] 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

572 
real_of_nat_add [symmetric], simp) 
25062  573 
also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc ni))" 
23127  574 
by (simp only: scaleR_right.setsum) 
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

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

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

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

579 

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

580 
lemma exp_add: "exp (x + y) = exp x * exp y" 
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset

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

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

583 

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

586 

23241  587 
lemma exp_of_real: "exp (of_real x) = of_real (exp x)" 
588 
unfolding exp_def 

589 
apply (subst of_real.suminf) 

590 
apply (rule summable_exp_generic) 

591 
apply (simp add: scaleR_conv_of_real) 

592 
done 

593 

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

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

597 
also assume "exp x = 0" 

598 
finally show "False" by simp 

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

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

600 

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

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

603 

29170  604 
lemma exp_diff: "exp (x  y) = exp x / exp y" 
605 
unfolding diff_minus divide_inverse 

606 
by (simp add: exp_add exp_minus) 

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

607 

29167  608 

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

610 

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

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

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

615 
proof  

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

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

618 
qed 

619 

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

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

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

622 

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

625 

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

627 
by (simp add: not_le) 

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

628 

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

629 
lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x" 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

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

631 

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

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

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

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

636 

29170  637 
text {* Strict monotonicity of exponential. *} 
638 

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

640 
apply (drule order_le_imp_less_or_eq, auto) 

641 
apply (simp add: exp_def) 

642 
apply (rule real_le_trans) 

643 
apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le) 

644 
apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff) 

645 
done 

646 

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

648 
proof  

649 
assume x: "0 < x" 

650 
hence "1 < 1 + x" by simp 

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

652 
by (simp add: exp_ge_add_one_self_aux) 

653 
finally show ?thesis . 

654 
qed 

655 

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

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

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

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

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

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

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

662 
hence "1 < exp y / exp x" by (simp only: exp_diff) 
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

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

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

665 

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

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

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

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

670 

29170  671 
lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

673 

29170  674 
lemma exp_le_cancel_iff [iff]: "exp (x::real) \<le> exp y \<longleftrightarrow> x \<le> y" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

676 

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

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

679 

29170  680 
text {* Comparisons of @{term "exp x"} with one. *} 
681 

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

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

684 

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

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

687 

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

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

690 

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

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

693 

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

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

696 

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

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

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

699 
apply (auto intro: isCont_exp simp add: le_diff_eq) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

700 
apply (subgoal_tac "1 + (y  1) \<le> exp (y  1)") 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

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

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

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

704 

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

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

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

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

708 
apply (rule_tac [2] x = 0 in exI) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

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

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

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

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

714 

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

715 

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

717 

23043  718 
definition 
719 
ln :: "real => real" where 

720 
"ln x = (THE u. exp u = x)" 

721 

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

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

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

724 

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

725 
lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x" 
c2b6b5a9e136
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents:
22653
diff
changeset

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

727 

29171  728 
lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x" 
729 
apply (rule iffI) 

730 
apply (erule subst, rule exp_gt_zero) 

731 
apply (erule exp_ln) 

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

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

733 

29171  734 
lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y" 
735 
by (erule subst, rule ln_exp) 

736 

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

738 
by (rule ln_unique, simp) 

739 

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

741 
by (rule ln_unique, simp add: exp_add) 

742 

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

744 
by (rule ln_unique, simp add: exp_minus) 

745 

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

747 
by (rule ln_unique, simp add: exp_diff) 

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

748 

29171  749 
lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x" 
750 
by (rule ln_unique, simp add: exp_real_of_nat_mult) 

751 

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

753 
by (subst exp_less_cancel_iff [symmetric], simp) 

754 

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

756 
by (simp add: linorder_not_less [symmetric]) 

757 

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

759 
by (simp add: order_eq_iff) 

760 

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

762 
apply (rule exp_le_cancel_iff [THEN iffD1]) 

763 
apply (simp add: exp_ge_add_one_self_aux) 

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

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

765 

29171  766 
lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x" 
767 
by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all 

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

768 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

769 
lemma ln_ge_zero [simp]: 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

770 
assumes x: "1 \<le> x" shows "0 \<le> ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

772 
have "0 < x" using x by arith 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

773 
hence "exp 0 \<le> exp (ln x)" 
22915  774 
by (simp add: x) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

775 
thus ?thesis by (simp only: exp_le_cancel_iff) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

777 

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

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

779 
assumes ln: "0 \<le> ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

780 
and x: "0 < x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

781 
shows "1 \<le> x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

783 
from ln have "ln 1 \<le> ln x" by simp 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

784 
thus ?thesis by (simp add: x del: ln_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

786 

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

787 
lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

788 
by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

789 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

790 
lemma ln_less_zero_iff [simp]: "0 < x ==> (ln x < 0) = (x < 1)" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

791 
by (insert ln_ge_zero_iff [of x], arith) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

792 

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

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

794 
assumes x: "1 < x" shows "0 < ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

796 
have "0 < x" using x by arith 
22915  797 
hence "exp 0 < exp (ln x)" by (simp add: x) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

798 
thus ?thesis by (simp only: exp_less_cancel_iff) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

800 

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

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

802 
assumes ln: "0 < ln x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

803 
and x: "0 < x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

804 
shows "1 < x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

806 
from ln have "ln 1 < ln x" by simp 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

807 
thus ?thesis by (simp add: x del: ln_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

809 

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

810 
lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

811 
by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

812 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

813 
lemma ln_eq_zero_iff [simp]: "0 < x ==> (ln x = 0) = (x = 1)" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

814 
by (insert ln_less_zero_iff [of x] ln_gt_zero_iff [of x], arith) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

815 

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

816 
lemma ln_less_zero: "[ 0 < x; x < 1 ] ==> ln x < 0" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

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

818 

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

819 
lemma exp_ln_eq: "exp u = x ==> ln x = u" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

821 

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

822 
lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x" 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

823 
apply (subgoal_tac "isCont ln (exp (ln x))", simp) 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

824 
apply (rule isCont_inverse_function [where f=exp], simp_all) 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

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

826 

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

827 
lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x" 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

828 
apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"]) 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

829 
apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln]) 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

830 
apply (simp_all add: abs_if isCont_ln) 
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset

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

832 

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

833 

29164  834 
subsection {* Sine and Cosine *} 
835 

836 
definition 

837 
sin :: "real => real" where 

838 
"sin x = (\<Sum>n. (if even(n) then 0 else 

839 
(1 ^ ((n  Suc 0) div 2))/(real (fact n))) * x ^ n)" 

840 

841 
definition 

842 
cos :: "real => real" where 

843 
"cos x = (\<Sum>n. (if even(n) then (1 ^ (n div 2))/(real (fact n)) 

844 
else 0) * x ^ n)" 

845 

846 
lemma summable_sin: 

847 
"summable (%n. 

848 
(if even n then 0 

849 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) * 

850 
x ^ n)" 

851 
apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test) 

852 
apply (rule_tac [2] summable_exp) 

853 
apply (rule_tac x = 0 in exI) 

854 
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff) 

855 
done 

856 

857 
lemma summable_cos: 

858 
"summable (%n. 

859 
(if even n then 

860 
1 ^ (n div 2)/(real (fact n)) else 0) * x ^ n)" 

861 
apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test) 

862 
apply (rule_tac [2] summable_exp) 

863 
apply (rule_tac x = 0 in exI) 

864 
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff) 

865 
done 

866 

867 
lemma lemma_STAR_sin: 

868 
"(if even n then 0 

869 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0" 

870 
by (induct "n", auto) 

871 

872 
lemma lemma_STAR_cos: 

873 
"0 < n > 

874 
1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0" 

875 
by (induct "n", auto) 

876 

877 
lemma lemma_STAR_cos1: 

878 
"0 < n > 

879 
(1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0" 

880 
by (induct "n", auto) 

881 

882 
lemma lemma_STAR_cos2: 

883 
"(\<Sum>n=1..<n. if even n then 1 ^ (n div 2)/(real (fact n)) * 0 ^ n 

884 
else 0) = 0" 

885 
apply (induct "n") 

886 
apply (case_tac [2] "n", auto) 

887 
done 

888 

889 
lemma sin_converges: 

890 
"(%n. (if even n then 0 

891 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) * 

892 
x ^ n) sums sin(x)" 

893 
unfolding sin_def by (rule summable_sin [THEN summable_sums]) 

894 

895 
lemma cos_converges: 

896 
"(%n. (if even n then 

897 
1 ^ (n div 2)/(real (fact n)) 

898 
else 0) * x ^ n) sums cos(x)" 

899 
unfolding cos_def by (rule summable_cos [THEN summable_sums]) 

900 

901 
lemma sin_fdiffs: 

902 
"diffs(%n. if even n then 0 

903 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) 

904 
= (%n. if even n then 

905 
1 ^ (n div 2)/(real (fact n)) 

906 
else 0)" 

907 
by (auto intro!: ext 

908 
simp add: diffs_def divide_inverse real_of_nat_def of_nat_mult 

909 
simp del: mult_Suc of_nat_Suc) 

910 

911 
lemma sin_fdiffs2: 

912 
"diffs(%n. if even n then 0 

913 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) n 

914 
= (if even n then 

915 
1 ^ (n div 2)/(real (fact n)) 

916 
else 0)" 

917 
by (simp only: sin_fdiffs) 

918 

919 
lemma cos_fdiffs: 

920 
"diffs(%n. if even n then 

921 
1 ^ (n div 2)/(real (fact n)) else 0) 

922 
= (%n.  (if even n then 0 

923 
else 1 ^ ((n  Suc 0)div 2)/(real (fact n))))" 

924 
by (auto intro!: ext 

925 
simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def of_nat_mult 

926 
simp del: mult_Suc of_nat_Suc) 

927 

928 

929 
lemma cos_fdiffs2: 

930 
"diffs(%n. if even n then 

931 
1 ^ (n div 2)/(real (fact n)) else 0) n 

932 
=  (if even n then 0 

933 
else 1 ^ ((n  Suc 0)div 2)/(real (fact n)))" 

934 
by (simp only: cos_fdiffs) 

935 

936 
text{*Now at last we can get the derivatives of exp, sin and cos*} 

937 

938 
lemma lemma_sin_minus: 

939 
" sin x = (\<Sum>n.  ((if even n then 0 

940 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) * x ^ n))" 

941 
by (auto intro!: sums_unique sums_minus sin_converges) 

942 

943 
lemma lemma_sin_ext: 

944 
"sin = (%x. \<Sum>n. 

945 
(if even n then 0 

946 
else 1 ^ ((n  Suc 0) div 2)/(real (fact n))) * 

947 
x ^ n)" 

948 
by (auto intro!: ext simp add: sin_def) 

949 

950 
lemma lemma_cos_ext: 

951 
"cos = (%x. \<Sum>n. 

952 
(if even n then 1 ^ (n div 2)/(real (fact n)) else 0) * 

953 
x ^ n)" 

954 
by (auto intro!: ext simp add: cos_def) 

955 

956 
lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)" 

957 
apply (simp add: cos_def) 

958 
apply (subst lemma_sin_ext) 

959 
apply (auto simp add: sin_fdiffs2 [symmetric]) 

960 
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs) 

961 
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs) 

962 
done 

963 

964 
lemma DERIV_cos [simp]: "DERIV cos x :> sin(x)" 

965 
apply (subst lemma_cos_ext) 

966 
apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left) 

967 
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs) 

968 
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus) 

969 
done 

970 

971 
lemma isCont_sin [simp]: "isCont sin x" 

972 
by (rule DERIV_sin [THEN DERIV_isCont]) 

973 

974 
lemma isCont_cos [simp]: "isCont cos x" 

975 
by (rule DERIV_cos [THEN DERIV_isCont]) 

976 

977 

978 
subsection {* Properties of Sine and Cosine *} 

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

979 

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

980 
lemma sin_zero [simp]: "sin 0 = 0" 
23278  981 
unfolding sin_def by (simp add: powser_zero) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

982 

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

983 
lemma cos_zero [simp]: "cos 0 = 1" 
23278  984 
unfolding cos_def by (simp add: powser_zero) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

985 

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

986 
lemma DERIV_sin_sin_mult [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

987 
"DERIV (%x. sin(x)*sin(x)) x :> cos(x) * sin(x) + cos(x) * sin(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

988 
by (rule DERIV_mult, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

989 

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

990 
lemma DERIV_sin_sin_mult2 [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

991 
"DERIV (%x. sin(x)*sin(x)) x :> 2 * cos(x) * sin(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

992 
apply (cut_tac x = x in DERIV_sin_sin_mult) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

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

995 

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

996 
lemma DERIV_sin_realpow2 [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

997 
"DERIV (%x. (sin x)\<twosuperior>) x :> cos(x) * sin(x) + cos(x) * sin(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

999 

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

1000 
lemma DERIV_sin_realpow2a [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1001 
"DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1003 

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

1004 
lemma DERIV_cos_cos_mult [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1005 
"DERIV (%x. cos(x)*cos(x)) x :> sin(x) * cos(x) + sin(x) * cos(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1006 
by (rule DERIV_mult, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1007 

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

1008 
lemma DERIV_cos_cos_mult2 [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1009 
"DERIV (%x. cos(x)*cos(x)) x :> 2 * cos(x) * sin(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1010 
apply (cut_tac x = x in DERIV_cos_cos_mult) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

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

1013 

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

1014 
lemma DERIV_cos_realpow2 [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1015 
"DERIV (%x. (cos x)\<twosuperior>) x :> sin(x) * cos(x) + sin(x) * cos(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1017 

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

1018 
lemma DERIV_cos_realpow2a [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1019 
"DERIV (%x. (cos x)\<twosuperior>) x :> 2 * cos(x) * sin(x)" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1021 

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

1022 
lemma lemma_DERIV_subst: "[ DERIV f x :> D; D = E ] ==> DERIV f x :> E" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1024 

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

1025 
lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> (2 * cos(x) * sin(x))" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1026 
apply (rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1027 
apply (rule DERIV_cos_realpow2a, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1029 

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

1030 
(* most useful *) 
15229  1031 
lemma DERIV_cos_cos_mult3 [simp]: 
1032 
"DERIV (%x. cos(x)*cos(x)) x :> (2 * cos(x) * sin(x))" 

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

1033 
apply (rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1034 
apply (rule DERIV_cos_cos_mult2, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1036 

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

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

1038 
"\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1039 
(2*cos(x)*sin(x)  2*cos(x)*sin(x))" 
15229  1040 
apply (simp only: diff_minus, safe) 
1041 
apply (rule DERIV_add) 

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

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

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

1044 

15229  1045 
lemma DERIV_sin_circle_all_zero [simp]: 
1046 
"\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0" 

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

1047 
by (cut_tac DERIV_sin_circle_all, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1048 

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

1049 
lemma sin_cos_squared_add [simp]: "((sin x)\<twosuperior>) + ((cos x)\<twosuperior>) = 1" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1050 
apply (cut_tac x = x and y = 0 in DERIV_sin_circle_all_zero [THEN DERIV_isconst_all]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

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

1053 

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

1054 
lemma sin_cos_squared_add2 [simp]: "((cos x)\<twosuperior>) + ((sin x)\<twosuperior>) = 1" 
23286  1055 
apply (subst add_commute) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1056 
apply (simp (no_asm) del: realpow_Suc) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1058 

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

1059 
lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1060 
apply (cut_tac x = x in sin_cos_squared_add2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

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

1063 

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

1064 
lemma sin_squared_eq: "(sin x)\<twosuperior> = 1  (cos x)\<twosuperior>" 
15229  1065 
apply (rule_tac a1 = "(cos x)\<twosuperior>" in add_right_cancel [THEN iffD1]) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

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

1068 

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

1069 
lemma cos_squared_eq: "(cos x)\<twosuperior> = 1  (sin x)\<twosuperior>" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1070 
apply (rule_tac a1 = "(sin x)\<twosuperior>" in add_right_cancel [THEN iffD1]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

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

1073 

15081  1074 
lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1" 
23097  1075 
by (rule power2_le_imp_le, simp_all add: sin_squared_eq) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1076 

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

1077 
lemma sin_ge_minus_one [simp]: "1 \<le> sin x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1078 
apply (insert abs_sin_le_one [of x]) 
22998  1079 
apply (simp add: abs_le_iff del: abs_sin_le_one) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1081 

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

1082 
lemma sin_le_one [simp]: "sin x \<le> 1" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1083 
apply (insert abs_sin_le_one [of x]) 
22998  1084 
apply (simp add: abs_le_iff del: abs_sin_le_one) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1086 

15081  1087 
lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1" 
23097  1088 
by (rule power2_le_imp_le, simp_all add: cos_squared_eq) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1089 

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

1090 
lemma cos_ge_minus_one [simp]: "1 \<le> cos x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1091 
apply (insert abs_cos_le_one [of x]) 
22998  1092 
apply (simp add: abs_le_iff del: abs_cos_le_one) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1094 

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

1095 
lemma cos_le_one [simp]: "cos x \<le> 1" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1096 
apply (insert abs_cos_le_one [of x]) 
22998  1097 
apply (simp add: abs_le_iff del: abs_cos_le_one) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1099 

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

1100 
lemma DERIV_fun_pow: "DERIV g x :> m ==> 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1101 
DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n  1) * m" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1102 
apply (rule lemma_DERIV_subst) 
15229  1103 
apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1104 
apply (rule DERIV_pow, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1106 

15229  1107 
lemma DERIV_fun_exp: 
1108 
"DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m" 

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

1109 
apply (rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1110 
apply (rule_tac f = exp in DERIV_chain2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1111 
apply (rule DERIV_exp, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1113 

15229  1114 
lemma DERIV_fun_sin: 
1115 
"DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m" 

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

1116 
apply (rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1117 
apply (rule_tac f = sin in DERIV_chain2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1118 
apply (rule DERIV_sin, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1120 

15229  1121 
lemma DERIV_fun_cos: 
1122 
"DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> sin(g x) * m" 

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

1123 
apply (rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1124 
apply (rule_tac f = cos in DERIV_chain2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1125 
apply (rule DERIV_cos, auto) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1127 

23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23066
diff
changeset

1128 
lemmas DERIV_intros = DERIV_ident DERIV_const DERIV_cos DERIV_cmult 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1129 
DERIV_sin DERIV_exp DERIV_inverse DERIV_pow 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1130 
DERIV_add DERIV_diff DERIV_mult DERIV_minus 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1131 
DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1132 
DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1133 

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

1134 
(* lemma *) 
15229  1135 
lemma lemma_DERIV_sin_cos_add: 
1136 
"\<forall>x. 

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

1137 
DERIV (%x. (sin (x + y)  (sin x * cos y + cos x * sin y)) ^ 2 + 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1138 
(cos (x + y)  (cos x * cos y  sin x * sin y)) ^ 2) x :> 0" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1139 
apply (safe, rule lemma_DERIV_subst) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1140 
apply (best intro!: DERIV_intros intro: DERIV_chain2) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1141 
{*replaces the old @{text DERIV_tac}*} 
29667  1142 
apply (auto simp add: algebra_simps) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1144 

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

1145 
lemma sin_cos_add [simp]: 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1146 
"(sin (x + y)  (sin x * cos y + cos x * sin y)) ^ 2 + 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1147 
(cos (x + y)  (cos x * cos y  sin x * sin y)) ^ 2 = 0" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1148 
apply (cut_tac y = 0 and x = x and y7 = y 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1149 
in lemma_DERIV_sin_cos_add [THEN DERIV_isconst_all]) 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

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

1152 

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

1153 
lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1154 
apply (cut_tac x = x and y = y in sin_cos_add) 
22969  1155 
apply (simp del: sin_cos_add) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1157 

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

1158 
lemma cos_add: "cos (x + y) = cos x * cos y  sin x * sin y" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1159 
apply (cut_tac x = x and y = y in sin_cos_add) 
22969  1160 
apply (simp del: sin_cos_add) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1162 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15081
diff
changeset

1163 
lemma lemma_DERIV_sin_cos_minus: 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15081
diff
changeset

1164 
"\<forall>x. DERIV (%x. (sin(x) + (sin x)) ^ 2 + (cos(x)  (cos x)) ^ 2) x :> 0" 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1165 
apply (safe, rule lemma_DERIV_subst) 
29667  1166 
apply (best intro!: DERIV_intros intro: DERIV_chain2) 
1167 
apply (simp add: algebra_simps) 

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

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

1169 

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

1170 
lemma sin_cos_minus: 
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15081
diff
changeset

1171 
"(sin(x) + (sin x)) ^ 2 + (cos(x)  (cos x)) ^ 2 = 0" 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15081
diff
changeset

1172 
apply (cut_tac y = 0 and x = x 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15081
diff
changeset

1173 
in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all]) 
22969  1174 
apply simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1176 

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

1177 
lemma sin_minus [simp]: "sin (x) = sin(x)" 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1178 
using sin_cos_minus [where x=x] by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1179 

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

1180 
lemma cos_minus [simp]: "cos (x) = cos(x)" 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1181 
using sin_cos_minus [where x=x] by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1182 

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

1183 
lemma sin_diff: "sin (x  y) = sin x * cos y  cos x * sin y" 
22969  1184 
by (simp add: diff_minus sin_add) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1185 

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

1186 
lemma sin_diff2: "sin (x  y) = cos y * sin x  sin y * cos x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1188 

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

1189 
lemma cos_diff: "cos (x  y) = cos x * cos y + sin x * sin y" 
22969  1190 
by (simp add: diff_minus cos_add) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1191 

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

1192 
lemma cos_diff2: "cos (x  y) = cos y * cos x + sin y * sin x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1194 

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

1195 
lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x" 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1196 
using sin_add [where x=x and y=x] by simp 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1197 

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

1198 
lemma cos_double: "cos(2* x) = ((cos x)\<twosuperior>)  ((sin x)\<twosuperior>)" 
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

1199 
using cos_add [where x=x and y=x] 
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset

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

1201 

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

1202 

29164  1203 
subsection {* The Constant Pi *} 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1204 

23043  1205 
definition 
1206 
pi :: "real" where 

23053  1207 
"pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)" 
23043  1208 

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

1209 
text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"}; 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1210 
hence define pi.*} 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1211 

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

1212 
lemma sin_paired: 
23177  1213 
"(%n. 1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1214 
sums sin x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1216 
have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1217 
(if even k then 0 
23177  1218 
else 1 ^ ((k  Suc 0) div 2) / real (fact k)) * 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1219 
x ^ k) 
23176  1220 
sums sin x" 
1221 
unfolding sin_def 

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

1222 
by (rule sin_converges [THEN sums_summable, THEN sums_group], simp) 
23176  1223 
thus ?thesis by (simp add: mult_ac) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

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

1225 

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

1226 
lemma sin_gt_zero: "[0 < x; x < 2 ] ==> 0 < sin x" 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1227 
apply (subgoal_tac 
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

1228 
"(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. 
< 