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\<^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 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 \<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)
    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 \<open>m \<le> n\<close> 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 \<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)
    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] = \<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)
  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)) =
        (\<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)
  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 \<open>auto simp: d_def N'_def\<close>)
  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
          (\<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)
  also have "\ = eval_fls f z"
    using \<open>n \<ge> 0\<close> 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 \<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)
  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 \<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)
  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 \<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
  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>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)
    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 (\<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
  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 \<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])
  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 \<open>auto simp: complex_powr_of_int\<close>)
  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 \<open>\<forall>\<^sub>F w in at z. f w = 0\<close> 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 (\<lambda>w. f (z + w)) 0) \<and>
             df w \<noteq> 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 \<open>r>0\<close> 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 (\<lambda>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 (\<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)
  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) \
             (\<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)
  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 \<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"
  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>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)
  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>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)
  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 \<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

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

quality100%

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.