author  immler 
Fri, 10 Mar 2017 23:16:40 +0100  
changeset 65204  d23eded35a33 
parent 65109  a79c1080f1e9 
child 65552  f533820e7248 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32047
diff
changeset

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

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

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

63558  7 
section \<open>Power Series, Transcendental Functions etc.\<close> 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

8 

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

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

12 

62083  13 
text \<open>A fact theorem on reals.\<close> 
14 

63467  15 
lemma square_fact_le_2_fact: "fact n * fact n \<le> (fact (2 * n) :: real)" 
62083  16 
proof (induct n) 
63467  17 
case 0 
18 
then show ?case by simp 

62083  19 
next 
20 
case (Suc n) 

21 
have "(fact (Suc n)) * (fact (Suc n)) = of_nat (Suc n) * of_nat (Suc n) * (fact n * fact n :: real)" 

22 
by (simp add: field_simps) 

23 
also have "\<dots> \<le> of_nat (Suc n) * of_nat (Suc n) * fact (2 * n)" 

24 
by (rule mult_left_mono [OF Suc]) simp 

25 
also have "\<dots> \<le> of_nat (Suc (Suc (2 * n))) * of_nat (Suc (2 * n)) * fact (2 * n)" 

26 
by (rule mult_right_mono)+ (auto simp: field_simps) 

27 
also have "\<dots> = fact (2 * Suc n)" by (simp add: field_simps) 

28 
finally show ?case . 

29 
qed 

30 

62347  31 
lemma fact_in_Reals: "fact n \<in> \<real>" 
32 
by (induction n) auto 

33 

34 
lemma of_real_fact [simp]: "of_real (fact n) = fact n" 

35 
by (metis of_nat_fact of_real_of_nat_eq) 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

36 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

37 
lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)" 
64272  38 
by (simp add: pochhammer_prod) 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

39 

63467  40 
lemma norm_fact [simp]: "norm (fact n :: 'a::real_normed_algebra_1) = fact n" 
61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61518
diff
changeset

41 
proof  
63467  42 
have "(fact n :: 'a) = of_real (fact n)" 
43 
by simp 

44 
also have "norm \<dots> = fact n" 

45 
by (subst norm_of_real) simp 

61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61518
diff
changeset

46 
finally show ?thesis . 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61518
diff
changeset

47 
qed 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61518
diff
changeset

48 

57025  49 
lemma root_test_convergence: 
50 
fixes f :: "nat \<Rightarrow> 'a::banach" 

61969  51 
assumes f: "(\<lambda>n. root n (norm (f n))) \<longlonglongrightarrow> x" \<comment> "could be weakened to lim sup" 
63467  52 
and "x < 1" 
57025  53 
shows "summable f" 
54 
proof  

55 
have "0 \<le> x" 

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

60758  57 
from \<open>x < 1\<close> obtain z where z: "x < z" "z < 1" 
57025  58 
by (metis dense) 
63467  59 
from f \<open>x < z\<close> have "eventually (\<lambda>n. root n (norm (f n)) < z) sequentially" 
57025  60 
by (rule order_tendstoD) 
61 
then have "eventually (\<lambda>n. norm (f n) \<le> z^n) sequentially" 

62 
using eventually_ge_at_top 

63 
proof eventually_elim 

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

66 
from power_strict_mono[OF less, of n] n show "norm (f n) \<le> z ^ n" 

57025  67 
by simp 
68 
qed 

69 
then show "summable f" 

70 
unfolding eventually_sequentially 

60758  71 
using z \<open>0 \<le> x\<close> by (auto intro!: summable_comparison_test[OF _ summable_geometric]) 
57025  72 
qed 
73 

63766
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

74 
subsection \<open>More facts about binomial coefficients\<close> 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

75 

695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

76 
text \<open> 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

77 
These facts could have been proven before, but having real numbers 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

78 
makes the proofs a lot easier. 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

79 
\<close> 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

80 

695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

81 
lemma central_binomial_odd: 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

82 
"odd n \<Longrightarrow> n choose (Suc (n div 2)) = n choose (n div 2)" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

83 
proof  
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

84 
assume "odd n" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

85 
hence "Suc (n div 2) \<le> n" by presburger 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

86 
hence "n choose (Suc (n div 2)) = n choose (n  Suc (n div 2))" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

87 
by (rule binomial_symmetric) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

88 
also from \<open>odd n\<close> have "n  Suc (n div 2) = n div 2" by presburger 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

89 
finally show ?thesis . 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

90 
qed 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

91 

695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

92 
lemma binomial_less_binomial_Suc: 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

93 
assumes k: "k < n div 2" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

94 
shows "n choose k < n choose (Suc k)" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

95 
proof  
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

96 
from k have k': "k \<le> n" "Suc k \<le> n" by simp_all 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

97 
from k' have "real (n choose k) = fact n / (fact k * fact (n  k))" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

98 
by (simp add: binomial_fact) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

99 
also from k' have "n  k = Suc (n  Suc k)" by simp 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

100 
also from k' have "fact \<dots> = (real n  real k) * fact (n  Suc k)" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

101 
by (subst fact_Suc) (simp_all add: of_nat_diff) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

102 
also from k have "fact k = fact (Suc k) / (real k + 1)" by (simp add: field_simps) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

103 
also have "fact n / (fact (Suc k) / (real k + 1) * ((real n  real k) * fact (n  Suc k))) = 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

104 
(n choose (Suc k)) * ((real k + 1) / (real n  real k))" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

105 
using k by (simp add: divide_simps binomial_fact) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

106 
also from assms have "(real k + 1) / (real n  real k) < 1" by simp 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

107 
finally show ?thesis using k by (simp add: mult_less_cancel_left) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

108 
qed 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

109 

695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

110 
lemma binomial_strict_mono: 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

111 
assumes "k < k'" "2*k' \<le> n" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

112 
shows "n choose k < n choose k'" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

113 
proof  
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

114 
from assms have "k \<le> k'  1" by simp 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

115 
thus ?thesis 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

116 
proof (induction rule: inc_induct) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

117 
case base 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

118 
with assms binomial_less_binomial_Suc[of "k'  1" n] 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

119 
show ?case by simp 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

120 
next 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

121 
case (step k) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

122 
from step.prems step.hyps assms have "n choose k < n choose (Suc k)" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

123 
by (intro binomial_less_binomial_Suc) simp_all 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

124 
also have "\<dots> < n choose k'" by (rule step.IH) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

125 
finally show ?case . 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

126 
qed 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

127 
qed 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

128 

695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

129 
lemma binomial_mono: 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

130 
assumes "k \<le> k'" "2*k' \<le> n" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

131 
shows "n choose k \<le> n choose k'" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

