Theory Theta_Functions
section ‹General theta functions›
theory Theta_Functions
imports
Nome
"Combinatorial_Q_Analogues.Q_Binomial_Identities"
Theta_Functions_Library
begin
subsection ‹The Ramanujan theta function›
text ‹
We define the other theta functions in terms of the Ramanujan theta function:
\[f(a,b) = \sum_{n=-\infty}^\infty a^{n(n+1)/2} b^{n(n-1)/2}\hskip1.5em (\text{for}\ |ab|<1)\]
This is, in some sense, more general than Jacobi's theta function: Jacobi's theta function can
be expressed very easily in terms of Ramanujan's; the other direction is only straightforward
in the real case. Due to the presence of square roots, the complex case becomes tedious
due to branch cuts.
However, even in the complex case, results can be transferred from Jacobi's theta function
to Ramanujan's by using the connection on the real line and then doing analytic continuation.
Some of the proofs below are loosely based on Ramanujan's lost notebook (as edited by
Berndt~\<^cite>‹berndt1991›).
›
definition ramanujan_theta :: "'a :: {real_normed_field, banach} ⇒ 'a ⇒ 'a" where
"ramanujan_theta a b =
(if norm (a*b) < 1 then (∑⇩∞n. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) else 0)"
lemma ramanujan_theta_outside [simp]: "norm (a * b) ≥ 1 ⟹ ramanujan_theta a b = 0"
by (simp add: ramanujan_theta_def)
lemma uniform_limit_ramanujan_theta:
fixes A :: "('a × 'a :: {real_normed_field, banach}) set"
assumes "compact A" "⋀a b. (a, b) ∈ A ⟹ norm (a * b) < 1"
shows "uniform_limit A (λX (a,b). ∑n∈X. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2))
(λ(a,b). ∑⇩∞n. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2))
(finite_subsets_at_top UNIV)"
proof (cases "A = {}")
case False
define f where "f = (λn ab. fst ab powi (n*(n+1) div 2) * snd ab powi (n*(n-1) div 2) :: 'a)"
define y where "y = max (1/2) (Sup ((λ(a,b). norm (a * b)) ` A))"
define x where "x = max 2 (Sup ((λ(a,b). max (norm a) (norm b)) ` A))"
have le_x: "norm a ≤ x" "norm b ≤ x" if "(a, b) ∈ A" for a b
proof -
have bounded: "bounded ((λ(a,b). max (norm a) (norm b)) ` A)"
unfolding case_prod_unfold
by (intro compact_imp_bounded compact_continuous_image continuous_intros assms)
have "(λ(a,b). max (norm a) (norm b)) (a, b) ≤ Sup ((λ(a,b). max (norm a) (norm b)) ` A)"
by (rule cSup_upper imageI)+
(use that bounded in ‹auto intro: bounded_imp_bdd_above›)
also have "… ≤ x"
unfolding x_def by linarith
finally show "norm a ≤ x" "norm b ≤ x"
by simp_all
qed
have le_y: "norm (a*b) ≤ y" if "(a, b) ∈ A" for a b
proof -
have bounded: "bounded ((λ(a,b). norm (a * b)) ` A)"
unfolding case_prod_unfold
by (intro compact_imp_bounded compact_continuous_image continuous_intros assms)
have "(λ(a,b). norm (a * b)) (a, b) ≤ Sup ((λ(a,b). norm (a * b)) ` A)"
by (rule cSup_upper imageI)+
(use that bounded in ‹auto intro: bounded_imp_bdd_above›)
also have "… ≤ y"
unfolding y_def by linarith
finally show ?thesis
by simp
qed
have "x > 1" "y > 0"
unfolding x_def y_def by linarith+
have "y < 1"
proof -
have "Sup ((λ(a,b). norm (a * b)) ` A) ∈ (λ(a,b). norm (a * b)) ` A" using ‹A ≠ {}›
unfolding case_prod_unfold
by (intro closed_contains_Sup compact_imp_closed compact_continuous_image
bounded_imp_bdd_above compact_imp_bounded continuous_intros assms) auto
with assms show ?thesis
by (auto simp: y_def)
qed
define h where "h = (λn. x ^ nat ¦n¦ * y ^ nat (min (n*(n+1) div 2) (n*(n-1) div 2)))"
have "uniform_limit A (λX wq. ∑n∈X. f n wq) (λwq. ∑⇩∞n. f n wq) (finite_subsets_at_top UNIV)"
proof (rule Weierstrass_m_test_general, clarify)
fix n :: int and a b :: 'a
assume ab: "(a, b) ∈ A"
have eq: "n * (n + 1) div 2 = n * (n - 1) div 2 + n"
by (simp add: algebra_simps)
have nonneg: "n * (n - 1) div 2 ≥ 0" "n * (n + 1) div 2 ≥ 0" "n * (n - 1) ≥ 0" "n * (n + 1) ≥ 0"
by (auto simp: zero_le_mult_iff)
have "norm (f n (a, b)) = norm a powi (n*(n+1) div 2) * norm b powi (n*(n-1) div 2)"
by (simp add: f_def norm_mult norm_power_int)
also have "(n*(n+1) div 2) = int (nat (n*(n+1) div 2))"
by (auto simp: zero_le_mult_iff)
also have "(n*(n-1) div 2) = int (nat (n*(n-1) div 2))"
by (auto simp: zero_le_mult_iff)
also have "norm a powi int (nat (n*(n+1) div 2)) * norm b powi int (nat (n*(n-1) div 2)) =
norm a ^ nat (n*(n+1) div 2) * norm b ^ nat (n*(n-1) div 2)"
unfolding power_int_of_nat ..
also have "… = (if n ≥ 0 then norm a ^ nat ¦n¦ * norm (a*b) ^ nat (n*(n-1) div 2)
else norm b ^ nat ¦n¦ * norm (a*b) ^ nat (n*(n+1) div 2))"
using nonneg(1,2) [[linarith_split_limit = 0]] unfolding eq
by (auto simp flip: power_add simp: power_mult_distrib norm_mult nat_eq_iff nonneg(3,4)
intro!: arg_cong[of _ _ "λn. x ^ n" for x] split: if_splits)
also have "… ≤ x ^ nat ¦n¦ * norm (a*b) ^ nat (min (n*(n+1) div 2) (n*(n-1) div 2))"
using le_x[of a b] ab ‹x > 1› le_y[of a b] ‹y < 1› [[linarith_split_limit = 0]]
by (auto intro!: mult_mono power_mono power_decreasing nat_mono)
also have "… ≤ x ^ nat ¦n¦ * y ^ nat (min (n*(n+1) div 2) (n*(n-1) div 2))"
by (intro mult_left_mono power_mono le_y) (use ab ‹x > 1› in auto)
also have "… = h n"
by (simp add: h_def)
finally show "norm (f n (a, b)) ≤ h n" .
next
obtain y' where y': "y < y'" "y' < 1"
using ‹y < 1› dense by blast
have "summable (λn. norm (h (int n)))"
proof (rule summable_comparison_test_bigo)
have "(λn. x ^ n * y ^ nat (min (int n * (int n + 1) div 2) (int n * (int n - 1) div 2))) ∈ O(λn. y' ^ n)"
using ‹x > 1› ‹y > 0› y' by real_asymp
thus "(λn. norm (h (int n))) ∈ O(λn. y' ^ n)"
unfolding h_def by (simp add: norm_power norm_mult nat_power_eq power_int_def)
next
show "summable (λn. norm (y' ^ n))"
unfolding norm_power by (rule summable_geometric) (use ‹y > 0› y' in auto)
qed
hence "(λn. h (int n)) summable_on UNIV"
by (rule norm_summable_imp_summable_on)
also have "?this ⟷ h summable_on {0..}"
by (rule summable_on_reindex_bij_witness[of _nat int]) auto
finally have *: "h summable_on {0..}" .
from * have "h summable_on {0<..}"
by (rule summable_on_subset) auto
also have "h summable_on {0<..} ⟷ h summable_on {..<0}"
by (rule summable_on_reindex_bij_witness[of _ "λn. -n" "λn. -n"])
(auto simp: h_def algebra_simps)
finally have "h summable_on {..<0}" .
from this and * have "h summable_on {..<0} ∪ {0..}"
by (rule summable_on_union)
also have "{..<0} ∪ {0..} = (UNIV :: int set)"
by auto
finally show "h summable_on UNIV" .
qed
thus ?thesis
by (simp add: f_def case_prod_unfold)
qed auto
lemma has_sum_ramanujan_theta:
assumes "norm (a*b) < 1"
shows "((λn. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum ramanujan_theta a b) UNIV"
proof -
show ?thesis
using uniform_limit_ramanujan_theta[of "{(a, b)}"] assms
by (simp add: ramanujan_theta_def has_sum_def uniform_limit_singleton)
qed
lemma ramanujan_theta_commute: "ramanujan_theta a b = ramanujan_theta b a"
proof (cases "norm (a * b) < 1")
case ab: True
have "((λn. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum ramanujan_theta a b) UNIV"
by (intro has_sum_ramanujan_theta ab)
also have "?this ⟷ ((λn. b powi (n*(n+1) div 2) * a powi (n*(n-1) div 2)) has_sum ramanujan_theta a b) UNIV"
by (intro has_sum_reindex_bij_witness[of _ uminus uminus]) (auto simp: algebra_simps)
finally have … .
moreover have "((λn. b powi (n*(n+1) div 2) * a powi (n*(n-1) div 2)) has_sum ramanujan_theta b a) UNIV"
by (intro has_sum_ramanujan_theta) (use ab in ‹simp_all add: norm_mult mult.commute›)
ultimately show ?thesis
using has_sum_unique by blast
qed (simp_all add: ramanujan_theta_def mult.commute)
lemma ramanujan_theta_0_left [simp]: "ramanujan_theta 0 b = 1 + b"
proof -
have *: "n * (n + 1) div 2 = 0 ⟷ n ∈ {0, -1}" for n :: int
proof -
have "even (n * (n + 1))"
by auto
hence "n * (n + 1) div 2 = 0 ⟷ n * (n + 1) = 0"
by (elim evenE) simp_all
also have "… ⟷ n ∈ {0, -1}"
unfolding mult_eq_0_iff by auto
finally show ?thesis .
qed
have "((λn. 0 powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum (1 + b)) {0, -1}"
by (rule has_sum_finiteI) auto
also have "?this ⟷ ((λn. 0 powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum (1 + b)) UNIV"
by (intro has_sum_cong_neutral) (auto simp: *)
finally have "((λn. 0 powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum (1 + b)) UNIV" .
moreover have "((λn. 0 powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum ramanujan_theta 0 b) UNIV"
by (intro has_sum_ramanujan_theta) auto
ultimately show ?thesis
using has_sum_unique by blast
qed
lemma ramanujan_theta_0_right [simp]: "ramanujan_theta a 0 = 1 + a"
by (subst ramanujan_theta_commute) simp_all
lemma has_sum_ramanujan_theta1:
assumes "norm (a*b) < 1" and [simp]: "a ≠ 0"
shows "((λn. a powi n * (a*b) powi (n*(n-1) div 2)) has_sum ramanujan_theta a b) UNIV"
proof -
have eq: "n*(n+1) div 2 = n*(n-1) div 2 + n" for n :: int
by (cases "even n") (auto elim!: evenE oddE simp: algebra_simps)
have "((λn. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum ramanujan_theta a b) UNIV"
by (rule has_sum_ramanujan_theta) (use assms in auto)
thus ?thesis
unfolding eq by (simp add: power_int_mult_distrib power_int_add mult_ac)
qed
lemma has_sum_ramanujan_theta2:
assumes "norm (a * b) < 1"
shows "((λn. (a*b) powi (n*(n-1) div 2) * (a powi n + b powi n)) has_sum
(ramanujan_theta a b - 1)) {1..}"
proof (cases "a * b = 0")
case True
have "((λn. (a*b) powi (n*(n-1) div 2) * (a powi n + b powi n)) has_sum (ramanujan_theta a b - 1)) {1}"
using True by (intro has_sum_finiteI) auto
also have "?this ⟷ ?thesis"
using True by (intro has_sum_cong_neutral) (auto simp: dvd_div_eq_0_iff)
finally show ?thesis .
next
case False
hence [simp]: "a ≠ 0" "b ≠ 0"
by auto
define S1 where "S1 = (∑⇩∞n∈{1..}. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2))"
define S2 where "S2 = (∑⇩∞n∈{..-1}. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2))"
have eq: "n*(n+1) div 2 = n*(n-1) div 2 + n" for n :: int
by (cases "even n") (auto elim!: evenE oddE simp: algebra_simps)
have 1: "((λn. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum ramanujan_theta a b) UNIV"
by (rule has_sum_ramanujan_theta) (use assms in auto)
have [intro]: "(λn. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) summable_on A" for A
by (rule summable_on_subset_banach, rule has_sum_imp_summable[OF 1]) auto
have S1: "((λn. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum S1) {1..}"
unfolding S1_def by (rule has_sum_infsum) rule
also have "(λn. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) =
(λn. (a*b) powi (n*(n-1) div 2) * a powi n)"
unfolding eq by (auto simp: power_int_mult_distrib power_int_add mult_ac)
finally have S1': "((λn. (a * b) powi (n * (n - 1) div 2) * a powi n) has_sum S1) {1..}" .
have S2: "((λn. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum S2) {..-1}"
unfolding S2_def by (rule has_sum_infsum) rule
also have "?this ⟷ ((λn. b powi (n*(n+1) div 2) * a powi (n*(n-1) div 2)) has_sum S2) {1..}"
by (rule has_sum_reindex_bij_witness[of _ uminus uminus]) (auto simp: algebra_simps)
also have "(λn. b powi (n*(n+1) div 2) * a powi (n*(n-1) div 2)) =
(λn. (a*b) powi (n*(n-1) div 2) * b powi n)"
unfolding eq by (auto simp: power_int_mult_distrib power_int_add mult_ac)
finally have S2': "((λn. (a * b) powi (n * (n - 1) div 2) * b powi n) has_sum S2) {1..}" .
have "((λn. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum (ramanujan_theta a b - 1)) (UNIV-{0})"
using 1 by (rule has_sum_Diff) (auto simp: has_sum_finite_iff)
also have "UNIV - {0::int} = {1..} ∪ {..-1}"
by auto
finally have "((λn. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum
(ramanujan_theta a b - 1)) ({1..} ∪ {..-1})" .
moreover have "((λn. a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) has_sum
(S1 + S2)) ({1..} ∪ {..-1})"
by (intro has_sum_Un_disjoint S1 S2) auto
ultimately have "ramanujan_theta a b - 1 = S1 + S2"
using has_sum_unique by blast
moreover have "((λn. (a * b) powi (n * (n - 1) div 2) * (a powi n + b powi n)) has_sum (S1 + S2)) {1..}"
using has_sum_add[OF S1' S2'] by (simp add: algebra_simps)
ultimately show "((λn. (a*b) powi (n*(n-1) div 2) * (a powi n + b powi n))
has_sum (ramanujan_theta a b - 1)) {1..}"
by simp
qed
lemma ramanujan_theta_of_real:
"ramanujan_theta (of_real a) (of_real b) = of_real (ramanujan_theta a b)"
proof (cases "norm (a*b) < 1")
case ab: True
have "((λn. of_real (a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) :: 'a) has_sum
of_real (ramanujan_theta a b)) UNIV"
by (intro has_sum_of_real has_sum_ramanujan_theta) (use ab in auto)
also have "(λn. of_real (a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2)) :: 'a) =
(λn. of_real a powi (n*(n+1) div 2) * of_real b powi (n*(n-1) div 2))" by simp
finally have "((λn. of_real a powi (n * (n + 1) div 2) * of_real b powi (n * (n - 1) div 2)) has_sum
(of_real (ramanujan_theta a b) :: 'a)) UNIV" .
moreover have "((λn. of_real a powi (n*(n+1) div 2) * of_real b powi (n*(n-1) div 2) :: 'a) has_sum
ramanujan_theta (of_real a) (of_real b)) UNIV"
by (rule has_sum_ramanujan_theta) (use ab in ‹auto simp: norm_mult›)
ultimately show ?thesis
using has_sum_unique by blast
qed (auto simp: ramanujan_theta_def norm_mult abs_mult)
lemma ramanujan_theta_cnj:
"ramanujan_theta (cnj a) (cnj b) = cnj (ramanujan_theta a b)"
proof (cases "norm (a*b) < 1")
case ab: True
have "((λn. cnj (a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2))) has_sum cnj (ramanujan_theta a b)) UNIV"
unfolding has_sum_cnj_iff by (intro has_sum_ramanujan_theta) (use ab in auto)
also have "(λn. cnj (a powi (n*(n+1) div 2) * b powi (n*(n-1) div 2))) =
(λn. cnj a powi (n*(n+1) div 2) * cnj b powi (n*(n-1) div 2))"
by simp
finally have "((λn. cnj a powi (n*(n+1) div 2) * cnj b powi (n*(n-1) div 2)) has_sum
cnj (ramanujan_theta a b)) UNIV" .
moreover have "((λn. cnj a powi (n*(n+1) div 2) * cnj b powi (n*(n-1) div 2)) has_sum
ramanujan_theta (cnj a) (cnj b)) UNIV"
by (rule has_sum_ramanujan_theta) (use ab in ‹auto simp: norm_mult›)
ultimately show ?thesis
using has_sum_unique by blast
qed (auto simp: ramanujan_theta_def norm_mult)
lemma ramanujan_theta_holomorphic [holomorphic_intros]:
assumes "f holomorphic_on A" "g holomorphic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z * g z) < 1" "open A"
shows "(λz. ramanujan_theta (f z) (g z)) holomorphic_on A"
proof -
have "(λz. ramanujan_theta (f z) (g z)) analytic_on {z}" if "z ∈ A" for z
proof -
obtain r where r: "r > 0" "cball z r ⊆ A"
using ‹open A› ‹z ∈ A› open_contains_cball_eq by blast
define h where "h = (λX (w,q). ∑n∈X. w powi (n*(n+1) div 2) * q powi (n*(n-1) div 2) :: complex)"
define H where "H = (λ(w,q). ∑⇩∞n. w powi (n*(n+1) div 2) * q powi (n*(n-1) div 2) :: complex)"
have lim: "uniform_limit (cball z r)
(λX x. h X (f x, g x)) (λx. H (f x, g x)) (finite_subsets_at_top UNIV)"
unfolding h_def H_def
proof (rule uniform_limit_compose'[OF uniform_limit_ramanujan_theta])
show "compact ((λx. (f x, g x)) ` cball z r)" using r
by (intro compact_continuous_image)
(auto intro!: continuous_intros holomorphic_on_imp_continuous_on
assms(1,2)[THEN holomorphic_on_subset])
qed (use r assms(3,4) in auto)
have "(λx. H (f x, g x)) holomorphic_on ball z r"
by (rule holomorphic_uniform_limit[OF _ lim])
(use r in ‹auto intro!: always_eventually continuous_intros holomorphic_intros
holomorphic_on_imp_continuous_on
assms(1,2)[THEN holomorphic_on_subset] assms(3)
simp: h_def zero_le_mult_iff›)
also have "?this ⟷ (λx. ramanujan_theta (f x) (g x)) holomorphic_on ball z r"
proof (rule holomorphic_cong)
fix w assume "w ∈ ball z r"
hence "w ∈ A"
using r by auto
hence "norm (f w * g w) < 1"
using assms(3) by auto
thus "H (f w, g w) = ramanujan_theta (f w) (g w)"
by (auto simp: H_def ramanujan_theta_def)
qed auto
finally show ?thesis
using ‹r > 0› analytic_at_ball by blast
qed
hence "(λz. ramanujan_theta (f z) (g z)) analytic_on A"
using analytic_on_analytic_at by blast
thus ?thesis
using analytic_imp_holomorphic by auto
qed
lemma ramanujan_theta_analytic [analytic_intros]:
assumes "f analytic_on A" "g analytic_on A" "⋀z. z ∈ A ⟹ norm (f z * g z) < 1"
shows "(λz. ramanujan_theta (f z) (g z)) analytic_on A"
proof -
from assms(1) obtain B1 where B1: "open B1" "A ⊆ B1" "f holomorphic_on B1"
using analytic_on_holomorphic by metis
from assms(2) obtain B2 where B2: "open B2" "A ⊆ B2" "g holomorphic_on B2"
using analytic_on_holomorphic by metis
note [holomorphic_intros] = holomorphic_on_subset[OF B1(3)] holomorphic_on_subset[OF B2(3)]
define B3 where "B3 = B1 ∩ B2 ∩ (λz. f z * g z) -` ball 0 1"
have "open B3" using B1 B2 unfolding B3_def
by (intro continuous_open_preimage holomorphic_on_imp_continuous_on
holomorphic_intros open_halfspace_Im_gt) auto
hence B3: "open B3" "B3 ⊆ B1" "B3 ⊆ B2" "⋀z. z ∈ B3 ⟹ f z * g z ∈ ball 0 1"
unfolding B3_def by auto
have "(λz. ramanujan_theta (f z) (g z)) holomorphic_on B3"
using B3 by (auto intro!: holomorphic_intros)
moreover have "A ⊆ B3"
using assms(3) B1 B2 by (auto simp: B3_def)
ultimately show ?thesis
using ‹open B3› analytic_on_holomorphic by metis
qed
lemma tendsto_ramanujan_theta [tendsto_intros]:
fixes f g :: "'a ⇒ 'b :: {real_normed_field, banach, heine_borel}"
assumes "(f ⤏ a) F" "(g ⤏ b) F" "norm (a * b) < 1"
shows "((λz. ramanujan_theta (f z) (g z)) ⤏ ramanujan_theta a b) F"
proof -
have "isCont (λ(w,q). ramanujan_theta w q) z" if z: "norm (fst z * snd z) < 1" for z :: "'b × 'b"
proof -
have "z ∈ (λz. (fst z * snd z)) -` ball 0 1"
using z by auto
moreover have "open ((λz. (fst z * snd z :: 'b)) -` ball 0 1)"
by (intro open_vimage continuous_intros) auto
ultimately obtain r where r: "r > 0" "cball z r ⊆ (λz. (fst z * snd z)) -` ball 0 1"
by (meson open_contains_cball)
have "continuous_on (cball z r)
(λ(a, b). ∑⇩∞n. a powi (n * (n + 1) div 2) * b powi (n * (n - 1) div 2))"
proof (rule uniform_limit_theorem)
show "uniform_limit (cball z r)
(λX (a, b). ∑n∈X. a powi (n * (n + 1) div 2) * b powi (n * (n - 1) div 2))
(λ(a, b). ∑⇩∞n. a powi (n * (n + 1) div 2) * b powi (n * (n - 1) div 2))
(finite_subsets_at_top UNIV)"
by (rule uniform_limit_ramanujan_theta) (use r in auto)
qed (auto intro!: always_eventually continuous_intros
simp: case_prod_unfold dist_norm zero_le_mult_iff)
also have "?this ⟷ continuous_on (cball z r) (λ(a,b). ramanujan_theta a b)"
by (intro continuous_on_cong) (use r in ‹auto simp: ramanujan_theta_def›)
finally have "continuous_on (ball z r) (λ(a,b). ramanujan_theta a b)"
by (rule continuous_on_subset) auto
thus ?thesis
using ‹r > 0› centre_in_ball continuous_on_interior interior_ball by blast
qed
from this[of "(a, b)"] have isCont: "isCont (λ(w,q). ramanujan_theta w q) (a, b)"
using assms by simp
have lim: "((λx. (f x, g x)) ⤏ (a, b)) F"
using assms by (intro tendsto_intros)
show ?thesis
using isCont_tendsto_compose[OF isCont lim] by simp
qed
lemma continuous_on_ramanujan_theta [continuous_intros]:
fixes f g :: "'a :: topological_space ⇒ 'b :: {real_normed_field, banach, heine_borel}"
assumes "continuous_on A f" "continuous_on A g" "⋀z. z ∈ A ⟹ norm (f z * g z) < 1"
shows "continuous_on A (λz. ramanujan_theta (f z) (g z))"
proof -
have *: "continuous_on {z. norm (fst z * snd z) < 1} (λ(a,b). ramanujan_theta a b :: 'b)"
unfolding continuous_on by (auto intro!: tendsto_eq_intros simp: case_prod_unfold)
have "continuous_on A ((λ(x,y). ramanujan_theta x y) ∘ (λx. (f x, g x)))"
by (intro continuous_on_compose continuous_on_subset[OF *] continuous_intros)
(use assms in auto)
thus ?thesis
by (simp add: o_def)
qed
lemma continuous_ramanujan_theta [continuous_intros]:
fixes f g :: "'a :: t2_space ⇒ 'b :: {real_normed_field, banach, heine_borel}"
assumes "continuous F f" "continuous F g" "norm (f (netlimit F) * g (netlimit F)) < 1"
shows "continuous F (λz. ramanujan_theta (f z) (g z))"
unfolding continuous_def
using assms by (auto intro!: tendsto_eq_intros simp: continuous_def)
lemma ramanujan_theta_1_left:
"ramanujan_theta 1 a = 2 * ramanujan_theta a (a ^ 3)"
proof (cases "a ≠ 0 ∧ norm a < 1")
case False
hence "a = 0 ∨ norm a ≥ 1"
by auto
thus ?thesis
proof
assume "norm a ≥ 1"
thus ?thesis
by (auto simp: ramanujan_theta_def norm_power power_less_one_iff
simp flip: power_Suc2 power_Suc)
qed auto
next
case a: True
hence [simp]: "a ≠ 0"
by auto
define S1 where "S1 = (∑⇩∞n∈{0..}. a powi (n*(n+1) div 2))"
define S2 where "S2 = (∑⇩∞n∈{..-1}. a powi (n*(n+1) div 2))"
have 1: "((λn. a powi (n*(n+1) div 2)) has_sum ramanujan_theta 1 a) UNIV"
using has_sum_ramanujan_theta[of a 1] a by (simp add: ramanujan_theta_commute)
have summable: "(λn. a powi (n*(n+1) div 2)) summable_on A" for A
by (rule summable_on_subset_banach, rule has_sum_imp_summable[OF 1]) auto
have S1: "((λn. a powi (n*(n+1) div 2)) has_sum S1) {0..}"
unfolding S1_def by (rule has_sum_infsum, rule summable)
also have "?this ⟷ ((λn. a powi (n*(n+1) div 2)) has_sum S1) {..-1}"
by (intro has_sum_reindex_bij_witness[of _ "λn. -n-1" "λn. -n-1"]) (auto simp: algebra_simps)
finally have S1': "((λn. a powi (n*(n+1) div 2)) has_sum S1) {..-1}" .
have "((λn. a powi (n*(n+1) div 2)) has_sum (S1 + S1)) ({..-1} ∪ {0..})"
by (intro has_sum_Un_disjoint S1 S1') auto
also have "{..-1} ∪ {0::int..} = UNIV"
by auto
finally have "((λn. a powi (n * (n + 1) div 2)) has_sum (2*S1)) UNIV"
by simp
with 1 have "ramanujan_theta 1 a = 2 * S1"
using has_sum_unique by blast
define S2 where "S2 = (∑⇩∞n | n ≥ 0 ∧ even n. a powi (n*(n+1) div 2))"
define S3 where "S3 = (∑⇩∞n | n ≥ 0 ∧ odd n. a powi (n*(n+1) div 2))"
have "((λn. a powi (n*(n+1) div 2)) has_sum (S2 + S3)) ({n. n ≥ 0 ∧ even n} ∪ {n. n ≥ 0 ∧ odd n})"
unfolding S2_def S3_def by (intro has_sum_Un_disjoint has_sum_infsum summable) auto
also have "{n. n ≥ 0 ∧ even n} ∪ {n. n ≥ 0 ∧ odd n} = {0::int..}"
by auto
finally have "S1 = S2 + S3"
using S1 has_sum_unique by blast
have "((λn. a powi (n*(n+1) div 2)) has_sum S2) {n. n ≥ 0 ∧ even n}"
unfolding S2_def by (intro has_sum_Un_disjoint has_sum_infsum summable)
also have "?this ⟷ ((λn. a powi (n*(2*n+1))) has_sum S2) {0..}"
by (intro has_sum_reindex_bij_witness[of _ "λn. 2*n" "λn. n div 2"]) auto
also have "(λn::int. n*(2*n+1)) = (λn. (n*(n-1) div 2) + 3*((n*(n+1)) div 2))"
proof
fix n :: int
show "n*(2*n+1) = (n*(n-1) div 2) + 3*((n*(n+1)) div 2)"
by (cases "even n") (auto elim!: evenE oddE simp: algebra_simps)
qed
also have "(λn. a powi … n) = (λn. a powi (n*(n-1) div 2) * (a ^ 3) powi (n*(n+1) div 2))"
by (simp add: power_int_add power_int_power)
finally have S2: "((λn. a powi (n*(n-1) div 2) * (a ^ 3) powi (n*(n+1) div 2)) has_sum S2) {0..}" .
have "((λn. a powi (n*(n+1) div 2)) has_sum S3) {n. n ≥ 0 ∧ odd n}"
unfolding S3_def by (intro has_sum_Un_disjoint has_sum_infsum summable)
also have "?this ⟷ ((λn. a powi (n*(2*n-1))) has_sum S3) {1..}"
by (intro has_sum_reindex_bij_witness[of _ "λn. 2*n-1" "λn. (n+1) div 2"])
(auto elim!: oddE simp: algebra_simps)
also have "(λn::int. n*(2*n-1)) = (λn. (n*(n+1) div 2) + 3*(n*(n-1) div 2))"
proof
fix n :: int
show "n*(2*n-1) = (n*(n+1) div 2) + 3*(n*(n-1) div 2)"
by (cases "even n") (auto elim!: evenE oddE simp: algebra_simps)
qed
also have "(λn. a powi … n) = (λn. a powi (n*(n+1) div 2) * (a^3) powi (n*(n-1) div 2))"
by (simp add: power_int_add power_int_power)
finally have "((λn. a powi (n*(n+1) div 2) * (a^3) powi (n*(n-1) div 2)) has_sum S3) {1..}" .
also have "?this ⟷ ((λn. a powi (n*(n-1) div 2) * (a^3) powi (n*(n+1) div 2)) has_sum S3) {..-1}"
by (intro has_sum_reindex_bij_witness[of _ "λn. -n" "λn. -n"]) (auto simp: algebra_simps)
finally have S3: "((λn. a powi (n*(n-1) div 2) * (a^3) powi (n*(n+1) div 2)) has_sum S3) {..-1}" .
have "((λn. a powi (n*(n-1) div 2) * (a^3) powi (n*(n+1) div 2)) has_sum (S2 + S3)) ({0..} ∪ {..-1})"
by (intro has_sum_Un_disjoint S2 S3) auto
also have "{0::int..} ∪ {..-1} = UNIV"
by auto
finally have "((λn. (a^3) powi (n*(n+1) div 2) * a powi (n*(n-1) div 2)) has_sum S2 + S3) UNIV"
by (simp add: mult.commute)
moreover have "((λn. (a^3) powi (n*(n+1) div 2) * a powi (n*(n-1) div 2)) has_sum
ramanujan_theta (a^3) a) UNIV"
by (intro has_sum_ramanujan_theta)
(use a in ‹auto simp: norm_power power_less_one_iff simp flip: power_Suc2›)
ultimately have "ramanujan_theta (a^3) a = S2 + S3"
using has_sum_unique by blast
also have "S2 + S3 = S1"
by (rule sym) fact
also have "S1 = ramanujan_theta 1 a / 2"
using ‹ramanujan_theta 1 a = 2 * S1› by (simp add: field_simps)
finally show ?thesis
by (simp add: field_simps ramanujan_theta_commute)
qed
lemma ramanujan_theta_1_right: "ramanujan_theta a 1 = 2 * ramanujan_theta a (a ^ 3)"
by (subst ramanujan_theta_commute, rule ramanujan_theta_1_left)
lemma ramanujan_theta_neg1_left [simp]: "ramanujan_theta (-1) a = 0"
proof (cases "a ≠ 0 ∧ norm a < 1")
case False
hence "a = 0 ∨ norm a ≥ 1"
by auto
thus ?thesis
proof
assume "norm a ≥ 1"
thus ?thesis
by (auto simp: ramanujan_theta_def norm_power power_less_one_iff
simp flip: power_Suc2 power_Suc)
qed auto
next
case a: True
hence [simp]: "a ≠ 0"
by auto
define S1 where "S1 = (∑⇩∞n∈{1..}. (-1) powi (n*(n+1) div 2) * a powi (n*(n-1) div 2))"
define S2 where "S2 = (∑⇩∞n∈{..-2}. (-1) powi (n*(n+1) div 2) * a powi (n*(n-1) div 2))"
have sum: "((λn. (-1) powi (n*(n+1) div 2) * a powi (n*(n-1) div 2)) has_sum ramanujan_theta (-1) a) UNIV"
using has_sum_ramanujan_theta[of "-1" a] a by simp
have summable: "(λn. (-1) powi (n*(n+1) div 2) * a powi (n*(n-1) div 2)) summable_on A" for A
by (rule summable_on_subset_banach, rule has_sum_imp_summable[OF sum]) auto
have S1: "((λn. (-1) powi (n*(n+1) div 2) * a powi (n*(n-1) div 2)) has_sum S1) {1..}"
unfolding S1_def by (rule has_sum_infsum, rule summable)
also have "?this ⟷ ((λn. (-1) powi ((n-2)*(n-1) div 2) * a powi (n*(n-1) div 2)) has_sum S1) {..0}"
by (intro has_sum_reindex_bij_witness[of _ "λn. -n+1" "λn. -n+1"]) (auto simp: algebra_simps)
also have "(λn. (n-2)*(n-1) div 2) = (λn::int. n*(n+1) div 2 - 2 * n + 1)"
by (auto simp: algebra_simps)
also have "(λn. (-1) powi (n*(n+1) div 2 - 2*n + 1)) =
(λn. - ((-1) powi (n*(n+1) div 2) :: 'a))"
by (simp add: power_int_add power_int_diff)
finally have S1': "((λn. ((-1) powi (n*(n+1) div 2) * a powi (n*(n-1) div 2))) has_sum (-S1)) {..0}"
by (simp add: has_sum_uminus)
have "((λn. ((-1) powi (n*(n+1) div 2) * a powi (n*(n-1) div 2))) has_sum (-S1 + S1)) ({..0} ∪ {1..})"
by (intro has_sum_Un_disjoint S1 S1') auto
also have "{..0} ∪ {1::int..} = UNIV"
by auto
also have "-S1 + S1 = 0"
by simp
finally show ?thesis
using sum has_sum_unique by blast
qed
lemma ramanujan_theta_neg1_right [simp]: "ramanujan_theta a (-1) = 0"
by (subst ramanujan_theta_commute) auto
lemma ramanujan_theta_mult_power_int:
assumes [simp]: "a ≠ 0" "b ≠ 0"
shows "ramanujan_theta a b =
a powi (m*(m+1) div 2) * b powi (m*(m-1) div 2) *
ramanujan_theta (a * (a*b) powi m) (b * (a*b) powi (-m))"
proof (cases "norm (a * b) < 1")
case False
thus ?thesis
by (simp add: ramanujan_theta_def field_simps power_int_minus)
next
case True
hence [simp]: "a ≠ 0" "b ≠ 0"
by auto
define e1 e2 where "e1 = (m*(m+1) div 2)" and "e2 = (m*(m-1) div 2)"
define a' b' where "a' = a*(a*b) powi m" and "b' = b*(a*b) powi -m"
have eq: "n * (n + 1) div 2 = n * (n - 1) div 2 + n" for n :: int
by (auto simp: algebra_simps)
have "((λn. a powi e1 * b powi e2 * (a' powi (n*(n+1) div 2) * b' powi (n*(n-1) div 2)))
has_sum (a powi e1 * b powi e2 * ramanujan_theta a' b')) UNIV"
by (intro has_sum_cmult_right has_sum_ramanujan_theta)
(use True in ‹auto simp: a'_def b'_def power_int_minus field_simps›)
also have "(λn. a powi e1 * b powi e2 * (a' powi (n*(n+1) div 2) * b' powi (n*(n-1) div 2))) =
(λn. a powi ((n+m)*(n+m+1) div 2) * b powi ((n+m)*(n+m-1) div 2))" (is "?lhs = ?rhs")
proof
fix n :: int
have "a powi e1 * b powi e2 * (a' powi (n*(n+1) div 2) * b' powi (n*(n-1) div 2)) =
a powi (e1 + (n*(n+1) div 2) + m*(n*(n+1) div 2) - m*(n*(n-1) div 2)) *
b powi (e2 + (n*(n-1) div 2) + m*(n*(n+1) div 2) - m*(n*(n-1) div 2))"
unfolding a'_def b'_def
by (simp add: a'_def b'_def power_int_mult_distrib power_int_add power_int_diff power_int_minus
power_int_divide_distrib field_simps flip: power_int_mult)
also have "e1 + (n*(n+1) div 2) + m*(n*(n+1) div 2) - m*(n*(n-1) div 2) =
(m * (m + 1) + 2 * m * n) div 2 + (n*(n+1) div 2)"
unfolding eq by (simp add: algebra_simps e1_def)
also have "… = (m * (m + 1) + 2 * m * n + n * (n + 1)) div 2"
by (rule div_add [symmetric]) auto
also have "(m * (m + 1) + 2 * m * n + n * (n + 1)) = (n+m)*(n+m+1)"
by Groebner_Basis.algebra
also have "e2 + (n*(n-1) div 2) + m*(n*(n+1) div 2) - m*(n*(n-1) div 2) =
(m*(m-1) + 2*m*n) div 2 + (n*(n-1) div 2)"
unfolding eq by (simp add: algebra_simps e2_def)
also have "… = (m*(m-1) + 2*m*n + n*(n-1)) div 2"
by (rule div_add [symmetric]) auto
also have "m*(m-1) + 2*m*n + n*(n-1) = (n+m)*(n+m-1)"
by Groebner_Basis.algebra
finally show "?lhs n = ?rhs n" .
qed
also have "((λn. a powi ((n+m)*(n+m+1) div 2) * b powi ((n+m)*(n+m-1) div 2)) has_sum
(a powi e1 * b powi e2 * ramanujan_theta a' b')) UNIV ⟷
((λn. a powi (n * (n + 1) div 2) * b powi (n * (n - 1) div 2)) has_sum
(a powi e1 * b powi e2 * ramanujan_theta a' b')) UNIV"
by (intro has_sum_reindex_bij_witness[of _ "λn. n - m" "λn. n + m"]) auto
finally have … .
moreover have "((λn. a powi (n * (n + 1) div 2) * b powi (n * (n - 1) div 2)) has_sum
ramanujan_theta a b) UNIV"
by (rule has_sum_ramanujan_theta) (use True in auto)
ultimately have "a powi e1 * b powi e2 * ramanujan_theta a' b' = ramanujan_theta a b"
using has_sum_unique by blast
thus ?thesis
by (simp add: e1_def e2_def a'_def b'_def)
qed
lemma ramanujan_theta_mult:
assumes [simp]: "a ≠ 0" "b ≠ 0"
shows "ramanujan_theta a b = a * ramanujan_theta (a⇧2 * b) (1 / a)"
using ramanujan_theta_mult_power_int[of a b 1]
by (simp add: eval_nat_numeral field_simps)
lemma ramanujan_theta_mult':
assumes [simp]: "a ≠ 0" "b ≠ 0"
shows "ramanujan_theta a b = b * ramanujan_theta (1 / b) (a * b⇧2)"
using ramanujan_theta_mult[of b a] by (simp add: ramanujan_theta_commute mult.commute)
subsection ‹The Jacobi theta function in terms of the nome›
text ‹
Based on Ramanujan's ‹θ› function, we introduce a version of Jacobi's ‹θ› function:
\[\vartheta(w,q) = \sum_{n=-\infty}^\infty w^n q^{n^2}\hskip1.5em (\text{for}\ |q|<1, w\neq 0)\]
Both parameters are still in terms of the nome rather than the complex plane.
This has some advantages, and we can easily derive the other versions from it later.
›
definition jacobi_theta_nome :: "'a :: {real_normed_field,banach} ⇒ 'a ⇒ 'a" where
"jacobi_theta_nome w q = (if w = 0 then 0 else ramanujan_theta (q*w) (q/w))"
lemma jacobi_theta_nome_0_left [simp]: "jacobi_theta_nome 0 q = 0"
by (simp add: jacobi_theta_nome_def)
lemma jacobi_theta_nome_outside [simp]:
assumes "norm q ≥ 1"
shows "jacobi_theta_nome w q = 0"
proof (cases "w = 0")
case False
thus ?thesis using assms
by (simp add: jacobi_theta_nome_def norm_mult ramanujan_theta_def power_less_one_iff norm_power
flip: power2_eq_square)
qed auto
lemma has_sum_jacobi_theta_nome:
assumes "norm q < 1" and [simp]: "w ≠ 0"
shows "((λn. w powi n * q powi (n ^ 2)) has_sum jacobi_theta_nome w q) UNIV"
proof (cases "q = 0")
case True
have "((λ_::int. 1) has_sum jacobi_theta_nome w q) {0}"
by (intro has_sum_finiteI) (use True in ‹auto simp: jacobi_theta_nome_def›)
also have "?this ⟷ ?thesis"
using True by (intro has_sum_cong_neutral) auto
finally show ?thesis .
next
case False
hence [simp]: "q ≠ 0" "w ≠ 0"
by auto
have "((λn. (q*w) powi (n*(n+1) div 2) * (q/w) powi (n*(n-1) div 2)) has_sum ramanujan_theta (q*w) (q/w)) UNIV"
by (rule has_sum_ramanujan_theta)
(use assms in ‹auto simp: norm_power power_less_one_iff simp flip: power2_eq_square›)
also have "(λn. (q*w) powi (n*(n+1) div 2) * (q/w) powi (n*(n-1) div 2)) =
(λn. w powi ((n*(n+1) div 2) - (n*(n-1) div 2)) * q powi ((n*(n+1) div 2) + (n*(n-1) div 2)))"
by (simp add: power_int_mult_distrib power_int_divide_distrib power_int_add power_int_diff field_simps)
also have "(λn::int. (n*(n+1) div 2) - (n*(n-1) div 2)) = (λn. n)"
by (auto simp: fun_eq_iff algebra_simps)
also have "(λn::int. (n*(n+1) div 2) + (n*(n-1) div 2)) = (λn. n ^ 2)"
by (auto simp: fun_eq_iff algebra_simps power2_eq_square simp flip: div_add)
finally show ?thesis
by (simp add: jacobi_theta_nome_def)
qed
lemma jacobi_theta_nome_same:
"q ≠ 0 ⟹ jacobi_theta_nome q q = 2 * jacobi_theta_nome (1 / q^2) (q^4)"
by (simp add: jacobi_theta_nome_def ramanujan_theta_1_right
flip: power_diff power2_eq_square)
lemma jacobi_theta_nome_minus_same: "q ≠ 0 ⟹ jacobi_theta_nome (-q) q = 0"
by (simp add: jacobi_theta_nome_def)
lemma jacobi_theta_nome_minus_same': "q ≠ 0 ⟹ jacobi_theta_nome q (-q) = 0"
by (simp add: jacobi_theta_nome_def)
lemma jacobi_theta_nome_0_right [simp]: "w ≠ 0 ⟹ jacobi_theta_nome w 0 = 1"
by (simp add: jacobi_theta_nome_def)
lemma jacobi_theta_nome_of_real:
"jacobi_theta_nome (of_real w) (of_real q) = of_real (jacobi_theta_nome w q)"
by (simp add: jacobi_theta_nome_def flip: ramanujan_theta_of_real)
lemma jacobi_theta_nome_cnj:
"jacobi_theta_nome (cnj w) (cnj q) = cnj (jacobi_theta_nome w q)"
by (simp add: jacobi_theta_nome_def flip: ramanujan_theta_cnj)
lemma jacobi_theta_nome_minus_left:
"jacobi_theta_nome (-w) q = jacobi_theta_nome w (-q)"
by (simp add: jacobi_theta_nome_def)
lemma jacobi_theta_nome_quasiperiod':
assumes [simp]: "w ≠ 0" "q ≠ 0"
shows "w * q * jacobi_theta_nome (q⇧2 * w) q = jacobi_theta_nome w q"
proof -
have "jacobi_theta_nome w q = ramanujan_theta (q * w) (q / w)"
by (simp add: jacobi_theta_nome_def)
also have "… = w * q * ramanujan_theta (q ^ 3 * w) (1 / (q * w))"
using ramanujan_theta_mult[of "q*w" "q/w"]
by (simp add: field_simps eval_nat_numeral)
also have "ramanujan_theta (q ^ 3 * w) (1 / (q * w)) = jacobi_theta_nome (q⇧2 * w) q"
by (simp add: jacobi_theta_nome_def eval_nat_numeral field_simps)
finally show ?thesis ..
qed
lemma jacobi_theta_nome_ii_left: "jacobi_theta_nome 𝗂 q = jacobi_theta_nome (-1) (q^4)"
proof (cases "norm q < 1")
case q: True
define S where "S = jacobi_theta_nome 𝗂 q"
have sum1: "((λn. 𝗂 powi n * q powi n⇧2) has_sum S) UNIV"
unfolding S_def by (rule has_sum_jacobi_theta_nome) (use q in auto)
also have "?this ⟷ ((λn. 𝗂 powi (-n) * q powi (-n)⇧2) has_sum S) UNIV"
by (rule has_sum_reindex_bij_witness[of _ uminus uminus]) auto
finally have sum2: "((λn. (-𝗂) powi n * q powi n⇧2) has_sum S) UNIV"
by (simp add: power_int_minus flip: power_int_inverse)
have "((λn. (𝗂 powi n + (-𝗂) powi n) * q powi n⇧2) has_sum (S + S)) UNIV"
unfolding ring_distribs by (intro has_sum_add sum1 sum2)
also have "?this ⟷ ((λn. 2 * 𝗂 powi n * q powi n⇧2) has_sum (S + S)) {n. even n}"
by (intro has_sum_cong_neutral) auto
also have "… ⟷ ((λn. 2 * (𝗂 powi (2*n) * q powi (2*n)⇧2)) has_sum (S + S)) UNIV"
by (intro has_sum_reindex_bij_witness[of _ "λn. 2*n" "λn. n div 2"]) auto
finally have sum3: "((λn. 2 * (𝗂 powi (2*n) * (q^4) powi n ^ 2)) has_sum (2 * S)) UNIV"
by (simp flip: mult_2[of S] power_int_mult add: power_int_mult)
have "((λn. 𝗂 powi (2*n) * (q^4) powi n ^ 2) has_sum S) UNIV"
using has_sum_cmult_right[OF sum3, of "1/2"] by simp
also have "(λn. 𝗂 powi (2*n)) = (λn. (-1) powi n)"
by (simp add: power_int_mult)
finally have "((λn. (-1) powi n * (q^4) powi n⇧2) has_sum S) UNIV" .
moreover have "((λn. (-1) powi n * (q^4) powi n⇧2) has_sum jacobi_theta_nome (-1) (q^4)) UNIV"
by (rule has_sum_jacobi_theta_nome) (use q in ‹auto simp: norm_power power_less_one_iff›)
ultimately show ?thesis
using has_sum_unique unfolding S_def by blast
qed (auto simp: norm_power power_less_one_iff)
lemma jacobi_theta_nome_quasiperiod:
assumes [simp]: "w ≠ 0" "q ≠ 0"
shows "jacobi_theta_nome (q⇧2 * w) q = jacobi_theta_nome w q / (w * q)"
using jacobi_theta_nome_quasiperiod'[of w q] by (simp add: field_simps)
lemma jacobi_theta_nome_holomorphic [holomorphic_intros]:
assumes "f holomorphic_on A" "g holomorphic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z) ≠ 0" "⋀z. z ∈ A ⟹ norm (g z) < 1" "open A"
shows "(λz. jacobi_theta_nome (f z) (g z)) holomorphic_on A"
proof -
have "(λz. ramanujan_theta (g z * f z) (g z / f z)) holomorphic_on A"
by (intro holomorphic_intros)
(use assms in ‹auto simp: norm_power power_less_one_iff simp flip: power2_eq_square›)
also have "?this ⟷ ?thesis"
by (intro holomorphic_cong) (use assms(3,4) in ‹auto simp: jacobi_theta_nome_def›)
finally show ?thesis .
qed
lemma jacobi_theta_nome_analytic [analytic_intros]:
assumes "f analytic_on A" "g analytic_on A"
assumes "⋀z. z ∈ A ⟹ f z ≠ 0" "⋀z. z ∈ A ⟹ norm (g z) < 1"
shows "(λz. jacobi_theta_nome (f z) (g z)) analytic_on A"
proof -
from assms(1) obtain B1 where B1: "open B1" "A ⊆ B1" "f holomorphic_on B1"
using analytic_on_holomorphic by metis
from assms(2) obtain B2 where B2: "open B2" "A ⊆ B2" "g holomorphic_on B2"
using analytic_on_holomorphic by metis
note [holomorphic_intros] = holomorphic_on_subset[OF B1(3)] holomorphic_on_subset[OF B2(3)]
define B3 where "B3 = B1 ∩ B2 ∩ (λz. (f z, g z)) -` ((-{0}) × ball 0 1)"
have "open B3" using B1 B2 unfolding B3_def
by (intro continuous_open_preimage holomorphic_on_imp_continuous_on
holomorphic_intros continuous_intros open_halfspace_Im_gt) (auto intro!: open_Times)
hence B3: "open B3" "B3 ⊆ B1" "B3 ⊆ B2" "⋀z. z ∈ B3 ⟹ f z ≠ 0 ∧ g z ∈ ball 0 1"
unfolding B3_def by auto
have "(λz. jacobi_theta_nome (f z) (g z)) holomorphic_on B3"
using B3 by (auto intro!: holomorphic_intros)
moreover have "A ⊆ B3"
using assms(3,4) B1 B2 by (auto simp: B3_def)
ultimately show ?thesis
using ‹open B3› analytic_on_holomorphic by metis
qed
lemma tendsto_jacobi_theta_nome [tendsto_intros]:
fixes f g :: "'a ⇒ 'b :: {real_normed_field, banach, heine_borel}"
assumes "(f ⤏ w) F" "(g ⤏ q) F" "w ≠ 0" "norm q < 1"
shows "((λz. jacobi_theta_nome (f z) (g z)) ⤏ jacobi_theta_nome w q) F"
proof -
have "((λz. jacobi_theta_nome (f z) (g z)) ⤏ ramanujan_theta (q * w) (q / w)) F"
proof (rule Lim_transform_eventually)
show "((λz. ramanujan_theta (g z * f z) (g z / f z)) ⤏
ramanujan_theta (q * w) (q / w)) F"
by (intro tendsto_intros assms)
(use assms(3,4) in ‹simp_all flip: power2_eq_square add: norm_power power_less_one_iff›)
next
have "eventually (λx. f x ∈ -{0}) F"
by (rule topological_tendstoD[OF assms(1)]) (use assms(3) in auto)
thus "eventually (λz. ramanujan_theta (g z * f z) (g z / f z) = jacobi_theta_nome (f z) (g z)) F"
by eventually_elim (simp add: jacobi_theta_nome_def)
qed
thus ?thesis
using assms(3) by (simp add: jacobi_theta_nome_def)
qed
lemma continuous_on_jacobi_theta_nome [continuous_intros]:
fixes f g :: "'a :: topological_space ⇒ 'b :: {real_normed_field, banach, heine_borel}"
assumes "continuous_on A f" "continuous_on A g"
assumes "⋀z. z ∈ A ⟹ f z ≠ 0" "⋀z. z ∈ A ⟹ norm (g z) < 1"
shows "continuous_on A (λz. jacobi_theta_nome (f z) (g z))"
proof -
have *: "continuous_on {z. fst z ≠ 0 ∧ norm (snd z) < 1} (λ(a,b). jacobi_theta_nome a b :: 'b)"
unfolding continuous_on by (auto intro!: tendsto_eq_intros simp: case_prod_unfold)
have "continuous_on A ((λ(x,y). jacobi_theta_nome x y) ∘ (λx. (f x, g x)))"
by (intro continuous_on_compose continuous_on_subset[OF *] continuous_intros)
(use assms in auto)
thus ?thesis
by (simp add: o_def)
qed
lemma continuous_jacobi_theta_nome [continuous_intros]:
fixes f g :: "'a :: t2_space ⇒ 'b :: {real_normed_field, banach, heine_borel}"
assumes "continuous F f" "continuous F g" "f (netlimit F) ≠ 0" "norm (g (netlimit F)) < 1"
shows "continuous F (λz. jacobi_theta_nome (f z) (g z))"
unfolding continuous_def
using assms by (auto intro!: tendsto_eq_intros simp: continuous_def)
subsection ‹The Jacobi theta function in the upper half of the complex plane›
text ‹
We now define the more usual version of the Jacobi ‹θ› function, which takes two complex
parameters $z$ and $t$ where $z$ is arbitrary and $t$ must lie in the upper half of the
complex plane.
›
definition jacobi_theta_00 :: "complex ⇒ complex ⇒ complex" where
"jacobi_theta_00 z t = jacobi_theta_nome (to_nome z ^ 2) (to_nome t)"
lemma jacobi_theta_00_outside: "Im t ≤ 0 ⟹ jacobi_theta_00 z t = 0"
by (simp add: jacobi_theta_00_def mult_le_0_iff to_nome_def)
lemma has_sum_jacobi_theta_00:
assumes "Im t > 0"
shows "((λn. to_nome (of_int n ^ 2 * t + 2 * of_int n * z)) has_sum jacobi_theta_00 z t) UNIV"
using has_sum_jacobi_theta_nome[of "exp (𝗂 * of_real pi * t)" "exp (2 * 𝗂 * of_real pi * z)"] assms
by (simp add: jacobi_theta_00_def algebra_simps exp_add exp_power_int to_nome_def
flip: exp_of_nat_mult)
lemma sums_jacobi_theta_00:
assumes "Im t > 0"
shows "((λn. if n = 0 then 1 else 2 * to_nome t ^ n⇧2 *
cos (2 * of_nat n * of_real pi * z)) sums jacobi_theta_00 z t)"
proof -
define f where "f = (λn::int. to_nome (of_int n ^ 2 * t + 2 * of_int n * z))"
define S1 where "S1 = (∑⇩∞n∈{1..}. f n)"
define S2 where "S2 = (∑⇩∞n∈{..-1}. f n)"
have sum: "(f has_sum jacobi_theta_00 z t) UNIV"
unfolding f_def by (rule has_sum_jacobi_theta_00) fact
have [simp]: "f summable_on A" for A
by (rule summable_on_subset_banach, rule has_sum_imp_summable[OF sum]) auto
have "(f has_sum S1) {1..}" "(f has_sum S2) {..-1}"
unfolding S1_def S2_def by (rule has_sum_infsum; simp)+
moreover have "(f has_sum 1) {0}"
by (rule has_sum_finiteI) (auto simp: f_def)
ultimately have "(f has_sum (1 + S1 + S2)) ({0} ∪ {1..} ∪ {..-1})"
by (intro has_sum_Un_disjoint) auto
also have "{0} ∪ {1..} ∪ {..-1::int} = UNIV"
by auto
finally have "(f has_sum 1 + S1 + S2) UNIV" .
with sum have eq: "jacobi_theta_00 z t = 1 + S1 + S2"
using has_sum_unique by blast
note ‹(f has_sum S2) {..-1}›
also have "(f has_sum S2) {..-1} ⟷ ((λn. f (-n)) has_sum S2) {1..}"
by (intro has_sum_reindex_bij_witness[of _ uminus uminus]) auto
finally have "((λn. f n + f (-n)) has_sum (S1 + S2)) {1..}"
using ‹(f has_sum S1) {1..}› by (intro has_sum_add)
also have "?this ⟷ ((λn. f (int n) + f (-int n)) has_sum (S1 + S2)) {1..}"
by (rule has_sum_reindex_bij_witness[of _ int nat]) auto
also have "(λn::nat. f (int n) + f (-int n)) =
(λn. 2 * to_nome t ^ (n ^ 2) * cos (2 * of_nat n * of_real pi * z))"
by (auto simp: f_def exp_add exp_diff ring_distribs to_nome_def mult_ac cos_exp_eq
simp flip: exp_of_nat_mult)
also have "(… has_sum (S1 + S2)) {1..} ⟷
((λn. if n = 0 then 1 else 2 * to_nome t ^ (n ^ 2) *
cos (2 * of_nat n * of_real pi * z)) has_sum (S1 + S2)) {1..}"
by (intro has_sum_cong) auto
finally have "((λn. if n = 0 then 1 else 2 * to_nome t ^ (n ^ 2) * cos (2 * of_nat n * of_real pi * z))
has_sum (1 + (S1 + S2))) ({0} ∪ {1..})"
by (intro has_sum_Un_disjoint) (auto intro: has_sum_finiteI)
also have "1 + (S1 + S2) = jacobi_theta_00 z t"
using eq by (simp add: add_ac)
also have "{0} ∪ {1::nat..} = UNIV"
by auto
finally show ?thesis
by (rule has_sum_imp_sums)
qed
lemma jacobi_theta_00_holomorphic [holomorphic_intros]:
assumes "f holomorphic_on A" "g holomorphic_on A" "⋀z. z ∈ A ⟹ Im (g z) > 0" "open A"
shows "(λz. jacobi_theta_00 (f z) (g z)) holomorphic_on A"
unfolding jacobi_theta_00_def using assms(3,4)
by (auto intro!: holomorphic_intros assms(1,2) simp: to_nome_def)
lemma jacobi_theta_00_analytic [analytic_intros]:
assumes "f analytic_on A" "g analytic_on A" "⋀z. z ∈ A ⟹ Im (g z) > 0"
shows "(λz. jacobi_theta_00 (f z) (g z)) analytic_on A"
unfolding jacobi_theta_00_def using assms(3)
by (auto intro!: analytic_intros assms(1,2) simp: to_nome_def)
lemma jacobi_theta_00_plus_half_left:
"jacobi_theta_00 (z + 1 / 2) t = jacobi_theta_00 z (t + 1)"
proof -
define q where "q = exp (𝗂 * of_real pi * t)"
define w where "w = exp (2 * 𝗂 * of_real pi * z)"
have "jacobi_theta_00 (z + 1 / 2) t = jacobi_theta_nome (-w) q"
by (simp add: jacobi_theta_00_def w_def q_def algebra_simps exp_add to_nome_def flip: exp_of_nat_mult)
also have "… = jacobi_theta_nome w (-q)"
by (simp add: jacobi_theta_nome_minus_left)
also have "… = jacobi_theta_00 z (t + 1)"
by (simp add: jacobi_theta_00_def algebra_simps exp_add q_def w_def to_nome_def flip: exp_of_nat_mult)
finally show ?thesis .
qed
lemma jacobi_theta_00_plus_2_right: "jacobi_theta_00 z (t + 2) = jacobi_theta_00 z t"
by (simp add: jacobi_theta_00_def algebra_simps exp_add to_nome_def)
interpretation jacobi_theta_00_left: periodic_fun_simple' "λz. jacobi_theta_00 z t"
proof
fix z :: complex
have "jacobi_theta_00 (z + 1) t = jacobi_theta_00 (z + 1/2 + 1/2) t"
by (simp add: add.commute)
also have "… = jacobi_theta_00 z (t + 2)"
unfolding jacobi_theta_00_plus_half_left by (simp add: add.commute)
also have "jacobi_theta_00 z (t + 2) = jacobi_theta_00 z t"
by (rule jacobi_theta_00_plus_2_right)
finally show "jacobi_theta_00 (z + 1) t = jacobi_theta_00 z t" .
qed
interpretation jacobi_theta_00_right: periodic_fun_simple "λt. jacobi_theta_00 z t" 2
proof
fix t :: complex
show "jacobi_theta_00 z (t + 2) = jacobi_theta_00 z t"
by (rule jacobi_theta_00_plus_2_right)
qed
lemma jacobi_theta_00_plus_quasiperiod:
"jacobi_theta_00 (z + t) t = jacobi_theta_00 z t / to_nome (t + 2 * z)"
proof -
define q where "q = exp (𝗂 * of_real pi * t)"
define w where "w = exp (2 * 𝗂 * of_real pi * z)"
have "jacobi_theta_00 (z + t) t = jacobi_theta_nome (q⇧2 * w) q"
by (simp add: w_def q_def jacobi_theta_00_def algebra_simps exp_add to_nome_def
flip: exp_of_nat_mult)
also have "… = jacobi_theta_nome w q / (w * q)"
by (subst jacobi_theta_nome_quasiperiod) (auto simp: w_def q_def)
also have "… = exp (-pi * 𝗂 * (t + 2 * z)) * jacobi_theta_00 z t"
by (simp add: w_def q_def jacobi_theta_00_def field_simps exp_add exp_minus exp_diff to_nome_def
flip: exp_of_nat_mult)
finally show ?thesis
by (simp add: exp_minus exp_diff exp_add to_nome_def field_simps)
qed
lemma jacobi_theta_00_quasiperiodic:
"jacobi_theta_00 (z + of_int m + of_int n * t) t =
jacobi_theta_00 z t / to_nome (of_int (n^2) * t + 2 * of_int n * z)"
proof -
write jacobi_theta_00 ("θ")
have "θ (z + of_int m + of_int n * t) t =
θ (z + of_int n * t + of_int m) t"
by (simp add: add_ac)
also have "… = θ (z + of_int n * t) t"
by (rule jacobi_theta_00_left.plus_of_int)
also have "… = θ z t / to_nome (of_int (n^2) * t + 2 * of_int n * z)"
proof -
have *: "θ (z + of_nat n * t) t = θ z t / to_nome (of_nat (n^2) * t + 2 * of_nat n * z)"
for z :: complex and n :: nat
proof (induction n)
case (Suc n)
have "θ (z + of_nat (Suc n) * t) t = θ (z + of_nat n * t + t) t"
by (simp add: algebra_simps)
also have "… = θ z t / (to_nome (of_nat (n⇧2) * t + 2 * of_nat n * z) *
to_nome (t + 2 * (z + of_nat n * t)))"
by (subst jacobi_theta_00_plus_quasiperiod, subst Suc.IH) auto
also have "to_nome (of_nat (n⇧2) * t + 2 * of_nat n * z) * to_nome (t + 2 * (z + of_nat n * t)) =
to_nome ((of_nat (n⇧2) * t + 2 * of_nat n * z) + (t + 2 * (z + of_nat n * t)))"
by (rule to_nome_add [symmetric])
also have "(of_nat (n⇧2) * t + 2 * of_nat n * z) + (t + 2 * (z + of_nat n * t)) =
of_nat ((Suc n)⇧2) * t + 2 * of_nat (Suc n) * z"
by (simp add: algebra_simps power2_eq_square)
finally show ?case .
qed auto
show ?thesis
proof (cases "n ≥ 0")
case True
thus ?thesis
using *[of z "nat n"] by simp
next
case False
thus ?thesis
using *[of "z + of_int n * t" "nat (-n)"] False
by (simp add: field_simps power2_eq_square to_nome_add to_nome_diff to_nome_minus)
qed
qed
finally show ?thesis .
qed
lemma jacobi_theta_00_onequarter_left:
"jacobi_theta_00 (1/4) t = jacobi_theta_00 (1/2) (4 * t)"
by (simp add: jacobi_theta_00_def to_nome_power jacobi_theta_nome_ii_left)
lemma jacobi_theta_00_eq_0: "jacobi_theta_00 ((t + 1) / 2) t = 0"
proof -
have "jacobi_theta_00 ((t + 1) / 2) t = jacobi_theta_nome (to_nome (t + 1)) (to_nome t)"
by (simp add: jacobi_theta_00_def to_nome_power add_divide_distrib)
also have "… = 0"
by (simp add: to_nome_add jacobi_theta_nome_minus_same)
finally show ?thesis .
qed
lemma jacobi_theta_00_eq_0': "jacobi_theta_00 ((of_int m + 1/2) + (of_int n + 1/2) * t) t = 0"
proof -
have "jacobi_theta_00 ((of_int m + 1/2) + (of_int n + 1/2) * t) t =
jacobi_theta_00 ((t + 1) / 2 + of_int m + of_int n * t) t"
by (simp add: algebra_simps add_divide_distrib)
also have "… = 0"
by (simp only: jacobi_theta_00_quasiperiodic jacobi_theta_00_eq_0) auto
finally show ?thesis .
qed
lemma tendsto_jacobi_theta_00 [tendsto_intros]:
assumes "(f ⤏ w) F" "(g ⤏ q) F" "Im q > 0"
shows "((λz. jacobi_theta_00 (f z) (g z)) ⤏ jacobi_theta_00 w q) F"
unfolding jacobi_theta_00_def
by (intro tendsto_intros assms(1,2)) (use assms(3) in ‹auto simp: norm_to_nome›)
lemma continuous_on_jacobi_theta_00 [continuous_intros]:
assumes "continuous_on A f" "continuous_on A g"
assumes "⋀z. z ∈ A ⟹ Im (g z) > 0"
shows "continuous_on A (λz. jacobi_theta_00 (f z) (g z))"
unfolding jacobi_theta_00_def
by (intro continuous_intros assms(1,2)) (use assms(3) in ‹auto simp: norm_to_nome›)
lemma continuous_jacobi_theta_00 [continuous_intros]:
assumes "continuous F f" "continuous F g" "Im (g (netlimit F)) > 0"
shows "continuous F (λz. jacobi_theta_00 (f z) (g z))"
unfolding jacobi_theta_00_def
by (intro continuous_intros assms(1,2)) (use assms(3) in ‹auto simp: norm_to_nome›)
subsection ‹The auxiliary theta functions in terms of the nome›
definition jacobi_theta_nome_00 :: "'a :: {real_normed_field, banach} ⇒ 'a ⇒ 'a" where
"jacobi_theta_nome_00 w q = jacobi_theta_nome (w^2) q"
definition jacobi_theta_nome_01 :: "'a :: {real_normed_field, banach} ⇒ 'a ⇒ 'a" where
"jacobi_theta_nome_01 w q = jacobi_theta_nome (-(w^2)) q"
definition jacobi_theta_nome_10 :: "'a :: {real_normed_field, banach, ln} ⇒ 'a ⇒ 'a" where
"jacobi_theta_nome_10 w q = w * q powr (1/4) * jacobi_theta_nome (w ^ 2 * q) q"
definition jacobi_theta_nome_11 :: "complex ⇒ complex ⇒ complex" where
"jacobi_theta_nome_11 w q = 𝗂 * w * q powr (1/4) * jacobi_theta_nome (-(w ^ 2) * q) q"
lemmas jacobi_theta_nome_xx_defs =
jacobi_theta_nome_00_def jacobi_theta_nome_01_def
jacobi_theta_nome_10_def jacobi_theta_nome_11_def
lemma jacobi_theta_nome_00_outside [simp]: "norm q ≥ 1 ⟹ jacobi_theta_nome_00 w q = 0"
and jacobi_theta_nome_01_outside [simp]: "norm q ≥ 1 ⟹ jacobi_theta_nome_01 w q = 0"
and jacobi_theta_nome_10_outside [simp]: "norm q' ≥ 1 ⟹ jacobi_theta_nome_10 w' q' = 0"
and jacobi_theta_nome_11_outside [simp]: "norm q'' ≥ 1 ⟹ jacobi_theta_nome_11 w'' q'' = 0"
by (simp_all add: jacobi_theta_nome_xx_defs)
lemma jacobi_theta_nome_01_conv_00: "jacobi_theta_nome_01 w' q' = jacobi_theta_nome_00 w' (-q')"
and jacobi_theta_nome_11_conv_10: "jacobi_theta_nome_11 w q = jacobi_theta_nome_10 (𝗂 * w) q"
by (simp_all add: jacobi_theta_nome_xx_defs power_mult_distrib jacobi_theta_nome_minus_left)
lemma jacobi_theta_nome_00_0_right [simp]: "w ≠ 0 ⟹ jacobi_theta_nome_00 w 0 = 1"
and jacobi_theta_nome_01_0_right [simp]: "w ≠ 0 ⟹ jacobi_theta_nome_01 w 0 = 1"
and jacobi_theta_nome_10_0_right [simp]: "jacobi_theta_nome_10 w' 0 = 0"
and jacobi_theta_nome_11_0_right [simp]: "jacobi_theta_nome_11 w'' 0 = 0"
by (simp_all add: jacobi_theta_nome_xx_defs)
lemma jacobi_theta_nome_00_of_real:
"jacobi_theta_nome_00 (of_real w :: 'a :: {banach, real_normed_field}) (of_real q) =
of_real (jacobi_theta_nome_00 w q)"
and jacobi_theta_nome_01_of_real:
"jacobi_theta_nome_01 (of_real w :: 'a) (of_real q) = of_real (jacobi_theta_nome_01 w q)"
and jacobi_theta_nome_10_complex_of_real:
"q ≥ 0 ⟹ jacobi_theta_nome_10 (complex_of_real w) (of_real q) =
of_real (jacobi_theta_nome_10 w q)"
by (simp_all add: jacobi_theta_nome_xx_defs flip: jacobi_theta_nome_of_real powr_of_real)
lemma jacobi_theta_nome_00_cnj:
"jacobi_theta_nome_00 (cnj w) (cnj q) = cnj (jacobi_theta_nome_00 w q)"
and jacobi_theta_nome_01_cnj:
"jacobi_theta_nome_01 (cnj w) (cnj q) = cnj (jacobi_theta_nome_01 w q)"
and jacobi_theta_nome_10_cnj:
"(Im q = 0 ⟹ Re q ≥ 0) ⟹
jacobi_theta_nome_10 (cnj w) (cnj q) = cnj (jacobi_theta_nome_10 w q)"
and jacobi_theta_nome_11_cnj:
"(Im q = 0 ⟹ Re q ≥ 0) ⟹
jacobi_theta_nome_11 (cnj w) (cnj q) = -cnj (jacobi_theta_nome_11 w q)"
by (simp_all add: jacobi_theta_nome_xx_defs cnj_powr flip: jacobi_theta_nome_cnj)
lemma has_sum_jacobi_theta_nome_00:
assumes "norm q < 1" "w ≠ 0"
shows "((λn. w powi (2*n) * q powi n⇧2) has_sum jacobi_theta_nome_00 w q) UNIV"
using has_sum_jacobi_theta_nome[of q "w^2"] assms
by (simp add: jacobi_theta_nome_00_def power_int_mult_distrib power_int_mult power_mult_distrib)
lemma has_sum_jacobi_theta_nome_01:
assumes "norm q < 1" "w ≠ 0"
shows "((λn. (-1) powi n * w powi (2*n) * q powi n⇧2) has_sum jacobi_theta_nome_01 w q) UNIV"
using has_sum_jacobi_theta_nome[of q "-(w^2)"] assms
by (simp add: jacobi_theta_nome_01_def power_int_mult power_mult_distrib
flip: power_int_mult_distrib)
lemma has_sum_jacobi_theta_nome_10':
assumes q: "norm q < 1" and [simp]: "w ≠ 0" "q ≠ 0"
shows "((λn. w powi (2*n+1) * q powi (n*(n+1))) has_sum
(jacobi_theta_nome_10 w q / q powr (1/4))) UNIV"
proof -
have "((λn. w * ((w⇧2 * q) powi n * q powi (n ^ 2))) has_sum
(w * jacobi_theta_nome (w ^ 2 * q) q)) UNIV"
by (intro has_sum_cmult_right has_sum_jacobi_theta_nome) (use q in auto)
also have "(λn. w * ((w⇧2 * q) powi n * q powi (n ^ 2))) = (λn. w powi (2*n+1) * q powi (n*(n+1)))"
by (simp add: power_int_mult_distrib power_int_power power_int_add ring_distribs)
(simp_all add: algebra_simps power2_eq_square)?
finally show ?thesis
by (simp add: jacobi_theta_nome_10_def)
qed
lemma has_sum_jacobi_theta_nome_10:
fixes q :: "'a :: {real_normed_field, banach, ln}"
assumes q: "norm q < 1" and [simp]: "w ≠ 0" "exp (ln q) = q"
shows "((λn. w powi (2*n+1) * q powr (of_int n + 1 / 2) ^ 2) has_sum
(jacobi_theta_nome_10 w q)) UNIV"
proof -
have "exp (ln q) ≠ 0"
by (rule exp_not_eq_zero)
hence [simp]: "q ≠ 0"
by auto
have "((λn. q powr (1/4) * (w powi (2*n+1) * q powi (n*(n+1)))) has_sum
(q powr (1/4) * (jacobi_theta_nome_10 w q / q powr (1/4)))) UNIV"
by (intro has_sum_cmult_right has_sum_jacobi_theta_nome_10') fact+
also have "(q powr (1/4) * (jacobi_theta_nome_10 w q / q powr (1/4))) = jacobi_theta_nome_10 w q"
by simp
also have "(λn::int. q powr (1/4) * (w powi (2*n+1) * q powi (n*(n+1)))) =
(λn::int. w powi (2*n+1) * q powr ((of_int n + 1/2) ^ 2))"
proof
fix n :: int
have "q powr (1/4) * (w powi (2*n+1) * q powi (n*(n+1))) =
w powi (2*n+1) * (q powr (1/4) * q powi (n*(n+1)))"
by (simp add: mult_ac)
also have "… = w powi (2*n+1) * (q powr (1/4) * q powr (of_int (n*(n+1))))"
proof -
have "q powr (of_int (n*(n+1))) = exp (of_int (n*(n+1)) * ln q)"
by (simp add: powr_def)
also have "… = q powi (n * (n + 1))"
by (subst exp_power_int [symmetric]) auto
finally show ?thesis
by simp
qed
also have "q powr (1/4) * q powr of_int (n*(n+1)) =
q powr (1/4 + of_int (n*(n+1)))"
by (simp add: powr_def field_simps flip: exp_add)
also have "1/4 + of_int (n*(n+1)) = (of_int n + 1/2 :: 'a) ^ 2"
by (simp add: field_simps power2_eq_square)
finally show "q powr (1/4) * (w powi (2*n+1) * q powi (n*(n+1))) =
w powi (2*n+1) * q powr ((of_int n + 1/2) ^ 2)" .
qed
finally show ?thesis .
qed
lemma has_sum_jacobi_theta_nome_11':
assumes q: "norm q < 1" and [simp]: "w ≠ 0" "q ≠ 0"
shows "((λn. (-1) powi n * w powi (2*n+1) * q powi (n*(n+1))) has_sum
(jacobi_theta_nome_11 w q / (𝗂 * q powr (1/4)))) UNIV"
proof -
have "((λn. w * ((-(w⇧2) * q) powi n * q powi (n ^ 2))) has_sum
(w * jacobi_theta_nome (-(w ^ 2) * q) q)) UNIV"
by (intro has_sum_cmult_right has_sum_jacobi_theta_nome) (use q in auto)
also have "(λn. (-(w⇧2) * q) powi n) = (λn. (-1) powi n * (w ^ 2 * q) powi n)"
by (subst power_int_mult_distrib [symmetric]) auto
also have "(λn. w * ((-1) powi n * (w⇧2 * q) powi n * q powi (n ^ 2))) =
(λn. (-1) powi n * w powi (2*n+1) * q powi (n*(n+1)))"
by (simp add: power_int_mult_distrib power_int_power power_int_add ring_distribs)
(simp_all add: algebra_simps power2_eq_square)?
finally show ?thesis
by (simp add: jacobi_theta_nome_11_def mult_ac)
qed
lemma has_sum_jacobi_theta_nome_11:
assumes q: "norm q < 1" and [simp]: "w ≠ 0" "q ≠ 0"
shows "((λn. 𝗂 * (-1) powi n * w powi (2*n+1) * q powr (of_int n + 1/2) ^ 2) has_sum
(jacobi_theta_nome_11 w q)) UNIV"
proof -
have "((λn. (𝗂*w) powi (2*n+1) * q powr (of_int n + 1 / 2) ^ 2) has_sum
(jacobi_theta_nome_10 (𝗂*w) q)) UNIV"
by (intro has_sum_jacobi_theta_nome_10) (use q in auto)
also have "(λn. (𝗂*w) powi (2*n+1)) = (λn. 𝗂 * 𝗂 powi (2*n) * w powi (2*n+1))"
by (simp add: power_int_mult_distrib power_int_add mult_ac)
also have "(λn. 𝗂 powi (2*n)) = (λn. (-1) powi n)"
by (subst power_int_mult) auto
finally show ?thesis
by (simp add: jacobi_theta_nome_11_conv_10)
qed
lemma jacobi_theta_nome_00_holomorphic [holomorphic_intros]:
assumes "f holomorphic_on A" "g holomorphic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z) ≠ 0" "⋀z. z ∈ A ⟹ norm (g z) < 1" "open A"
shows "(λz. jacobi_theta_nome_00 (f z) (g z)) holomorphic_on A"
unfolding jacobi_theta_nome_00_def
by (intro holomorphic_intros assms(1,2)) (use assms(3-) in auto)
lemma jacobi_theta_nome_01_holomorphic [holomorphic_intros]:
assumes "f holomorphic_on A" "g holomorphic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z) ≠ 0" "⋀z. z ∈ A ⟹ norm (g z) < 1" "open A"
shows "(λz. jacobi_theta_nome_01 (f z) (g z)) holomorphic_on A"
unfolding jacobi_theta_nome_01_def
by (intro holomorphic_intros assms(1,2)) (use assms(3-) in auto)
lemma jacobi_theta_nome_10_holomorphic [holomorphic_intros]:
assumes "f holomorphic_on A" "g holomorphic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z) ≠ 0"
assumes "⋀z. z ∈ A ⟹ norm (g z) < 1 ∧ g z ∉ ℝ⇩≤⇩0" "open A"
shows "(λz. jacobi_theta_nome_10 (f z) (g z)) holomorphic_on A"
unfolding jacobi_theta_nome_10_def
by (intro holomorphic_intros assms(1,2)) (use assms(3-) in force)+
lemma jacobi_theta_nome_11_holomorphic [holomorphic_intros]:
assumes "f holomorphic_on A" "g holomorphic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z) ≠ 0"
assumes "⋀z. z ∈ A ⟹ norm (g z) < 1 ∧ g z ∉ ℝ⇩≤⇩0" "open A"
shows "(λz. jacobi_theta_nome_11 (f z) (g z)) holomorphic_on A"
unfolding jacobi_theta_nome_11_def
by (intro holomorphic_intros assms(1,2)) (use assms(3-) in force)+
lemma jacobi_theta_nome_00_analytic [analytic_intros]:
assumes "f analytic_on A" "g analytic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z) ≠ 0" "⋀z. z ∈ A ⟹ norm (g z) < 1"
shows "(λz. jacobi_theta_nome_00 (f z) (g z)) analytic_on A"
unfolding jacobi_theta_nome_00_def
by (intro analytic_intros assms(1,2)) (use assms(3-) in auto)
lemma jacobi_theta_nome_01_analytic [analytic_intros]:
assumes "f analytic_on A" "g analytic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z) ≠ 0" "⋀z. z ∈ A ⟹ norm (g z) < 1"
shows "(λz. jacobi_theta_nome_01 (f z) (g z)) analytic_on A"
unfolding jacobi_theta_nome_01_def
by (intro analytic_intros assms(1,2)) (use assms(3-) in auto)
lemma jacobi_theta_nome_10_analytic [analytic_intros]:
assumes "f analytic_on A" "g analytic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z) ≠ 0"
assumes "⋀z. z ∈ A ⟹ norm (g z) < 1 ∧ g z ∉ ℝ⇩≤⇩0"
shows "(λz. jacobi_theta_nome_10 (f z) (g z)) analytic_on A"
unfolding jacobi_theta_nome_10_def
by (intro analytic_intros assms(1,2)) (use assms(3-) in force)+
lemma jacobi_theta_nome_11_analytic [analytic_intros]:
assumes "f analytic_on A" "g analytic_on A"
assumes "⋀z. z ∈ A ⟹ norm (f z) ≠ 0"
assumes "⋀z. z ∈ A ⟹ norm (g z) < 1 ∧ g z ∉ ℝ⇩≤⇩0"
shows "(λz. jacobi_theta_nome_11 (f z) (g z)) analytic_on A"
unfolding jacobi_theta_nome_11_def
by (intro analytic_intros assms(1,2)) (use assms(3-) in force)+
lemma tendsto_jacobi_theta_nome_00 [tendsto_intros]:
fixes f g :: "'a ⇒ 'b :: {real_normed_field, banach, heine_borel}"
assumes "(f ⤏ w) F" "(g ⤏ q) F" "w ≠ 0" "norm q < 1"
shows "((λz. jacobi_theta_nome_00 (f z) (g z)) ⤏ jacobi_theta_nome_00 w q) F"
unfolding jacobi_theta_nome_00_def
by (intro tendsto_intros assms(1,2)) (use assms(3,4) in auto)
lemma continuous_on_jacobi_theta_nome_00 [continuous_intros]:
fixes f g :: "'a :: topological_space ⇒ 'b :: {real_normed_field, banach, heine_borel}"
assumes "continuous_on A f" "continuous_on A g"
assumes "⋀z. z ∈ A ⟹ f z ≠ 0" "⋀z. z ∈ A ⟹ norm (g z) < 1"
shows "continuous_on A (λz. jacobi_theta_nome_00 (f z) (g z))"
unfolding jacobi_theta_nome_00_def
by (intro continuous_intros assms(1,2)) (use assms(3,4) in auto)
lemma continuous_jacobi_theta_nome_00 [continuous_intros]:
fixes f g :: "'a :: t2_space ⇒ 'b :: {real_normed_field, banach, heine_borel}"
assumes "continuous F f" "continuous F g" "f (netlimit F) ≠ 0" "norm (g (netlimit F)) < 1"
shows "continuous F (λz. jacobi_theta_nome_00 (f z) (g z))"
unfolding jacobi_theta_nome_00_def
by (intro continuous_intros assms(1,2)) (use assms(3,4) in auto)
lemma tendsto_jacobi_theta_nome_01 [tendsto_intros]:
fixes f g :: "'a ⇒ 'b :: {real_normed_field, banach, heine_borel}"
assumes "(f ⤏ w) F" "(g ⤏ q) F" "w ≠ 0" "norm q < 1"
shows "((λz. jacobi_theta_nome_01 (f z) (g z)) ⤏ jacobi_theta_nome_01 w q) F"
unfolding jacobi_theta_nome_01_def
by (intro tendsto_intros assms(1,2)) (use assms(3,4) in auto)
lemma continuous_on_jacobi_theta_nome_01 [continuous_intros]:
fixes f g :: "'a :: topological_space ⇒ 'b :: {real_normed_field, banach, heine_borel}"
assumes "continuous_on A f" "continuous_on A g"
assumes "⋀z. z ∈ A ⟹ f z ≠ 0" "⋀z. z ∈ A ⟹ norm (g z) < 1"
shows "continuous_on A (λz. jacobi_theta_nome_01 (f z) (g z))"
unfolding jacobi_theta_nome_01_def
by (intro continuous_intros assms(1,2)) (use assms(3,4) in auto)
lemma continuous_jacobi_theta_nome_01 [continuous_intros]:
fixes f g :: "'a :: t2_space ⇒ 'b :: {real_normed_field, banach, heine_borel}"
assumes "continuous F f" "continuous F g" "f (netlimit F) ≠ 0" "norm (g (netlimit F)) < 1"
shows "continuous F (λz. jacobi_theta_nome_01 (f z) (g z))"
unfolding jacobi_theta_nome_01_def
by (intro continuous_intros assms(1,2)) (use assms(3,4) in auto)
lemma tendsto_jacobi_theta_nome_10_complex [tendsto_intros]:
fixes f g :: "complex ⇒ complex"
assumes "(f ⤏ w) F" "(g ⤏ q) F" "w ≠ 0" "norm q < 1" "q ∉ ℝ⇩≤⇩0"
shows "((λz. jacobi_theta_nome_10 (f z) (g z)) ⤏ jacobi_theta_nome_10 w q) F"
unfolding jacobi_theta_nome_10_def
by (intro tendsto_intros assms(1,2)) (use assms(3-5) in auto)
lemma continuous_on_jacobi_theta_nome_10_complex [continuous_intros]:
fixes f g :: "complex ⇒ complex"
assumes "continuous_on A f" "continuous_on A g"
assumes "⋀z. z ∈ A ⟹ f z ≠ 0" "⋀z. z ∈ A ⟹ norm (g z) < 1 ∧ (Re (g z) > 0 ∨ Im (g z) ≠ 0)"
shows "continuous_on A (λz. jacobi_theta_nome_10 (f z) (g z))"
unfolding jacobi_theta_nome_10_def
by (intro continuous_intros assms(1,2); use assms(3,4) in force)
lemma continuous_jacobi_theta_nome_10_complex [continuous_intros]:
assumes "continuous F f" "continuous F g" "f (netlimit F) ≠ 0"
assumes "norm (g (netlimit F)) < 1" "Re (g (netlimit F)) > 0 ∨ Im (g (netlimit F)) ≠ 0"
shows "continuous F (λz. jacobi_theta_nome_10 (f z) (g z))"
unfolding jacobi_theta_nome_10_def
by (intro continuous_intros assms(1,2); use assms(3-) in force)
lemma tendsto_jacobi_theta_nome_10_real [tendsto_intros]:
fixes f g :: "real ⇒ real"
assumes "(f ⤏ w) F" "(g ⤏ q) F" "w ≠ 0" "norm q < 1" "q > 0"
shows "((λz. jacobi_theta_nome_10 (f z) (g z)) ⤏ jacobi_theta_nome_10 w q) F"
unfolding jacobi_theta_nome_10_def
by (intro tendsto_intros assms(1,2)) (use assms(3-5) in auto)
lemma continuous_on_jacobi_theta_nome_10_real [continuous_intros]:
fixes f g :: "real ⇒ real"
assumes "continuous_on A f" "continuous_on A g"
assumes "⋀z. z ∈ A ⟹ f z ≠ 0" "⋀z. z ∈ A ⟹ g z ∈ {0<..<1}"
shows "continuous_on A (λz. jacobi_theta_nome_10 (f z) (g z))"
unfolding jacobi_theta_nome_10_def
by (intro continuous_intros assms(1,2); use assms(3,4) in force)
lemma continuous_jacobi_theta_nome_10_real [continuous_intros]:
fixes f g :: "real ⇒ real"
assumes "continuous F f" "continuous F g" "f (netlimit F) ≠ 0" "g (netlimit F) ∈ {0<..<1}"
shows "continuous F (λz. jacobi_theta_nome_10 (f z) (g z))"
unfolding jacobi_theta_nome_10_def
by (intro continuous_intros assms(1,2); use assms(3-) in auto)
lemma tendsto_jacobi_theta_nome_11_complex [tendsto_intros]:
fixes f g :: "complex ⇒ complex"
assumes "(f ⤏ w) F" "(g ⤏ q) F" "w ≠ 0" "norm q < 1" "q ∉ ℝ⇩≤⇩0"
shows "((λz. jacobi_theta_nome_11 (f z) (g z)) ⤏ jacobi_theta_nome_11 w q) F"
unfolding jacobi_theta_nome_11_def
by (intro tendsto_intros assms(1,2)) (use assms(3-5) in auto)
lemma continuous_on_jacobi_theta_nome_11_complex [continuous_intros]:
fixes f g :: "complex ⇒ complex"
assumes "continuous_on A f" "continuous_on A g"
assumes "⋀z. z ∈ A ⟹ f z ≠ 0" "⋀z. z ∈ A ⟹ norm (g z) < 1 ∧ (Re (g z) > 0 ∨ Im (g z) ≠ 0)"
shows "continuous_on A (λz. jacobi_theta_nome_11 (f z) (g z))"
unfolding jacobi_theta_nome_11_def
by (intro continuous_intros assms(1,2); use assms(3,4) in force)
lemma continuous_jacobi_theta_nome_11_complex [continuous_intros]:
assumes "continuous F f" "continuous F g" "f (netlimit F) ≠ 0"
assumes "norm (g (netlimit F)) < 1" "Re (g (netlimit F)) > 0 ∨ Im (g (netlimit F)) ≠ 0"
shows "continuous F (λz. jacobi_theta_nome_11 (f z) (g z))"
unfolding jacobi_theta_nome_11_def
by (intro continuous_intros assms(1,2); use assms(3-) in force)
lemma tendsto_jacobi_theta_nome_11_real [tendsto_intros]:
fixes f g :: "real ⇒ real"
assumes "(f ⤏ w) F" "(g ⤏ q) F" "w ≠ 0" "norm q < 1" "q > 0"
shows "((λz. jacobi_theta_nome_11 (f z) (g z)) ⤏ jacobi_theta_nome_11 w q) F"
unfolding jacobi_theta_nome_11_def
by (intro tendsto_intros assms(1,2)) (use assms(3-5) in auto)
lemma continuous_on_jacobi_theta_nome_11_real [continuous_intros]:
fixes f g :: "real ⇒ real"
assumes "continuous_on A f" "continuous_on A g"
assumes "⋀z. z ∈ A ⟹ f z ≠ 0" "⋀z. z ∈ A ⟹ g z ∈ {0<..<1}"
shows "continuous_on A (λz. jacobi_theta_nome_11 (f z) (g z))"
unfolding jacobi_theta_nome_11_def
by (intro continuous_intros assms(1,2); use assms(3,4) in force)
lemma continuous_jacobi_theta_nome_11_real [continuous_intros]:
fixes f g :: "real ⇒ real"
assumes "continuous F f" "continuous F g" "f (netlimit F) ≠ 0" "g (netlimit F) ∈ {0<..<1}"
shows "continuous F (λz. jacobi_theta_nome_11 (f z) (g z))"
unfolding jacobi_theta_nome_11_def
by (intro continuous_intros assms(1,2); use assms(3-) in auto)
subsection ‹The auxiliary theta functions in the complex plane›
definition jacobi_theta_01 :: "complex ⇒ complex ⇒ complex" where
"jacobi_theta_01 z t = jacobi_theta_00 (z + 1/2) t"
definition jacobi_theta_10 :: "complex ⇒ complex ⇒ complex" where
"jacobi_theta_10 z t = to_nome (z + t/4) * jacobi_theta_00 (z + t/2) t"
definition jacobi_theta_11 :: "complex ⇒ complex ⇒ complex" where
"jacobi_theta_11 z t = to_nome (z + t/4 + 1/2) * jacobi_theta_00 (z + t/2 + 1/2) t"
lemma jacobi_theta_00_conv_nome:
"jacobi_theta_00 z t = jacobi_theta_nome_00 (to_nome z) (to_nome t)"
by (simp add: jacobi_theta_00_def jacobi_theta_nome_00_def)
lemma jacobi_theta_01_conv_nome:
"jacobi_theta_01 z t = jacobi_theta_nome_01 (to_nome z) (to_nome t)"
by (simp add: jacobi_theta_01_def jacobi_theta_nome_01_def jacobi_theta_00_conv_nome
jacobi_theta_nome_00_def to_nome_add power_mult_distrib)
lemma jacobi_theta_10_conv_nome:
assumes "Re t ∈ {-1<..1}"
shows "jacobi_theta_10 z t = jacobi_theta_nome_10 (to_nome z) (to_nome t)"
using assms
by (simp add: jacobi_theta_10_def jacobi_theta_nome_10_def jacobi_theta_00_conv_nome
jacobi_theta_nome_00_def to_nome_add power_mult_distrib to_nome_power to_nome_powr)
lemma jacobi_theta_11_conv_nome:
assumes "Re t ∈ {-1<..1}"
shows "jacobi_theta_11 z t = jacobi_theta_nome_11 (to_nome z) (to_nome t)"
using assms
by (simp add: jacobi_theta_11_def jacobi_theta_nome_11_def jacobi_theta_00_conv_nome
jacobi_theta_nome_00_def to_nome_add power_mult_distrib to_nome_power to_nome_powr)
lemma has_sum_jacobi_theta_01:
assumes "Im t > 0"
shows "((λn. (-1) powi n * to_nome (of_int n ^ 2 * t + 2 * of_int n * z))
has_sum jacobi_theta_01 z t) UNIV"
proof -
have "((λn. to_nome (of_int n ^ 2 * t + 2 * of_int n * (z + 1 / 2))) has_sum jacobi_theta_01 z t) UNIV"
unfolding jacobi_theta_01_def by (intro has_sum_jacobi_theta_00 assms)
also have "(λn. to_nome (of_int n ^ 2 * t + 2 * of_int n * (z + 1 / 2))) =
(λn. (-1) powi n * to_nome (of_int n ^ 2 * t + 2 * of_int n * z))"
by (simp add: ring_distribs exp_add mult_ac to_nome_add)
finally show ?thesis .
qed
lemma sums_jacobi_theta_01:
assumes "Im t > 0"
shows "((λn. if n = 0 then 1 else 2 * (-1) ^ n * to_nome t ^ n⇧2 *
cos (2 * of_nat n * of_real pi * z)) sums jacobi_theta_01 z t)"
proof -
have [simp]: "sin (of_nat n * of_real pi :: complex) = 0" for n
by (metis of_real_0 of_real_mult of_real_of_nat_eq sin_npi sin_of_real)
have [simp]: "cos (of_nat n * of_real pi :: complex) = (-1) ^ n" for n
proof -
have "cos (of_nat n * of_real pi) = complex_of_real (cos (real n * pi))"
by (subst cos_of_real [symmetric]) simp
also have "cos (real n * pi) = (-1) ^ n"
by simp
finally show ?thesis by simp
qed
show ?thesis
using sums_jacobi_theta_00[of t "z + 1/2"] assms
by (simp add: jacobi_theta_01_def ring_distribs cos_add mult_ac cong: if_cong)
qed
interpretation jacobi_theta_01_left: periodic_fun_simple' "λz. jacobi_theta_01 z t"
proof
fix z :: complex
show "jacobi_theta_01 (z + 1) t = jacobi_theta_01 z t"
using jacobi_theta_00_left.plus_1[of "z + 1/2" t] by (simp add: jacobi_theta_01_def)
qed
interpretation jacobi_theta_01_right: periodic_fun_simple "λt. jacobi_theta_01 z t" 2
proof
fix t :: complex
show "jacobi_theta_01 z (t + 2) = jacobi_theta_01 z t"
using jacobi_theta_00_right.plus_period[of "z + 1/2" t] by (simp add: jacobi_theta_01_def)
qed
lemma jacobi_theta_10_plus1_left: "jacobi_theta_10 (z + 1) t = -jacobi_theta_10 z t"
using jacobi_theta_00_left.plus_1[of "z + t / 2" t]
by (simp add: jacobi_theta_10_def to_nome_add algebra_simps)
lemma jacobi_theta_11_plus1_left: "jacobi_theta_11 (z + 1) t = -jacobi_theta_11 z t"
using jacobi_theta_00_left.plus_1[of "z + t / 2 + 1 / 2" t]
by (simp add: jacobi_theta_11_def to_nome_add algebra_simps)
lemma jacobi_theta_10_plus2_right: "jacobi_theta_10 z (t + 2) = 𝗂 * jacobi_theta_10 z t"
using jacobi_theta_00_right.plus_1[of "z + t / 2" t]
jacobi_theta_00_left.plus_1[of "z + t / 2" "t + 2"]
by (simp add: jacobi_theta_10_def to_nome_add algebra_simps add_divide_distrib)
lemma jacobi_theta_11_plus2_right: "jacobi_theta_11 z (t + 2) = 𝗂 * jacobi_theta_11 z t"
using jacobi_theta_00_right.plus_1[of "z + t / 2 + 1 / 2" t]
jacobi_theta_00_left.plus_1[of "z + t / 2 + 1 / 2" "t + 2"]
by (simp add: jacobi_theta_11_def to_nome_add algebra_simps add_divide_distrib)
lemma jacobi_theta_00_plus_half_left': "jacobi_theta_00 (z + 1/2) t = jacobi_theta_01 z t"
by (simp add: jacobi_theta_01_def to_nome_add algebra_simps)
lemma jacobi_theta_01_plus_half_left: "jacobi_theta_01 (z + 1/2) t = jacobi_theta_00 z t"
using jacobi_theta_00_left.plus_1[of z t]
by (simp add: jacobi_theta_01_def to_nome_add algebra_simps)
lemma jacobi_theta_10_plus_half_left': "jacobi_theta_10 (z + 1/2) t = jacobi_theta_11 z t"
by (simp add: jacobi_theta_10_def jacobi_theta_11_def to_nome_add algebra_simps)
lemma jacobi_theta_11_plus_half_left': "jacobi_theta_11 (z + 1/2) t = -jacobi_theta_10 z t"
using jacobi_theta_00_left.plus_1[of "z + t / 2" t]
by (simp add: jacobi_theta_10_def jacobi_theta_11_def to_nome_add algebra_simps)
lemma tendsto_jacobi_theta_01 [tendsto_intros]:
assumes "(f ⤏ w) F" "(g ⤏ q) F" "Im q > 0"
shows "((λz. jacobi_theta_01 (f z) (g z)) ⤏ jacobi_theta_01 w q) F"
unfolding jacobi_theta_01_def
by (intro tendsto_intros assms(1,2)) (use assms(3) in ‹auto simp: norm_to_nome›)
lemma continuous_on_jacobi_theta_01 [continuous_intros]:
assumes "continuous_on A f" "continuous_on A g"
assumes "⋀z. z ∈ A ⟹ Im (g z) > 0"
shows "continuous_on A (λz. jacobi_theta_01 (f z) (g z))"
unfolding jacobi_theta_01_def
by (intro continuous_intros assms(1,2)) (use assms(3) in ‹auto simp: norm_to_nome›)
lemma continuous_jacobi_theta_01 [continuous_intros]:
assumes "continuous F f" "continuous F g" "Im (g (netlimit F)) > 0"
shows "continuous F (λz. jacobi_theta_01 (f z) (g z))"
unfolding jacobi_theta_01_def
by (intro continuous_intros assms(1,2)) (use assms(3) in ‹auto simp: norm_to_nome›)
lemma holomorphic_jacobi_theta_01 [holomorphic_intros]:
assumes "f holomorphic_on A" "g holomorphic_on A" "⋀z. z ∈ A ⟹ Im (g z) > 0" "open A"
shows "(λz. jacobi_theta_01 (f z) (g z)) holomorphic_on A"
unfolding jacobi_theta_01_def by (intro holomorphic_intros assms(1,2)) (use assms(3-) in auto)
lemma analytic_jacobi_theta_01 [analytic_intros]:
assumes "f analytic_on A" "g analytic_on A" "⋀z. z ∈ A ⟹ Im (g z) > 0"
shows "(λz. jacobi_theta_01 (f z) (g z)) analytic_on A"
unfolding jacobi_theta_01_def by (intro analytic_intros assms(1,2)) (use assms(3-) in auto)
lemma tendsto_jacobi_theta_10 [tendsto_intros]:
assumes "(f ⤏ w) F" "(g ⤏ q) F" "Im q > 0"
shows "((λz. jacobi_theta_10 (f z) (g z)) ⤏ jacobi_theta_10 w q) F"
unfolding jacobi_theta_10_def
by (intro tendsto_intros assms(1,2)) (use assms(3) in ‹auto simp: norm_to_nome›)
lemma continuous_on_jacobi_theta_10 [continuous_intros]:
assumes "continuous_on A f" "continuous_on A g"
assumes "⋀z. z ∈ A ⟹ Im (g z) > 0"
shows "continuous_on A (λz. jacobi_theta_10 (f z) (g z))"
unfolding jacobi_theta_10_def
by (intro continuous_intros assms(1,2)) (use assms(3) in ‹auto simp: norm_to_nome›)
lemma continuous_jacobi_theta_10 [continuous_intros]:
assumes "continuous F f" "continuous F g" "Im (g (netlimit F)) > 0"
shows "continuous F (λz. jacobi_theta_10 (f z) (g z))"
unfolding jacobi_theta_10_def
by (intro continuous_intros continuous_divide assms(1,2))
(use assms(3) in ‹auto simp: norm_to_nome›)
lemma holomorphic_jacobi_theta_10 [holomorphic_intros]:
assumes "f holomorphic_on A" "g holomorphic_on A" "⋀z. z ∈ A ⟹ Im (g z) > 0" "open A"
shows "(λz. jacobi_theta_10 (f z) (g z)) holomorphic_on A"
unfolding jacobi_theta_10_def by (intro holomorphic_intros assms(1,2)) (use assms(3-) in auto)
lemma analytic_jacobi_theta_10 [analytic_intros]:
assumes "f analytic_on A" "g analytic_on A" "⋀z. z ∈ A ⟹ Im (g z) > 0"
shows "(λz. jacobi_theta_10 (f z) (g z)) analytic_on A"
unfolding jacobi_theta_10_def by (intro analytic_intros assms(1,2)) (use assms(3-) in auto)
lemma tendsto_jacobi_theta_11 [tendsto_intros]:
assumes "(f ⤏ w) F" "(g ⤏ q) F" "Im q > 0"
shows "((λz. jacobi_theta_11 (f z) (g z)) ⤏ jacobi_theta_11 w q) F"
unfolding jacobi_theta_11_def
by (intro tendsto_intros assms(1,2)) (use assms(3) in ‹auto simp: norm_to_nome›)
lemma continuous_on_jacobi_theta_11 [continuous_intros]:
assumes "continuous_on A f" "continuous_on A g"
assumes "⋀z. z ∈ A ⟹ Im (g z) > 0"
shows "continuous_on A (λz. jacobi_theta_11 (f z) (g z))"
unfolding jacobi_theta_11_def
by (intro continuous_intros assms(1,2)) (use assms(3) in ‹auto simp: norm_to_nome›)
lemma continuous_jacobi_theta_11 [continuous_intros]:
assumes "continuous F f" "continuous F g" "Im (g (netlimit F)) > 0"
shows "continuous F (λz. jacobi_theta_11 (f z) (g z))"
unfolding jacobi_theta_11_def
by (intro continuous_intros continuous_divide assms(1,2))
(use assms(3) in ‹auto simp: norm_to_nome›)
lemma holomorphic_jacobi_theta_11 [holomorphic_intros]:
assumes "f holomorphic_on A" "g holomorphic_on A" "⋀z. z ∈ A ⟹ Im (g z) > 0" "open A"
shows "(λz. jacobi_theta_11 (f z) (g z)) holomorphic_on A"
unfolding jacobi_theta_11_def by (intro holomorphic_intros assms(1,2)) (use assms(3-) in auto)
lemma analytic_jacobi_theta_11 [analytic_intros]:
assumes "f analytic_on A" "g analytic_on A" "⋀z. z ∈ A ⟹ Im (g z) > 0"
shows "(λz. jacobi_theta_11 (f z) (g z)) analytic_on A"
unfolding jacobi_theta_11_def by (intro analytic_intros assms(1,2)) (use assms(3-) in auto)
end