Optimal Gabor frame bounds for separable lattices and estimates for Jacobi theta functions

We study sharp frame bounds of Gabor frames for integer redundancy with the standard Gaussian window and prove that the square lattice optimizes both the lower and the upper frame bound among all rectangular lattices. This proves a conjecture of Floch, Alard & Berrou (as reformulated by Strohmer & Beaver). The proof is based on refined log-convexity/concavity estimates for the Jacobi theta functions θ3θ3 and θ4θ4.