The infinite q-Pochhammer products ∏_{n ≥ 1} (1 - qⁿ w)

For ‖q‖ < 1 in a complete normed field, the product ∏_{n ≥ 1} (1 - qⁿ w) (the q-Pochhammer symbol (q w; q)_∞) converges absolutely. This file records its convergence, the shift identity obtained by splitting off the first factor, and its nonvanishing. It also introduces the theta product θ_q(w) = (w; q)_∞ (q w⁻¹; q)_∞ = (1 - w) ∏_{n ≥ 1} (1 - qⁿ w) (1 - qⁿ w⁻¹) and proves its convergence, its nonvanishing and its quasi-periodicity θ_q(q w) = -w⁻¹ θ_q(w), and evaluates it at w = -1 and at q = w². These evaluations, together with Euler's identity ∏_{n ≥ 1} (1 + qⁿ) ∏_{n ≥ 0} (1 - q^{2n+1}) = 1, compute the Siegel functions of level two. Its evaluations at q = w³ and at a primitive cube root of unity w, multiplied by an Euler function, compute those of level three. When q and w depend continuously on τ in an open set U ⊆ ℂ with ‖q‖ < 1 on U, the product converges locally uniformly on U, and is holomorphic there when q and w are; for example q = e^{2π i τ} on the upper half-plane. The locally uniform convergence and holomorphy argument is adapted from Mathlib.NumberTheory.ModularForms.DedekindEta (C. Birkbeck, D. Loeffler).

Main results