132 
using assms binomial_strict_mono[of k k' n] by (cases "k = k'") simp_all 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

133 

695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

134 
lemma binomial_strict_antimono: 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

135 
assumes "k < k'" "2 * k \<ge> n" "k' \<le> n" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

136 
shows "n choose k > n choose k'" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

137 
proof  
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

138 
from assms have "n choose (n  k) > n choose (n  k')" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

139 
by (intro binomial_strict_mono) (simp_all add: algebra_simps) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

140 
with assms show ?thesis by (simp add: binomial_symmetric [symmetric]) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

141 
qed 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

142 

695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

143 
lemma binomial_antimono: 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

144 
assumes "k \<le> k'" "k \<ge> n div 2" "k' \<le> n" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

145 
shows "n choose k \<ge> n choose k'" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

146 
proof (cases "k = k'") 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

147 
case False 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

148 
note not_eq = False 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

149 
show ?thesis 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

150 
proof (cases "k = n div 2 \<and> odd n") 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

151 
case False 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

152 
with assms(2) have "2*k \<ge> n" by presburger 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

153 
with not_eq assms binomial_strict_antimono[of k k' n] 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

154 
show ?thesis by simp 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

155 
next 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

156 
case True 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

157 
have "n choose k' \<le> n choose (Suc (n div 2))" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

158 
proof (cases "k' = Suc (n div 2)") 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

159 
case False 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

160 
with assms True not_eq have "Suc (n div 2) < k'" by simp 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

161 
with assms binomial_strict_antimono[of "Suc (n div 2)" k' n] True 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

162 
show ?thesis by auto 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

163 
qed simp_all 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

164 
also from True have "\<dots> = n choose k" by (simp add: central_binomial_odd) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

165 
finally show ?thesis . 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

166 
qed 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

167 
qed simp_all 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

168 

695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

169 
lemma binomial_maximum: "n choose k \<le> n choose (n div 2)" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

170 
proof  
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

171 
have "k \<le> n div 2 \<longleftrightarrow> 2*k \<le> n" by linarith 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

172 
consider "2*k \<le> n"  "2*k \<ge> n" "k \<le> n"  "k > n" by linarith 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

173 
thus ?thesis 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

174 
proof cases 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

175 
case 1 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

176 
thus ?thesis by (intro binomial_mono) linarith+ 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

177 
next 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

178 
case 2 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

179 
thus ?thesis by (intro binomial_antimono) simp_all 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

180 
qed (simp_all add: binomial_eq_0) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

181 
qed 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

182 

695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

183 
lemma binomial_maximum': "(2*n) choose k \<le> (2*n) choose n" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

184 
using binomial_maximum[of "2*n"] by simp 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

185 

695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

186 
lemma central_binomial_lower_bound: 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

187 
assumes "n > 0" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

188 
shows "4^n / (2*real n) \<le> real ((2*n) choose n)" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

189 
proof  
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

190 
from binomial[of 1 1 "2*n"] 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

191 
have "4 ^ n = (\<Sum>k=0..2*n. (2*n) choose k)" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

192 
by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

193 
also have "{0..2*n} = {0<..<2*n} \<union> {0,2*n}" by auto 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

194 
also have "(\<Sum>k\<in>\<dots>. (2*n) choose k) = 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

195 
(\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)" 
64267  196 
by (subst sum.union_disjoint) auto 
63766
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

197 
also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

198 
by (cases n) simp_all 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

199 
also from assms have "\<dots> \<le> (\<Sum>k\<le>n. (n choose k)\<^sup>2)" 
64267  200 
by (intro sum_mono3) auto 
63766
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

201 
also have "\<dots> = (2*n) choose n" by (rule choose_square_sum) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

202 
also have "(\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) \<le> (\<Sum>k\<in>{0<..<2*n}. (2*n) choose n)" 
64267  203 
by (intro sum_mono binomial_maximum') 
63766
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

204 
also have "\<dots> = card {0<..<2*n} * ((2*n) choose n)" by simp 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

205 
also have "card {0<..<2*n} \<le> 2*n  1" by (cases n) simp_all 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

206 
also have "(2 * n  1) * (2 * n choose n) + (2 * n choose n) = ((2*n) choose n) * (2*n)" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

207 
using assms by (simp add: algebra_simps) 
63834  208 
finally have "4 ^ n \<le> (2 * n choose n) * (2 * n)" by simp_all 
63766
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

209 
hence "real (4 ^ n) \<le> real ((2 * n choose n) * (2 * n))" 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

210 
by (subst of_nat_le_iff) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

211 
with assms show ?thesis by (simp add: field_simps) 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

212 
qed 
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63721
diff
changeset

213 

63467  214 

60758  215 
subsection \<open>Properties of Power Series\<close> 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

216 

63467  217 
lemma powser_zero [simp]: "(\<Sum>n. f n * 0 ^ n) = f 0" 
218 
for f :: "nat \<Rightarrow> 'a::real_normed_algebra_1" 

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

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

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

221 
by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left) 
63558  222 
then show ?thesis by simp 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

224 

63467  225 
lemma powser_sums_zero: "(\<lambda>n. a n * 0^n) sums a 0" 
226 
for a :: "nat \<Rightarrow> 'a::real_normed_div_algebra" 

227 
using sums_finite [of "{0}" "\<lambda>n. a n * 0 ^ n"] 

228 
by simp 

229 

230 
lemma powser_sums_zero_iff [simp]: "(\<lambda>n. a n * 0^n) sums x \<longleftrightarrow> a 0 = x" 

231 
for a :: "nat \<Rightarrow> 'a::real_normed_div_algebra" 

232 
using powser_sums_zero sums_unique2 by blast 

233 

234 
text \<open> 

235 
Power series has a circle or radius of convergence: if it sums for \<open>x\<close>, 

236 
then it sums absolutely for \<open>z\<close> with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.\<close> 

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

237 

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

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

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

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

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

244 
from 2 have x_neq_0: "x \<noteq> 0" by clarsimp 
61969  245 
from 1 have "(\<lambda>n. f n * x^n) \<longlonglongrightarrow> 0" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

246 
by (rule summable_LIMSEQ_zero) 
63558  247 
then have "convergent (\<lambda>n. f n * x^n)" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

248 
by (rule convergentI) 
63558  249 
then have "Cauchy (\<lambda>n. f n * x^n)" 
44726  250 
by (rule convergent_Cauchy) 
63558  251 
then have "Bseq (\<lambda>n. f n * x^n)" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

253 
then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x^n) \<le> K" 
63558  254 
by (auto simp add: Bseq_def) 
255 
have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le> K * norm (z ^ n) * inverse (norm (x^n))" 

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

256 
proof (intro exI allI impI) 
63558  257 
fix n :: nat 
53079  258 
assume "0 \<le> n" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

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

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

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

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

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

264 
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

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

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

267 
by (simp only: mult.assoc) 
63558  268 
finally show "norm (norm (f n * z ^ n)) \<le> K * norm (z ^ n) * inverse (norm (x^n))" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

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

271 
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

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

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

274 
using x_neq_0 
53599  275 
by (simp add: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric]) 
63558  276 
then have "summable (\<lambda>n. norm (z * inverse x) ^ n)" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

277 
by (rule summable_geometric) 
63558  278 
then have "summable (\<lambda>n. K * norm (z * inverse x) ^ n)" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

279 
by (rule summable_mult) 
63558  280 
then show "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

282 
by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib 
63558  283 
power_inverse norm_power mult.assoc) 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

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

285 
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

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

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

288 

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

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

295 

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

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

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

298 
assumes "norm x < 1" 
61969  299 
shows "(\<lambda>n. of_nat n * x ^ n) \<longlonglongrightarrow> 0" 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

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

301 
have "norm x / (1  norm x) \<ge> 0" 
63558  302 
using assms by (auto simp: divide_simps) 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

303 
moreover obtain N where N: "norm x / (1  norm x) < of_int N" 
63558  304 
using ex_le_of_int by (meson ex_less_of_int) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

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

306 
by auto 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

307 
then have *: "real_of_int (N + 1) * norm x / real_of_int N < 1" 
63558  308 
using N assms by (auto simp: field_simps) 
309 
have **: "real_of_int N * (norm x * (real_of_nat (Suc n) * norm (x ^ n))) \<le> 

