Theory Theta_Nullwert

section ‹The theta nullwert functions›
theory Theta_Nullwert
  imports "Sum_Of_Squares_Count.Sum_Of_Squares_Count" Jacobi_Triple_Product
begin

text ‹
  The theta nullwert function (nullwert being German for ``zero value'') are the 
  four functions $\vartheta_{xy}(z; \tau)$ with $z = 0$. However, they are very commonly
  denoted in terms of the nome instead, corresponding to $\vartheta_{xy}(w, q)$ with $w = 1$.

  It is easy to see that $\vartheta_{11}(0; \tau) = \vartheta_{11}(1, q)$ is identically zero 
  and therefore uninteresting. The remaining three functions $\vartheta_{10}(0, q)$,
  $\vartheta_{00}(0, q)$, and $\vartheta_{01}(0, q)$ are denoted $\vartheta_2(q)$, 
  $\vartheta_3(q)$, and $\vartheta_4(q)$.

  It is also not hard to see that in fact $\vartheta_4(q) = \vartheta_3(-q)$, but we still
  introduce separate notation for $\vartheta_4$ since it is very commonly used in the literature.
›

lemma jacobi_theta_nome_11_1_left [simp]: "jacobi_theta_nome_11 1 q = 0"
  using jacobi_theta_nome_minus_same[of q] by (auto simp: jacobi_theta_nome_11_def)

abbreviation jacobi_theta_nw_10 :: "'a :: {real_normed_field, banach, ln} ⇒ 'a" where
  "jacobi_theta_nw_10 q ≡ jacobi_theta_nome_10 1 q"

abbreviation jacobi_theta_nw_00 :: "'a :: {real_normed_field, banach} ⇒ 'a" where
  "jacobi_theta_nw_00 q ≡ jacobi_theta_nome_00 1 q"

abbreviation jacobi_theta_nw_01 :: "'a :: {real_normed_field, banach} ⇒ 'a" where
  "jacobi_theta_nw_01 q ≡ jacobi_theta_nome_01 1 q"


bundle jacobi_theta_nw_notation
begin
notation jacobi_theta_nw_10 ("θ2")
notation jacobi_theta_nw_00 ("θ3")
notation jacobi_theta_nw_01 ("θ4")
end

bundle no_jacobi_theta_nw_notation
begin
no_notation jacobi_theta_nw_10 ("θ2")
no_notation jacobi_theta_nw_00 ("θ3")
no_notation jacobi_theta_nw_01 ("θ4")
end

unbundle jacobi_theta_nw_notation


lemma jacobi_theta_nw_10_0 [simp]: "θ2 0 = 0"
  and jacobi_theta_nw_00_0 [simp]: "θ3 0 = 1"
  and jacobi_theta_nw_01_0 [simp]: "θ4 0 = 1"
  by simp_all

lemma jacobi_theta_nw_01_conv_00: "θ4 q = θ3 (-q)"
  by (simp add: jacobi_theta_nome_01_conv_00)


lemma jacobi_theta_nw_10_of_real:
        "y ≥ 0 ⟹ θ2 (complex_of_real y) = of_real (θ2 y)"
  and jacobi_theta_nw_00_of_real: "θ3 (of_real x) = of_real (θ3 x)"
  and jacobi_theta_nw_01_of_real: "θ4 (of_real x) = of_real (θ4 x)"
  by (simp_all flip: jacobi_theta_nome_10_complex_of_real jacobi_theta_nome_00_of_real
                     jacobi_theta_nome_01_of_real)

lemma jacobi_theta_nw_10_cnj:
        "(Im q = 0 ⟹ Re q ≥ 0) ⟹ θ2 (cnj q) = cnj (θ2 q)"
  and jacobi_theta_nw_00_cnj: "θ3 (cnj q) = cnj (θ3 q)"
  and jacobi_theta_nw_01_cnj: "θ4 (cnj q) = cnj (θ4 q)"
  by (simp_all flip: jacobi_theta_nome_10_cnj jacobi_theta_nome_00_cnj jacobi_theta_nome_01_cnj)


text ‹
  The nullwerte have the following definitions as infinite sums:
  \begin{align*}
    \vartheta_2(q) &= \sum\limits_{-\infty}^\infty q^{(n+\frac{1}{2})^2}\\
    \vartheta_3(q) &= \sum\limits_{-\infty}^\infty q^{n^2}\\
    \vartheta_4(q) &= \sum\limits_{-\infty}^\infty (-1)^n q^{n^2}
  \end{align*}
›

lemma has_sum_jacobi_theta_nw_10_complex:
  assumes "norm (q :: complex) < 1"
  shows   "((λn. q powr ((of_int n + 1 / 2) ^ 2)) has_sum θ2 q) UNIV"
proof (cases "q = 0")
  case [simp]: False
  show ?thesis
    using has_sum_jacobi_theta_nome_10[of q 1] assms by simp
qed auto

lemma has_sum_jacobi_theta_nw_10_real:
  assumes "q ∈ {0<..<1::real}"
  shows   "((λn. q powr ((of_int n + 1 / 2) ^ 2)) has_sum θ2 q) UNIV"
proof (cases "q = 0")
  case [simp]: False
  show ?thesis
    using has_sum_jacobi_theta_nome_10[of q 1] assms by simp
qed auto

lemma has_sum_jacobi_theta_nw_00:
  assumes "norm q < 1"
  shows   "((λn. q powi (n ^ 2)) has_sum θ3 q) UNIV"
  using has_sum_jacobi_theta_nome_00[of q 1] assms by simp

lemma has_sum_jacobi_theta_nw_01:
  assumes "norm q < 1"
  shows   "((λn. (-1) powi n * q powi (n ^ 2)) has_sum θ4 q) UNIV"
  using has_sum_jacobi_theta_nome_01[of q 1] assms by simp

text ‹
  The theta nullwert functions do not vanish (except for ‹θ2(0) = 0›).
›
lemma jacobi_theta_00_nw_nonzero_complex: "norm (q::complex) < 1 ⟹ θ3 q ≠ 0"
  by (simp add: jacobi_theta_nome_00_def jacobi_theta_nome_1_left_nonzero_complex)

lemma jacobi_theta_01_nw_nonzero_complex: "norm (q::complex) < 1 ⟹ θ4 q ≠ 0"
  by (simp add: jacobi_theta_nw_01_conv_00 jacobi_theta_00_nw_nonzero_complex)

lemma jacobi_theta_10_nw_nonzero_complex:
  assumes "q ≠ 0" "norm (q::complex) < 1"
  shows   "θ2 q ≠ 0"
  using jacobi_theta_nome_q_q_nonzero_complex[of q] assms
  by (auto simp: jacobi_theta_nome_10_def)

lemma jacobi_theta_00_nw_nonzero_real: "¦q::real¦ < 1 ⟹ θ3 q ≠ 0"
  and jacobi_theta_01_nw_nonzero_real: "¦q::real¦ < 1 ⟹ θ4 q ≠ 0"
  and jacobi_theta_10_nw_nonzero_real: "q ∈ {0..<1} ⟹ q ≠ 0 ⟹ θ2 q ≠ 0"
  using jacobi_theta_00_nw_nonzero_complex[of "of_real q"]
        jacobi_theta_01_nw_nonzero_complex[of "of_real q"]
        jacobi_theta_10_nw_nonzero_complex[of "of_real q"]
  by (simp_all add: jacobi_theta_nw_00_of_real jacobi_theta_nw_01_of_real
                    jacobi_theta_nw_10_of_real)


subsection ‹The Maclaurin series of $\vartheta_3$ and $\vartheta_4$›

text ‹
  It is easy to see from the above infinite sums that $\vartheta_3(q)$ and $\vartheta_4(q)$ have the 
  Maclaurin series
  \[1 + 2\sum_{n=1}^\infty [\exists i.\ n = i^2] c^n q^n\]
  for $c = 1$ and $c = -1$, respectively.

  In other words, $\vartheta_3(q)$ is the generating function of the number $r_1(n)$ of ways to write 
  an integer $n$ as a square of an integer -- 1 for $n = 0$, 2 if $n$ is a non-zero perfect square,
  and $0$ otherwise.

  Consequently, $\vartheta_3(q)^k$ is the generating function of the number $r_k(n)$ of ways to write
  an integer $n$ as a square of $k$ integers. The function $r_k(n)$ is written as 
  const‹count_sos› ‹k› ‹n› in Isabelle.
›
definition fps_jacobi_theta_nw :: "'a :: field ⇒ 'a fps" where
  "fps_jacobi_theta_nw c = Abs_fps (λn. if n = 0 then 1 else if is_square n then 2 * c ^ n else 0)"

theorem fps_jacobi_theta_power_eq:
  "fps_jacobi_theta_nw c ^ k = Abs_fps (λn. of_nat (count_sos k n) * c ^ n)"
