Theory Weierstrass_Sigma_Zeta

section ‹The Weierstra\ss\ ‹σ› and ‹ζ› Functions›
theory Weierstrass_Sigma_Zeta
  imports Eisenstein_Series Elliptic_Functions_Library
begin

(*<*)
lemmas [simp del] = div_add div_diff div_mult_self1 div_mult_self2 div_mult_self3 div_mult_self4
(*>*)

subsection ‹The ‹σ› function›

text ‹
  We use a somewhat odd way to define the Weierstra\ss\ ‹σ› function as an infinite product.
  The product in question converges absolutely, but since at the time of writing this we had no
  theory for absolute convergence of products over infinite sets (only sequences), we pick an
  arbitrary sequence and do the product in that order.

  Now that a library of infinite products indexed by an arbitrary set is available one should
  probably switch to that. Maybe the existing Weierstra\ss\ factorisation theory can be generalised
  to the new more general products. Or maybe we can do this without using Weierstra\ss\ factorisation.
  Not sure what the best approach is.
›

lemma (in weierstrass_product) zero_eq [simp]: "f 0 = 1"
proof -
  have "((λx. 1) has_setprod f 0) I"
    using has_setprod[of 0] by simp
  moreover have "((λx. 1) has_setprod 1) I"
    by simp
  ultimately show "f 0 = 1"
    by (rule has_setprod_unique)
qed

context complex_lattice
begin

sublocale weierstrass_sigma: weierstrass_product "λz. z" "λ_. 2" "Λ⇧*"
proof
  have "inf cofinite (principal Λ⇧*) ≤ at_infinity"
  proof (rule filter_leI)
    fix P assume "eventually P (at_infinity :: complex filter)"
    then obtain R where R: "P x" if "norm x ≥ R" for x
      by (auto simp: eventually_at_infinity)
    have "{x ∈ Λ⇧*. ¬ P x} ⊆ Λ ∩ ball 0 R"
      using R by force
    moreover have "finite (Λ ∩ ball 0 R)"
      by (rule bounded_lattice_finite) auto
    ultimately have "finite {x ∈ Λ⇧*. ¬ P x}"
      by (rule finite_subset)
    thus "eventually P (inf cofinite (principal Λ⇧*))"
      unfolding eventually_inf_principal eventually_cofinite by simp
  qed
  thus "filterlim (λz. z) at_infinity (inf cofinite (principal (Λ⇧*)))"
    by (simp add: filterlim_def)
next
  fix r :: real
  assume r: "r > 0"
  have "(λw. 1 / norm w ^ 3) summable_on Λ⇧*"
    by (rule eisenstein_series_norm_summable) auto
  hence "(λz. r ^ 3 * (1 / norm z ^ 3)) summable_on Λ⇧*"
    by (intro summable_on_cmult_right)
  thus "(λz. (r / norm z) ^ Suc 2) summable_on Λ⇧*"
    by (simp add: field_simps)
qed auto

definition weierstrass_sigma :: "complex ⇒ complex" where
  "weierstrass_sigma z = z * weierstrass_sigma.f z"

lemma has_field_derivative_weierstrass_sigma_0:
  "(weierstrass_sigma has_field_derivative 1) (at 0)"
  unfolding weierstrass_sigma_def
  by (auto intro!: derivative_eq_intros analytic_derivI[OF weierstrass_sigma.analytic])

lemma deriv_weierstrass_sigma_0 [simp]: "deriv weierstrass_sigma 0 = 1"
  by (rule DERIV_imp_deriv, rule has_field_derivative_weierstrass_sigma_0)

lemma analytic_on_weierstrass_sigma [analytic_intros]:
  assumes "f analytic_on A"
  shows   "(λz. weierstrass_sigma (f z)) analytic_on A"
proof -
  have "weierstrass_sigma ∘ f analytic_on A"
    unfolding weierstrass_sigma_def [abs_def] 
    by (intro analytic_on_compose assms analytic_intros)
  thus ?thesis
    by (simp add: o_def)
qed

lemma holomorphic_on_weierstrass_sigma [holomorphic_intros]:
  assumes "f holomorphic_on A"
  shows   "(λz. weierstrass_sigma (f z)) holomorphic_on A"
proof -
  have "weierstrass_sigma ∘ f holomorphic_on A"
    unfolding weierstrass_sigma_def [abs_def] 
    by (intro holomorphic_on_compose assms holomorphic_intros)
  thus ?thesis
    by (simp add: o_def)
qed

lemma continuous_on_weierstrass_sigma [continuous_intros]:
  assumes "continuous_on A f"
  shows   "continuous_on A (λz. weierstrass_sigma (f z))"
  by (rule continuous_on_compose2[OF _ assms order.refl])
     (auto intro!: holomorphic_on_imp_continuous_on holomorphic_intros)

lemma weierstrass_sigma_altdef:
  "weierstrass_sigma z = 
     z * (∏⇩∞w∈Λ⇧*. (1 - z / w) * exp (z / w + z⇧2 / (2 * w⇧2)))"
  unfolding weierstrass_sigma_def weierstrass_sigma.f_def weierstrass_factor_def
  by (simp add: numeral_2_eq_2 Let_def mult_ac)

text ‹
  The $\sigma$ function is odd:
›
lemma weierstrass_sigma_uminus: "weierstrass_sigma (-z) = -weierstrass_sigma z"
proof -
  have "((λx. weierstrass_factor 2 (z / x)) has_setprod weierstrass_sigma.f z) Λ⇧*"
    by (rule weierstrass_sigma.has_setprod)
  also have "?this ⟷ ((λx. weierstrass_factor 2 ((-z) / x)) has_setprod weierstrass_sigma.f z) Λ⇧*"
    unfolding weierstrass_factor_def
    by (rule has_setprod_reindex_bij_witness[of _ "λw. -w" "λw. -w"])
       (auto simp: uminus_in_lattice0_iff)
  finally have "((λx. weierstrass_factor 2 ((-z) / x)) has_setprod weierstrass_sigma.f z) Λ⇧*"
    by (simp add: weierstrass_factor_def)
  moreover have "((λx. weierstrass_factor 2 ((-z) / x)) has_setprod weierstrass_sigma.f (-z)) Λ⇧*"
    by (rule weierstrass_sigma.has_setprod)
  ultimately have "weierstrass_sigma.f (-z) = weierstrass_sigma.f z"
    using has_setprod_unique by blast
  thus ?thesis
    by (simp add: weierstrass_sigma_def)
qed

lemma weierstrass_sigma_eq_0_iff: "weierstrass_sigma z = 0 ⟷ z ∈ Λ"
  by (simp add: weierstrass_sigma_def lattice_lattice0 weierstrass_sigma.zero)

lemma weierstrass_sigma_eq_0 [simp]: "z ∈ Λ ⟹ weierstrass_sigma z = 0"
  by (subst weierstrass_sigma_eq_0_iff) auto

lemma has_zorder_weierstrass_sigma [zorder_intros]:
  "has_zorder weierstrass_sigma z (if z ∈ Λ then 1 else 0)"
proof -
  have 1: "has_zorder (λz. z) z (if z = 0 then 1 else 0)"
    by (rule zorder_intros) auto
  have 2: "has_zorder weierstrass_sigma.f z (if z ∈ Λ⇧* then 1 else 0)"
    using weierstrass_sigma.has_zorder[of z] by auto
  have "has_zorder weierstrass_sigma z ((if z = 0 then 1 else 0) + (if z ∈ Λ⇧* then 1 else 0))"
    unfolding weierstrass_sigma_def using has_zorder_mult[OF 1 2 refl] .
  also have "((if z = 0 then 1 else 0) + (if z ∈ Λ⇧* then 1 else 0)) = (if z ∈ Λ then 1 else 0 :: int)"
    by auto
  finally show ?thesis .
qed

lemma zorder_weierstrass_sigma:
  "zorder weierstrass_sigma z = (if z ∈ Λ then 1 else 0)"
  using has_zorder_weierstrass_sigma[of z] by (simp add: has_zorder_def)


subsection ‹The ‹ζ› function›

text ‹
  The Weierstra\ss\ ‹ζ› function, the logarithmic derivative of the Weierstra\ss\ ‹σ›
  function. Not to be confused with the Riemann ‹ζ› function.
›
definition weierstrass_zeta :: "complex ⇒ complex" where
  "weierstrass_zeta z =
     (if z ∈ Λ then 0 else deriv weierstrass_sigma z / weierstrass_sigma z)"

lemma has_field_derivative_weierstrass_sigma [derivative_intros]:
  assumes "(f has_field_derivative f') (at z within A)" "f z ∉ Λ"
  shows   "((λz. weierstrass_sigma (f z)) has_field_derivative
             (f' * weierstrass_sigma (f z) * weierstrass_zeta (f z))) (at z within A)"
proof -
  have deriv: "(weierstrass_sigma has_field_derivative 
                 (weierstrass_sigma z * weierstrass_zeta z)) (at z)"
    if z: "z ∉ Λ" for z
  proof -
    have "(weierstrass_sigma has_field_derivative deriv weierstrass_sigma z) (at z)"
      by (rule analytic_derivI) (auto intro!: analytic_intros)
    also have "deriv weierstrass_sigma z = weierstrass_sigma z * weierstrass_zeta z"
      using z by (simp add: weierstrass_zeta_def weierstrass_sigma_eq_0_iff)
    finally show ?thesis .
  qed

  have "((weierstrass_sigma ∘ f) has_field_derivative 
          (weierstrass_sigma (f z) * weierstrass_zeta (f z) * f')) (at z within A)"
    by (intro DERIV_chain assms deriv)
  thus ?thesis
    by (simp add: o_def mult_ac)
qed

lemma has_log_derivative_weierstrass_sigma [derivative_intros]:
  assumes "(f has_field_derivative f') (at z within A)" "f z ∉ Λ"
  shows   "((λz. weierstrass_sigma (f z)) has_log_derivative
             (f' * weierstrass_zeta (f z))) (at z within A)"
proof (cases "at z within A = bot")
  case False
  thus ?thesis using assms
    by (auto simp: has_log_derivative_def Lim_ident_at weierstrass_sigma_eq_0_iff
             intro!: derivative_eq_intros)
qed auto

lemma has_field_derivative_weierstrass_sigma_aux:
  assumes w: "w ∉ Λ"
  shows "(weierstrass_sigma.f has_field_derivative 
           (weierstrass_zeta w - 1 / w) * weierstrass_sigma.f w) (at w)"
proof -
  write weierstrass_sigma ("σ")
  write weierstrass_zeta ("ζ")
  from w have [simp]: "w ≠ 0"
    by auto
  from w have "((λw. σ w / w) has_field_derivative (w * ζ w - 1) * σ w / w ^ 2) (at w)"
    by (auto intro!: derivative_eq_intros simp: field_simps power2_eq_square)
  also have "?this ⟷ (weierstrass_sigma.f has_field_derivative 
                         ((ζ w - 1 / w) * weierstrass_sigma.f w)) (at w)"
  proof (rule DERIV_cong_ev)
    have "eventually (λw. w ∈ -{0}) (nhds w)"
      by (intro eventually_nhds_in_open) (use w in auto)
    thus "eventually (λw. σ w / w = weierstrass_sigma.f w) (nhds w)"
      by eventually_elim (auto simp: weierstrass_sigma_def)
  qed (auto simp: weierstrass_sigma_def power2_eq_square field_simps)
  finally show ?thesis .
qed

lemma analytic_on_weierstrass_zeta [analytic_intros]:
  assumes "f analytic_on A" "⋀z. z ∈ A ⟹ f z ∉ Λ"
  shows   "(λz. weierstrass_zeta (f z)) analytic_on A"
proof -
  have "(λz. deriv weierstrass_sigma z / weierstrass_sigma z) analytic_on (-Λ)"
    by (intro analytic_intros) (auto simp: weierstrass_sigma_eq_0_iff)
  hence "(λz. deriv weierstrass_sigma z / weierstrass_sigma z) holomorphic_on (-Λ)"
    by (rule analytic_imp_holomorphic)
  also have "?this ⟷ weierstrass_zeta holomorphic_on (-Λ)"
    by (rule holomorphic_cong) (auto simp: weierstrass_zeta_def)
  finally have "weierstrass_zeta analytic_on (-Λ)"
    by (subst analytic_on_open) (auto intro: closed_subset_lattice)
  hence "weierstrass_zeta analytic_on (f ` A)"
    by (rule analytic_on_subset) (use assms(2) in auto)
  hence "weierstrass_zeta ∘ f analytic_on A"
    by (intro analytic_on_compose assms(1)) (use assms(2) in auto)
  thus ?thesis
    by (simp add: o_def)
qed

lemma holomorphic_on_weierstrass_zeta [holomorphic_intros]:
  assumes "f holomorphic_on A" "⋀z. z ∈ A ⟹ f z ∉ Λ"
  shows   "(λz. weierstrass_zeta (f z)) holomorphic_on A"
proof -
  have "weierstrass_zeta holomorphic_on (f ` A)"
    by (intro analytic_imp_holomorphic analytic_intros) (use assms in auto)
  hence "weierstrass_zeta ∘ f holomorphic_on A"
    by (rule holomorphic_on_compose[OF assms(1)])
  thus ?thesis
    by (simp add: o_def)
qed

lemma meromorphic_on_weierstrass_zeta [meromorphic_intros]:
  assumes "f analytic_on A"
  shows   "(λz. weierstrass_zeta (f z)) meromorphic_on A"