• TauCeti.multipliable_one_sub_pow_mul: for ‖q‖ < 1 the product ∏_{n ≥ 1} (1 - qⁿ w) converges.
• TauCeti.tprod_one_sub_pow_mul_eq: ∏_{n ≥ 1} (1 - qⁿ w) = (1 - q w) ∏_{n ≥ 1} (1 - qⁿ (q w)).
• TauCeti.tprod_one_sub_pow_mul_ne_zero: the product is nonzero when all of its factors are.
• TauCeti.tendsto_tprod_one_sub_pow_mul: ∏_{n ≥ 1} (1 - qⁿ w) → 1 when q → 0 and q w → 0; w may be unbounded, and no completeness assumption is needed.
• TauCeti.tprod_one_sub_pow_ne_zero: the Euler function ∏_{n ≥ 1} (1 - qⁿ) is nonzero.
• TauCeti.norm_tprod_one_sub_pow_mul_le, TauCeti.norm_qTheta_le: the bounds ‖∏_{n ≥ 1} (1 - qⁿ w)‖ ≤ exp (‖q‖ ‖w‖ / (1 - ‖q‖)) and ‖θ_q(w)‖ ≤ ‖1 - w‖ exp (‖q‖ (‖w‖ + ‖w‖⁻¹) / (1 - ‖q‖)) for ‖q‖ < 1.
• TauCeti.norm_tprod_one_sub_pow_mul_sub_one_le, TauCeti.norm_tprod_one_add_pow_sub_one_le: the product is close to 1 for small q, ‖∏_{n ≥ 1} (1 - qⁿ w) - 1‖ ≤ exp (‖q‖ ‖w‖ / (1 - ‖q‖)) - 1, and ‖∏_{n ≥ 1} (1 + qⁿ) - 1‖ ≤ ‖q‖ / (1 - 2‖q‖) for ‖q‖ < 1/2.
• TauCeti.multipliable_one_add_pow, TauCeti.multipliable_one_sub_pow_odd, TauCeti.multipliable_one_add_pow_odd: for ‖q‖ < 1 the products ∏_{n ≥ 1} (1 + qⁿ) and ∏_{n ≥ 0} (1 ∓ q^{2n+1}) converge.
• TauCeti.qTheta: the theta product θ_q(w) = (1 - w) ∏_{n ≥ 1} (1 - qⁿ w) (1 - qⁿ w⁻¹).
• TauCeti.multipliable_qTheta, TauCeti.qTheta_ne_zero: for ‖q‖ < 1 the product in θ_q(w) converges, and θ_q(w) ≠ 0 when w is not an integral power of q.
• TauCeti.qTheta_mul_left: its quasi-periodicity θ_q(q w) = -w⁻¹ θ_q(w) for 0 < ‖q‖ < 1 and w ≠ 0.
• TauCeti.qTheta_one, TauCeti.differentiableOn_qTheta, TauCeti.hasDerivAt_qTheta_one: θ_q(1) = 0, and for ‖q‖ < 1 the theta product is holomorphic on ℂ \ {0} with derivative -(∏_{n ≥ 1} (1 - qⁿ))² at w = 1.
• TauCeti.qTheta_eq_mul_tprod_mul_tprod: θ_q(w) is 1 - w times its two half products.
• TauCeti.differentiable_qTheta_exp, TauCeti.hasDerivAt_qTheta_exp_zero: for ‖q‖ < 1, z ↦ θ_q(e^{2π i z}) is entire, with derivative -2π i (∏_{n ≥ 1} (1 - qⁿ))² at z = 0.
• TauCeti.qTheta_neg_one, TauCeti.qTheta_sq_self: θ_q(-1) = 2 (∏_{n ≥ 1} (1 + qⁿ))² and θ_{s²}(s) = (∏_{n ≥ 0} (1 - s^{2n+1}))².
• TauCeti.qTheta_pow_three_self_mul, TauCeti.qTheta_mul_tprod_of_sq_add_add_one_eq_zero: θ_{s³}(s) ∏_{n ≥ 1} (1 - s^{3n}) = ∏_{n ≥ 1} (1 - sⁿ), and θ_q(ω) ∏_{n ≥ 1} (1 - qⁿ) = (1 - ω) ∏_{n ≥ 1} (1 - q^{3n}) for a primitive cube root of unity ω.
• TauCeti.tprod_one_sub_pow_eq_tprod_one_sub_pow_odd_mul, TauCeti.tprod_one_add_pow_mul_tprod_one_sub_pow: the Euler function ∏_{n ≥ 1} (1 - qⁿ) is ∏_{n ≥ 0} (1 - q^{2n+1}) ∏_{n ≥ 1} (1 - q^{2n}), and multiplying it by ∏_{n ≥ 1} (1 + qⁿ) gives ∏_{n ≥ 1} (1 - q^{2n}).
• TauCeti.tprod_one_add_pow_mul_tprod_one_sub_pow_odd: Euler's identity ∏_{n ≥ 1} (1 + qⁿ) ∏_{n ≥ 0} (1 - q^{2n+1}) = 1 for ‖q‖ < 1, the analytic form of the equinumerosity of partitions into distinct parts and into odd parts.
• TauCeti.tprod_one_sub_pow_odd_ne_zero: ∏_{n ≥ 0} (1 - q^{2n+1}) ≠ 0 for ‖q‖ < 1.
• TauCeti.hasDerivAt_tprod_one_sub_pow_odd: the odd product ∏_{n ≥ 0} (1 - s^{2n+1}) has derivative -1 at s = 0.
• TauCeti.tendsto_tprod_one_sub_pow_odd_pow_sub_neg_div: for P(s) = ∏_{n ≥ 0} (1 - s^{2n+1}), (P(s)ᵏ - P(-s)ᵏ) / s → -2k as s → 0.
• TauCeti.tendsto_tprod_one_sub_qParam_pow_odd_pow: P(q)ᵏ → 1 at i∞, for q = e^{2π i τ} on the upper half-plane.
• TauCeti.hasProdLocallyUniformlyOn_one_sub_pow_mul: for q and w continuous on an open set U with ‖q‖ < 1 there, ∏_{n ≥ 1} (1 - q(τ)ⁿ w(τ)) converges locally uniformly on U.
• TauCeti.differentiableOn_tprod_one_sub_pow_mul: for q and w holomorphic on such a U, so is this product.

theorem TauCeti.summable_norm_pow_succ_mul {𝕜 : Type u_1} [NormedField 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) (w : 𝕜) : Summable fun (n : ℕ) => ‖q ^ (n + 1) * w‖

For ‖q‖ < 1 the norms ‖qⁿ⁺¹ w‖ are summable.

theorem TauCeti.tsum_norm_pow_succ_mul {𝕜 : Type u_1} [NormedField 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) (w : 𝕜) : ∑' (n : ℕ), ‖q ^ (n + 1) * w‖ = ‖q‖ * ‖w‖ / (1 - ‖q‖)

For ‖q‖ < 1, ∑_{n ≥ 1} ‖qⁿ w‖ = ‖q‖ ‖w‖ / (1 - ‖q‖).