proof (induction k)
  case (Suc k)
  have "fps_jacobi_theta_nw (c::'a) ^ Suc k =
          fps_jacobi_theta_nw c * Abs_fps (λn. of_nat (count_sos k n) * c ^ n)"
    by (simp add: Suc.IH mult.commute)
  also have "… = Abs_fps (λn. of_nat (count_sos (Suc k) n) * c ^ n)" (is "?lhs = ?rhs")
  proof (rule fps_ext)
    fix n :: nat
    have "fps_nth (fps_jacobi_theta_nw (c::'a) * Abs_fps (λn. of_nat (count_sos k n) * c ^ n)) n =
            (∑i=0..n. fps_nth (fps_jacobi_theta_nw c) i * of_nat (count_sos k (n - i)) * c ^ (n - i))"
      by (simp add: fps_mult_nth sum_distrib_left sum_distrib_right algebra_simps)
    also have "… = of_nat (count_sos k n) * c ^ n + 
                   (∑i∈{0<..n}. fps_nth (fps_jacobi_theta_nw c) i * 
                                 of_nat (count_sos k (n - i)) * c ^ (n - i))"
      (is "_ = _ + ?S")
      by (subst sum.head) (auto simp: fps_jacobi_theta_nw_def)
    also have "?S =  (∑i | i ∈ {0<..n} ∧ is_square i. 
                       2 * of_nat (count_sos k (n - i)) * c ^ n)"
      by (rule sum.mono_neutral_cong_right) (auto simp: fps_jacobi_theta_nw_def simp flip: power_add)
    also have "… = (∑i ∈ {1..Discrete.sqrt n}. 
                       2 * of_nat (count_sos k (n - i ^ 2)) * c ^ n)"
      by (intro sum.reindex_bij_witness[of _ "λi. i ^ 2" Discrete.sqrt])
         (auto elim!: is_nth_powerE simp: Discrete.le_sqrt_iff)
    also have "of_nat (count_sos k n) * c ^ n + … = of_nat (count_sos (Suc k) n) * c ^ n"
      by (simp add: count_sos_Suc sum_distrib_left sum_distrib_right power_add algebra_simps)
    finally show "fps_nth ?lhs n = fps_nth ?rhs n"
      by simp
  qed
  finally show ?case .
qed (auto intro!: fps_ext)

corollary fps_jacobi_theta_altdef:
  "fps_jacobi_theta_nw c = Abs_fps (λn. of_nat (count_sos 1 n) * c ^ n)"
  using fps_jacobi_theta_power_eq[of c 1] by simp

lemma norm_summable_fps_jacobi_theta:
  fixes q :: "'a :: {real_normed_field, banach}"
  assumes "norm (c * q) < 1"
  shows   "summable (λn. norm (fps_nth (fps_jacobi_theta_nw c) n * q ^ n))"
proof (rule summable_comparison_test)
  show "summable (λn. 2 * norm (c * q) ^ n)"
    by (intro summable_mult summable_geometric) (use assms in auto)
  show "∃N. ∀n≥N. norm (norm (fps_nth (fps_jacobi_theta_nw c) n * q ^ n)) ≤ 2 * norm (c * q) ^ n"
    by (rule exI[of _ 0]) (auto simp: fps_jacobi_theta_nw_def norm_mult norm_power power_mult_distrib)
qed

lemma summable_fps_jacobi_theta:
  fixes q :: "'a :: {real_normed_field, banach}"
  assumes "norm (c * q) < 1"
  shows   "summable (λn. fps_nth (fps_jacobi_theta_nw c) n * q ^ n)"
  using norm_summable_fps_jacobi_theta[OF assms] by (rule summable_norm_cancel)

lemma summable_ints_symmetric:
  fixes f :: "int ⇒ 'a :: {real_normed_vector, banach}"
  assumes "summable (λn. norm (f (int n)))"
  assumes "⋀n. f (-n) = f n"
  shows   "f abs_summable_on UNIV" and "summable (λn. norm ((if n = 0 then 1 else 2) *R f (int n)))"
proof -
  show "summable (λn. norm ((if n = 0 then 1 else 2) *R f (int n)))"
  proof (rule summable_comparison_test)
    show "summable (λn. 2 * norm (f n))"
      by (intro summable_mult assms)
  qed (auto intro!: exI[of _ 0])
next
  have "(λn. f (int n)) abs_summable_on UNIV"
    using assms by (subst summable_on_UNIV_nonneg_real_iff) auto
  also have "?this ⟷ f abs_summable_on {0..}"
    by (rule summable_on_reindex_bij_witness[of _ nat int]) auto
  finally have 1: "f abs_summable_on {0<..}"
    by (rule summable_on_subset) auto
  also have "?this ⟷ f abs_summable_on {..<0}"
    by (rule summable_on_reindex_bij_witness[of _ uminus uminus]) (use assms(2) in auto)
  finally have "f abs_summable_on ({..<0} ∪ {0} ∪ {0<..})"
    by (intro summable_on_Un_disjoint 1) auto
  also have "({..<(0::int)} ∪ {0} ∪ {0<..}) = UNIV"
    by auto
  finally show "f abs_summable_on UNIV" .
qed

lemma has_sum_ints_symmetric_iff:
  fixes f :: "int ⇒ 'a :: {banach, real_normed_vector}"
  assumes "⋀n. f (-n) = f n"
  shows   "(f has_sum S) UNIV ⟷ ((λn. (if n = 0 then 1 else 2) *R f (int n)) has_sum S) UNIV"
proof
  assume *: "((λn. (if n = 0 then 1 else 2) *R f (int n)) has_sum S) UNIV"
  have "((λn. (if n = 0 then 1 else 2) *R f (int n)) has_sum (S - f 0)) (UNIV - {0})"
    using has_sum_Diff[OF * has_sum_finite[of "{0}"]] by simp
  also have "?this ⟷ ((λn. (if n = 0 then 1 else 2) *R f n) has_sum (S - f 0)) {0<..}"
    by (intro has_sum_reindex_bij_witness[of _ nat int]) auto
  finally have "((λn. (if n = 0 then 1 else 2) *R f n) has_sum S - f 0) {0<..}" .
  also have "?this ⟷ ((λn. 2 *R f n) has_sum (S - f 0)) {0<..}"
    by (intro has_sum_cong) auto
  also have "… ⟷ (f has_sum (S - f 0) /R 2) {0<..}"
    by (rule has_sum_scaleR_iff) auto
  finally have 1: "(f has_sum (S - f 0) /R 2) {0<..}" .

  have "(f has_sum (S - f 0) /R 2) {0<..} ⟷ (f has_sum (S - f 0) /R 2) {..<0}"
    by (intro has_sum_reindex_bij_witness[of _ uminus uminus]) (use assms in auto)
  with 1 have 2: "(f has_sum (S - f 0) /R 2) {..<0}"
    by simp

  have "(f has_sum ((S - f 0) /R 2 + (S - f 0) /R 2 + f 0)) ({..<0} ∪ {0<..} ∪ {0})"
    by (intro has_sum_Un_disjoint 1 2) (auto simp: has_sum_finite_iff)
  also have "{..<0} ∪ {0<..} ∪ {0::int} = UNIV"
    by auto
  also have "(S - f 0) /R 2 + (S - f 0) /R 2 + f 0 = S"
    by (simp flip: mult_2 scaleR_2)
  finally show "(f has_sum S) UNIV" .
next
  assume *: "(f has_sum S) UNIV"
  define S' where "S' = (∑∞n∈{0<..}. f n)"
  have "f summable_on {0<..}"
    by (rule summable_on_subset_banach[of _ UNIV]) (use * in ‹auto dest: has_sum_imp_summable›)
  hence 1: "(f has_sum S') {0<..}"
    unfolding S'_def by (rule has_sum_infsum)
  
  have "(f has_sum S') {0<..} ⟷ (f has_sum S') {..<0}"
    by (rule has_sum_reindex_bij_witness[of _ uminus uminus]) (use assms in auto)
  with 1 have 2: "(f has_sum S') {..<0}"
    by simp

  have "(f has_sum (S' + S' + f 0)) ({..<0} ∪ {0<..} ∪ {0})"
    by (intro has_sum_Un_disjoint 1 2) (auto simp: has_sum_finite_iff)
  also have "({..<0} ∪ {0<..} ∪ {0::int}) = UNIV"
    by auto
  also have "S' + S' + f 0 = 2 *R S' + f 0"
    by (simp add: algebra_simps flip: scaleR_2)
  finally have 3: "S = 2 *R S' + f 0"
    using * has_sum_unique by blast

  have "((λn. 2 *R f n) has_sum (2 *R S')) {0<..}"
    by (intro has_sum_scaleR 1)
  also have "?this ⟷ ((λn. (if n = 0 then 1 else 2) *R f n) has_sum (2 *R S')) {0<..}"
    by (intro has_sum_cong) auto
  finally have "((λn. (if n = 0 then 1 else 2) *R f n) has_sum (f 0 + 2 *R S')) ({0} ∪ {0<..})"
    by (intro has_sum_Un_disjoint) (auto simp: has_sum_finite_iff)
  also have "?this ⟷ ((λn. (if n = 0 then 1 else 2) *R f (int n)) has_sum (f 0 + 2 *R S')) UNIV"
    by (rule has_sum_reindex_bij_witness[of _ int nat]) auto
  finally show "((λn. (if n = 0 then 1 else 2) *R f (int n)) has_sum S) UNIV"
    using 3 by (simp add: add.commute)
