English
For z ∈ ℂ and τ with im τ > 0, HasDerivAt (z ↦ θ₂(z,τ)) equals the derivative θ₂'(z,τ) in z.
Русский
Для фиксированного τ с положительной мнимая частью и переменной z функция z ↦ θ₂(z,τ) имеет производную θ₂'(z,τ).
LaTeX
$$$\text{HasDerivAt}(\lambda z. \theta_2(z,\tau), \theta_2'(z,\tau), z).$$$
Lean4
theorem hasDerivAt_jacobiTheta₂_fst (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :
HasDerivAt (jacobiTheta₂ · τ) (jacobiTheta₂' z τ) z := by
-- This proof is annoyingly fiddly, because of the need to commute "evaluation at a point"
-- through infinite sums of continuous linear maps.
let eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
{ toFun := fun f ↦ f (1, 0)
cont := continuous_id'.clm_apply continuous_const
map_add' := by simp only [ContinuousLinearMap.add_apply, forall_const]
map_smul' := by
simp only [ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul, RingHom.id_apply, forall_const] }
have step1 : HasSum (fun n ↦ (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0)) := by
apply eval_fst_CLM.hasSum (hasSum_jacobiTheta₂_term_fderiv z hτ)
have step2 (n : ℤ) : (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ := by
simp only [jacobiTheta₂_term_fderiv, smul_add, ContinuousLinearMap.add_apply, ContinuousLinearMap.coe_smul',
ContinuousLinearMap.coe_fst', Pi.smul_apply, smul_eq_mul, mul_one, ContinuousLinearMap.coe_snd', mul_zero,
add_zero, jacobiTheta₂'_term, jacobiTheta₂_term, mul_comm _ (cexp _)]
rw [funext step2] at step1
have step3 : HasDerivAt (fun x ↦ jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ) (1, 0)) z :=
(((hasFDerivAt_jacobiTheta₂ z hτ).comp z (hasFDerivAt_prodMk_left z τ)).hasDerivAt :)
rwa [← step1.tsum_eq] at step3
