author | Manuel Eberl <eberlm@in.tum.de> |
Mon, 21 Aug 2017 20:49:15 +0200 | |
changeset 66480 | 4b8d1df8933b |
child 68046 | 6aba668aea78 |
permissions | -rw-r--r-- |
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1 |
(* |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
2 |
Title: HOL/Analysis/FPS_Convergence.thy |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
3 |
Author: Manuel Eberl, TU München |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
4 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
5 |
Connection of formal power series and actual convergent power series on Banach spaces |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
6 |
(most notably the complex numbers). |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
7 |
*) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
8 |
section \<open>Convergence of formal power series\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
9 |
theory FPS_Convergence |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
10 |
imports |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
11 |
Conformal_Mappings |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
12 |
Generalised_Binomial_Theorem |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
13 |
"HOL-Computational_Algebra.Formal_Power_Series" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
14 |
begin |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
15 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
16 |
subsection \<open>Balls with extended real radius\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
17 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
18 |
text \<open> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
19 |
The following is a variant of @{const ball} that also allows an infinite radius. |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
20 |
\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
21 |
definition eball :: "'a :: metric_space \<Rightarrow> ereal \<Rightarrow> 'a set" where |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
22 |
"eball z r = {z'. ereal (dist z z') < r}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
23 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
24 |
lemma in_eball_iff [simp]: "z \<in> eball z0 r \<longleftrightarrow> ereal (dist z0 z) < r" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
25 |
by (simp add: eball_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
26 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
27 |
lemma eball_ereal [simp]: "eball z (ereal r) = ball z r" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
28 |
by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
29 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
30 |
lemma eball_inf [simp]: "eball z \<infinity> = UNIV" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
31 |
by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
32 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
33 |
lemma eball_empty [simp]: "r \<le> 0 \<Longrightarrow> eball z r = {}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
34 |
proof safe |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
35 |
fix x assume "r \<le> 0" "x \<in> eball z r" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
36 |
hence "dist z x < r" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
37 |
also have "\<dots> \<le> ereal 0" using \<open>r \<le> 0\<close> by (simp add: zero_ereal_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
38 |
finally show "x \<in> {}" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
39 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
40 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
41 |
lemma eball_conv_UNION_balls: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
42 |
"eball z r = (\<Union>r'\<in>{r'. ereal r' < r}. ball z r')" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
43 |
by (cases r) (use dense gt_ex in force)+ |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
44 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
45 |
lemma eball_mono: "r \<le> r' \<Longrightarrow> eball z r \<le> eball z r'" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
46 |
by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
47 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
48 |
lemma ball_eball_mono: "ereal r \<le> r' \<Longrightarrow> ball z r \<le> eball z r'" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
49 |
using eball_mono[of "ereal r" r'] by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
50 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
51 |
lemma open_eball [simp, intro]: "open (eball z r)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
52 |
by (cases r) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
53 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
54 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
55 |
subsection \<open>Basic properties of convergent power series\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
56 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
57 |
definition fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
58 |
"fps_conv_radius f = conv_radius (fps_nth f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
59 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
60 |
definition eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
61 |
"eval_fps f z = (\<Sum>n. fps_nth f n * z ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
62 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
63 |
definition fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
64 |
"fps_expansion f z0 = Abs_fps (\<lambda>n. (deriv ^^ n) f z0 / fact n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
65 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
66 |
lemma norm_summable_fps: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
67 |
fixes f :: "'a :: {banach, real_normed_div_algebra} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
68 |
shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. norm (fps_nth f n * z ^ n))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
69 |
by (rule abs_summable_in_conv_radius) (simp_all add: fps_conv_radius_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
70 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
71 |
lemma summable_fps: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
72 |
fixes f :: "'a :: {banach, real_normed_div_algebra} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
73 |
shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. fps_nth f n * z ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
74 |
by (rule summable_in_conv_radius) (simp_all add: fps_conv_radius_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
75 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
76 |
lemma sums_eval_fps: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
77 |
fixes f :: "'a :: {banach, real_normed_div_algebra} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
78 |
assumes "norm z < fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
79 |
shows "(\<lambda>n. fps_nth f n * z ^ n) sums eval_fps f z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
80 |
using assms unfolding eval_fps_def fps_conv_radius_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
81 |
by (intro summable_sums summable_in_conv_radius) simp_all |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
82 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
83 |
lemma |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
84 |
fixes r :: ereal |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
85 |
assumes "f holomorphic_on eball z0 r" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
86 |
shows conv_radius_fps_expansion: "fps_conv_radius (fps_expansion f z0) \<ge> r" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
87 |
and eval_fps_expansion: "\<And>z. z \<in> eball z0 r \<Longrightarrow> eval_fps (fps_expansion f z0) (z - z0) = f z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
88 |
and eval_fps_expansion': "\<And>z. norm z < r \<Longrightarrow> eval_fps (fps_expansion f z0) z = f (z0 + z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
89 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
90 |
have "(\<lambda>n. fps_nth (fps_expansion f z0) n * (z - z0) ^ n) sums f z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
91 |
if "z \<in> ball z0 r'" "ereal r' < r" for z r' |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
92 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
93 |
from that(2) have "ereal r' \<le> r" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
94 |
from assms(1) and this have "f holomorphic_on ball z0 r'" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
95 |
by (rule holomorphic_on_subset[OF _ ball_eball_mono]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
96 |
from holomorphic_power_series [OF this that(1)] |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
97 |
show ?thesis by (simp add: fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
98 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
99 |
hence *: "(\<lambda>n. fps_nth (fps_expansion f z0) n * (z - z0) ^ n) sums f z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
100 |
if "z \<in> eball z0 r" for z |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
101 |
using that by (subst (asm) eball_conv_UNION_balls) blast |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
102 |
show "fps_conv_radius (fps_expansion f z0) \<ge> r" unfolding fps_conv_radius_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
103 |
proof (rule conv_radius_geI_ex) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
104 |
fix r' :: real assume r': "r' > 0" "ereal r' < r" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
105 |
thus "\<exists>z. norm z = r' \<and> summable (\<lambda>n. fps_nth (fps_expansion f z0) n * z ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
106 |
using *[of "z0 + of_real r'"] |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
107 |
by (intro exI[of _ "of_real r'"]) (auto simp: summable_def dist_norm) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
108 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
109 |
show "eval_fps (fps_expansion f z0) (z - z0) = f z" if "z \<in> eball z0 r" for z |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
110 |
using *[OF that] by (simp add: eval_fps_def sums_iff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
111 |
show "eval_fps (fps_expansion f z0) z = f (z0 + z)" if "ereal (norm z) < r" for z |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
112 |
using *[of "z0 + z"] and that by (simp add: eval_fps_def sums_iff dist_norm) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
113 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
114 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
115 |
lemma continuous_on_eval_fps: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
116 |
fixes f :: "'a :: {banach, real_normed_div_algebra} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
117 |
shows "continuous_on (eball 0 (fps_conv_radius f)) (eval_fps f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
118 |
proof (subst continuous_on_eq_continuous_at [OF open_eball], safe) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
119 |
fix x :: 'a assume x: "x \<in> eball 0 (fps_conv_radius f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
120 |
define r where "r = (if fps_conv_radius f = \<infinity> then norm x + 1 else |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
121 |
(norm x + real_of_ereal (fps_conv_radius f)) / 2)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
122 |
have r: "norm x < r \<and> ereal r < fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
123 |
using x by (cases "fps_conv_radius f") |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
124 |
(auto simp: r_def eball_def split: if_splits) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
125 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
126 |
have "continuous_on (cball 0 r) (\<lambda>x. \<Sum>i. fps_nth f i * (x - 0) ^ i)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
127 |
by (rule powser_continuous_suminf) (insert r, auto simp: fps_conv_radius_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
128 |
hence "continuous_on (cball 0 r) (eval_fps f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
129 |
by (simp add: eval_fps_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
130 |
thus "isCont (eval_fps f) x" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
131 |
by (rule continuous_on_interior) (use r in auto) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
132 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
133 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
134 |
lemma continuous_on_eval_fps' [continuous_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
135 |
assumes "continuous_on A g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
136 |
assumes "g ` A \<subseteq> eball 0 (fps_conv_radius f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
137 |
shows "continuous_on A (\<lambda>x. eval_fps f (g x))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
138 |
using continuous_on_compose2[OF continuous_on_eval_fps assms] . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
139 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
140 |
lemma has_field_derivative_powser: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
141 |
fixes z :: "'a :: {banach, real_normed_field}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
142 |
assumes "ereal (norm z) < conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
143 |
shows "((\<lambda>z. \<Sum>n. f n * z ^ n) has_field_derivative (\<Sum>n. diffs f n * z ^ n)) (at z within A)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
144 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
145 |
define K where "K = (if conv_radius f = \<infinity> then norm z + 1 |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
146 |
else (norm z + real_of_ereal (conv_radius f)) / 2)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
147 |
have K: "norm z < K \<and> ereal K < conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
148 |
using assms by (cases "conv_radius f") (auto simp: K_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
149 |
have "0 \<le> norm z" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
150 |
also from K have "\<dots> < K" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
151 |
finally have K_pos: "K > 0" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
152 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
153 |
have "summable (\<lambda>n. f n * of_real K ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
154 |
using K and K_pos by (intro summable_in_conv_radius) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
155 |
moreover from K and K_pos have "norm z < norm (of_real K :: 'a)" by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
156 |
ultimately show ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
157 |
by (rule has_field_derivative_at_within [OF termdiffs_strong]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
158 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
159 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
160 |
lemma has_field_derivative_eval_fps: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
161 |
fixes z :: "'a :: {banach, real_normed_field}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
162 |
assumes "norm z < fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
163 |
shows "(eval_fps f has_field_derivative eval_fps (fps_deriv f) z) (at z within A)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
164 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
165 |
have "(eval_fps f has_field_derivative eval_fps (Abs_fps (diffs (fps_nth f))) z) (at z within A)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
166 |
using assms unfolding eval_fps_def fps_nth_Abs_fps fps_conv_radius_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
167 |
by (intro has_field_derivative_powser) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
168 |
also have "Abs_fps (diffs (fps_nth f)) = fps_deriv f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
169 |
by (simp add: fps_eq_iff diffs_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
170 |
finally show ?thesis . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
171 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
172 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
173 |
lemma holomorphic_on_eval_fps [holomorphic_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
174 |
fixes z :: "'a :: {banach, real_normed_field}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
175 |
assumes "A \<subseteq> eball 0 (fps_conv_radius f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
176 |
shows "eval_fps f holomorphic_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
177 |
proof (rule holomorphic_on_subset [OF _ assms]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
178 |
show "eval_fps f holomorphic_on eball 0 (fps_conv_radius f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
179 |
proof (subst holomorphic_on_open [OF open_eball], safe, goal_cases) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
180 |
case (1 x) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
181 |
thus ?case |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
182 |
by (intro exI[of _ "eval_fps (fps_deriv f) x"]) (auto intro: has_field_derivative_eval_fps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
183 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
184 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
185 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
186 |
lemma analytic_on_eval_fps: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
187 |
fixes z :: "'a :: {banach, real_normed_field}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
188 |
assumes "A \<subseteq> eball 0 (fps_conv_radius f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
189 |
shows "eval_fps f analytic_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
190 |
proof (rule analytic_on_subset [OF _ assms]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
191 |
show "eval_fps f analytic_on eball 0 (fps_conv_radius f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
192 |
using holomorphic_on_eval_fps[of "eball 0 (fps_conv_radius f)"] |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
193 |
by (subst analytic_on_open) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
194 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
195 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
196 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
197 |
subsection \<open>Lower bounds on radius of convergence\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
198 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
199 |
lemma fps_conv_radius_deriv: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
200 |
fixes f :: "'a :: {banach, real_normed_field} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
201 |
shows "fps_conv_radius (fps_deriv f) \<ge> fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
202 |
unfolding fps_conv_radius_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
203 |
proof (rule conv_radius_geI_ex) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
204 |
fix r :: real assume r: "r > 0" "ereal r < conv_radius (fps_nth f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
205 |
define K where "K = (if conv_radius (fps_nth f) = \<infinity> then r + 1 |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
206 |
else (real_of_ereal (conv_radius (fps_nth f)) + r) / 2)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
207 |
have K: "r < K \<and> ereal K < conv_radius (fps_nth f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
208 |
using r by (cases "conv_radius (fps_nth f)") (auto simp: K_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
209 |
have "summable (\<lambda>n. diffs (fps_nth f) n * of_real r ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
210 |
proof (rule termdiff_converges) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
211 |
fix x :: 'a assume "norm x < K" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
212 |
hence "ereal (norm x) < ereal K" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
213 |
also have "\<dots> < conv_radius (fps_nth f)" using K by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
214 |
finally show "summable (\<lambda>n. fps_nth f n * x ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
215 |
by (intro summable_in_conv_radius) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
216 |
qed (insert K r, auto) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
217 |
also have "\<dots> = (\<lambda>n. fps_nth (fps_deriv f) n * of_real r ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
218 |
by (simp add: fps_deriv_def diffs_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
219 |
finally show "\<exists>z::'a. norm z = r \<and> summable (\<lambda>n. fps_nth (fps_deriv f) n * z ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
220 |
using r by (intro exI[of _ "of_real r"]) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
221 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
222 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
223 |
lemma eval_fps_at_0: "eval_fps f 0 = fps_nth f 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
224 |
by (simp add: eval_fps_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
225 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
226 |
lemma fps_conv_radius_norm [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
227 |
"fps_conv_radius (Abs_fps (\<lambda>n. norm (fps_nth f n))) = fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
228 |
by (simp add: fps_conv_radius_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
229 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
230 |
lemma fps_conv_radius_const [simp]: "fps_conv_radius (fps_const c) = \<infinity>" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
231 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
232 |
have "fps_conv_radius (fps_const c) = conv_radius (\<lambda>_. 0 :: 'a)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
233 |
unfolding fps_conv_radius_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
234 |
by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of 0]]) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
235 |
thus ?thesis by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
236 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
237 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
238 |
lemma fps_conv_radius_0 [simp]: "fps_conv_radius 0 = \<infinity>" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
239 |
by (simp only: fps_const_0_eq_0 [symmetric] fps_conv_radius_const) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
240 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
241 |
lemma fps_conv_radius_1 [simp]: "fps_conv_radius 1 = \<infinity>" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
242 |
by (simp only: fps_const_1_eq_1 [symmetric] fps_conv_radius_const) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
243 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
244 |
lemma fps_conv_radius_numeral [simp]: "fps_conv_radius (numeral n) = \<infinity>" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
245 |
by (simp add: numeral_fps_const) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
246 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
247 |
lemma fps_conv_radius_fps_X_power [simp]: "fps_conv_radius (fps_X ^ n) = \<infinity>" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
248 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
249 |
have "fps_conv_radius (fps_X ^ n :: 'a fps) = conv_radius (\<lambda>_. 0 :: 'a)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
250 |
unfolding fps_conv_radius_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
251 |
by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of n]]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
252 |
(auto simp: fps_X_power_iff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
253 |
thus ?thesis by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
254 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
255 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
256 |
lemma fps_conv_radius_fps_X [simp]: "fps_conv_radius fps_X = \<infinity>" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
257 |
using fps_conv_radius_fps_X_power[of 1] by (simp only: power_one_right) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
258 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
259 |
lemma fps_conv_radius_shift [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
260 |
"fps_conv_radius (fps_shift n f) = fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
261 |
by (simp add: fps_conv_radius_def fps_shift_def conv_radius_shift) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
262 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
263 |
lemma fps_conv_radius_cmult_left: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
264 |
"c \<noteq> 0 \<Longrightarrow> fps_conv_radius (fps_const c * f) = fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
265 |
unfolding fps_conv_radius_def by (simp add: conv_radius_cmult_left) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
266 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
267 |
lemma fps_conv_radius_cmult_right: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
268 |
"c \<noteq> 0 \<Longrightarrow> fps_conv_radius (f * fps_const c) = fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
269 |
unfolding fps_conv_radius_def by (simp add: conv_radius_cmult_right) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
270 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
271 |
lemma fps_conv_radius_uminus [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
272 |
"fps_conv_radius (-f) = fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
273 |
using fps_conv_radius_cmult_left[of "-1" f] |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
274 |
by (simp add: fps_const_neg [symmetric] del: fps_const_neg) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
275 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
276 |
lemma fps_conv_radius_add: "fps_conv_radius (f + g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
277 |
unfolding fps_conv_radius_def using conv_radius_add_ge[of "fps_nth f" "fps_nth g"] |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
278 |
by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
279 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
280 |
lemma fps_conv_radius_diff: "fps_conv_radius (f - g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
281 |
using fps_conv_radius_add[of f "-g"] by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
282 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
283 |
lemma fps_conv_radius_mult: "fps_conv_radius (f * g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
284 |
using conv_radius_mult_ge[of "fps_nth f" "fps_nth g"] |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
285 |
by (simp add: fps_mult_nth fps_conv_radius_def atLeast0AtMost) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
286 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
287 |
lemma fps_conv_radius_power: "fps_conv_radius (f ^ n) \<ge> fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
288 |
proof (induction n) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
289 |
case (Suc n) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
290 |
hence "fps_conv_radius f \<le> min (fps_conv_radius f) (fps_conv_radius (f ^ n))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
291 |
by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
292 |
also have "\<dots> \<le> fps_conv_radius (f * f ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
293 |
by (rule fps_conv_radius_mult) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
294 |
finally show ?case by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
295 |
qed simp_all |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
296 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
297 |
context |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
298 |
begin |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
299 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
300 |
lemma natfun_inverse_bound: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
301 |
fixes f :: "'a :: {real_normed_field} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
302 |
assumes "fps_nth f 0 = 1" and "\<delta> > 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
303 |
and summable: "summable (\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
304 |
and le: "(\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) \<le> 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
305 |
shows "norm (natfun_inverse f n) \<le> inverse (\<delta> ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
306 |
proof (induction n rule: less_induct) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
307 |
case (less m) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
308 |
show ?case |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
309 |
proof (cases m) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
310 |
case 0 |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
311 |
thus ?thesis using assms by (simp add: divide_simps norm_inverse norm_divide) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
312 |
next |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
313 |
case [simp]: (Suc n) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
314 |
have "norm (natfun_inverse f (Suc n)) = |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
315 |
norm (\<Sum>i = Suc 0..Suc n. fps_nth f i * natfun_inverse f (Suc n - i))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
316 |
(is "_ = norm ?S") using assms |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
317 |
by (simp add: field_simps norm_mult norm_divide del: sum_cl_ivl_Suc) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
318 |
also have "norm ?S \<le> (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i * natfun_inverse f (Suc n - i)))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
319 |
by (rule norm_sum) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
320 |
also have "\<dots> \<le> (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) / \<delta> ^ (Suc n - i))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
321 |
proof (intro sum_mono, goal_cases) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
322 |
case (1 i) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
323 |
have "norm (fps_nth f i * natfun_inverse f (Suc n - i)) = |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
324 |
norm (fps_nth f i) * norm (natfun_inverse f (Suc n - i))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
325 |
by (simp add: norm_mult) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
326 |
also have "\<dots> \<le> norm (fps_nth f i) * inverse (\<delta> ^ (Suc n - i))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
327 |
using 1 by (intro mult_left_mono less.IH) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
328 |
also have "\<dots> = norm (fps_nth f i) / \<delta> ^ (Suc n - i)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
329 |
by (simp add: divide_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
330 |
finally show ?case . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
331 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
332 |
also have "\<dots> = (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) * \<delta> ^ i) / \<delta> ^ Suc n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
333 |
by (subst sum_divide_distrib, rule sum.cong) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
334 |
(insert \<open>\<delta> > 0\<close>, auto simp: field_simps power_diff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
335 |
also have "(\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) * \<delta> ^ i) = |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
336 |
(\<Sum>i=0..n. norm (fps_nth f (Suc i)) * \<delta> ^ (Suc i))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
337 |
by (subst sum.atLeast_Suc_atMost_Suc_shift) simp_all |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
338 |
also have "{0..n} = {..<Suc n}" by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
339 |
also have "(\<Sum>i< Suc n. norm (fps_nth f (Suc i)) * \<delta> ^ (Suc i)) \<le> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
340 |
(\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ (Suc n))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
341 |
using \<open>\<delta> > 0\<close> by (intro sum_le_suminf ballI mult_nonneg_nonneg zero_le_power summable) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
342 |
also have "\<dots> \<le> 1" by fact |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
343 |
finally show ?thesis using \<open>\<delta> > 0\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
344 |
by (simp add: divide_right_mono divide_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
345 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
346 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
347 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
348 |
private lemma fps_conv_radius_inverse_pos_aux: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
349 |
fixes f :: "'a :: {banach, real_normed_field} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
350 |
assumes "fps_nth f 0 = 1" "fps_conv_radius f > 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
351 |
shows "fps_conv_radius (inverse f) > 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
352 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
353 |
let ?R = "fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
354 |
define h where "h = Abs_fps (\<lambda>n. norm (fps_nth f n))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
355 |
have [simp]: "fps_conv_radius h = ?R" by (simp add: h_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
356 |
have "continuous_on (eball 0 (fps_conv_radius h)) (eval_fps h)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
357 |
by (intro continuous_on_eval_fps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
358 |
hence *: "open (eval_fps h -` A \<inter> eball 0 ?R)" if "open A" for A |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
359 |
using that by (subst (asm) continuous_on_open_vimage) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
360 |
have "open (eval_fps h -` {..<2} \<inter> eball 0 ?R)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
361 |
by (rule *) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
362 |
moreover have "0 \<in> eval_fps h -` {..<2} \<inter> eball 0 ?R" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
363 |
using assms by (auto simp: eball_def zero_ereal_def eval_fps_at_0 h_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
364 |
ultimately obtain \<epsilon> where \<epsilon>: "\<epsilon> > 0" "ball 0 \<epsilon> \<subseteq> eval_fps h -` {..<2} \<inter> eball 0 ?R" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
365 |
by (subst (asm) open_contains_ball_eq) blast+ |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
366 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
367 |
define \<delta> where "\<delta> = real_of_ereal (min (ereal \<epsilon> / 2) (?R / 2))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
368 |
have \<delta>: "0 < \<delta> \<and> \<delta> < \<epsilon> \<and> ereal \<delta> < ?R" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
369 |
using \<open>\<epsilon> > 0\<close> and assms by (cases ?R) (auto simp: \<delta>_def min_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
370 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
371 |
have summable: "summable (\<lambda>n. norm (fps_nth f n) * \<delta> ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
372 |
using \<delta> by (intro summable_in_conv_radius) (simp_all add: fps_conv_radius_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
373 |
hence "(\<lambda>n. norm (fps_nth f n) * \<delta> ^ n) sums eval_fps h \<delta>" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
374 |
by (simp add: eval_fps_def summable_sums h_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
375 |
hence "(\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) sums (eval_fps h \<delta> - 1)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
376 |
by (subst sums_Suc_iff) (auto simp: assms) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
377 |
moreover { |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
378 |
from \<delta> have "\<delta> \<in> ball 0 \<epsilon>" by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
379 |
also have "\<dots> \<subseteq> eval_fps h -` {..<2} \<inter> eball 0 ?R" by fact |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
380 |
finally have "eval_fps h \<delta> < 2" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
381 |
} |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
382 |
ultimately have le: "(\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) \<le> 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
383 |
by (simp add: sums_iff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
384 |
from summable have summable: "summable (\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
385 |
by (subst summable_Suc_iff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
386 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
387 |
have "0 < \<delta>" using \<delta> by blast |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
388 |
also have "\<delta> = inverse (limsup (\<lambda>n. ereal (inverse \<delta>)))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
389 |
using \<delta> by (subst Limsup_const) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
390 |
also have "\<dots> \<le> conv_radius (natfun_inverse f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
391 |
unfolding conv_radius_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
392 |
proof (intro ereal_inverse_antimono Limsup_mono |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
393 |
eventually_mono[OF eventually_gt_at_top[of 0]]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
394 |
fix n :: nat assume n: "n > 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
395 |
have "root n (norm (natfun_inverse f n)) \<le> root n (inverse (\<delta> ^ n))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
396 |
using n assms \<delta> le summable |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
397 |
by (intro real_root_le_mono natfun_inverse_bound) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
398 |
also have "\<dots> = inverse \<delta>" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
399 |
using n \<delta> by (simp add: power_inverse [symmetric] real_root_pos2) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
400 |
finally show "ereal (inverse \<delta>) \<ge> ereal (root n (norm (natfun_inverse f n)))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
401 |
by (subst ereal_less_eq) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
402 |
next |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
403 |
have "0 = limsup (\<lambda>n. 0::ereal)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
404 |
by (rule Limsup_const [symmetric]) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
405 |
also have "\<dots> \<le> limsup (\<lambda>n. ereal (root n (norm (natfun_inverse f n))))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
406 |
by (intro Limsup_mono) (auto simp: real_root_ge_zero) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
407 |
finally show "0 \<le> \<dots>" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
408 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
409 |
also have "\<dots> = fps_conv_radius (inverse f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
410 |
using assms by (simp add: fps_conv_radius_def fps_inverse_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
411 |
finally show ?thesis by (simp add: zero_ereal_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
412 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
413 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
414 |
lemma fps_conv_radius_inverse_pos: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
415 |
fixes f :: "'a :: {banach, real_normed_field} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
416 |
assumes "fps_nth f 0 \<noteq> 0" and "fps_conv_radius f > 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
417 |
shows "fps_conv_radius (inverse f) > 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
418 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
419 |
let ?c = "fps_nth f 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
420 |
have "fps_conv_radius (inverse f) = fps_conv_radius (fps_const ?c * inverse f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
421 |
using assms by (subst fps_conv_radius_cmult_left) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
422 |
also have "fps_const ?c * inverse f = inverse (fps_const (inverse ?c) * f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
423 |
using assms by (simp add: fps_inverse_mult fps_const_inverse) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
424 |
also have "fps_conv_radius \<dots> > 0" using assms |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
425 |
by (intro fps_conv_radius_inverse_pos_aux) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
426 |
(auto simp: fps_conv_radius_cmult_left) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
427 |
finally show ?thesis . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
428 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
429 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
430 |
end |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
431 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
432 |
lemma fps_conv_radius_exp [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
433 |
fixes c :: "'a :: {banach, real_normed_field}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
434 |
shows "fps_conv_radius (fps_exp c) = \<infinity>" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
435 |
unfolding fps_conv_radius_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
436 |
proof (rule conv_radius_inftyI'') |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
437 |
fix z :: 'a |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
438 |
have "(\<lambda>n. norm (c * z) ^ n /\<^sub>R fact n) sums exp (norm (c * z))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
439 |
by (rule exp_converges) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
440 |
also have "(\<lambda>n. norm (c * z) ^ n /\<^sub>R fact n) = (\<lambda>n. norm (fps_nth (fps_exp c) n * z ^ n))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
441 |
by (rule ext) (simp add: norm_divide norm_mult norm_power divide_simps power_mult_distrib) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
442 |
finally have "summable \<dots>" by (simp add: sums_iff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
443 |
thus "summable (\<lambda>n. fps_nth (fps_exp c) n * z ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
444 |
by (rule summable_norm_cancel) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
445 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
446 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
447 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
448 |
subsection \<open>Evaluating power series\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
449 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
450 |
lemma eval_fps_deriv: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
451 |
assumes "norm z < fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
452 |
shows "eval_fps (fps_deriv f) z = deriv (eval_fps f) z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
453 |
by (intro DERIV_imp_deriv [symmetric] has_field_derivative_eval_fps assms) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
454 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
455 |
lemma fps_nth_conv_deriv: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
456 |
fixes f :: "complex fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
457 |
assumes "fps_conv_radius f > 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
458 |
shows "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
459 |
using assms |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
460 |
proof (induction n arbitrary: f) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
461 |
case 0 |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
462 |
thus ?case by (simp add: eval_fps_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
463 |
next |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
464 |
case (Suc n f) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
465 |
have "(deriv ^^ Suc n) (eval_fps f) 0 = (deriv ^^ n) (deriv (eval_fps f)) 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
466 |
unfolding funpow_Suc_right o_def .. |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
467 |
also have "eventually (\<lambda>z::complex. z \<in> eball 0 (fps_conv_radius f)) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
468 |
using Suc.prems by (intro eventually_nhds_in_open) (auto simp: zero_ereal_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
469 |
hence "eventually (\<lambda>z. deriv (eval_fps f) z = eval_fps (fps_deriv f) z) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
470 |
by eventually_elim (simp add: eval_fps_deriv) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
471 |
hence "(deriv ^^ n) (deriv (eval_fps f)) 0 = (deriv ^^ n) (eval_fps (fps_deriv f)) 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
472 |
by (intro higher_deriv_cong_ev refl) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
473 |
also have "\<dots> / fact n = fps_nth (fps_deriv f) n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
474 |
using Suc.prems fps_conv_radius_deriv[of f] |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
475 |
by (intro Suc.IH [symmetric]) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
476 |
also have "\<dots> / of_nat (Suc n) = fps_nth f (Suc n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
477 |
by (simp add: fps_deriv_def del: of_nat_Suc) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
478 |
finally show ?case by (simp add: divide_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
479 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
480 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
481 |
lemma eval_fps_eqD: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
482 |
fixes f g :: "complex fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
483 |
assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
484 |
assumes "eventually (\<lambda>z. eval_fps f z = eval_fps g z) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
485 |
shows "f = g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
486 |
proof (rule fps_ext) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
487 |
fix n :: nat |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
488 |
have "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
489 |
using assms by (intro fps_nth_conv_deriv) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
490 |
also have "(deriv ^^ n) (eval_fps f) 0 = (deriv ^^ n) (eval_fps g) 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
491 |
by (intro higher_deriv_cong_ev refl assms) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
492 |
also have "\<dots> / fact n = fps_nth g n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
493 |
using assms by (intro fps_nth_conv_deriv [symmetric]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
494 |
finally show "fps_nth f n = fps_nth g n" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
495 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
496 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
497 |
lemma eval_fps_const [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
498 |
fixes c :: "'a :: {banach, real_normed_div_algebra}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
499 |
shows "eval_fps (fps_const c) z = c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
500 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
501 |
have "(\<lambda>n::nat. if n \<in> {0} then c else 0) sums (\<Sum>n\<in>{0::nat}. c)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
502 |
by (rule sums_If_finite_set) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
503 |
also have "?this \<longleftrightarrow> (\<lambda>n::nat. fps_nth (fps_const c) n * z ^ n) sums (\<Sum>n\<in>{0::nat}. c)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
504 |
by (intro sums_cong) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
505 |
also have "(\<Sum>n\<in>{0::nat}. c) = c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
506 |
by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
507 |
finally show ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
508 |
by (simp add: eval_fps_def sums_iff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
509 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
510 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
511 |
lemma eval_fps_0 [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
512 |
"eval_fps (0 :: 'a :: {banach, real_normed_div_algebra} fps) z = 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
513 |
by (simp only: fps_const_0_eq_0 [symmetric] eval_fps_const) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
514 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
515 |
lemma eval_fps_1 [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
516 |
"eval_fps (1 :: 'a :: {banach, real_normed_div_algebra} fps) z = 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
517 |
by (simp only: fps_const_1_eq_1 [symmetric] eval_fps_const) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
518 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
519 |
lemma eval_fps_numeral [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
520 |
"eval_fps (numeral n :: 'a :: {banach, real_normed_div_algebra} fps) z = numeral n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
521 |
by (simp only: numeral_fps_const eval_fps_const) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
522 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
523 |
lemma eval_fps_X_power [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
524 |
"eval_fps (fps_X ^ m :: 'a :: {banach, real_normed_div_algebra} fps) z = z ^ m" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
525 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
526 |
have "(\<lambda>n::nat. if n \<in> {m} then z ^ n else 0 :: 'a) sums (\<Sum>n\<in>{m::nat}. z ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
527 |
by (rule sums_If_finite_set) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
528 |
also have "?this \<longleftrightarrow> (\<lambda>n::nat. fps_nth (fps_X ^ m) n * z ^ n) sums (\<Sum>n\<in>{m::nat}. z ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
529 |
by (intro sums_cong) (auto simp: fps_X_power_iff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
530 |
also have "(\<Sum>n\<in>{m::nat}. z ^ n) = z ^ m" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
531 |
by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
532 |
finally show ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
533 |
by (simp add: eval_fps_def sums_iff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
534 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
535 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
536 |
lemma eval_fps_X [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
537 |
"eval_fps (fps_X :: 'a :: {banach, real_normed_div_algebra} fps) z = z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
538 |
using eval_fps_X_power[of 1 z] by (simp only: power_one_right) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
539 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
540 |
lemma eval_fps_minus: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
541 |
fixes f :: "'a :: {banach, real_normed_div_algebra} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
542 |
assumes "norm z < fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
543 |
shows "eval_fps (-f) z = -eval_fps f z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
544 |
using assms unfolding eval_fps_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
545 |
by (subst suminf_minus [symmetric]) (auto intro!: summable_fps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
546 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
547 |
lemma eval_fps_add: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
548 |
fixes f g :: "'a :: {banach, real_normed_div_algebra} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
549 |
assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
550 |
shows "eval_fps (f + g) z = eval_fps f z + eval_fps g z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
551 |
using assms unfolding eval_fps_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
552 |
by (subst suminf_add) (auto simp: ring_distribs intro!: summable_fps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
553 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
554 |
lemma eval_fps_diff: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
555 |
fixes f g :: "'a :: {banach, real_normed_div_algebra} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
556 |
assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
557 |
shows "eval_fps (f - g) z = eval_fps f z - eval_fps g z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
558 |
using assms unfolding eval_fps_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
559 |
by (subst suminf_diff) (auto simp: ring_distribs intro!: summable_fps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
560 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
561 |
lemma eval_fps_mult: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
562 |
fixes f g :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
563 |
assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
564 |
shows "eval_fps (f * g) z = eval_fps f z * eval_fps g z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
565 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
566 |
have "eval_fps f z * eval_fps g z = |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
567 |
(\<Sum>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * (z ^ i * z ^ (k - i)))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
568 |
unfolding eval_fps_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
569 |
proof (subst Cauchy_product) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
570 |
show "summable (\<lambda>k. norm (fps_nth f k * z ^ k))" "summable (\<lambda>k. norm (fps_nth g k * z ^ k))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
571 |
by (rule norm_summable_fps assms)+ |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
572 |
qed (simp_all add: algebra_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
573 |
also have "(\<lambda>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * (z ^ i * z ^ (k - i))) = |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
574 |
(\<lambda>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * z ^ k)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
575 |
by (intro ext sum.cong refl) (simp add: power_add [symmetric]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
576 |
also have "suminf \<dots> = eval_fps (f * g) z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
577 |
by (simp add: eval_fps_def fps_mult_nth atLeast0AtMost sum_distrib_right) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
578 |
finally show ?thesis .. |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
579 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
580 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
581 |
lemma eval_fps_shift: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
582 |
fixes f :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
583 |
assumes "n \<le> subdegree f" "norm z < fps_conv_radius f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
584 |
shows "eval_fps (fps_shift n f) z = (if z = 0 then fps_nth f n else eval_fps f z / z ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
585 |
proof (cases "z = 0") |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
586 |
case False |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
587 |
have "eval_fps (fps_shift n f * fps_X ^ n) z = eval_fps (fps_shift n f) z * z ^ n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
588 |
using assms by (subst eval_fps_mult) simp_all |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
589 |
also from assms have "fps_shift n f * fps_X ^ n = f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
590 |
by (simp add: fps_shift_times_fps_X_power) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
591 |
finally show ?thesis using False by (simp add: field_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
592 |
qed (simp_all add: eval_fps_at_0) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
593 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
594 |
lemma eval_fps_exp [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
595 |
fixes c :: "'a :: {banach, real_normed_field}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
596 |
shows "eval_fps (fps_exp c) z = exp (c * z)" unfolding eval_fps_def exp_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
597 |
by (simp add: eval_fps_def exp_def scaleR_conv_of_real divide_simps power_mult_distrib) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
598 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
599 |
lemma |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
600 |
fixes f :: "complex fps" and r :: ereal |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
601 |
assumes "\<And>z. ereal (norm z) < r \<Longrightarrow> eval_fps f z \<noteq> 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
602 |
shows fps_conv_radius_inverse: "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
603 |
and eval_fps_inverse: "\<And>z. ereal (norm z) < fps_conv_radius f \<Longrightarrow> ereal (norm z) < r \<Longrightarrow> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
604 |
eval_fps (inverse f) z = inverse (eval_fps f z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
605 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
606 |
define R where "R = min (fps_conv_radius f) r" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
607 |
have *: "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f) \<and> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
608 |
(\<forall>z\<in>eball 0 (min (fps_conv_radius f) r). eval_fps (inverse f) z = inverse (eval_fps f z))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
609 |
proof (cases "min r (fps_conv_radius f) > 0") |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
610 |
case True |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
611 |
define f' where "f' = fps_expansion (\<lambda>z. inverse (eval_fps f z)) 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
612 |
have holo: "(\<lambda>z. inverse (eval_fps f z)) holomorphic_on eball 0 (min r (fps_conv_radius f))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
613 |
using assms by (intro holomorphic_intros) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
614 |
from holo have radius: "fps_conv_radius f' \<ge> min r (fps_conv_radius f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
615 |
unfolding f'_def by (rule conv_radius_fps_expansion) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
616 |
have eval_f': "eval_fps f' z = inverse (eval_fps f z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
617 |
if "norm z < fps_conv_radius f" "norm z < r" for z |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
618 |
using that unfolding f'_def by (subst eval_fps_expansion'[OF holo]) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
619 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
620 |
have "f * f' = 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
621 |
proof (rule eval_fps_eqD) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
622 |
from radius and True have "0 < min (fps_conv_radius f) (fps_conv_radius f')" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
623 |
by (auto simp: min_def split: if_splits) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
624 |
also have "\<dots> \<le> fps_conv_radius (f * f')" by (rule fps_conv_radius_mult) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
625 |
finally show "\<dots> > 0" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
626 |
next |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
627 |
from True have "R > 0" by (auto simp: R_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
628 |
hence "eventually (\<lambda>z. z \<in> eball 0 R) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
629 |
by (intro eventually_nhds_in_open) (auto simp: zero_ereal_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
630 |
thus "eventually (\<lambda>z. eval_fps (f * f') z = eval_fps 1 z) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
631 |
proof eventually_elim |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
632 |
case (elim z) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
633 |
hence "eval_fps (f * f') z = eval_fps f z * eval_fps f' z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
634 |
using radius by (intro eval_fps_mult) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
635 |
(auto simp: R_def min_def split: if_splits intro: less_trans) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
636 |
also have "eval_fps f' z = inverse (eval_fps f z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
637 |
using elim by (intro eval_f') (auto simp: R_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
638 |
also from elim have "eval_fps f z \<noteq> 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
639 |
by (intro assms) (auto simp: R_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
640 |
hence "eval_fps f z * inverse (eval_fps f z) = eval_fps 1 z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
641 |
by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
642 |
finally show "eval_fps (f * f') z = eval_fps 1 z" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
643 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
644 |
qed simp_all |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
645 |
hence "f' = inverse f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
646 |
by (intro fps_inverse_unique [symmetric]) (simp_all add: mult_ac) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
647 |
with eval_f' and radius show ?thesis by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
648 |
next |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
649 |
case False |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
650 |
hence *: "eball 0 R = {}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
651 |
by (intro eball_empty) (auto simp: R_def min_def split: if_splits) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
652 |
show ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
653 |
proof safe |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
654 |
from False have "min r (fps_conv_radius f) \<le> 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
655 |
by (simp add: min_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
656 |
also have "0 \<le> fps_conv_radius (inverse f)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
657 |
by (simp add: fps_conv_radius_def conv_radius_nonneg) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
658 |
finally show "min r (fps_conv_radius f) \<le> \<dots>" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
659 |
qed (unfold * [unfolded R_def], auto) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
660 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
661 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
662 |
from * show "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f)" by blast |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
663 |
from * show "eval_fps (inverse f) z = inverse (eval_fps f z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
664 |
if "ereal (norm z) < fps_conv_radius f" "ereal (norm z) < r" for z |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
665 |
using that by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
666 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
667 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
668 |
lemma |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
669 |
fixes f g :: "complex fps" and r :: ereal |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
670 |
defines "R \<equiv> Min {r, fps_conv_radius f, fps_conv_radius g}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
671 |
assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" "r > 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
672 |
assumes nz: "\<And>z. z \<in> eball 0 r \<Longrightarrow> eval_fps g z \<noteq> 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
673 |
shows fps_conv_radius_divide': "fps_conv_radius (f / g) \<ge> R" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
674 |
and eval_fps_divide': |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
675 |
"ereal (norm z) < R \<Longrightarrow> eval_fps (f / g) z = eval_fps f z / eval_fps g z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
676 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
677 |
from nz[of 0] and \<open>r > 0\<close> have nz': "fps_nth g 0 \<noteq> 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
678 |
by (auto simp: eval_fps_at_0 zero_ereal_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
679 |
have "R \<le> min r (fps_conv_radius g)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
680 |
by (auto simp: R_def intro: min.coboundedI2) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
681 |
also have "min r (fps_conv_radius g) \<le> fps_conv_radius (inverse g)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
682 |
by (intro fps_conv_radius_inverse assms) (auto simp: zero_ereal_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
683 |
finally have radius: "fps_conv_radius (inverse g) \<ge> R" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
684 |
have "R \<le> min (fps_conv_radius f) (fps_conv_radius (inverse g))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
685 |
by (intro radius min.boundedI) (auto simp: R_def intro: min.coboundedI1 min.coboundedI2) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
686 |
also have "\<dots> \<le> fps_conv_radius (f * inverse g)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
687 |
by (rule fps_conv_radius_mult) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
688 |
also have "f * inverse g = f / g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
689 |
by (intro fps_divide_unit [symmetric] nz') |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
690 |
finally show "fps_conv_radius (f / g) \<ge> R" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
691 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
692 |
assume z: "ereal (norm z) < R" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
693 |
have "eval_fps (f * inverse g) z = eval_fps f z * eval_fps (inverse g) z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
694 |
using radius by (intro eval_fps_mult less_le_trans[OF z]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
695 |
(auto simp: R_def intro: min.coboundedI1 min.coboundedI2) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
696 |
also have "eval_fps (inverse g) z = inverse (eval_fps g z)" using \<open>r > 0\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
697 |
by (intro eval_fps_inverse[where r = r] less_le_trans[OF z] nz) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
698 |
(auto simp: R_def intro: min.coboundedI1 min.coboundedI2) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
699 |
also have "f * inverse g = f / g" by fact |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
700 |
finally show "eval_fps (f / g) z = eval_fps f z / eval_fps g z" by (simp add: divide_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
701 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
702 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
703 |
lemma |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
704 |
fixes f g :: "complex fps" and r :: ereal |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
705 |
defines "R \<equiv> Min {r, fps_conv_radius f, fps_conv_radius g}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
706 |
assumes "subdegree g \<le> subdegree f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
707 |
assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" "r > 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
708 |
assumes "\<And>z. z \<in> eball 0 r \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> eval_fps g z \<noteq> 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
709 |
shows fps_conv_radius_divide: "fps_conv_radius (f / g) \<ge> R" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
710 |
and eval_fps_divide: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
711 |
"ereal (norm z) < R \<Longrightarrow> c = fps_nth f (subdegree g) / fps_nth g (subdegree g) \<Longrightarrow> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
712 |
eval_fps (f / g) z = (if z = 0 then c else eval_fps f z / eval_fps g z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
713 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
714 |
define f' g' where "f' = fps_shift (subdegree g) f" and "g' = fps_shift (subdegree g) g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
715 |
have f_eq: "f = f' * fps_X ^ subdegree g" and g_eq: "g = g' * fps_X ^ subdegree g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
716 |
unfolding f'_def g'_def by (rule subdegree_decompose' le_refl | fact)+ |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
717 |
have subdegree: "subdegree f' = subdegree f - subdegree g" "subdegree g' = 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
718 |
using assms(2) by (simp_all add: f'_def g'_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
719 |
have [simp]: "fps_conv_radius f' = fps_conv_radius f" "fps_conv_radius g' = fps_conv_radius g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
720 |
by (simp_all add: f'_def g'_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
721 |
have [simp]: "fps_nth f' 0 = fps_nth f (subdegree g)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
722 |
"fps_nth g' 0 = fps_nth g (subdegree g)" by (simp_all add: f'_def g'_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
723 |
have g_nz: "g \<noteq> 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
724 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
725 |
define z :: complex where "z = (if r = \<infinity> then 1 else of_real (real_of_ereal r / 2))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
726 |
from \<open>r > 0\<close> have "z \<in> eball 0 r" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
727 |
by (cases r) (auto simp: z_def eball_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
728 |
moreover have "z \<noteq> 0" using \<open>r > 0\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
729 |
by (cases r) (auto simp: z_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
730 |
ultimately have "eval_fps g z \<noteq> 0" by (rule assms(6)) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
731 |
thus "g \<noteq> 0" by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
732 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
733 |
have fg: "f / g = f' * inverse g'" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
734 |
by (subst f_eq, subst (2) g_eq) (insert g_nz, simp add: fps_divide_unit) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
735 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
736 |
have g'_nz: "eval_fps g' z \<noteq> 0" if z: "norm z < min r (fps_conv_radius g)" for z |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
737 |
proof (cases "z = 0") |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
738 |
case False |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
739 |
with assms and z have "eval_fps g z \<noteq> 0" by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
740 |
also from z have "eval_fps g z = eval_fps g' z * z ^ subdegree g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
741 |
by (subst g_eq) (auto simp: eval_fps_mult) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
742 |
finally show ?thesis by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
743 |
qed (insert \<open>g \<noteq> 0\<close>, auto simp: g'_def eval_fps_at_0) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
744 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
745 |
have "R \<le> min (min r (fps_conv_radius g)) (fps_conv_radius g')" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
746 |
by (auto simp: R_def min.coboundedI1 min.coboundedI2) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
747 |
also have "\<dots> \<le> fps_conv_radius (inverse g')" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
748 |
using g'_nz by (rule fps_conv_radius_inverse) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
749 |
finally have conv_radius_inv: "R \<le> fps_conv_radius (inverse g')" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
750 |
hence "R \<le> fps_conv_radius (f' * inverse g')" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
751 |
by (intro order.trans[OF _ fps_conv_radius_mult]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
752 |
(auto simp: R_def intro: min.coboundedI1 min.coboundedI2) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
753 |
thus "fps_conv_radius (f / g) \<ge> R" by (simp add: fg) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
754 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
755 |
fix z c :: complex assume z: "ereal (norm z) < R" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
756 |
assume c: "c = fps_nth f (subdegree g) / fps_nth g (subdegree g)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
757 |
show "eval_fps (f / g) z = (if z = 0 then c else eval_fps f z / eval_fps g z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
758 |
proof (cases "z = 0") |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
759 |
case False |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
760 |
from z and conv_radius_inv have "ereal (norm z) < fps_conv_radius (inverse g')" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
761 |
by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
762 |
with z have "eval_fps (f / g) z = eval_fps f' z * eval_fps (inverse g') z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
763 |
unfolding fg by (subst eval_fps_mult) (auto simp: R_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
764 |
also have "eval_fps (inverse g') z = inverse (eval_fps g' z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
765 |
using z by (intro eval_fps_inverse[of "min r (fps_conv_radius g')"] g'_nz) (auto simp: R_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
766 |
also have "eval_fps f' z * \<dots> = eval_fps f z / eval_fps g z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
767 |
using z False assms(2) by (simp add: f'_def g'_def eval_fps_shift R_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
768 |
finally show ?thesis using False by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
769 |
qed (simp_all add: eval_fps_at_0 fg field_simps c) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
770 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
771 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
772 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
773 |
subsection \<open>Power series expansion of complex functions\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
774 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
775 |
text \<open> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
776 |
This predicate contains the notion that the given formal power series converges |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
777 |
in some disc of positive radius around the origin and is equal to the given complex |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
778 |
function there. |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
779 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
780 |
This relationship is unique in the sense that no complex function can have more than |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
781 |
one formal power series to which it expands, and if two holomorphic functions that are |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
782 |
holomorphic on a connected open set around the origin and have the same power series |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
783 |
expansion, they must be equal on that set. |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
784 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
785 |
More concrete statements about the radius of convergence can usually be made, but for |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
786 |
many purposes, the statment that the series converges to the function in some neighbourhood |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
787 |
of the origin is enough, and that can be shown almost fully automatically in most cases, |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
788 |
as there are straightforward introduction rules to show this. |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
789 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
790 |
In particular, when one wants to relate the coefficients of the power series to the |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
791 |
values of the derivatives of the function at the origin, or if one wants to approximate |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
792 |
the coefficients of the series with the singularities of the function, this predicate |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
793 |
is enough. |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
794 |
\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
795 |
definition has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
796 |
(infixl "has'_fps'_expansion" 60) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
797 |
where "(f has_fps_expansion F) \<longleftrightarrow> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
798 |
fps_conv_radius F > 0 \<and> eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
799 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
800 |
named_theorems fps_expansion_intros |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
801 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
802 |
lemma fps_nth_fps_expansion: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
803 |
fixes f :: "complex \<Rightarrow> complex" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
804 |
assumes "f has_fps_expansion F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
805 |
shows "fps_nth F n = (deriv ^^ n) f 0 / fact n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
806 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
807 |
have "fps_nth F n = (deriv ^^ n) (eval_fps F) 0 / fact n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
808 |
using assms by (intro fps_nth_conv_deriv) (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
809 |
also have "(deriv ^^ n) (eval_fps F) 0 = (deriv ^^ n) f 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
810 |
using assms by (intro higher_deriv_cong_ev) (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
811 |
finally show ?thesis . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
812 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
813 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
814 |
lemma has_fps_expansion_fps_expansion [intro]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
815 |
assumes "open A" "0 \<in> A" "f holomorphic_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
816 |
shows "f has_fps_expansion fps_expansion f 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
817 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
818 |
from assms(1,2) obtain r where r: "r > 0 " "ball 0 r \<subseteq> A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
819 |
by (auto simp: open_contains_ball) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
820 |
have holo: "f holomorphic_on eball 0 (ereal r)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
821 |
using r(2) and assms(3) by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
822 |
from r(1) have "0 < ereal r" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
823 |
also have "r \<le> fps_conv_radius (fps_expansion f 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
824 |
using holo by (intro conv_radius_fps_expansion) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
825 |
finally have "\<dots> > 0" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
826 |
moreover have "eventually (\<lambda>z. z \<in> ball 0 r) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
827 |
using r(1) by (intro eventually_nhds_in_open) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
828 |
hence "eventually (\<lambda>z. eval_fps (fps_expansion f 0) z = f z) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
829 |
by eventually_elim (subst eval_fps_expansion'[OF holo], auto) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
830 |
ultimately show ?thesis using r(1) by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
831 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
832 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
833 |
lemma has_fps_expansion_const [simp, intro, fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
834 |
"(\<lambda>_. c) has_fps_expansion fps_const c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
835 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
836 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
837 |
lemma has_fps_expansion_0 [simp, intro, fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
838 |
"(\<lambda>_. 0) has_fps_expansion 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
839 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
840 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
841 |
lemma has_fps_expansion_1 [simp, intro, fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
842 |
"(\<lambda>_. 1) has_fps_expansion 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
843 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
844 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
845 |
lemma has_fps_expansion_numeral [simp, intro, fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
846 |
"(\<lambda>_. numeral n) has_fps_expansion numeral n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
847 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
848 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
849 |
lemma has_fps_expansion_fps_X_power [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
850 |
"(\<lambda>x. x ^ n) has_fps_expansion (fps_X ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
851 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
852 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
853 |
lemma has_fps_expansion_fps_X [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
854 |
"(\<lambda>x. x) has_fps_expansion fps_X" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
855 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
856 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
857 |
lemma has_fps_expansion_cmult_left [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
858 |
fixes c :: "'a :: {banach, real_normed_div_algebra, comm_ring_1}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
859 |
assumes "f has_fps_expansion F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
860 |
shows "(\<lambda>x. c * f x) has_fps_expansion fps_const c * F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
861 |
proof (cases "c = 0") |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
862 |
case False |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
863 |
from assms have "eventually (\<lambda>z. z \<in> eball 0 (fps_conv_radius F)) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
864 |
by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
865 |
moreover from assms have "eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
866 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
867 |
ultimately have "eventually (\<lambda>z. eval_fps (fps_const c * F) z = c * f z) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
868 |
by eventually_elim (simp_all add: eval_fps_mult) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
869 |
with assms and False show ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
870 |
by (auto simp: has_fps_expansion_def fps_conv_radius_cmult_left) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
871 |
qed auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
872 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
873 |
lemma has_fps_expansion_cmult_right [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
874 |
fixes c :: "'a :: {banach, real_normed_div_algebra, comm_ring_1}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
875 |
assumes "f has_fps_expansion F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
876 |
shows "(\<lambda>x. f x * c) has_fps_expansion F * fps_const c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
877 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
878 |
have "F * fps_const c = fps_const c * F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
879 |
by (intro fps_ext) (auto simp: mult.commute) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
880 |
with has_fps_expansion_cmult_left [OF assms] show ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
881 |
by (simp add: mult.commute) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
882 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
883 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
884 |
lemma has_fps_expansion_minus [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
885 |
assumes "f has_fps_expansion F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
886 |
shows "(\<lambda>x. - f x) has_fps_expansion -F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
887 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
888 |
from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
889 |
by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
890 |
moreover from assms have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
891 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
892 |
ultimately have "eventually (\<lambda>x. eval_fps (-F) x = -f x) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
893 |
by eventually_elim (auto simp: eval_fps_minus) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
894 |
thus ?thesis using assms by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
895 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
896 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
897 |
lemma has_fps_expansion_add [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
898 |
assumes "f has_fps_expansion F" "g has_fps_expansion G" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
899 |
shows "(\<lambda>x. f x + g x) has_fps_expansion F + G" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
900 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
901 |
from assms have "0 < min (fps_conv_radius F) (fps_conv_radius G)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
902 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
903 |
also have "\<dots> \<le> fps_conv_radius (F + G)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
904 |
by (rule fps_conv_radius_add) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
905 |
finally have radius: "\<dots> > 0" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
906 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
907 |
from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
908 |
"eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius G)) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
909 |
by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+ |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
910 |
moreover have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
911 |
and "eventually (\<lambda>x. eval_fps G x = g x) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
912 |
using assms by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
913 |
ultimately have "eventually (\<lambda>x. eval_fps (F + G) x = f x + g x) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
914 |
by eventually_elim (auto simp: eval_fps_add) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
915 |
with radius show ?thesis by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
916 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
917 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
918 |
lemma has_fps_expansion_diff [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
919 |
assumes "f has_fps_expansion F" "g has_fps_expansion G" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
920 |
shows "(\<lambda>x. f x - g x) has_fps_expansion F - G" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
921 |
using has_fps_expansion_add[of f F "\<lambda>x. - g x" "-G"] assms |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
922 |
by (simp add: has_fps_expansion_minus) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
923 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
924 |
lemma has_fps_expansion_mult [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
925 |
fixes F G :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
926 |
assumes "f has_fps_expansion F" "g has_fps_expansion G" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
927 |
shows "(\<lambda>x. f x * g x) has_fps_expansion F * G" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
928 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
929 |
from assms have "0 < min (fps_conv_radius F) (fps_conv_radius G)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
930 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
931 |
also have "\<dots> \<le> fps_conv_radius (F * G)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
932 |
by (rule fps_conv_radius_mult) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
933 |
finally have radius: "\<dots> > 0" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
934 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
935 |
from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
936 |
"eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius G)) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
937 |
by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+ |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
938 |
moreover have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
939 |
and "eventually (\<lambda>x. eval_fps G x = g x) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
940 |
using assms by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
941 |
ultimately have "eventually (\<lambda>x. eval_fps (F * G) x = f x * g x) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
942 |
by eventually_elim (auto simp: eval_fps_mult) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
943 |
with radius show ?thesis by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
944 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
945 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
946 |
lemma has_fps_expansion_inverse [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
947 |
fixes F :: "'a :: {banach, real_normed_field} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
948 |
assumes "f has_fps_expansion F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
949 |
assumes "fps_nth F 0 \<noteq> 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
950 |
shows "(\<lambda>x. inverse (f x)) has_fps_expansion inverse F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
951 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
952 |
have radius: "fps_conv_radius (inverse F) > 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
953 |
using assms unfolding has_fps_expansion_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
954 |
by (intro fps_conv_radius_inverse_pos) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
955 |
let ?R = "min (fps_conv_radius F) (fps_conv_radius (inverse F))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
956 |
from assms radius |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
957 |
have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
958 |
"eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius (inverse F))) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
959 |
by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+ |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
960 |
moreover have "eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
961 |
using assms by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
962 |
ultimately have "eventually (\<lambda>z. eval_fps (inverse F) z = inverse (f z)) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
963 |
proof eventually_elim |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
964 |
case (elim z) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
965 |
hence "eval_fps (inverse F * F) z = eval_fps (inverse F) z * f z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
966 |
by (subst eval_fps_mult) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
967 |
also have "eval_fps (inverse F * F) z = 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
968 |
using assms by (simp add: inverse_mult_eq_1) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
969 |
finally show ?case by (auto simp: divide_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
970 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
971 |
with radius show ?thesis by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
972 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
973 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
974 |
lemma has_fps_expansion_exp [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
975 |
fixes c :: "'a :: {banach, real_normed_field}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
976 |
shows "(\<lambda>x. exp (c * x)) has_fps_expansion fps_exp c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
977 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
978 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
979 |
lemma has_fps_expansion_exp1 [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
980 |
"(\<lambda>x::'a :: {banach, real_normed_field}. exp x) has_fps_expansion fps_exp 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
981 |
using has_fps_expansion_exp[of 1] by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
982 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
983 |
lemma has_fps_expansion_exp_neg1 [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
984 |
"(\<lambda>x::'a :: {banach, real_normed_field}. exp (-x)) has_fps_expansion fps_exp (-1)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
985 |
using has_fps_expansion_exp[of "-1"] by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
986 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
987 |
lemma has_fps_expansion_deriv [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
988 |
assumes "f has_fps_expansion F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
989 |
shows "deriv f has_fps_expansion fps_deriv F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
990 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
991 |
have "eventually (\<lambda>z. z \<in> eball 0 (fps_conv_radius F)) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
992 |
using assms by (intro eventually_nhds_in_open) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
993 |
(auto simp: has_fps_expansion_def zero_ereal_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
994 |
moreover from assms have "eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
995 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
996 |
then obtain s where "open s" "0 \<in> s" and s: "\<And>w. w \<in> s \<Longrightarrow> eval_fps F w = f w" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
997 |
by (auto simp: eventually_nhds) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
998 |
hence "eventually (\<lambda>w. w \<in> s) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
999 |
by (intro eventually_nhds_in_open) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1000 |
ultimately have "eventually (\<lambda>z. eval_fps (fps_deriv F) z = deriv f z) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1001 |
proof eventually_elim |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1002 |
case (elim z) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1003 |
hence "eval_fps (fps_deriv F) z = deriv (eval_fps F) z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1004 |
by (simp add: eval_fps_deriv) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1005 |
also have "eventually (\<lambda>w. w \<in> s) (nhds z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1006 |
using elim and \<open>open s\<close> by (intro eventually_nhds_in_open) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1007 |
hence "eventually (\<lambda>w. eval_fps F w = f w) (nhds z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1008 |
by eventually_elim (simp add: s) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1009 |
hence "deriv (eval_fps F) z = deriv f z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1010 |
by (intro deriv_cong_ev refl) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1011 |
finally show ?case . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1012 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1013 |
with assms and fps_conv_radius_deriv[of F] show ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1014 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1015 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1016 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1017 |
lemma fps_conv_radius_binomial: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1018 |
fixes c :: "'a :: {real_normed_field,banach}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1019 |
shows "fps_conv_radius (fps_binomial c) = (if c \<in> \<nat> then \<infinity> else 1)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1020 |
unfolding fps_conv_radius_def by (simp add: conv_radius_gchoose) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1021 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1022 |
lemma fps_conv_radius_ln: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1023 |
fixes c :: "'a :: {banach, real_normed_field, field_char_0}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1024 |
shows "fps_conv_radius (fps_ln c) = (if c = 0 then \<infinity> else 1)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1025 |
proof (cases "c = 0") |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1026 |
case False |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1027 |
have "conv_radius (\<lambda>n. 1 / of_nat n :: 'a) = 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1028 |
proof (rule conv_radius_ratio_limit_nonzero) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1029 |
show "(\<lambda>n. norm (1 / of_nat n :: 'a) / norm (1 / of_nat (Suc n) :: 'a)) \<longlonglongrightarrow> 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1030 |
using LIMSEQ_Suc_n_over_n by (simp add: norm_divide del: of_nat_Suc) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1031 |
qed auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1032 |
also have "conv_radius (\<lambda>n. 1 / of_nat n :: 'a) = |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1033 |
conv_radius (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n :: 'a)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1034 |
by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of 0]]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1035 |
(simp add: norm_mult norm_divide norm_power) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1036 |
finally show ?thesis using False unfolding fps_ln_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1037 |
by (subst fps_conv_radius_cmult_left) (simp_all add: fps_conv_radius_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1038 |
qed (auto simp: fps_ln_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1039 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1040 |
lemma fps_conv_radius_ln_nonzero [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1041 |
assumes "c \<noteq> (0 :: 'a :: {banach,real_normed_field,field_char_0})" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1042 |
shows "fps_conv_radius (fps_ln c) = 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1043 |
using assms by (simp add: fps_conv_radius_ln) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1044 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1045 |
lemma fps_conv_radius_sin [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1046 |
fixes c :: "'a :: {banach, real_normed_field, field_char_0}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1047 |
shows "fps_conv_radius (fps_sin c) = \<infinity>" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1048 |
proof (cases "c = 0") |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1049 |
case False |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1050 |
have "\<infinity> = conv_radius (\<lambda>n. of_real (sin_coeff n) :: 'a)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1051 |
proof (rule sym, rule conv_radius_inftyI'', rule summable_norm_cancel, goal_cases) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1052 |
case (1 z) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1053 |
show ?case using summable_norm_sin[of z] by (simp add: norm_mult) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1054 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1055 |
also have "\<dots> / norm c = conv_radius (\<lambda>n. c ^ n * of_real (sin_coeff n) :: 'a)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1056 |
using False by (subst conv_radius_mult_power) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1057 |
also have "\<dots> = fps_conv_radius (fps_sin c)" unfolding fps_conv_radius_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1058 |
by (rule conv_radius_cong_weak) (auto simp add: fps_sin_def sin_coeff_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1059 |
finally show ?thesis by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1060 |
qed simp_all |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1061 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1062 |
lemma fps_conv_radius_cos [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1063 |
fixes c :: "'a :: {banach, real_normed_field, field_char_0}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1064 |
shows "fps_conv_radius (fps_cos c) = \<infinity>" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1065 |
proof (cases "c = 0") |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1066 |
case False |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1067 |
have "\<infinity> = conv_radius (\<lambda>n. of_real (cos_coeff n) :: 'a)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1068 |
proof (rule sym, rule conv_radius_inftyI'', rule summable_norm_cancel, goal_cases) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1069 |
case (1 z) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1070 |
show ?case using summable_norm_cos[of z] by (simp add: norm_mult) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1071 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1072 |
also have "\<dots> / norm c = conv_radius (\<lambda>n. c ^ n * of_real (cos_coeff n) :: 'a)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1073 |
using False by (subst conv_radius_mult_power) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1074 |
also have "\<dots> = fps_conv_radius (fps_cos c)" unfolding fps_conv_radius_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1075 |
by (rule conv_radius_cong_weak) (auto simp add: fps_cos_def cos_coeff_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1076 |
finally show ?thesis by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1077 |
qed simp_all |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1078 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1079 |
lemma eval_fps_sin [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1080 |
fixes z :: "'a :: {banach, real_normed_field, field_char_0}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1081 |
shows "eval_fps (fps_sin c) z = sin (c * z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1082 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1083 |
have "(\<lambda>n. sin_coeff n *\<^sub>R (c * z) ^ n) sums sin (c * z)" by (rule sin_converges) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1084 |
also have "(\<lambda>n. sin_coeff n *\<^sub>R (c * z) ^ n) = (\<lambda>n. fps_nth (fps_sin c) n * z ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1085 |
by (rule ext) (auto simp: sin_coeff_def fps_sin_def power_mult_distrib scaleR_conv_of_real) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1086 |
finally show ?thesis by (simp add: sums_iff eval_fps_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1087 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1088 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1089 |
lemma eval_fps_cos [simp]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1090 |
fixes z :: "'a :: {banach, real_normed_field, field_char_0}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1091 |
shows "eval_fps (fps_cos c) z = cos (c * z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1092 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1093 |
have "(\<lambda>n. cos_coeff n *\<^sub>R (c * z) ^ n) sums cos (c * z)" by (rule cos_converges) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1094 |
also have "(\<lambda>n. cos_coeff n *\<^sub>R (c * z) ^ n) = (\<lambda>n. fps_nth (fps_cos c) n * z ^ n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1095 |
by (rule ext) (auto simp: cos_coeff_def fps_cos_def power_mult_distrib scaleR_conv_of_real) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1096 |
finally show ?thesis by (simp add: sums_iff eval_fps_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1097 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1098 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1099 |
lemma cos_eq_zero_imp_norm_ge: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1100 |
assumes "cos (z :: complex) = 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1101 |
shows "norm z \<ge> pi / 2" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1102 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1103 |
from assms obtain n where "z = complex_of_real ((of_int n + 1 / 2) * pi)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1104 |
by (auto simp: cos_eq_0 algebra_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1105 |
also have "norm \<dots> = \<bar>real_of_int n + 1 / 2\<bar> * pi" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1106 |
by (subst norm_of_real) (simp_all add: abs_mult) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1107 |
also have "real_of_int n + 1 / 2 = of_int (2 * n + 1) / 2" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1108 |
also have "\<bar>\<dots>\<bar> = of_int \<bar>2 * n + 1\<bar> / 2" by (subst abs_divide) simp_all |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1109 |
also have "\<dots> * pi = of_int \<bar>2 * n + 1\<bar> * (pi / 2)" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1110 |
also have "\<dots> \<ge> of_int 1 * (pi / 2)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1111 |
by (intro mult_right_mono, subst of_int_le_iff) (auto simp: abs_if) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1112 |
finally show ?thesis by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1113 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1114 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1115 |
lemma fps_conv_radius_tan: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1116 |
fixes c :: complex |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1117 |
assumes "c \<noteq> 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1118 |
shows "fps_conv_radius (fps_tan c) \<ge> pi / (2 * norm c)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1119 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1120 |
have "fps_conv_radius (fps_tan c) \<ge> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1121 |
Min {pi / (2 * norm c), fps_conv_radius (fps_sin c), fps_conv_radius (fps_cos c)}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1122 |
unfolding fps_tan_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1123 |
proof (rule fps_conv_radius_divide) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1124 |
fix z :: complex assume "z \<in> eball 0 (pi / (2 * norm c))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1125 |
with cos_eq_zero_imp_norm_ge[of "c*z"] assms |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1126 |
show "eval_fps (fps_cos c) z \<noteq> 0" by (auto simp: norm_mult field_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1127 |
qed (insert assms, auto) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1128 |
thus ?thesis by (simp add: min_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1129 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1130 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1131 |
lemma eval_fps_tan: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1132 |
fixes c :: complex |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1133 |
assumes "norm z < pi / (2 * norm c)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1134 |
shows "eval_fps (fps_tan c) z = tan (c * z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1135 |
proof (cases "c = 0") |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1136 |
case False |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1137 |
show ?thesis unfolding fps_tan_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1138 |
proof (subst eval_fps_divide'[where r = "pi / (2 * norm c)"]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1139 |
fix z :: complex assume "z \<in> eball 0 (pi / (2 * norm c))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1140 |
with cos_eq_zero_imp_norm_ge[of "c*z"] assms |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1141 |
show "eval_fps (fps_cos c) z \<noteq> 0" using False by (auto simp: norm_mult field_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1142 |
qed (insert False assms, auto simp: field_simps tan_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1143 |
qed simp_all |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1144 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1145 |
lemma eval_fps_binomial: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1146 |
fixes c :: complex |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1147 |
assumes "norm z < 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1148 |
shows "eval_fps (fps_binomial c) z = (1 + z) powr c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1149 |
using gen_binomial_complex[OF assms] by (simp add: sums_iff eval_fps_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1150 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1151 |
lemma has_fps_expansion_binomial_complex [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1152 |
fixes c :: complex |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1153 |
shows "(\<lambda>x. (1 + x) powr c) has_fps_expansion fps_binomial c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1154 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1155 |
have *: "eventually (\<lambda>z::complex. z \<in> eball 0 1) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1156 |
by (intro eventually_nhds_in_open) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1157 |
thus ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1158 |
by (auto simp: has_fps_expansion_def eval_fps_binomial fps_conv_radius_binomial |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1159 |
intro!: eventually_mono [OF *]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1160 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1161 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1162 |
lemma has_fps_expansion_sin [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1163 |
fixes c :: "'a :: {banach, real_normed_field, field_char_0}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1164 |
shows "(\<lambda>x. sin (c * x)) has_fps_expansion fps_sin c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1165 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1166 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1167 |
lemma has_fps_expansion_sin' [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1168 |
"(\<lambda>x::'a :: {banach, real_normed_field}. sin x) has_fps_expansion fps_sin 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1169 |
using has_fps_expansion_sin[of 1] by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1170 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1171 |
lemma has_fps_expansion_cos [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1172 |
fixes c :: "'a :: {banach, real_normed_field, field_char_0}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1173 |
shows "(\<lambda>x. cos (c * x)) has_fps_expansion fps_cos c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1174 |
by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1175 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1176 |
lemma has_fps_expansion_cos' [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1177 |
"(\<lambda>x::'a :: {banach, real_normed_field}. cos x) has_fps_expansion fps_cos 1" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1178 |
using has_fps_expansion_cos[of 1] by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1179 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1180 |
lemma has_fps_expansion_shift [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1181 |
fixes F :: "'a :: {banach, real_normed_field} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1182 |
assumes "f has_fps_expansion F" and "n \<le> subdegree F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1183 |
assumes "c = fps_nth F n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1184 |
shows "(\<lambda>x. if x = 0 then c else f x / x ^ n) has_fps_expansion (fps_shift n F)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1185 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1186 |
have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1187 |
using assms by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1188 |
moreover have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1189 |
using assms by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1190 |
ultimately have "eventually (\<lambda>x. eval_fps (fps_shift n F) x = |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1191 |
(if x = 0 then c else f x / x ^ n)) (nhds 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1192 |
by eventually_elim (auto simp: eval_fps_shift assms) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1193 |
with assms show ?thesis by (auto simp: has_fps_expansion_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1194 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1195 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1196 |
lemma has_fps_expansion_divide [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1197 |
fixes F G :: "'a :: {banach, real_normed_field} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1198 |
assumes "f has_fps_expansion F" and "g has_fps_expansion G" and |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1199 |
"subdegree G \<le> subdegree F" "G \<noteq> 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1200 |
"c = fps_nth F (subdegree G) / fps_nth G (subdegree G)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1201 |
shows "(\<lambda>x. if x = 0 then c else f x / g x) has_fps_expansion (F / G)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1202 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1203 |
define n where "n = subdegree G" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1204 |
define F' and G' where "F' = fps_shift n F" and "G' = fps_shift n G" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1205 |
have "F = F' * fps_X ^ n" "G = G' * fps_X ^ n" unfolding F'_def G'_def n_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1206 |
by (rule fps_shift_times_fps_X_power [symmetric] le_refl | fact)+ |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1207 |
moreover from assms have "fps_nth G' 0 \<noteq> 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1208 |
by (simp add: G'_def n_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1209 |
ultimately have FG: "F / G = F' * inverse G'" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1210 |
by (simp add: fps_divide_unit) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1211 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1212 |
have "(\<lambda>x. (if x = 0 then fps_nth F n else f x / x ^ n) * |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1213 |
inverse (if x = 0 then fps_nth G n else g x / x ^ n)) has_fps_expansion F / G" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1214 |
(is "?h has_fps_expansion _") unfolding FG F'_def G'_def n_def using \<open>G \<noteq> 0\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1215 |
by (intro has_fps_expansion_mult has_fps_expansion_inverse |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1216 |
has_fps_expansion_shift assms) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1217 |
also have "?h = (\<lambda>x. if x = 0 then c else f x / g x)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1218 |
using assms(5) unfolding n_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1219 |
by (intro ext) (auto split: if_splits simp: field_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1220 |
finally show ?thesis . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1221 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1222 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1223 |
lemma has_fps_expansion_divide' [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1224 |
fixes F G :: "'a :: {banach, real_normed_field} fps" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1225 |
assumes "f has_fps_expansion F" and "g has_fps_expansion G" and "fps_nth G 0 \<noteq> 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1226 |
shows "(\<lambda>x. f x / g x) has_fps_expansion (F / G)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1227 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1228 |
have "(\<lambda>x. if x = 0 then fps_nth F 0 / fps_nth G 0 else f x / g x) has_fps_expansion (F / G)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1229 |
(is "?h has_fps_expansion _") using assms(3) by (intro has_fps_expansion_divide assms) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1230 |
also from assms have "fps_nth F 0 = f 0" "fps_nth G 0 = g 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1231 |
by (auto simp: has_fps_expansion_def eval_fps_at_0 dest: eventually_nhds_x_imp_x) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1232 |
hence "?h = (\<lambda>x. f x / g x)" by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1233 |
finally show ?thesis . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1234 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1235 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1236 |
lemma has_fps_expansion_tan [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1237 |
fixes c :: "'a :: {banach, real_normed_field, field_char_0}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1238 |
shows "(\<lambda>x. tan (c * x)) has_fps_expansion fps_tan c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1239 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1240 |
have "(\<lambda>x. sin (c * x) / cos (c * x)) has_fps_expansion fps_sin c / fps_cos c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1241 |
by (intro fps_expansion_intros) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1242 |
thus ?thesis by (simp add: tan_def fps_tan_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1243 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1244 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1245 |
lemma has_fps_expansion_tan' [fps_expansion_intros]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1246 |
"tan has_fps_expansion fps_tan (1 :: 'a :: {banach, real_normed_field, field_char_0})" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1247 |
using has_fps_expansion_tan[of 1] by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1248 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1249 |
lemma has_fps_expansion_imp_holomorphic: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1250 |
assumes "f has_fps_expansion F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1251 |
obtains s where "open s" "0 \<in> s" "f holomorphic_on s" "\<And>z. z \<in> s \<Longrightarrow> f z = eval_fps F z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1252 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1253 |
from assms obtain s where s: "open s" "0 \<in> s" "\<And>z. z \<in> s \<Longrightarrow> eval_fps F z = f z" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1254 |
unfolding has_fps_expansion_def eventually_nhds by blast |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1255 |
let ?s' = "eball 0 (fps_conv_radius F) \<inter> s" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1256 |
have "eval_fps F holomorphic_on ?s'" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1257 |
by (intro holomorphic_intros) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1258 |
also have "?this \<longleftrightarrow> f holomorphic_on ?s'" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1259 |
using s by (intro holomorphic_cong) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1260 |
finally show ?thesis using s assms |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1261 |
by (intro that[of ?s']) (auto simp: has_fps_expansion_def zero_ereal_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1262 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1263 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1264 |
lemma residue_fps_expansion_over_power_at_0: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1265 |
assumes "f has_fps_expansion F" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1266 |
shows "residue (\<lambda>z. f z / z ^ Suc n) 0 = fps_nth F n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1267 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1268 |
from has_fps_expansion_imp_holomorphic[OF assms] guess s . note s = this |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1269 |
have "residue (\<lambda>z. f z / (z - 0) ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1270 |
using assms s unfolding has_fps_expansion_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1271 |
by (intro residue_holomorphic_over_power[of s]) (auto simp: zero_ereal_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1272 |
also from assms have "\<dots> = fps_nth F n" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1273 |
by (subst fps_nth_fps_expansion) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1274 |
finally show ?thesis by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1275 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1276 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1277 |
end |