Quelle  Laurent_Convergence.thy   Sprache: Isabelle

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🍋‹tag important›
  has_laurent_expansion :: "(complex \ complex) \ complex fls \ bool"
  (infixl ‹has'_laurent'_expansion› 60)
  where "(f has_laurent_expansion F) \
            fls_conv_radius F > 0 ∧ eventually (λ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 ‹auto simp: at_to_0' eventually_filtermap add_ac\)

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 (λ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 (λ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 fps_conv_radius_fls_regpart: "fps_conv_radius (fls_regpart F) = fls_conv_radius F"
  by (simp add: fls_conv_radius_def)

lemma fls_conv_radius_0 [simp]: "fls_conv_radius 0 = \"
  and fls_conv_radius_1 [simp]: "fls_conv_radius 1 = \"
  and fls_conv_radius_const [simp]: "fls_conv_radius (fls_const c) = \"
  and fls_conv_radius_numeral [simp]: "fls_conv_radius (numeral num) = \"
  and fls_conv_radius_of_nat [simp]: "fls_conv_radius (of_nat n) = \"
  and fls_conv_radius_of_int [simp]: "fls_conv_radius (of_int m) = \"
  and fls_conv_radius_X [simp]: "fls_conv_radius fls_X = \"
  and fls_conv_radius_X_inv [simp]: "fls_conv_radius fls_X_inv = \"
  and fls_conv_radius_X_intpow [simp]: "fls_conv_radius (fls_X_intpow m) = \"
  by (simp_all add: fls_conv_radius_def fls_X_intpow_regpart)

lemma fls_conv_radius_shift [simp]: "fls_conv_radius (fls_shift n F) = fls_conv_radius F"
  unfolding fls_conv_radius_altdef by (subst fls_base_factor_to_fps_shift) (rule refl)

lemma fls_conv_radius_fps_to_fls [simp]: "fls_conv_radius (fps_to_fls F) = fps_conv_radius F"
  by (simp add: fls_conv_radius_def)

lemma fls_conv_radius_deriv [simp]: "fls_conv_radius (fls_deriv F) \ fls_conv_radius F"
proof -
  have "fls_conv_radius (fls_deriv F) = fps_conv_radius (fls_regpart (fls_deriv F))"
    by (simp add: fls_conv_radius_def)
  also have "fls_regpart (fls_deriv F) = fps_deriv (fls_regpart F)"
    by (intro fps_ext) (auto simp: add_ac)
  also have "fps_conv_radius \ \ fls_conv_radius F"
    by (simp add: fls_conv_radius_def fps_conv_radius_deriv)
  finally show ?thesis .
qed

lemma fls_conv_radius_uminus [simp]: "fls_conv_radius (-F) = fls_conv_radius F"
  by (simp add: fls_conv_radius_def)

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)
  also have "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)
  also have "fps_conv_radius \ \ min (fls_conv_radius F) (fls_conv_radius G)"
    unfolding fls_conv_radius_altdef by (rule fps_conv_radius_mult)
  finally show ?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 fls_conv_radius_power: "fls_conv_radius (F ^ n) \ fls_conv_radius F"
  by (induction n) (auto intro!: fls_conv_radius_mult_ge)

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)
  also have "\ = eval_fps (unit_factor F * fps_X ^ subdegree F) z"
    by simp
  also have "\ = eval_fps (unit_factor F) z * z ^ subdegree F"
    using assms by (subst eval_fps_mult) auto
  also have "\ = 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 ..
  finally show ?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 ‹F ≠ 0›], 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] = ‹z ≠ 0›
    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)
    also have "\ = (eval_fps F' z + eval_fps G' z * z powi (n - m)) * z powi m"
      by (simp add: algebra_simps power_int_diff)
    also have "eval_fps G' z * z powi (n - m) = eval_fps (G' * fps_X ^ nat (n - m)) z"
      using assms ‹m ≤ n› conv1 by (subst eval_fps_mult) (auto simp: power_int_def)
    also have "eval_fps F' z + \ = eval_fps (F' + G' * fps_X ^ nat (n - m)) z"
      using conv1 conv2 by (subst eval_fps_add) auto
    also have "\ = eval_fls (fps_to_fls (F' + G' * fps_X ^ nat (n - m))) z"
      using conv3 by (subst eval_fps_to_fls) auto
    also have "\ * 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
    also have "fls_shift (-m) (fps_to_fls (F' + G' * fps_X ^ nat (n - m))) = F + G"
      using ‹m ≤ n›
      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)
    finally show ?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] = ‹z ≠ 0›
  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)
  also have "\ = 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)
  also have "\ = eval_fls (F * G) z"
    by (simp add: eval_fls_def F'_G'_def m_n_def) (simp add: fls_times_def)
  finally show ?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
  also have "\ = 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])
  finally show ?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)) =
        (λn. if n ∈ (if N ≤ 0 then {nat (-N)} else {}) then fls_nth F (int n + N) else 0)"
    by (auto simp: fun_eq_iff split: if_splits)
  also have "\ sums (\n\(if N \ 0 then {nat (-N)} else {}). fls_nth F (int n + N))"
    by (rule sums_If_finite_set) auto
  also have "\ = fls_nth F 0"
    using assms by auto
  also have "\ = eval_fls F z"
    using assms by (auto simp: eval_fls_def eval_fps_at_0 power_int_0_left_if)
  finally show ?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
  also have "?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 ‹auto simp: d_def N'_def\)
  also have "(\n. int (n+d) + N) = (\n. int n + N')"
    using assms by (auto simp: N'_def d_def)
  finally have "(\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
          (∑k∈(if n ≤ 0 then {nat (-n)} else {}). fls_nth f (int k + n) * z powi (int k + n))"
    by (intro sums_finite) (auto split: if_splits)
  also have "\ = eval_fls f z"
    using ‹n ≥ 0› by (auto simp: eval_fls_at_0 n_def not_le)
  finally show ?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)
  moreover have "\ holomorphic_on A"
    using True assms(2) by (intro holomorphic_intros) (auto simp: fls_conv_radius_altdef)
  ultimately show ?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)

