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.18    "fps_conv_radius f = conv_radius (fps_nth f)"
    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.31    by (rule summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
    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.45  lemma fps_conv_radius_deriv:
    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.69    assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0"
    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 -