qed

lemma sums_jacobi_theta_nw_00:
  assumes "norm q < 1"
  shows   "(λn. fps_nth (fps_jacobi_theta_nw 1) n * q ^ n) sums θ3 q"
proof -
  define S where "S = (∑n. if is_square n ∧ n > 0 then q ^ n else 0)"
  have "((λn. (if n = 0 then 1 else 2) *R q powi (int n ^ 2)) has_sum (θ3 q)) UNIV"
  proof (subst has_sum_ints_symmetric_iff [symmetric])
    show "((λn. q powi n2) has_sum θ3 q) UNIV"
      by (rule has_sum_jacobi_theta_nw_00) fact
  qed auto
  also have "?this ⟷ ((λn. fps_nth (fps_jacobi_theta_nw 1) n * q ^ n) has_sum
                          θ3 q) {n. is_square n}"
    by (rule has_sum_reindex_bij_witness[of _ Discrete.sqrt "λi. i ^ 2"])
       (auto simp: fps_jacobi_theta_nw_def power_int_def scaleR_conv_of_real nat_power_eq
             elim!: is_nth_powerE)
  also have "… ⟷ ((λn. fps_nth (fps_jacobi_theta_nw 1) n * q ^ n) has_sum
                          θ3 q) UNIV"
    by (intro has_sum_cong_neutral) (auto simp: fps_jacobi_theta_nw_def intro: Nat.gr0I)
  finally show ?thesis
    by (rule has_sum_imp_sums)
qed

lemma sums_jacobi_theta_nw_01:
  assumes "norm q < 1"
  shows   "(λn. fps_nth (fps_jacobi_theta_nw (-1)) n * q ^ n) sums θ4 q"