lemmas has_field_derivative_eval_fps' [derivative_intros] =
  DERIV_chain2[OF has_field_derivative_eval_fps]

(* 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)
  also have "(\z. eval_fps g z * z powi fls_subdegree f) = eval_fls f"
    by (simp add: eval_fls_def g_def fun_eq_iff)
  also have "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)
  also have "(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)
  also have "\ = 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
  also have "\ * 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
  also have "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"])
  finally show ?thesis .
qed

lemma eval_fls_deriv:
  assumes "z \ eball 0 (fls_conv_radius F) - {0}"
  shows   "eval_fls (fls_deriv F) z = deriv (eval_fls F) z"
  by (metis DERIV_imp_deriv assms has_field_derivative_eval_fls)

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)
  also have "\ = (\z. eval_fps G z * z powi n)"
    by (intro ext) (simp_all add: eval_fls_def G_def n_def)
  also have "\ \[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)
  also have "fps_nth G 0 = fls_nth F n"
    by (simp add: G_def n_def)
  finally show ?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 ‹auto simp: power_int_0_left_if›)
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)
  moreover have "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
  ultimately show 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
  then show ?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)
  then obtain 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)
  then obtain R :: real where R: "R > 0" "R \ min r (fls_conv_radius F)"
    using ‹r > 0› 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)
  also have "?this \ f holomorphic_on ball 0 R - {0}"
    using r R by (intro holomorphic_cong) auto
  also have "\ \ f analytic_on ball 0 R - {0}"
    by (subst analytic_on_open) auto
  finally show "isolated_singularity_at f 0"
    unfolding isolated_singularity_at_def using ‹R > 0› 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
  moreover have "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)
  ultimately have "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_0 [simp, intro, laurent_expansion_intros]:
  "(\_. 0) has_laurent_expansion 0"
  by (auto simp: has_laurent_expansion_def)

lemma has_fps_expansion_0_iff: "f has_fps_expansion 0 \ eventually (\z. f z = 0) (nhds 0)"
  by (auto simp: has_fps_expansion_def)

lemma has_laurent_expansion_1 [simp, intro, laurent_expansion_intros]:
  "(\_. 1) has_laurent_expansion 1"
  by (auto simp: has_laurent_expansion_def)

lemma has_laurent_expansion_numeral [simp, intro, laurent_expansion_intros]:
  "(\_. numeral n) has_laurent_expansion numeral n"
  by (auto simp: has_laurent_expansion_def)

lemma has_laurent_expansion_fps_X_power [laurent_expansion_intros]:
  "(\x. x ^ n) has_laurent_expansion (fls_X_intpow n)"
  by (auto simp: has_laurent_expansion_def)

lemma has_laurent_expansion_fps_X_power_int [laurent_expansion_intros]:
  "(\x. x powi n) has_laurent_expansion (fls_X_intpow n)"
  by (auto simp: has_laurent_expansion_def)