theorem TauCeti.norm_tprod_one_sub_pow_mul_le {𝕜 : Type u_1} [NormedField 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) (w : 𝕜) : ‖∏' (n : ℕ), (1 - q ^ (n + 1) * w)‖ ≤ Real.exp (‖q‖ * ‖w‖ / (1 - ‖q‖))

For ‖q‖ < 1, ‖∏_{n ≥ 1} (1 - qⁿ w)‖ ≤ exp (‖q‖ ‖w‖ / (1 - ‖q‖)).

theorem TauCeti.norm_tprod_one_sub_pow_mul_sub_one_le {𝕜 : Type u_1} [NormedField 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) (w : 𝕜) : ‖∏' (n : ℕ), (1 - q ^ (n + 1) * w) - 1‖ ≤ Real.exp (‖q‖ * ‖w‖ / (1 - ‖q‖)) - 1

For ‖q‖ < 1, ‖∏_{n ≥ 1} (1 - qⁿ w) - 1‖ ≤ exp (‖q‖ ‖w‖ / (1 - ‖q‖)) - 1.

theorem TauCeti.norm_tprod_one_add_pow_sub_one_le {𝕜 : Type u_1} [NormedField 𝕜] {q : 𝕜} (hq : 2 * ‖q‖ < 1) : ‖∏' (n : ℕ), (1 + q ^ (n + 1)) - 1‖ ≤ ‖q‖ / (1 - 2 * ‖q‖)

For ‖q‖ < 1/2, ‖∏_{n ≥ 1} (1 + qⁿ) - 1‖ ≤ ‖q‖ / (1 - 2‖q‖).

noncomputable def TauCeti.qTheta {𝕜 : Type u_1} [NormedField 𝕜] (q w : 𝕜) : 𝕜

The theta product θ_q(w) = (w; q)_∞ (q w⁻¹; q)_∞, written as (1 - w) ∏_{n ≥ 1} (1 - qⁿ w) (1 - qⁿ w⁻¹). The product converges for ‖q‖ < 1; otherwise the value is a junk value. With q = e^{2π i τ} and w = e^{2π i (r₁ τ + r₂)} it is the product in the Siegel function g_r(τ).

theorem TauCeti.qTheta_def {𝕜 : Type u_1} [NormedField 𝕜] (q w : 𝕜) : qTheta q w = (1 - w) * ∏' (n : ℕ), (1 - q ^ (n + 1) * w) * (1 - q ^ (n + 1) * w⁻¹)

The defining product of the theta product θ_q(w).

@[simp]

theorem TauCeti.qTheta_one {𝕜 : Type u_1} [NormedField 𝕜] (q : 𝕜) : qTheta q 1 = 0

The theta product vanishes at w = 1.

theorem TauCeti.multipliable_one_sub_pow_mul {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) (w : 𝕜) : Multipliable fun (n : ℕ) => 1 - q ^ (n + 1) * w

For ‖q‖ < 1 the product ∏_{n ≥ 1} (1 - qⁿ w) converges.

