Documentation

Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

The two-variable Jacobi theta function #

This file defines the two-variable Jacobi theta function

$$\theta(z, \tau) = \sum_{n \in \mathbb{Z}} \exp (2 i \pi n z + i \pi n ^ 2 \tau),$$

and proves the functional equation relating the values at (z, τ) and (z / τ, -1 / τ), using Poisson's summation formula. We also show holomorphy (jointly in both variables).

Additionally, we show some analogous results about the derivative (in the z-variable)

$$\theta'(z, τ) = \sum_{n \in \mathbb{Z}} 2 \pi i n \exp (2 i \pi n z + i \pi n ^ 2 \tau).$$

(Note that the Mellin transform of θ will give us functional equations for L-functions of even Dirichlet characters, and that of θ' will do the same for odd Dirichlet characters.)

Definitions of the summands #

def jacobiTheta₂_term (n : ) (z : ) (τ : ) :

Summand in the series for the Jacobi theta function.

Equations
Instances For

    Summand in the series for the Fréchet derivative of the Jacobi theta function.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem hasFDerivAt_jacobiTheta₂_term (n : ) (z : ) (τ : ) :
      HasFDerivAt (fun (p : × ) => jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ)
      def jacobiTheta₂'_term (n : ) (z : ) (τ : ) :

      Summand in the series for the z-derivative of the Jacobi theta function.

      Equations
      Instances For

        Bounds for the summands #

        We show that the sums of the three functions jacobiTheta₂_term, jacobiTheta₂'_term and jacobiTheta₂_term_fderiv are locally uniformly convergent in the domain 0 < im τ, and diverge everywhere else.

        theorem norm_jacobiTheta₂_term (n : ) (z : ) (τ : ) :
        jacobiTheta₂_term n z τ = Real.exp (-Real.pi * n ^ 2 * τ.im - 2 * Real.pi * n * z.im)
        theorem norm_jacobiTheta₂_term_le {S : } {T : } (hT : 0 < T) {z : } {τ : } (hz : |z.im| S) (hτ : T τ.im) (n : ) :
        jacobiTheta₂_term n z τ Real.exp (-Real.pi * (T * n ^ 2 - 2 * S * |n|))

        A uniform upper bound for jacobiTheta₂_term on compact subsets.

        theorem norm_jacobiTheta₂'_term_le {S : } {T : } (hT : 0 < T) {z : } {τ : } (hz : |z.im| S) (hτ : T τ.im) (n : ) :
        jacobiTheta₂'_term n z τ 2 * Real.pi * |n| * Real.exp (-Real.pi * (T * n ^ 2 - 2 * S * |n|))

        A uniform upper bound for jacobiTheta₂'_term on compact subsets.

        theorem summable_pow_mul_jacobiTheta₂_term_bound (S : ) {T : } (hT : 0 < T) (k : ) :
        Summable fun (n : ) => |n| ^ k * Real.exp (-Real.pi * (T * n ^ 2 - 2 * S * |n|))

        The uniform bound we have given is summable, and remains so after multiplying by any fixed power of |n| (we shall need this for k = 0, 1, 2).

        theorem summable_jacobiTheta₂_term_iff (z : ) (τ : ) :
        (Summable fun (x : ) => jacobiTheta₂_term x z τ) 0 < τ.im

        The series defining the theta function is summable if and only if 0 < im τ.

        theorem summable_jacobiTheta₂'_term_iff (z : ) (τ : ) :
        (Summable fun (x : ) => jacobiTheta₂'_term x z τ) 0 < τ.im

        Definitions of the functions #

        def jacobiTheta₂ (z : ) (τ : ) :

        The two-variable Jacobi theta function, θ z τ = ∑' (n : ℤ), cexp (2 * π * I * n * z + π * I * n ^ 2 * τ).

        Equations
        Instances For

          Fréchet derivative of the two-variable Jacobi theta function.

          Equations
          Instances For
            def jacobiTheta₂' (z : ) (τ : ) :

            The z-derivative of the Jacobi theta function, θ' z τ = ∑' (n : ℤ), 2 * π * I * n * cexp (2 * π * I * n * z + π * I * n ^ 2 * τ).

            Equations
            Instances For
              theorem hasSum_jacobiTheta₂_term (z : ) {τ : } (hτ : 0 < τ.im) :
              HasSum (fun (n : ) => jacobiTheta₂_term n z τ) (jacobiTheta₂ z τ)
              theorem hasSum_jacobiTheta₂_term_fderiv (z : ) {τ : } (hτ : 0 < τ.im) :
              theorem hasSum_jacobiTheta₂'_term (z : ) {τ : } (hτ : 0 < τ.im) :
              HasSum (fun (n : ) => jacobiTheta₂'_term n z τ) (jacobiTheta₂' z τ)
              theorem jacobiTheta₂_undef (z : ) {τ : } (hτ : τ.im 0) :
              theorem jacobiTheta₂_fderiv_undef (z : ) {τ : } (hτ : τ.im 0) :
              theorem jacobiTheta₂'_undef (z : ) {τ : } (hτ : τ.im 0) :

              Derivatives and continuity #

              theorem hasFDerivAt_jacobiTheta₂ (z : ) {τ : } (hτ : 0 < τ.im) :
              HasFDerivAt (fun (p : × ) => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
              theorem continuousAt_jacobiTheta₂ (z : ) {τ : } (hτ : 0 < τ.im) :
              ContinuousAt (fun (p : × ) => jacobiTheta₂ p.1 p.2) (z, τ)
              theorem differentiableAt_jacobiTheta₂_fst (z : ) {τ : } (hτ : 0 < τ.im) :
              DifferentiableAt (fun (x : ) => jacobiTheta₂ x τ) z

              Differentiability of Θ z τ in z, for fixed τ.

              theorem differentiableAt_jacobiTheta₂_snd (z : ) {τ : } (hτ : 0 < τ.im) :

              Differentiability of Θ z τ in τ, for fixed z.

              theorem hasDerivAt_jacobiTheta₂_fst (z : ) {τ : } (hτ : 0 < τ.im) :
              HasDerivAt (fun (x : ) => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
              theorem continuousAt_jacobiTheta₂' (z : ) {τ : } (hτ : 0 < τ.im) :
              ContinuousAt (fun (p : × ) => jacobiTheta₂' p.1 p.2) (z, τ)

              Periodicity and conjugation #

              theorem jacobiTheta₂_add_right (z : ) (τ : ) :

              The two-variable Jacobi theta function is periodic in τ with period 2.

              theorem jacobiTheta₂_add_left (z : ) (τ : ) :

              The two-variable Jacobi theta function is periodic in z with period 1.

              theorem jacobiTheta₂_add_left' (z : ) (τ : ) :

              The two-variable Jacobi theta function is quasi-periodic in z with period τ.

              The two-variable Jacobi theta function is even in z.

              Functional equations #

              theorem jacobiTheta₂_functional_equation (z : ) (τ : ) :
              jacobiTheta₂ z τ = 1 / (-Complex.I * τ) ^ (1 / 2) * Complex.exp (-Real.pi * Complex.I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

              The functional equation for the Jacobi theta function: jacobiTheta₂ z τ is an explicit factor times jacobiTheta₂ (z / τ) (-1 / τ). This is the key lemma behind the proof of the functional equation for L-series of even Dirichlet characters.

              theorem jacobiTheta₂'_functional_equation (z : ) (τ : ) :
              jacobiTheta₂' z τ = 1 / (-Complex.I * τ) ^ (1 / 2) * Complex.exp (-Real.pi * Complex.I * z ^ 2 / τ) / τ * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * Real.pi * Complex.I * z * jacobiTheta₂ (z / τ) (-1 / τ))

              The functional equation for the derivative of the Jacobi theta function, relating jacobiTheta₂' z τ to jacobiTheta₂' (z / τ) (-1 / τ). This is the key lemma behind the proof of the functional equation for L-series of odd Dirichlet characters.