lemma has_laurent_expansion_fps_X [laurent_expansion_intros]:
  "(\x. x) has_laurent_expansion fls_X"
  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)
  moreover from assms have "eventually (\z. eval_fls F z = f z) (at 0)"
    by (auto simp: has_laurent_expansion_def)
  ultimately have "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)
  moreover from assms have "eventually (\x. eval_fls F x = f x) (at 0)"
    by (auto simp: has_laurent_expansion_def)
  ultimately have "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)
  also have "\ \ fls_conv_radius (F + G)"
    by (rule fls_conv_radius_add)
  finally have 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)+
  moreover have "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)
  ultimately have "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)
  also have "\ \ fls_conv_radius (F * G)"
    by (rule fls_conv_radius_mult)
  finally have 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)+
  moreover have "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)
  ultimately have "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)
  moreover from assms have "eventually (\z. eval_fls F z = f z) (at 0)"
    by (auto simp: has_laurent_expansion_def)
  then obtain 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
  ultimately have "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)
    also have "eventually (\w. w \ s - {0}) (nhds z)"
      using elim and ‹open s› 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)
    finally show ?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)
  moreover have "eventually (\x. eval_fls F x = f x) (at 0)"
    using assms by (auto simp: has_laurent_expansion_def)
  ultimately have "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)
  also have "?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
  finally show ?thesis .
qed

definition laurent_expansion :: "(complex \ complex) \ complex \ complex fls" where
  "laurent_expansion f z =
     (if eventually (λ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
  also have "?this \ f has_laurent_expansion 0"
    using False by (intro has_laurent_expansion_cong) (auto simp: frequently_def)
  finally show ?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 ≠ 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 ‹r > 0› 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])
  also have "?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 ‹auto simp: complex_powr_of_int›)
  finally show ?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)
  moreover from assms(2) have ness:"not_essential (\x. f (z + x)) 0"
    by (simp add: not_essential_shift_0)
  ultimately have "(\x. f (z + x)) has_laurent_expansion laurent_expansion (\x. f (z + x)) 0"
    by (rule not_essential_has_laurent_expansion_0)

  also have "\ = laurent_expansion f z"
  proof (cases "\\<^sub>F w in at z. f w \ 0")
    case False
    then have "\\<^sub>F w in at z. f w = 0" using not_frequently by force
    then have "laurent_expansion (\x. f (z + x)) 0 = 0"
      by (smt (verit, best) add.commute eventually_at_to_0 eventually_mono
          laurent_expansion_def)
    moreover have "laurent_expansion f z = 0"
      using ‹∀🚫F w in at z. f w = 0› unfolding laurent_expansion_def by auto
    ultimately show ?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 (λw. f (z + w)) 0) ∧
             df w ≠ 0"
        by auto
      then have 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 ‹r>0› by auto
        show " \w. w \ ball z r \ w - z \ ball 0 r"
          by (simp add: dist_norm)
      qed auto
      then show ?thesis
        unfolding fps_expansion_def by auto
    qed
    also have "... = 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 (λu. f (z + u)) 0 (w - z)"
        apply (rule zor_poly_shift)
        using True assms by auto
      then show "\\<^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
    finally show ?thesis unfolding df_def
      by (auto simp: laurent_expansion_def at_to_0[of z]
          eventually_filtermap add_ac zorder_shift')
  qed
  finally show ?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)
  moreover have "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)
  ultimately have "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_0:
  assumes "f has_fps_expansion F"
  shows   "f analytic_on {0}"
  by (meson analytic_at_two assms has_fps_expansion_imp_holomorphic)

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
  also have "is_pole f z \
             is_pole (λ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)
  also have "\ \ is_pole (\w. (w - z) powi fls_subdegree F) z"
    by simp
  finally have 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
  also have "\ = fps_expansion f z"
    by (simp add: fps_expansion_def higher_deriv_shift_0')
  finally show ?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)
  also have "fls_shift (-(-n)) F = fps_to_fls (fls_base_factor_to_fps F)"
    by (simp add: n_def fls_shift_nonneg_subdegree)
  also have "(\z. f z * z powi - n) has_laurent_expansion fps_to_fls (fls_base_factor_to_fps F) \
             (λ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)
  also have "\ \ (\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)
  finally show ?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
  moreover have "(\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)
  moreover have "?f \0\ 0 \ (\_::complex. 0 :: complex) \0\ 0"
    by (intro filterlim_cong) (auto simp: eventually_at_filter)
  hence "?f \0\ 0"
    by simp
  ultimately have "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 ‹F ≠ 0› 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"
  moreover have "\ (\\<^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
    then show ?thesis unfolding not_eventually
      by (auto elim:eventually_frequentlyE)
  qed
  ultimately show "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 *)
  also have "?this \ (\x. 1) has_laurent_expansion F * G"
    by (intro has_laurent_expansion_cong refl eventually_mono[OF ev]) auto
  finally have "(\_. 1) has_laurent_expansion F * G" .
  moreover have "(\_. 1) has_laurent_expansion 1"
    by simp
  ultimately have "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)
  then obtain 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 B› 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)
  then obtain 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 B› ‹0 ∈ B› 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] = ‹F ≠ 0›
  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 ≠ 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)
  also have "?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 ‹r > 0› ‹r' > 0\ 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 ‹r > 0› ‹r' > 0\ 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

--> --------------------