theorem TauCeti.tendsto_tprod_one_sub_pow_mul {𝕜 : Type u_1} [NormedField 𝕜] {α : Type u_2} {l : Filter α} {q w : α → 𝕜} (hq : Filter.Tendsto q l (nhds 0)) (hqw : Filter.Tendsto (fun (x : α) => q x * w x) l (nhds 0)) : Filter.Tendsto (fun (x : α) => ∏' (n : ℕ), (1 - q x ^ (n + 1) * w x)) l (nhds 1)

The product ∏_{n ≥ 1} (1 - qⁿ w) tends to 1 whenever q → 0 and q w → 0. The argument w itself need not converge or remain bounded.

theorem TauCeti.tprod_one_sub_pow_mul_eq {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) (w : 𝕜) : ∏' (n : ℕ), (1 - q ^ (n + 1) * w) = (1 - q * w) * ∏' (n : ℕ), (1 - q ^ (n + 1) * (q * w))

Shifting the product: ∏_{n ≥ 1} (1 - qⁿ w) = (1 - q w) ∏_{n ≥ 1} (1 - qⁿ (q w)).

theorem TauCeti.tprod_one_sub_pow_mul_inv_eq {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) (hq₀ : q ≠ 0) (w : 𝕜) : ∏' (n : ℕ), (1 - q ^ (n + 1) * (q * w)⁻¹) = (1 - w⁻¹) * ∏' (n : ℕ), (1 - q ^ (n + 1) * w⁻¹)

Shifting the product with an inverted argument: ∏_{n ≥ 1} (1 - qⁿ (q w)⁻¹) = (1 - w⁻¹) ∏_{n ≥ 1} (1 - qⁿ w⁻¹) for q ≠ 0.

theorem TauCeti.tprod_one_sub_pow_mul_ne_zero {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) {w : 𝕜} (h : ∀ (n : ℕ), 1 - q ^ (n + 1) * w ≠ 0) : ∏' (n : ℕ), (1 - q ^ (n + 1) * w) ≠ 0

If the factors 1 - qⁿ⁺¹ w are nonzero, so is ∏_{n ≥ 1} (1 - qⁿ w).

theorem TauCeti.tprod_one_sub_pow_ne_zero {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) : ∏' (n : ℕ), (1 - q ^ (n + 1)) ≠ 0

For ‖q‖ < 1 the Euler function ∏_{n ≥ 1} (1 - qⁿ) is nonzero.

theorem TauCeti.multipliable_one_add_pow {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) : Multipliable fun (n : ℕ) => 1 + q ^ (n + 1)

For ‖q‖ < 1 the product ∏_{n ≥ 1} (1 + qⁿ) converges.

theorem TauCeti.multipliable_qTheta {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) (w : 𝕜) : Multipliable fun (n : ℕ) => (1 - q ^ (n + 1) * w) * (1 - q ^ (n + 1) * w⁻¹)

For ‖q‖ < 1 the product ∏_{n ≥ 1} (1 - qⁿ w) (1 - qⁿ w⁻¹) in the theta product converges.

theorem TauCeti.qTheta_eq_mul_tprod_mul_tprod {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) (w : 𝕜) : qTheta q w = (1 - w) * ((∏' (n : ℕ), (1 - q ^ (n + 1) * w)) * ∏' (n : ℕ), (1 - q ^ (n + 1) * w⁻¹))

For ‖q‖ < 1 the theta product θ_q(w) is 1 - w times its two half products ∏_{n ≥ 1} (1 - qⁿ w) and ∏_{n ≥ 1} (1 - qⁿ w⁻¹).

theorem TauCeti.norm_qTheta_le {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) (w : 𝕜) : ‖qTheta q w‖ ≤ ‖1 - w‖ * Real.exp (‖q‖ * (‖w‖ + ‖w‖⁻¹) / (1 - ‖q‖))

For ‖q‖ < 1 the theta product is bounded by ‖θ_q(w)‖ ≤ ‖1 - w‖ exp (‖q‖ (‖w‖ + ‖w‖⁻¹) / (1 - ‖q‖)).

theorem TauCeti.qTheta_ne_zero {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) {w : 𝕜} (hw : ∀ (k : ℤ), w ≠ q ^ k) : qTheta q w ≠ 0

For ‖q‖ < 1 the theta product θ_q(w) is nonzero when w is not an integral power of q.

theorem TauCeti.qTheta_mul_left {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) (hq₀ : q ≠ 0) {w : 𝕜} (hw : w ≠ 0) : qTheta q (q * w) = -w⁻¹ * qTheta q w

Quasi-periodicity of the theta product: θ_q(q w) = -w⁻¹ θ_q(w) for 0 < ‖q‖ < 1 and w ≠ 0.

theorem TauCeti.multipliable_one_sub_pow_odd {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) : Multipliable fun (n : ℕ) => 1 - q ^ (2 * n + 1)

For ‖q‖ < 1 the product ∏_{n ≥ 0} (1 - q^{2n+1}) over the odd powers of q converges.

theorem TauCeti.multipliable_one_add_pow_odd {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) : Multipliable fun (n : ℕ) => 1 + q ^ (2 * n + 1)

For ‖q‖ < 1 the product ∏_{n ≥ 0} (1 + q^{2n+1}) over the odd powers of q converges.

theorem TauCeti.tprod_one_sub_pow_odd_mul_tprod_one_add_pow_odd {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) : (∏' (n : ℕ), (1 - q ^ (2 * n + 1))) * ∏' (n : ℕ), (1 + q ^ (2 * n + 1)) = ∏' (n : ℕ), (1 - (q ^ 2) ^ (2 * n + 1))

∏_{n ≥ 0} (1 - q^{2n+1}) ∏_{n ≥ 0} (1 + q^{2n+1}) = ∏_{n ≥ 0} (1 - (q²)^{2n+1}) for ‖q‖ < 1.

theorem TauCeti.tprod_one_sub_pow_eq_tprod_one_sub_pow_odd_mul {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) : ∏' (n : ℕ), (1 - q ^ (n + 1)) = (∏' (n : ℕ), (1 - q ^ (2 * n + 1))) * ∏' (n : ℕ), (1 - (q ^ 2) ^ (n + 1))

The Euler product ∏_{n ≥ 1} (1 - qⁿ) split into its odd and even factors: ∏_{n ≥ 1} (1 - qⁿ) = ∏_{n ≥ 0} (1 - q^{2n+1}) ∏_{n ≥ 1} (1 - q^{2n}) for ‖q‖ < 1.

theorem TauCeti.tprod_one_add_pow_mul_tprod_one_sub_pow {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) : (∏' (n : ℕ), (1 + q ^ (n + 1))) * ∏' (n : ℕ), (1 - q ^ (n + 1)) = ∏' (n : ℕ), (1 - (q ^ 2) ^ (n + 1))

∏_{n ≥ 1} (1 + qⁿ) ∏_{n ≥ 1} (1 - qⁿ) = ∏_{n ≥ 1} (1 - q^{2n}) for ‖q‖ < 1.

theorem TauCeti.tprod_one_add_pow_mul_tprod_one_sub_pow_odd {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) : (∏' (n : ℕ), (1 + q ^ (n + 1))) * ∏' (n : ℕ), (1 - q ^ (2 * n + 1)) = 1

Euler's identity ∏_{n ≥ 1} (1 + qⁿ) ∏_{n ≥ 0} (1 - q^{2n+1}) = 1 for ‖q‖ < 1. Comparing coefficients, partitions into distinct parts and partitions into odd parts are equinumerous.

theorem TauCeti.tprod_one_sub_pow_odd_ne_zero {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) : ∏' (n : ℕ), (1 - q ^ (2 * n + 1)) ≠ 0

For ‖q‖ < 1 the product ∏_{n ≥ 0} (1 - q^{2n+1}) over the odd powers of q does not vanish: by Euler's identity it is the inverse of ∏_{n ≥ 1} (1 + qⁿ).

theorem TauCeti.qTheta_neg_one {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) : qTheta q (-1) = 2 * (∏' (n : ℕ), (1 + q ^ (n + 1))) ^ 2

The theta product at w = -1: θ_q(-1) = 2 (∏_{n ≥ 1} (1 + qⁿ))² for ‖q‖ < 1.

theorem TauCeti.qTheta_sq_self {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {s : 𝕜} (hs : ‖s‖ < 1) : qTheta (s ^ 2) s = (∏' (n : ℕ), (1 - s ^ (2 * n + 1))) ^ 2

The theta product with nome the square of its argument: θ_{s²}(s) = (∏_{n ≥ 0} (1 - s^{2n+1}))² for ‖s‖ < 1.

theorem TauCeti.qTheta_pow_three_self_mul {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {s : 𝕜} (hs : ‖s‖ < 1) : qTheta (s ^ 3) s * ∏' (n : ℕ), (1 - (s ^ 3) ^ (n + 1)) = ∏' (n : ℕ), (1 - s ^ (n + 1))

The theta product with nome the cube of its argument, times the Euler function of the nome, is the Euler function of the argument: θ_{s³}(s) ∏_{n ≥ 1} (1 - s^{3n}) = ∏_{n ≥ 1} (1 - sⁿ) for ‖s‖ < 1.

theorem TauCeti.qTheta_mul_tprod_of_sq_add_add_one_eq_zero {𝕜 : Type u_1} [NormedField 𝕜] [CompleteSpace 𝕜] {q ω : 𝕜} (hq : ‖q‖ < 1) (hω : ω ^ 2 + ω + 1 = 0) : qTheta q ω * ∏' (n : ℕ), (1 - q ^ (n + 1)) = (1 - ω) * ∏' (n : ℕ), (1 - (q ^ 3) ^ (n + 1))

The theta product at a primitive cube root of unity, times the Euler function of the nome: if ω² + ω + 1 = 0 then θ_q(ω) ∏_{n ≥ 1} (1 - qⁿ) = (1 - ω) ∏_{n ≥ 1} (1 - q^{3n}) for ‖q‖ < 1.

theorem TauCeti.hasDerivAt_tprod_one_sub_pow_odd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] : HasDerivAt (fun (s : 𝕜) => ∏' (n : ℕ), (1 - s ^ (2 * n + 1))) (-1) 0

Near s = 0 the odd product is ∏_{n ≥ 0} (1 - s^{2n+1}) = 1 - s + O(s²): it has derivative -1 at 0.

theorem TauCeti.tendsto_tprod_one_sub_pow_odd_pow_sub_neg_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] (k : ℕ) : Filter.Tendsto (fun (s : 𝕜) => ((∏' (n : ℕ), (1 - s ^ (2 * n + 1))) ^ k - (∏' (n : ℕ), (1 - (-s) ^ (2 * n + 1))) ^ k) / s) (nhdsWithin 0 {0}ᶜ) (nhds (-(2 * ↑k)))

The odd difference quotient of a power P(s)ᵏ of the odd product P(s) = ∏_{n ≥ 0} (1 - s^{2n+1}) tends to -2k at s = 0: (P(s)ᵏ - P(-s)ᵏ) / s → -2k, since P(s)ᵏ = 1 - k s + O(s²).

theorem TauCeti.tendsto_tprod_one_sub_qParam_pow_odd_pow (k : ℕ) : Filter.Tendsto (fun (τ : UpperHalfPlane) => (∏' (n : ℕ), (1 - Function.Periodic.qParam 1 ↑τ ^ (2 * n + 1))) ^ k) UpperHalfPlane.atImInfty (nhds 1)

(∏_{n ≥ 0} (1 - q^{2n+1}))ᵏ → 1 at i∞, for q = e^{2π i τ}.

theorem TauCeti.hasProdLocallyUniformlyOn_one_sub_pow_mul {q w : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (hq : ContinuousOn q U) (hq₁ : ∀ τ ∈ U, ‖q τ‖ < 1) (hw : ContinuousOn w U) : HasProdLocallyUniformlyOn (fun (n : ℕ) (τ : ℂ) => 1 - q τ ^ (n + 1) * w τ) (fun (τ : ℂ) => ∏' (n : ℕ), (1 - q τ ^ (n + 1) * w τ)) U

For q and w continuous on an open set U with ‖q‖ < 1 on U, the product ∏_{n ≥ 1} (1 - q(τ)ⁿ w(τ)) converges locally uniformly on U.

theorem TauCeti.differentiableOn_tprod_one_sub_pow_mul {q w : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (hq : DifferentiableOn ℂ q U) (hq₁ : ∀ τ ∈ U, ‖q τ‖ < 1) (hw : DifferentiableOn ℂ w U) : DifferentiableOn ℂ (fun (τ : ℂ) => ∏' (n : ℕ), (1 - q τ ^ (n + 1) * w τ)) U

For q and w holomorphic on an open set U with ‖q‖ < 1 on U, the product ∏_{n ≥ 1} (1 - q(τ)ⁿ w(τ)) is holomorphic on U.

theorem TauCeti.differentiableOn_qTheta {q : ℂ} (hq : ‖q‖ < 1) : DifferentiableOn ℂ (qTheta q) {0}ᶜ

For ‖q‖ < 1 the theta product w ↦ θ_q(w) is holomorphic on ℂ \ {0}.

theorem TauCeti.hasDerivAt_qTheta_one {q : ℂ} (hq : ‖q‖ < 1) : HasDerivAt (qTheta q) (-(∏' (n : ℕ), (1 - q ^ (n + 1))) ^ 2) 1

For ‖q‖ < 1 the theta product has a simple zero at w = 1: its derivative there is -(∏_{n ≥ 1} (1 - qⁿ))².

theorem TauCeti.differentiable_qTheta_exp {q : ℂ} (hq : ‖q‖ < 1) : Differentiable ℂ fun (z : ℂ) => qTheta q (Complex.exp (2 * ↑Real.pi * Complex.I * z))

For ‖q‖ < 1, z ↦ θ_q(e^{2π i z}) is an entire function.

theorem TauCeti.hasDerivAt_qTheta_exp_zero {q : ℂ} (hq : ‖q‖ < 1) : HasDerivAt (fun (z : ℂ) => qTheta q (Complex.exp (2 * ↑Real.pi * Complex.I * z))) (-(2 * ↑Real.pi * Complex.I) * (∏' (n : ℕ), (1 - q ^ (n + 1))) ^ 2) 0

For ‖q‖ < 1 the derivative of z ↦ θ_q(e^{2π i z}) at z = 0 is -2π i (∏_{n ≥ 1} (1 - qⁿ))².