Theory Complex_Lattices_Theta

section ‹Connection between complex lattices and theta functions›
theory Complex_Lattices_Theta
  imports Eisenstein_Series "Theta_Functions.Theta_Nullwert"
begin

(* TODO Move. Or rather, fix whatever causes these problems. *)
lemmas [simp del] = div_mult_self1 div_mult_self2 div_mult_self3 div_mult_self4

(* TODO Move *)
lemma analytic_at_continuation:
  assumes "eventually (λz. f z = g z) (at z)" "f analytic_on {z}" "g analytic_on {z}"
  shows   "f z = g z"
proof -
  have "isCont (λz. f z - g z) z"
    by (intro analytic_at_imp_isCont analytic_intros assms)
  hence "(λz. f z - g z) ─z→ (f z - g z)"
    by (rule isContD)
  also have "?this ⟷ (λz. 0) ─z→ (f z - g z)"
    by (intro filterlim_cong eventually_mono[OF assms(1)]) auto
  finally show "f z = g z"
    by (simp add: tendsto_const_iff)
qed

(* TODO Move *)
lemma analytic_on_continuation:
  assumes "eventually (λz. f z = g z) (cosparse B)" "f analytic_on A" "g analytic_on A" "z ∈ A ∩ B"
  shows   "f z = g z"
  using analytic_at_continuation[of f g z] assms analytic_on_subset
  by (auto dest: eventually_cosparse_imp_eventually_at)

unbundle jacobi_theta_nw_notation


text ‹
  We make the connection to theta functions. In order to do that, we first assume that the
  generators $\omega_1$ and $\omega_2$ are such that their ratio $\tau := \omega_2/\omega_1$ has
  positive imaginary part.
›
locale complex_lattice_Im_pos = complex_lattice +
  assumes Im_ratio_pos: "Im ratio > 0"
begin

text ‹
  We fix this ratio $\tau$ as the second parameter of the theta functions so that the theta
  functions become quasi-elliptic functions in one variable $z$.
›
definition theta_00 ("(‹notation=‹mixfix complex_lattice_Im_pos.theta_00››θ00'(_'))")
  where "theta_00 z ≡ jacobi_theta_00 (z / ω1) τ"

definition theta_01 ("(‹notation=‹mixfix complex_lattice_Im_pos.theta_00››θ01'(_'))")
  where "theta_01 z ≡ jacobi_theta_01 (z / ω1) τ"

definition theta_10 ("(‹notation=‹mixfix complex_lattice_Im_pos.theta_00››θ10'(_'))")
  where "theta_10 z ≡ jacobi_theta_10 (z / ω1) τ"

definition theta_11 ("(‹notation=‹mixfix complex_lattice_Im_pos.theta_00››θ11'(_'))")
  where "theta_11 z ≡ jacobi_theta_11 (z / ω1) τ"

lemma theta_01_conv_00: "theta_01 z = theta_00 (z + ω1 / 2)"
  by (simp add: theta_01_def jacobi_theta_01_def theta_00_def add_divide_distrib)

lemma theta_10_conv_00: "theta_10 z = to_nome (z / ω1 + τ / 4) * theta_00 (z + ω2 / 2)"
  by (simp add: theta_10_def jacobi_theta_10_def theta_00_def add_divide_distrib ratio_def mult_ac)

lemma theta_11_conv_00:
  "theta_11 z = to_nome (z / ω1 + τ / 4 + 1 / 2) * theta_00 (z + (ω1 + ω2) / 2)"
  by (simp add: theta_11_def jacobi_theta_11_def theta_00_def add_divide_distrib
                ratio_def algebra_simps)

text ‹
  The four zeta functions then each have their zeros at various lattice or half-lattice points.
