jacobiTheta₂_neg_left
theorem jacobiTheta₂_neg_left : ∀ (z τ : ℂ), jacobiTheta₂ (-z) τ = jacobiTheta₂ z τ
This theorem states that the two-variable Jacobi theta function, denoted as `jacobiTheta₂`, exhibits the property of being even in its first variable `z`. In other words, for any complex numbers `z` and `τ`, the value of `jacobiTheta₂` at `(-z, τ)` is equal to its value at `(z, τ)`. This is mathematically expressed as `jacobiTheta₂(-z, τ) = jacobiTheta₂(z, τ)`.
More concisely: The two-variable Jacobi theta function `jacobiTheta₂` is even in its first variable, i.e., `jacobiTheta₂(-z, τ) = jacobiTheta₂(z, τ)` for all complex numbers `z` and `τ`.
|
jacobiTheta₂_add_left'
theorem jacobiTheta₂_add_left' :
∀ (z τ : ℂ), jacobiTheta₂ (z + τ) τ = (-↑Real.pi * Complex.I * (τ + 2 * z)).exp * jacobiTheta₂ z τ
The theorem `jacobiTheta₂_add_left'` states that the two-variable Jacobi theta function, `jacobiTheta₂`, exhibits quasi-periodicity in its first variable `z` with period `τ`. More specifically, for any complex numbers `z` and `τ`, the value of the Jacobi theta function at `z + τ` is equal to the exponential of negative pi times the imaginary unit times `τ + 2z`, all multiplied by the value of the Jacobi theta function at `z`.
This is expressed mathematically as `jacobiTheta₂(z + τ, τ) = e^{-πi(τ + 2z)} * jacobiTheta₂(z, τ)`.
More concisely: The two-variable Jacobi theta function `jacobiTheta₂` satisfies the quasi-periodicity property `jacobiTheta₂(z + τ, τ) = e^{-πi(τ + 2z)} * jacobiTheta₂(z, τ)`.
|
jacobiTheta₂_add_right
theorem jacobiTheta₂_add_right : ∀ (z τ : ℂ), jacobiTheta₂ z (τ + 2) = jacobiTheta₂ z τ
The theorem `jacobiTheta₂_add_right` states that the two-variable Jacobi theta function, denoted as `θ z τ = ∑' (n : ℤ), cexp (2 * π * I * n * z + π * I * n ^ 2 * τ)`, has a periodicity in `τ` of period 2. More specifically, for any complex numbers `z` and `τ`, the value of the Jacobi theta function at `τ + 2` is equal to its value at `τ`, that is `θ(z, τ + 2) = θ(z, τ)`.
More concisely: The two-variable Jacobi theta function `θ(z, τ)` is periodic with period 2 in `τ`.
|
jacobiTheta₂_add_left
theorem jacobiTheta₂_add_left : ∀ (z τ : ℂ), jacobiTheta₂ (z + 1) τ = jacobiTheta₂ z τ
The theorem states that the two-variable Jacobi theta function, denoted as `θ z τ = ∑' (n : ℤ), cexp (2 * π * I * n * z + π * I * n ^ 2 * τ)`, is periodic in its first variable `z` with a period of 1. In other words, for any complex numbers `z` and `τ`, the value of the Jacobi theta function at `z + 1` and `τ` is the same as its value at `z` and `τ`.
More concisely: The two-variable Jacobi theta function `θ z τ` is periodic in `z` with period 1.
|
jacobiTheta₂_functional_equation
theorem jacobiTheta₂_functional_equation :
∀ (z τ : ℂ),
jacobiTheta₂ z τ =
1 / (-Complex.I * τ) ^ (1 / 2) * (-↑Real.pi * Complex.I * z ^ 2 / τ).exp * jacobiTheta₂ (z / τ) (-1 / τ)
The theorem `jacobiTheta₂_functional_equation` states that for any two complex numbers `z` and `τ`, the Jacobi theta function `jacobiTheta₂ z τ` is equal to a factor composed of complex and real numbers and functions, times `jacobiTheta₂ (z / τ) (-1 / τ)`. More specifically, the factor is the inverse of `(-Complex.I * τ) ^ (1 / 2)`, multiplied by the exponential of `(-↑Real.pi * Complex.I * z ^ 2 / τ)`, where `Complex.I` represents the imaginary unit, `Real.pi` represents the value of Pi, and `exp` is the exponential function. This theorem is a key lemma behind the proof of the functional equation for L-series of even Dirichlet characters.
More concisely: The Jacobi theta function `jacobiTheta₂` satisfies the functional equation `jacobiTheta₂ z τ = (1 / ( Complex.I * τ ^ 0.5) * exp(-Real.pi * Complex.I * z ^ 2 / τ)) * jacobiTheta₂ (z / τ) (-1 / τ)`.
|