proof -
  have "(λz. deriv weierstrass_sigma z / weierstrass_sigma z) meromorphic_on UNIV"
    by (auto intro!: meromorphic_intros analytic_intros
                     analytic_on_imp_meromorphic_on[of weierstrass_sigma])
  also have "eventually (λz. z ∉ Λ) (cosparse UNIV)"
    by (simp add: eventually_not_in_cosparse lattice_sparse)
  hence "eventually (λz. deriv weierstrass_sigma z / weierstrass_sigma z = 
           weierstrass_zeta z) (cosparse UNIV)"
    by eventually_elim (auto simp: weierstrass_zeta_def)
  hence "(λz. deriv weierstrass_sigma z / weierstrass_sigma z) meromorphic_on UNIV ⟷
         weierstrass_zeta meromorphic_on UNIV"
    by (rule meromorphic_on_cong') auto
  finally have "weierstrass_zeta meromorphic_on UNIV" .
  thus ?thesis
    by (rule meromorphic_on_compose[OF _ assms(1)]) auto
qed

lemma continuous_on_weierstrass_zeta [continuous_intros]:
  assumes "continuous_on A f" "⋀z. z ∈ A ⟹ f z ∉ Λ"
  shows   "continuous_on A (λz. weierstrass_zeta (f z))"
  by (rule continuous_on_compose2[OF _ assms(1) order.refl])
     (use assms(2) in ‹auto intro!: holomorphic_on_imp_continuous_on holomorphic_intros›)

lemma has_zorder_weierstrass_zeta:
  assumes z: "z ∈ Λ"
  shows   "has_zorder weierstrass_zeta z (-1)"
proof -
  have "has_zorder (λz. deriv weierstrass_sigma z / weierstrass_sigma z) z (-1)"
    by (rule has_zorder_logderiv has_zorder_weierstrass_sigma)+ (use z in auto)
  also have "?this ⟷ ?thesis"
  proof (rule has_zorder_cong_ev)
    have "eventually (λz. z ∉ Λ) (at z)"
      using not_islimpt_lattice[of z] by (auto simp: islimpt_iff_eventually)
    thus "∀⇩F z in at z. deriv weierstrass_sigma z / weierstrass_sigma z = weierstrass_zeta z"
      by eventually_elim (auto simp: weierstrass_zeta_def)
  qed auto
  finally show ?thesis .
qed

lemma uniform_limit_weierstrass_zeta:
  assumes K: "compact K" "K ∩ Λ = {}"
  shows   "uniform_limit K (λX z. ∑w∈X. 1 / (z - w) + 1 / w + z / w⇧2) 
             (λz. weierstrass_zeta z - 1 / z) (finite_subsets_at_top Λ⇧*)"
proof -
  have "uniform_limit K (λJ z. ∑x∈J. (z / x)⇧2 / (z - x))
          (λz. deriv weierstrass_sigma.f z / weierstrass_sigma.f z) (finite_subsets_at_top Λ⇧*)"
    by (rule weierstrass_sigma.uniform_limit_logderiv) (use assms in auto)
  also have "?this ⟷ ?thesis"
  proof (intro uniform_limit_cong eventually_finite_subsets_at_top_weakI ballI sum.cong refl)
    fix J z w assume "finite J" "J ⊆ Λ⇧*" and z: "z ∈ K" and w: "w ∈ J"
    hence "w ≠ z" "w ≠ 0"
      using assms by auto
    thus "(z / w)⇧2 / (z - w) = 1 / (z - w) + 1 / w + z / w⇧2"
      by (simp add: field_simps power2_eq_square)
  next
    fix z assume "z ∈ K"
    hence z: "z ≠ 0" "z ∉ Λ" "z ∉ Λ⇧*"
      using K by auto
    have "deriv weierstrass_sigma z = z * deriv weierstrass_sigma.f z + weierstrass_sigma.f z"
      unfolding weierstrass_sigma_def
      by (subst complex_derivative_mult_at) (use assms in ‹auto intro!: analytic_intros›)
    also have "… / weierstrass_sigma z = 1 / z + deriv weierstrass_sigma.f z / weierstrass_sigma.f z"
      using z by (auto simp: weierstrass_sigma_def field_simps weierstrass_sigma.zero)
    also have "deriv weierstrass_sigma z / weierstrass_sigma z = weierstrass_zeta z"
      using z by (simp add: weierstrass_zeta_def)
    finally show "deriv weierstrass_sigma.f z / weierstrass_sigma.f z = weierstrass_zeta z - 1 / z"
      by (simp add: field_simps)
  qed
  finally show ?thesis .
qed

lemma has_sum_weierstrass_zeta:
  assumes "z ∉ Λ"
  shows   "((λw. 1 / (z - w) + 1 / w + z / w⇧2) has_sum (weierstrass_zeta z - 1 / z)) Λ⇧*"
proof -
  have "uniform_limit {z} (λX z. ∑w∈X. 1 / (z - w) + 1 / w + z / w⇧2) 
             (λz. weierstrass_zeta z - 1 / z) (finite_subsets_at_top Λ⇧*)"
    by (rule uniform_limit_weierstrass_zeta) (use assms in auto)
  thus ?thesis
    by (simp add: has_sum_def)
qed

text ‹
  The Weierstra\ss\ ‹ζ› function is odd as well:
›
lemma weierstrass_zeta_uminus: "weierstrass_zeta (-z) = -weierstrass_zeta z"
proof (cases "z ∈ Λ")
  case z: False
  have "((λz. weierstrass_sigma z + weierstrass_sigma (-z)) has_field_derivative
          (weierstrass_sigma z * (weierstrass_zeta z + weierstrass_zeta (-z)))) (at z)"
    using z weierstrass_sigma_uminus[of z]
    by (auto intro!: derivative_eq_intros simp: uminus_in_lattice_iff ring_distribs)
  hence "((λz. 0) has_field_derivative 
           (weierstrass_sigma z * (weierstrass_zeta z + weierstrass_zeta (-z)))) (at z)"
    by (simp add: weierstrass_sigma_uminus)
  moreover have "((λz. 0::complex) has_field_derivative 0) (at z)"
    by simp
  ultimately have "weierstrass_sigma z * (weierstrass_zeta z + weierstrass_zeta (-z)) = 0"
    by (rule DERIV_unique)
  thus "weierstrass_zeta (-z) = -weierstrass_zeta z"
    using z by (simp add: weierstrass_sigma_eq_0_iff add_eq_0_iff)
qed (auto simp: weierstrass_zeta_def uminus_in_lattice_iff)

text ‹
  The derivative of ‹ζ› is ‹-℘›:
›
theorem has_field_derivative_weierstrass_zeta:
  assumes z: "z ∉ Λ"
  shows   "(weierstrass_zeta has_field_derivative (-℘ z)) (at z)"
proof -
  define f where "f = (λz. weierstrass_zeta z - 1 / z)"
  have "open (-Λ)" "z ∈ -Λ"
    using closed_lattice z by auto
  then obtain R where R: "R > 0" "cball z R ⊆ -Λ"
    using open_contains_cball_eq by blast

  have *: "∀⇩F X in finite_subsets_at_top Λ⇧*.
             continuous_on (cball z R) (λz. ∑w∈X. 1 / (z - w) + 1 / w + z / w⇧2) ∧
             (∀z∈ball z R. ((λz. ∑w∈X. 1 / (z - w) + 1 / w + z / w⇧2) has_field_derivative
                                 (∑w∈X. 1 / w⇧2 - 1 / (z - w)⇧2)) (at z))"
  proof (intro eventually_finite_subsets_at_top_weakI conjI ballI, goal_cases)
    case (1 X)
    thus ?case using R by (auto intro!: continuous_intros simp: lattice0_def)
  next
    case (2 X u)
    have "u ∉ X" "0 ∉ X"
      using R 2 by force+
    hence "((λz. ∑w∈X. 1 / (z - w) + 1 / w + z / w⇧2) has_field_derivative
                (∑w∈X. w ^ 2 / w ^ 4 - 1 / (u - w)⇧2)) (at u)"
      by (auto intro!: derivative_eq_intros sum.cong simp flip: power2_eq_square)
    also have "(∑w∈X. w ^ 2 / w ^ 4 - 1 / (u - w)⇧2) = (∑w∈X. 1 / w ^ 2 - 1 / (u - w)⇧2)"
      by (intro sum.cong) (auto simp: field_simps power_numeral_reduce)
    finally show ?case .
  qed

  obtain g where g:
     "(f has_field_derivative g w) (at w) ∧
        ((λwa. 1 / wa⇧2 - 1 / (w - wa)⇧2) has_sum g w) Λ⇧*" 
   if "w ∈ ball z R" for w
    unfolding has_sum_def f_def
    by (rule has_complex_derivative_uniform_limit[OF * uniform_limit_weierstrass_zeta])
       (use R in auto)
  have "(f has_field_derivative g z) (at z)"
    using g[of z] ‹R > 0› by auto
  hence "((λw. f w + 1 / w) has_field_derivative (g z - 1 / z ^ 2)) (at z)"
    using z by (auto intro!: derivative_eq_intros simp: power2_eq_square)
  hence deriv: "(weierstrass_zeta has_field_derivative (g z - 1 / z ^ 2)) (at z)"
    by (simp add: f_def)

  have "((λw. 1 / w⇧2 - 1 / (z - w)⇧2) has_sum g z) Λ⇧*"
    using g[of z] ‹R > 0› by (auto simp: has_sum_iff)
  hence "((λw. 1 / (z - w)⇧2 - 1 / w⇧2) has_sum (-g z)) Λ⇧*"
    by (subst has_sum_uminus [symmetric]) auto
  moreover have "((λw. 1 / (z - w)⇧2 - 1 / w⇧2) has_sum weierstrass_fun_aux z) Λ⇧*"
    by (rule weierstrass_fun_aux_has_sum) (use z in auto)
  ultimately have eq: "weierstrass_fun_aux z = -g z"
    using has_sum_unique by blast

  from deriv show "(weierstrass_zeta has_field_derivative (-℘ z)) (at z)"
    using z by (simp add: weierstrass_fun_def eq)
qed

lemma has_field_derivative_weierstrass_zeta' [derivative_intros]:
  assumes "(f has_field_derivative f') (at z within A)" "f z ∉ Λ"
  shows   "((λz. weierstrass_zeta (f z)) has_field_derivative (-f' * ℘ (f z))) (at z within A)"
proof -
  have "((weierstrass_zeta ∘ f) has_field_derivative ((-℘ (f z)) * f')) (at z within A)"
    by (rule DERIV_chain[OF has_field_derivative_weierstrass_zeta[OF assms(2)] assms(1)])
  thus ?thesis
    by (simp add: o_def mult_ac)
qed

lemma deriv_weierstrass_zeta:
  assumes "z ∉ Λ"
  shows   "deriv weierstrass_zeta z = -℘ z"
  by (rule DERIV_imp_deriv) (use assms in ‹auto intro!: derivative_eq_intros›)


subsection ‹Series expansions›

text ‹
  Lastly, we look at the series expansion of $\zeta(z)$ and $\sigma(z)$ at $z = 0$.

  The expansion of $\zeta$ has the following form:
  \[\zeta(z) = \frac{1}{z} - \sum_{k\geq 3} G_{k+1} z^k\]
›

definition fps_weierstrass_zeta :: "complex fps" where
  "fps_weierstrass_zeta = Abs_fps (λk. if k < 3 then 0 else -eisenstein_series (Suc k))"

definition fls_weierstrass_zeta :: "complex fls" where
  "fls_weierstrass_zeta = fls_X_intpow (-1) + fps_to_fls fps_weierstrass_zeta"

lemma fps_deriv_weierstrass_zeta: "fps_deriv fps_weierstrass_zeta = -fps_weierstrass"
proof (rule fps_ext)
  fix n
  show "fps_nth (fps_deriv fps_weierstrass_zeta) n = fps_nth (-fps_weierstrass) n"
    by (cases "n = 1") (auto simp: fps_weierstrass_zeta_def fps_weierstrass_def not_less)
qed

lemma fls_deriv_weierstrass_zeta: "fls_deriv fls_weierstrass_zeta = -fls_weierstrass"
  by (simp add: fls_weierstrass_zeta_def fls_weierstrass_def fls_deriv_fps_to_fls
                fls_deriv_shift fps_deriv_weierstrass_zeta)

lemma has_laurent_expansion_weierstrass_zeta [laurent_expansion_intros]:
  "weierstrass_zeta has_laurent_expansion fls_weierstrass_zeta"
proof -
  have [simp]: "fls_nth fls_weierstrass_zeta 0 = 0"
    by (simp add: fls_weierstrass_zeta_def fps_weierstrass_zeta_def)
  have "weierstrass_zeta meromorphic_on {0}"
    by (auto intro!: meromorphic_intros)
  then obtain F where F: "weierstrass_zeta has_laurent_expansion F"
    by (auto simp: meromorphic_on_def)

  have "((λz. -weierstrass_zeta z) ∘ (λz. -z)) has_laurent_expansion (fls_compose_fps (-F) (-fps_X))"
    by (intro has_laurent_expansion_compose F has_laurent_expansion_fps 
              laurent_expansion_intros fps_expansion_intros) auto
  hence "weierstrass_zeta has_laurent_expansion (fls_compose_fps (-F) (-fps_X))"
    by (auto simp: o_def weierstrass_zeta_uminus)
  with F have "fls_compose_fps (-F) (-fps_X) = F"
    using has_laurent_expansion_unique by blast
  hence "fls_nth (fls_compose_fps (-F) (-fps_X)) 0 = fls_nth F 0"
    by (rule arg_cong)
  hence [simp]: "fls_nth F 0 = 0"
    using fls_nth_fls_compose_fps_linear[of "-1" F 0] by (simp flip: fps_const_neg)

  have "deriv weierstrass_zeta has_laurent_expansion fls_deriv F"
    by (intro laurent_expansion_intros F)
  also have "?this ⟷ (λz. -℘ z) has_laurent_expansion fls_deriv F"
  proof (rule has_laurent_expansion_cong)
    have "eventually (λz. z ∉ Λ) (at 0)"
      by (rule eventually_not_in_lattice_at)
    thus "∀⇩F z in at 0. deriv weierstrass_zeta z = -℘ z"
      by eventually_elim (auto simp: deriv_weierstrass_zeta)
  qed auto
  finally have "(λz. -℘ z) has_laurent_expansion fls_deriv F" .
  moreover have "(λz. -℘ z) has_laurent_expansion (-fls_weierstrass)"
    by (intro laurent_expansion_intros)
  ultimately have "fls_deriv F = fls_deriv fls_weierstrass_zeta"
    using has_laurent_expansion_unique unfolding fls_deriv_weierstrass_zeta by blast
  hence "F = fls_weierstrass_zeta"
    by (simp add: fls_deriv_eq_iff)
  thus ?thesis
    using F by simp
qed

lemma residue_weierstrass_zeta: "residue weierstrass_zeta 0 = 1"
  using has_laurent_expansion_residue_0[OF has_laurent_expansion_weierstrass_zeta]
  by (simp add: fls_weierstrass_zeta_def)



text ‹
  The expansion for $\sigma$ has the following form:
  \[\sigma(z) = z \exp\left( \sum_{k\geq 3} \frac{G_k}{k} z^k \right)\]
›

definition fps_weierstrass_sigma_aux1 :: "complex fps" where
  "fps_weierstrass_sigma_aux1 = 
     Abs_fps (λk. if k ≤ 2 then 0 else eisenstein_series k / of_nat k)"

definition fps_weierstrass_sigma_aux2 :: "complex fps" where
  "fps_weierstrass_sigma_aux2 = fps_compose (fps_exp (-1)) fps_weierstrass_sigma_aux1"

definition fps_weierstrass_sigma :: "complex fps" where
  "fps_weierstrass_sigma = fps_X * fps_weierstrass_sigma_aux2"

lemma fps_nth_0_weierstrass_sigma_aux2 [simp]:
  "fps_nth fps_weierstrass_sigma_aux2 0 = 1"
  by (simp add: fps_weierstrass_sigma_aux2_def)

lemma fps_nth_0_weierstrass_sigma [simp]:
  "fps_nth fps_weierstrass_sigma 0 = 0"
  by (simp add: fps_weierstrass_sigma_def)

lemma fps_weierstrass_sigma_aux2_nonzero [simp]: "fps_weierstrass_sigma_aux2 ≠ 0"
  by (auto simp: fps_weierstrass_sigma_aux2_def fps_compose_eq_0_iff fps_weierstrass_sigma_aux1_def)

lemma fps_weierstrass_sigma_nonzero [simp]: "fps_weierstrass_sigma ≠ 0"
  by (auto simp: fps_weierstrass_sigma_def)

lemma fps_nth_1_weierstrass_sigma [simp]:
  "fps_nth fps_weierstrass_sigma (Suc 0) = 1"
  by (simp add: fps_weierstrass_sigma_def)

lemma subdegree_fps_weierstrass_sigma_aux2 [simp]:
  "subdegree fps_weierstrass_sigma_aux2 = 0"
  by (rule subdegreeI) auto

lemma subdegree_fps_weierstrass_sigma [simp]:
  "subdegree fps_weierstrass_sigma = 1"
  by (rule subdegreeI) auto


lemma has_fps_expansion_weierstrass_sigma_aux [fps_expansion_intros]:
  "weierstrass_sigma.f has_fps_expansion fps_weierstrass_sigma_aux2"