310 
real_of_nat n * (norm x * ((1 + N) * norm (x ^ n)))" if "N \<le> int n" for n :: nat 

311 
proof  

312 
from that have "real_of_int N * real_of_nat (Suc n) \<le> real_of_nat n * real_of_int (1 + N)" 

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

313 
by (simp add: algebra_simps) 
63558  314 
then have "(real_of_int N * real_of_nat (Suc n)) * (norm x * norm (x ^ n)) \<le> 
315 
(real_of_nat n * (1 + N)) * (norm x * norm (x ^ n))" 

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

316 
using N0 mult_mono by fastforce 
63558  317 
then show ?thesis 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

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

320 
show ?thesis using * 
63558  321 
by (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"]) 
322 
(simp add: N0 norm_mult field_simps ** del: of_nat_Suc of_int_add) 

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

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

324 

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

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

326 
fixes x :: "'a::{real_normed_field,banach}" 
61973  327 
shows "1 < norm x \<Longrightarrow> ((\<lambda>n. of_nat n / x^n) \<longlongrightarrow> 0) sequentially" 
63558  328 
using powser_times_n_limit_0 [of "inverse x"] 
329 
by (simp add: norm_divide divide_simps) 

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

330 

53079  331 
lemma sum_split_even_odd: 
332 
fixes f :: "nat \<Rightarrow> real" 

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

334 
proof (induct n) 
53079  335 
case 0 
336 
then show ?case by simp 

337 
next 

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

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

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

340 
(\<Sum>i<n. f (2 * i)) + (\<Sum>i<n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))" 
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset

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

342 
also have "\<dots> = (\<Sum>i<Suc n. f (2 * i)) + (\<Sum>i<Suc n. g (2 * i + 1))" 
53079  343 
by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

344 
finally show ?case . 
53079  345 
qed 
346 

347 
lemma sums_if': 

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

349 
assumes "g sums x" 

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

350 
shows "(\<lambda> n. if even n then 0 else g ((n  1) div 2)) sums x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

352 
proof (rule LIMSEQ_I) 
53079  353 
fix r :: real 
354 
assume "0 < r" 

60758  355 
from \<open>g sums x\<close>[unfolded sums_def, THEN LIMSEQ_D, OF this] 
64267  356 
obtain no where no_eq: "\<And>n. n \<ge> no \<Longrightarrow> (norm (sum g {..<n}  x) < r)" 
63558  357 
by blast 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

358 

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

359 
let ?SUM = "\<lambda> m. \<Sum>i<m. if even i then 0 else g ((i  1) div 2)" 
63558  360 
have "(norm (?SUM m  x) < r)" if "m \<ge> 2 * no" for m 
361 
proof  

362 
from that have "m div 2 \<ge> no" by auto 

64267  363 
have sum_eq: "?SUM (2 * (m div 2)) = sum g {..< m div 2}" 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

364 
using sum_split_even_odd by auto 
63558  365 
then have "(norm (?SUM (2 * (m div 2))  x) < r)" 
60758  366 
using no_eq unfolding sum_eq using \<open>m div 2 \<ge> no\<close> by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

368 
have "?SUM (2 * (m div 2)) = ?SUM m" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

369 
proof (cases "even m") 
53079  370 
case True 
63558  371 
then show ?thesis 
372 
by (auto simp add: even_two_times_div_two) 

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

373 
next 
53079  374 
case False 
58834  375 
then have eq: "Suc (2 * (m div 2)) = m" by simp 
63558  376 
then have "even (2 * (m div 2))" using \<open>odd m\<close> by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

377 
have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq .. 
60758  378 
also have "\<dots> = ?SUM (2 * (m div 2))" using \<open>even (2 * (m div 2))\<close> by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

380 
qed 
63558  381 
ultimately show ?thesis by auto 
382 
qed 

383 
then show "\<exists>no. \<forall> m \<ge> no. norm (?SUM m  x) < r" 

384 
by blast 

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

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

386 

53079  387 
lemma sums_if: 
388 
fixes g :: "nat \<Rightarrow> real" 

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

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

390 
shows "(\<lambda> n. if even n then f (n div 2) else g ((n  1) div 2)) sums (x + y)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

392 
let ?s = "\<lambda> n. if even n then 0 else f ((n  1) div 2)" 
63558  393 
have if_sum: "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)" 
394 
for B T E 

395 
by (cases B) auto 

53079  396 
have g_sums: "(\<lambda> n. if even n then 0 else g ((n  1) div 2)) sums x" 
60758  397 
using sums_if'[OF \<open>g sums x\<close>] . 
63558  398 
have if_eq: "\<And>B T E. (if \<not> B then T else E) = (if B then E else T)" 
399 
by auto 

400 
have "?s sums y" using sums_if'[OF \<open>f sums y\<close>] . 

401 
from this[unfolded sums_def, THEN LIMSEQ_Suc] 

402 
have "(\<lambda>n. if even n then f (n div 2) else 0) sums y" 

64267  403 
by (simp add: lessThan_Suc_eq_insert_0 sum_atLeast1_atMost_eq image_Suc_lessThan 
63566  404 
if_eq sums_def cong del: if_weak_cong) 
63558  405 
from sums_add[OF g_sums this] show ?thesis 
406 
by (simp only: if_sum) 

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

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

408 

60758  409 
subsection \<open>Alternating series test / Leibniz formula\<close> 
63558  410 
(* FIXME: generalise these results from the reals via type classes? *) 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

411 

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

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

413 
fixes a :: "nat \<Rightarrow> real" 
63558  414 
assumes mono: "\<And>n. a (Suc n) \<le> a n" 
415 
and a_pos: "\<And>n. 0 \<le> a n" 

416 
and "a \<longlonglongrightarrow> 0" 

61969  417 
shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. ( 1)^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. ( 1)^i*a i) \<longlonglongrightarrow> l) \<and> 
418 
((\<forall>n. l \<le> (\<Sum>i<2*n + 1. ( 1)^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. ( 1)^i*a i) \<longlonglongrightarrow> l)" 

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

419 
(is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)") 
53079  420 
proof (rule nested_sequence_unique) 
63558  421 
have fg_diff: "\<And>n. ?f n  ?g n =  a (2 * n)" by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

422 

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

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

53079  427 
qed 
428 
show "\<forall>n. ?g (Suc n) \<le> ?g n" 

429 
proof 

63558  430 
show "?g (Suc n) \<le> ?g n" for n 
431 
using mono[of "Suc (2*n)"] by auto 

53079  432 
qed 
433 
show "\<forall>n. ?f n \<le> ?g n" 

434 
proof 

63558  435 
show "?f n \<le> ?g n" for n 
436 
using fg_diff a_pos by auto 

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

437 
qed 
63558  438 
show "(\<lambda>n. ?f n  ?g n) \<longlonglongrightarrow> 0" 
439 
unfolding fg_diff 

53079  440 
proof (rule LIMSEQ_I) 
441 
fix r :: real 

442 
assume "0 < r" 

61969  443 
with \<open>a \<longlonglongrightarrow> 0\<close>[THEN LIMSEQ_D] obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n  0) < r" 
53079  444 
by auto 
63558  445 
then have "\<forall>n \<ge> N. norm ( a (2 * n)  0) < r" 
446 
by auto 

447 
then show "\<exists>N. \<forall>n \<ge> N. norm ( a (2 * n)  0) < r" 

448 
by auto 

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

451 

53079  452 
lemma summable_Leibniz': 
453 
fixes a :: "nat \<Rightarrow> real" 

