English
For given n,z,τ the map p ↦ jacobiTheta₂_term n p.1 p.2 has Fréchet derivative jacobiTheta₂_term_fderiv n z τ at (z,τ).
Русский
Для заданных n,z,τ отображение p ↦ jacobiTheta₂_term n p1 p2 имеет производную Фреше: jacobiTheta₂_term_fderiv n z τ в точке (z,τ).
LaTeX
$$$\text{HasFDerivAt}\bigl( p \mapsto \ jacobiTheta_2\_term(n,p_1,p_2)\bigr)\big|_{(z,\tau)} = \ jacobiTheta_2\_term\_fderiv(n,z,\tau) $$$
Lean4
theorem hasFDerivAt_jacobiTheta₂_term (n : ℤ) (z τ : ℂ) :
HasFDerivAt (fun p : ℂ × ℂ ↦ jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ) :=
by
let f : ℂ × ℂ → ℂ := fun p ↦ 2 * π * I * n * p.1 + π * I * n ^ 2 * p.2
suffices
HasFDerivAt f
((2 * π * I * n) • (ContinuousLinearMap.fst ℂ ℂ ℂ) + (π * I * n ^ 2) • (ContinuousLinearMap.snd ℂ ℂ ℂ)) (z, τ)
from this.cexp
exact (hasFDerivAt_fst.const_mul _).add (hasFDerivAt_snd.const_mul _)