proof -
  write weierstrass_sigma ("σ")
  write weierstrass_zeta ("ζ")

  have "weierstrass_sigma.f analytic_on {0}"
    by (auto intro!: analytic_intros)
  then obtain F where F: "weierstrass_sigma.f has_fps_expansion F"
    using analytic_at_imp_has_fps_expansion_0 by blast
  have F': "weierstrass_sigma.f has_laurent_expansion (fps_to_fls F)"
    unfolding weierstrass_sigma_def by (intro has_laurent_expansion_fps fps_expansion_intros F)

  define H1 where "H1 = fps_weierstrass_sigma_aux1"
  define H2 where "H2 = fps_weierstrass_sigma_aux2"
  obtain c where c: "F = fps_const c * H2"
  proof (rule fps_logderiv_unique)
    have "fps_nth H2 0 ≠ fps_nth 0 0"
      by (auto simp: H2_def fps_weierstrass_sigma_aux2_def)
    thus "H2 ≠ 0"
      by blast
  next      
    have "deriv weierstrass_sigma.f has_laurent_expansion fls_deriv (fps_to_fls F)"
      by (intro laurent_expansion_intros F')
    also have "?this ⟷ (λz. (ζ z - 1 / z) * weierstrass_sigma.f z) has_laurent_expansion 
                            fls_deriv (fps_to_fls F)"
    proof (intro has_laurent_expansion_cong)
      show "eventually (λw. deriv weierstrass_sigma.f w = (ζ w - 1 / w) * weierstrass_sigma.f w) (at 0)"
        using eventually_not_in_lattice_at
      proof eventually_elim
        case (elim w)
        thus ?case by (intro DERIV_imp_deriv has_field_derivative_weierstrass_sigma_aux)
      qed
    qed auto
    finally have "(λz. (ζ z - 1 / z) * weierstrass_sigma.f z) has_laurent_expansion fls_deriv (fps_to_fls F)" .
    moreover have "(λz. (ζ z - 1 / z) * weierstrass_sigma.f z) has_laurent_expansion
                     ((fls_weierstrass_zeta - 1 / fls_X) * fps_to_fls F)"
      by (intro laurent_expansion_intros F')
    ultimately have "fls_deriv (fps_to_fls F) = (fls_weierstrass_zeta - 1 / fls_X) * fps_to_fls F"
      using has_laurent_expansion_unique by blast
    also have "… = fps_to_fls (F * fps_weierstrass_zeta)"
      by (simp add: fls_weierstrass_zeta_def fls_times_fps_to_fls)
    also have "fls_deriv (fps_to_fls F) = fps_to_fls (fps_deriv F)"
      by (simp add: fls_deriv_fps_to_fls)
    finally show "fps_deriv F = fps_weierstrass_zeta * F"
      by (simp add: mult_ac)
  next
    have [simp]: "fps_nth H1 0 = 0"
      by (simp add: H1_def fps_weierstrass_sigma_aux1_def)
    have "fps_deriv H1 = -fps_weierstrass_zeta"
    proof (rule fps_ext)
      show "fps_nth (fps_deriv H1) n = fps_nth (-fps_weierstrass_zeta) n" for n
        by (cases "n = 2")
           (auto simp: H1_def fps_weierstrass_zeta_def fps_weierstrass_sigma_aux1_def 
                 simp del: of_nat_Suc intro!: fps_ext)
    qed
    thus "fps_deriv H2 = fps_weierstrass_zeta * H2"
      by (simp add: H2_def fps_weierstrass_sigma_aux2_def fps_compose_deriv fps_compose_uminus
               flip: fps_const_neg H1_def)
  qed

  have "c = fps_nth (fps_const c * H2) 0"
    by (auto simp: H2_def fps_weierstrass_sigma_aux2_def)
  also have "… = fps_nth F 0"
    by (simp add: c)
  also have "… = 1"
    using has_fps_expansion_imp_0_eq_fps_nth_0[OF F] by simp
  finally have [simp]: "c = 1" .

  from F and c show ?thesis
    by (simp add: H2_def)
qed

theorem has_fps_expansion_weierstrass_sigma [fps_expansion_intros]:
  "weierstrass_sigma has_fps_expansion fps_weierstrass_sigma"
  unfolding weierstrass_sigma_def fps_weierstrass_sigma_def
  by (intro fps_expansion_intros)


subsection ‹Quasiperiodicity and Legendre's relation›

definition weierstrass_eta :: "complex ⇒ complex" where
  "weierstrass_eta ω = 
     weierstrass_zeta (ω1 / 2 + ω) - weierstrass_zeta (ω1 / 2)"

text ‹
  The Weierstra\ss\ $\eta$ function gives the shifts induced in $\zeta$ by a lattice point.
›
theorem weierstrass_zeta_plus_lattice:
  assumes ω: "ω ∈ Λ" and z: "z ∉ Λ"
  shows   "weierstrass_zeta (z + ω) = weierstrass_zeta z + weierstrass_eta ω"
proof -
  define f where "f = (λz. weierstrass_zeta (z + ω) - weierstrass_zeta z)"
  have "f constant_on (-Λ)"
  proof (rule has_field_derivative_0_imp_constant_on)
    show "(f has_field_derivative 0) (at z)" if z: "z ∈ -Λ" for z
      unfolding f_def using ω z
      by (auto intro!: derivative_eq_intros weierstrass_fun.lattice_cong 
               simp: rel_def uminus_in_lattice_iff)
  next
    have "connected (UNIV - Λ)"
      by (rule connected_open_diff_countable) auto
    also have "UNIV - Λ = -Λ"
      by auto
    finally show "connected (-Λ)" .
  qed (use closed_lattice in auto)
  then obtain c where c: "f z = c" if "z ∉ Λ" for z
    by (auto simp: constant_on_def)
  have "f z = f (ω1 / 2)"
    using z by (simp add: c)
  thus ?thesis
    by (simp add: f_def weierstrass_eta_def algebra_simps)
qed


text ‹
  The Weierstra\ss\ $\eta$ function is a group homomorphism from \<^term>‹Λ› to ‹ℂ›.
  Hence the values $\eta_1 = \eta(\omega_1)$ and $\eta_2 = \eta(\omega_2)$ are of particular
  interest since they generate all the remaining ones.
›
lemma weierstrass_eta_0 [simp]: "weierstrass_eta 0 = 0"
  by (simp add: weierstrass_eta_def)

lemma weierstrass_eta_add:
  assumes "ω ∈ Λ" "ω' ∈ Λ"
  shows   "weierstrass_eta (ω + ω') = weierstrass_eta ω + weierstrass_eta ω'"
  using weierstrass_zeta_plus_lattice[of ω "ω1 / 2"]
        weierstrass_zeta_plus_lattice[of ω' "ω1 / 2 + ω"]
        weierstrass_zeta_plus_lattice[of "ω + ω'" "ω1 / 2"] assms
  by (simp add: algebra_simps)

lemma weierstrass_eta_uminus:
  assumes "ω ∈ Λ"
  shows   "weierstrass_eta (-ω) = -weierstrass_eta ω"
  using assms uminus_in_lattice weierstrass_eta_0 weierstrass_eta_add
  by (metis diff_minus_eq_add right_minus_eq)

lemma weierstrass_eta_diff:
  assumes "ω ∈ Λ" "ω' ∈ Λ"
  shows   "weierstrass_eta (ω - ω') = weierstrass_eta ω - weierstrass_eta ω'"
  using weierstrass_eta_add[of ω "-ω'"] assms
  by (simp add: weierstrass_eta_uminus uminus_in_lattice_iff)

lemma weierstrass_eta_of_nat_times_lattice:
  assumes "ω ∈ Λ"
  shows   "weierstrass_eta (of_nat n * ω) = of_nat n * weierstrass_eta ω"
  by (induction n)
     (simp_all add: weierstrass_eta_add assms ring_distribs weierstrass_eta_add lattice_intros)

lemma weierstrass_eta_of_int_times_lattice:
  assumes "ω ∈ Λ"
  shows   "weierstrass_eta (of_int n * ω) = of_int n * weierstrass_eta ω"
proof (cases "n ≥ 0")
  case True
  define m where "m = nat n"
  have n_eq: "n = int m"
    using True by (auto simp: m_def)
  show ?thesis
    by (simp add: n_eq weierstrass_eta_of_nat_times_lattice assms)
next
  case False
  define m where "m = nat (-n)"
  have n_eq: "n = -int m"
    using False by (auto simp: m_def)
  show ?thesis
    by (simp add: n_eq weierstrass_eta_of_nat_times_lattice weierstrass_eta_uminus assms lattice_intros)
qed

lemma weierstrass_eta_of_ω12_coords:
  "weierstrass_eta (of_ω12_coords (of_int m, of_int n)) = 
     of_int m * weierstrass_eta ω1 + of_int n * weierstrass_eta ω2"
  by (simp add: of_ω12_coords_def weierstrass_eta_add 
                weierstrass_eta_of_int_times_lattice lattice_intros)

lemma weierstrass_eta_conv_zeta:
  assumes "ω ∈ Λ" "ω / 2 ∉ Λ"
  shows   "weierstrass_eta ω = 2 * weierstrass_zeta (ω / 2)"
  using weierstrass_zeta_plus_lattice[of ω "-ω/2"] assms
  by (simp add: uminus_in_lattice_iff weierstrass_zeta_uminus)

lemma weierstrass_eta1_conv_zeta: "weierstrass_eta ω1 = 2 * weierstrass_zeta (ω1 / 2)"
  and weierstrass_eta2_conv_zeta: "weierstrass_eta ω2 = 2 * weierstrass_zeta (ω2 / 2)"
  by (rule weierstrass_eta_conv_zeta; simp; fail)+


text ‹
  Legendre's relation links $\eta_1$ and $\eta_2$. This is proven in a straightforward way by
  integrating $\zeta$ along a parallelogram-shaped contour not containing any lattice points.
  For convenience, we choose the one that starts at $\frac{1}{2}(\omega_1 + \omega_2)$.
›
theorem legendre_relation:
  "ω2 * weierstrass_eta ω1 - ω1 * weierstrass_eta ω2 = of_real (2 * pi * sgn (Im (ω2 / ω1))) * 𝗂"
proof -                          
  write weierstrass_zeta ("ζ")
  write weierstrass_eta ("η")
  define z0 where "z0 = (-(ω1 + ω2) / 2)"
  define P where "P = period_parallelogram z0"
  define γ where "γ = parallelogram_path z0 ω1 ω2"

  have closure_P: "Λ ∩ closure P = {0}"
  proof -
    have "closure P = of_ω12_coords ` (λ(a,b). (a-1/2, b-1/2)) ` (cbox (0, 0) (1, 1))"
      unfolding P_def closure_period_parallelogram image_image z0_def
      by (simp add: of_ω12_coords_def case_prod_unfold diff_divide_distrib algebra_simps)
    also have "Λ ∩ … = {0}" (is "?lhs = ?rhs")
    proof (intro equalityI subsetI)
      fix z assume "z ∈ ?lhs"
      then obtain a b 
        where ab: "z = of_ω12_coords (a - 1 / 2, b - 1 / 2)" "a ∈ {0..1}" "b ∈ {0..1}" 
                  "a - 1 / 2 ∈ ℤ" "b - 1 / 2 ∈ ℤ"
        by (auto simp: of_ω12_coords_in_lattice_iff mem_box Basis_pair_def)
      then obtain m n where "a - 1 / 2 = of_int m" "b - 1 / 2 = of_int n"
        by (elim Ints_cases)
      hence mn: "a = of_int m + 1 / 2" "b = of_int n + 1 / 2"
        by auto
      from ab(2,3) have "m = 0 ∧ n = 0"
        by (auto simp: mn)
      with ab(1) show "z ∈ {0}"
        by (auto simp: mn)
    next
      fix z assume "z ∈ {0::complex}"
      hence "z ∈ Λ" "z = of_ω12_coords ((λ(a,b). (a - 1/2, b - 1/2)) (1/2, 1/2))"
           "(1/2, 1/2) ∈ cbox (0, 0) (1 :: real, 1 :: real)"
        by auto
      thus "z ∈ ?lhs"
        by blast
    qed
    finally show ?thesis .
  qed

  have γ: "Λ ∩ path_image γ = {}"
  proof -
    have "path_image γ = of_ω12_coords ` (λ(a,b). (a-1/2, b-1/2)) ` (cbox (0, 0) (1, 1) - box (0, 0) (1, 1))"
      unfolding γ_def path_image_parallelogram_path' image_image z0_def
      by (simp add: of_ω12_coords_def case_prod_unfold diff_divide_distrib algebra_simps)
    also have "Λ ∩ … = {}"
      by (auto simp: of_ω12_coords_in_lattice_iff mem_box Basis_pair_def)
    finally show ?thesis .
  qed

  have "compact (closure P)"
    unfolding P_def by auto
  then obtain R where R: "closure P ⊆ ball 0 R"
    using compact_imp_bounded bounded_subset_ballD by blast
  define A :: "complex set" where "A = ball 0 R"
  have A: "closure P ⊆ A"
    using R by (simp add: A_def)
  have fin: "finite (Λ ∩ A)"
    by (rule bounded_lattice_finite) (auto simp: A_def)

  have "0 = z0 + of_ω12_coords (1/2, 1/2)" "(1/2 :: real, 1/2::real) ∈ box (0, 0) (1, 1)"
    by (auto simp: z0_def of_ω12_coords_def field_simps mem_box Basis_pair_def)
  hence "0 ∈ interior P"
    unfolding P_def interior_period_parallelogram by blast

  define s where "s = complex_of_real (sgn (Im (ω2 / ω1)))"
  have s: "s ∈ {-1, 1}"
    using fundpair by (auto simp: s_def sgn_if fundpair_def complex_is_Real_iff)
  
  have "contour_integral γ ζ = of_real (2 * pi) * 𝗂 * (∑z∈Λ∩A. winding_number γ z * residue ζ z)"
  proof (rule Residue_theorem)
    show "open A" "connected A"
      by (auto simp: A_def)
  next
    show "ζ holomorphic_on A - Λ ∩ A"
      by (auto intro!: holomorphic_intros)
  next
    show "path_image γ ⊆ A - Λ ∩ A"
      using A γ path_image_parallelogram_subset_closure[of z0] 
      by (auto simp: γ_def P_def)
  next
    show "finite (Λ ∩ A)"
      by fact
  next
    show "∀z. z ∉ A ⟶ winding_number γ z = 0"
      using A unfolding γ_def P_def by (auto intro!: winding_number_parallelogram_outside)
  qed (auto simp: γ_def)
  also have "(∑p∈Λ∩A. winding_number γ p * residue ζ p) =
             (∑p∈{0::complex}. s)"
  proof (intro sum.mono_neutral_cong_right ballI, goal_cases)
    case (3 z)
    have "z ∉ closure P"
      using closure_P using 3 by auto
    hence "winding_number γ z = 0"
      unfolding γ_def P_def using winding_number_parallelogram_outside by blast
    thus ?case
      by simp
  next
    case (4 z)
    with ‹0 ∈ interior P› have "winding_number γ z = s"
      unfolding γ_def by (subst winding_number_parallelogram_inside) (auto simp: s_def P_def)
    thus ?case using residue_weierstrass_zeta 4
      by simp
  next
    show "{0} ⊆ Λ ∩ A"
      using ‹0 ∈ interior P› interior_subset[of P] closure_subset[of P] A by auto
  qed (use fin in auto)
  also have "… = s"
    by simp
  also have "contour_integral γ ζ =
               contour_integral (linepath z0 (z0 + ω1)) (λx. ζ x - ζ (x + ω2)) -
               contour_integral (linepath z0 (z0 + ω2)) (λx. ζ x - ζ (x + ω1))" unfolding γ_def
    by (rule contour_integral_parallelogram_path')
       (use γ in ‹auto intro!: continuous_intros simp: γ_def›)
  also have "contour_integral (linepath z0 (z0 + ω1)) (λx. ζ x - ζ (x + ω2)) =
             contour_integral (linepath z0 (z0 + ω1)) (λx. -η ω2)"
  proof (intro contour_integral_cong refl)
    fix z assume "z ∈ path_image (linepath z0 (z0 + ω1))"
    then obtain u where u: "u ∈ {0..1}" "z = linepath z0 (z0 + ω1) u"
      unfolding path_image_def by blast
    have "z = of_ω12_coords (u - 1 / 2, -1 / 2)"
      by (auto simp: of_ω12_coords_def u(2) linepath_def scaleR_conv_of_real field_simps z0_def)
    also have "… ∉ Λ"
      by (auto simp: of_ω12_coords_in_lattice_iff)
    finally show "ζ z - ζ (z + ω2) = -η ω2"
      by (subst weierstrass_zeta_plus_lattice) auto
  qed
  also have "… = -η ω2 * ω1"
    by simp
  also have "contour_integral (linepath z0 (z0 + ω2)) (λx. ζ x - ζ (x + ω1)) =
             contour_integral (linepath z0 (z0 + ω2)) (λx. -η ω1)"
  proof (intro contour_integral_cong refl)
    fix z assume "z ∈ path_image (linepath z0 (z0 + ω2))"
    then obtain u where u: "u ∈ {0..1}" "z = linepath z0 (z0 + ω2) u"
      unfolding path_image_def by blast
    have "z = of_ω12_coords (-1 / 2, u - 1 / 2)"
      by (auto simp: of_ω12_coords_def u(2) linepath_def scaleR_conv_of_real field_simps z0_def)
    also have "… ∉ Λ"
      by (auto simp: of_ω12_coords_in_lattice_iff)
    finally show "ζ z - ζ (z + ω1) = -η ω1"
      by (subst weierstrass_zeta_plus_lattice) auto
  qed
  also have "… = -η ω1 * ω2"
    by simp
  finally show ?thesis
    by (auto simp: mult_ac s_def)
qed


text ‹
  The $\sigma$ function satisfies a similar quasiperiodicity. We first derive the version that
  assumes $\frac{\omega}{2} \notin \Lambda$ and then use this to prove the general version.
›
lemma weierstrass_sigma_plus_lattice_weak:
  assumes ω: "ω ∈ Λ" "ω / 2 ∉ Λ"
  shows "weierstrass_sigma (z + ω) =
           -exp (weierstrass_eta ω * (z + ω / 2)) * weierstrass_sigma z"
proof (cases "z ∈ Λ")
  case True
  thus ?thesis
    using ω by simp
next
  case z: False
  write weierstrass_sigma ("σ")
  write weierstrass_eta ("η")
  write weierstrass_zeta ("ζ")
  define g where
    "g = (λz. σ (z + ω) / (exp (η ω * z) * σ z))"

  have "g constant_on (-Λ)"
  proof (rule has_field_derivative_0_imp_constant_on)
    fix z assume z: "z ∈ -Λ"
    have "(g has_field_derivative 
            (σ z * σ (z + ω) * exp (η ω * z) * (ζ (z + ω) - ζ z - η ω) / (exp (η ω * z) * σ z) ^ 2)) (at z)"
      using z ω by (auto simp: g_def weierstrass_sigma_eq_0_iff simp: algebra_simps power2_eq_square
                         intro!: derivative_eq_intros)
    also have "ζ (z + ω) - ζ z - η ω = 0"
      by (subst weierstrass_zeta_plus_lattice) (use ω z in auto)
    finally show "(g has_field_derivative 0) (at z)"
      by simp
  next
    have "connected (UNIV - Λ)"
      by (rule connected_open_diff_countable) auto
    also have "UNIV - Λ = -Λ" by auto
    finally show "connected (-Λ)" .
  qed (use closed_lattice in auto)

  then obtain c where c: "g z = c" if "z ∉ Λ" for z
    by (auto simp: constant_on_def)
  have "c = g (-ω/2)"
    using ω by (simp add: c uminus_in_lattice_iff)
  also have "… = -exp (η ω * ω / 2)" using ω 
    by (simp add: g_def weierstrass_sigma_uminus weierstrass_sigma_eq_0_iff exp_minus field_simps)
  finally have c_eq: "c = -exp (η ω * ω / 2)" .

  show ?thesis
    using c[of z] z
    by (simp add: g_def c_eq field_simps weierstrass_sigma_eq_0_iff flip: exp_add)
qed

theorem weierstrass_sigma_plus_lattice:
  assumes ω: "ω ∈ Λ"
  defines "ε ≡ (if ω/2 ∈ Λ then 1 else -1)"
  shows "weierstrass_sigma (z + ω) =
           ε * exp (weierstrass_eta ω * (z + ω / 2)) * weierstrass_sigma z"
proof -
  write weierstrass_sigma ("σ")
  write weierstrass_eta ("η")

  have 1: "σ (z + of_nat n * ω) = 
          (if even n then 1 else -1) * exp (of_nat n * η ω * (z + of_nat n * ω / 2)) * σ z"
    if ω: "ω ∈ Λ" "ω / 2 ∉ Λ" for n ω z
  proof (induction n)
    case (Suc n)
    have "σ (z + of_nat (Suc n) * ω) = σ (z + of_nat n * ω + ω)"
      by (simp add: algebra_simps)
    also have "… = -exp (η ω * (z + of_nat n * ω + ω / 2)) * σ (z + of_nat n * ω)"
      by (subst weierstrass_sigma_plus_lattice_weak) (use ω in auto)
    also have "… = (if even (Suc n) then 1 else -1) * 
                       exp (η ω * (z + of_nat n * ω + ω / 2) + of_nat n * η ω * (z + of_nat n * ω / 2)) * σ z"
      unfolding exp_add by (subst Suc.IH) (auto simp: algebra_simps)
    also have "η ω * (z + of_nat n * ω + ω / 2) + of_nat n * η ω * (z + of_nat n * ω / 2) =
               of_nat (Suc n) * η ω * (z + of_nat (Suc n) * ω / 2)"
      by (simp add: field_simps)
    finally show ?case .
  qed auto

  have 2: "σ (z + of_int n * ω) = 
            (if even n then 1 else -1) * exp (of_int n * η ω * (z + of_int n * ω / 2)) * σ z"
    if ω: "ω ∈ Λ" "ω / 2 ∉ Λ" for n ω z
  proof (cases "n ≥ 0")
    case True
    define m where "m = nat n"
    have n_eq: "n = int m"
      using True by (auto simp: m_def)
    show ?thesis
      using 1[of ω z m] ω by (simp add: n_eq)
  next
    case False
    define m where "m = nat (-n)"
    have n_eq: "n = -int m"
      using False by (auto simp: m_def)
    show ?thesis
      using 1[of "-ω" z m] ω by (simp add: n_eq uminus_in_lattice_iff weierstrass_eta_uminus)
  qed

  from assms obtain m n where ω: "ω = of_ω12_coords (of_int m, of_int n)"
    by (auto simp: lattice_def elim!: Ints_cases)
  define c where "c = of_int (m * n) / 2 * (ω2 * η ω1 - ω1 * η ω2)"
  define s where "s = (if Im (ω2 / ω1) > 0 then 1 else -1 :: int)"

  have "σ (z + ω) = σ (z + of_int m * ω1 + of_int n * ω2)"
    by (simp add: ω of_ω12_coords_def algebra_simps)
  also have "… = (if even n then 1 else -1) * 
                    exp (of_int n * η ω2 * (z + of_int m * ω1 + of_int n * ω2 / 2)) *
                    σ (z + of_int m * ω1)"
    by (subst 2) auto
  also have "… = (if even n = even m then 1 else -1) * 
                    exp (of_int n * η ω2 * (z + of_int m * ω1 + of_int n * ω2 / 2) + 
                         of_int m * η ω1 * (z + of_int m * ω1 / 2)) * σ z"
    unfolding exp_add by (subst 2) (auto simp: mult_ac)
  also have "of_int n * η ω2 * (z + of_int m * ω1 + of_int n * ω2 / 2) + 
               of_int m * η ω1 * (z + of_int m * ω1 / 2) =
             η ω * (z + ω / 2) - c" 
    unfolding ω by (subst weierstrass_eta_of_ω12_coords) 
                   (simp_all add: of_ω12_coords_def field_simps c_def)
  also have "exp … = exp (η ω * (z + ω / 2)) / exp c"
    by (simp add: exp_diff)
  also have "c = of_int (m * n) * sgn (Im (ω2 / ω1)) * 𝗂 * pi"
    by (simp add: c_def legendre_relation)
  also have "… = of_int (m * n * s) * 𝗂 * pi"
    using ratio_not_in_Reals by (auto simp: s_def sgn_if ratio_def complex_is_Real_iff)
  also have "exp … = cis (of_int (m * n * s) * pi)"
    by (simp add: exp_eq_polar)
  also have "… = cis pi powi (m * n * s)"
    by (subst cis_power_int) auto
  also have "… = (-1) powi (m * n * s)"
    by simp
  also have "… = (-1) powi (m * n)"
    by (auto simp: s_def power_int_minus field_simps)
  also have "(if even n = even m then 1 else -1) * (exp (η ω * (z + ω / 2)) / …) * σ z =
             (if even m ∧ even n then 1 else -1) * exp (η ω * (z + ω / 2)) * σ z"
    by auto
  also have "even m ∧ even n ⟷ of_ω12_coords (of_int m / 2, of_int n / 2) ∈ Λ"
    unfolding of_ω12_coords_in_lattice_iff
    using of_int_div_of_int_in_Ints_iff[of m 2] of_int_div_of_int_in_Ints_iff[of n 2]
    by auto
  also have "of_ω12_coords (of_int m / 2, of_int n / 2) = ω / 2"
    by (auto simp: ω of_ω12_coords_def field_simps)
  finally show ?thesis
    by (simp add: ε_def)
qed

end


subsection ‹Expressing elliptic functions in terms of $\sigma$›

subsubsection ‹Multisets modulo lattice points›

text ‹
  In this section, we build some infrastructure to count the number of occurrences of a point
  in a multiset modulo the lattice.
›

context complex_lattice
begin

definition count_rel :: "complex multiset ⇒ complex ⇒ nat" where
  "count_rel A z = size {# w ∈# A. rel w z #}"

lemma count_rel_eq_0_iff: "count_rel A z = 0 ⟷ (∀w∈#A. ¬rel w z)"
  by (auto simp: count_rel_def)

lemma count_rel_pos_iff: "count_rel A z > 0 ⟷ (∃w∈#A. rel w z)"
  using count_rel_eq_0_iff[of A z] by auto

lemma count_rel_cong: "rel z z' ⟹ count_rel A z = count_rel A z'"
  unfolding count_rel_def using rel_trans rel_sym by metis

lemma count_rel_to_fund_parallelogram:
  "count_rel (image_mset to_fund_parallelogram A) z = count_rel A z"
  by (simp add: count_rel_def filter_mset_image_mset)

lemma count_rel_empty [simp]: "count_rel {#} z = 0"
  by (simp_all add: count_rel_def)

lemma count_rel_add_mset [simp]:
  "count_rel (add_mset w A) z = (if rel w z then 1 else 0) + count_rel A z"
  by (auto simp: count_rel_def)

lemma count_rel_replicate_mset [simp]:
  "count_rel (replicate_mset n w) z = (if rel w z then n else 0)"
  by (induction n) (auto simp: count_rel_def)

lemma count_rel_add [simp]: "count_rel (A + B) z = count_rel A z + count_rel B z"
  by (simp_all add: count_rel_def)

lemma count_rel_sum [simp]: "count_rel (∑x∈A. f x) z = (∑x∈A. count_rel (f x) z)"
  by (induction A rule: infinite_finite_induct) auto

lemma count_rel_diff_subset:
  assumes "B ⊆# A"
  shows   "count_rel (A - B) z = count_rel A z - count_rel B z"
proof -
  define C where "C = A - B"
  have A_eq: "A = B + C"
    using assms unfolding C_def by (metis subset_mset.add_diff_inverse)
  have "count_rel A z - count_rel B z = count_rel C z"
    by (simp add: A_eq)
  thus ?thesis
    by (simp add: C_def)
qed

lemma sum_count_rel_eq_size:
  assumes "finite X" "⋀x. x ∈# A ⟹ ∃y∈X. rel x y" "X ⊆ period_parallelogram 0"
  shows   "(∑z∈X. count_rel A z) = size A"
proof -
  define A' where "A' = image_mset to_fund_parallelogram A"
  have "(∑z∈X. count_rel A z) = (∑z∈X. count_rel A' z)"
    by (simp add: A'_def count_rel_to_fund_parallelogram)
  also have "… = (∑z∈set_mset A'. count_rel A' z)"
  proof (intro sum.mono_neutral_right ballI)
    show "set_mset A' ⊆ X"
      using assms to_fund_parallelogram_unique by (auto simp: A'_def)
  next
    fix x assume "x ∈ X - set_mset A'"
    thus "count_rel A' x = 0"
      unfolding A'_def count_rel_to_fund_parallelogram
      using assms to_fund_parallelogram_unique[of _ x]
      by (fastforce simp: count_rel_def)
  qed fact+
  also have "… = (∑z∈set_mset A'. count A' z)"
  proof (intro sum.cong refl)
    fix z assume z: "z ∈# A'"
    hence "{# w ∈# A'. rel w z #} = {# w ∈# A'. w = z #}"
      by (intro filter_mset_cong) (auto simp: A'_def)
    thus "count_rel A' z = count A' z"
      by (simp add: count_rel_def count_conv_size_mset)
  qed
  also have "… = size A'"
    by (simp add: size_multiset_overloaded_eq)
  also have "… = size A"
    by (simp add: A'_def)
  finally show ?thesis .
qed


subsubsection ‹Products and quotients of $\sigma$›

text ‹
  Next, we introduce a ``multiple \sigma'' function 
  \[\sigma_{A,B}(z) = \frac{\prod_{a\in A} \sigma(z-a)}{\prod_{b\in B} \sigma(z-b)}\]
  where $A$ and $B$ are multisets of complex numbers. Typically we will have $|A|=|B|$, since
  then $\sigma_{A,B}$ is elliptic.
›

definition weierstrass_multi_sigma :: "complex multiset ⇒ complex multiset ⇒ complex ⇒ complex"
  where "weierstrass_multi_sigma A B = 
           (λz. (∏w∈#A. weierstrass_sigma (z - w)) / (∏w∈#B. weierstrass_sigma (z - w)))"

lemma weierstrass_multi_sigma_eq_0_iff:
  "weierstrass_multi_sigma A B z = 0 ⟷ (∃w∈#(A+B). rel w z)"
  by (force simp: weierstrass_multi_sigma_def weierstrass_sigma_eq_0_iff rel_def 
                  diff_in_lattice_commute)

lemma analytic_on_weierstrass_multi_sigma [analytic_intros]:
  assumes "f analytic_on X" "⋀z w. z ∈ X ⟹ w ∈# B ⟹ ¬rel (f z) w"
  shows   "(λz. weierstrass_multi_sigma A B (f z)) analytic_on X"
  using assms unfolding weierstrass_multi_sigma_def
  by (auto intro!: analytic_intros simp: weierstrass_sigma_eq_0_iff rel_def)

lemma holomorphic_on_weierstrass_multi_sigma [holomorphic_intros]:
  assumes "f holomorphic_on X" "⋀z w. z ∈ X ⟹ w ∈# B ⟹ ¬rel (f z) w"
  shows   "(λz. weierstrass_multi_sigma A B (f z)) holomorphic_on X"
  using assms unfolding weierstrass_multi_sigma_def
  by (auto intro!: holomorphic_intros simp: weierstrass_sigma_eq_0_iff rel_def)

lemma meromorphic_on_weierstrass_multi_sigma [meromorphic_intros]:
  assumes "f analytic_on X"
  shows   "(λz. weierstrass_multi_sigma A B (f z)) meromorphic_on X"
  using assms unfolding weierstrass_multi_sigma_def
  by (intro meromorphic_intros) (auto intro!: analytic_on_imp_meromorphic_on analytic_intros)

text ‹
  Obviously, the zero order of any point is the number of its occurrences in $A$ minus those
  in $B$, counted modulo lattice points.

  Note that this does allow points to be present in both $A$ and $B$. If that happens, they do
  cancel except for a removable singularity. This could be fixed using either a more careful
  definition or the \<^const>‹remove_sings› operator, but it is not worth the effort.
›
lemma has_zorder_weierstrass_multi_sigma:
  "has_zorder (weierstrass_multi_sigma A B) z (int (count_rel A z) - int (count_rel B z))"
proof -
  write weierstrass_sigma ("σ")
  define g where "g = (λX z. ∏w∈#X. σ (z - w))"
  have *: "has_zorder (g X) z (count_rel X z)" for X z
  proof -
    have "has_zorder (g X) z (∑w∈#X. if rel w z then 1 else 0)"
      unfolding g_def
    proof (rule zorder_intros)
      fix w assume w: "w ∈# X"
      have "has_zorder σ (z - w) (if z - w ∈ Λ then 1 else 0)"
        by (rule has_zorder_weierstrass_sigma)
      thus "has_zorder (λz. σ (z - w)) z (if rel w z then 1 else 0)"
        by (auto simp: rel_def diff_in_lattice_commute has_zorder_shift' algebra_simps)
    qed
    also have "… = count_rel X z"
      by (induction X) auto
    finally show ?thesis .
  qed

  have "has_zorder (λz. g A z / g B z) z 
          (int (count_rel A z) - int (count_rel B z))"
    using * * by (rule has_zorder_divide) auto
  thus ?thesis
    by (simp add: weierstrass_multi_sigma_def g_def)
qed

lemma nicely_meromorphic_weierstrass_multi_sigma [meromorphic_intros]:
  assumes "⋀a b. a ∈# A ⟹ b ∈# B ⟹ ¬rel a b"
  defines "f ≡ weierstrass_multi_sigma A B"
  shows "f nicely_meromorphic_on X"
  unfolding nicely_meromorphic_on_def
proof (intro conjI ballI)
  fix z assume "z ∈ X"
  show "is_pole f z ∧ f z = 0 ∨ f ─z→ f z"
  proof (cases "∃b∈#B. rel z b")
    case False
    hence "f ─z→ f z"
      by (auto intro!: analytic_at_imp_isCont isContD analytic_intros simp: f_def)
    thus ?thesis by blast
  next
    case True
    with assms(1) have not_in_A: "∀a∈#A. ¬rel z a"
      using rel_trans rel_sym by blast
    define n where "n = int (count_rel B z)"
    have "has_zorder f z (int (count_rel A z) - int (count_rel B z))"
      unfolding f_def by (rule has_zorder_weierstrass_multi_sigma)
    also have "int (count_rel A z) = 0"
      using not_in_A by (simp add: count_rel_eq_0_iff rel_sym)
    finally have "has_zorder f z (-n)"
      by (simp add: n_def)
    moreover have "n > 0"
      using True by (auto simp: n_def count_rel_pos_iff rel_sym)
    ultimately have "is_pole f z"
      by (simp add: has_zorder_imp_is_pole_iff)
    moreover have "f z = 0"
      using True by (auto simp: f_def weierstrass_multi_sigma_eq_0_iff rel_sym)
    ultimately show ?thesis
      by blast
  qed
qed (auto intro!: meromorphic_intros simp: f_def)

end


locale elliptic_multiple_sigma = complex_lattice +
  fixes A B :: "complex multiset"
  assumes same_size: "size A = size B"
  assumes sum_eq: "sum_mset A = sum_mset B"
begin

sublocale elliptic_function ω1 ω2 "weierstrass_multi_sigma A B"
proof
  show "weierstrass_multi_sigma A B meromorphic_on UNIV" unfolding weierstrass_multi_sigma_def
    by (intro meromorphic_intros) (auto intro!: analytic_on_imp_meromorphic_on analytic_intros)
next
  write weierstrass_sigma ("σ")
  write weierstrass_eta ("η")
  have *: "weierstrass_multi_sigma A B (z + ω) = weierstrass_multi_sigma A B z" 
    if ω: "ω ∈ Λ" "ω / 2 ∉ Λ" for z ω
  proof -
    define n where "n = size A"
    define c where "c = (-1) ^ n * exp (of_nat n * (η ω * (z + ω / 2)))"
    have [simp]: "c ≠ 0"
      by (auto simp: c_def)

    have *: "(∏w∈#X. σ (z + ω - w)) = c / exp (η ω * sum_mset X) * (∏w∈#X. σ (z - w))"
      if "size X = n" for X
    proof -
      have "(∏w∈#X. σ (z + ω - w)) = (∏w∈#X. -exp (η ω * (z - w + ω / 2)) * σ (z - w))"
      proof (intro arg_cong[of _ _ prod_mset] image_mset_cong)
        fix w assume w: "w ∈# X"
        have "σ (z + ω - w) = σ (z - w + ω)"
          by (simp add: algebra_simps)
        also have "… = -exp (η ω * (z - w + ω / 2)) * σ (z - w)"
          by (rule weierstrass_sigma_plus_lattice_weak) (use ω in auto)
        finally show "σ (z + ω - w) = …" .
      qed
      also have "… = (∏w∈#X. (-1) * exp (η ω * (z - w + ω / 2))) * (∏w∈#X. σ (z - w))"
        by (subst prod_mset.distrib) auto
      also have "… = (-1) ^ n * (∏w∈#X. exp (η ω * (z - w + ω / 2))) * (∏w∈#X. σ (z - w))"
        by (subst prod_mset.distrib) (auto simp: ‹size X = n›)
      also have "(∏w∈#X. exp (η ω * (z - w + ω / 2))) = exp (∑w∈#X. η ω * (z - w + ω / 2))"
        by (simp add: exp_sum_mset')
      also have "(∑w∈#X. η ω * (z - w + ω / 2)) = 
                   of_nat n * (η ω * (z + ω / 2)) - η ω * sum_mset X"
        by (simp add: ‹size X = n› ring_distribs sum_mset.distrib sum_mset_subtractf 
                      sum_mset_distrib_left)
      finally show "(∏w∈#X. σ (z + ω - w)) = c / exp (η ω * sum_mset X) * (∏w∈#X. σ (z - w))"
        by (simp add: exp_diff c_def ‹size X = n›)
    qed

    show "weierstrass_multi_sigma A B (z + ω) = weierstrass_multi_sigma A B z"
      using same_size by (simp add: weierstrass_multi_sigma_def * n_def exp_diff sum_eq)
  qed

  show "weierstrass_multi_sigma A B (z + ω1) = weierstrass_multi_sigma A B z"
       "weierstrass_multi_sigma A B (z + ω2) = weierstrass_multi_sigma A B z" for z
    using *[of ω1] *[of ω2] by simp_all
qed

end

locale nicely_elliptic_multiple_sigma = elliptic_multiple_sigma +
  assumes disjoint: "⋀a b. a ∈# A ⟹ b ∈# B ⟹ ¬rel a b"
begin

sublocale nicely_elliptic_function ω1 ω2 "weierstrass_multi_sigma A B"
  by standard (use disjoint in ‹auto intro!: meromorphic_intros›)

end



subsubsection ‹Writing concrete elliptic functions in terms of $\sigma$›

lemma (in elliptic_function) in_terms_of_sigma_explicit_aux:
  assumes "⋀z. zorder f z = int (count_rel A z) - int (count_rel B z)"
  assumes "sum_mset A = sum_mset B"
  assumes "elliptic_order f > 0"
  shows "size A = size B"
proof -
  define P where "P = period_parallelogram 0"
  define P' where "P' = to_fund_parallelogram ` (set_mset (A + B))"

  have "((λz. zorder f z) has_sum 0) P"
    using has_sum_zorder_0[of 0] ‹elliptic_order f > 0› by (simp add: P_def)
  also have "?this ⟷ ((λz. zorder f z) has_sum 0) P'"
  proof (rule has_sum_cong_neutral)
    fix z assume "z ∈ P - P'"
    hence "count_rel A z = 0" "count_rel B z = 0"
      using to_fund_parallelogram_unique by (auto simp: P_def P'_def count_rel_eq_0_iff)
    thus "zorder f z = 0"
      by (simp add: assms(1))
  qed (auto simp: P'_def P_def)
  also have "… ⟷ ((∑z∈P'. zorder f z) = 0)"
    by (subst has_sum_finite_iff) (auto simp: P'_def)
  also have "(∑z∈P'. zorder f z) = int (∑z∈P'. count_rel A z) - int (∑z∈P'. count_rel B z)"
    by (simp add: assms(1) sum_subtractf)
  also have "… = int (size A) - int (size B)"
    by (subst (1 2) sum_count_rel_eq_size) (auto simp: P'_def)
  finally show "size A = size B"
    by simp
qed

text ‹
  Consider an elliptic function $f$.
  Given a complete set of representatives of the zeros $A$ and the poles $B$
  (with the right multiplicities) such that $\sum A = \sum B$, we can write $f$ in terms of 
  the Weierstra\ss\ ‹σ› function as
  \[ f(z) = c \frac{\prod_{a\in A} \sigma(z-a)}{\prod_{b\in B} \sigma(z-b)} \]
  where $c$ is a constant. Note that $A$ and $B$ are multisets here.

  This is useful when trying to establish a relationship between ‹σ› and a particular elliptic
  function with known zeros and poles. Later, we will apply this to a function of the form
  $\wp(z) - \wp(z_0)$.
›
lemma (in elliptic_function) in_terms_of_sigma_explicit:
  assumes "⋀z. zorder f z = int (count_rel A z) - int (count_rel B z)"
  assumes "sum_mset A = sum_mset B"
  assumes "elliptic_order f > 0"
  obtains c where "c ≠ 0" "∀⇩≈z. f z = c * weierstrass_multi_sigma A B z"
proof -
  define h where "h = (λz. f z / weierstrass_multi_sigma A B z)"
  have "size A = size B"
    by (rule in_terms_of_sigma_explicit_aux) (use assms in auto)
  interpret construct: elliptic_multiple_sigma ω1 ω2 A B
    by standard (use ‹size A = size B› ‹sum_mset A = sum_mset B› in auto)
  interpret h: elliptic_function ω1 ω2 h
    unfolding h_def by (intro elliptic_function_intros)

  have "¬is_pole h z" for z
  proof -
    have "has_zorder h z 0"
      unfolding h_def
    proof (rule has_zorder_divide)
      show "has_zorder f z (zorder f z)"
        using avoid'[of 0] ‹elliptic_order f > 0›
        by (auto simp: has_zorder_def intro!: meromorphic_on_subset[OF meromorphic])
    next
      show "has_zorder (weierstrass_multi_sigma A B) z (zorder f z)"
        using assms(1)[of z] has_zorder_weierstrass_multi_sigma[of A B z] by simp
    qed auto
    thus "¬is_pole h z"
      using has_zorder_imp_is_pole_iff by blast
  qed
  hence "elliptic_order h = 0"
    using h.elliptic_order_eq_0_iff_no_poles by metis
  then obtain c where c: "∀⇩≈z. h z = c"
    using h.elliptic_order_eq_0_iff_const_cosparse by blast

  have "∀⇩≈z. ∀w∈#(A+B). ¬rel z w"
    by (intro eventually_ball_finite ballI eventually_not_rel_cosparse) auto
  hence ev_nz: "∀⇩≈z. weierstrass_multi_sigma A B z ≠ 0"
    by eventually_elim (auto simp: weierstrass_multi_sigma_eq_0_iff rel_sym)

  have "c ≠ 0"
  proof -
    have "∀⇩≈z. f z ≠ 0"
      using avoid[of 0] ‹elliptic_order f > 0› by simp
    with ev_nz c have "∀⇩≈(z::complex). c ≠ 0"
      by eventually_elim (auto simp: h_def)
    thus ?thesis
      by simp
  qed

  show ?thesis
  proof (rule that)
    have "∀⇩≈z. ∀w∈#(A+B). ¬rel z w"
      by (intro eventually_ball_finite ballI eventually_not_rel_cosparse) auto
    show "∀⇩≈z. f z = c * weierstrass_multi_sigma A B z"
      using ev_nz c by eventually_elim (auto simp: h_def)
  qed fact+
qed

text ‹
  For nicely elliptic functions we can slightly strengthen the conclusion from
  ``equal except at singularities'' to ``equal everywhere''.
›
lemma (in nicely_elliptic_function) in_terms_of_sigma_explicit':
  assumes "⋀z. zorder f z = int (count_rel A z) - int (count_rel B z)"
  assumes disjoint: "⋀a b. a ∈# A ⟹ b ∈# B ⟹ ¬rel a b"
  assumes "sum_mset A = sum_mset B"
  assumes "elliptic_order f > 0"
  obtains c where "c ≠ 0" "⋀z. f z = c * weierstrass_multi_sigma A B z"
proof -
  obtain c where c: "c ≠ 0" "∀⇩≈z. f z = c * weierstrass_multi_sigma A B z"
    by (rule in_terms_of_sigma_explicit[of A B]) (use assms in auto)
  have "size A = size B"
    by (rule in_terms_of_sigma_explicit_aux) (use assms in auto)
  interpret multi_sigma: nicely_elliptic_multiple_sigma ω1 ω2 A B
    by standard (use assms ‹size A = size B› in auto)
  show ?thesis
  proof (rule that[of c])
    fix z :: complex
    show "f z = c * weierstrass_multi_sigma A B z" using c(2)
      by (rule nicely_meromorphic_on_cosparse_eq_imp_eq) (auto intro!: meromorphic_intros)
  qed fact+
qed

text ‹
  We now look at two concrete examples.

  First, we consider the function $f(z) = \wp(z) - \wp(z_0)$ for some $z_0\notin\Lambda$.
  This function has a double pole at every lattice point and a single zero at lattice equivalents
  of $\pm z_0$, except if $2z_0\in\Lambda$, in which case it has a double zero at lattice
  equivalents of $z_0$.

  In either case, the representatives $A = \{z_0, -z_0\}$ for the zeroes and $B = \{0, 0\}$ 
  for the poles satisfy the requirements of the theorem above and we obtain
  \[ \wp(z) - \wp(z_0) = c \frac{\sigma(z+z_0)\sigma(z-z_0)}{\sigma(z)^2}\]
  for some constant $c$.

  It remains to determine what the constant $c$ is. To do this, we inspect the leading coefficient
  of the Laurent series expansion of both sides at $z = 0$. More concretely, we multiply both sides
  with $z^2$ and take the limit as $z\to 0$. This way, we easily find that 
  $c = -\frac{1}{\sigma(z_0)^2}$ and therefore:
  \[\wp(z) = \wp(z_0) - \frac{\sigma(z+z_0)\sigma(z-z_0)}{\sigma(z)^2 \sigma(z_0)^2}\]
›
theorem (in complex_lattice) weierstrass_fun_conv_sigma_half_period:
  assumes z0: "z0 ∉ Λ" and z: "z ∉ Λ"
  defines "σ ≡ weierstrass_sigma"
  shows "℘ z = ℘ z0 - σ (z + z0) * σ (z - z0) / (σ z * σ z0)⇧2"
proof -
  define g where "g = (λz. ℘ z - ℘ z0)"
  interpret g: weierstrass_fun_minus_const ω1 ω2 z0 g
    by unfold_locales (use z0 in ‹auto simp: g_def›)
  write weierstrass_sigma ("σ")

  obtain c where c: "∀⇩≈z. g z = c * σ (z - z0) * σ (z + z0) / σ z ^ 2"
  proof (rule g.affine.in_terms_of_sigma_explicit)
    show "elliptic_order g > 0"
      by (auto simp: g.order_eq)
  next
    show "zorder g z = int (count_rel {#z0, -z0#} z) - int (count_rel {#0, 0#} z)" for z
    proof -
      consider "z ∈ Λ" | "rel z z0 ∨ rel z (-z0)" | "z ∉ Λ" "¬rel z z0 ∧ ¬rel z (-z0)"
        by blast
      thus ?thesis
      proof cases
        assume z: "z ∈ Λ"
        have "¬rel z z0"
          using z0 z rel_lattice_trans_left by blast
        with z z0 show ?thesis
          by (subst g.zorder_pole_eq)
             (auto simp: is_pole_weierstrass_fun_iff zorder_weierstrass_fun_pole 
                         rel_def uminus_in_lattice_iff diff_in_lattice_commute)
      next
        assume z: "rel z z0 ∨ rel z (-z0)"
        from z have "z ∉ Λ"
          using z0 rel_lattice_trans_left uminus_in_lattice_iff by blast
        have "2 * z0 ∈ Λ ⟷ rel z z0 ∧ rel z (-z0)"
        proof
          assume "2 * z0 ∈ Λ"
          hence "rel z z0 ⟷ rel z (-z0)"
            using add_in_lattice[of "z - z0" "2 * z0"] diff_in_lattice[of "z + z0" "2 * z0"]
            by (auto simp: add.commute rel_def)
          thus "rel z z0 ∧ rel z (-z0)"
            using z by auto
        next
          assume "rel z z0 ∧ rel z (-z0)"
          hence "rel z0 (-z0)"
            using rel_trans rel_sym by blast
          thus "2 * z0 ∈ Λ"
            by (auto simp: rel_def)
        qed
        with z ‹z ∉ Λ› show ?thesis
          by (auto simp: g.zorder_zero_eq rel_def diff_in_lattice_commute uminus_in_lattice_iff)
      qed (auto simp: g.zorder_zero_eq' rel_def uminus_in_lattice_iff diff_in_lattice_commute)
    qed
  qed (auto simp: weierstrass_multi_sigma_def power2_eq_square mult_ac)

  have c_eq: "c = -1 / σ z0 ^ 2"
  proof -
    note [tendsto_intros] =
      isContD[of _ "λz. σ (z - z0)"] isContD[of _ "λz. σ (z + z0)"] isContD[of _ weierstrass_sigma.f]
    have "(λz. z ^ 2 * ℘ z - z ^ 2 * ℘ z0 - c * σ (z - z0) * σ (z + z0) / weierstrass_sigma.f z ^ 2)
             ─0→ (1 - 0 ^ 2 * ℘ z0 - c * σ (0 - z0) * σ (0 + z0) / weierstrass_sigma.f 0 ^ 2)"
    proof (intro tendsto_intros analytic_at_imp_isCont analytic_intros)
      have *: "(λz. z⇧2 * ℘ z) has_laurent_expansion (fls_X ^ 2 * fls_weierstrass)"
        by (intro laurent_expansion_intros)
      have "fls_subdegree (fls_X⇧2 * fls_weierstrass) = 0"
        by (subst fls_subdegree_mult) (auto simp: fls_subdegree_weierstrass)
      hence "(λz. z⇧2 * ℘ z) ─0→ fls_nth (fls_X⇧2 * fls_weierstrass) 0"
        using has_laurent_expansion_imp_tendsto_0[OF *] by simp
      also have "fls_nth (fls_X⇧2 * fls_weierstrass) 0 = 1"
        by (simp add: fls_X_power_conv_shift_1 fls_X_intpow_times_conv_shift 
                      fls_weierstrass_def fps_weierstrass_def)
      finally show "(λz. z⇧2 * ℘ z) ─0→ 1" .
    qed auto
    also have "?this ⟷ (λz::complex. 0) ─0→ (1 + c * σ z0 ^ 2)"
    proof (rule filterlim_cong)
      have "eventually (λz. g z = c * σ (z - z0) * σ (z + z0) / σ z ^ 2) (at 0)"
        using c by (auto simp: eventually_cosparse_open_eq)
      thus "∀⇩F x in at 0. x⇧2 * ℘ x - x⇧2 * ℘ z0 - c * σ (x - z0) * σ (x + z0) /
                                      (weierstrass_sigma.f x)⇧2 = 0"
        using eventually_neq_at_within[of 0]
      proof eventually_elim
        case (elim z)
        thus ?case
          by (auto simp: g_def weierstrass_sigma_def[of z] field_simps power2_eq_square)
      qed
    qed (auto simp: weierstrass_sigma_uminus power2_eq_square mult_ac)
    finally have "0 = 1 + c * σ z0 ^ 2"
      by (simp add: tendsto_const_iff)
    thus "c = -1 / σ z0 ^ 2"
      using z0 by (auto simp: field_simps weierstrass_sigma_eq_0_iff add_eq_0_iff)
  qed

  have "g z = c * σ (z - z0) * σ (z + z0) / (σ z)⇧2"
    using c
  proof (rule analytic_on_continuation)
    show "g analytic_on (-Λ)"
      by (auto simp: g_def intro!: analytic_intros)
    show "(λz. c * σ (z - z0) * σ (z + z0) / σ z ^ 2) analytic_on (-Λ)"
      by (auto intro!: analytic_intros simp: weierstrass_sigma_eq_0_iff)
  qed (use z in auto)
  thus ?thesis
    by (simp add: g_def c_eq field_simps σ_def)
qed

text ‹
  Next, we analogously derive a formula for $\wp'(z)$ interms of $\sigma$, namely:
  \[\wp'(z) = \frac{2}{\sigma(z)^3} \prod_{i=1,2,3} \frac{\sigma(z-h_i)}{\sigma(h_i)}\]
  where $h_1 = \frac{1}{2}\omega_1$, $h_2 = \frac{1}{2}\omega_2$, and 
  $h_3 = -\frac{1}{2}(\omega_1+\omega_2)$.
›
theorem (in complex_lattice) weierstrass_fun_deriv_conv_sigma_half_period:
  defines "σ ≡ weierstrass_sigma"
  shows "℘' z = 2 / σ z ^ 3 * (∏w←[ω1/2, ω2/2, -(ω1+ω2)/2]. σ (z-w) / σ w)"
proof -
  write weierstrass_sigma ("σ")
  define h1 where "h1 = of_ω12_coords (1/2, 0)"
  define h2 where "h2 = of_ω12_coords (0, 1/2)"
  define h3 where "h3 = of_ω12_coords (-1/2, -1/2)"
  have "h3 ∉ Λ"
    using half_periods_notin_lattice(3) uminus_in_lattice_iff[of "(ω1+ω2)/2"]
    by (auto simp: h3_def add_divide_distrib diff_divide_distrib of_ω12_coords_def minus_diff_commute)
  hence h123: "∀h∈{h1,h2,h3}. h ∉ Λ ∧ 2 * h ∈ Λ"
    by (auto simp: h1_def h2_def h3_def lattice_intros diff_divide_distrib of_ω12_coords_def)
  have h123_unique: "¬rel h1 h2 ∧ ¬rel h1 h3 ∧ ¬rel h2 h3"
    unfolding h1_def h2_def h3_def rel_def of_ω12_coords.diff [symmetric] of_ω12_coords_in_lattice_iff
    by auto
  have zorder_h123: "∀h∈{h1,h2,h3}. zorder ℘' h = 1"
    using h123 by (auto intro!: zorder_weierstrass_fun_deriv_zero)
  have [simp]: "zorder ℘' (to_fund_parallelogram z) = zorder ℘' z" for z
    by (rule weierstrass_fun_deriv.zorder.lattice_cong) auto
  have zorder_0: "zorder ℘' z = 0" if "z ∉ Λ" "∀h∈{h1,h2,h3}. ¬rel z h" for z
  proof -
    have "rel ((ω1 + ω2) / 2) h3"
      by (auto simp: rel_def h3_def of_ω12_coords_def diff_divide_distrib add_divide_distrib)
    hence *: "2 * z ∉ Λ"
      using that rel_half_period[of z] rel_trans[of z "(ω1+ω2)/2" h3]
      by (auto simp: h1_def h2_def h3_def of_ω12_coords_def)
    show ?thesis
    by (rule zorder_eq_0I) 
       (use that * in ‹auto intro!: analytic_intros simp: weierstrass_fun_deriv_eq_0_iff›)
  qed

  obtain c where c: "⋀z. ℘' z = c * σ (z - h1) * σ (z - h2) * σ (z - h3) / σ z ^ 3"
  proof (rule weierstrass_fun_deriv.in_terms_of_sigma_explicit')
    show "elliptic_order ℘' > 0"
      by simp
  next
    show "zorder ℘' z = int (count_rel {#h1, h2, h3#} z) - int (count_rel {#0, 0, 0#} z)" for z
    proof -
      define z' where "z' = to_fund_parallelogram z"
      have rel_iff: "rel w z ⟷ to_fund_parallelogram w = z'" for w
        by (auto simp: z'_def simp flip: to_fund_parallelogram_eq_iff)
      have z_in_lattice_iff: "z ∈ Λ ⟷ z' = 0"
        by (auto simp: z'_def)
      have *: "zorder ℘' z = zorder ℘' z'"
        by (simp add: z'_def)
      show ?thesis
        using h123 h123_unique zorder_h123 zorder_0[of z]
        by (auto simp: rel_iff zorder_weierstrass_fun_deriv_pole rel_sym z_in_lattice_iff *)
    qed
  next
    fix a b :: complex
    assume "a ∈# {#h1, h2, h3#}" "b ∈# {#0, 0, 0#}"
    thus "¬rel a b"
      using h123 by (auto simp: rel_def)
  qed (auto simp: h1_def h2_def h3_def of_ω12_coords_def weierstrass_multi_sigma_def 
                  mult_ac power_numeral_reduce)

  have c_eq: "c = 2 / (σ h1 * σ h2 * σ h3)"
  proof -
    note [tendsto_intros] =
      isContD[of _ "λz. σ (z - w)" for w] isContD[of _ weierstrass_sigma.f]
    have "(λz. z ^ 3 * ℘' z - c * σ (z - h1) * σ (z - h2) * σ (z - h3) / weierstrass_sigma.f z ^ 3)
             ─0→ (-2 - c * σ (0 - h1) * σ (0 - h2) * σ (0 - h3) / weierstrass_sigma.f 0 ^ 3)"
    proof (intro tendsto_intros analytic_at_imp_isCont analytic_intros)
      have *: "(λz. z ^ 3 * ℘' z) has_laurent_expansion (fls_X ^ 3 * fls_deriv fls_weierstrass)"
        by (intro laurent_expansion_intros)
      have "fls_subdegree (fls_X ^ 3 * fls_deriv fls_weierstrass) = 0"
      proof (subst fls_subdegree_mult)
        have "fls_nth (fls_deriv fls_weierstrass) (-3) ≠ fls_nth 0 (-3)"
          by (auto simp: fls_weierstrass_def)
        thus "fls_deriv fls_weierstrass ≠ 0"
          by metis
      qed (auto simp: fls_subdegree_weierstrass fls_subdegree_deriv)
      hence "(λz. z ^ 3 * ℘' z) ─0→ fls_nth (fls_X ^ 3 * fls_deriv fls_weierstrass) 0"
        using has_laurent_expansion_imp_tendsto_0[OF *] by simp
      also have "fls_nth (fls_X ^ 3 * fls_deriv fls_weierstrass) 0 = -2"
        by (simp add: fls_X_power_conv_shift_1 fls_X_intpow_times_conv_shift 
                      fls_weierstrass_def fps_weierstrass_def)
      finally show "(λz. z ^ 3 * ℘' z) ─0→ -2" .
    qed auto
    also have "?this ⟷ (λz::complex. 0) ─0→ (-2 + c * σ h1 * σ h2 * σ h3)"
    proof (rule filterlim_cong)
      have "eventually (λz. ℘' z = c * σ (z - h1) * σ (z - h2) * σ (z - h3) / σ z ^ 3) (at 0)"
        using c by (auto simp: eventually_cosparse_open_eq)
      thus "∀⇩F x in at 0. x ^ 3 * ℘' x - c * σ (x - h1) * σ (x - h2) * σ (x - h3) /
                                      weierstrass_sigma.f x ^ 3 = 0"
        using eventually_neq_at_within[of 0]
      proof eventually_elim
        case (elim z)
        thus ?case
          by (auto simp: weierstrass_sigma_def[of z] field_simps power2_eq_square)
      qed
    qed (auto simp: weierstrass_sigma_uminus mult_ac)
    finally have "0 = -2 + c * σ h1 * σ h2 * σ h3"
      by (simp add: tendsto_const_iff)
    thus "c = 2 / (σ h1 * σ h2 * σ h3)"
      using h123 by (auto simp: field_simps weierstrass_sigma_eq_0_iff add_eq_0_iff)
  qed

  show ?thesis using c[of z]
    by (simp add: c_eq field_simps σ_def h1_def h2_def h3_def of_ω12_coords_def minus_diff_commute)
qed


subsubsection ‹Generic representation theorem in terms of $\sigma$›

text ‹
  Lastly, we prove a generic theorem for an arbitrary elliptic function, showing that it can
  be written in the form $c \cdot \sigma_{A,B}$ for an appropriate constant $c$ and
  multisets $A$ and $B$.

  The construction is fairly straightforward: $A$ consists of all zeros in the fundamental
  parallelogram (with appropriate multiplicities) and $B$ of all the poles. However, this will
  violate the condition that $\sum A = \sum B$, so we pick some arbitrary zero $a\in A$ and shift
  it by a lattice point in order to make things work out.
›
theorem (in elliptic_function) in_terms_of_sigma:
  obtains c A B 
  where "size A = elliptic_order f" "⋀z. z ∈# A ⟹ isolated_zero f z"
        "size B = elliptic_order f" "⋀z. z ∈# B ⟹ is_pole f z"
        "sum_mset A = sum_mset B"
        "∀⇩≈z. f z = c * weierstrass_multi_sigma A B z"
proof (cases "elliptic_order f = 0")
  case True
  then obtain c where c: "∀⇩≈z. f z = c"
    using elliptic_order_eq_0_iff_const_cosparse by blast
  show ?thesis
    using that[of "{#}" "{#}" c] c True by (auto simp: weierstrass_multi_sigma_def)
next
  case False
  define P where "P = period_parallelogram 0"
  note fin = finite_poles_in_parallelogram[of 0, folded P_def]
             finite_zeros_in_parallelogram[of 0, folded P_def]
  define A where "A = (∑z | z ∈ P ∧ isolated_zero f z. replicate_mset (nat (zorder f z)) z)"
  define B where "B = (∑z | z ∈ P ∧ is_pole f z. replicate_mset (nat (-zorder f z)) z)"
  have "size A = elliptic_order f"
    using zeros_eq_elliptic_order[of 0] by (simp add: A_def P_def)
  have "size B = elliptic_order f"
    using poles_eq_elliptic_order[of 0] by (simp add: B_def P_def)
  have "A ≠ {#}"
    using False ‹size A = _› by auto
  then obtain a where a: "a ∈# A"
    by blast
  define d where "d = sum_mset A - sum_mset B"
  have "d ∈ Λ"
  proof -
    have "d = (∑z | z ∈ P ∧ isolated_zero f z. of_nat (nat (zorder f z)) * z) -
              (∑z | z ∈ P ∧ is_pole f z. of_nat (nat (- zorder f z)) * z)"
      by (simp add: d_def A_def B_def sum_mset_sum)
    also have "(∑z | z ∈ P ∧ isolated_zero f z. of_nat (nat (zorder f z)) * z) =
               (∑z | z ∈ P ∧ isolated_zero f z. of_int (zorder f z) * z)"
      using False by (intro sum.cong) (auto simp: isolated_zero_iff_zorder_pos)
    also have "(∑z | z ∈ P ∧ is_pole f z. of_nat (nat (- zorder f z)) * z) =
               (∑z | z ∈ P ∧ is_pole f z. -of_int (zorder f z) * z)"
      using False by (intro sum.cong) (auto simp: is_pole_iff_zorder_neg) 
    also have "(∑z | z ∈ P ∧ isolated_zero f z. of_int (zorder f z) * z) -
               (∑z | z ∈ P ∧ is_pole f z. -of_int (zorder f z) * z) =
               (∑z∈{z∈P. isolated_zero f z}∪{z∈P. is_pole f z}. of_int (zorder f z) * z)"
      using fin pole_is_not_zero[of f]
      by (subst sum.union_disjoint) (auto simp: sum_negf)
    also have "… = (∑z | z ∈ P ∧ (isolated_zero f z ∨ is_pole f z). of_int (zorder f z) * z)"
      by (rule sum.cong) auto
    also have "… ∈ Λ"
      using sum_zeros_poles_in_lattice[of 0, folded P_def] .
    finally show ?thesis .
  qed

  define a' where "a' = a - d"
  define A' where "A' = A - {#a#} + {#a'#}"
  have "size A' = elliptic_order f"
    using ‹size A = _› a by (simp add: A'_def size_Suc_Diff1)

  obtain c where c: "∀⇩≈z. f z = c * weierstrass_multi_sigma A' B z"
  proof (rule in_terms_of_sigma_explicit[of A' B])
    fix z :: complex
    define P' where "P' = {w∈P. rel w z}"

    have [simp]: "card P' = 1"
    proof -
      have "P' = {to_fund_parallelogram z}"
        using to_fund_parallelogram_eq_iff[of z] to_fund_parallelogram_unique[of z]
        unfolding P'_def P_def by (auto simp: rel_sym)
      thus ?thesis
        by simp
    qed

    have 1: "count_rel A' z = nat (zorder f z)"
    proof -
      have "rel a a'"
        using ‹d ∈ Λ› by (auto simp: a'_def rel_def)
      moreover have "Suc (count_rel A z - Suc 0) = count_rel A z" if "rel a z"
        by (subst Suc_diff_Suc) (use that a in ‹auto simp: count_rel_pos_iff›)
      ultimately have "count_rel A' z = count_rel A z"
        using a rel_trans[of a a' z] rel_trans[of a' a z]
        by (auto simp: A'_def count_rel_diff_subset rel_sym)
      also have "… = (∑w | w ∈ P ∧ isolated_zero f w. if rel w z then nat (zorder f w) else 0)"
        by (auto simp: A_def count_rel_sum)
      also have "… = (∑w | w ∈ P' ∧ isolated_zero f z. nat (zorder f w))"
        by (rule sum.mono_neutral_cong_right) (use fin zeros.lattice_cong in ‹auto simp: P'_def›)
      also have "… = (∑w∈(if isolated_zero f z then P' else {}). nat (zorder f z))"
        by (intro sum.cong) 
           (auto intro!: arg_cong[of _ _ nat] zorder.lattice_cong simp: P'_def split: if_splits)
      also have "… = nat (zorder f z)"
        using False by (auto simp: isolated_zero_iff_zorder_pos)
      finally show "count_rel A' z = nat (zorder f z)" .
    qed

    have 2: "count_rel B z = nat (-zorder f z)"
    proof -
      have "count_rel B z = (∑w | w ∈ P ∧ is_pole f w. if rel w z then nat (-zorder f w) else 0)"
        by (auto simp: B_def count_rel_sum)
      also have "… = (∑w | w ∈ P' ∧ is_pole f z. nat (-zorder f w))"
        by (rule sum.mono_neutral_cong_right) (use fin poles.lattice_cong in ‹auto simp: P'_def›)
      also have "… = (∑w∈(if is_pole f z then P' else {}). nat (-zorder f z))"
        by (intro sum.cong) 
           (auto intro!: arg_cong[of _ _ nat] zorder.lattice_cong simp: P'_def split: if_splits)
      also have "… = nat (-zorder f z)"
        using False by (auto simp: is_pole_iff_zorder_neg)
      finally show "count_rel B z = nat (-zorder f z)" .
    qed

    show "zorder f z = int (count_rel A' z) - int (count_rel B z)"
      by (simp add: 1 2)
  next
    show "sum_mset A' = sum_mset B"
      using a by (simp add: A'_def sum_mset_diff a'_def d_def)
  qed (use False in auto)

  show ?thesis
  proof (rule that)
    show "size A' = elliptic_order f" "size B = elliptic_order f"
      by fact+
    from ‹d ∈ Λ› have "isolated_zero f a' ⟷ isolated_zero f a"
      by (intro zeros.lattice_cong) (auto simp: a'_def rel_def uminus_in_lattice_iff)
    thus "isolated_zero f z" if "z ∈# A'" for z
      using that fin a by (auto simp: A'_def A_def set_mset_sum dest!: in_diffD)
    show "is_pole f z" if "z ∈# B" for z
      using that fin by (auto simp: B_def set_mset_sum)
    show "∀⇩≈z. f z = c * weierstrass_multi_sigma A' B z"
      by fact
    show "sum_mset A' = sum_mset B"
      using a by (simp add: A'_def sum_mset_diff a'_def d_def)
  qed
qed

lemma (in nicely_elliptic_function) in_terms_of_sigma':
  obtains c A B 
  where "size A = elliptic_order f" "⋀z. z ∈# A ⟹ isolated_zero f z"
        "size B = elliptic_order f" "⋀z. z ∈# B ⟹ is_pole f z"
        "⋀z. f z = c * weierstrass_multi_sigma A B z"
proof -
  obtain c A B where cAB:
    "size A = elliptic_order f" "⋀z. z ∈# A ⟹ isolated_zero f z"
    "size B = elliptic_order f" "⋀z. z ∈# B ⟹ is_pole f z"
    "sum_mset A = sum_mset B"
    "∀⇩≈z. f z = c * weierstrass_multi_sigma A B z"
    by (rule in_terms_of_sigma) auto
  have disjoint: "¬rel a b" if "a ∈# A" "b ∈# B" for a b
    using cAB(2,4) that pole_is_not_zero poles.lattice_cong by blast

  interpret multi_sigma: nicely_elliptic_multiple_sigma ω1 ω2 A B
    by standard (use cAB disjoint in auto)
  show ?thesis
  proof (rule that[of A B c])
    fix z :: complex
    show "f z = c * weierstrass_multi_sigma A B z" using cAB(6)
      by (rule nicely_meromorphic_on_cosparse_eq_imp_eq) (auto intro!: meromorphic_intros)
  qed fact+
qed


subsection ‹Addition and duplication theorems›

context complex_lattice
begin

theorem weierstrass_sigma_add_diff:
  assumes u: "u ∉ Λ" and v: "v ∉ Λ"
  shows "weierstrass_sigma (u + v) * weierstrass_sigma (u - v) =
           (℘ v - ℘ u) * weierstrass_sigma u ^ 2 * weierstrass_sigma v ^ 2"
proof -
  write weierstrass_sigma ("σ")
  write weierstrass_eta ("η")

  text ‹
    We consider the following function:
      \[g(u) = \frac{\sigma(u+v)\sigma(u-v)}{\sigma(u)^2\sigma(v)^2} + \wp(u)\]
  ›
  define g where "g = (λu. σ (u + v) * σ (u - v) / (σ u * σ v)⇧2 + ℘ u)"

  text ‹
    Due to the periodicity of ‹℘› and the quasiperiodicity of ‹σ›, this is an ellpitic function.
  ›
  interpret g: elliptic_function ω1 ω2 g
  proof
    show "g meromorphic_on UNIV"
      by (auto simp: g_def intro!: meromorphic_intros)
         (auto intro!: analytic_on_imp_meromorphic_on analytic_intros)?
  next
    have *: "g (z + ω) = g z" if ω: "ω ∈ Λ" "ω / 2 ∉ Λ" for ω z
    proof -
      have "g (z + ω) = σ (z + v + ω) * σ (z - v + ω) / (σ (z + ω) * σ v)⇧2 + ℘ (z + ω)"
        by (simp add: g_def algebra_simps)
      also have "… = exp (η ω * (z + v + ω / 2)) * exp (η ω * (z - v + ω / 2)) / 
                        exp (η ω * (z + ω / 2)) ^ 2 *
                      (σ (z + v) * σ (z - v) / (σ z * σ v)⇧2) + ℘ (z + ω)"
        by (subst (1 2 3) weierstrass_sigma_plus_lattice_weak)
           (use ω v in ‹auto simp: weierstrass_sigma_eq_0_iff field_simps›)
      also have "exp (η ω * (z + v + ω / 2)) * exp (η ω * (z - v + ω / 2)) /
                   exp (η ω * (z + ω / 2)) ^ 2 = 1"
        unfolding exp_of_nat_mult [symmetric] exp_add [symmetric] exp_diff [symmetric]
        by (simp add: algebra_simps)
      also have "℘ (z + ω) = ℘ z"
        by (rule weierstrass_fun.lattice_cong) (use ω in ‹auto simp: rel_def›)
      also have "1 * (σ (z + v) * σ (z - v) / (σ z * σ v)⇧2) + ℘ z = g z"
        by (simp add: g_def)
      finally show ?thesis .
    qed
    show "g (z + ω1) = g z" "g (z + ω2) = g z" for z
      using *[of ω1] *[of ω2] by simp_all
  qed

  text ‹
    Since the constituent functions only have poles at lattice points, our \<^term>‹g› cannot have
    poles except at the lattice points either.
  ›
  have no_poles_off_lattice: "¬is_pole g z" if z: "z ∉ Λ" for z
  proof -
    from z have "g analytic_on {z}" using v
      by (auto simp: g_def weierstrass_sigma_eq_0_iff intro!: analytic_intros)
    thus ?thesis
      using analytic_at_imp_no_pole by blast
  qed

  text ‹
    Now comes the most tedious part: we show that the poles at the lattice points cancel.
    Due to ellipticity, it is of course enough to show this for the origin.
  ›
  have "¬is_pole g 0"
  proof
    assume "is_pole g 0"

    define h where "h = (λu. σ (u + v) * σ (u - v) / σ v ^ 2)"
    define F1 where "F1 = fps_expansion h 0"
    have F1: "h has_fps_expansion F1"
      unfolding F1_def using v
      by (intro fps_expansion_intros analytic_at_imp_has_fps_expansion_0)
         (auto simp: h_def weierstrass_sigma_eq_0_iff intro!: analytic_intros)
    have "h 0 = -1" using v 
      by (simp add: h_def weierstrass_sigma_uminus power2_eq_square weierstrass_sigma_eq_0_iff)
    hence "fps_nth F1 0 = -1"
      using has_fps_expansion_imp_0_eq_fps_nth_0[OF F1] by simp
    hence "subdegree F1 = 0"
      by (intro subdegreeI) auto
    have [simp]: "F1 ≠ 0"
      using ‹fps_nth F1 0 = -1› by auto
    
    define F2 where "F2 = fps_weierstrass_sigma"
    have F2: "σ has_fps_expansion F2"
      unfolding F2_def by (intro fps_expansion_intros)

    define F3 where "F3 = fls_weierstrass"
    define F where "F = fps_to_fls F1 / (fps_to_fls F2)⇧2 + F3"

    have F: "g has_laurent_expansion F"
    proof -
      have "(λu. h u / σ u ^ 2 + ℘ u) has_laurent_expansion F"
        unfolding F_def F3_def using v
        by (intro laurent_expansion_intros F1 F2 has_laurent_expansion_fps)
      also have "(λu. h u / σ u ^ 2 + ℘ u) = g"
        by (simp add: g_def h_def divide_simps fun_eq_iff)
      finally show ?thesis .
    qed
    have [simp]: "F ≠ 0"
      using F ‹is_pole g 0› is_pole_0_imp_neg_fls_subdegree by fastforce

    have "fls_subdegree F ≤ -2"
    proof -
      have "(∑z | z ∈ period_parallelogram 0 ∧ is_pole g z. nat (-zorder g z)) = elliptic_order g"
        by (rule g.poles_eq_elliptic_order)
      also have "{z. z ∈ period_parallelogram 0 ∧ is_pole g z} = {0}"
      proof (intro equalityI subsetI)
        fix z assume "z ∈ {z. z ∈ period_parallelogram 0 ∧ is_pole g z}"
        hence z: "z ∈ period_parallelogram 0" "z ∈ Λ"
          using no_poles_off_lattice by auto
        from z(2) obtain m n where z_eq: "z = of_ω12_coords (of_int m, of_int n)"
          by (auto simp: lattice_def elim!: Ints_cases)
        from z(1) show "z ∈ {0}"
          by (auto simp: period_parallelogram_altdef z_eq)
      qed (use ‹is_pole g 0› in auto)
      finally have "nat (-zorder g 0) = elliptic_order g"
        by simp
      moreover have "g meromorphic_on {0}"
        by (intro meromorphic_on_subset[OF g.meromorphic]) auto
      hence "zorder g 0 < 0" using ‹is_pole g 0›
        by (intro isolated_pole_imp_neg_zorder meromorphic_on_isolated_singularity)
      ultimately have "zorder g 0 = -int (elliptic_order g)"
        by simp
      moreover have "elliptic_order g ≥ 2"
        using g.elliptic_order_neq_1 g.elliptic_order_eq_0_iff_no_poles ‹is_pole g 0› by auto
      ultimately have "zorder g 0 ≤ -2"
        by simp
      also have "zorder g 0 = fls_subdegree F"
        using has_laurent_expansion_zorder_0[OF F] by auto
      finally show ?thesis .
    qed
    moreover have "fls_subdegree F ≥ -2"
    proof -
      have "min (fls_subdegree (fps_to_fls F1 / (fps_to_fls F2)⇧2)) (fls_subdegree F3) ≤ fls_subdegree F"
        unfolding F_def by (rule fls_plus_subdegree) (use ‹F ≠ 0› in ‹auto simp: F_def›)
      also have "fls_subdegree F3 = -2"
        unfolding F3_def by (simp add: fls_subdegree_weierstrass)
      also have "fls_subdegree (fps_to_fls F1 / (fps_to_fls F2)⇧2) = -2"
        by (subst fls_divide_subdegree) 
           (auto simp: fls_subdegree_fls_to_fps ‹subdegree F1 = _› F2_def
                 simp flip: fps_to_fls_power)
      finally show ?thesis
        by simp
    qed
    ultimately have "fls_subdegree F = -2"
      by linarith

    have "fls_nth F (-2) = 0"
    proof -
      have "fls_nth (fps_to_fls F1 / (fps_to_fls F2)⇧2) (-2) = 
              fls_nth (fps_to_fls F1 / (fps_to_fls F2)⇧2) 
                (fls_subdegree (fps_to_fls F1) - fls_subdegree (fps_to_fls F2 ^ 2))"
        by (simp add: fls_subdegree_fls_to_fps ‹subdegree F1 = _› F2_def
                 flip: fps_to_fls_power)
      also have "… = fps_nth F1 0 / fps_nth (F2 ^ 2) (2 * subdegree F2)"
        by (subst fls_divide_nth_base)
           (auto simp: fls_subdegree_fls_to_fps ‹subdegree F1 = _› F2_def
                 simp flip: fps_to_fls_power)
      also have "… = -1"
        by (subst fps_pow_base) (auto simp: F2_def ‹fps_nth F1 0 = _›)
      finally show ?thesis
        by (simp add: F_def F3_def fls_weierstrass_def)
    qed
    also have "-2 = fls_subdegree F"
      by (rule sym) fact
    finally have "F = 0"
      by simp
    thus False
      using ‹F ≠ 0› by contradiction
  qed

  text ‹
    It follows that the function has no poles and must therefore be constant except possibly for
    removable singularities at the lattice points.
  ›
  have no_poles: "¬is_pole g z" for z
  proof (cases "z ∈ Λ")
    case True
    hence "rel z 0"
      by (auto simp: rel_def)
    hence "is_pole g z ⟷ is_pole g 0"
      by (rule g.poles.lattice_cong)
    with ‹¬is_pole g 0› show ?thesis
      by auto
  qed (use no_poles_off_lattice in auto)
  hence "elliptic_order g = 0"
    by (simp add: elliptic_order_def)
  then obtain c where c: "∀⇩≈z. g z = c"
    using g.elliptic_order_eq_0_iff_const_cosparse by blast

  text ‹
    By looking at $g(v)$, we determine the constant to be $\wp(v)$, which concludes the proof.
  ›
  hence g_eq: "g z = c" if z: "z ∉ Λ" for z
  proof (rule analytic_on_continuation)
    show "g analytic_on {z}"
      using z v by (auto simp: g_def weierstrass_sigma_eq_0_iff intro!: analytic_intros)
  qed auto
  have c_eq: "c = ℘ v"
    using g_eq[of v] v by (simp add: g_def)

  have "g u = ℘ v"
    using u by (simp add: g_eq c_eq)
  thus ?thesis
    using u v by (simp add: g_def weierstrass_sigma_eq_0_iff field_simps)
qed

text ‹
  From the addition theorem for ‹σ›, it is also easy to derive two related three-term identities:
›
corollary weierstrass_sigma_three_term:
  assumes uvw: "u ∉ Λ" "v ∉ Λ" "w ∉ Λ"
  defines "σ ≡ weierstrass_sigma"
  shows   "σ (u+v) * σ (u-v) * σ w ^ 2 +
           σ (v+w) * σ (v-w) * σ u ^ 2 + 
           σ (w+u) * σ (w-u) * σ v ^ 2 = 0"
  unfolding σ_def
  by (subst (1 2 3) weierstrass_sigma_add_diff) (use uvw in ‹auto simp: algebra_simps›)

corollary weierstrass_sigma_sym_three_term:
  assumes uxyz: "u ∉ Λ" "x ∉ Λ" "y ∉ Λ" "z ∉ Λ"
  defines "σ ≡ weierstrass_sigma"
  shows   "σ (u+x) * σ (u-x) * σ (y+z) * σ (y-z) +
           σ (u+y) * σ (u-y) * σ (z+x) * σ (z-x) +
           σ (u+z) * σ (u-z) * σ (x+y) * σ (x-y) = 0"
proof -
  have *: "a * b * c * d = (a * b) * (c * d)" for a b c d :: complex
    by (simp add: mult_ac)
  show ?thesis unfolding σ_def *
    by (subst (1 2 3 4 5 6) weierstrass_sigma_add_diff) (use uxyz in ‹auto simp: algebra_simps›)
qed

text ‹
  Taking the derivative of the addition formula for ‹σ› and setting $v = u$, we obtain the
  duplication formula:
›
theorem weierstrass_sigma_duplication:
  assumes u: "u ∉ Λ" "2 * u ∉ Λ"
  shows "weierstrass_sigma (2 * u) = -℘' u * weierstrass_sigma u ^ 4"
proof -
  write weierstrass_sigma ("σ")
  write weierstrass_zeta ("ζ")
  write weierstrass_eta ("η")

  define S where "S = σ ∘ (λv. u - v)"
  have [derivative_intros]: "(S has_field_derivative (1 * (-1))) (at u)" unfolding S_def 
    by (intro DERIV_chain) (auto intro!: derivative_eq_intros has_field_derivative_weierstrass_sigma_0)
  have [simp]: "S u = 0"
    by (simp add: S_def)
  define g where "g = (λv. σ (u + v) * S v - (℘ v - ℘ u) * σ u ^ 2 * σ v ^ 2)"
  note [derivative_intros] = has_field_derivative_weierstrass_sigma_0[folded S_def]

  have "(g has_field_derivative (-σ (2 * u) - ℘' u * (σ u)⇧2 * (σ u)⇧2)) (at u)"
    unfolding g_def using u by (auto intro!: derivative_eq_intros)
  also have "?this ⟷ ((λ_. 0) has_field_derivative (-σ (2 * u) - ℘' u * (σ u)⇧2 * (σ u)⇧2)) (at u)"
  proof (rule DERIV_cong_ev)
    have "eventually (λv. v ∈ -Λ) (nhds u)"
      by (rule eventually_nhds_in_open) (use closed_lattice u in auto)
    thus "eventually (λv. g v = 0) (nhds u)"
    proof eventually_elim
      case (elim v)
      thus ?case
        unfolding g_def S_def using weierstrass_sigma_add_diff[of u v] u by simp
    qed
  qed auto
  finally have "((λ_. 0) has_field_derivative (-σ (2 * u) - ℘' u * σ u ^ 4)) (at u)"
    by (simp add: power_numeral_reduce mult_ac)
  moreover have "((λ_. 0) has_field_derivative 0) (at u)" by simp
  ultimately have "-σ (2 * u) - ℘' u * σ u ^ 4 = 0"
    using DERIV_unique by blast
  thus ?thesis
    by Groebner_Basis.algebra
qed


text ‹
  By taking the logarithmic derivative of the addition formula for $\sigma$, 
  we obtain the addition formula for $\zeta$. This is only well-defined if $u\neq \pm v$.
›
theorem weierstrass_zeta_add:
  assumes u: "u ∉ Λ" and v: "v ∉ Λ" and "¬rel u v" "¬rel u (-v)"
  shows "weierstrass_zeta (u + v) = 
           weierstrass_zeta u + weierstrass_zeta v + 1 / 2 * (℘' v - ℘' u) / (℘ v - ℘ u)"
proof -
  have uv: "u + v ∉ Λ" "u - v ∉ Λ"
    using assms weierstrass_fun.lattice_cong'[of u v] by (auto simp: rel_def)
  have "℘ u ≠ ℘ v"
    using assms weierstrass_fun_eq_iff by simp
  write weierstrass_sigma ("σ")
  write weierstrass_zeta ("ζ")
  write weierstrass_eta ("η")

  define g where "g = (λu v. σ (u + v) * σ (u - v) / ((℘ v - ℘ u) * σ u ^ 2 * σ v ^ 2))"
  have g1: "g u v = 1"
    using weierstrass_sigma_add_diff[of u v] u v uv by (auto simp: g_def weierstrass_sigma_eq_0_iff)

  have g2: "eventually (λu. g u v = 1) (at u)"
  proof -
    show ?thesis
      using eventually_not_rel_at[of 0 u] eventually_not_rel_at[of v u]
            eventually_not_rel_at[of "-v" u]
    proof eventually_elim
      case (elim u)
      thus ?case
        using weierstrass_sigma_add_diff[of u v] v
        by (auto simp: g_def weierstrass_sigma_eq_0_iff rel_def)
    qed
  qed

  have g3: "eventually (λv. g u v = 1) (at v)"
  proof -
    show ?thesis
      using eventually_not_rel_at[of 0 v] eventually_not_rel_at[of u v]
            eventually_not_rel_at[of "-u" v]
    proof eventually_elim
      case (elim v)
      thus ?case
        using weierstrass_sigma_add_diff[of u v] u
        by (auto simp: g_def weierstrass_sigma_eq_0_iff rel_def add_ac diff_in_lattice_commute)
    qed
  qed

  have 1: "ζ (u - v) = -ζ (u + v) + 2 * ζ u - ℘' u / (℘ v - ℘ u)"
  proof -
    define h where "h = (λu. ℘ v - ℘ u)"
    define D where "D = (ζ (u + v) + ζ (u - v) + ℘' u / (℘ v - ℘ u) - 2 * ζ u)"
    have [derivative_intros]: "(h has_log_derivative (-℘' u / (℘ v - ℘ u))) (at u)"
      using u ‹℘ u ≠ ℘ v› unfolding h_def
      by (intro has_field_derivative_imp_has_log_derivative) (auto intro!: derivative_eq_intros)
    have "((λu. σ (u + v) * σ (u - v) / (h u * σ u ^ 2 * σ v ^ 2)) has_log_derivative D) (at u)"
      using u v uv by (auto intro!: derivative_eq_intros simp: weierstrass_sigma_eq_0_iff D_def)
    also have "?this ⟷ ((λ_. 1) has_log_derivative D) (at u)"
    proof (rule has_log_derivative_cong_ev)
      show "∀⇩F u in at u. σ (u + v) * σ (u - v) / (h u * (σ u)⇧2 * (σ v)⇧2) = 1"
        using g2 by eventually_elim (auto simp: g_def h_def)
    qed (use g1 in ‹auto simp: h_def g_def›)
    finally have "((λ_. 1) has_log_derivative D) (at u)" .
    moreover have "((λ_. 1) has_log_derivative 0) (at u)"
      by auto
    ultimately have "D = 0"
      by (rule has_log_derivative_unique) auto
    thus ?thesis
      by (simp add: D_def algebra_simps)
  qed

  have 2: "ζ (u - v) = ζ (u + v) - 2 * ζ v - ℘' v / (℘ v - ℘ u)"
  proof -
    define h where "h = (λv. ℘ v - ℘ u)"
    define D where "D = (ζ (u + v) - ζ (u - v) - ℘' v / (℘ v - ℘ u) - 2 * ζ v)"
    have [derivative_intros]: "(h has_log_derivative (℘' v / (℘ v - ℘ u))) (at v)"
      using u v ‹℘ u ≠ ℘ v› unfolding h_def
      by (intro has_field_derivative_imp_has_log_derivative) (auto intro!: derivative_eq_intros)
    have "((λv. σ (u + v) * σ (u - v) / (h v * σ u ^ 2 * σ v ^ 2)) has_log_derivative D) (at v)"
      using u v uv by (auto intro!: derivative_eq_intros simp: weierstrass_sigma_eq_0_iff D_def)
    also have "?this ⟷ ((λ_. 1) has_log_derivative D) (at v)"
    proof (rule has_log_derivative_cong_ev)
      show "∀⇩F v in at v. σ (u + v) * σ (u - v) / (h v * (σ u)⇧2 * (σ v)⇧2) = 1"
        using g3 by eventually_elim (auto simp: g_def h_def)
    qed (use g1 in ‹auto simp: h_def g_def›)
    finally have "((λ_. 1) has_log_derivative D) (at v)" .
    moreover have "((λ_. 1) has_log_derivative 0) (at v)"
      by auto
    ultimately have "D = 0"
      by (rule has_log_derivative_unique) auto
    thus ?thesis
      by (simp add: D_def algebra_simps)
  qed

  have "-ζ (u + v) + 2 * ζ u - ℘' u / (℘ v - ℘ u) = ζ (u + v) - 2 * ζ v - ℘' v / (℘ v - ℘ u)"
    using 1 2 by simp
  hence "2 * ζ (u + v) = 2 * (ζ u + ζ v) + ℘' v / (℘ v - ℘ u) - ℘' u / (℘ v - ℘ u)"
    by Groebner_Basis.algebra
  also have "… = 2 * (ζ u + ζ v) + (℘' v - ℘' u) / (℘ v - ℘ u)"
    by (simp add: divide_simps)
  also have "… = 2 * (ζ u + ζ v + 1/2 * (℘' v - ℘' u) / (℘ v - ℘ u))"
    by (simp add: algebra_simps)
  finally show "ζ (u + v) = ζ u + ζ v + 1 / 2 * (℘' v - ℘' u) / (℘ v - ℘ u)"
    by Groebner_Basis.algebra
qed

text ‹
  Taking the logarithmic derivative of the duplication identity for $\sigma$ gives us the
  one for $\zeta$:
›
theorem weierstrass_zeta_duplication:
  assumes u: "u ∉ Λ" "2 * u ∉ Λ"
  shows "weierstrass_zeta (2 * u) = 2 * weierstrass_zeta u + (3 * ℘ u ^ 2 - 15 * G 4) / ℘' u"
proof -
  write weierstrass_sigma ("σ")
  write weierstrass_zeta ("ζ")

  define g where "g = (λu. -σ (2 * u) / (℘' u * σ u ^ 4))"
  define D where "D = 2 * ζ (2 * u) - (6 * (℘ u)⇧2 - 30 * G 4) / ℘' u - 4 * ζ u"
  have [derivative_intros]: "(℘' has_log_derivative ((6 * ℘ u ^ 2 - 30 * G 4) / ℘' u)) (at u)"
    using u by (auto intro!: has_field_derivative_imp_has_log_derivative derivative_eq_intros 
                     simp: weierstrass_fun_deriv_eq_0_iff)
  have "(g has_log_derivative D) (at u)"
    using u by (auto simp: D_def g_def weierstrass_sigma_eq_0_iff intro!: derivative_eq_intros)
  also have "?this ⟷ ((λ_. 1) has_log_derivative D) (at u)"
  proof (rule has_log_derivative_cong_ev')
    have "eventually (λu. u ∈ -Λ) (nhds u)"
      by (intro eventually_nhds_in_open) (use closed_lattice u in auto)
    moreover have "eventually (λu. u ∈ (λw. 2 * w) -` (-Λ)) (nhds u)"
      by (intro eventually_nhds_in_open open_vimage continuous_intros) (use u closed_lattice in auto)
    ultimately show "eventually (λu. g u = 1) (nhds u)"
    proof eventually_elim
      case (elim u)
      thus ?case
        using weierstrass_sigma_duplication[of u] by (auto simp: g_def weierstrass_sigma_eq_0_iff)
    qed
  qed
  finally have "((λ_. 1) has_log_derivative D) (at u)" .
  moreover have "((λ_. 1) has_log_derivative 0) (at u)" by auto
  ultimately have "D = 0"
    by (rule has_log_derivative_unique) auto
  hence "2 * ζ (2 * u) - 2 * ((3 * ℘ u ^ 2 - 15 * G 4) / ℘' u) = 4 * ζ u"
    by (simp add: D_def)
  thus ?thesis
    by Groebner_Basis.algebra
qed

end

end