61969  454 
assumes a_zero: "a \<longlonglongrightarrow> 0" 
63558  455 
and a_pos: "\<And>n. 0 \<le> a n" 
456 
and a_monotone: "\<And>n. a (Suc n) \<le> a n" 

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

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

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

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

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

464 
let ?P = "\<lambda>n. \<Sum>i<n. ?S i" 
53079  465 
let ?f = "\<lambda>n. ?P (2 * n)" 
466 
let ?g = "\<lambda>n. ?P (2 * n + 1)" 

467 
obtain l :: real 

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

61969  469 
and "?f \<longlonglongrightarrow> l" 
53079  470 
and above_l: "\<forall> n. l \<le> ?g n" 
61969  471 
and "?g \<longlonglongrightarrow> l" 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

472 
using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast 
41970  473 

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

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

476 
proof (rule LIMSEQ_I) 
53079  477 
fix r :: real 
478 
assume "0 < r" 

61969  479 
with \<open>?f \<longlonglongrightarrow> l\<close>[THEN LIMSEQ_D] 
63558  480 
obtain f_no where f: "\<And>n. n \<ge> f_no \<Longrightarrow> norm (?f n  l) < r" 
481 
by auto 

61969  482 
from \<open>0 < r\<close> \<open>?g \<longlonglongrightarrow> l\<close>[THEN LIMSEQ_D] 
63558  483 
obtain g_no where g: "\<And>n. n \<ge> g_no \<Longrightarrow> norm (?g n  l) < r" 
484 
by auto 

485 
have "norm (?Sa n  l) < r" if "n \<ge> (max (2 * f_no) (2 * g_no))" for n 

486 
proof  

487 
from that have "n \<ge> 2 * f_no" and "n \<ge> 2 * g_no" by auto 

488 
show ?thesis 

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

489 
proof (cases "even n") 
53079  490 
case True 
63558  491 
then have n_eq: "2 * (n div 2) = n" 
492 
by (simp add: even_two_times_div_two) 

60758  493 
with \<open>n \<ge> 2 * f_no\<close> have "n div 2 \<ge> f_no" 
53079  494 
by auto 
495 
from f[OF this] show ?thesis 

496 
unfolding n_eq atLeastLessThanSuc_atLeastAtMost . 

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

497 
next 
53079  498 
case False 
63558  499 
then have "even (n  1)" by simp 
58710
7216a10d69ba
augmented and tuned facts on even/odd and division
haftmann
parents:
58709
diff
changeset

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

501 
by (simp add: even_two_times_div_two) 
63558  502 
then have range_eq: "n  1 + 1 = n" 
53079  503 
using odd_pos[OF False] by auto 
60758  504 
from n_eq \<open>n \<ge> 2 * g_no\<close> have "(n  1) div 2 \<ge> g_no" 
53079  505 
by auto 
506 
from g[OF this] show ?thesis 

63558  507 
by (simp only: n_eq range_eq) 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

508 
qed 
63558  509 
qed 
510 
then show "\<exists>no. \<forall>n \<ge> no. norm (?Sa n  l) < r" by blast 

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

511 
qed 
63558  512 
then have sums_l: "(\<lambda>i. (1)^i * a i) sums l" 
513 
by (simp only: sums_def) 

514 
then show "summable ?S" 

515 
by (auto simp: summable_def) 

516 

517 
have "l = suminf ?S" by (rule sums_unique[OF sums_l]) 

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

518 

53079  519 
fix n 
520 
show "suminf ?S \<le> ?g n" 

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

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

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

61969  524 
show "?g \<longlonglongrightarrow> suminf ?S" 
525 
using \<open>?g \<longlonglongrightarrow> l\<close> \<open>l = suminf ?S\<close> by auto 

526 
show "?f \<longlonglongrightarrow> suminf ?S" 

527 
using \<open>?f \<longlonglongrightarrow> l\<close> \<open>l = suminf ?S\<close> by auto 

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

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

529 

53079  530 
theorem summable_Leibniz: 
531 
fixes a :: "nat \<Rightarrow> real" 

63558  532 
assumes a_zero: "a \<longlonglongrightarrow> 0" 
533 
and "monoseq a" 

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

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

536 
(\<forall>n. (\<Sum>i. ( 1)^i*a i) \<in> { \<Sum>i<2*n. ( 1)^i * a i .. \<Sum>i<2*n+1. ( 1)^i * a i})" (is "?pos") 
53079  537 
and "a 0 < 0 \<longrightarrow> 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57514
diff
changeset

538 
(\<forall>n. (\<Sum>i. ( 1)^i*a i) \<in> { \<Sum>i<2*n+1. ( 1)^i * a i .. \<Sum>i<2*n. ( 1)^i * a i})" (is "?neg") 
61969  539 
and "(\<lambda>n. \<Sum>i<2*n. ( 1)^i*a i) \<longlonglongrightarrow> (\<Sum>i. ( 1)^i*a i)" (is "?f") 
540 
and "(\<lambda>n. \<Sum>i<2*n+1. ( 1)^i*a i) \<longlonglongrightarrow> (\<Sum>i. ( 1)^i*a i)" (is "?g") 

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

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

542 
have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g" 
63558  543 
proof (cases "(\<forall>n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)") 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

544 
case True 
63558  545 
then have ord: "\<And>n m. m \<le> n \<Longrightarrow> a n \<le> a m" 
546 
and ge0: "\<And>n. 0 \<le> a n" 

53079  547 
by auto 
63558  548 
have mono: "a (Suc n) \<le> a n" for n 
549 
using ord[where n="Suc n" and m=n] by auto 

61969  550 
note leibniz = summable_Leibniz'[OF \<open>a \<longlonglongrightarrow> 0\<close> ge0] 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

551 
from leibniz[OF mono] 
60758  552 
show ?thesis using \<open>0 \<le> a 0\<close> by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

553 
next 
63558  554 
let ?a = "\<lambda>n.  a n" 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

555 
case False 
61969  556 
with monoseq_le[OF \<open>monoseq a\<close> \<open>a \<longlonglongrightarrow> 0\<close>] 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

557 
have "(\<forall> n. a n \<le> 0) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)" by auto 
63558  558 
then have ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n" 
53079  559 
by auto 
63558  560 
have monotone: "?a (Suc n) \<le> ?a n" for n 
561 
using ord[where n="Suc n" and m=n] by auto 

53079  562 
note leibniz = 
563 
summable_Leibniz'[OF _ ge0, of "\<lambda>x. x", 

61969  564 
OF tendsto_minus[OF \<open>a \<longlonglongrightarrow> 0\<close>, unfolded minus_zero] monotone] 
53079  565 
have "summable (\<lambda> n. (1)^n * ?a n)" 
566 
using leibniz(1) by auto 

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

568 
unfolding summable_def by auto 

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

570 
by auto 

63558  571 
then have ?summable by (auto simp: summable_def) 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

572 
moreover 
63558  573 
have "\<bar> a   b\<bar> = \<bar>a  b\<bar>" for a b :: real 
53079  574 
unfolding minus_diff_minus by auto 
41970  575 

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

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

577 
have move_minus: "(\<Sum>n.  (( 1) ^ n * a n)) =  (\<Sum>n. ( 1) ^ n * a n)" 
53079  578 
by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

579 

60758  580 
have ?pos using \<open>0 \<le> ?a 0\<close> by auto 
53079  581 
moreover have ?neg 
582 
using leibniz(2,4) 

64267  583 
unfolding mult_minus_right sum_negf move_minus neg_le_iff_le 
53079  584 
by auto 
585 
moreover have ?f and ?g 