proof -
  have "(λn. fps_nth (fps_jacobi_theta_nw 1) n * (-q) ^ n) sums θ3 (-q)"
    by (rule sums_jacobi_theta_nw_00) (use assms in auto)
  also have "(λn. fps_nth (fps_jacobi_theta_nw 1) n * (-q) ^ n) =
             (λn. fps_nth (fps_jacobi_theta_nw (-1)) n * q ^ n)"
    by (auto simp: fun_eq_iff fps_jacobi_theta_nw_def power_minus')
  also have "θ3 (-q) = θ4 q"
    by (simp add: jacobi_theta_nw_01_conv_00)
  finally show ?thesis .
qed

lemma has_fps_expansion_jacobi_theta_3 [fps_expansion_intros]:
  "θ3 has_fps_expansion fps_jacobi_theta_nw 1"
proof (rule has_fps_expansionI)
  have "eventually (λq. q ∈ ball 0 1) (nhds (0 :: 'a))"
    by (rule eventually_nhds_in_open) auto
  thus "eventually (λq. (λn. fps_nth (fps_jacobi_theta_nw 1) n * q ^ n :: 'a) sums θ3 q) (nhds 0)"
    by eventually_elim (rule sums_jacobi_theta_nw_00, auto)
qed

lemma has_fps_expansion_jacobi_theta_4 [fps_expansion_intros]:
  "θ4 has_fps_expansion fps_jacobi_theta_nw (-1)"
proof (rule has_fps_expansionI)
  have "eventually (λq. q ∈ ball 0 1) (nhds (0 :: 'a))"
    by (rule eventually_nhds_in_open) auto
  thus "eventually (λq. (λn. fps_nth (fps_jacobi_theta_nw (-1)) n * q ^ n :: 'a) sums θ4 q) (nhds 0)"
    by eventually_elim (rule sums_jacobi_theta_nw_01, auto)
qed

lemma fps_conv_radius_jacobi_theta_nw [simp]:
  fixes c :: "'a :: {banach, real_normed_field}"
  shows "fps_conv_radius (fps_jacobi_theta_nw c) = 1 / ereal (norm c)"
proof -
  have "fps_conv_radius (fps_jacobi_theta_nw c) = 
          inverse (limsup (λn. ereal (root n (norm (fps_nth (fps_jacobi_theta_nw c) n)))))"
    by (simp add: fps_conv_radius_def conv_radius_def)
  also have "limsup (λn. ereal (root n (norm (fps_nth (fps_jacobi_theta_nw c) n)))) = norm c"
    (is "?lhs = _")
  proof (rule antisym)
    have "?lhs ≤ limsup (λn. root n 2 * norm c)"
      by (intro Limsup_mono always_eventually)
         (auto simp: fps_jacobi_theta_nw_def norm_power real_root_mult real_root_power)
    also have "(λn. ereal (root n 2 * norm c)) ⇢ ereal (1 * norm c)"
      by (intro tendsto_intros LIMSEQ_root_const) auto
    hence "limsup (λn. root n 2 * norm c) = ereal (1 * norm c)" 
      by (intro lim_imp_Limsup) auto
    finally show "?lhs ≤ norm c"
      by simp
  next
    have "limsup ((λn. ereal (root n (norm (fps_nth (fps_jacobi_theta_nw c) n)))) ∘ (λn. n ^ 2)) ≤ ?lhs"
      by (rule limsup_subseq_mono) (auto intro!: strict_monoI power_strict_mono)
    also have "limsup ((λn. ereal (root n (norm (fps_nth (fps_jacobi_theta_nw c) n)))) ∘ (λn. n ^ 2)) =
               limsup ((λn. ereal (root (n^2) 2 * norm c)))"
      by (rule Limsup_eq, rule eventually_mono[OF eventually_gt_at_top[of 0]])
         (auto simp: o_def fps_jacobi_theta_nw_def norm_power real_root_mult real_root_power)
    also have "(λn. ereal (root (n^2) 2 * norm c)) ⇢ ereal (1 * norm c)"
      by (intro tendsto_intros filterlim_compose[OF LIMSEQ_root_const]
                filterlim_subseq[of "λn. n ^ 2"] strict_monoI power_strict_mono) auto
    hence "limsup (λn. ereal (root (n^2) 2 * norm c)) = ereal (1 * norm c)"
      by (intro lim_imp_Limsup) auto
    finally show "norm c ≤ ?lhs"
      by simp
  qed
  finally show ?thesis
    by (simp add: divide_ereal_def)
qed


text ‹
  Recall that $\vartheta_2(q) = q^{1/4} \vartheta(q, q)$. Since the factor $q^{1/4}$ has a branch cut,
  it is somewhat unpleasant to deal with and we will concentrate only on the factor $\vartheta(q,q)$
  for now. This is a holomorphic function on the unit disc except for a removable singularity
  at $q = 0$.

  For $q\neq 0$ and $|q|<1$, $\vartheta(q,q)$ has following the power series expansion:
  \[ \vartheta(q,q) = \sum_{n=-\infty}^{\infty} q^{n(n+1)} = \sum_{n=0}^{\infty} 2 q^{n(n+1)} \]
  Note that $n(n+1)$ is twice the triangular number $n(n+1)/2$, so we can also see this as a
  series expansion in terms of powers of $q^2$.
›
lemma has_sum_jacobi_theta_nw_10_aux:
  assumes q: "norm q < 1" "q ≠ 0"
  shows   "((λn. 2 * q ^ (n*(n+1))) has_sum jacobi_theta_nome q q) UNIV"
proof -
  define S where "S = jacobi_theta_nome q q"
  have 1: "((λn. q powi (n*(n+1))) has_sum S) UNIV"
    using has_sum_jacobi_theta_nome[of q q]
    using q by (simp add: algebra_simps power2_eq_square power_int_add S_def)
  have summable: "(λn. q powi (n * (n + 1))) summable_on I" for I
    by (rule summable_on_subset_banach, rule has_sum_imp_summable[OF 1]) auto

  define S1 where "S1 = (∑∞n∈{0..}. q powi (n*(n+1)))"
  have S1: "((λn. q powi (n*(n+1))) has_sum S1) {0..}"
    unfolding S1_def by (rule has_sum_infsum[OF summable])
  have "((λn. q powi (n*(n+1))) has_sum S1) {0..} ⟷
        ((λn. q powi (n*(n+1))) has_sum S1) {..<0}"
    by (intro has_sum_reindex_bij_witness[of _ "λn. -n-1" "λn. -n-1"])
       (auto simp: algebra_simps)
  with S1 have S1': "((λn. q powi (n*(n+1))) has_sum S1) {..<0}"
    by simp
  have "((λn. q powi (n*(n+1))) has_sum (S1 + S1)) ({..<0} ∪ {0..})"
    by (intro has_sum_Un_disjoint S1 S1') auto
  also have "{..<(0::int)} ∪ {0..} = UNIV"
    by auto
  finally have 2: "((λn. q powi (n*(n+1))) has_sum (2 * S1)) UNIV"
    by simp
  
  from this and 1 have 3: "2 * S1 = S"
    using has_sum_unique by blast

  have "((λn. q powi (n*(n+1))) has_sum S1) {0..} ⟷ ((λn. q ^ (n*(n+1))) has_sum S1) UNIV"
    by (rule has_sum_reindex_bij_witness[of _ int nat]) 
       (auto simp: power_int_def algebra_simps power_add nat_add_distrib nat_mult_distrib)
  with S1 show "((λn. 2 * q ^ (n*(n+1))) has_sum S) UNIV"
    unfolding 3 [symmetric] by (intro has_sum_cmult_right) auto
qed

lemma sums_jacobi_theta_nw_10_aux:
  assumes q: "norm q < 1" "q ≠ 0"
  shows   "(λn. if ∃i. n = i*(i+1) then 2 * q ^ n else 0) sums jacobi_theta_nome q q"
proof -
  have inj: "inj (λi::nat. i * (i + 1))"
    by (rule strict_mono_imp_inj_on) (auto simp: strict_mono_Suc_iff)
  have "((λn. 2 * q ^ (n*(n+1))) has_sum jacobi_theta_nome q q) UNIV"
    by (rule has_sum_jacobi_theta_nw_10_aux) fact+
  also have "?this ⟷ ((λn. 2 * q ^ n) has_sum jacobi_theta_nome q q) (range (λi. i*(i+1)))"
    by (subst has_sum_reindex[OF inj]) (auto simp: o_def)
  also have "… ⟷ ((λn. if ∃i. n = i*(i+1) then 2 * q ^ n else 0) has_sum jacobi_theta_nome q q) UNIV"
    by (rule has_sum_cong_neutral) auto
  finally show ?thesis
    by (rule has_sum_imp_sums)
qed

definition fps_jacobi_theta_nw_10 :: "'a :: field fps" where
  "fps_jacobi_theta_nw_10 = Abs_fps (λn. if ∃i. n = i*(i+1) then 2 else 0)"

lemma fps_conv_radius_jacobi_theta_2 [simp]: "fps_conv_radius fps_jacobi_theta_nw_10 = 1"
proof -
  have "fps_conv_radius (fps_jacobi_theta_nw_10 :: 'a fps) =
          inverse (limsup (λn. ereal (root n (norm (fps_nth fps_jacobi_theta_nw_10 n :: 'a)))))"
    unfolding fps_conv_radius_def conv_radius_def ..
  also have "limsup (λn. ereal (root n (norm (fps_nth fps_jacobi_theta_nw_10 n :: 'a)))) = 1"
    (is "?lhs = _")
  proof (rule antisym)
    have "?lhs ≤ limsup (λn. root n 2)"
      by (intro Limsup_mono always_eventually)
         (auto simp: fps_jacobi_theta_nw_10_def norm_power real_root_ge_zero)
    also have "(λn. ereal (root n 2)) ⇢ ereal 1"
      by (intro tendsto_intros LIMSEQ_root_const) auto
    hence "limsup (λn. root n 2) = ereal 1" 
      by (intro lim_imp_Limsup) auto
    finally show "?lhs ≤ 1"
      by (simp add: one_ereal_def)
  next
    define h where "h = (λn::nat. n * (n + 1))"
    have h: "strict_mono h"
      by (rule strict_monoI_Suc) (auto simp: algebra_simps h_def)
    have "limsup ((λn. ereal (root n (norm (fps_nth fps_jacobi_theta_nw_10 n :: 'a)))) ∘ h) ≤ ?lhs"
      using h by (rule limsup_subseq_mono)
    also have "limsup ((λn. ereal (root n (norm (fps_nth fps_jacobi_theta_nw_10 n :: 'a)))) ∘ h) =
               limsup ((λn. ereal (root (h n) 2)))"
      by (rule Limsup_eq, rule eventually_mono[OF eventually_gt_at_top[of 0]])
         (auto simp: o_def fps_jacobi_theta_nw_10_def h_def algebra_simps)
    also have "(λn. ereal (root (h n) 2)) ⇢ ereal 1"
      by (intro tendsto_intros filterlim_compose[OF LIMSEQ_root_const]
                filterlim_subseq[of h] h) auto
    hence "limsup (λn. ereal (root (h n) 2)) = ereal 1"
      by (intro lim_imp_Limsup) auto
    finally show "1 ≤ ?lhs"
      by (simp add: one_ereal_def)
  qed
  finally show ?thesis
    by simp
qed

lemma has_laurent_expansion_jacobi_theta_2 [laurent_expansion_intros]:
  "(λq. jacobi_theta_nome q q) has_laurent_expansion fps_to_fls fps_jacobi_theta_nw_10"
  unfolding has_laurent_expansion_def
proof safe
  show "fls_conv_radius (fps_to_fls fps_jacobi_theta_nw_10 :: complex fls) > 0"
    unfolding fls_conv_radius_fps_to_fls by simp
next
  have "eventually (λq. q ∈ ball 0 1 - {0}) (at (0 :: complex))"
    by (rule eventually_at_in_open) auto
  thus "eventually (λq. eval_fls (fps_to_fls fps_jacobi_theta_nw_10) q = 
         jacobi_theta_nome q q) (at (0::complex))"
  proof eventually_elim
    case q: (elim q)
    have "eval_fls (fps_to_fls fps_jacobi_theta_nw_10) q = eval_fps fps_jacobi_theta_nw_10 q"
      by (subst eval_fps_to_fls) (use q in auto)
    also have "eval_fps fps_jacobi_theta_nw_10 q = (∑n. fps_nth fps_jacobi_theta_nw_10 n * q ^ n)"
      by (simp add: eval_fps_def)
    also have "(λn. fps_nth fps_jacobi_theta_nw_10 n * q ^ n) = 
               (λn. if ∃i. n = i*(i+1) then 2 * q ^ n else 0)"
      by (auto simp: fun_eq_iff fps_jacobi_theta_nw_10_def)
    also have "(∑n. … n) = jacobi_theta_nome q q"
      using sums_jacobi_theta_nw_10_aux[of q] q by (simp add: sums_iff)
    finally show ?case .
  qed
qed

text ‹
  For $\vartheta(q,q)^2$, we can find the following expansion into a double sum:
  \[\vartheta(q,q)^2 = \sum_{n=-\infty}^\infty \sum_{n=-\infty}^\infty q^{i(i+1) + j(j+1)}\]
›
lemma has_sum_jacobi_theta_nw_10_aux_square:
  fixes q :: complex
  assumes q: "norm q < 1" "q ≠ 0"
  shows "((λ(i,j). q powi (i*(i+1) + j*(j+1))) has_sum jacobi_theta_nome q q ^ 2) UNIV"
proof -
  define S where "S = jacobi_theta_nome q q"
  have 1: "((λn. q powi (n*(n+1))) has_sum S) UNIV"
    using has_sum_jacobi_theta_nome[of q q]
    using q by (simp add: algebra_simps power2_eq_square power_int_add S_def)
  have summable: "(λn. q powi (n * (n + 1))) summable_on I" for I
    by (rule summable_on_subset_banach, rule has_sum_imp_summable[OF 1]) auto

  define S' where "S' = jacobi_theta_nome (norm q) (norm q)"
  have 2: "((λn. norm q powi (n*(n+1))) has_sum S') UNIV"
    using has_sum_jacobi_theta_nome[of "norm q" "norm q"]
    using q by (simp add: algebra_simps power2_eq_square power_int_add S'_def)

  have "((λ(i,j). q powi (i*(i+1) + j*(j+1))) has_sum S2) (UNIV × UNIV)"
  proof (rule has_sum_SigmaI; (unfold prod.case)?)
    show "((λi. S * q powi (i*(i+1))) has_sum S^2) UNIV"
      unfolding power2_eq_square by (intro has_sum_cmult_right 1)
  next
    fix i :: int
    show "((λj. q powi (i * (i + 1) + j * (j + 1))) has_sum S * q powi (i * (i + 1))) UNIV"
      using has_sum_cmult_left[OF 1, of "q powi (i * (i + 1))"] q
      by (simp add: power_int_add mult_ac)
  next
    have "(λij. norm (case ij of (i,j) ⇒ q powi (i * (i + 1) + j * (j + 1)))) summable_on UNIV × UNIV"
    proof (rule summable_on_SigmaI; (unfold prod.case)?)
      show "(λj. S' * norm q powi (j * (j + 1))) summable_on UNIV"
        using has_sum_imp_summable[OF 2] by (intro summable_on_cmult_right)
    next
      fix i :: int
      show "((λj. norm (q powi (i*(i+1) + j*(j+1)))) has_sum (S' * norm q powi (i*(i+1)))) UNIV"
        using has_sum_cmult_left[OF 2, of "norm q powi (i*(i+1))"] q
        by (simp add: norm_power_int norm_mult power_int_add mult_ac)
    qed auto
    thus "(λ(i, j). q powi (i * (i + 1) + j * (j + 1))) summable_on UNIV × UNIV"
      by (rule abs_summable_summable)
  qed
  thus ?thesis
    by (simp add: S_def)
qed

text ‹
  With some creative reindexing, we find the following power series expansion:
  \[ q \vartheta(q^2, q^2)^2 = \sum_{n=0}^\infty r_2(2n+1) q^{2n+1} \]
›
lemma sums_q_times_jacobi_theta_nw_10_aux_square_square:
  fixes q :: complex
  assumes q: "q ≠ 0" "norm q < 1"
  shows "(λn. (if odd n then of_nat (count_sos 2 n) else 0) * q ^ n) sums
           (q * jacobi_theta_nome (q2) (q2) ^ 2)"
proof -
  define IJ where "IJ = (λn. {(i, j). i2 + j2 = int n})"
  have [simp, intro]: "finite (IJ n)" for n
    using bij_betw_finite[OF bij_betw_sos_decomps_2[of n]] by (simp add: IJ_def)

  have aux: "1 + x ≠ y" if "even x" "even y" for x y :: int
    using that by presburger

  define S where "S = q * jacobi_theta_nome (q2) (q2) ^ 2"
  have "((λ(i,j). (q^2) powi (i*(i+1) + j*(j+1))) has_sum jacobi_theta_nome (q2) (q2) ^ 2) UNIV"
    by (intro has_sum_jacobi_theta_nw_10_aux_square) 
       (use q in ‹auto simp: norm_power power_less_one_iff›)
  hence "((λ(i,j). q * (q^2) powi (i*(i+1) + j*(j+1))) has_sum S) (UNIV × UNIV)"
    unfolding S_def case_prod_unfold by (intro has_sum_cmult_right) auto
  also have "((λ(i,j). q * (q^2) powi (i*(i+1) + j*(j+1)))) =
             ((λ(i,j). q powi (1 + 2 * (i*(i+1) + j*(j+1)))))" using q
    by (auto simp: power_int_add power2_eq_square fun_eq_iff power_int_mult_distrib algebra_simps)
       (auto simp flip: power_int_add simp: algebra_simps)?
  also have "(… has_sum S) (UNIV × UNIV) ⟷
             ((λ(i,j). q powi (i ^ 2 + j ^ 2)) has_sum S) {(i,j). odd (i^2+j^2)}"
    by (rule has_sum_reindex_bij_witness[of _ 
             "λ(i,j). ((j+i-1) div 2, (j-i-1) div 2)" "λ(i,j). (i-j, i+j+1)"])
       (auto elim!: evenE oddE simp: algebra_simps power2_eq_square aux
             intro!: arg_cong[of _ _ "λa. q powi a"])
  also have "… ⟷ ((λ(n,(i,j)). q powi n) has_sum S) (SIGMA n:{n. odd n}. IJ n)"
  proof (rule has_sum_reindex_bij_witness[of _ snd "λ(i,j). (nat (i^2+j^2), (i,j))"])
    fix nij assume nij: "nij ∈ Sigma {n. odd n} IJ"
    obtain n i j where [simp]: "nij = (n, (i, j))"
      using prod_cases3 by blast
    from nij have n: "odd n" and ij: "i ^ 2 + j ^ 2 = int n"
      by (auto simp: IJ_def)
    have "odd (int n)"
      using n by simp
    also have "int n = i ^ 2 + j ^ 2"
      by (rule ij [symmetric])
    finally show "snd nij ∈ {(i, j). odd (i2 + j2)}"
      by auto
  qed (auto simp: IJ_def even_nat_iff)    
  finally have *: "((λ(n,(i,j)). q powi n) has_sum S) (SIGMA n:{n. odd n}. IJ n)" .
  have "((λn. count_sos 2 n * q ^ n) has_sum S) {n. odd n}"
  proof (rule has_sum_SigmaD[OF *]; unfold prod.case)
    fix n :: nat assume n: "n ∈ {n. odd n}"
    have "count_sos 2 n = card (IJ n)"
      by (simp add: IJ_def count_sos_2)
    thus "((λ(i,j). q powi int n) has_sum complex_of_nat (count_sos 2 n) * q ^ n) (IJ n)"
      using q by (simp add: has_sum_finite_iff)
  qed
  also have "?this ⟷ ((λn. (if odd n then of_nat (count_sos 2 n) else 0) * q ^ n) has_sum S) UNIV"
    by (intro has_sum_cong_neutral) auto
  finally show "(λn. (λn. if odd n then of_nat (count_sos 2 n) else 0) n * q ^ n) sums S"
    by (rule has_sum_imp_sums)
qed

lemma has_laurent_expansion_q_times_jacobi_theta_nw_10_aux_square_square:
  defines "F ≡ Abs_fps (λn. if odd n then of_nat (count_sos 2 n) else 0)"
  shows "(λq. q * jacobi_theta_nome (q2) (q2) ^ 2) has_laurent_expansion fps_to_fls F"
  unfolding has_laurent_expansion_def
proof
  have "0 < norm (1/2::complex)"
    by simp
  also have "fls_conv_radius (fps_to_fls F) ≥ norm (1 / 2 :: complex)"
    unfolding fls_conv_radius_fps_to_fls fps_conv_radius_def
    by (rule conv_radius_geI) (use sums_q_times_jacobi_theta_nw_10_aux_square_square[of "1/2"] 
        in  ‹auto simp: sums_iff F_def›)
  finally show "fls_conv_radius (fps_to_fls F) > 0" 
    by - (simp_all add: zero_ereal_def)
next
  have "eventually (λq. q ∈ ball 0 1 - {0}) (at (0::complex))"
    by (rule eventually_at_in_open) auto
  thus "∀F q in at 0. eval_fls (fps_to_fls F) q = q * (jacobi_theta_nome (q2) (q2))2"
  proof eventually_elim
    case q: (elim q)
    have "(λn. fps_nth F n * q ^ n) sums (q * (jacobi_theta_nome (q2) (q2))2)"
      using sums_q_times_jacobi_theta_nw_10_aux_square_square[of q] q by (simp add: F_def)
    thus "eval_fls (fps_to_fls F) q = q * (jacobi_theta_nome (q2) (q2))2"
      using eval_fls_eq[of 0 "fps_to_fls F" q "q * (jacobi_theta_nome (q2) (q2))2"]
      by (simp add: fls_subdegree_fls_to_fps_gt0)
  qed
qed


subsection ‹Identities›

text ‹
  Lastly, we derive a variety of identities between the different theta functions.
›

theorem jacobi_theta_nw_00_plus_01_complex: "θ3 q + θ4 q = 2 * θ3 (q ^ 4 :: complex)"
proof (cases "norm q < 1")
  case q: True
  define f :: "complex ⇒ complex" where "f = (λq. θ3 q + θ4 q - 2 * θ3 (q ^ 4))"
  define F :: "complex fps" 
    where "F = fps_jacobi_theta_nw 1 + fps_jacobi_theta_nw (-1) - 
               2 * (fps_jacobi_theta_nw 1 oo fps_X ^ 4)"
  have [simp]: "is_square (4 :: nat)"
    unfolding is_nth_power_def by (rule exI[of _ 2]) auto
  have "fps_jacobi_theta_nw 1 + fps_jacobi_theta_nw (-1 :: complex) =
        2 * Abs_fps (λn. if n = 0 then 1 else if even n ∧ is_square n then 2 else 0)"
    by (intro fps_ext) (auto simp: fps_jacobi_theta_nw_def intro: Nat.gr0I)
  also have "Abs_fps (λn. if n = 0 then 1 else if even n ∧ is_square n then 2 else 0) =
               fps_compose (fps_jacobi_theta_nw 1) (fps_X ^ 4)"
    by (auto simp: fps_eq_iff fps_jacobi_theta_nw_def fps_nth_compose_X_power is_square_mult2_nat_iff
                   is_nth_power_mult_cancel_left elim!: dvdE)
  finally have "F = 0"
    by (simp add: F_def)

  have "f q = 0"
  proof (rule has_fps_expansion_0_analytic_continuation[of f])
    have "(λq. θ3 q + θ4 q - 2 * (θ3 ∘ (λq. q ^ 4)) q) has_fps_expansion F"
      unfolding F_def by (intro fps_expansion_intros has_fps_expansion_compose) auto
    also have "F = 0"
      by fact
    finally show "f has_fps_expansion 0"
      by (simp add: f_def)
  next
    show "f holomorphic_on ball 0 1"
      unfolding f_def by (auto intro!: holomorphic_intros simp: norm_power power_less_one_iff)
  qed (use q in auto)
  thus ?thesis
    by (simp add: f_def)
qed (auto simp: norm_power power_less_one_iff)

lemma jacobi_theta_nw_00_plus_01_real: "θ3 q + θ4 q = 2 * θ3 (q ^ 4 :: real)"
  by (subst of_real_eq_iff [where ?'a = complex, symmetric],
         unfold of_real_add of_real_mult of_real_diff)
     (use jacobi_theta_nw_00_plus_01_complex[of q] 
      in  ‹simp_all flip: jacobi_theta_nome_00_of_real jacobi_theta_nome_01_of_real›)


theorem jacobi_theta_nw_00_plus_01_square_complex:
  "θ3 q ^ 2 + θ4 q ^ 2 = 2 * θ3 (q ^ 2 :: complex) ^ 2"
proof (cases "norm q < 1")
  case q: True
  define F :: "complex fps"
    where "F = 2 * fps_compose (fps_jacobi_theta_nw 1 ^ 2) (fps_X ^ 2) - 
               fps_jacobi_theta_nw 1 ^ 2 - fps_jacobi_theta_nw (-1) ^ 2"
  have "(λz. 2 * ((λz. θ3 z ^ 2) ∘ (λz. z ^ 2)) z - θ3 z ^ 2 - θ4 z ^ 2) has_fps_expansion F"
    unfolding F_def by (intro fps_expansion_intros has_fps_expansion_compose) auto
  also have "F = 0"
  proof -
    have "2 * fps_compose (Abs_fps (λn. of_nat (count_sos 2 n) :: complex)) (fps_X ^ 2) =
            Abs_fps (λn. if even n then of_nat (2 * count_sos 2 n) else 0)"
      by (auto elim!: evenE simp: fps_nth_compose_X_power fps_eq_iff count_sos_2_double)
    also have "… = fps_jacobi_theta_nw 1 ^ 2 + fps_jacobi_theta_nw (-1) ^ 2"
      by (auto simp: fps_eq_iff fps_jacobi_theta_power_eq)
    also have "Abs_fps (λn. of_nat (count_sos 2 n)) = fps_jacobi_theta_nw 1 ^ 2"
      by (simp add: fps_jacobi_theta_power_eq)
    finally show "F = 0" 
      by (simp add: algebra_simps F_def)
  qed
  finally have "(λz::complex. 2 * θ3 (z2) ^ 2 - θ3 z ^ 2 - θ4 z ^ 2) has_fps_expansion 0"
    by simp
  hence "2 * (θ3 (q2))2 - (θ3 q)2 - (θ4 q)2 = 0"
    by (rule has_fps_expansion_0_analytic_continuation[where A = "ball 0 1"])
       (use q in ‹auto intro!: holomorphic_intros simp: norm_power power_less_one_iff›)
  thus ?thesis
    by (simp add: algebra_simps)
qed (auto simp: norm_power power_less_one_iff)

corollary midpoint_jacobi_theta_nw_00_01_square_complex:
  "midpoint (θ3 q ^ 2) (θ4 q ^ 2) = θ3 (q ^ 2 :: complex) ^ 2"
  using jacobi_theta_nw_00_plus_01_square_complex[of q] by (simp add: midpoint_def)

lemma jacobi_theta_nw_00_plus_01_square_real: "θ3 q ^ 2 + θ4 q ^ 2 = 2 * θ3 (q ^ 2 :: real) ^ 2"
  by (subst of_real_eq_iff [where ?'a = complex, symmetric],
         unfold of_real_add of_real_mult of_real_diff)
     (use jacobi_theta_nw_00_plus_01_square_complex[of q] 
      in  ‹simp_all flip: jacobi_theta_nome_00_of_real jacobi_theta_nome_01_of_real›)

theorem jacobi_theta_nw_00_times_01_complex: "θ3 q * θ4 q = (θ4 (q ^ 2) ^ 2 :: complex)"
proof -
  have "2 * θ3 q * θ4 q = (θ3 q + θ4 q) ^ 2 - (θ3 q ^ 2 + θ4 q ^ 2)"
    by Groebner_Basis.algebra
  also have "… = 2 * (2 * θ3 (q ^ 4) ^ 2 - θ3 (q2) ^ 2)"
    unfolding jacobi_theta_nw_00_plus_01_complex jacobi_theta_nw_00_plus_01_square_complex
    by Groebner_Basis.algebra
  also have "2 * θ3 (q ^ 4) ^ 2 - θ3 (q2) ^ 2 = θ4 (q2) ^ 2"
    using jacobi_theta_nw_00_plus_01_square_complex[of "q ^ 2"]
    by (simp add: algebra_simps)
  finally show ?thesis
    by simp
qed

lemma jacobi_theta_nw_00_times_01_real: "θ3 q * θ4 q = (θ4 (q ^ 2) ^ 2 :: real)"
  by (subst of_real_eq_iff [where ?'a = complex, symmetric],
         unfold of_real_add of_real_mult of_real_diff)
     (use jacobi_theta_nw_00_times_01_complex[of q] 
      in  ‹simp_all flip: jacobi_theta_nome_00_of_real jacobi_theta_nome_01_of_real›)

lemma jacobi_theta_nw_00_plus_10_square_square_aux:
  fixes q :: complex
  shows "θ3 q ^ 2 - θ3 (q2) ^ 2 = q * jacobi_theta_nome (q2) (q2) ^ 2"
proof (cases "q ≠ 0 ∧ norm q < 1")
  case True
  define f :: "complex ⇒ complex"
    where "f = (λq. θ3 q ^ 2 - ((λq. θ3 q ^ 2) ∘ (λq. q ^ 2)) q - q * jacobi_theta_nome (q2) (q2) ^ 2)"
  define F where "F = (fps_to_fls (fps_jacobi_theta_nw 1))2 -
    fps_to_fls ((fps_jacobi_theta_nw 1)2 oo fps_X2) -
    fps_to_fls (Abs_fps (λn. if odd n then complex_of_nat (count_sos 2 n) else 0))"
  have "f has_laurent_expansion F"
    unfolding F_def f_def
    by (intro laurent_expansion_intros fps_expansion_intros
              has_laurent_expansion_q_times_jacobi_theta_nw_10_aux_square_square
              has_laurent_expansion_fps) auto
  also have "F = fps_to_fls 0"
    unfolding F_def fps_to_fls_power [symmetric] fps_to_fls_minus [symmetric] fps_to_fls_eq_iff
    by (auto simp: fps_eq_iff fps_jacobi_theta_power_eq fps_nth_compose_X_power count_sos_2_double 
             elim!: evenE)
  finally have "f has_laurent_expansion 0" 
    by simp

  have "f q = 0"
  proof (rule has_laurent_expansion_0_analytic_continuation[of f])
    show "f has_laurent_expansion 0"
      by fact
    show "f holomorphic_on ball 0 1 - {0}"
      by (auto simp: f_def o_def norm_power power_less_one_iff intro!: holomorphic_intros)
  qed (use True in auto)
  thus ?thesis
    by (simp add: f_def)
qed (auto simp: norm_power power_less_one_iff)

theorem jacobi_theta_nw_00_plus_10_square_square_complex:
  fixes q :: complex
  assumes "Re q ≥ 0 ∧ (Re q = 0 ⟶ Im q ≥ 0)"
  shows   "θ3 (q2) ^ 2 + θ2 (q2) ^ 2 = θ3 q ^ 2"
proof -
  have "θ3 q ^ 2 - θ3 (q2) ^ 2 = q * jacobi_theta_nome (q2) (q2) ^ 2"
    by (rule jacobi_theta_nw_00_plus_10_square_square_aux)
  also have "q = ((q ^ 2) powr (1 / 4)) ^ 2"
  proof -
    have "((q ^ 2) powr (1 / 4)) ^ 2 = csqrt (q ^ 2)"
      using assms by (auto simp add: powr_def csqrt_exp_Ln simp flip: exp_of_nat_mult)
    also have "csqrt (q ^ 2) = q"
      by (rule csqrt_unique) (use assms in ‹auto simp: not_less›)
    finally show ?thesis ..
  qed
  hence "q * jacobi_theta_nome (q2) (q2) ^ 2 = θ2 (q ^ 2) ^ 2"
    by (simp add: jacobi_theta_nome_10_def power_mult_distrib)
  finally show ?thesis by (Groebner_Basis.algebra)
qed

lemma jacobi_theta_nw_00_plus_10_square_square_real:
  assumes "q ≥ (0::real)"
  shows   "θ3 (q2) ^ 2 + θ2 (q2) ^ 2 = θ3 q ^ 2"
  by (subst of_real_eq_iff [where ?'a = complex, symmetric],
         unfold of_real_add of_real_mult of_real_diff)
     (use jacobi_theta_nw_00_plus_10_square_square_complex[of q] assms 
      in  ‹simp_all flip: jacobi_theta_nome_00_of_real jacobi_theta_nome_10_complex_of_real›)


theorem jacobi_theta_nw_00_minus_10_square_square_complex:
  assumes "0 ≤ Re q ∧ (Re q = 0 ⟶ 0 ≤ Im q)"
  shows   "θ3 (q2) ^ 2 - θ2 (q2) ^ 2 = θ4 (q :: complex) ^ 2"
  using jacobi_theta_nw_00_plus_01_square_complex[of q]
        jacobi_theta_nw_00_plus_10_square_square_complex[OF assms]
  by Groebner_Basis.algebra

lemma jacobi_theta_nw_00_minus_10_square_square_real:
  assumes "q ≥ (0::real)"
  shows   "θ3 (q2) ^ 2 - θ2 (q2) ^ 2 = θ4 q ^ 2"
  using jacobi_theta_nw_00_plus_01_square_real[of q]
        jacobi_theta_nw_00_plus_10_square_square_real[OF assms]
  by Groebner_Basis.algebra

text ‹
  The following shows that the theta nullwerte provide a parameterisation of the
  Fermat curve $X^4 + Y^4 = Z^4$:
›
theorem jacobi_theta_nw_pow4_complex: "θ2 q ^ 4 + θ4 q ^ 4 = (θ3 q ^ 4 :: complex)"
proof (cases "norm q < 1")
  case q: True
  define r where "r = csqrt q"
  have q_eq: "q = r ^ 2"
    by (simp add: r_def)
  have "norm r < 1"
    using q by (auto simp: r_def)
  have "0 ≤ Re r ∧ (Re r = 0 ⟶ 0 ≤ Im r)"
    using csqrt_principal[of q] by (auto simp: r_def simp del: csqrt.sel)
  note r = ‹norm r < 1› this

  have "θ3 q ^ 4 - θ2 q ^ 4 = (θ3 q ^ 2 + θ2 q ^ 2) * (θ3 q ^ 2 - θ2 q ^ 2)"
    by Groebner_Basis.algebra
  also have "… = (θ3 r * θ4 r) ^ 2"
    using jacobi_theta_nw_00_plus_10_square_square_complex[OF r(2)]
          jacobi_theta_nw_00_minus_10_square_square_complex[OF r(2)]
    unfolding q_eq by Groebner_Basis.algebra
  also have "θ3 r * θ4 r = θ4 q ^ 2"
    unfolding q_eq using jacobi_theta_nw_00_times_01_complex[of r] .
  finally have "θ3 q ^ 4 - θ2 q ^ 4 = θ4 q ^ 4"
    by simp
  thus ?thesis
    by Groebner_Basis.algebra
qed auto

lemma jacobi_theta_nw_pow4_real: "q ≥ 0 ⟹ θ2 q ^ 4 + θ4 q ^ 4 = (θ3 q ^ 4 :: real)"
  by (subst of_real_eq_iff [where ?'a = complex, symmetric],
         unfold of_real_add of_real_mult of_real_diff)
      (use jacobi_theta_nw_pow4_complex[of q] 
       in  ‹simp_all flip: jacobi_theta_nome_00_of_real jacobi_theta_nome_01_of_real 
                           jacobi_theta_nome_10_complex_of_real›)




subsection ‹Properties of the nullwert functions on the real line›

lemma has_field_derivative_jacobi_theta_nw_00:
  fixes q :: "'a :: {real_normed_field,banach}"
  assumes q: "norm q < 1"
  defines "a ≡ (λn. 2 * (of_nat n + 1)2 * q ^ (n * (n + 2)))"
  shows "summable a" "(θ3 has_field_derivative (∑n. a n)) (at q)"
proof -
  define F :: "'a fps" where "F = fps_jacobi_theta_nw 1"
  define F' where [simp]: "F' = fps_deriv F"
  define f' :: "'a ⇒ 'a" where "f' = eval_fps F"
  have [simp]: "fps_conv_radius F = 1"
    unfolding F_def using fps_conv_radius_jacobi_theta_nw[of "1::'a"] 
    by (simp add: one_ereal_def)

  have "(λn. fps_nth F' n * q ^ n) sums eval_fps F' q"
    by (rule sums_eval_fps)
       (use q in ‹auto intro!: less_le_trans[OF _ fps_conv_radius_deriv]›)
  moreover have "bij_betw (λn. (n+1)^2 - 1) UNIV {n. is_square (Suc n)}"
    by (rule bij_betwI[of _ _ _ "λn. Discrete.sqrt (n+1) - 1"]) (auto elim!: is_nth_powerE)
  moreover have "strict_mono (λn::nat. (n+1)^2 - 1)"
    by (intro strict_monoI_Suc) (auto simp: power2_eq_square)
  ultimately have "(λn. fps_nth (fps_deriv F) ((n+1)^2 - 1) * q ^ ((n+1)^2 - 1)) sums 
                     eval_fps (fps_deriv F) q"
    by (subst sums_mono_reindex) (auto simp: F_def fps_jacobi_theta_nw_def bij_betw_def)
  also have "(λn. fps_nth (fps_deriv F) ((n+1)^2 - 1) * q ^ ((n+1)^2 - 1)) = 
             (λn. 2 * (of_nat n + 1)^2 * q ^ ((n+1)^2-1))"
    by (auto simp: F_def fps_jacobi_theta_nw_def add_ac)
  also have "(λn::nat. (n+1) ^ 2 - 1) = (λn. n * (n + 2))"
    by (simp add: algebra_simps power2_eq_square)
  finally have "a sums eval_fps (fps_deriv F) q"
    by (simp only: a_def)

  moreover have "(θ3 has_field_derivative (eval_fps F' q)) (at q)"
  proof -
    have "ereal (norm q) < fps_conv_radius F"
      using q by (auto simp: one_ereal_def)
    hence "(eval_fps F has_field_derivative (eval_fps F' q)) (at q)"
      unfolding F'_def by (rule has_field_derivative_eval_fps)
    also have "?this ⟷ ?thesis"
    proof (intro DERIV_cong_ev)
      have "eventually (λt. t ∈ ball 0 1) (nhds q)"
        by (rule eventually_nhds_in_open) (use q in auto)
      thus "eventually (λt. eval_fps F t = θ3 t) (nhds q)"
      proof eventually_elim
        case (elim t)
        thus ?case
          using sums_jacobi_theta_nw_00[of t] by (simp add: sums_iff eval_fps_def F_def)
      qed
    qed auto
    finally show ?thesis .
  qed

  ultimately show "summable a" "(θ3 has_field_derivative (∑n. a n)) (at q)"
    by (simp_all add: sums_iff)
qed

lemma jacobi_theta_nw_10_le_00:
  assumes "q ≥ (0::real)"
  shows   "θ2 q ≤ θ3 q"
proof (cases "q < 1")
  case True
  with assms have q: "q ≥ 0" "q < 1"
    by auto
  define r where "r = sqrt q"
  have "0 ≤ θ3 q"
    using has_sum_jacobi_theta_nw_00[of q] by (rule has_sum_nonneg) (use q in auto)
  have "(θ3 q)2 - (θ2 q)2 = (θ4 r)2"
    using jacobi_theta_nw_00_minus_10_square_square_real[of r] q
    by (simp add: r_def)
  also have "… ≥ 0"
    by simp
  finally have "(θ3 q)2 ≥ (θ2 q)2"
    by simp
  thus "θ3 q ≥ θ2 q"
    by (rule power2_le_imp_le) (fact ‹θ3 q ≥ 0›)
qed auto

lemma jacobi_theta_nw_00_pos:
  fixes q :: real
  assumes "q ∈ {-1<..<1}"
  shows   "θ3 q > 0"
proof -
  have pos: "θ3 q > 0" if "q ∈ {0..<1}" for q :: real
    using has_sum_0 has_sum_jacobi_theta_nw_00
  proof (rule has_sum_strict_mono)
    show "0 < q powi 0 ^ 2"
      by auto
  qed (use that in auto)

  have "θ4 q > 0" if q: "q ∈ {0..<1}" for q :: real
  proof - 
    have eq: "θ3 q * θ4 q = (θ4 (q ^ 2) ^ 2)"
      by (rule jacobi_theta_nw_00_times_01_real)
    have "θ3 q * θ4 q ≥ 0"
      by (subst eq) auto
    with pos[of q] q have "θ4 q ≥ 0"
      by (simp add: zero_le_mult_iff)
  
    have zero_iff: "θ4 q = 0 ⟷ θ4 (q ^ 2) = 0" if "q ∈ {0..<1}" for q :: real
      using jacobi_theta_nw_00_times_01_real[of q] pos[of q] that by auto
  
    have "θ4 q ≠ 0"
    proof
      assume "θ4 q = 0"
      have "θ4 (q ^ (2 ^ n)) = 0" for n
      proof (induction n)
        case (Suc n)
        have "θ4 (q ^ (2 ^ Suc n)) = θ4 ((q ^ (2 ^ n)) ^ 2)"
          by (simp flip: power_mult add: mult_ac)
        also have "… = 0 ⟷ θ4 (q ^ (2 ^ n)) = 0"
          by (subst zero_iff [symmetric]) (use q in ‹auto simp: power_less_one_iff›)
        finally show ?case
          using Suc.IH by simp
      qed (use ‹θ4 q = 0› in auto)
      hence "(λn. θ4 (q ^ (2 ^ n))) ⇢ 0"
        by simp
      moreover have "(λn. θ4 (q ^ (2 ^ n))) ⇢ θ4 0"
      proof (rule continuous_on_tendsto_compose[of _ θ4])
        show "continuous_on {0..<1::real} θ4"
          by (intro continuous_intros) auto
        show "(λn. q ^ (2 ^ n)) ⇢ 0"
        proof (cases "q = 0")
          case False
          thus ?thesis
            using q by real_asymp
        qed (auto simp: power_0_left)
      qed (use q in ‹auto simp: power_less_one_iff›)
      ultimately have "θ4 (0::real) = 0"
        using LIMSEQ_unique by blast
      thus False
        by simp
    qed
    with ‹θ4 q ≥ 0› show "θ4 q > 0"
      by simp
  qed
  from this[of "-q"] and pos[of q] show ?thesis
    using assms by (cases "q ≥ 0") (auto simp: jacobi_theta_nw_01_conv_00)
qed

lemma jacobi_theta_nw_01_pos: "q ∈ {-1<..<1} ⟹ θ4 q > (0::real)"
  using jacobi_theta_nw_00_pos[of "-q"]
  by (simp add: jacobi_theta_nw_01_conv_00)

lemma jacobi_theta_nw_00_nonneg: "θ3 q ≥ (0::real)"
  using jacobi_theta_nw_00_pos[of q] by (cases "norm q < 1") (auto simp: abs_less_iff)

lemma jacobi_theta_nw_01_nonneg: "θ4 q ≥ (0::real)"
  by (simp add: jacobi_theta_nw_01_conv_00 jacobi_theta_nw_00_nonneg)

lemma strict_mono_jacobi_theta_nw_00: "strict_mono_on {-1<..<1::real} θ3"
proof -
  have theta3_less: "θ3 x < θ3 y" if xy: "0 ≤ x" "x < y" "y < 1" for x y :: real
  proof (rule has_sum_strict_mono)
    show "((λn. x powi n2) has_sum θ3 x) UNIV" "((λn. y powi n2) has_sum θ3 y) UNIV"
      by (rule has_sum_jacobi_theta_nw_00; use xy in simp)+
    show "x powi (n^2) ≤ y powi (n^2)" for n :: int
      by (intro power_int_mono) (use xy in auto)
    show "x powi (1^2) < y powi (1^2)"
      using xy by auto
  qed auto    

  have theta4_less: "θ4 x < θ4 y" if xy: "0 ≤ y" "y < x" "x < 1" for x y :: real
  proof -
    include qpochhammer_inf_notation
    have "θ4 x = jacobi_theta_nome (-1) x"
      by (simp add: jacobi_theta_nome_01_def)
    also have "… = (x2 ; x2)∞ * ((x ; x2)∞) ^ 2"
      by (subst jacobi_theta_nome_triple_product_real) (use xy in ‹simp_all add: power2_eq_square›)
    also have "… < (x2 ; x2)∞ * ((y ; y2)∞) ^ 2"
    proof (intro mult_strict_left_mono power_strict_mono)
      show "(x2 ; x2)∞ > 0" "(x ; x2)∞ ≥ 0"
        using xy by (auto intro!: qpochhammer_inf_pos qpochhammer_inf_nonneg simp: power_less_one_iff)
    next
      show "(x ; x2)∞ < (y ; y2)∞"
      proof (rule has_prod_less)
        show "(λn. 1 - x * (x^2)^n) has_prod (x ; x2)∞"
             "(λn. 1 - y * (y^2)^n) has_prod (y ; y2)∞"
          by (rule has_prod_qpochhammer_inf; use xy in ‹simp add: power_less_one_iff›)+
      next
        show "1 - x * (x^2)^0 < 1 - y * (y^2)^0"
          using xy by simp
      next
        fix n :: nat
        have "x * (x2)^n = x^(2*n+1)"
          by (simp add: power_mult power_add)
        also have "… < 1"
          by (subst power_less_one_iff) (use xy in auto)
        finally show "1 - x * (x2)^n > 0"
          by simp
      next
        fix n :: nat
        have "x^(2*n+1) ≥ y^(2*n+1)"
          by (intro power_mono) (use xy in auto)
        thus "1 - x * (x2) ^ n ≤ 1 - y * (y2) ^ n"
          by (simp add: power_mult)
      qed      
    qed auto
    also have "… ≤ (y2 ; y2)∞ * ((y ; y2)∞) ^ 2"
    proof (intro mult_right_mono zero_le_power)
      show "(y ; y2)∞ ≥ 0"
        by (intro qpochhammer_inf_nonneg) (use xy in ‹auto simp: power_less_one_iff›)
    next
      show "(x2 ; x2)∞ ≤ (y2 ; y2)∞"
      proof (rule has_prod_le[OF _ _ conjI])
        show "(λn. 1 - x2 * (x^2)^n) has_prod (x2 ; x2)∞"
             "(λn. 1 - y2 * (y^2)^n) has_prod (y2 ; y2)∞"
          by (rule has_prod_qpochhammer_inf; use xy in ‹simp add: power_less_one_iff›)+
      next
        fix n :: nat
        have "x2 * (x2)^n = x^(2*n+2)"
          by (simp add: power_mult power_add power2_eq_square)
        also have "… ≤ 1"
          by (subst power_le_one_iff) (use xy in auto)
        finally show "1 - x2 * (x2)^n ≥ 0"
          by simp
      next
        fix n :: nat
        have "x^(2*n+2) ≥ y^(2*n+2)"
          by (intro power_mono) (use xy in auto)
        thus "1 - x2 * (x2) ^ n ≤ 1 - y2 * (y2) ^ n"
          by (simp add: power_mult power2_eq_square)
      qed
    qed
    also have "… = jacobi_theta_nome (-1) y"
      by (subst jacobi_theta_nome_triple_product_real) (use xy in ‹simp_all add: power2_eq_square›)
    also have "… = θ4 y"
      by (simp add: jacobi_theta_nome_01_def)
    finally show "θ4 x < θ4 y" .
  qed

  show "strict_mono_on {-1<..<1::real} θ3"
  proof (rule strict_mono_onI)
    fix x y :: real
    assume xy: "x ∈ {-1<..<1}" "y ∈ {-1<..<1}" "x < y"
    consider "x ≥ 0" | "y ≤ 0" | "x < 0" "y > 0"
      using xy by linarith
    thus "θ3 x < θ3 y"
    proof cases
      assume "x ≥ 0"
      thus ?thesis by (intro theta3_less) (use xy in auto)
    next
      assume "y ≤ 0"
      hence "θ4 (-x) < θ4 (-y)"
        by (intro theta4_less) (use xy in auto)
      thus ?thesis
        by (simp add: jacobi_theta_nw_01_conv_00)
    next
      assume xy': "x < 0" "y > 0"
      have "θ4 (-x) < θ4 0"
        by (rule theta4_less) (use xy xy' in auto)
      moreover have "θ3 0 < θ3 y"
        by (rule theta3_less) (use xy xy' in auto)
      ultimately show ?thesis
        by (simp add: jacobi_theta_nw_01_conv_00)
    qed
  qed
qed

lemma strict_antimono_jacobi_theta_nw_01: "strict_antimono_on {-1<..<1::real} θ4"
  by (auto intro!: monotone_onI strict_mono_onD[OF strict_mono_jacobi_theta_nw_00] 
           simp: jacobi_theta_nw_01_conv_00)

lemma jacobi_theta_nw_10_nonneg:
  assumes "x ≥ 0"
  shows   "θ2 x ≥ (0::real)"
proof -
  consider "x = 0" | "x ≥ 1" | "x ∈ {0<..<1}"
    using assms by force
  thus ?thesis
  proof cases
    assume x: "x ∈ {0<..<1}"
    show ?thesis
      using has_sum_jacobi_theta_nw_10_real
      by (rule has_sum_nonneg) (use x in auto)
  qed auto
qed

lemma strict_mono_jacobi_theta_nw_10: "strict_mono_on {0::real..<1} θ2"
proof (rule strict_mono_onI)
  fix x y :: real
  assume xy: "x ∈ {0..<1}" "y ∈ {0..<1}" "x < y"
  note mono_rules = strict_mono_jacobi_theta_nw_00 strict_antimono_jacobi_theta_nw_01

  have "θ2 x ^ 4 = θ3 x ^ 4 - θ4 x ^ 4"
    by (subst jacobi_theta_nw_pow4_real [symmetric]) (use xy in auto)
  also have "… < θ3 y ^ 4 - θ4 y ^ 4"
    by (intro diff_strict_mono power_strict_mono mono_rules[THEN monotone_onD]
             jacobi_theta_nw_00_nonneg jacobi_theta_nw_01_nonneg)
       (use xy in auto)
  also have "… = θ2 y ^ 4"
    by (subst jacobi_theta_nw_pow4_real [symmetric]) (use xy in auto)
  finally show "θ2 x < θ2 y"
    by (rule power_less_imp_less_base) (use xy in ‹auto intro!: jacobi_theta_nw_10_nonneg›)
qed

lemma jacobi_theta_nw_10_pos:
  assumes "x ∈ {0<..<1}"
  shows   "θ2 x > (0::real)"
  using strict_mono_onD[OF strict_mono_jacobi_theta_nw_10, of 0 x] assms by simp

end