norm_jacobiTheta_sub_one_le
theorem norm_jacobiTheta_sub_one_le :
∀ {τ : ℂ}, 0 < τ.im → ‖jacobiTheta τ - 1‖ ≤ 2 / (1 - (-Real.pi * τ.im).exp) * (-Real.pi * τ.im).exp
This theorem provides an explicit upper bound for the absolute difference between the Jacobi's one-variable theta function and 1. For any complex number 'τ' with its imaginary part greater than zero, the norm (or absolute value) of the difference between the theta function at 'τ' and 1 is less than or equal to twice the exponential of the negative product of π and the imaginary part of 'τ', divided by (1 minus the exponential of the negative product of π and the imaginary part of 'τ').
More concisely: For any complex number τ with positive imaginary part, the norm of the difference between the Jacobi theta function evaluated at τ and 1 is bounded by $2\cdot e^{-\pi\cdot\text{Im}(\tau)}/\left(1-e^{-\pi\cdot\text{Im}(\tau)}\right)$.
|
jacobiTheta_eq_jacobiTheta₂
theorem jacobiTheta_eq_jacobiTheta₂ : ∀ (τ : ℂ), jacobiTheta τ = jacobiTheta₂ 0 τ
This theorem states that for every complex number τ, the Jacobi one-variable theta function `jacobiTheta τ`, which is defined as the sum over all integers n of the complex exponential function `exp (π * I * n ^ 2 * τ)`, is equal to the Jacobi two-variable theta function `jacobiTheta₂ 0 τ`, which is defined as the sum over all integers n of the complex exponential function `exp (2 * π * I * n * 0 + π * I * n ^ 2 * τ)`. In other words, when the first argument of the two-variable Jacobi theta function is zero, it simplifies to the one-variable Jacobi theta function.
More concisely: The one-variable Jacobi theta function equals the zero-first-argument two-variable Jacobi theta function. Specifically, for all complex numbers τ, `jacobiTheta τ = jacobiTheta₂ 0 τ`.
|
isBigO_at_im_infty_jacobiTheta_sub_one
theorem isBigO_at_im_infty_jacobiTheta_sub_one :
(fun τ => jacobiTheta τ - 1) =O[Filter.comap Complex.im Filter.atTop] fun τ => (-Real.pi * τ.im).exp
This theorem states that the norm of the difference between the Jacobi Theta function of a complex number `τ` and `1` decays exponentially as the imaginary part of `τ` approaches infinity. In other words, as the imaginary part of `τ` increases without limit, the difference between the value of the Jacobi Theta function at `τ` and `1` gets arbitrarily close to zero at a rate that is proportional to the exponential of the negative product of the mathematical constant π and the imaginary part of `τ`. In mathematical notation, this is expressed as `|jacobiTheta(τ) - 1| = O(e^(-π * Im(τ)))` as `Im(τ) → ∞`.
More concisely: As the imaginary part of `τ` approaches infinity, the difference between `jacobiTheta(τ)` and `1` decreases exponentially, with rate proportional to `e^(-π * Im(τ))`.
|