Limits at infinity

In this file we prove the limit of Θᵢ(z) as z tends to i∞. This will be useful as we do computations with Fourier coefficients, e.g. comparing two q-expansions. This is also useful when we compute limits of forms later on (following Seewoo's approach).

theorem Int.ne_half (a : ℤ) : ↑a ≠ 1 / 2

theorem jacobiTheta₂_half_mul_apply_tendsto_atImInfty : Filter.Tendsto (fun (x : UpperHalfPlane) => jacobiTheta₂ (↑x / 2) ↑x) UpperHalfPlane.atImInfty (nhds 2)

theorem jacobiTheta₂_zero_apply_tendsto_atImInfty : Filter.Tendsto (fun (x : UpperHalfPlane) => jacobiTheta₂ 0 ↑x) UpperHalfPlane.atImInfty (nhds 1)

theorem jacobiTheta₂_half_apply_tendsto_atImInfty : Filter.Tendsto (fun (x : UpperHalfPlane) => jacobiTheta₂ (1 / 2) ↑x) UpperHalfPlane.atImInfty (nhds 1)

theorem Θ₂_tendsto_atImInfty : Filter.Tendsto Θ₂ UpperHalfPlane.atImInfty (nhds 0)

theorem Θ₃_tendsto_atImInfty : Filter.Tendsto Θ₃ UpperHalfPlane.atImInfty (nhds 1)

theorem Θ₄_tendsto_atImInfty : Filter.Tendsto Θ₄ UpperHalfPlane.atImInfty (nhds 1)

theorem H₂_tendsto_atImInfty : Filter.Tendsto H₂ UpperHalfPlane.atImInfty (nhds 0)

theorem H₃_tendsto_atImInfty : Filter.Tendsto H₃ UpperHalfPlane.atImInfty (nhds 1)

theorem H₄_tendsto_atImInfty : Filter.Tendsto H₄ UpperHalfPlane.atImInfty (nhds 1)