theory Laurent_Convergence imports"HOL-Computational_Algebra.Formal_Laurent_Series""HOL-Library.Landau_Symbols"
Residue_Theorem
begin
definition%important fls_conv_radius :: "complex fls \ ereal" where "fls_conv_radius f = fps_conv_radius (fls_regpart f)"
definition%important eval_fls :: "complex fls \ complex \ complex" where "eval_fls F z = eval_fps (fls_base_factor_to_fps F) z * z powi fls_subdegree F"
definition\<^marker>\<open>tag important\<close>
has_laurent_expansion :: "(complex \ complex) \ complex fls \ bool"
(infixl\<open>has'_laurent'_expansion\<close> 60) where"(f has_laurent_expansion F) \
fls_conv_radius F > 0 \<and> eventually (\<lambda>z. eval_fls F z = f z) (at 0)"
lemma has_laurent_expansion_schematicI: "f has_laurent_expansion F \ F = G \ f has_laurent_expansion G" by simp
lemma has_laurent_expansion_cong: assumes"eventually (\x. f x = g x) (at 0)" "F = G" shows"(f has_laurent_expansion F) \ (g has_laurent_expansion G)" proof - have"eventually (\z. eval_fls F z = g z) (at 0)" if"eventually (\z. eval_fls F z = f z) (at 0)" "eventually (\x. f x = g x) (at 0)" for f g using that by eventually_elim auto from this[of f g] this[of g f] show ?thesis using assms by (auto simp: eq_commute has_laurent_expansion_def) qed
lemma has_laurent_expansion_cong': assumes"eventually (\x. f x = g x) (at z)" "F = G" "z = z'" shows"((\x. f (z + x)) has_laurent_expansion F) \ ((\x. g (z' + x)) has_laurent_expansion G)" by (intro has_laurent_expansion_cong)
(use assms in\<open>auto simp: at_to_0' eventually_filtermap add_ac\<close>)
lemma fls_conv_radius_altdef: "fls_conv_radius F = fps_conv_radius (fls_base_factor_to_fps F)" proof - have"conv_radius (\n. fls_nth F (int n)) = conv_radius (\n. fls_nth F (int n + fls_subdegree F))" proof (cases "fls_subdegree F \ 0") case True hence"conv_radius (\n. fls_nth F (int n + fls_subdegree F)) =
conv_radius (\<lambda>n. fls_nth F (int (n + nat (fls_subdegree F))))" by auto thus ?thesis by (subst (asm) conv_radius_shift) auto next case False hence"conv_radius (\n. fls_nth F (int n)) =
conv_radius (\<lambda>n. fls_nth F (fls_subdegree F + int (n + nat (-fls_subdegree F))))" by auto thus ?thesis by (subst (asm) conv_radius_shift) (auto simp: add_ac) qed thus ?thesis by (simp add: fls_conv_radius_def fps_conv_radius_def) qed
lemma eval_fps_of_nat [simp]: "eval_fps (of_nat n) z = of_nat n" and eval_fps_of_int [simp]: "eval_fps (of_int m) z = of_int m" by (simp_all flip: fps_of_nat fps_of_int)
lemma fps_conv_radius_of_nat [simp]: "fps_conv_radius (of_nat n) = \" and fps_conv_radius_of_int [simp]: "fps_conv_radius (of_int m) = \" by (simp_all flip: fps_of_nat fps_of_int)
lemma fls_conv_radius_add: "fls_conv_radius (F + G) \ min (fls_conv_radius F) (fls_conv_radius G)" by (simp add: fls_conv_radius_def fps_conv_radius_add)
lemma fls_conv_radius_diff: "fls_conv_radius (F - G) \ min (fls_conv_radius F) (fls_conv_radius G)" by (simp add: fls_conv_radius_def fps_conv_radius_diff)
lemma fls_conv_radius_mult: "fls_conv_radius (F * G) \ min (fls_conv_radius F) (fls_conv_radius G)" proof (cases "F = 0 \ G = 0") case False hence [simp]: "F \ 0" "G \ 0" by auto have"fls_conv_radius (F * G) = fps_conv_radius (fls_regpart (fls_shift (fls_subdegree F + fls_subdegree G) (F * G)))" by (simp add: fls_conv_radius_altdef) alsohave"fls_regpart (fls_shift (fls_subdegree F + fls_subdegree G) (F * G)) =
fls_base_factor_to_fps F * fls_base_factor_to_fps G" by (simp add: fls_times_def) alsohave"fps_conv_radius \ \ min (fls_conv_radius F) (fls_conv_radius G)" unfolding fls_conv_radius_altdef by (rule fps_conv_radius_mult) finallyshow ?thesis . qed auto
lemma fps_conv_radius_add_ge: "fps_conv_radius F \ r \ fps_conv_radius G \ r \ fps_conv_radius (F + G) \ r" using fps_conv_radius_add[of F G] by (simp add: min_def split: if_splits)
lemma fps_conv_radius_diff_ge: "fps_conv_radius F \ r \ fps_conv_radius G \ r \ fps_conv_radius (F - G) \ r" using fps_conv_radius_diff[of F G] by (simp add: min_def split: if_splits)
lemma fps_conv_radius_mult_ge: "fps_conv_radius F \ r \ fps_conv_radius G \ r \ fps_conv_radius (F * G) \ r" using fps_conv_radius_mult[of F G] by (simp add: min_def split: if_splits)
lemma fls_conv_radius_add_ge: "fls_conv_radius F \ r \ fls_conv_radius G \ r \ fls_conv_radius (F + G) \ r" using fls_conv_radius_add[of F G] by (simp add: min_def split: if_splits)
lemma fls_conv_radius_diff_ge: "fls_conv_radius F \ r \ fls_conv_radius G \ r \ fls_conv_radius (F - G) \ r" using fls_conv_radius_diff[of F G] by (simp add: min_def split: if_splits)
lemma fls_conv_radius_mult_ge: "fls_conv_radius F \ r \ fls_conv_radius G \ r \ fls_conv_radius (F * G) \ r" using fls_conv_radius_mult[of F G] by (simp add: min_def split: if_splits)
lemma eval_fls_0 [simp]: "eval_fls 0 z = 0" and eval_fls_1 [simp]: "eval_fls 1 z = 1" and eval_fls_const [simp]: "eval_fls (fls_const c) z = c" and eval_fls_numeral [simp]: "eval_fls (numeral num) z = numeral num" and eval_fls_of_nat [simp]: "eval_fls (of_nat n) z = of_nat n" and eval_fls_of_int [simp]: "eval_fls (of_int m) z = of_int m" and eval_fls_X [simp]: "eval_fls fls_X z = z" and eval_fls_X_intpow [simp]: "eval_fls (fls_X_intpow m) z = z powi m" by (simp_all add: eval_fls_def)
lemma eval_fls_at_0: "eval_fls F 0 = (if fls_subdegree F \ 0 then fls_nth F 0 else 0)" by (cases "fls_subdegree F = 0")
(simp_all add: eval_fls_def fls_regpart_def eval_fps_at_0)
lemma eval_fps_to_fls: assumes"norm z < fps_conv_radius F" shows"eval_fls (fps_to_fls F) z = eval_fps F z" proof (cases "F = 0") case [simp]: False have"eval_fps F z = eval_fps (unit_factor F * normalize F) z" by (metis unit_factor_mult_normalize) alsohave"\ = eval_fps (unit_factor F * fps_X ^ subdegree F) z" by simp alsohave"\ = eval_fps (unit_factor F) z * z ^ subdegree F" using assms by (subst eval_fps_mult) auto alsohave"\ = eval_fls (fps_to_fls F) z" unfolding eval_fls_def fls_base_factor_to_fps_to_fls fls_subdegree_fls_to_fps
power_int_of_nat .. finallyshow ?thesis .. qed auto
lemma eval_fls_shift: assumes [simp]: "z \ 0" shows"eval_fls (fls_shift n F) z = eval_fls F z * z powi -n" proof (cases "F = 0") case [simp]: False show ?thesis unfolding eval_fls_def by (subst fls_base_factor_to_fps_shift, subst fls_shift_subdegree[OF \<open>F \<noteq> 0\<close>], subst power_int_diff)
(auto simp: power_int_minus divide_simps) qed auto
lemma eval_fls_add: assumes"ereal (norm z) < fls_conv_radius F""ereal (norm z) < fls_conv_radius G""z \ 0" shows"eval_fls (F + G) z = eval_fls F z + eval_fls G z" using assms proof (induction"fls_subdegree F""fls_subdegree G" arbitrary: F G rule: linorder_wlog) case (sym F G) show ?case using sym(1)[of G F] sym(2-) by (simp add: add_ac) next case (le F G) show ?case proof (cases "F = 0 \ G = 0") case False hence [simp]: "F \ 0" "G \ 0" by auto note [simp] = \<open>z \<noteq> 0\<close>
define F' G'where"F' = fls_base_factor_to_fps F""G' = fls_base_factor_to_fps G"
define m n where"m = fls_subdegree F""n = fls_subdegree G" have"m \ n" using le by (auto simp: m_n_def) have conv1: "ereal (cmod z) < fps_conv_radius F'""ereal (cmod z) < fps_conv_radius G'" using assms le by (simp_all add: F'_G'_def fls_conv_radius_altdef) have conv2: "ereal (cmod z) < fps_conv_radius (G' * fps_X ^ nat (n - m))" using conv1 by (intro less_le_trans[OF _ fps_conv_radius_mult]) auto have conv3: "ereal (cmod z) < fps_conv_radius (F' + G' * fps_X ^ nat (n - m))" using conv1 conv2 by (intro less_le_trans[OF _ fps_conv_radius_add]) auto
have"eval_fls F z + eval_fls G z = eval_fps F' z * z powi m + eval_fps G' z * z powi n" unfolding eval_fls_def m_n_def[symmetric] F'_G'_def[symmetric] by (simp add: power_int_add algebra_simps) alsohave"\ = (eval_fps F' z + eval_fps G' z * z powi (n - m)) * z powi m" by (simp add: algebra_simps power_int_diff) alsohave"eval_fps G' z * z powi (n - m) = eval_fps (G' * fps_X ^ nat (n - m)) z" using assms \<open>m \<le> n\<close> conv1 by (subst eval_fps_mult) (auto simp: power_int_def) alsohave"eval_fps F' z + \ = eval_fps (F' + G' * fps_X ^ nat (n - m)) z" using conv1 conv2 by (subst eval_fps_add) auto alsohave"\ = eval_fls (fps_to_fls (F' + G' * fps_X ^ nat (n - m))) z" using conv3 by (subst eval_fps_to_fls) auto alsohave"\ * z powi m = eval_fls (fls_shift (-m) (fps_to_fls (F' + G' * fps_X ^ nat (n - m)))) z" by (subst eval_fls_shift) auto alsohave"fls_shift (-m) (fps_to_fls (F' + G' * fps_X ^ nat (n - m))) = F + G" using\<open>m \<le> n\<close> by (simp add: fls_times_fps_to_fls fps_to_fls_power fls_X_power_conv_shift_1
fls_shifted_times_simps F'_G'_def m_n_def) finallyshow ?thesis .. qed auto qed
lemma eval_fls_minus: assumes"ereal (norm z) < fls_conv_radius F" shows"eval_fls (-F) z = -eval_fls F z" using assms by (simp add: eval_fls_def eval_fps_minus fls_conv_radius_altdef)
lemma eval_fls_diff: assumes"ereal (norm z) < fls_conv_radius F""ereal (norm z) < fls_conv_radius G" and [simp]: "z \ 0" shows"eval_fls (F - G) z = eval_fls F z - eval_fls G z" proof - have"eval_fls (F + (-G)) z = eval_fls F z - eval_fls G z" using assms by (subst eval_fls_add) (auto simp: eval_fls_minus) thus ?thesis by simp qed
lemma eval_fls_mult: assumes"ereal (norm z) < fls_conv_radius F""ereal (norm z) < fls_conv_radius G""z \ 0" shows"eval_fls (F * G) z = eval_fls F z * eval_fls G z" proof (cases "F = 0 \ G = 0") case False hence [simp]: "F \ 0" "G \ 0" by auto note [simp] = \<open>z \<noteq> 0\<close>
define F' G'where"F' = fls_base_factor_to_fps F""G' = fls_base_factor_to_fps G"
define m n where"m = fls_subdegree F""n = fls_subdegree G" have"eval_fls F z * eval_fls G z = (eval_fps F' z * eval_fps G' z) * z powi (m + n)" unfolding eval_fls_def m_n_def[symmetric] F'_G'_def[symmetric] by (simp add: power_int_add algebra_simps) alsohave"\ = eval_fps (F' * G') z * z powi (m + n)" using assms by (subst eval_fps_mult) (auto simp: F'_G'_def fls_conv_radius_altdef) alsohave"\ = eval_fls (F * G) z" by (simp add: eval_fls_def F'_G'_def m_n_def) (simp add: fls_times_def) finallyshow ?thesis .. qed auto
lemma eval_fls_power: assumes"ereal (norm z) < fls_conv_radius F""z \ 0" shows"eval_fls (F ^ n) z = eval_fls F z ^ n" proof (induction n) case (Suc n) have"eval_fls (F ^ Suc n) z = eval_fls (F * F ^ n) z" by simp alsohave"\ = eval_fls F z * eval_fls (F ^ n) z" using assms by (subst eval_fls_mult) (auto intro!: less_le_trans[OF _ fls_conv_radius_power]) finallyshow ?case using Suc by simp qed auto
lemma eval_fls_eq: assumes"N \ fls_subdegree F" "fls_subdegree F \ 0 \ z \ 0" assumes"(\n. fls_nth F (int n + N) * z powi (int n + N)) sums S" shows"eval_fls F z = S" proof (cases "z = 0") case [simp]: True have"(\n. fls_nth F (int n + N) * z powi (int n + N)) =
(\<lambda>n. if n \<in> (if N \<le> 0 then {nat (-N)} else {}) then fls_nth F (int n + N) else 0)" by (auto simp: fun_eq_iff split: if_splits) alsohave"\ sums (\n\(if N \ 0 then {nat (-N)} else {}). fls_nth F (int n + N))" by (rule sums_If_finite_set) auto alsohave"\ = fls_nth F 0" using assms by auto alsohave"\ = eval_fls F z" using assms by (auto simp: eval_fls_def eval_fps_at_0 power_int_0_left_if) finallyshow ?thesis using assms by (simp add: sums_iff) next case [simp]: False
define N' where "N' = fls_subdegree F"
define d where"d = nat (N' - N)"
have"(\n. fls_nth F (int n + N) * z powi (int n + N)) sums S" by fact alsohave"?this \ (\n. fls_nth F (int (n+d) + N) * z powi (int (n+d) + N)) sums S" by (rule sums_zero_iff_shift [symmetric]) (use assms in\<open>auto simp: d_def N'_def\<close>) alsohave"(\n. int (n+d) + N) = (\n. int n + N')" using assms by (auto simp: N'_def d_def) finallyhave"(\n. fls_nth F (int n + N') * z powi (int n + N')) sums S" . hence"(\n. z powi (-N') * (fls_nth F (int n + N') * z powi (int n + N'))) sums (z powi (-N') * S)" by (intro sums_mult) hence"(\n. fls_nth F (int n + N') * z ^ n) sums (z powi (-N') * S)" by (simp add: power_int_add power_int_minus field_simps) thus ?thesis by (simp add: eval_fls_def eval_fps_def sums_iff power_int_minus N'_def) qed
lemma norm_summable_fls: "norm z < fls_conv_radius f \ summable (\n. norm (fls_nth f n * z ^ n))" using norm_summable_fps[of z "fls_regpart f"] by (simp add: fls_conv_radius_def)
lemma norm_summable_fls': "norm z < fls_conv_radius f \ summable (\n. norm (fls_nth f (n + fls_subdegree f) * z ^ n))" using norm_summable_fps[of z "fls_base_factor_to_fps f"] by (simp add: fls_conv_radius_altdef)
lemma summable_fls: "norm z < fls_conv_radius f \ summable (\n. fls_nth f n * z ^ n)" by (rule summable_norm_cancel[OF norm_summable_fls])
theorem sums_eval_fls: fixes f defines"n \ fls_subdegree f" assumes"norm z < fls_conv_radius f"and"z \ 0 \ n \ 0" shows"(\k. fls_nth f (int k + n) * z powi (int k + n)) sums eval_fls f z" proof (cases "z = 0") case [simp]: False have"(\k. fps_nth (fls_base_factor_to_fps f) k * z ^ k * z powi n) sums
(eval_fps (fls_base_factor_to_fps f) z * z powi n)" using assms(2) by (intro sums_eval_fps sums_mult2) (auto simp: fls_conv_radius_altdef) thus ?thesis by (simp add: power_int_add n_def eval_fls_def mult_ac) next case [simp]: True with assms have"n \ 0" by auto have"(\k. fls_nth f (int k + n) * z powi (int k + n)) sums
(\<Sum>k\<in>(if n \<le> 0 then {nat (-n)} else {}). fls_nth f (int k + n) * z powi (int k + n))" by (intro sums_finite) (auto split: if_splits) alsohave"\ = eval_fls f z" using\<open>n \<ge> 0\<close> by (auto simp: eval_fls_at_0 n_def not_le) finallyshow ?thesis . qed
lemma holomorphic_on_eval_fls: fixes f defines"n \ fls_subdegree f" assumes"A \ eball 0 (fls_conv_radius f) - (if n \ 0 then {} else {0})" shows"eval_fls f holomorphic_on A" proof (cases "n \ 0") case True have"eval_fls f = (\z. eval_fps (fls_base_factor_to_fps f) z * z ^ nat n)" using True by (simp add: fun_eq_iff eval_fls_def power_int_def n_def) moreoverhave"\ holomorphic_on A" using True assms(2) by (intro holomorphic_intros) (auto simp: fls_conv_radius_altdef) ultimatelyshow ?thesis by simp next case False show ?thesis using assms unfolding eval_fls_def by (intro holomorphic_intros) (auto simp: fls_conv_radius_altdef) qed
lemma holomorphic_on_eval_fls' [holomorphic_intros]: assumes"g holomorphic_on A" assumes"g ` A \ eball 0 (fls_conv_radius f) - (if fls_subdegree f \ 0 then {} else {0})" shows"(\x. eval_fls f (g x)) holomorphic_on A" by (meson assms holomorphic_on_compose holomorphic_on_eval_fls holomorphic_transform o_def)
lemma continuous_on_eval_fls: fixes f defines"n \ fls_subdegree f" assumes"A \ eball 0 (fls_conv_radius f) - (if n \ 0 then {} else {0})" shows"continuous_on A (eval_fls f)" using assms holomorphic_on_eval_fls holomorphic_on_imp_continuous_on by blast
lemma continuous_on_eval_fls' [continuous_intros]: fixes f defines"n \ fls_subdegree f" assumes"g ` A \ eball 0 (fls_conv_radius f) - (if n \ 0 then {} else {0})" assumes"continuous_on A g" shows"continuous_on A (\x. eval_fls f (g x))" by (metis assms continuous_on_compose2 continuous_on_eval_fls order.refl)
(* TODO: generalise for nonneg subdegree *) lemma has_field_derivative_eval_fls: assumes"z \ eball 0 (fls_conv_radius f) - {0}" shows"(eval_fls f has_field_derivative eval_fls (fls_deriv f) z) (at z within A)" proof -
define g where"g = fls_base_factor_to_fps f"
define n where"n = fls_subdegree f" have [simp]: "fps_conv_radius g = fls_conv_radius f" by (simp add: fls_conv_radius_altdef g_def) have conv1: "fps_conv_radius (fps_deriv g * fps_X) \ fls_conv_radius f" by (intro fps_conv_radius_mult_ge order.trans[OF _ fps_conv_radius_deriv]) auto have conv2: "fps_conv_radius (of_int n * g) \ fls_conv_radius f" by (intro fps_conv_radius_mult_ge) auto have conv3: "fps_conv_radius (fps_deriv g * fps_X + of_int n * g) \ fls_conv_radius f" by (intro fps_conv_radius_add_ge conv1 conv2)
have [simp]: "fps_conv_radius g = fls_conv_radius f" by (simp add: g_def fls_conv_radius_altdef) have"((\z. eval_fps g z * z powi fls_subdegree f) has_field_derivative
(eval_fps (fps_deriv g) z * z powi n + of_int n * z powi (n - 1) * eval_fps g z))
(at z within A)" using assms by (auto intro!: derivative_eq_intros simp: n_def) alsohave"(\z. eval_fps g z * z powi fls_subdegree f) = eval_fls f" by (simp add: eval_fls_def g_def fun_eq_iff) alsohave"eval_fps (fps_deriv g) z * z powi n + of_int n * z powi (n - 1) * eval_fps g z =
(z * eval_fps (fps_deriv g) z + of_int n * eval_fps g z) * z powi (n - 1)" using assms by (auto simp: power_int_diff field_simps) alsohave"(z * eval_fps (fps_deriv g) z + of_int n * eval_fps g z) =
eval_fps (fps_deriv g * fps_X + of_int n * g) z" using conv1 conv2 assms fps_conv_radius_deriv[of g] by (subst eval_fps_add) (auto simp: eval_fps_mult) alsohave"\ = eval_fls (fps_to_fls (fps_deriv g * fps_X + of_int n * g)) z" using conv3 assms by (subst eval_fps_to_fls) auto alsohave"\ * z powi (n - 1) = eval_fls (fls_shift (1 - n) (fps_to_fls (fps_deriv g * fps_X + of_int n * g))) z" using assms by (subst eval_fls_shift) auto alsohave"fls_shift (1 - n) (fps_to_fls (fps_deriv g * fps_X + of_int n * g)) = fls_deriv f" by (intro fls_eqI) (auto simp: g_def n_def algebra_simps eq_commute[of _ "fls_subdegree f"]) finallyshow ?thesis . qed
lemma analytic_on_eval_fls: assumes"A \ eball 0 (fls_conv_radius f) - (if fls_subdegree f \ 0 then {} else {0})" shows"eval_fls f analytic_on A" proof (rule analytic_on_subset [OF _ assms]) show"eval_fls f analytic_on eball 0 (fls_conv_radius f) - (if fls_subdegree f \0 then {} else {0})" using holomorphic_on_eval_fls[OF order.refl] by (subst analytic_on_open) auto qed
lemma analytic_on_eval_fls' [analytic_intros]: assumes"g analytic_on A" assumes"g ` A \ eball 0 (fls_conv_radius f) - (if fls_subdegree f \ 0 then {} else {0})" shows"(\x. eval_fls f (g x)) analytic_on A" proof - have"eval_fls f \ g analytic_on A" by (intro analytic_on_compose[OF assms(1) analytic_on_eval_fls]) (use assms in auto) thus ?thesis by (simp add: o_def) qed
lemma continuous_eval_fls [continuous_intros]: assumes"z \ eball 0 (fls_conv_radius F) - (if fls_subdegree F \ 0 then {} else {0})" shows"continuous (at z within A) (eval_fls F)" proof - have"isCont (eval_fls F) z" using continuous_on_eval_fls[OF order.refl] assms by (subst (asm) continuous_on_eq_continuous_at) auto thus ?thesis using continuous_at_imp_continuous_at_within by blast qed
named_theorems laurent_expansion_intros
lemma has_laurent_expansion_imp_asymp_equiv_0: assumes F: "f has_laurent_expansion F" defines"n \ fls_subdegree F" shows"f \[at 0] (\z. fls_nth F n * z powi n)" proof (cases "F = 0") case True thus ?thesis using assms by (auto simp: has_laurent_expansion_def) next case [simp]: False
define G where"G = fls_base_factor_to_fps F" have"fls_conv_radius F > 0" using F by (auto simp: has_laurent_expansion_def) hence"isCont (eval_fps G) 0" by (intro continuous_intros) (auto simp: G_def fps_conv_radius_fls_regpart zero_ereal_def) hence lim: "eval_fps G \0\ eval_fps G 0" by (meson isContD) have [simp]: "fps_nth G 0 \ 0" by (auto simp: G_def)
have"f \[at 0] eval_fls F" using F by (intro asymp_equiv_refl_ev) (auto simp: has_laurent_expansion_def eq_commute) alsohave"\ = (\z. eval_fps G z * z powi n)" by (intro ext) (simp_all add: eval_fls_def G_def n_def) alsohave"\ \[at 0] (\z. fps_nth G 0 * z powi n)" using lim by (intro asymp_equiv_intros tendsto_imp_asymp_equiv_const) (auto simp: eval_fps_at_0) alsohave"fps_nth G 0 = fls_nth F n" by (simp add: G_def n_def) finallyshow ?thesis by simp qed
lemma has_laurent_expansion_imp_asymp_equiv: assumes F: "(\w. f (z + w)) has_laurent_expansion F" defines"n \ fls_subdegree F" shows"f \[at z] (\w. fls_nth F n * (w - z) powi n)" using has_laurent_expansion_imp_asymp_equiv_0[OF assms(1)] unfolding n_def by (simp add: at_to_0[of z] asymp_equiv_filtermap_iff add_ac)
lemmas [tendsto_intros del] = tendsto_power_int
lemma has_laurent_expansion_imp_tendsto_0: assumes F: "f has_laurent_expansion F"and"fls_subdegree F \ 0" shows"f \0\ fls_nth F 0" proof (rule asymp_equiv_tendsto_transfer) show"(\z. fls_nth F (fls_subdegree F) * z powi fls_subdegree F) \[at 0] f" by (rule asymp_equiv_symI, rule has_laurent_expansion_imp_asymp_equiv_0) fact show"(\z. fls_nth F (fls_subdegree F) * z powi fls_subdegree F) \0\ fls_nth F 0" by (rule tendsto_eq_intros refl | use assms(2) in simp)+
(use assms(2) in\<open>auto simp: power_int_0_left_if\<close>) qed
lemma has_laurent_expansion_imp_tendsto: assumes F: "(\w. f (z + w)) has_laurent_expansion F" and "fls_subdegree F \ 0" shows"f \z\ fls_nth F 0" using has_laurent_expansion_imp_tendsto_0[OF assms] by (simp add: at_to_0[of z] filterlim_filtermap add_ac)
lemma has_laurent_expansion_imp_filterlim_infinity_0: assumes F: "f has_laurent_expansion F"and"fls_subdegree F < 0" shows"filterlim f at_infinity (at 0)" proof (rule asymp_equiv_at_infinity_transfer) have [simp]: "F \ 0" using assms(2) by auto show"(\z. fls_nth F (fls_subdegree F) * z powi fls_subdegree F) \[at 0] f" by (rule asymp_equiv_symI, rule has_laurent_expansion_imp_asymp_equiv_0) fact show"filterlim (\z. fls_nth F (fls_subdegree F) * z powi fls_subdegree F) at_infinity (at 0)" by (rule tendsto_mult_filterlim_at_infinity tendsto_const
filterlim_power_int_neg_at_infinity | use assms(2) in simp)+
(auto simp: eventually_at_filter) qed
lemma has_laurent_expansion_imp_neg_fls_subdegree: assumes F: "f has_laurent_expansion F" and infy:"filterlim f at_infinity (at 0)" shows"fls_subdegree F < 0" proof (rule ccontr) assume asm:"\ fls_subdegree F < 0"
define ff where"ff=(\z. fls_nth F (fls_subdegree F)
* z powi fls_subdegree F)"
have"(ff \ (if fls_subdegree F =0 then fls_nth F 0 else 0)) (at 0)" using asm unfolding ff_def by (auto intro!: tendsto_eq_intros) moreoverhave"filterlim ff at_infinity (at 0)" proof (rule asymp_equiv_at_infinity_transfer) show"f \[at 0] ff" unfolding ff_def using has_laurent_expansion_imp_asymp_equiv_0[OF F] unfolding ff_def . show"filterlim f at_infinity (at 0)"by fact qed ultimatelyshow False using not_tendsto_and_filterlim_at_infinity[of "at (0::complex)"] by auto qed
lemma has_laurent_expansion_imp_filterlim_infinity: assumes F: "(\w. f (z + w)) has_laurent_expansion F" and "fls_subdegree F < 0" shows"filterlim f at_infinity (at z)" using has_laurent_expansion_imp_filterlim_infinity_0[OF assms] by (simp add: at_to_0[of z] filterlim_filtermap add_ac)
lemma has_laurent_expansion_imp_is_pole_0: assumes F: "f has_laurent_expansion F"and"fls_subdegree F < 0" shows"is_pole f 0" using has_laurent_expansion_imp_filterlim_infinity_0[OF assms] by (simp add: is_pole_def)
lemma is_pole_0_imp_neg_fls_subdegree: assumes F: "f has_laurent_expansion F"and"is_pole f 0" shows"fls_subdegree F < 0" using F assms(2) has_laurent_expansion_imp_neg_fls_subdegree is_pole_def by blast
lemma has_laurent_expansion_imp_is_pole: assumes F: "(\x. f (z + x)) has_laurent_expansion F" and "fls_subdegree F < 0" shows"is_pole f z" using has_laurent_expansion_imp_is_pole_0[OF assms] by (simp add: is_pole_shift_0')
lemma is_pole_imp_neg_fls_subdegree: assumes F: "(\x. f (z + x)) has_laurent_expansion F" and "is_pole f z" shows"fls_subdegree F < 0" proof - have"is_pole (\x. f (z + x)) 0" using assms(2) is_pole_shift_0 by blast thenshow ?thesis using F is_pole_0_imp_neg_fls_subdegree by blast qed
lemma is_pole_fls_subdegree_iff: assumes"(\x. f (z + x)) has_laurent_expansion F" shows"is_pole f z \ fls_subdegree F < 0" using assms is_pole_imp_neg_fls_subdegree has_laurent_expansion_imp_is_pole by auto
lemma assumes"f has_laurent_expansion F" shows has_laurent_expansion_isolated_0: "isolated_singularity_at f 0" and has_laurent_expansion_not_essential_0: "not_essential f 0" proof - from assms have"eventually (\z. eval_fls F z = f z) (at 0)" by (auto simp: has_laurent_expansion_def) thenobtain r where r: "r > 0""\z. z \ ball 0 r - {0} \ eval_fls F z = f z" by (auto simp: eventually_at_filter ball_def eventually_nhds_metric)
have"fls_conv_radius F > 0" using assms by (auto simp: has_laurent_expansion_def) thenobtain R :: real where R: "R > 0""R \ min r (fls_conv_radius F)" using\<open>r > 0\<close> by (metis dual_order.strict_implies_order ereal_dense2 ereal_less(2) min_def)
have"eval_fls F holomorphic_on ball 0 R - {0}" using r R by (intro holomorphic_intros ball_eball_mono Diff_mono) (auto simp: ereal_le_less) alsohave"?this \ f holomorphic_on ball 0 R - {0}" using r R by (intro holomorphic_cong) auto alsohave"\ \ f analytic_on ball 0 R - {0}" by (subst analytic_on_open) auto finallyshow"isolated_singularity_at f 0" unfolding isolated_singularity_at_def using\<open>R > 0\<close> by blast
show"not_essential f 0" proof (cases "fls_subdegree F \ 0") case True hence"f \0\ fls_nth F 0" by (intro has_laurent_expansion_imp_tendsto_0[OF assms]) thus ?thesis by (auto simp: not_essential_def) next case False hence"is_pole f 0" by (intro has_laurent_expansion_imp_is_pole_0[OF assms]) auto thus ?thesis by (auto simp: not_essential_def) qed qed
lemma assumes"(\w. f (z + w)) has_laurent_expansion F" shows has_laurent_expansion_isolated: "isolated_singularity_at f z" and has_laurent_expansion_not_essential: "not_essential f z" using has_laurent_expansion_isolated_0[OF assms] has_laurent_expansion_not_essential_0[OF assms] by (simp_all add: isolated_singularity_at_shift_0 not_essential_shift_0)
lemma has_laurent_expansion_fps: assumes"f has_fps_expansion F" shows"f has_laurent_expansion fps_to_fls F" proof - from assms have radius: "0 < fps_conv_radius F"and eval: "\\<^sub>F z in nhds 0. eval_fps F z = f z" by (auto simp: has_fps_expansion_def) from eval have eval': "\\<^sub>F z in at 0. eval_fps F z = f z" using eventually_at_filter eventually_mono by fastforce moreoverhave"eventually (\z. z \ eball 0 (fps_conv_radius F) - {0}) (at 0)" using radius by (intro eventually_at_in_open) (auto simp: zero_ereal_def) ultimatelyhave"eventually (\z. eval_fls (fps_to_fls F) z = f z) (at 0)" by eventually_elim (auto simp: eval_fps_to_fls) thus ?thesis using radius by (auto simp: has_laurent_expansion_def) qed
lemma has_laurent_expansion_const [simp, intro, laurent_expansion_intros]: "(\_. c) has_laurent_expansion fls_const c" by (auto simp: has_laurent_expansion_def)
lemma has_laurent_expansion_cmult_left [laurent_expansion_intros]: assumes"f has_laurent_expansion F" shows"(\x. c * f x) has_laurent_expansion fls_const c * F" proof - from assms have"eventually (\z. z \ eball 0 (fls_conv_radius F) - {0}) (at 0)" by (intro eventually_at_in_open) (auto simp: has_laurent_expansion_def zero_ereal_def) moreoverfrom assms have"eventually (\z. eval_fls F z = f z) (at 0)" by (auto simp: has_laurent_expansion_def) ultimatelyhave"eventually (\z. eval_fls (fls_const c * F) z = c * f z) (at 0)" by eventually_elim (simp_all add: eval_fls_mult) with assms show ?thesis by (auto simp: has_laurent_expansion_def intro!: less_le_trans[OF _ fls_conv_radius_mult]) qed
lemma has_laurent_expansion_cmult_right [laurent_expansion_intros]: assumes"f has_laurent_expansion F" shows"(\x. f x * c) has_laurent_expansion F * fls_const c" proof - have"F * fls_const c = fls_const c * F" by (intro fls_eqI) (auto simp: mult.commute) with has_laurent_expansion_cmult_left [OF assms] show ?thesis by (simp add: mult.commute) qed
lemma has_fps_expansion_scaleR [fps_expansion_intros]: fixes F :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps" shows"f has_fps_expansion F \ (\x. c *\<^sub>R f x) has_fps_expansion fps_const (of_real c) * F" unfolding scaleR_conv_of_real by (intro fps_expansion_intros)
lemma has_laurent_expansion_scaleR [laurent_expansion_intros]: "f has_laurent_expansion F \ (\x. c *\<^sub>R f x) has_laurent_expansion fls_const (of_real c) * F" unfolding scaleR_conv_of_real by (intro laurent_expansion_intros)
lemma has_laurent_expansion_minus [laurent_expansion_intros]: assumes"f has_laurent_expansion F" shows"(\x. - f x) has_laurent_expansion -F" proof - from assms have"eventually (\x. x \ eball 0 (fls_conv_radius F) - {0}) (at 0)" by (intro eventually_at_in_open) (auto simp: has_laurent_expansion_def zero_ereal_def) moreoverfrom assms have"eventually (\x. eval_fls F x = f x) (at 0)" by (auto simp: has_laurent_expansion_def) ultimatelyhave"eventually (\x. eval_fls (-F) x = -f x) (at 0)" by eventually_elim (auto simp: eval_fls_minus) thus ?thesis using assms by (auto simp: has_laurent_expansion_def) qed
lemma has_laurent_expansion_add [laurent_expansion_intros]: assumes"f has_laurent_expansion F""g has_laurent_expansion G" shows"(\x. f x + g x) has_laurent_expansion F + G" proof - from assms have"0 < min (fls_conv_radius F) (fls_conv_radius G)" by (auto simp: has_laurent_expansion_def) alsohave"\ \ fls_conv_radius (F + G)" by (rule fls_conv_radius_add) finallyhave radius: "\ > 0" .
from assms have"eventually (\x. x \ eball 0 (fls_conv_radius F) - {0}) (at 0)" "eventually (\x. x \ eball 0 (fls_conv_radius G) - {0}) (at 0)" by (intro eventually_at_in_open; force simp: has_laurent_expansion_def zero_ereal_def)+ moreoverhave"eventually (\x. eval_fls F x = f x) (at 0)" and"eventually (\x. eval_fls G x = g x) (at 0)" using assms by (auto simp: has_laurent_expansion_def) ultimatelyhave"eventually (\x. eval_fls (F + G) x = f x + g x) (at 0)" by eventually_elim (auto simp: eval_fls_add) with radius show ?thesis by (auto simp: has_laurent_expansion_def) qed
lemma has_laurent_expansion_diff [laurent_expansion_intros]: assumes"f has_laurent_expansion F""g has_laurent_expansion G" shows"(\x. f x - g x) has_laurent_expansion F - G" using has_laurent_expansion_add[of f F "\x. - g x" "-G"] assms by (simp add: has_laurent_expansion_minus)
lemma has_laurent_expansion_mult [laurent_expansion_intros]: assumes"f has_laurent_expansion F""g has_laurent_expansion G" shows"(\x. f x * g x) has_laurent_expansion F * G" proof - from assms have"0 < min (fls_conv_radius F) (fls_conv_radius G)" by (auto simp: has_laurent_expansion_def) alsohave"\ \ fls_conv_radius (F * G)" by (rule fls_conv_radius_mult) finallyhave radius: "\ > 0" .
from assms have"eventually (\x. x \ eball 0 (fls_conv_radius F) - {0}) (at 0)" "eventually (\x. x \ eball 0 (fls_conv_radius G) - {0}) (at 0)" by (intro eventually_at_in_open; force simp: has_laurent_expansion_def zero_ereal_def)+ moreoverhave"eventually (\x. eval_fls F x = f x) (at 0)" and"eventually (\x. eval_fls G x = g x) (at 0)" using assms by (auto simp: has_laurent_expansion_def) ultimatelyhave"eventually (\x. eval_fls (F * G) x = f x * g x) (at 0)" by eventually_elim (auto simp: eval_fls_mult) with radius show ?thesis by (auto simp: has_laurent_expansion_def) qed
lemma has_fps_expansion_power [fps_expansion_intros]: fixes F :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps" shows"f has_fps_expansion F \ (\x. f x ^ m) has_fps_expansion F ^ m" by (induction m) (auto intro!: fps_expansion_intros)
lemma has_laurent_expansion_power [laurent_expansion_intros]: assumes"f has_laurent_expansion F" shows"(\x. f x ^ n) has_laurent_expansion F ^ n" by (induction n) (auto intro!: laurent_expansion_intros assms)
lemma has_laurent_expansion_sum [laurent_expansion_intros]: assumes"\x. x \ I \ f x has_laurent_expansion F x" shows"(\y. \x\I. f x y) has_laurent_expansion (\x\I. F x)" using assms by (induction I rule: infinite_finite_induct) (auto intro!: laurent_expansion_intros)
lemma has_laurent_expansion_prod [laurent_expansion_intros]: assumes"\x. x \ I \ f x has_laurent_expansion F x" shows"(\y. \x\I. f x y) has_laurent_expansion (\x\I. F x)" using assms by (induction I rule: infinite_finite_induct) (auto intro!: laurent_expansion_intros)
lemma has_laurent_expansion_deriv [laurent_expansion_intros]: assumes"f has_laurent_expansion F" shows"deriv f has_laurent_expansion fls_deriv F" proof - have"eventually (\z. z \ eball 0 (fls_conv_radius F) - {0}) (at 0)" using assms by (intro eventually_at_in_open)
(auto simp: has_laurent_expansion_def zero_ereal_def) moreoverfrom assms have"eventually (\z. eval_fls F z = f z) (at 0)" by (auto simp: has_laurent_expansion_def) thenobtain s where"open s""0 \ s" and s: "\w. w \ s - {0} \ eval_fls F w = f w" by (auto simp: eventually_nhds eventually_at_filter) hence"eventually (\w. w \ s - {0}) (at 0)" by (intro eventually_at_in_open) auto ultimatelyhave"eventually (\z. eval_fls (fls_deriv F) z = deriv f z) (at 0)" proof eventually_elim case (elim z) hence"eval_fls (fls_deriv F) z = deriv (eval_fls F) z" by (simp add: eval_fls_deriv) alsohave"eventually (\w. w \ s - {0}) (nhds z)" using elim and\<open>open s\<close> by (intro eventually_nhds_in_open) auto hence"eventually (\w. eval_fls F w = f w) (nhds z)" by eventually_elim (use s in auto) hence"deriv (eval_fls F) z = deriv f z" by (intro deriv_cong_ev refl) finallyshow ?case . qed with assms show ?thesis by (auto simp: has_laurent_expansion_def intro!: less_le_trans[OF _ fls_conv_radius_deriv]) qed
lemma has_laurent_expansion_shift [laurent_expansion_intros]: assumes"f has_laurent_expansion F" shows"(\x. f x * x powi n) has_laurent_expansion (fls_shift (-n) F)" proof - have"eventually (\x. x \ eball 0 (fls_conv_radius F) - {0}) (at 0)" using assms by (intro eventually_at_in_open) (auto simp: has_laurent_expansion_def zero_ereal_def) moreoverhave"eventually (\x. eval_fls F x = f x) (at 0)" using assms by (auto simp: has_laurent_expansion_def) ultimatelyhave"eventually (\x. eval_fls (fls_shift (-n) F) x = f x * x powi n) (at 0)" by eventually_elim (auto simp: eval_fls_shift assms) with assms show ?thesis by (auto simp: has_laurent_expansion_def) qed
lemma has_laurent_expansion_shift' [laurent_expansion_intros]: assumes"f has_laurent_expansion F" shows"(\x. f x * x powi (-n)) has_laurent_expansion (fls_shift n F)" using has_laurent_expansion_shift[OF assms, of "-n"] by simp
lemma has_laurent_expansion_deriv': assumes"f has_laurent_expansion F" assumes"open A""0 \ A" "\x. x \ A - {0} \ (f has_field_derivative f' x) (at x)" shows"f' has_laurent_expansion fls_deriv F" proof - have"deriv f has_laurent_expansion fls_deriv F" by (intro laurent_expansion_intros assms) alsohave"?this \ ?thesis" proof (intro has_laurent_expansion_cong refl) have"eventually (\z. z \ A - {0}) (at 0)" by (intro eventually_at_in_open assms) thus"eventually (\z. deriv f z = f' z) (at 0)" by eventually_elim (auto intro!: DERIV_imp_deriv assms) qed finallyshow ?thesis . qed
definition laurent_expansion :: "(complex \ complex) \ complex \ complex fls" where "laurent_expansion f z =
(if eventually (\<lambda>z. f z = 0) (at z) then 0
else fls_shift (-zorder f z) (fps_to_fls (fps_expansion (zor_poly f z) z)))"
lemma laurent_expansion_cong: assumes"eventually (\w. f w = g w) (at z)" "z = z'" shows"laurent_expansion f z = laurent_expansion g z'" unfolding laurent_expansion_def using zor_poly_cong[OF assms(1,2)] zorder_cong[OF assms] assms by (intro if_cong refl) (auto elim: eventually_elim2)
theorem not_essential_has_laurent_expansion_0: assumes"isolated_singularity_at f 0""not_essential f 0" shows"f has_laurent_expansion laurent_expansion f 0" proof (cases "\\<^sub>F w in at 0. f w \ 0") case False have"(\_. 0) has_laurent_expansion 0" by simp alsohave"?this \ f has_laurent_expansion 0" using False by (intro has_laurent_expansion_cong) (auto simp: frequently_def) finallyshow ?thesis using False by (simp add: laurent_expansion_def frequently_def) next case True
define n where"n = zorder f 0" obtain r where r: "zor_poly f 0 0 \ 0" "zor_poly f 0 holomorphic_on cball 0 r" "r > 0" "\w\cball 0 r - {0}. f w = zor_poly f 0 w * w powi n \
zor_poly f 0 w \<noteq> 0" using zorder_exist[OF assms True] unfolding n_def by auto have holo: "zor_poly f 0 holomorphic_on ball 0 r" by (rule holomorphic_on_subset[OF r(2)]) auto
define F where"F = fps_expansion (zor_poly f 0) 0" have F: "zor_poly f 0 has_fps_expansion F" unfolding F_def by (rule has_fps_expansion_fps_expansion[OF _ _ holo]) (use\<open>r > 0\<close> in auto) have"(\z. zor_poly f 0 z * z powi n) has_laurent_expansion fls_shift (-n) (fps_to_fls F)" by (intro laurent_expansion_intros has_laurent_expansion_fps[OF F]) alsohave"?this \ f has_laurent_expansion fls_shift (-n) (fps_to_fls F)" by (intro has_laurent_expansion_cong refl eventually_mono[OF eventually_at_in_open[of "ball 0 r"]])
(use r in\<open>auto simp: complex_powr_of_int\<close>) finallyshow ?thesis using True by (simp add: laurent_expansion_def F_def n_def frequently_def) qed
lemma not_essential_has_laurent_expansion: assumes"isolated_singularity_at f z""not_essential f z" shows"(\x. f (z + x)) has_laurent_expansion laurent_expansion f z" proof - from assms(1) have iso:"isolated_singularity_at (\x. f (z + x)) 0" by (simp add: isolated_singularity_at_shift_0) moreoverfrom assms(2) have ness:"not_essential (\x. f (z + x)) 0" by (simp add: not_essential_shift_0) ultimatelyhave"(\x. f (z + x)) has_laurent_expansion laurent_expansion (\x. f (z + x)) 0" by (rule not_essential_has_laurent_expansion_0)
alsohave"\ = laurent_expansion f z" proof (cases "\\<^sub>F w in at z. f w \ 0") case False thenhave"\\<^sub>F w in at z. f w = 0" using not_frequently by force thenhave"laurent_expansion (\x. f (z + x)) 0 = 0" by (smt (verit, best) add.commute eventually_at_to_0 eventually_mono
laurent_expansion_def) moreoverhave"laurent_expansion f z = 0" using\<open>\<forall>\<^sub>F w in at z. f w = 0\<close> unfolding laurent_expansion_def by auto ultimatelyshow ?thesis by auto next case True
define df where"df=zor_poly (\x. f (z + x)) 0"
define g where"g=(\u. u-z)"
have"fps_expansion df 0
= fps_expansion (df o g) z" proof - have"\\<^sub>F w in at 0. f (z + w) \ 0" using True by (smt (verit, best) add.commute eventually_at_to_0
eventually_mono not_frequently) from zorder_exist[OF iso ness this,folded df_def] obtain r where"r>0"and df_holo:"df holomorphic_on cball 0 r"and"df 0 \ 0" "\w\cball 0 r - {0}.
f (z + w) = df w * w powi (zorder (\<lambda>w. f (z + w)) 0) \<and>
df w \<noteq> 0" by auto thenhave df_nz:"\w\ball 0 r. df w\0" by auto
have"(deriv ^^ n) df 0 = (deriv ^^ n) (df \ g) z" for n unfolding comp_def g_def proof (subst higher_deriv_compose_linear'[where u=1 and c="-z",simplified]) show"df holomorphic_on ball 0 r" using df_holo by auto show"open (ball z r)""open (ball 0 r)""z \ ball z r" using\<open>r>0\<close> by auto show" \w. w \ ball z r \ w - z \ ball 0 r" by (simp add: dist_norm) qed auto thenshow ?thesis unfolding fps_expansion_def by auto qed alsohave"... = fps_expansion (zor_poly f z) z" proof (rule fps_expansion_cong) have"\\<^sub>F w in nhds z. zor_poly f z w
= zor_poly (\<lambda>u. f (z + u)) 0 (w - z)" apply (rule zor_poly_shift) using True assms by auto thenshow"\\<^sub>F w in nhds z. (df \ g) w = zor_poly f z w" unfolding df_def g_def comp_def by (auto elim:eventually_mono) qed finallyshow ?thesis unfolding df_def by (auto simp: laurent_expansion_def at_to_0[of z]
eventually_filtermap add_ac zorder_shift') qed finallyshow ?thesis . qed
lemma has_fps_expansion_to_laurent: "f has_fps_expansion F \ f has_laurent_expansion fps_to_fls F \ f 0 = fps_nth F 0" proof safe assume *: "f has_laurent_expansion fps_to_fls F""f 0 = fps_nth F 0" have"eventually (\z. z \ eball 0 (fps_conv_radius F)) (nhds 0)" using * by (intro eventually_nhds_in_open) (auto simp: has_laurent_expansion_def zero_ereal_def) moreoverhave"eventually (\z. z \ 0 \ eval_fls (fps_to_fls F) z = f z) (nhds 0)" using * by (auto simp: has_laurent_expansion_def eventually_at_filter) ultimatelyhave"eventually (\z. f z = eval_fps F z) (nhds 0)" by eventually_elim
(auto simp: has_laurent_expansion_def eventually_at_filter eval_fps_at_0 eval_fps_to_fls *(2)) thus"f has_fps_expansion F" using * by (auto simp: has_fps_expansion_def has_laurent_expansion_def eq_commute) next assume"f has_fps_expansion F" thus"f 0 = fps_nth F 0" by (metis eval_fps_at_0 has_fps_expansion_imp_holomorphic) qed (auto intro: has_laurent_expansion_fps)
lemma eval_fps_fls_base_factor [simp]: assumes"z \ 0" shows"eval_fps (fls_base_factor_to_fps F) z = eval_fls F z * z powi -fls_subdegree F" using assms unfolding eval_fls_def by (simp add: power_int_minus field_simps)
lemma has_fps_expansion_imp_analytic: assumes"(\x. f (z + x)) has_fps_expansion F" shows"f analytic_on {z}" proof - have"(\x. f (z + x)) analytic_on {0}" by (rule has_fps_expansion_imp_analytic_0) fact hence"(\x. f (z + x)) \ (\x. x - z) analytic_on {z}" by (intro analytic_on_compose_gen analytic_intros) auto thus ?thesis by (simp add: o_def) qed
lemma is_pole_cong_asymp_equiv: assumes"f \[at z] g" "z = z'" shows"is_pole f z = is_pole g z'" using asymp_equiv_at_infinity_transfer[OF assms(1)]
asymp_equiv_at_infinity_transfer[OF asymp_equiv_symI[OF assms(1)]] assms(2) unfolding is_pole_def by auto
lemma not_is_pole_const [simp]: "\is_pole (\_::'a::perfect_space. c :: complex) z" using not_tendsto_and_filterlim_at_infinity[of "at z""\_::'a. c" c] by (auto simp: is_pole_def)
lemma has_laurent_expansion_imp_is_pole_iff: assumes F: "(\x. f (z + x)) has_laurent_expansion F" shows"is_pole f z \ fls_subdegree F < 0" proof assume pole: "is_pole f z" have [simp]: "F \ 0" proof assume"F = 0" hence"is_pole f z \ is_pole (\_. 0 :: complex) z" using assms by (intro is_pole_cong)
(auto simp: has_laurent_expansion_def at_to_0[of z] eventually_filtermap add_ac) with pole show False by simp qed
note pole alsohave"is_pole f z \
is_pole (\<lambda>w. fls_nth F (fls_subdegree F) * (w - z) powi fls_subdegree F) z" using has_laurent_expansion_imp_asymp_equiv[OF F] by (intro is_pole_cong_asymp_equiv refl) alsohave"\ \ is_pole (\w. (w - z) powi fls_subdegree F) z" by simp finallyhave pole': \ .
have False if"fls_subdegree F \ 0" proof - have"(\w. (w - z) powi fls_subdegree F) holomorphic_on UNIV" using that by (intro holomorphic_intros) auto hence"\is_pole (\w. (w - z) powi fls_subdegree F) z" by (meson UNIV_I not_is_pole_holomorphic open_UNIV) with pole' show False by simp qed thus"fls_subdegree F < 0" by force qed (use has_laurent_expansion_imp_is_pole[OF assms] in auto)
lemma analytic_at_imp_has_fps_expansion_0: assumes"f analytic_on {0}" shows"f has_fps_expansion fps_expansion f 0" using assms has_fps_expansion_fps_expansion analytic_at by fast
lemma analytic_at_imp_has_fps_expansion: assumes"f analytic_on {z}" shows"(\x. f (z + x)) has_fps_expansion fps_expansion f z" proof - have"f \ (\x. z + x) analytic_on {0}" by (intro analytic_on_compose_gen[OF _ assms] analytic_intros) auto hence"(f \ (\x. z + x)) has_fps_expansion fps_expansion (f \ (\x. z + x)) 0" unfolding o_def by (intro analytic_at_imp_has_fps_expansion_0) auto alsohave"\ = fps_expansion f z" by (simp add: fps_expansion_def higher_deriv_shift_0') finallyshow ?thesis by (simp add: add_ac) qed
lemma has_laurent_expansion_zorder_0: assumes"f has_laurent_expansion F""F \ 0" shows"zorder f 0 = fls_subdegree F" proof -
define G where"G = fls_base_factor_to_fps F" from assms obtain A where A: "0 \ A" "open A" "\x. x \ A - {0} \ eval_fls F x = f x" unfolding has_laurent_expansion_def eventually_at_filter eventually_nhds by blast
show ?thesis proof (rule zorder_eqI) show"open (A \ eball 0 (fls_conv_radius F))" "0 \ A \ eball 0 (fls_conv_radius F)" using assms A by (auto simp: has_laurent_expansion_def zero_ereal_def) show"eval_fps G holomorphic_on A \ eball 0 (fls_conv_radius F)" by (intro holomorphic_intros) (auto simp: fls_conv_radius_altdef G_def) show"eval_fps G 0 \ 0" using \F \ 0\ by (auto simp: eval_fps_at_0 G_def) next fix w :: complex assume"w \ A \ eball 0 (fls_conv_radius F)" "w \ 0" thus"f w = eval_fps G w * (w - 0) powi (fls_subdegree F)" using A unfolding G_def by (subst eval_fps_fls_base_factor)
(auto simp: complex_powr_of_int power_int_minus field_simps) qed qed
lemma has_laurent_expansion_zorder: assumes"(\w. f (z + w)) has_laurent_expansion F" "F \ 0" shows"zorder f z = fls_subdegree F" using has_laurent_expansion_zorder_0[OF assms] by (simp add: zorder_shift' add_ac)
lemma has_fps_expansion_zorder_0: assumes"f has_fps_expansion F""F \ 0" shows"zorder f 0 = int (subdegree F)" using assms has_laurent_expansion_zorder_0[of f "fps_to_fls F"] by (auto simp: has_fps_expansion_to_laurent fls_subdegree_fls_to_fps)
lemma has_fps_expansion_zorder: assumes"(\w. f (z + w)) has_fps_expansion F" "F \ 0" shows"zorder f z = int (subdegree F)" using has_fps_expansion_zorder_0[OF assms] by (simp add: zorder_shift' add_ac)
lemma has_fps_expansion_fls_base_factor_to_fps: assumes"f has_laurent_expansion F" defines"n \ fls_subdegree F" defines"c \ fps_nth (fls_base_factor_to_fps F) 0" shows"(\z. if z = 0 then c else f z * z powi -n) has_fps_expansion fls_base_factor_to_fps F" proof - have"(\z. f z * z powi -n) has_laurent_expansion fls_shift (-(-n)) F" by (intro laurent_expansion_intros assms) alsohave"fls_shift (-(-n)) F = fps_to_fls (fls_base_factor_to_fps F)" by (simp add: n_def fls_shift_nonneg_subdegree) alsohave"(\z. f z * z powi - n) has_laurent_expansion fps_to_fls (fls_base_factor_to_fps F) \
(\<lambda>z. if z = 0 then c else f z * z powi -n) has_laurent_expansion fps_to_fls (fls_base_factor_to_fps F)" by (intro has_laurent_expansion_cong) (auto simp: eventually_at_filter) alsohave"\ \ (\z. if z = 0 then c else f z * z powi -n) has_fps_expansion fls_base_factor_to_fps F" by (subst has_fps_expansion_to_laurent) (auto simp: c_def) finallyshow ?thesis . qed
lemma zero_has_laurent_expansion_imp_eq_0: assumes"(\_. 0) has_laurent_expansion F" shows"F = 0" proof - have"at (0 :: complex) \ bot" by auto moreoverhave"(\z. if z = 0 then fls_nth F (fls_subdegree F) else 0) has_fps_expansion
fls_base_factor_to_fps F" (is "?f has_fps_expansion _") using has_fps_expansion_fls_base_factor_to_fps[OF assms] by (simp cong: if_cong) hence"isCont ?f 0" using has_fps_expansion_imp_continuous by blast hence"?f \0\ fls_nth F (fls_subdegree F)" by (auto simp: isCont_def) moreoverhave"?f \0\ 0 \ (\_::complex. 0 :: complex) \0\ 0" by (intro filterlim_cong) (auto simp: eventually_at_filter) hence"?f \0\ 0" by simp ultimatelyhave"fls_nth F (fls_subdegree F) = 0" by (rule tendsto_unique) thus ?thesis by (meson nth_fls_subdegree_nonzero) qed
lemma has_laurent_expansion_unique: assumes"f has_laurent_expansion F""f has_laurent_expansion G" shows"F = G" proof - from assms have"(\x. f x - f x) has_laurent_expansion F - G" by (intro laurent_expansion_intros) hence"(\_. 0) has_laurent_expansion F - G" by simp hence"F - G = 0" by (rule zero_has_laurent_expansion_imp_eq_0) thus ?thesis by simp qed
lemma laurent_expansion_eqI: assumes"(\x. f (z + x)) has_laurent_expansion F" shows"laurent_expansion f z = F" using assms has_laurent_expansion_isolated has_laurent_expansion_not_essential
has_laurent_expansion_unique not_essential_has_laurent_expansion by blast
lemma laurent_expansion_0_eqI: assumes"f has_laurent_expansion F" shows"laurent_expansion f 0 = F" using assms laurent_expansion_eqI[of f 0] by simp
lemma has_laurent_expansion_nonzero_imp_eventually_nonzero: assumes"f has_laurent_expansion F""F \ 0" shows"eventually (\x. f x \ 0) (at 0)" proof (rule ccontr) assume"\eventually (\x. f x \ 0) (at 0)" with assms have"eventually (\x. f x = 0) (at 0)" by (intro not_essential_frequently_0_imp_eventually_0 has_laurent_expansion_isolated
has_laurent_expansion_not_essential)
(auto simp: frequently_def) hence"(f has_laurent_expansion 0) \ ((\_. 0) has_laurent_expansion 0)" by (intro has_laurent_expansion_cong) auto hence"f has_laurent_expansion 0" by simp with assms(1) have"F = 0" using has_laurent_expansion_unique by blast with\<open>F \<noteq> 0\<close> show False by contradiction qed
lemma has_laurent_expansion_eventually_nonzero_iff': assumes"f has_laurent_expansion F" shows"eventually (\x. f x \ 0) (at 0) \ F \ 0 " proof assume"\\<^sub>F x in at 0. f x \ 0" moreoverhave"\ (\\<^sub>F x in at 0. f x \ 0)" if "F=0" proof - have"\\<^sub>F x in at 0. f x = 0" using assms that unfolding has_laurent_expansion_def by simp thenshow ?thesis unfolding not_eventually by (auto elim:eventually_frequentlyE) qed ultimatelyshow"F \ 0" by auto qed (simp add:has_laurent_expansion_nonzero_imp_eventually_nonzero[OF assms])
lemma has_laurent_expansion_eventually_nonzero_iff: assumes"(\w. f (z+w)) has_laurent_expansion F" shows"eventually (\x. f x \ 0) (at z) \ F \ 0" apply (subst eventually_at_to_0) apply (rule has_laurent_expansion_eventually_nonzero_iff') using assms by (simp add:add.commute)
lemma has_laurent_expansion_inverse [laurent_expansion_intros]: assumes"f has_laurent_expansion F" shows"(\x. inverse (f x)) has_laurent_expansion inverse F" proof (cases "F = 0") case True thus ?thesis using assms by (auto simp: has_laurent_expansion_def) next case False
define G where"G = laurent_expansion (\x. inverse (f x)) 0" from False have ev: "eventually (\z. f z \ 0) (at 0)" by (intro has_laurent_expansion_nonzero_imp_eventually_nonzero[OF assms])
have *: "(\x. inverse (f x)) has_laurent_expansion G" unfolding G_def by (intro not_essential_has_laurent_expansion_0 isolated_singularity_at_inverse not_essential_inverse
has_laurent_expansion_isolated_0[OF assms] has_laurent_expansion_not_essential_0[OF assms]) have"(\x. f x * inverse (f x)) has_laurent_expansion F * G" by (intro laurent_expansion_intros assms *) alsohave"?this \ (\x. 1) has_laurent_expansion F * G" by (intro has_laurent_expansion_cong refl eventually_mono[OF ev]) auto finallyhave"(\_. 1) has_laurent_expansion F * G" . moreoverhave"(\_. 1) has_laurent_expansion 1" by simp ultimatelyhave"F * G = 1" using has_laurent_expansion_unique by blast hence"G = inverse F" using inverse_unique by blast with * show ?thesis by simp qed
lemma has_laurent_expansion_power_int [laurent_expansion_intros]: "f has_laurent_expansion F \ (\x. f x powi n) has_laurent_expansion (F powi n)" by (auto simp: power_int_def intro!: laurent_expansion_intros)
lemma has_fps_expansion_0_analytic_continuation: assumes"f has_fps_expansion 0""f holomorphic_on A" assumes"open A""connected A""0 \ A" "x \ A" shows"f x = 0" proof - have"eventually (\z. z \ A \ f z = 0) (nhds 0)" using assms by (intro eventually_conj eventually_nhds_in_open) (auto simp: has_fps_expansion_def) thenobtain B where B: "open B""0 \ B" "\z\B. z \ A \ f z = 0" unfolding eventually_nhds by blast show ?thesis proof (rule analytic_continuation_open[where f = f and g = "\_. 0"]) show"B \ {}" using\<open>open B\<close> B by auto show"connected A" using assms by auto qed (use assms B in auto) qed
lemma has_laurent_expansion_0_analytic_continuation: assumes"f has_laurent_expansion 0""f holomorphic_on A - {0}" assumes"open A""connected A""0 \ A" "x \ A - {0}" shows"f x = 0" proof - have"eventually (\z. z \ A - {0} \ f z = 0) (at 0)" using assms by (intro eventually_conj eventually_at_in_open) (auto simp: has_laurent_expansion_def) thenobtain B where B: "open B""0 \ B" "\z\B - {0}. z \ A - {0} \ f z = 0" unfolding eventually_at_filter eventually_nhds by blast show ?thesis proof (rule analytic_continuation_open[where f = f and g = "\_. 0"]) show"B - {0} \ {}" using\<open>open B\<close> \<open>0 \<in> B\<close> by (metis insert_Diff not_open_singleton) show"connected (A - {0})" using assms by (intro connected_open_delete) auto qed (use assms B in auto) qed
lemma has_fps_expansion_cong: assumes"eventually (\x. f x = g x) (nhds 0)" "F = G" shows"f has_fps_expansion F \ g has_fps_expansion G" using assms(2) by (auto simp: has_fps_expansion_def elim!: eventually_elim2[OF assms(1)])
lemma zor_poly_has_fps_expansion: assumes"f has_laurent_expansion F""F \ 0" shows"zor_poly f 0 has_fps_expansion fls_base_factor_to_fps F" proof - note [simp] = \<open>F \<noteq> 0\<close> have"eventually (\z. f z \ 0) (at 0)" by (rule has_laurent_expansion_nonzero_imp_eventually_nonzero[OF assms]) hence freq: "frequently (\z. f z \ 0) (at 0)" by (rule eventually_frequently[rotated]) auto
have *: "isolated_singularity_at f 0""not_essential f 0" using has_laurent_expansion_isolated_0[OF assms(1)] has_laurent_expansion_not_essential_0[OF assms(1)] by auto
define G where"G = fls_base_factor_to_fps F"
define n where"n = zorder f 0" have n_altdef: "n = fls_subdegree F" using has_laurent_expansion_zorder_0 [OF assms(1)] by (simp add: n_def) obtain r where r: "zor_poly f 0 0 \ 0" "zor_poly f 0 holomorphic_on cball 0 r" "r > 0" "\w\cball 0 r - {0}. f w = zor_poly f 0 w * w powi n \
zor_poly f 0 w \<noteq> 0" using zorder_exist[OF * freq] unfolding n_def by auto obtain r' where r': "r' > 0""\x\ball 0 r'-{0}. eval_fls F x = f x" using assms(1) unfolding has_laurent_expansion_def eventually_at_filter eventually_nhds_metric ball_def by (auto simp: dist_commute) have holo: "zor_poly f 0 holomorphic_on ball 0 r" by (rule holomorphic_on_subset[OF r(2)]) auto
have"(\z. if z = 0 then fps_nth G 0 else f z * z powi -n) has_fps_expansion G" unfolding G_def n_altdef by (intro has_fps_expansion_fls_base_factor_to_fps assms) alsohave"?this \ zor_poly f 0 has_fps_expansion G" proof (intro has_fps_expansion_cong) have"eventually (\z. z \ ball 0 (min r r')) (nhds 0)" using\<open>r > 0\<close> \<open>r' > 0\<close> by (intro eventually_nhds_in_open) auto thus"\\<^sub>F x in nhds 0. (if x = 0 then G $ 0 else f x * x powi - n) = zor_poly f 0 x" proof eventually_elim case (elim w) have w: "w \ ball 0 r" "w \ ball 0 r'" using elim by auto show ?case proof (cases "w = 0") case False hence"f w = zor_poly f 0 w * w powi n" using r w by auto thus ?thesis using False by (simp add: powr_minus complex_powr_of_int power_int_minus) next case [simp]: True obtain R where R: "R > 0""R \ r" "R \ r'" "R \ fls_conv_radius F" using\<open>r > 0\<close> \<open>r' > 0\<close> assms(1) unfolding has_laurent_expansion_def by (smt (verit, ccfv_SIG) ereal_dense2 ereal_less(2) less_ereal.simps(1) order.strict_implies_order order_trans) have"eval_fps G 0 = zor_poly f 0 0" proof (rule analytic_continuation_open[where f = "eval_fps G"and g = "zor_poly f 0"])
--> --------------------
--> maximum size reached
--> --------------------
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.28Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
