author | noschinl |
Sat, 25 May 2013 13:59:08 +0200 | |
changeset 52139 | 40fe6b80b481 |
parent 51641 | cd05e9fcc63d |
child 53015 | a1119cf551e8 |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
1 |
(* Title: HOL/Transcendental.thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
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 tab-width;
wenzelm
parents:
32047
diff
changeset
|
3 |
Author: Lawrence C Paulson |
51527 | 4 |
Author: Jeremy Avigad |
5 |
||
12196 | 6 |
*) |
7 |
||
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
8 |
header{*Power Series, Transcendental Functions etc.*} |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
9 |
|
15131 | 10 |
theory Transcendental |
25600 | 11 |
imports Fact Series Deriv NthRoot |
15131 | 12 |
begin |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
13 |
|
29164 | 14 |
subsection {* Properties of Power Series *} |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
15 |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
16 |
lemma lemma_realpow_diff: |
31017 | 17 |
fixes y :: "'a::monoid_mult" |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
18 |
shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
19 |
proof - |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
20 |
assume "p \<le> n" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
21 |
hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le) |
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30082
diff
changeset
|
22 |
thus ?thesis by (simp add: power_commutes) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
23 |
qed |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
24 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
25 |
lemma lemma_realpow_diff_sumr: |
31017 | 26 |
fixes y :: "'a::{comm_semiring_0,monoid_mult}" shows |
41970 | 27 |
"(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) = |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
28 |
y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))" |
29163 | 29 |
by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac |
33549 | 30 |
del: setsum_op_ivl_Suc) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
31 |
|
15229 | 32 |
lemma lemma_realpow_diff_sumr2: |
31017 | 33 |
fixes y :: "'a::{comm_ring,monoid_mult}" shows |
41970 | 34 |
"x ^ (Suc n) - y ^ (Suc n) = |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
35 |
(x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))" |
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30082
diff
changeset
|
36 |
apply (induct n, simp) |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30082
diff
changeset
|
37 |
apply (simp del: setsum_op_ivl_Suc) |
15561 | 38 |
apply (subst setsum_op_ivl_Suc) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
39 |
apply (subst lemma_realpow_diff_sumr) |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47489
diff
changeset
|
40 |
apply (simp add: distrib_left del: setsum_op_ivl_Suc) |
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
33667
diff
changeset
|
41 |
apply (subst mult_left_commute [of "x - y"]) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
42 |
apply (erule subst) |
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30082
diff
changeset
|
43 |
apply (simp add: algebra_simps) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
44 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
45 |
|
15229 | 46 |
lemma lemma_realpow_rev_sumr: |
41970 | 47 |
"(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) = |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
48 |
(\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
49 |
apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"]) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
50 |
apply (rule inj_onI, simp) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
51 |
apply auto |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
52 |
apply (rule_tac x="n - x" in image_eqI, simp, simp) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
53 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
54 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
55 |
text{*Power series has a `circle` of convergence, i.e. if it sums for @{term |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
56 |
x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*} |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
57 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
58 |
lemma powser_insidea: |
44726 | 59 |
fixes x z :: "'a::real_normed_field" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
60 |
assumes 1: "summable (\<lambda>n. f n * x ^ n)" |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
61 |
assumes 2: "norm z < norm x" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
62 |
shows "summable (\<lambda>n. norm (f n * z ^ n))" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
63 |
proof - |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
64 |
from 2 have x_neq_0: "x \<noteq> 0" by clarsimp |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
65 |
from 1 have "(\<lambda>n. f n * x ^ n) ----> 0" |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
66 |
by (rule summable_LIMSEQ_zero) |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
67 |
hence "convergent (\<lambda>n. f n * x ^ n)" |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
68 |
by (rule convergentI) |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
69 |
hence "Cauchy (\<lambda>n. f n * x ^ n)" |
44726 | 70 |
by (rule convergent_Cauchy) |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
71 |
hence "Bseq (\<lambda>n. f n * x ^ n)" |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
72 |
by (rule Cauchy_Bseq) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
73 |
then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
74 |
by (simp add: Bseq_def, safe) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
75 |
have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le> |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
76 |
K * norm (z ^ n) * inverse (norm (x ^ n))" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
77 |
proof (intro exI allI impI) |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
78 |
fix n::nat assume "0 \<le> n" |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
79 |
have "norm (norm (f n * z ^ n)) * norm (x ^ n) = |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
80 |
norm (f n * x ^ n) * norm (z ^ n)" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
81 |
by (simp add: norm_mult abs_mult) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
82 |
also have "\<dots> \<le> K * norm (z ^ n)" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
83 |
by (simp only: mult_right_mono 4 norm_ge_zero) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
84 |
also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
85 |
by (simp add: x_neq_0) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
86 |
also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
87 |
by (simp only: mult_assoc) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
88 |
finally show "norm (norm (f n * z ^ n)) \<le> |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
89 |
K * norm (z ^ n) * inverse (norm (x ^ n))" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
90 |
by (simp add: mult_le_cancel_right x_neq_0) |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
91 |
qed |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
92 |
moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
93 |
proof - |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
94 |
from 2 have "norm (norm (z * inverse x)) < 1" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
95 |
using x_neq_0 |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
96 |
by (simp add: nonzero_norm_divide divide_inverse [symmetric]) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
97 |
hence "summable (\<lambda>n. norm (z * inverse x) ^ n)" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
98 |
by (rule summable_geometric) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
99 |
hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
100 |
by (rule summable_mult) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
101 |
thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
102 |
using x_neq_0 |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
103 |
by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
104 |
power_inverse norm_power mult_assoc) |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
105 |
qed |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
106 |
ultimately show "summable (\<lambda>n. norm (f n * z ^ n))" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
107 |
by (rule summable_comparison_test) |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
108 |
qed |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
109 |
|
15229 | 110 |
lemma powser_inside: |
31017 | 111 |
fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" shows |
41970 | 112 |
"[| summable (%n. f(n) * (x ^ n)); norm z < norm x |] |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
113 |
==> summable (%n. f(n) * (z ^ n))" |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
114 |
by (rule powser_insidea [THEN summable_norm_cancel]) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
115 |
|
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
116 |
lemma sum_split_even_odd: fixes f :: "nat \<Rightarrow> real" shows |
41970 | 117 |
"(\<Sum> i = 0 ..< 2 * n. if even i then f i else g i) = |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
118 |
(\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1))" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
119 |
proof (induct n) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
120 |
case (Suc n) |
41970 | 121 |
have "(\<Sum> i = 0 ..< 2 * Suc n. if even i then f i else g i) = |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
122 |
(\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< 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
|
123 |
using Suc.hyps unfolding One_nat_def by auto |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
124 |
also have "\<dots> = (\<Sum> i = 0 ..< Suc n. f (2 * i)) + (\<Sum> i = 0 ..< Suc n. g (2 * i + 1))" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
125 |
finally show ?case . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
126 |
qed auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
127 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
128 |
lemma sums_if': fixes g :: "nat \<Rightarrow> real" assumes "g sums x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
129 |
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
|
130 |
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
|
131 |
proof (rule LIMSEQ_I) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
132 |
fix r :: real assume "0 < r" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
133 |
from `g sums x`[unfolded sums_def, THEN LIMSEQ_D, OF this] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
134 |
obtain no where no_eq: "\<And> n. n \<ge> no \<Longrightarrow> (norm (setsum g { 0..<n } - x) < r)" by blast |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
135 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
136 |
let ?SUM = "\<lambda> m. \<Sum> i = 0 ..< m. if even i then 0 else g ((i - 1) div 2)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
137 |
{ fix m assume "m \<ge> 2 * no" hence "m div 2 \<ge> no" by auto |
41970 | 138 |
have sum_eq: "?SUM (2 * (m div 2)) = setsum g { 0 ..< 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
|
139 |
using sum_split_even_odd by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
140 |
hence "(norm (?SUM (2 * (m div 2)) - x) < r)" using no_eq unfolding sum_eq using `m div 2 \<ge> no` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
141 |
moreover |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
142 |
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
|
143 |
proof (cases "even m") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
144 |
case True show ?thesis unfolding even_nat_div_two_times_two[OF True, unfolded numeral_2_eq_2[symmetric]] .. |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
145 |
next |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
146 |
case False hence "even (Suc m)" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
147 |
from even_nat_div_two_times_two[OF this, unfolded numeral_2_eq_2[symmetric]] odd_nat_plus_one_div_two[OF False, unfolded numeral_2_eq_2[symmetric]] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
148 |
have eq: "Suc (2 * (m div 2)) = m" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
149 |
hence "even (2 * (m div 2))" using `odd m` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
150 |
have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq .. |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
151 |
also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
152 |
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
|
153 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
154 |
ultimately have "(norm (?SUM m - x) < r)" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
155 |
} |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
156 |
thus "\<exists> no. \<forall> m \<ge> no. norm (?SUM m - x) < r" by blast |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
157 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
158 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
159 |
lemma sums_if: fixes g :: "nat \<Rightarrow> real" assumes "g sums x" and "f sums y" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
160 |
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
|
161 |
proof - |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
162 |
let ?s = "\<lambda> n. if even n then 0 else f ((n - 1) div 2)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
163 |
{ fix B T E have "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
164 |
by (cases B) auto } note if_sum = this |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
165 |
have g_sums: "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x" using sums_if'[OF `g sums x`] . |
41970 | 166 |
{ |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
167 |
have "?s 0 = 0" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
168 |
have Suc_m1: "\<And> n. Suc n - 1 = n" by auto |
41550 | 169 |
have if_eq: "\<And>B T E. (if \<not> B then T else E) = (if B then E else T)" by auto |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
170 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
171 |
have "?s sums y" using sums_if'[OF `f sums y`] . |
41970 | 172 |
from this[unfolded sums_def, THEN LIMSEQ_Suc] |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
173 |
have "(\<lambda> n. if even n then f (n div 2) else 0) sums y" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
174 |
unfolding sums_def setsum_shift_lb_Suc0_0_upt[where f="?s", OF `?s 0 = 0`, symmetric] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
175 |
image_Suc_atLeastLessThan[symmetric] setsum_reindex[OF inj_Suc, unfolded comp_def] |
31148 | 176 |
even_Suc Suc_m1 if_eq . |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
177 |
} from sums_add[OF g_sums this] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
178 |
show ?thesis unfolding if_sum . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
179 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
180 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
181 |
subsection {* Alternating series test / Leibniz formula *} |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
182 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
183 |
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
|
184 |
fixes a :: "nat \<Rightarrow> real" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
185 |
assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0" |
41970 | 186 |
shows "\<exists>l. ((\<forall>n. (\<Sum>i=0..<2*n. -1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i=0..<2*n. -1^i*a i) ----> l) \<and> |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
187 |
((\<forall>n. l \<le> (\<Sum>i=0..<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i=0..<2*n + 1. -1^i*a i) ----> l)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
188 |
(is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
189 |
proof - |
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset
|
190 |
have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
191 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
192 |
have "\<forall> n. ?f n \<le> ?f (Suc n)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
193 |
proof fix n show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
194 |
moreover |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
195 |
have "\<forall> n. ?g (Suc n) \<le> ?g n" |
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset
|
196 |
proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"] |
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset
|
197 |
unfolding One_nat_def by auto qed |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
198 |
moreover |
41970 | 199 |
have "\<forall> n. ?f n \<le> ?g n" |
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset
|
200 |
proof fix n show "?f n \<le> ?g n" using fg_diff a_pos |
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset
|
201 |
unfolding One_nat_def by auto qed |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
202 |
moreover |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
203 |
have "(\<lambda> n. ?f n - ?g n) ----> 0" unfolding fg_diff |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
204 |
proof (rule LIMSEQ_I) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
205 |
fix r :: real assume "0 < r" |
41970 | 206 |
with `a ----> 0`[THEN LIMSEQ_D] |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
207 |
obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n - 0) < r" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
208 |
hence "\<forall> n \<ge> N. norm (- a (2 * n) - 0) < r" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
209 |
thus "\<exists> N. \<forall> n \<ge> N. norm (- a (2 * n) - 0) < r" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
210 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
211 |
ultimately |
51477
2990382dc066
clean up lemma_nest_unique and renamed to nested_sequence_unique
hoelzl
parents:
50347
diff
changeset
|
212 |
show ?thesis by (rule nested_sequence_unique) |
41970 | 213 |
qed |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
214 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
215 |
lemma summable_Leibniz': fixes a :: "nat \<Rightarrow> real" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
216 |
assumes a_zero: "a ----> 0" and a_pos: "\<And> n. 0 \<le> a n" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
217 |
and a_monotone: "\<And> n. a (Suc n) \<le> a n" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
218 |
shows summable: "summable (\<lambda> n. (-1)^n * a n)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
219 |
and "\<And>n. (\<Sum>i=0..<2*n. (-1)^i*a i) \<le> (\<Sum>i. (-1)^i*a i)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
220 |
and "(\<lambda>n. \<Sum>i=0..<2*n. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
221 |
and "\<And>n. (\<Sum>i. (-1)^i*a i) \<le> (\<Sum>i=0..<2*n+1. (-1)^i*a i)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
222 |
and "(\<lambda>n. \<Sum>i=0..<2*n+1. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
223 |
proof - |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
224 |
let "?S n" = "(-1)^n * a n" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
225 |
let "?P n" = "\<Sum>i=0..<n. ?S i" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
226 |
let "?f n" = "?P (2 * n)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
227 |
let "?g n" = "?P (2 * n + 1)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
228 |
obtain l :: real where below_l: "\<forall> n. ?f n \<le> l" and "?f ----> l" and above_l: "\<forall> n. l \<le> ?g n" and "?g ----> l" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
229 |
using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast |
41970 | 230 |
|
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
231 |
let ?Sa = "\<lambda> m. \<Sum> n = 0..<m. ?S n" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
232 |
have "?Sa ----> l" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
233 |
proof (rule LIMSEQ_I) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
234 |
fix r :: real assume "0 < r" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
235 |
|
41970 | 236 |
with `?f ----> l`[THEN LIMSEQ_D] |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
237 |
obtain f_no where f: "\<And> n. n \<ge> f_no \<Longrightarrow> norm (?f n - l) < r" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
238 |
|
41970 | 239 |
from `0 < r` `?g ----> l`[THEN LIMSEQ_D] |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
240 |
obtain g_no where g: "\<And> n. n \<ge> g_no \<Longrightarrow> norm (?g n - l) < r" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
241 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
242 |
{ fix n :: nat |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
243 |
assume "n \<ge> (max (2 * f_no) (2 * g_no))" hence "n \<ge> 2 * f_no" and "n \<ge> 2 * g_no" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
244 |
have "norm (?Sa n - l) < r" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
245 |
proof (cases "even n") |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
246 |
case True from even_nat_div_two_times_two[OF this] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
247 |
have n_eq: "2 * (n div 2) = n" unfolding numeral_2_eq_2[symmetric] by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
248 |
with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no" by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
249 |
from f[OF this] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
250 |
show ?thesis 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
|
251 |
next |
35213 | 252 |
case False hence "even (n - 1)" by simp |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
253 |
from even_nat_div_two_times_two[OF this] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
254 |
have n_eq: "2 * ((n - 1) div 2) = n - 1" unfolding numeral_2_eq_2[symmetric] by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
255 |
hence range_eq: "n - 1 + 1 = n" using odd_pos[OF False] by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
256 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
257 |
from n_eq `n \<ge> 2 * g_no` have "(n - 1) div 2 \<ge> g_no" by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
258 |
from g[OF this] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
259 |
show ?thesis unfolding n_eq atLeastLessThanSuc_atLeastAtMost 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
|
260 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
261 |
} |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
262 |
thus "\<exists> no. \<forall> n \<ge> no. norm (?Sa n - l) < r" by blast |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
263 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
264 |
hence sums_l: "(\<lambda>i. (-1)^i * a i) sums l" unfolding sums_def atLeastLessThanSuc_atLeastAtMost[symmetric] . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
265 |
thus "summable ?S" using summable_def by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
266 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
267 |
have "l = suminf ?S" using sums_unique[OF sums_l] . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
268 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
269 |
{ fix n show "suminf ?S \<le> ?g n" unfolding sums_unique[OF sums_l, symmetric] using above_l by auto } |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
270 |
{ fix n show "?f n \<le> suminf ?S" unfolding sums_unique[OF sums_l, symmetric] using below_l by auto } |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
271 |
show "?g ----> suminf ?S" using `?g ----> l` `l = suminf ?S` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
272 |
show "?f ----> suminf ?S" using `?f ----> l` `l = suminf ?S` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
273 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
274 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
275 |
theorem summable_Leibniz: fixes a :: "nat \<Rightarrow> real" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
276 |
assumes a_zero: "a ----> 0" and "monoseq a" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
277 |
shows "summable (\<lambda> n. (-1)^n * a n)" (is "?summable") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
278 |
and "0 < a 0 \<longrightarrow> (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i=0..<2*n. -1^i * a i .. \<Sum>i=0..<2*n+1. -1^i * a i})" (is "?pos") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
279 |
and "a 0 < 0 \<longrightarrow> (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i=0..<2*n+1. -1^i * a i .. \<Sum>i=0..<2*n. -1^i * a i})" (is "?neg") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
280 |
and "(\<lambda>n. \<Sum>i=0..<2*n. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?f") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
281 |
and "(\<lambda>n. \<Sum>i=0..<2*n+1. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?g") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
282 |
proof - |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
283 |
have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
284 |
proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
285 |
case True |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
286 |
hence ord: "\<And>n m. m \<le> n \<Longrightarrow> a n \<le> a m" and ge0: "\<And> n. 0 \<le> a n" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
287 |
{ fix n have "a (Suc n) \<le> a n" using ord[where n="Suc n" and m=n] by auto } |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
288 |
note leibniz = summable_Leibniz'[OF `a ----> 0` ge0] and mono = this |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
289 |
from leibniz[OF mono] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
290 |
show ?thesis using `0 \<le> a 0` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
291 |
next |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
292 |
let ?a = "\<lambda> n. - a n" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
293 |
case False |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
294 |
with monoseq_le[OF `monoseq a` `a ----> 0`] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
295 |
have "(\<forall> n. a n \<le> 0) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
296 |
hence ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
297 |
{ fix n have "?a (Suc n) \<le> ?a n" using ord[where n="Suc n" and m=n] by auto } |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
298 |
note monotone = this |
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44319
diff
changeset
|
299 |
note leibniz = summable_Leibniz'[OF _ ge0, of "\<lambda>x. x", OF tendsto_minus[OF `a ----> 0`, unfolded minus_zero] monotone] |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
300 |
have "summable (\<lambda> n. (-1)^n * ?a n)" using leibniz(1) by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
301 |
then obtain l where "(\<lambda> n. (-1)^n * ?a n) sums l" unfolding summable_def by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
302 |
from this[THEN sums_minus] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
303 |
have "(\<lambda> n. (-1)^n * a n) sums -l" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
304 |
hence ?summable unfolding summable_def by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
305 |
moreover |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
306 |
have "\<And> a b :: real. \<bar> - a - - b \<bar> = \<bar>a - b\<bar>" unfolding minus_diff_minus by auto |
41970 | 307 |
|
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
308 |
from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
309 |
have move_minus: "(\<Sum>n. - (-1 ^ n * a n)) = - (\<Sum>n. -1 ^ n * a n)" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
310 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
311 |
have ?pos using `0 \<le> ?a 0` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
312 |
moreover have ?neg using leibniz(2,4) unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le by auto |
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44319
diff
changeset
|
313 |
moreover have ?f and ?g using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel] 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
|
314 |
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
|
315 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
316 |
from this[THEN conjunct1] this[THEN conjunct2, THEN conjunct1] this[THEN conjunct2, THEN conjunct2, THEN conjunct1] this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct1] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
317 |
this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct2] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
318 |
show ?summable and ?pos and ?neg and ?f and ?g . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
319 |
qed |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
320 |
|
29164 | 321 |
subsection {* Term-by-Term Differentiability of Power Series *} |
23043 | 322 |
|
323 |
definition |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
324 |
diffs :: "(nat => 'a::ring_1) => nat => 'a" where |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
325 |
"diffs c = (%n. of_nat (Suc n) * c(Suc n))" |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
326 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
327 |
text{*Lemma about distributing negation over it*} |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
328 |
lemma diffs_minus: "diffs (%n. - c n) = (%n. - diffs c n)" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
329 |
by (simp add: diffs_def) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
330 |
|
29163 | 331 |
lemma sums_Suc_imp: |
332 |
assumes f: "f 0 = 0" |
|
333 |
shows "(\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s" |
|
334 |
unfolding sums_def |
|
335 |
apply (rule LIMSEQ_imp_Suc) |
|
336 |
apply (subst setsum_shift_lb_Suc0_0_upt [where f=f, OF f, symmetric]) |
|
337 |
apply (simp only: setsum_shift_bounds_Suc_ivl) |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
338 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
339 |
|
15229 | 340 |
lemma diffs_equiv: |
41970 | 341 |
fixes x :: "'a::{real_normed_vector, ring_1}" |
342 |
shows "summable (%n. (diffs c)(n) * (x ^ n)) ==> |
|
343 |
(%n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums |
|
15546 | 344 |
(\<Sum>n. (diffs c)(n) * (x ^ n))" |
29163 | 345 |
unfolding diffs_def |
346 |
apply (drule summable_sums) |
|
347 |
apply (rule sums_Suc_imp, simp_all) |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
348 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
349 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
350 |
lemma lemma_termdiff1: |
31017 | 351 |
fixes z :: "'a :: {monoid_mult,comm_ring}" shows |
41970 | 352 |
"(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) = |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
353 |
(\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))" |
41550 | 354 |
by(auto simp add: algebra_simps power_add [symmetric]) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
355 |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
356 |
lemma sumr_diff_mult_const2: |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
357 |
"setsum f {0..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i - r)" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
358 |
by (simp add: setsum_subtractf) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
359 |
|
15229 | 360 |
lemma lemma_termdiff2: |
31017 | 361 |
fixes h :: "'a :: {field}" |
20860 | 362 |
assumes h: "h \<noteq> 0" shows |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
363 |
"((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) = |
20860 | 364 |
h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p. |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
365 |
(z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs") |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
366 |
apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h) |
20860 | 367 |
apply (simp add: right_diff_distrib diff_divide_distrib h) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
368 |
apply (simp add: mult_assoc [symmetric]) |
20860 | 369 |
apply (cases "n", simp) |
370 |
apply (simp add: lemma_realpow_diff_sumr2 h |
|
371 |
right_diff_distrib [symmetric] mult_assoc |
|
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30082
diff
changeset
|
372 |
del: power_Suc setsum_op_ivl_Suc of_nat_Suc) |
20860 | 373 |
apply (subst lemma_realpow_rev_sumr) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
374 |
apply (subst sumr_diff_mult_const2) |
20860 | 375 |
apply simp |
376 |
apply (simp only: lemma_termdiff1 setsum_right_distrib) |
|
377 |
apply (rule setsum_cong [OF refl]) |
|
15539 | 378 |
apply (simp add: diff_minus [symmetric] less_iff_Suc_add) |
20860 | 379 |
apply (clarify) |
380 |
apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac |
|
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30082
diff
changeset
|
381 |
del: setsum_op_ivl_Suc power_Suc) |
20860 | 382 |
apply (subst mult_assoc [symmetric], subst power_add [symmetric]) |
383 |
apply (simp add: mult_ac) |
|
384 |
done |
|
385 |
||
386 |
lemma real_setsum_nat_ivl_bounded2: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
387 |
fixes K :: "'a::linordered_semidom" |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
388 |
assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
389 |
assumes K: "0 \<le> K" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
390 |
shows "setsum f {0..<n-k} \<le> of_nat n * K" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
391 |
apply (rule order_trans [OF setsum_mono]) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
392 |
apply (rule f, simp) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
393 |
apply (simp add: mult_right_mono K) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
394 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
395 |
|
15229 | 396 |
lemma lemma_termdiff3: |
31017 | 397 |
fixes h z :: "'a::{real_normed_field}" |
20860 | 398 |
assumes 1: "h \<noteq> 0" |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
399 |
assumes 2: "norm z \<le> K" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
400 |
assumes 3: "norm (z + h) \<le> K" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
401 |
shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
402 |
\<le> of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h" |
20860 | 403 |
proof - |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
404 |
have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) = |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
405 |
norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p. |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
406 |
(z + h) ^ q * z ^ (n - 2 - q)) * norm h" |
20860 | 407 |
apply (subst lemma_termdiff2 [OF 1]) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
408 |
apply (subst norm_mult) |
20860 | 409 |
apply (rule mult_commute) |
410 |
done |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
411 |
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
|
412 |
proof (rule mult_right_mono [OF _ norm_ge_zero]) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
413 |
from norm_ge_zero 2 have K: "0 \<le> K" by (rule order_trans) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
414 |
have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n" |
20860 | 415 |
apply (erule subst) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
416 |
apply (simp only: norm_mult norm_power power_add) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
417 |
apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K) |
20860 | 418 |
done |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
419 |
show "norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p. |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
420 |
(z + h) ^ q * z ^ (n - 2 - q)) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
421 |
\<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))" |
20860 | 422 |
apply (intro |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
423 |
order_trans [OF norm_setsum] |
20860 | 424 |
real_setsum_nat_ivl_bounded2 |
425 |
mult_nonneg_nonneg |
|
47489 | 426 |
of_nat_0_le_iff |
20860 | 427 |
zero_le_power K) |
428 |
apply (rule le_Kn, simp) |
|
429 |
done |
|
430 |
qed |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
431 |
also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h" |
20860 | 432 |
by (simp only: mult_assoc) |
433 |
finally show ?thesis . |
|
434 |
qed |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
435 |
|
20860 | 436 |
lemma lemma_termdiff4: |
31017 | 437 |
fixes f :: "'a::{real_normed_field} \<Rightarrow> |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
438 |
'b::real_normed_vector" |
20860 | 439 |
assumes k: "0 < (k::real)" |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
440 |
assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h" |
20860 | 441 |
shows "f -- 0 --> 0" |
31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
31271
diff
changeset
|
442 |
unfolding LIM_eq diff_0_right |
29163 | 443 |
proof (safe) |
444 |
let ?h = "of_real (k / 2)::'a" |
|
445 |
have "?h \<noteq> 0" and "norm ?h < k" using k by simp_all |
|
446 |
hence "norm (f ?h) \<le> K * norm ?h" by (rule le) |
|
447 |
hence "0 \<le> K * norm ?h" by (rule order_trans [OF norm_ge_zero]) |
|
448 |
hence zero_le_K: "0 \<le> K" using k by (simp add: zero_le_mult_iff) |
|
449 |
||
20860 | 450 |
fix r::real assume r: "0 < r" |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
451 |
show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" |
20860 | 452 |
proof (cases) |
453 |
assume "K = 0" |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
454 |
with k r le have "0 < k \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < k \<longrightarrow> norm (f x) < r)" |
20860 | 455 |
by simp |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
456 |
thus "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" .. |
20860 | 457 |
next |
458 |
assume K_neq_zero: "K \<noteq> 0" |
|
459 |
with zero_le_K have K: "0 < K" by simp |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
460 |
show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" |
20860 | 461 |
proof (rule exI, safe) |
462 |
from k r K show "0 < min k (r * inverse K / 2)" |
|
463 |
by (simp add: mult_pos_pos positive_imp_inverse_positive) |
|
464 |
next |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
465 |
fix x::'a |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
466 |
assume x1: "x \<noteq> 0" and x2: "norm x < min k (r * inverse K / 2)" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
467 |
from x2 have x3: "norm x < k" and x4: "norm x < r * inverse K / 2" |
20860 | 468 |
by simp_all |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
469 |
from x1 x3 le have "norm (f x) \<le> K * norm x" by simp |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
470 |
also from x4 K have "K * norm x < K * (r * inverse K / 2)" |
20860 | 471 |
by (rule mult_strict_left_mono) |
472 |
also have "\<dots> = r / 2" |
|
473 |
using K_neq_zero by simp |
|
474 |
also have "r / 2 < r" |
|
475 |
using r by simp |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
476 |
finally show "norm (f x) < r" . |
20860 | 477 |
qed |
478 |
qed |
|
479 |
qed |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
480 |
|
15229 | 481 |
lemma lemma_termdiff5: |
31017 | 482 |
fixes g :: "'a::{real_normed_field} \<Rightarrow> |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
483 |
nat \<Rightarrow> 'b::banach" |
20860 | 484 |
assumes k: "0 < (k::real)" |
485 |
assumes f: "summable f" |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
486 |
assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h" |
20860 | 487 |
shows "(\<lambda>h. suminf (g h)) -- 0 --> 0" |
488 |
proof (rule lemma_termdiff4 [OF k]) |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
489 |
fix h::'a assume "h \<noteq> 0" and "norm h < k" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
490 |
hence A: "\<forall>n. norm (g h n) \<le> f n * norm h" |
20860 | 491 |
by (simp add: le) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
492 |
hence "\<exists>N. \<forall>n\<ge>N. norm (norm (g h n)) \<le> f n * norm h" |
20860 | 493 |
by simp |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
494 |
moreover from f have B: "summable (\<lambda>n. f n * norm h)" |
20860 | 495 |
by (rule summable_mult2) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
496 |
ultimately have C: "summable (\<lambda>n. norm (g h n))" |
20860 | 497 |
by (rule summable_comparison_test) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
498 |
hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
499 |
by (rule summable_norm) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
500 |
also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)" |
20860 | 501 |
by (rule summable_le) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
502 |
also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h" |
20860 | 503 |
by (rule suminf_mult2 [symmetric]) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
504 |
finally show "norm (suminf (g h)) \<le> suminf f * norm h" . |
20860 | 505 |
qed |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
506 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
507 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
508 |
text{* FIXME: Long proofs*} |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
509 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
510 |
lemma termdiffs_aux: |
31017 | 511 |
fixes x :: "'a::{real_normed_field,banach}" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
512 |
assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)" |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
513 |
assumes 2: "norm x < norm K" |
20860 | 514 |
shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
515 |
- of_nat n * x ^ (n - Suc 0))) -- 0 --> 0" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
516 |
proof - |
20860 | 517 |
from dense [OF 2] |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
518 |
obtain r where r1: "norm x < r" and r2: "r < norm K" by fast |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
519 |
from norm_ge_zero r1 have r: "0 < r" |
20860 | 520 |
by (rule order_le_less_trans) |
521 |
hence r_neq_0: "r \<noteq> 0" by simp |
|
522 |
show ?thesis |
|
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
523 |
proof (rule lemma_termdiff5) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
524 |
show "0 < r - norm x" using r1 by simp |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
525 |
next |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
526 |
from r r2 have "norm (of_real r::'a) < norm K" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
527 |
by simp |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
528 |
with 1 have "summable (\<lambda>n. norm (diffs (diffs c) n * (of_real r ^ n)))" |
20860 | 529 |
by (rule powser_insidea) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
530 |
hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. norm (c n))) n * r ^ n)" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
531 |
using r |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
532 |
by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
533 |
hence "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))" |
20860 | 534 |
by (rule diffs_equiv [THEN sums_summable]) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
535 |
also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0)) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
536 |
= (\<lambda>n. diffs (%m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))" |
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
537 |
apply (rule ext) |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
538 |
apply (simp add: diffs_def) |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
539 |
apply (case_tac n, simp_all add: r_neq_0) |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
540 |
done |
41970 | 541 |
finally have "summable |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
542 |
(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))" |
20860 | 543 |
by (rule diffs_equiv [THEN sums_summable]) |
544 |
also have |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
545 |
"(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * |
20860 | 546 |
r ^ (n - Suc 0)) = |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
547 |
(\<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
|
548 |
apply (rule ext) |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
549 |
apply (case_tac "n", simp) |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
550 |
apply (case_tac "nat", simp) |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
551 |
apply (simp add: r_neq_0) |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
552 |
done |
20860 | 553 |
finally show |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
554 |
"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
|
555 |
next |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
556 |
fix h::'a and n::nat |
20860 | 557 |
assume h: "h \<noteq> 0" |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
558 |
assume "norm h < r - norm x" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
559 |
hence "norm x + norm h < r" by simp |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
560 |
with norm_triangle_ineq have xh: "norm (x + h) < r" |
20860 | 561 |
by (rule order_le_less_trans) |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
562 |
show "norm (c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
563 |
\<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
564 |
apply (simp only: norm_mult mult_assoc) |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
565 |
apply (rule mult_left_mono [OF _ norm_ge_zero]) |
20860 | 566 |
apply (simp (no_asm) add: mult_assoc [symmetric]) |
567 |
apply (rule lemma_termdiff3) |
|
568 |
apply (rule h) |
|
569 |
apply (rule r1 [THEN order_less_imp_le]) |
|
570 |
apply (rule xh [THEN order_less_imp_le]) |
|
571 |
done |
|
20849
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
572 |
qed |
389cd9c8cfe1
rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents:
20692
diff
changeset
|
573 |
qed |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset
|
574 |
|
20860 | 575 |
lemma termdiffs: |
31017 | 576 |
fixes K x :: "'a::{real_normed_field,banach}" |
20860 | 577 |
assumes 1: "summable (\<lambda>n. c n * K ^ n)" |
578 |
assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)" |
|
579 |
assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)" |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
580 |
assumes 4: "norm x < norm K" |
20860 | 581 |
shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)" |
29163 | 582 |
unfolding deriv_def |
583 |
proof (rule LIM_zero_cancel) |
|
20860 | 584 |
show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h |
585 |
- suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0" |
|
586 |
proof (rule LIM_equal2) |
|
29163 | 587 |
show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq) |
20860 | 588 |
next |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
589 |
fix h :: 'a |
20860 | 590 |
assume "h \<noteq> 0" |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
591 |
assume "norm (h - 0) < norm K - norm x" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
592 |
hence "norm x + norm h < norm K" by simp |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
593 |
hence 5: "norm (x + h) < norm K" |
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
594 |
by (rule norm_triangle_ineq [THEN order_le_less_trans]) |
20860 | 595 |
have A: "summable (\<lambda>n. c n * x ^ n)" |
596 |
by (rule powser_inside [OF 1 4]) |
|
597 |
have B: "summable (\<lambda>n. c n * (x + h) ^ n)" |
|
598 |
by (rule powser_inside [OF 1 5]) |
|
599 |
have C: "summable (\<lambda>n. diffs c n * x ^ n)" |
|
600 |
by (rule powser_inside [OF 2 4]) |
|
601 |
show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h |
|
41970 | 602 |
- (\<Sum>n. diffs c n * x ^ n) = |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
603 |
(\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))" |
20860 | 604 |
apply (subst sums_unique [OF diffs_equiv [OF C]]) |
605 |
apply (subst suminf_diff [OF B A]) |
|
606 |
apply (subst suminf_divide [symmetric]) |
|
607 |
apply (rule summable_diff [OF B A]) |
|
608 |
apply (subst suminf_diff) |
|
609 |
apply (rule summable_divide) |
|
610 |
apply (rule summable_diff [OF B A]) |
|
611 |
apply (rule sums_summable [OF diffs_equiv [OF C]]) |
|
29163 | 612 |
apply (rule arg_cong [where f="suminf"], rule ext) |
29667 | 613 |
apply (simp add: algebra_simps) |
20860 | 614 |
done |
615 |
next |
|
616 |
show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - |
|
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
617 |
of_nat n * x ^ (n - Suc 0))) -- 0 --> 0" |
20860 | 618 |
by (rule termdiffs_aux [OF 3 4]) |
619 |
qed |
|
620 |
qed |
|
621 |
||
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
622 |
|
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
623 |
subsection {* Derivability of power series *} |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
624 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
625 |
lemma DERIV_series': fixes f :: "real \<Rightarrow> nat \<Rightarrow> real" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
626 |
assumes DERIV_f: "\<And> n. DERIV (\<lambda> x. f x n) x0 :> (f' x0 n)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
627 |
and allf_summable: "\<And> x. x \<in> {a <..< b} \<Longrightarrow> summable (f x)" and x0_in_I: "x0 \<in> {a <..< b}" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
628 |
and "summable (f' x0)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
629 |
and "summable L" and L_def: "\<And> n x y. \<lbrakk> x \<in> { a <..< b} ; y \<in> { a <..< b} \<rbrakk> \<Longrightarrow> \<bar> f x n - f y n \<bar> \<le> L n * \<bar> x - y \<bar>" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
630 |
shows "DERIV (\<lambda> x. suminf (f x)) x0 :> (suminf (f' x0))" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
631 |
unfolding deriv_def |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
632 |
proof (rule LIM_I) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
633 |
fix r :: real assume "0 < r" hence "0 < r/3" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
634 |
|
41970 | 635 |
obtain N_L where N_L: "\<And> n. N_L \<le> n \<Longrightarrow> \<bar> \<Sum> i. L (i + n) \<bar> < r/3" |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
636 |
using suminf_exist_split[OF `0 < r/3` `summable L`] by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
637 |
|
41970 | 638 |
obtain N_f' where N_f': "\<And> n. N_f' \<le> n \<Longrightarrow> \<bar> \<Sum> i. f' x0 (i + n) \<bar> < r/3" |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
639 |
using suminf_exist_split[OF `0 < r/3` `summable (f' x0)`] by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
640 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
641 |
let ?N = "Suc (max N_L N_f')" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
642 |
have "\<bar> \<Sum> i. f' x0 (i + ?N) \<bar> < r/3" (is "?f'_part < r/3") and |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
643 |
L_estimate: "\<bar> \<Sum> i. L (i + ?N) \<bar> < r/3" using N_L[of "?N"] and N_f' [of "?N"] by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
644 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
645 |
let "?diff i x" = "(f (x0 + x) i - f x0 i) / x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
646 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
647 |
let ?r = "r / (3 * real ?N)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
648 |
have "0 < 3 * real ?N" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
649 |
from divide_pos_pos[OF `0 < r` this] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
650 |
have "0 < ?r" . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
651 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
652 |
let "?s 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)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
653 |
def S' \<equiv> "Min (?s ` { 0 ..< ?N })" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
654 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
655 |
have "0 < S'" unfolding S'_def |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
656 |
proof (rule iffD2[OF Min_gr_iff]) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
657 |
show "\<forall> x \<in> (?s ` { 0 ..< ?N }). 0 < x" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
658 |
proof (rule ballI) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
659 |
fix x assume "x \<in> ?s ` {0..<?N}" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
660 |
then obtain n where "x = ?s n" and "n \<in> {0..<?N}" using image_iff[THEN iffD1] by blast |
41970 | 661 |
from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def] |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
662 |
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)" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
663 |
have "0 < ?s n" by (rule someI2[where a=s], auto simp add: s_bound) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
664 |
thus "0 < x" unfolding `x = ?s n` . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
665 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
666 |
qed auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
667 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
668 |
def S \<equiv> "min (min (x0 - a) (b - x0)) S'" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
669 |
hence "0 < S" and S_a: "S \<le> x0 - a" and S_b: "S \<le> b - x0" and "S \<le> S'" using x0_in_I and `0 < S'` |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
670 |
by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
671 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
672 |
{ fix x assume "x \<noteq> 0" and "\<bar> x \<bar> < S" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
673 |
hence x_in_I: "x0 + x \<in> { a <..< b }" using S_a S_b by auto |
41970 | 674 |
|
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
675 |
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
|
676 |
note div_smbl = summable_divide[OF diff_smbl] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
677 |
note all_smbl = summable_diff[OF div_smbl `summable (f' x0)`] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
678 |
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
|
679 |
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
|
680 |
note div_shft_smbl = summable_divide[OF diff_shft_smbl] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
681 |
note all_shft_smbl = summable_diff[OF div_smbl ign[OF `summable (f' x0)`]] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
682 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
683 |
{ fix n |
41970 | 684 |
have "\<bar> ?diff (n + ?N) x \<bar> \<le> L (n + ?N) * \<bar> (x0 + x) - x0 \<bar> / \<bar> x \<bar>" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
685 |
using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero] unfolding abs_divide . |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
686 |
hence "\<bar> ( \<bar> ?diff (n + ?N) x \<bar>) \<bar> \<le> L (n + ?N)" using `x \<noteq> 0` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
687 |
} note L_ge = summable_le2[OF allI[OF this] ign[OF `summable L`]] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
688 |
from order_trans[OF summable_rabs[OF conjunct1[OF L_ge]] L_ge[THEN conjunct2]] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
689 |
have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))" . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
690 |
hence "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3") using L_estimate by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
691 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
692 |
have "\<bar>\<Sum>n \<in> { 0 ..< ?N}. ?diff n x - f' x0 n \<bar> \<le> (\<Sum>n \<in> { 0 ..< ?N}. \<bar>?diff n x - f' x0 n \<bar>)" .. |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
693 |
also have "\<dots> < (\<Sum>n \<in> { 0 ..< ?N}. ?r)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
694 |
proof (rule setsum_strict_mono) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
695 |
fix n assume "n \<in> { 0 ..< ?N}" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
696 |
have "\<bar> x \<bar> < S" using `\<bar> x \<bar> < S` . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
697 |
also have "S \<le> S'" using `S \<le> S'` . |
41970 | 698 |
also have "S' \<le> ?s n" unfolding S'_def |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
699 |
proof (rule Min_le_iff[THEN iffD2]) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
700 |
have "?s n \<in> (?s ` {0..<?N}) \<and> ?s n \<le> ?s n" using `n \<in> { 0 ..< ?N}` by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
701 |
thus "\<exists> a \<in> (?s ` {0..<?N}). a \<le> ?s n" by blast |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
702 |
qed auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
703 |
finally have "\<bar> x \<bar> < ?s n" . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
704 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
705 |
from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def diff_0_right, unfolded some_eq_ex[symmetric], THEN conjunct2] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
706 |
have "\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < ?s n \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r" . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
707 |
with `x \<noteq> 0` and `\<bar>x\<bar> < ?s n` |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
708 |
show "\<bar>?diff n x - f' x0 n\<bar> < ?r" by blast |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
709 |
qed auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
710 |
also have "\<dots> = of_nat (card {0 ..< ?N}) * ?r" by (rule setsum_constant) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
711 |
also have "\<dots> = real ?N * ?r" unfolding real_eq_of_nat by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
712 |
also have "\<dots> = r/3" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
713 |
finally have "\<bar>\<Sum>n \<in> { 0 ..< ?N}. ?diff n x - f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
714 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
715 |
from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]] |
41970 | 716 |
have "\<bar> (suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0) \<bar> = |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
717 |
\<bar> \<Sum>n. ?diff n x - f' x0 n \<bar>" unfolding suminf_diff[OF div_smbl `summable (f' x0)`, symmetric] using suminf_divide[OF diff_smbl, symmetric] by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
718 |
also have "\<dots> \<le> ?diff_part + \<bar> (\<Sum>n. ?diff (n + ?N) x) - (\<Sum> n. f' x0 (n + ?N)) \<bar>" unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"] unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]] by (rule abs_triangle_ineq) |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
719 |
also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part" using abs_triangle_ineq4 by auto |
41970 | 720 |
also have "\<dots> < r /3 + r/3 + r/3" |
36842 | 721 |
using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3` |
722 |
by (rule add_strict_mono [OF add_less_le_mono]) |
|
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
723 |
finally have "\<bar> (suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0) \<bar> < r" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
724 |
by auto |
41970 | 725 |
} thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x - 0) < s \<longrightarrow> |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
726 |
norm (((\<Sum>n. f (x0 + x) n) - (\<Sum>n. f x0 n)) / x - (\<Sum>n. f' x0 n)) < r" using `0 < S` |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
727 |
unfolding real_norm_def diff_0_right by blast |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
728 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
729 |
|
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
730 |
lemma DERIV_power_series': fixes f :: "nat \<Rightarrow> real" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
731 |
assumes converges: "\<And> x. x \<in> {-R <..< R} \<Longrightarrow> summable (\<lambda> n. f n * real (Suc n) * x^n)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
732 |
and x0_in_I: "x0 \<in> {-R <..< R}" and "0 < R" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
733 |
shows "DERIV (\<lambda> x. (\<Sum> n. f n * x^(Suc n))) x0 :> (\<Sum> n. f n * real (Suc n) * x0^n)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
734 |
(is "DERIV (\<lambda> x. (suminf (?f x))) x0 :> (suminf (?f' x0))") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
735 |
proof - |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
736 |
{ fix R' assume "0 < R'" and "R' < R" and "-R' < x0" and "x0 < R'" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
737 |
hence "x0 \<in> {-R' <..< R'}" and "R' \<in> {-R <..< R}" and "x0 \<in> {-R <..< R}" by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
738 |
have "DERIV (\<lambda> x. (suminf (?f x))) x0 :> (suminf (?f' x0))" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
739 |
proof (rule DERIV_series') |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
740 |
show "summable (\<lambda> n. \<bar>f n * real (Suc n) * R'^n\<bar>)" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
741 |
proof - |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
742 |
have "(R' + R) / 2 < R" and "0 < (R' + R) / 2" using `0 < R'` `0 < R` `R' < R` by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
743 |
hence in_Rball: "(R' + R) / 2 \<in> {-R <..< R}" using `R' < R` by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
744 |
have "norm R' < norm ((R' + R) / 2)" using `0 < R'` `0 < R` `R' < R` by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
745 |
from powser_insidea[OF converges[OF in_Rball] this] show ?thesis 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
|
746 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
747 |
{ fix n x y assume "x \<in> {-R' <..< R'}" and "y \<in> {-R' <..< R'}" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
748 |
show "\<bar>?f x n - ?f y n\<bar> \<le> \<bar>f n * real (Suc n) * R'^n\<bar> * \<bar>x-y\<bar>" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
749 |
proof - |
41970 | 750 |
have "\<bar>f n * x ^ (Suc n) - f n * y ^ (Suc n)\<bar> = (\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar>" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
751 |
unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult by auto |
41970 | 752 |
also have "\<dots> \<le> (\<bar>f n\<bar> * \<bar>x-y\<bar>) * (\<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>)" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
753 |
proof (rule mult_left_mono) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
754 |
have "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> (\<Sum>p = 0..<Suc n. \<bar>x ^ p * y ^ (n - p)\<bar>)" by (rule setsum_abs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
755 |
also have "\<dots> \<le> (\<Sum>p = 0..<Suc n. R' ^ n)" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
756 |
proof (rule setsum_mono) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
757 |
fix p assume "p \<in> {0..<Suc n}" hence "p \<le> n" by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
758 |
{ fix n fix x :: real assume "x \<in> {-R'<..<R'}" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
759 |
hence "\<bar>x\<bar> \<le> R'" by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
760 |
hence "\<bar>x^n\<bar> \<le> R'^n" unfolding power_abs by (rule power_mono, auto) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
761 |
} from mult_mono[OF this[OF `x \<in> {-R'<..<R'}`, of p] this[OF `y \<in> {-R'<..<R'}`, of "n-p"]] `0 < R'` |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
762 |
have "\<bar>x^p * y^(n-p)\<bar> \<le> R'^p * R'^(n-p)" unfolding abs_mult by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
763 |
thus "\<bar>x^p * y^(n-p)\<bar> \<le> R'^n" unfolding power_add[symmetric] using `p \<le> n` by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
764 |
qed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
765 |
also have "\<dots> = real (Suc n) * R' ^ n" unfolding setsum_constant card_atLeastLessThan real_of_nat_def by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
766 |
finally show "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>" unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
767 |
show "0 \<le> \<bar>f n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult[symmetric] by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
768 |
qed |
36777
be5461582d0f
avoid using real-specific versions of generic lemmas
huffman
parents:
36776
diff
changeset
|
769 |
also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult mult_assoc[symmetric] by algebra |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
770 |
finally show ?thesis . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
771 |
qed } |
31881 | 772 |
{ fix n show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
773 |
by (auto intro!: DERIV_intros simp del: power_Suc) } |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
774 |
{ fix x assume "x \<in> {-R' <..< R'}" hence "R' \<in> {-R <..< R}" and "norm x < norm R'" using assms `R' < R` by auto |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
775 |
have "summable (\<lambda> n. f n * x^n)" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
776 |
proof (rule summable_le2[THEN conjunct1, OF _ powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`]], rule allI) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
777 |
fix n |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
778 |
have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)" by (rule mult_left_mono, auto) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
779 |
show "\<bar>f n * x ^ n\<bar> \<le> norm (f n * real (Suc n) * x ^ n)" unfolding real_norm_def abs_mult |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
780 |
by (rule mult_right_mono, auto simp add: le[unfolded mult_1_right]) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
781 |
qed |
36777
be5461582d0f
avoid using real-specific versions of generic lemmas
huffman
parents:
36776
diff
changeset
|
782 |
from this[THEN summable_mult2[where c=x], unfolded mult_assoc, unfolded mult_commute] |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32047
diff
changeset
|
783 |
show "summable (?f x)" 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
|
784 |
show "summable (?f' x0)" using converges[OF `x0 \<in> {-R <..< R}`] . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
785 |
show "x0 \<in> {-R' <..< R'}" using `x0 \<in> {-R' <..< R'}` . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
786 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
787 |
} note for_subinterval = this |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
788 |
let ?R = "(R + \<bar>x0\<bar>) / 2" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
789 |
have "\<bar>x0\<bar> < ?R" using assms by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
790 |
hence "- ?R < x0" |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
791 |
proof (cases "x0 < 0") |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
792 |
case True |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
793 |
hence "- x0 < ?R" using `\<bar>x0\<bar> < ?R` by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
794 |
thus ?thesis unfolding neg_less_iff_less[symmetric, of "- x0"] by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
795 |
next |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
796 |
case False |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
797 |
have "- ?R < 0" using assms by auto |
41970 | 798 |
also have "\<dots> \<le> x0" using False by auto |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
799 |
finally show ?thesis . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
800 |
qed |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
801 |
hence "0 < ?R" "?R < R" "- ?R < x0" and "x0 < ?R" using assms by auto |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
802 |
from for_subinterval[OF this] |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
803 |
show ?thesis . |
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29695
diff
changeset
|
804 |
qed |
29695 | 805 |
|
29164 | 806 |
subsection {* Exponential Function *} |
23043 | 807 |
|
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
808 |
definition exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
809 |
"exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))" |
23043 | 810 |
|
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
811 |
lemma summable_exp_generic: |
31017 | 812 |
fixes x :: "'a::{real_normed_algebra_1,banach}" |
25062 | 813 |
defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)" |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
814 |
shows "summable S" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
815 |
proof - |
25062 | 816 |
have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)" |
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30082
diff
changeset
|
817 |
unfolding S_def by (simp del: mult_Suc) |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
818 |
obtain r :: real where r0: "0 < r" and r1: "r < 1" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
819 |
using dense [OF zero_less_one] by fast |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
820 |
obtain N :: nat where N: "norm x < real N * r" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
821 |
using reals_Archimedean3 [OF r0] by fast |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
822 |
from r1 show ?thesis |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
823 |
proof (rule ratio_test [rule_format]) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
824 |
fix n :: nat |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
825 |
assume n: "N \<le> n" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
826 |
have "norm x \<le> real N * r" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
827 |
using N by (rule order_less_imp_le) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
828 |
also have "real N * r \<le> real (Suc n) * r" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
829 |
using r0 n by (simp add: mult_right_mono) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
830 |
finally have "norm x * norm (S n) \<le> real (Suc n) * r * norm (S n)" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
831 |
using norm_ge_zero by (rule mult_right_mono) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
832 |
hence "norm (x * S n) \<le> real (Suc n) * r * norm (S n)" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
833 |
by (rule order_trans [OF norm_mult_ineq]) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
834 |
hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
835 |
by (simp add: pos_divide_le_eq mult_ac) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
836 |
thus "norm (S (Suc n)) \<le> r * norm (S n)" |
35216 | 837 |
by (simp add: S_Suc inverse_eq_divide) |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
838 |
qed |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
839 |
qed |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
840 |
|
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
841 |
lemma summable_norm_exp: |
31017 | 842 |
fixes x :: "'a::{real_normed_algebra_1,banach}" |
25062 | 843 |
shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))" |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
844 |
proof (rule summable_norm_comparison_test [OF exI, rule_format]) |
25062 | 845 |
show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))" |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
846 |
by (rule summable_exp_generic) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
847 |
next |
25062 | 848 |
fix n show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)" |
35216 | 849 |
by (simp add: norm_power_ineq) |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
850 |
qed |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
851 |
|
23043 | 852 |
lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)" |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
853 |
by (insert summable_exp_generic [where x=x], simp) |
23043 | 854 |
|
25062 | 855 |
lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x" |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
856 |
unfolding exp_def by (rule summable_exp_generic [THEN summable_sums]) |
23043 | 857 |
|
858 |
||
41970 | 859 |
lemma exp_fdiffs: |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
860 |
"diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))" |
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23413
diff
changeset
|
861 |
by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def of_nat_mult |
23082
ffef77eed382
generalize powerseries and termdiffs lemmas using axclasses
huffman
parents:
23069
diff
changeset
|
862 |
del: mult_Suc of_nat_Suc) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
863 |
|
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
864 |
lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
865 |
by (simp add: diffs_def) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
866 |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
867 |
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" |
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
868 |
unfolding exp_def scaleR_conv_of_real |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
869 |
apply (rule DERIV_cong) |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
870 |
apply (rule termdiffs [where K="of_real (1 + norm x)"]) |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
871 |
apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
872 |
apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+ |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
873 |
apply (simp del: of_real_add) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
874 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
875 |
|
51527 | 876 |
declare DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] |
877 |
||
44311 | 878 |
lemma isCont_exp: "isCont exp x" |
879 |
by (rule DERIV_exp [THEN DERIV_isCont]) |
|
880 |
||
881 |
lemma isCont_exp' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a" |
|
882 |
by (rule isCont_o2 [OF _ isCont_exp]) |
|
883 |
||
884 |
lemma tendsto_exp [tendsto_intros]: |
|
885 |
"(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F" |
|
886 |
by (rule isCont_tendsto_compose [OF isCont_exp]) |
|
23045
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset
|
887 |
|
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
888 |
lemma continuous_exp [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
889 |
unfolding continuous_def by (rule tendsto_exp) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
890 |
|
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
891 |
lemma continuous_on_exp [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
892 |
unfolding continuous_on_def by (auto intro: tendsto_exp) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
893 |
|
29167 | 894 |
subsubsection {* Properties of the Exponential Function *} |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
895 |
|
23278 | 896 |
lemma powser_zero: |
31017 | 897 |
fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}" |
23278 | 898 |
shows "(\<Sum>n. f n * 0 ^ n) = f 0" |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
899 |
proof - |
23278 | 900 |
have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)" |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
901 |
by (rule sums_unique [OF series_zero], simp add: power_0_left) |
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset
|
902 |
thus ?thesis unfolding One_nat_def by simp |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
903 |
qed |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
904 |
|
23278 | 905 |
lemma exp_zero [simp]: "exp 0 = 1" |
906 |
unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero) |
|
907 |
||
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
908 |
lemma setsum_cl_ivl_Suc2: |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
909 |
"(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))" |
28069 | 910 |
by (simp add: setsum_head_Suc setsum_shift_bounds_cl_Suc_ivl |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
911 |
del: setsum_cl_ivl_Suc) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
912 |
|
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
913 |
lemma exp_series_add: |
31017 | 914 |
fixes x y :: "'a::{real_field}" |
25062 | 915 |
defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)" |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
916 |
shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
917 |
proof (induct n) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
918 |
case 0 |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
919 |
show ?case |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
920 |
unfolding S_def by simp |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
921 |
next |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
922 |
case (Suc n) |
25062 | 923 |
have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)" |
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30082
diff
changeset
|
924 |
unfolding S_def by (simp del: mult_Suc) |
25062 | 925 |
hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)" |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
926 |
by simp |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
927 |
|
25062 | 928 |
have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n" |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
929 |
by (simp only: times_S) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
930 |
also have "\<dots> = (x + y) * (\<Sum>i=0..n. S x i * S y (n-i))" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
931 |
by (simp only: Suc) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
932 |
also have "\<dots> = x * (\<Sum>i=0..n. S x i * S y (n-i)) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
933 |
+ y * (\<Sum>i=0..n. S x i * S y (n-i))" |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47489
diff
changeset
|
934 |
by (rule distrib_right) |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
935 |
also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (n-i)) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
936 |
+ (\<Sum>i=0..n. S x i * (y * S y (n-i)))" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
937 |
by (simp only: setsum_right_distrib mult_ac) |
25062 | 938 |
also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) |
939 |
+ (\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))" |
|
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
940 |
by (simp add: times_S Suc_diff_le) |
25062 | 941 |
also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) = |
942 |
(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))" |
|
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
943 |
by (subst setsum_cl_ivl_Suc2, simp) |
25062 | 944 |
also have "(\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) = |
945 |
(\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))" |
|
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
946 |
by (subst setsum_cl_ivl_Suc, simp) |
25062 | 947 |
also have "(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) + |
948 |
(\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) = |
|
949 |
(\<Sum>i=0..Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))" |
|
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
950 |
by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric] |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
951 |
real_of_nat_add [symmetric], simp) |
25062 | 952 |
also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))" |
23127 | 953 |
by (simp only: scaleR_right.setsum) |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
954 |
finally show |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
955 |
"S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))" |
35216 | 956 |
by (simp del: setsum_cl_ivl_Suc) |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
957 |
qed |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
958 |
|
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
959 |
lemma exp_add: "exp (x + y) = exp x * exp y" |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
960 |
unfolding exp_def |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
961 |
by (simp only: Cauchy_product summable_norm_exp exp_series_add) |
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
962 |
|
29170 | 963 |
lemma mult_exp_exp: "exp x * exp y = exp (x + y)" |
964 |
by (rule exp_add [symmetric]) |
|
965 |
||
23241 | 966 |
lemma exp_of_real: "exp (of_real x) = of_real (exp x)" |
967 |
unfolding exp_def |
|
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
43335
diff
changeset
|
968 |
apply (subst suminf_of_real) |
23241 | 969 |
apply (rule summable_exp_generic) |
970 |
apply (simp add: scaleR_conv_of_real) |
|
971 |
done |
|
972 |
||
29170 | 973 |
lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0" |
974 |
proof |
|
975 |
have "exp x * exp (- x) = 1" by (simp add: mult_exp_exp) |
|
976 |
also assume "exp x = 0" |
|
977 |
finally show "False" by simp |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
978 |
qed |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
979 |
|
29170 | 980 |
lemma exp_minus: "exp (- x) = inverse (exp x)" |
981 |
by (rule inverse_unique [symmetric], simp add: mult_exp_exp) |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
982 |
|
29170 | 983 |
lemma exp_diff: "exp (x - y) = exp x / exp y" |
984 |
unfolding diff_minus divide_inverse |
|
985 |
by (simp add: exp_add exp_minus) |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
986 |
|
29167 | 987 |
|
988 |
subsubsection {* Properties of the Exponential Function on Reals *} |
|
989 |
||
29170 | 990 |
text {* Comparisons of @{term "exp x"} with zero. *} |
29167 | 991 |
|
992 |
text{*Proof: because every exponential can be seen as a square.*} |
|
993 |
lemma exp_ge_zero [simp]: "0 \<le> exp (x::real)" |
|
994 |
proof - |
|
995 |
have "0 \<le> exp (x/2) * exp (x/2)" by simp |
|
996 |
thus ?thesis by (simp add: exp_add [symmetric]) |
|
997 |
qed |
|
998 |
||
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
999 |
lemma exp_gt_zero [simp]: "0 < exp (x::real)" |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1000 |
by (simp add: order_less_le) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1001 |
|
29170 | 1002 |
lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0" |
1003 |
by (simp add: not_less) |
|
1004 |
||
1005 |
lemma not_exp_le_zero [simp]: "\<not> exp (x::real) \<le> 0" |
|
1006 |
by (simp add: not_le) |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1007 |
|
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
1008 |
lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x" |
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset
|
1009 |
by simp |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1010 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1011 |
lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" |
15251 | 1012 |
apply (induct "n") |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47489
diff
changeset
|
1013 |
apply (auto simp add: real_of_nat_Suc distrib_left exp_add mult_commute) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1014 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1015 |
|
29170 | 1016 |
text {* Strict monotonicity of exponential. *} |
1017 |
||
1018 |
lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) ==> (1 + x) \<le> exp(x)" |
|
1019 |
apply (drule order_le_imp_less_or_eq, auto) |
|
1020 |
apply (simp add: exp_def) |
|
36777
be5461582d0f
avoid using real-specific versions of generic lemmas
huffman
parents:
36776
diff
changeset
|
1021 |
apply (rule order_trans) |
29170 | 1022 |
apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le) |
1023 |
apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff) |
|
1024 |
done |
|
1025 |
||
1026 |
lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x" |
|
1027 |
proof - |
|
1028 |
assume x: "0 < x" |
|
1029 |
hence "1 < 1 + x" by simp |
|
1030 |
also from x have "1 + x \<le> exp x" |
|
1031 |
by (simp add: exp_ge_add_one_self_aux) |
|
1032 |
finally show ?thesis . |
|
1033 |
qed |
|
1034 |
||
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1035 |
lemma exp_less_mono: |
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
1036 |
fixes x y :: real |
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset
|
1037 |
assumes "x < y" shows "exp x < exp y" |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1038 |
proof - |
29165
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset
|
1039 |
from `x < y` have "0 < y - x" by simp |
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset
|
1040 |
hence "1 < exp (y - x)" by (rule exp_gt_one) |
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset
|
1041 |
hence "1 < exp y / exp x" by (simp only: exp_diff) |
562f95f06244
cleaned up some proofs; removed redundant simp rules
huffman
parents:
29164
diff
changeset
|
1042 |
thus "exp x < exp y" by simp |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1043 |
qed |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1044 |
|
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
1045 |
lemma exp_less_cancel: "exp (x::real) < exp y ==> x < y" |
29170 | 1046 |
apply (simp add: linorder_not_le [symmetric]) |
1047 |
apply (auto simp add: order_le_less exp_less_mono) |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1048 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1049 |
|
29170 | 1050 |
lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y" |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1051 |
by (auto intro: exp_less_mono exp_less_cancel) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1052 |
|
29170 | 1053 |
lemma exp_le_cancel_iff [iff]: "exp (x::real) \<le> exp y \<longleftrightarrow> x \<le> y" |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1054 |
by (auto simp add: linorder_not_less [symmetric]) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1055 |
|
29170 | 1056 |
lemma exp_inj_iff [iff]: "exp (x::real) = exp y \<longleftrightarrow> x = y" |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1057 |
by (simp add: order_eq_iff) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1058 |
|
29170 | 1059 |
text {* Comparisons of @{term "exp x"} with one. *} |
1060 |
||
1061 |
lemma one_less_exp_iff [simp]: "1 < exp (x::real) \<longleftrightarrow> 0 < x" |
|
1062 |
using exp_less_cancel_iff [where x=0 and y=x] by simp |
|
1063 |
||
1064 |
lemma exp_less_one_iff [simp]: "exp (x::real) < 1 \<longleftrightarrow> x < 0" |
|
1065 |
using exp_less_cancel_iff [where x=x and y=0] by simp |
|
1066 |
||
1067 |
lemma one_le_exp_iff [simp]: "1 \<le> exp (x::real) \<longleftrightarrow> 0 \<le> x" |
|
1068 |
using exp_le_cancel_iff [where x=0 and y=x] by simp |
|
1069 |
||
1070 |
lemma exp_le_one_iff [simp]: "exp (x::real) \<le> 1 \<longleftrightarrow> x \<le> 0" |
|
1071 |
using exp_le_cancel_iff [where x=x and y=0] by simp |
|
1072 |
||
1073 |
lemma exp_eq_one_iff [simp]: "exp (x::real) = 1 \<longleftrightarrow> x = 0" |
|
1074 |
using exp_inj_iff [where x=x and y=0] by simp |
|
1075 |
||
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
1076 |
lemma lemma_exp_total: "1 \<le> y ==> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y" |
44755 | 1077 |
proof (rule IVT) |
1078 |
assume "1 \<le> y" |
|
1079 |
hence "0 \<le> y - 1" by simp |
|
1080 |
hence "1 + (y - 1) \<le> exp (y - 1)" by (rule exp_ge_add_one_self_aux) |
|
1081 |
thus "y \<le> exp (y - 1)" by simp |
|
1082 |
qed (simp_all add: le_diff_eq) |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1083 |
|
23115
4615b2078592
generalized exp to work over any complete field; new proof of exp_add
huffman
parents:
23112
diff
changeset
|
1084 |
lemma exp_total: "0 < (y::real) ==> \<exists>x. exp x = y" |
44755 | 1085 |
proof (rule linorder_le_cases [of 1 y]) |
1086 |
assume "1 \<le> y" thus "\<exists>x. exp x = y" |
|
1087 |
by (fast dest: lemma_exp_total) |
|
1088 |
next |
|
1089 |
assume "0 < y" and "y \<le> 1" |
|
1090 |
hence "1 \<le> inverse y" by (simp add: one_le_inverse_iff) |
|
1091 |
then obtain x where "exp x = inverse y" by (fast dest: lemma_exp_total) |
|
1092 |
hence "exp (- x) = y" by (simp add: exp_minus) |
|
1093 |
thus "\<exists>x. exp x = y" .. |
|
1094 |
qed |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1095 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1096 |
|
29164 | 1097 |
subsection {* Natural Logarithm *} |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1098 |
|
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1099 |
definition ln :: "real \<Rightarrow> real" where |
23043 | 1100 |
"ln x = (THE u. exp u = x)" |
1101 |
||
1102 |
lemma ln_exp [simp]: "ln (exp x) = x" |
|
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1103 |
by (simp add: ln_def) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1104 |
|
22654
c2b6b5a9e136
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents:
22653
diff
changeset
|
1105 |
lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x" |
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1106 |
by (auto dest: exp_total) |
22654
c2b6b5a9e136
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
huffman
parents:
22653
diff
changeset
|
1107 |
|
29171 | 1108 |
lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x" |
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1109 |
by (metis exp_gt_zero exp_ln) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1110 |
|
29171 | 1111 |
lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y" |
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1112 |
by (erule subst, rule ln_exp) |
29171 | 1113 |
|
1114 |
lemma ln_one [simp]: "ln 1 = 0" |
|
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1115 |
by (rule ln_unique, simp) |
29171 | 1116 |
|
1117 |
lemma ln_mult: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x * y) = ln x + ln y" |
|
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1118 |
by (rule ln_unique, simp add: exp_add) |
29171 | 1119 |
|
1120 |
lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x" |
|
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1121 |
by (rule ln_unique, simp add: exp_minus) |
29171 | 1122 |
|
1123 |
lemma ln_div: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x / y) = ln x - ln y" |
|
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1124 |
by (rule ln_unique, simp add: exp_diff) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1125 |
|
29171 | 1126 |
lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x" |
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1127 |
by (rule ln_unique, simp add: exp_real_of_nat_mult) |
29171 | 1128 |
|
1129 |
lemma ln_less_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y" |
|
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1130 |
by (subst exp_less_cancel_iff [symmetric], simp) |
29171 | 1131 |
|
1132 |
lemma ln_le_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y" |
|
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1133 |
by (simp add: linorder_not_less [symmetric]) |
29171 | 1134 |
|
1135 |
lemma ln_inj_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y" |
|
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1136 |
by (simp add: order_eq_iff) |
29171 | 1137 |
|
1138 |
lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x" |
|
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1139 |
apply (rule exp_le_cancel_iff [THEN iffD1]) |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1140 |
apply (simp add: exp_ge_add_one_self_aux) |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1141 |
done |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1142 |
|
29171 | 1143 |
lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x" |
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1144 |
by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1145 |
|
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1146 |
lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x" |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1147 |
using ln_le_cancel_iff [of 1 x] by simp |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1148 |
|
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1149 |
lemma ln_ge_zero_imp_ge_one: "\<lbrakk>0 \<le> ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 \<le> x" |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1150 |
using ln_le_cancel_iff [of 1 x] by simp |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1151 |
|
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1152 |
lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> (0 \<le> ln x) = (1 \<le> x)" |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1153 |
using ln_le_cancel_iff [of 1 x] by simp |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1154 |
|
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1155 |
lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x < 0) = (x < 1)" |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1156 |
using ln_less_cancel_iff [of x 1] by simp |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1157 |
|
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1158 |
lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x" |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1159 |
using ln_less_cancel_iff [of 1 x] by simp |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1160 |
|
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1161 |
lemma ln_gt_zero_imp_gt_one: "\<lbrakk>0 < ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 < x" |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1162 |
using ln_less_cancel_iff [of 1 x] by simp |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1163 |
|
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1164 |
lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> (0 < ln x) = (1 < x)" |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1165 |
using ln_less_cancel_iff [of 1 x] by simp |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1166 |
|
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1167 |
lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x = 0) = (x = 1)" |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1168 |
using ln_inj_iff [of x 1] by simp |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1169 |
|
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1170 |
lemma ln_less_zero: "\<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ln x < 0" |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1171 |
by simp |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
1172 |
|
23045
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset
|
1173 |
lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x" |
44308
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1174 |
apply (subgoal_tac "isCont ln (exp (ln x))", simp) |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1175 |
apply (rule isCont_inverse_function [where f=exp], simp_all) |
d2a6f9af02f4
Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman
parents:
44307
diff
changeset
|
1176 |
done |
23045
95e04f335940
add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents:
23043
diff
changeset
|
1177 |
|
45915 | 1178 |
lemma tendsto_ln [tendsto_intros]: |
1179 |
"\<lbrakk>(f ---> a) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F" |
|
1180 |
by (rule isCont_tendsto_compose [OF isCont_ln]) |
|
1181 |
||
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1182 |
lemma continuous_ln: |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1183 |
"continuous F f \<Longrightarrow> 0 < f (Lim F (\<lambda>x. x)) \<Longrightarrow> continuous F (\<lambda>x. ln (f x))" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1184 |
unfolding continuous_def by (rule tendsto_ln) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1185 |
|
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1186 |
lemma isCont_ln' [continuous_intros]: |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1187 |
"continuous (at x) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1188 |
unfolding continuous_at by (rule tendsto_ln) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1189 |
|
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1190 |
lemma continuous_within_ln [continuous_intros]: |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1191 |
"continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1192 |
unfolding continuous_within by (rule tendsto_ln) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1193 |
|
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1194 |
lemma continuous_on_ln [continuous_on_intros]: |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51477
diff
changeset
|
1195 |
"continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; |