64267  586 
using leibniz(3,5)[unfolded mult_minus_right sum_negf move_minus, THEN tendsto_minus_cancel] 
53079  587 
by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

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

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

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

593 

63558  594 

60758  595 
subsection \<open>TermbyTerm Differentiability of Power Series\<close> 
23043  596 

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

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

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

599 

63558  600 
text \<open>Lemma about distributing negation over it.\<close> 
53079  601 
lemma diffs_minus: "diffs (\<lambda>n.  c n) = (\<lambda>n.  diffs c n)" 
602 
by (simp add: diffs_def) 

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

603 

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

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

610 

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

611 
lemma lemma_termdiff1: 
63558  612 
fixes z :: "'a :: {monoid_mult,comm_ring}" 
613 
shows "(\<Sum>p<m. (((z + h) ^ (m  p)) * (z ^ p))  (z ^ m)) = 

614 
(\<Sum>p<m. (z ^ p) * (((z + h) ^ (m  p))  (z ^ (m  p))))" 

53079  615 
by (auto simp add: algebra_simps power_add [symmetric]) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

616 

64267  617 
lemma sumr_diff_mult_const2: "sum f {..<n}  of_nat n * r = (\<Sum>i<n. f i  r)" 
63558  618 
for r :: "'a::ring_1" 
64267  619 
by (simp add: sum_subtractf) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

620 

60162  621 
lemma lemma_realpow_rev_sumr: 
63558  622 
"(\<Sum>p<Suc n. (x ^ p) * (y ^ (n  p))) = (\<Sum>p<Suc n. (x ^ (n  p)) * (y ^ p))" 
64267  623 
by (subst nat_diff_sum_reindex[symmetric]) simp 
60162  624 

15229  625 
lemma lemma_termdiff2: 
63558  626 
fixes h :: "'a::field" 
53079  627 
assumes h: "h \<noteq> 0" 
63558  628 
shows "((z + h) ^ n  z ^ n) / h  of_nat n * z ^ (n  Suc 0) = 
629 
h * (\<Sum>p< n  Suc 0. \<Sum>q< n  Suc 0  p. (z + h) ^ q * z ^ (n  2  q))" 

630 
(is "?lhs = ?rhs") 

631 
apply (subgoal_tac "h * ?lhs = h * ?rhs") 

632 
apply (simp add: h) 

53079  633 
apply (simp add: right_diff_distrib diff_divide_distrib h) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

634 
apply (simp add: mult.assoc [symmetric]) 
63558  635 
apply (cases n) 
636 
apply simp 

64267  637 
apply (simp add: diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc 
638 
del: power_Suc sum_lessThan_Suc of_nat_Suc) 

53079  639 
apply (subst lemma_realpow_rev_sumr) 
640 
apply (subst sumr_diff_mult_const2) 

641 
apply simp 

64267  642 
apply (simp only: lemma_termdiff1 sum_distrib_left) 
643 
apply (rule sum.cong [OF refl]) 

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

644 
apply (simp add: less_iff_Suc_add) 
63558  645 
apply clarify 
64267  646 
apply (simp add: sum_distrib_left diff_power_eq_sum ac_simps 
647 
del: sum_lessThan_Suc power_Suc) 

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

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

649 
apply (simp add: ac_simps) 
53079  650 
done 
20860  651 

64267  652 
lemma real_sum_nat_ivl_bounded2: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

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

654 
assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K" 
53079  655 
and K: "0 \<le> K" 
64267  656 
shows "sum f {..<nk} \<le> of_nat n * K" 
657 
apply (rule order_trans [OF sum_mono]) 

63558  658 
apply (rule f) 
659 
apply simp 

53079  660 
apply (simp add: mult_right_mono K) 
661 
done 

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

662 

15229  663 
lemma lemma_termdiff3: 
63558  664 
fixes h z :: "'a::real_normed_field" 
20860  665 
assumes 1: "h \<noteq> 0" 
53079  666 
and 2: "norm z \<le> K" 
667 
and 3: "norm (z + h) \<le> K" 

63558  668 
shows "norm (((z + h) ^ n  z ^ n) / h  of_nat n * z ^ (n  Suc 0)) \<le> 
669 
of_nat n * of_nat (n  Suc 0) * K ^ (n  2) * norm h" 

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

671 
have "norm (((z + h) ^ n  z ^ n) / h  of_nat n * z ^ (n  Suc 0)) = 
63558  672 
norm (\<Sum>p<n  Suc 0. \<Sum>q<n  Suc 0  p. (z + h) ^ q * z ^ (n  2  q)) * norm h" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

673 
by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult.commute norm_mult) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

674 
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

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

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

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

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

681 
apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K) 
20860  682 
done 
63558  683 
show "norm (\<Sum>p<n  Suc 0. \<Sum>q<n  Suc 0  p. (z + h) ^ q * z ^ (n  2  q)) \<le> 
684 
of_nat n * (of_nat (n  Suc 0) * K ^ (n  2))" 

20860  685 
apply (intro 
64267  686 
order_trans [OF norm_sum] 
687 
real_sum_nat_ivl_bounded2 

63558  688 
mult_nonneg_nonneg 
689 
of_nat_0_le_iff 

690 
zero_le_power K) 

691 
apply (rule le_Kn) 

692 
apply simp 

20860  693 
done 
694 
qed 

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

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

696 
by (simp only: mult.assoc) 
20860  697 
finally show ?thesis . 
698 
qed 

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

699 

20860  700 
lemma lemma_termdiff4: 
56167  701 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
63558  702 
and k :: real 
703 
assumes k: "0 < k" 

704 
and le: "\<And>h. h \<noteq> 0 \<Longrightarrow> norm h < k \<Longrightarrow> norm (f h) \<le> K * norm h" 

61976  705 
shows "f \<midarrow>0\<rightarrow> 0" 
56167  706 
proof (rule tendsto_norm_zero_cancel) 
61976  707 
show "(\<lambda>h. norm (f h)) \<midarrow>0\<rightarrow> 0" 
56167  708 
proof (rule real_tendsto_sandwich) 
709 
show "eventually (\<lambda>h. 0 \<le> norm (f h)) (at 0)" 

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

61976  713 
show "(\<lambda>h. 0) \<midarrow>(0::'a)\<rightarrow> (0::real)" 
56167  714 
by (rule tendsto_const) 
61976  715 
have "(\<lambda>h. K * norm h) \<midarrow>(0::'a)\<rightarrow> K * norm (0::'a)" 
56167  716 
by (intro tendsto_intros) 
61976  717 
then show "(\<lambda>h. K * norm h) \<midarrow>(0::'a)\<rightarrow> 0" 
56167  718 
by simp 
20860  719 
qed 
720 
qed 

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

721 

15229  722 
lemma lemma_termdiff5: 
56167  723 
fixes g :: "'a::real_normed_vector \<Rightarrow> nat \<Rightarrow> 'b::banach" 
63558  724 
and k :: real 
725 
assumes k: "0 < k" 

726 
and f: "summable f" 

727 
and le: "\<And>h n. h \<noteq> 0 \<Longrightarrow> norm h < k \<Longrightarrow> norm (g h n) \<le> f n * norm h" 

