src/HOL/Analysis/FPS_Convergence.thy
 changeset 68643 3db6c9338ec1 parent 68403 223172b97d0b child 68721 53ad5c01be3f
```     1.1 --- a/src/HOL/Analysis/FPS_Convergence.thy	Mon Jul 16 15:24:06 2018 +0200
1.2 +++ b/src/HOL/Analysis/FPS_Convergence.thy	Mon Jul 16 17:50:07 2018 +0200
1.3 @@ -13,7 +13,7 @@
1.4    "HOL-Computational_Algebra.Formal_Power_Series"
1.5  begin
1.6
1.7 -subsection \<open>Balls with extended real radius\<close>
1.8 +subsection%unimportant \<open>Balls with extended real radius\<close>
1.9
1.10  text \<open>
1.11    The following is a variant of @{const ball} that also allows an infinite radius.
1.12 @@ -54,13 +54,13 @@
1.13
1.14  subsection \<open>Basic properties of convergent power series\<close>
1.15
1.16 -definition fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where
1.17 +definition%important fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where
1.19
1.20 -definition eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where
1.21 +definition%important eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where
1.22    "eval_fps f z = (\<Sum>n. fps_nth f n * z ^ n)"
1.23
1.24 -definition fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
1.25 +definition%important fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
1.26    "fps_expansion f z0 = Abs_fps (\<lambda>n. (deriv ^^ n) f z0 / fact n)"
1.27
1.28  lemma norm_summable_fps:
1.29 @@ -73,7 +73,7 @@
1.30    shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. fps_nth f n * z ^ n)"
1.32
1.33 -lemma sums_eval_fps:
1.34 +theorem sums_eval_fps:
1.35    fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
1.36    assumes "norm z < fps_conv_radius f"
1.37    shows   "(\<lambda>n. fps_nth f n * z ^ n) sums eval_fps f z"
1.38 @@ -194,7 +194,7 @@
1.39  qed
1.40
1.41
1.42 -subsection \<open>Lower bounds on radius of convergence\<close>
1.43 +subsection%unimportant \<open>Lower bounds on radius of convergence\<close>
1.44
1.46    fixes f :: "'a :: {banach, real_normed_field} fps"
1.47 @@ -447,12 +447,12 @@
1.48
1.49  subsection \<open>Evaluating power series\<close>
1.50
1.51 -lemma eval_fps_deriv:
1.52 +theorem eval_fps_deriv:
1.53    assumes "norm z < fps_conv_radius f"
1.54    shows   "eval_fps (fps_deriv f) z = deriv (eval_fps f) z"
1.55    by (intro DERIV_imp_deriv [symmetric] has_field_derivative_eval_fps assms)
1.56
1.57 -lemma fps_nth_conv_deriv:
1.58 +theorem fps_nth_conv_deriv:
1.59    fixes f :: "complex fps"
1.60    assumes "fps_conv_radius f > 0"
1.61    shows   "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n"
1.62 @@ -478,7 +478,7 @@
1.63    finally show ?case by (simp add: divide_simps)
1.64  qed
1.65
1.66 -lemma eval_fps_eqD:
1.67 +theorem eval_fps_eqD:
1.68    fixes f g :: "complex fps"
1.70    assumes "eventually (\<lambda>z. eval_fps f z = eval_fps g z) (nhds 0)"
1.71 @@ -792,7 +792,8 @@
1.72    the coefficients of the series with the singularities of the function, this predicate
1.73    is enough.
1.74  \<close>
1.75 -definition has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool"
1.76 +definition%important
1.77 +  has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool"
1.78    (infixl "has'_fps'_expansion" 60)
1.79    where "(f has_fps_expansion F) \<longleftrightarrow>
1.80              fps_conv_radius F > 0 \<and> eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
1.81 @@ -1261,7 +1262,7 @@
1.82      by (intro that[of ?s']) (auto simp: has_fps_expansion_def zero_ereal_def)
1.83  qed
1.84
1.85 -lemma residue_fps_expansion_over_power_at_0:
1.86 +theorem residue_fps_expansion_over_power_at_0:
1.87    assumes "f has_fps_expansion F"
1.88    shows   "residue (\<lambda>z. f z / z ^ Suc n) 0 = fps_nth F n"
1.89  proof -
```