›
lemma theta_00_eq_0_iff: "θ00(z) = 0 ⟷ rel z ((ω1 + ω2) / 2)" for z
proof
  assume "θ00(z) = 0"
  then obtain m n :: int where "z / ω1 = (of_int m + 1 / 2) + (of_int n + 1 / 2) * τ"
    using Im_ratio_pos by (auto simp: theta_00_def jacobi_theta_00_eq_0_iff_complex)
  hence "z = (ω1 + ω2) / 2 + of_int m * ω1 + of_int n * ω2"
    by (auto simp: ratio_def divide_simps) (auto simp: algebra_simps)?
  also have "rel … ((ω1 + ω2) / 2)"
    by (auto simp: rel_def intro!: lattice_intros)
  finally show "rel z ((ω1 + ω2) / 2)" .
next
  assume "rel z ((ω1 + ω2) / 2)"
  then obtain m n :: int where "z = (ω1 + ω2) / 2 + of_int m * ω1 + of_int n * ω2"
    by (auto simp: rel_def of_ω12_coords_def field_simps elim!: latticeE)
  also have "… / ω1 = (of_int m + 1 / 2) + (of_int n + 1 / 2) * τ"
    by (auto simp: ratio_def field_simps)
  also have "jacobi_theta_00 … τ = 0"
    by (rule jacobi_theta_00_eq_0')
  finally show "θ00(z) = 0"
    by (simp add: theta_00_def)
qed

lemma theta_01_eq_0_iff: "θ01(z) = 0 ⟷ rel z (ω2 / 2)"
  unfolding theta_01_conv_00 theta_00_eq_0_iff rel_def 
  by (simp add: add_divide_distrib)

lemma theta_10_eq_0_iff: "θ10(z) = 0 ⟷ rel z (ω1 / 2)"
  unfolding theta_10_conv_00 
  by (simp add: theta_00_eq_0_iff add_divide_distrib rel_def)

lemma theta_11_eq_0_iff: "θ11(z) = 0 ⟷ z ∈ Λ"
  unfolding theta_11_conv_00 
  by (simp add: theta_00_eq_0_iff add_divide_distrib rel_def)

lemma zorder_theta_00: "zorder theta_00 ((ω1 + ω2) / 2) = 1"
proof -
  define z0 where "z0 = (ω1 + ω2) / 2"
  have z0_over_ω1: "z0 / ω1 = (τ + 1) / 2"
    by (auto simp: z0_def ratio_def field_simps)
  have *: "(λz. theta_00 (z0 + z)) = ((λz. θ00((τ + 1) / 2 + z ; τ)) ∘ (λz. z / ω1))"
    unfolding z0_over_ω1 [symmetric] by (simp add: theta_00_def [abs_def] o_def add_divide_distrib)

  define F where "F = fps_expansion (λz. θ00(z ; τ)) ((τ + 1) / 2)"
  have F: "(λz. θ00((τ + 1) / 2 + z ; τ)) has_fps_expansion F"
    unfolding F_def by (intro analytic_at_imp_has_fps_expansion analytic_intros Im_ratio_pos)
  have F': "(λz. theta_00 (z0 + z)) has_fps_expansion (F oo (fps_X / fps_const ω1))" 
    unfolding F_def *
    by (intro fps_expansion_intros analytic_at_imp_has_fps_expansion
              analytic_intros Im_ratio_pos) auto

  have nz: "F oo (fps_X / fps_const ω1) ≠ 0"
  proof
    assume "F oo (fps_X / fps_const ω1) = 0"
    hence "(λz. θ00(z0 + z)) has_fps_expansion 0"
      using F' by simp
    hence "θ00(z0 + (-z0)) = 0"
      by (rule has_fps_expansion_0_analytic_continuation[where A = UNIV])
         (auto intro!: holomorphic_intros simp: theta_00_def [abs_def] Im_ratio_pos)
    thus False
      by (simp add: theta_00_eq_0_iff rel_def uminus_in_lattice_iff)
  qed
  hence [simp]: "F ≠ 0"
    by auto

  have "1 = zorder (λz. θ00(z ; τ)) ((τ + 1) / 2)"
    by (subst jacobi_theta_00_simple_zero) (simp_all add: Im_ratio_pos jacobi_theta_00_eq_0)
  also have "… = subdegree F"
    using has_fps_expansion_zorder[OF F] by simp
  also have "… = zorder theta_00 z0"
    using has_fps_expansion_zorder[OF F'] nz by simp
  finally show ?thesis
    by (simp add: z0_def)
qed

text ‹
  By comparing the zeros of $\wp(z) - e_2$ and $(\vartheta_{01}(z)/\vartheta_{11}(z))^2$ we
  find that the two functions are identical up to a constant factor, which we then determine
  to be $(\pi\vartheta_{10}(0)\vartheta_{00}(0)/\omega_1)^2$ by comparing the Laurent series expansions
  of the two functions at their pole at the origin.

  It follows that we can express $\wp$ in terms of the constant $e_2$ and the theta functions.
›
lemma weierstrass_fun_conv_theta:
  assumes z: "z ∉ Λ"
  shows   "℘ z = 𝖾2 + (pi * θ10(0) * θ00(0) / ω1) ^ 2 * θ01(z) ^ 2 / θ11(z) ^ 2" 
proof -
  define f where "f = (λz. ℘ z - number_e2)"
  interpret f: weierstrass_fun_minus_const ω1 ω2 "ω2 / 2" f
    by unfold_locales (auto simp: f_def number_e2_def)
  define g where "g = (λz. (theta_01 z / theta_11 z) ^ 2)"

  interpret g: even_elliptic_function ω1 ω2 g
  proof                     
    fix z :: complex
    show "g (z + ω1) = g z"
      by (simp add: g_def add_divide_distrib theta_01_def theta_11_def 
                    jacobi_theta_01_left.plus_1 jacobi_theta_11_plus1_left)
  next
    fix z :: complex
    have "g (z + ω2) = g z * (to_nome (τ + 2 * z / ω1) / to_nome (2 * z / ω1 + τ)) ^ 2"
      by (simp add: g_def add_divide_distrib ratio_def jacobi_theta_01_plus_quasiperiod 
                    jacobi_theta_11_plus_quasiperiod power_divide theta_01_def theta_11_def)
    also have "to_nome (τ + 2 * z / ω1) / to_nome (2 * z / ω1 + τ) = 1"
      unfolding to_nome_diff [symmetric] by simp
    finally show "g (z + ω2) = g z"
      by simp
  next
    show "g meromorphic_on UNIV"
      unfolding g_def theta_01_def theta_11_def using Im_ratio_pos
      by (intro meromorphic_intros analytic_on_imp_meromorphic_on analytic_intros) auto
  next
    fix z show "g (-z) = g z"
      by (auto simp: g_def theta_01_def theta_11_def)
  qed

  define Z where "Z = {z ∈ half_fund_parallelogram ∖ {0}. is_pole g z ∨ isolated_zero g z}"
  define h where "h = (λz. zorder g z div (if 2 * z ∈ Λ then 2 else 1))"
  have [analytic_intros]: "g analytic_on A" if "A ∩ Λ = {}" for A
    using Im_ratio_pos that theta_11_eq_0_iff unfolding g_def theta_01_def theta_11_def
    by (auto intro!: analytic_intros)

  have g_nz: "¬(∀≈z. g z = 0)"
  proof
    assume "∀≈z. g z = 0"
    moreover have "∀≈z. g z ≠ 0"
      using eventually_not_rel_cosparse[of "ω2 / 2"] eventually_not_in_lattice_cosparse
      by eventually_elim (auto simp: g_def theta_01_eq_0_iff theta_11_eq_0_iff)
    ultimately have "∀≈z::complex. False"
      by eventually_elim auto
    thus False
      by simp
  qed

  define z0 where "z0 = ω2 / 2"
  have z0: "z0 ∈ half_fund_parallelogram" "z0 ≠ 0" "z0 ∉ Λ" "rel z0 (ω2 / 2)"
    by (auto simp: half_fund_parallelogram_altdef z0_def)

  have zero_at_z0: "isolated_zero g z0"
  proof (subst g.isolated_zero_analytic_iff)
    show "g analytic_on {z0}" using z0
      by (auto intro!: analytic_intros)
  next
    show "g z0 = 0" using z0
      by (auto simp: g_def theta_01_eq_0_iff)
  qed (use g_nz in auto)

  have Z_eq: "Z = {z0}"
  proof (intro equalityI subsetI)
    fix z assume "z ∈ Z"
    hence z: "z ∈ half_fund_parallelogram" "z ≠ 0" and z': "is_pole g z ∨ isolated_zero g z"
      by (auto simp: Z_def)
    have "z ∉ Λ"
      using z by (metis half_fund_parallelogram_in_lattice_iff)
    hence "g analytic_on {z}"
      by (auto intro!: analytic_intros)
    hence "¬is_pole g z"
      by (rule analytic_at_imp_no_pole)
    with z' have "isolated_zero g z"
      by auto
    hence "g z = 0"
      using ‹g analytic_on {z}› by (simp add: zero_isolated_zero_analytic)
    with ‹z ∉ Λ› have "rel z (ω2 / 2)"
      by (auto simp: g_def theta_01_eq_0_iff theta_11_eq_0_iff)
    moreover have "ω2 / 2 ∈ period_parallelogram 0"
      unfolding period_parallelogram_altdef by auto
    moreover have "z ∈ period_parallelogram 0"
      using z(1) half_fund_parallelogram_subset_period_parallelogram by blast
    ultimately show "z ∈ {z0}"
      using to_fund_parallelogram_unique' unfolding z0_def by blast
  next
    fix z assume "z ∈ {z0}"
    thus "z ∈ Z"
      using z0 zero_at_z0 by (auto simp: Z_def)
  qed

  define A where "A = fps_expansion theta_01 0"
  define B where "B = fps_expansion theta_11 0"
  have A[fps_expansion_intros]: "theta_01 has_fps_expansion A"
    unfolding A_def theta_01_def
    by (intro analytic_at_imp_has_fps_expansion_0 analytic_intros) (use Im_ratio_pos in auto)
  have B[fps_expansion_intros]: "theta_11 has_fps_expansion B"
    unfolding B_def theta_11_def
    by (intro analytic_at_imp_has_fps_expansion_0 analytic_intros) (use Im_ratio_pos in auto)

  have A0: "fps_nth A 0 = θ01(0)"
    using has_fps_expansion_imp_0_eq_fps_nth_0[OF A] by (simp add: theta_01_def)
  have [simp]: "A ≠ 0"
  proof -
    have "fps_nth A 0 ≠ 0"
      by (auto simp: A0 theta_01_eq_0_iff rel_def uminus_in_lattice_iff)
    thus "A ≠ 0"
      by auto
  qed
  have [simp]: "subdegree A = 0"
    by (rule subdegree_eq_0)
       (use theta_01_eq_0_iff[of 0] in ‹auto simp: A0 rel_def uminus_in_lattice_iff›)

  have B0: "fps_nth B 0 = 0"
    using has_fps_expansion_imp_0_eq_fps_nth_0[OF B] by (simp add: theta_11_def)
  have B1: "fps_nth B (Suc 0) = deriv theta_11 0"
    using fps_nth_fps_expansion[OF B, of 1] by simp
  have B1': "fps_nth B (Suc 0) = 
               -(of_real pi * theta_00 0 * theta_01 0 * theta_10 0 / ω1)"
  proof -
    have "(((λx. jacobi_theta_11 x τ) ∘ (λx. x / ω1)) has_field_derivative 
            (deriv (λx. jacobi_theta_11 x τ) (0 / ω1) * (1 / ω1))) (at 0)"
      unfolding B1 using Im_ratio_pos
      by (intro DERIV_chain analytic_derivI analytic_intros)
         (auto intro!: derivative_eq_intros)
    hence "(theta_11 has_field_derivative  (deriv (λx. jacobi_theta_11 x τ) 0 / ω1)) (at 0)"
      by (simp add: o_def theta_11_def [abs_def])
    thus ?thesis
      unfolding B1 using Im_ratio_pos
      by (intro DERIV_imp_deriv) 
         (simp add: deriv_jacobi_theta_11_at_0 theta_00_def theta_01_def theta_10_def mult_ac)
  qed
  have B1_nz: "fps_nth B (Suc 0) ≠ 0"
    by (auto simp: B1' theta_00_eq_0_iff theta_01_eq_0_iff theta_10_eq_0_iff 
                   rel_def uminus_in_lattice_iff)
  have [simp]: "B ≠ 0"
    using B1_nz by auto
  have [simp]: "subdegree B = 1"
    by (rule subdegreeI) (auto simp: B1_nz B0)
  have B1_nz: "fps_nth B (Suc 0) ≠ 0"
    using nth_subdegree_nonzero[of B] by (simp del: nth_subdegree_nonzero)
  obtain c where "∀≈z. g z = c * (∏w∈Z. (℘ z - ℘ w) powi h w)"
    using g.in_terms_of_weierstrass_fun_even_aux[OF g_nz]
    unfolding h_def unfolding Z_def by blast
  also have "(λz. c * (∏w∈Z. (℘ z - ℘ w) powi h w)) = (λz. c * (℘ z - 𝖾2) powi h z0)"
    by (simp add: Z_eq z0_def number_e2_def)
  also have "h z0 = zorder g z0 div 2"
    by (simp add: h_def z0_def)
  also have "zorder g z0 = 2"
  proof -
    (* TODO: this could probably be simplified using Laurent series *)
    have ev_nz: "∀F z in at z0. θ01(z) ≠ 0" "∀F z in at z0. θ11(z) ≠ 0"
      using eventually_not_rel_cosparse[of "ω2/2"] eventually_not_in_lattice_cosparse
      by (auto simp: theta_01_eq_0_iff theta_11_eq_0_iff dest: eventually_cosparse_imp_eventually_at)
    from z0 have nz: "θ11(z0) ≠ 0"
      by (subst theta_11_eq_0_iff) auto

    have "∀F z in at z0. θ01(z) / θ11(z) ≠ 0"
      using ev_nz by eventually_elim auto
    hence "zorder g z0 = 2 * zorder (λz. θ01(z) / θ11(z)) z0 "
      unfolding g_def using ev_nz nz
      by (subst zorder_power) 
         (auto simp: theta_11_def [abs_def] theta_01_def [abs_def] Im_ratio_pos theta_11_eq_0_iff
               intro!: analytic_on_imp_meromorphic_on analytic_intros eventually_frequently)
    also have "zorder (λz. θ01(z) / θ11(z)) z0 = zorder (λz. θ01(z)) z0 - zorder (λz. θ11(z)) z0"
      using ev_nz by (subst zorder_divide)
                     (auto intro!: analytic_on_imp_meromorphic_on analytic_intros eventually_frequently
                           simp: theta_01_def [abs_def] theta_11_def [abs_def] Im_ratio_pos)
    also from Im_ratio_pos and nz have "zorder (λz. θ11(z)) z0 = 0"
      by (intro zorder_eq_0I) (auto simp: theta_11_def [abs_def] intro!: analytic_intros)
    also have "zorder theta_01 z0 = zorder theta_00 ((ω1 + ω2) / 2)"
      by (simp add: theta_01_conv_00 [abs_def] zorder_shift' z0_def add_ac add_divide_distrib)
    also have "… = 1"
      by (rule zorder_theta_00)
    finally show "zorder g z0 = 2"
      by simp
  qed
  finally have g_eq: "∀≈z. g z = c * (℘ z - 𝖾2)"
    by simp
  
  have g_eq': "g z = c * (℘ z - 𝖾2)" if "z ∉ Λ" for z
    using g_eq
  proof (rule analytic_on_continuation)
    show "z ∈ (-Λ) ∩ UNIV"
      using that by auto
  qed (auto intro!: analytic_intros)

  define F where "F = ((fps_to_fls A / fps_to_fls B) ^ 2 - fls_const c * (fls_weierstrass - fls_const 𝖾2))"

  have "(λz. g z - c * (℘ z - 𝖾2)) has_laurent_expansion F"
    unfolding F_def g_def
    by (intro laurent_expansion_intros has_laurent_expansion_fps fps_expansion_intros)
  also have "?this ⟷ (λz. 0) has_laurent_expansion F"
  proof (rule has_laurent_expansion_cong)
    have "∀F x in at 0. g x = c * (℘ x - 𝖾2)"
      using g_eq by (auto dest: eventually_cosparse_imp_eventually_at)
    thus "∀F x in at 0. g x - c * (℘ x - 𝖾2) = 0"
      by eventually_elim auto
  qed auto
  finally have "F = 0"
    by (rule zero_has_laurent_expansion_imp_eq_0)

  have "0 = fls_nth F (-2)"
    by (simp add: ‹F = 0›)
  also have "… = fls_nth ((fps_to_fls A / fps_to_fls B)2) (- 2) - c"
    by (simp add: fls_weierstrass_def F_def)
  also have "-2 = int 2 * fls_subdegree (fps_to_fls A / fps_to_fls B)"
    by (subst fls_divide_subdegree) (auto simp: fls_subdegree_fls_to_fps)
  also have "fls_nth ((fps_to_fls A / fps_to_fls B) ^ 2) … = 
               (fls_nth (fps_to_fls A / fps_to_fls B) (-1))2"
    by (subst fls_pow_base) (auto simp: fls_divide_subdegree fls_subdegree_fls_to_fps)
  also have "-1 = fls_subdegree (fps_to_fls A) - fls_subdegree (fps_to_fls B)"
    by (simp add: fls_subdegree_fls_to_fps)
  also have "fls_nth (fps_to_fls A / fps_to_fls B) … = θ01(0) / fps_nth B (Suc 0)"
    by (subst fls_divide_nth_base) 
       (auto simp: fls_subdegree_fls_to_fps A0 B1 theta_01_def)
  finally have c_eq: "c = (θ01(0) / fps_nth B (Suc 0)) ^ 2"
    by simp

  have "℘ z = 𝖾2 + (fps_nth B 1 / θ01(0)) ^ 2 * θ01(z) ^ 2 / θ11(z) ^ 2"
    using g_eq'[of z] theta_01_eq_0_iff[of 0] theta_11_eq_0_iff[of z] z B1_nz
    by (auto simp: c_eq g_def rel_def uminus_in_lattice_iff field_simps)
  also have "(fps_nth B 1 / θ01(0)) ^ 2 * θ01(z) ^ 2 / θ11(z) ^ 2 =
               (of_real pi * θ10(0) * θ00(0) / ω1)2 * θ01(z)2 / θ11(z)2"
    by (simp add: B1' field_simps theta_01_eq_0_iff rel_def uminus_in_lattice_iff)
  finally show ?thesis .
qed

text ‹
  By plugging in values into the above identity, we derive expressions for $e_1$, $e_2$, $e_3$
  and the lattice modulus $\lambda$ purely in terms of theta functions.
›
lemma e12_conv_theta: "𝖾1 - 𝖾2 = (pi / ω1) ^ 2 * θ00(0) ^ 4"
  and e32_conv_theta: "𝖾3 - 𝖾2 = (pi / ω1) ^ 2 * θ10(0) ^ 4"
  and e13_conv_theta: "𝖾1 - 𝖾3 = (pi / ω1) ^ 2 * θ01(0) ^ 4"
  and e1_conv_theta:  "𝖾1 = (pi / ω1) ^ 2 / 3 * (θ00(0) ^ 4 + θ01(0) ^ 4)"
  and e2_conv_theta:  "𝖾2 = -(pi / ω1)2 / 3 * (θ00(0) ^ 4 + θ10(0) ^ 4)"
  and e3_conv_theta:  "𝖾3 = (pi / ω1)2 / 3 * (θ10(0) ^ 4 - θ01(0) ^ 4)"
  and modulus_conv_theta: "modulus = θ10(0) ^ 4 / θ00(0) ^ 4"
proof -
  have "𝖾1 - 𝖾2 = (of_real pi * θ10(0) * θ00(0) / ω1)2 * θ01(ω1/2)2 / θ11(ω1/2)2"
    using weierstrass_fun_conv_theta[of "ω1 / 2"]
    unfolding number_e1_def by simp
  also have "θ01(ω1/2) = θ00(0)"
    using jacobi_theta_00_left.plus_1[of 0 τ]
    by (simp add: jacobi_theta_01_def theta_00_def theta_01_def)
  also have "θ11(ω1/2) = -θ10(0)"
    using jacobi_theta_00_left.plus_1[of "τ / 2" τ]
    by (simp add: jacobi_theta_11_def algebra_simps to_nome_add jacobi_theta_10_def 
                  theta_10_def theta_11_def)
  also have "(of_real pi * θ10(0) * θ00(0) / ω1)2 * θ00(0)2 / (- θ10(0))2 =
               (pi / ω1) ^ 2 * θ00(0) ^ 4"
    using theta_10_eq_0_iff[of 0] by (simp add: field_simps rel_def uminus_in_lattice_iff)
  finally show e12: "𝖾1 - 𝖾2 = (pi / ω1) ^ 2 * θ00(0) ^ 4" .

  have "𝖾3 - 𝖾2 = (of_real pi * θ10(0) * θ00(0) / ω1)2 * 
                         (θ01((ω1 + ω2) / 2) / θ11((ω1 + ω2) / 2))2"
    using weierstrass_fun_conv_theta[of "(ω1 + ω2) / 2"] unfolding number_e3_def
    by (simp add: power_divide)
  also have "θ01((ω1 + ω2) / 2) = θ00(τ/2 + 1 ; τ)"
    by (simp add: theta_01_conv_00 theta_00_def add_divide_distrib ratio_def mult_ac add_ac)
  also have "… = θ00(τ/2 ; τ)"
    by (subst jacobi_theta_00_left.plus_1) auto
  also have "… = θ10(0) * to_nome (-τ/4)"
    by (simp add: theta_10_conv_00 theta_00_def ratio_def mult_ac to_nome_minus)
  also have "θ11((ω1 + ω2) / 2) = -θ00(0 + τ + 1 ; τ) * to_nome (3/4*τ)"
    by (simp add: theta_11_conv_00 theta_00_def add_divide_distrib ratio_def mult_ac add_ac to_nome_add) 
  also have "… = -θ00(0) * to_nome (3/4*τ - τ)"
    unfolding jacobi_theta_00_left.plus_1 jacobi_theta_00_plus_quasiperiod to_nome_diff theta_00_def
    by simp
  also have "θ10(0) * to_nome (-τ/4) / … = -θ10(0) / θ00(0) * to_nome (-τ/4 - 3/4 * τ + τ)"
    unfolding to_nome_diff to_nome_add by (simp add: field_simps)
  also have "… ^ 2 = θ10(0) ^ 2 / θ00(0) ^ 2"
    by (simp add: power_divide)
  also have "(of_real pi * θ10(0) * θ00(0) / ω1)2 * (θ10(0)2 / θ00(0)2) = (pi / ω1) ^ 2 * θ10(0) ^ 4"
    by (simp add: field_simps rel_def uminus_in_lattice_iff to_nome_minus theta_00_eq_0_iff)
  finally show e32: "𝖾3 - 𝖾2 = (pi / ω1) ^ 2 * θ10(0) ^ 4" .

  have "(𝖾1 - 𝖾2) - (𝖾3 - 𝖾2) = (pi / ω1) ^ 2 * (θ00(0) ^ 4 - θ10(0) ^ 4)"
    unfolding e32 e12 by (simp add: field_simps)
  also have "θ00(0) ^ 4 - θ10(0) ^ 4 = θ01(0) ^ 4"
    using jacobi_theta_xy_0_pow4_complex[of τ] Im_ratio_pos
    by (simp add: theta_00_def theta_01_def theta_10_def algebra_simps)
  finally show e13: "𝖾1 - 𝖾3 = (pi / ω1) ^ 2 * θ01(0) ^ 4"
    by simp

  have e3_eq: "𝖾3 = -(𝖾1 + 𝖾2)"
    using sum_e123_0 by (Groebner_Basis.algebra)
  have "𝖾1 = ((𝖾1 - 𝖾2) + (𝖾1 - 𝖾3)) / 3"
    by (simp add: algebra_simps e3_eq)
  also have "… = (pi / ω1) ^ 2 / 3 * (θ00(0) ^ 4 + θ01(0) ^ 4)"
    unfolding e12 e13 by (simp add: algebra_simps add_divide_distrib)
  finally show e1: "𝖾1 = (pi / ω1) ^ 2 / 3 * (θ00(0) ^ 4 + θ01(0) ^ 4)" .

  have e2_eq: "𝖾2 = -(𝖾1 + 𝖾3)"
    using sum_e123_0 by (Groebner_Basis.algebra)
  have "𝖾3 = ((𝖾1 - 𝖾2) - 2 * (𝖾1 - 𝖾3)) / 3"
    by (simp add: algebra_simps e2_eq)
  also have "… = (pi / ω1) ^ 2 / 3 * (θ00(0) ^ 4 - 2 * θ01(0) ^ 4)"
    unfolding e12 e13 by (simp add: algebra_simps diff_divide_distrib)
  also have "θ00(0) ^ 4 - 2 * θ01(0) ^ 4 = θ10(0) ^ 4 - θ01(0) ^ 4"
    using jacobi_theta_xy_0_pow4_complex[of τ, symmetric] Im_ratio_pos
    by (simp add: theta_00_def theta_01_def theta_10_def)
  finally show e3: "𝖾3 = (pi / ω1)2 / 3 * (θ10(0) ^ 4 - θ01(0) ^ 4)" .

  show e2: "𝖾2 = -(pi / ω1)2 / 3 * (θ00(0) ^ 4 + θ10(0) ^ 4)"
    unfolding e2_eq e1 e3 by (simp add: field_simps)

  have "modulus = (𝖾3 - 𝖾2) / (𝖾1 - 𝖾2)"
    by (simp add: modulus_def)
  also have "… = θ10(0) ^ 4 / θ00(0) ^ 4"
    unfolding e32 e12 by simp
  finally show "modulus = θ10(0) ^ 4 / θ00(0) ^ 4" .
qed

text ‹
  Using this, we also obtain an expression of $\wp$ purely in terms of theta functions.
  This immediately shows that $\wp(z, \tau)$ (which we have not defined yet) is holomorphic in 
  both $z$ and $\tau$.
›
lemma weierstrass_fun_conv_theta':
  assumes "z ∉ Λ"
  shows   "℘ z = (pi / ω1)2 * (-1/3 * (θ00(0)^4 + θ10(0)^4) + (θ10(0) * θ00(0))2 * θ01(z)2 / θ11(z)2)"
  by (subst weierstrass_fun_conv_theta[OF assms], subst e2_conv_theta)
     (simp_all add: field_simps)

end


context std_complex_lattice
begin

sublocale complex_lattice_Im_pos 1 τ
  rewrites "ratio = τ"
  by unfold_locales (auto simp: ratio_def Im_τ_pos)

end

unbundle no jacobi_theta_nw_notation

end