61976  728 
shows "(\<lambda>h. suminf (g h)) \<midarrow>0\<rightarrow> 0" 
20860  729 
proof (rule lemma_termdiff4 [OF k]) 
63558  730 
fix h :: 'a 
53079  731 
assume "h \<noteq> 0" and "norm h < k" 
63558  732 
then have 1: "\<forall>n. norm (g h n) \<le> f n * norm h" 
20860  733 
by (simp add: le) 
63558  734 
then have "\<exists>N. \<forall>n\<ge>N. norm (norm (g h n)) \<le> f n * norm h" 
20860  735 
by simp 
63558  736 
moreover from f have 2: "summable (\<lambda>n. f n * norm h)" 
20860  737 
by (rule summable_mult2) 
63558  738 
ultimately have 3: "summable (\<lambda>n. norm (g h n))" 
20860  739 
by (rule summable_comparison_test) 
63558  740 
then have "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))" 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

741 
by (rule summable_norm) 
63558  742 
also from 1 3 2 have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)" 
56213  743 
by (rule suminf_le) 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

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

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

748 

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

749 

63558  750 
(* FIXME: Long proofs *) 
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset

751 

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

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

754 
assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)" 
53079  755 
and 2: "norm x < norm K" 
63558  756 
shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n  x^n) / h  of_nat n * x ^ (n  Suc 0))) \<midarrow>0\<rightarrow> 0" 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

757 
proof  
63558  758 
from dense [OF 2] obtain r where r1: "norm x < r" and r2: "r < norm K" 
759 
by fast 

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

760 
from norm_ge_zero r1 have r: "0 < r" 
20860  761 
by (rule order_le_less_trans) 
63558  762 
then have r_neq_0: "r \<noteq> 0" by simp 
20860  763 
show ?thesis 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

764 
proof (rule lemma_termdiff5) 
63558  765 
show "0 < r  norm x" 
766 
using r1 by simp 

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

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

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

769 
with 1 have "summable (\<lambda>n. norm (diffs (diffs c) n * (of_real r ^ n)))" 
20860  770 
by (rule powser_insidea) 
63558  771 
then have "summable (\<lambda>n. diffs (diffs (\<lambda>n. norm (c n))) n * r ^ n)" 
772 
using r by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc) 

773 
then have "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n  Suc 0))" 

20860  774 
by (rule diffs_equiv [THEN sums_summable]) 
53079  775 
also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n  Suc 0)) = 
776 
(\<lambda>n. diffs (\<lambda>m. of_nat (m  Suc 0) * norm (c m) * inverse r) n * (r ^ n))" 

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

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

778 
apply (simp add: diffs_def) 
63558  779 
apply (case_tac n) 
780 
apply (simp_all add: r_neq_0) 

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

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

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

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

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

788 
apply (rule ext) 
63558  789 
apply (case_tac n) 
790 
apply simp 

55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
54576
diff
changeset

791 
apply (rename_tac nat) 
63558  792 
apply (case_tac nat) 
793 
apply simp 

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

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

795 
done 
63558  796 
finally show "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n  Suc 0) * r ^ (n  2))" . 
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset

797 
next 
63558  798 
fix h :: 'a 
799 
fix n :: nat 

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

801 
assume "norm h < r  norm x" 
63558  802 
then have "norm x + norm h < r" by simp 
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset

803 
with norm_triangle_ineq have xh: "norm (x + h) < r" 
20860  804 
by (rule order_le_less_trans) 
63558  805 
show "norm (c n * (((x + h) ^ n  x^n) / h  of_nat n * x ^ (n  Suc 0))) \<le> 
806 
norm (c n) * of_nat n * of_nat (n  Suc 0) * r ^ (n  2) * norm h" 

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

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

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

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

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

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

814 

20860  815 
lemma termdiffs: 
31017  816 
fixes K x :: "'a::{real_normed_field,banach}" 
20860  817 
assumes 1: "summable (\<lambda>n. c n * K ^ n)" 
63558  818 
and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)" 
819 
and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)" 

820 
and 4: "norm x < norm K" 

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

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

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

824 
show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n)  suminf (\<lambda>n. c n * x^n)) / h 
61976  825 
 suminf (\<lambda>n. diffs c n * x^n)) \<midarrow>0\<rightarrow> 0" 
20860  826 
proof (rule LIM_equal2) 
63558  827 
show "0 < norm K  norm x" 
828 
using 4 by (simp add: less_diff_eq) 

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

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

831 
assume "norm (h  0) < norm K  norm x" 
63558  832 
then have "norm x + norm h < norm K" by simp 
833 
then have 5: "norm (x + h) < norm K" 

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

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

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

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

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

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

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

843 
(\<Sum>n. c n * (((x + h) ^ n  x^n) / h  of_nat n * x ^ (n  Suc 0)))" 
54575  844 
by (simp add: algebra_simps) 
20860  845 
next 
61976  846 
show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n  x^n) / h  of_nat n * x ^ (n  Suc 0))) \<midarrow>0\<rightarrow> 0" 
53079  847 
by (rule termdiffs_aux [OF 3 4]) 
20860  848 
qed 
849 
qed 

850 

60758  851 
subsection \<open>The Derivative of a Power Series Has the Same Radius of Convergence\<close> 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

852 

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

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

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

855 
assumes K: "norm x < K" 
63558  856 
and sm: "\<And>x. norm x < K \<Longrightarrow> summable(\<lambda>n. c n * x ^ n)" 
857 
shows "summable (\<lambda>n. diffs c n * x ^ n)" 

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

858 
proof (cases "x = 0") 
63558  859 
case True 
860 
then show ?thesis 

861 
using powser_sums_zero sums_summable by auto 

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

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

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

865 
using K less_trans zero_less_norm_iff by blast 
63558  866 
then obtain r :: real where r: "norm x < norm r" "norm r < K" "r > 0" 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

867 
using K False 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

868 
by (auto simp: field_simps abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"]) 
61969  869 
have "(\<lambda>n. of_nat n * (x / of_real r) ^ n) \<longlonglongrightarrow> 0" 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

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

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

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

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

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

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

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

877 
apply (rule summable_comparison_test' [of "\<lambda>n. norm(c n * (of_real r) ^ n)" N]) 
63558  878 
apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]]) 
879 
using N r norm_of_real [of "r + K", where 'a = 'a] 

880 
apply (auto simp add: norm_divide norm_mult norm_power field_simps) 

881 
apply (fastforce simp: less_eq_real_def) 

882 
done 

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

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

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

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

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

887 
using False summable_mult2 [of "\<lambda>n. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"] 
60867  888 
by (simp add: mult.assoc) (auto simp: ac_simps) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

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

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

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

892 

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

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

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

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

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

898 
using assms 
63558  899 
apply auto 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

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

901 

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

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

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

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

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

907 
proof  
60762  908 
have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K" 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

909 
using K 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

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

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

913 
done 
60762  914 
then have [simp]: "norm ((of_real (norm K) + of_real (norm x)) :: 'a) < norm K * 2" 
915 
by simp 

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

916 
have "summable (\<lambda>n. c n * (of_real (norm x + norm K) / 2) ^ n)" 
60762  917 
by (metis K2 summable_norm_cancel [OF powser_insidea [OF sm]] add.commute of_real_add) 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
60036
diff
changeset

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

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

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

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

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

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

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

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

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

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

929 

61552
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

930 
lemma termdiffs_strong_converges_everywhere: 
63558  931 
fixes K x :: "'a::{real_normed_field,banach}" 
61552
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

932 
assumes "\<And>y. summable (\<lambda>n. c n * y ^ n)" 
63558  933 
shows "((\<lambda>x. \<Sum>n. c n * x^n) has_field_derivative (\<Sum>n. diffs c n * x^n)) (at x)" 
61552
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

934 
using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x] 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

