mathlib3 documentation

number_theory.modular_forms.jacobi_theta.manifold

Manifold differentiability of the Jacobi's theta function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we reformulate differentiability of the Jacobi's theta function in terms of manifold differentiability.

TODO #

Prove smoothness (in terms of smooth).

source
theorem mdifferentiable_jacobi_theta  :
mdifferentiable (model_with_corners_self ℂ ℂ) (model_with_corners_self ℂ ℂ) (jacobi_theta ∘ coe)