935 
by (force simp del: of_real_add) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

936 

63721  937 
lemma termdiffs_strong': 
938 
fixes z :: "'a :: {real_normed_field,banach}" 

939 
assumes "\<And>z. norm z < K \<Longrightarrow> summable (\<lambda>n. c n * z ^ n)" 

940 
assumes "norm z < K" 

941 
shows "((\<lambda>z. \<Sum>n. c n * z^n) has_field_derivative (\<Sum>n. diffs c n * z^n)) (at z)" 

942 
proof (rule termdiffs_strong) 

943 
define L :: real where "L = (norm z + K) / 2" 

944 
have "0 \<le> norm z" by simp 

945 
also note \<open>norm z < K\<close> 

946 
finally have K: "K \<ge> 0" by simp 

947 
from assms K have L: "L \<ge> 0" "norm z < L" "L < K" by (simp_all add: L_def) 

948 
from L show "norm z < norm (of_real L :: 'a)" by simp 

949 
from L show "summable (\<lambda>n. c n * of_real L ^ n)" by (intro assms(1)) simp_all 

950 
qed 

951 

952 
lemma termdiffs_sums_strong: 

953 
fixes z :: "'a :: {banach,real_normed_field}" 

954 
assumes sums: "\<And>z. norm z < K \<Longrightarrow> (\<lambda>n. c n * z ^ n) sums f z" 

955 
assumes deriv: "(f has_field_derivative f') (at z)" 

956 
assumes norm: "norm z < K" 

957 
shows "(\<lambda>n. diffs c n * z ^ n) sums f'" 

958 
proof  

959 
have summable: "summable (\<lambda>n. diffs c n * z^n)" 

960 
by (intro termdiff_converges[OF norm] sums_summable[OF sums]) 

961 
from norm have "eventually (\<lambda>z. z \<in> norm ` {..<K}) (nhds z)" 

962 
by (intro eventually_nhds_in_open open_vimage) 

963 
(simp_all add: continuous_on_norm continuous_on_id) 

964 
hence eq: "eventually (\<lambda>z. (\<Sum>n. c n * z^n) = f z) (nhds z)" 

965 
by eventually_elim (insert sums, simp add: sums_iff) 

966 

967 
have "((\<lambda>z. \<Sum>n. c n * z^n) has_field_derivative (\<Sum>n. diffs c n * z^n)) (at z)" 

968 
by (intro termdiffs_strong'[OF _ norm] sums_summable[OF sums]) 

969 
hence "(f has_field_derivative (\<Sum>n. diffs c n * z^n)) (at z)" 

970 
by (subst (asm) DERIV_cong_ev[OF refl eq refl]) 

971 
from this and deriv have "(\<Sum>n. diffs c n * z^n) = f'" by (rule DERIV_unique) 

972 
with summable show ?thesis by (simp add: sums_iff) 

973 
qed 

974 

61552
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

975 
lemma isCont_powser: 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

976 
fixes K x :: "'a::{real_normed_field,banach}" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

977 
assumes "summable (\<lambda>n. c n * K ^ n)" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

978 
assumes "norm x < norm K" 
63558  979 
shows "isCont (\<lambda>x. \<Sum>n. c n * x^n) x" 
61552
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

980 
using termdiffs_strong[OF assms] by (blast intro!: DERIV_isCont) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

981 

61552
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

982 
lemmas isCont_powser' = isCont_o2[OF _ isCont_powser] 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

983 

980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

984 
lemma isCont_powser_converges_everywhere: 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

985 
fixes K x :: "'a::{real_normed_field,banach}" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

986 
assumes "\<And>y. summable (\<lambda>n. c n * y ^ n)" 
63558  987 
shows "isCont (\<lambda>x. \<Sum>n. c n * x^n) x" 
61552
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

988 
using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x] 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

989 
by (force intro!: DERIV_isCont simp del: of_real_add) 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

990 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

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

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

993 
assumes s: "0 < s" 
63558  994 
and sm: "\<And>x. norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)" 
995 
shows "(f \<longlongrightarrow> a 0) (at 0)" 

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

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

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

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

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

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

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

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

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

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

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

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

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

1008 
by (blast intro: DERIV_continuous) 
61973  1009 
then have "((\<lambda>x. \<Sum>n. a n * x ^ n) \<longlongrightarrow> a 0) (at 0)" 
63558  1010 
by (simp add: continuous_within) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

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

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

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

1014 
apply (rule_tac x="s" in exI) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

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

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

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

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

1019 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

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

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

1022 
assumes s: "0 < s" 
63558  1023 
and sm: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)" 
1024 
shows "(f \<longlongrightarrow> a 0) (at 0)" 

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

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

1027 
apply (rule powser_limit_0 [OF s]) 
63558  1028 
apply (case_tac "x = 0") 
1029 
apply (auto simp add: powser_sums_zero sm) 

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

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

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

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

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

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

1036 

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

1037 

60758  1038 
subsection \<open>Derivability of power series\<close> 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1039 

53079  1040 
lemma DERIV_series': 
1041 
fixes f :: "real \<Rightarrow> nat \<Rightarrow> real" 

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

1042 
assumes DERIV_f: "\<And> n. DERIV (\<lambda> x. f x n) x0 :> (f' x0 n)" 
63558  1043 
and allf_summable: "\<And> x. x \<in> {a <..< b} \<Longrightarrow> summable (f x)" 
1044 
and x0_in_I: "x0 \<in> {a <..< b}" 

53079  1045 
and "summable (f' x0)" 
1046 
and "summable L" 

63558  1047 
and L_def: "\<And>n x y. x \<in> {a <..< b} \<Longrightarrow> y \<in> {a <..< b} \<Longrightarrow> \<bar>f x n  f y n\<bar> \<le> L n * \<bar>x  y\<bar>" 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

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

1050 
proof (rule LIM_I) 
53079  1051 
fix r :: real 
63558  1052 
assume "0 < r" then have "0 < r/3" by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1053 

41970  1054 
obtain N_L where N_L: "\<And> n. N_L \<le> n \<Longrightarrow> \<bar> \<Sum> i. L (i + n) \<bar> < r/3" 
60758  1055 
using suminf_exist_split[OF \<open>0 < r/3\<close> \<open>summable L\<close>] by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1056 

41970  1057 
obtain N_f' where N_f': "\<And> n. N_f' \<le> n \<Longrightarrow> \<bar> \<Sum> i. f' x0 (i + n) \<bar> < r/3" 
60758  1058 
using suminf_exist_split[OF \<open>0 < r/3\<close> \<open>summable (f' x0)\<close>] by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1059 

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

1060 
let ?N = "Suc (max N_L N_f')" 
63558  1061 
have "\<bar> \<Sum> i. f' x0 (i + ?N) \<bar> < r/3" (is "?f'_part < r/3") 
1062 
and L_estimate: "\<bar> \<Sum> i. L (i + ?N) \<bar> < r/3" 

1063 
using N_L[of "?N"] and N_f' [of "?N"] by auto 

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

1064 

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

1066 

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

1067 
let ?r = "r / (3 * real ?N)" 
60758  1068 
from \<open>0 < r\<close> have "0 < ?r" by simp 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1069 

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

1070 
let ?s = "\<lambda>n. SOME s. 0 < s \<and> (\<forall> x. x \<noteq> 0 \<and> \<bar> x \<bar> < s \<longrightarrow> \<bar> ?diff n x  f' x0 n \<bar> < ?r)" 
63040  1071 
define S' where "S' = Min (?s ` {..< ?N })" 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1072 

63558  1073 
have "0 < S'" 
1074 
unfolding S'_def 

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

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

1076 
show "\<forall>x \<in> (?s ` {..< ?N }). 0 < x" 
53079  1077 
proof 
1078 
fix x 

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

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

1080 
then obtain n where "x = ?s n" and "n \<in> {..<?N}" 
53079  1081 
using image_iff[THEN iffD1] by blast 
60758  1082 
from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF \<open>0 < ?r\<close>, unfolded real_norm_def] 
53079  1083 
obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x  f' x0 n\<bar> < ?r)" 
1084 
by auto 

63558  1085 
have "0 < ?s n" 
1086 
by (rule someI2[where a=s]) (auto simp add: s_bound simp del: of_nat_Suc) 

1087 
then show "0 < x" by (simp only: \<open>x = ?s n\<close>) 

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

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

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

1090 

63040  1091 
define S where "S = min (min (x0  a) (b  x0)) S'" 
63558  1092 
then have "0 < S" and S_a: "S \<le> x0  a" and S_b: "S \<le> b  x0" 
60758  1093 
and "S \<le> S'" using x0_in_I and \<open>0 < S'\<close> 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

1095 

63558  1096 
have "\<bar>(suminf (f (x0 + x))  suminf (f x0)) / x  suminf (f' x0)\<bar> < r" 
1097 
if "x \<noteq> 0" and "\<bar>x\<bar> < S" for x 

1098 
proof  

1099 
from that have x_in_I: "x0 + x \<in> {a <..< b}" 

53079  1100 
using S_a S_b by auto 
41970  1101 

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

1102 
note diff_smbl = summable_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1103 
note div_smbl = summable_divide[OF diff_smbl] 
60758  1104 
note all_smbl = summable_diff[OF div_smbl \<open>summable (f' x0)\<close>] 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1105 
note ign = summable_ignore_initial_segment[where k="?N"] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1106 
note diff_shft_smbl = summable_diff[OF ign[OF allf_summable[OF x_in_I]] ign[OF allf_summable[OF x0_in_I]]] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1107 
note div_shft_smbl = summable_divide[OF diff_shft_smbl] 
60758  1108 
note all_shft_smbl = summable_diff[OF div_smbl ign[OF \<open>summable (f' x0)\<close>]] 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1109 

63558  1110 
have 1: "\<bar>(\<bar>?diff (n + ?N) x\<bar>)\<bar> \<le> L (n + ?N)" for n 
1111 
proof  

1112 
have "\<bar>?diff (n + ?N) x\<bar> \<le> L (n + ?N) * \<bar>(x0 + x)  x0\<bar> / \<bar>x\<bar>" 

53079  1113 
using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero] 
63558  1114 
by (simp only: abs_divide) 
1115 
with \<open>x \<noteq> 0\<close> show ?thesis by auto 

1116 
qed 

1117 
note 2 = summable_rabs_comparison_test[OF _ ign[OF \<open>summable L\<close>]] 

1118 
from 1 have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))" 

1119 
by (metis (lifting) abs_idempotent 

1120 
order_trans[OF summable_rabs[OF 2] suminf_le[OF _ 2 ign[OF \<open>summable L\<close>]]]) 

1121 
then have "\<bar>\<Sum>i. ?diff (i + ?N) x\<bar> \<le> r / 3" (is "?L_part \<le> r/3") 

53079  1122 
using L_estimate by auto 
1123 

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

1125 
also have "\<dots> < (\<Sum>n<?N. ?r)" 
64267  1126 
proof (rule sum_strict_mono) 
53079  1127 
fix n 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

1128 
assume "n \<in> {..< ?N}" 
60758  1129 
have "\<bar>x\<bar> < S" using \<open>\<bar>x\<bar> < S\<close> . 
1130 
also have "S \<le> S'" using \<open>S \<le> S'\<close> . 

63558  1131 
also have "S' \<le> ?s n" 
1132 
unfolding S'_def 

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

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

1134 
have "?s n \<in> (?s ` {..<?N}) \<and> ?s n \<le> ?s n" 
60758  1135 
using \<open>n \<in> {..< ?N}\<close> by auto 
63558  1136 
then show "\<exists> a \<in> (?s ` {..<?N}). a \<le> ?s n" 
1137 
by blast 

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

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

1140 

63558  1141 
from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF \<open>0 < ?r\<close>, 
1142 
unfolded real_norm_def diff_0_right, unfolded some_eq_ex[symmetric], THEN conjunct2] 

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

1143 
have "\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < ?s n \<longrightarrow> \<bar>?diff n x  f' x0 n\<bar> < ?r" . 
60758  1144 
with \<open>x \<noteq> 0\<close> and \<open>\<bar>x\<bar> < ?s n\<close> show "\<bar>?diff n x  f' x0 n\<bar> < ?r" 
53079  1145 
by blast 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

1147 
also have "\<dots> = of_nat (card {..<?N}) * ?r" 
64267  1148 
by (rule sum_constant) 
63558  1149 
also have "\<dots> = real ?N * ?r" 
1150 
by simp 

1151 
also have "\<dots> = r/3" 

1152 
by (auto simp del: of_nat_Suc) 

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

1153 
finally have "\<bar>\<Sum>n<?N. ?diff n x  f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") . 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1154 

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

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

60758  1158 
unfolding suminf_diff[OF div_smbl \<open>summable (f' x0)\<close>, symmetric] 
53079  1159 
using suminf_divide[OF diff_smbl, symmetric] by auto 
63558  1160 
also have "\<dots> \<le> ?diff_part + \<bar>(\<Sum>n. ?diff (n + ?N) x)  (\<Sum> n. f' x0 (n + ?N))\<bar>" 
53079  1161 
unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"] 
60758  1162 
unfolding suminf_diff[OF div_shft_smbl ign[OF \<open>summable (f' x0)\<close>]] 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

1163 
apply (subst (5) add.commute) 
63558  1164 
apply (rule abs_triangle_ineq) 
1165 
done 

53079  1166 
also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part" 
1167 
using abs_triangle_ineq4 by auto 

41970  1168 
also have "\<dots> < r /3 + r/3 + r/3" 
60758  1169 
using \<open>?diff_part < r/3\<close> \<open>?L_part \<le> r/3\<close> and \<open>?f'_part < r/3\<close> 
36842  1170 
by (rule add_strict_mono [OF add_less_le_mono]) 
63558  1171 
finally show ?thesis 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

1172 
by auto 
63558  1173 
qed 
1174 
then show "\<exists>s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x  0) < s \<longrightarrow> 

53079  1175 
norm (((\<Sum>n. f (x0 + x) n)  (\<Sum>n. f x0 n)) / x  (\<Sum>n. f' x0 n)) < r" 
63558  1176 
using \<open>0 < S\<close> by auto 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset

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

1178 

53079  1179 
lemma DERIV_power_series': 
1180 
fixes f :: "nat \<Rightarrow> real" 

63558  1181 
assumes converges: "\<And>x. x \<in> {R <..< R} \<Longrightarrow> summable (\<lambda>n. f n * real (Suc n) * x^n)" 
1182 
and x0_in_I: "x0 \<in> {R <..< R}" 

1183 
and "0 < R" 

1184 
shows "DERIV (\<lambda>x. (\<Sum>n. f n * x^(Suc n))) x0 :> (\<Sum>n. f n * real (Suc n) * x0^n)" 

1185 
(is "DERIV (\<lambda>x. suminf (?f x)) x0 :> suminf (?f' x0)") 
