English
The function r1 is a real-valued function on the upper half-plane, given by r1(z) = Im(z)^2 / (Re(z)^2 + Im(z)^2).
Русский
Функция r1 представляет собой вещественную функцию на верхней полуплоскости: r1(z) = Im(z)^2 / (Re(z)^2 + Im(z)^2).
LaTeX
$$$r_1(z) = \dfrac{\operatorname{Im}(z)^2}{\operatorname{Re}(z)^2 + \operatorname{Im}(z)^2}$$$
Lean4
theorem hasFDerivAt_jacobiTheta₂ (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :
HasFDerivAt (fun p : ℂ × ℂ ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ) :=
by
obtain ⟨T, hT, hτ'⟩ := exists_between hτ
obtain ⟨S, hz⟩ := exists_gt |im z|
let V := {u | |im u| < S} ×ˢ {v | T < im v}
have hVo : IsOpen V :=
by
refine ((_root_.continuous_abs.comp continuous_im).isOpen_preimage _ isOpen_Iio).prod ?_
exact continuous_im.isOpen_preimage _ isOpen_Ioi
have hVmem : (z, τ) ∈ V := ⟨hz, hτ'⟩
have hVp : IsPreconnected V :=
by
refine (Convex.isPreconnected ?_).prod (convex_halfSpace_im_gt T).isPreconnected
simpa only [abs_lt] using (convex_halfSpace_im_gt _).inter (convex_halfSpace_im_lt _)
let f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
let f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
have hf (n : ℤ) : ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p := fun p _ ↦ hasFDerivAt_jacobiTheta₂_term n p.1 p.2
let u : ℤ → ℝ := fun n ↦ 3 * π * |n| ^ 2 * Real.exp (-π * (T * n ^ 2 - 2 * S * |n|))
have hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n :=
by
refine fun n p hp ↦ (norm_jacobiTheta₂_term_fderiv_le n p.1 p.2).trans ?_
refine mul_le_mul_of_nonneg_left ?_ (by positivity)
exact norm_jacobiTheta₂_term_le hT (le_of_lt hp.1) (le_of_lt hp.2) n
have hu_sum : Summable u := by
simp_rw [u, mul_assoc (3 * π)]
exact (summable_pow_mul_jacobiTheta₂_term_bound S hT 2).mul_left _
have hf_sum : Summable fun n : ℤ ↦ f n (z, τ) :=
by
refine (summable_pow_mul_jacobiTheta₂_term_bound S hT 0).of_norm_bounded ?_
simpa only [pow_zero, one_mul] using norm_jacobiTheta₂_term_le hT hz.le hτ'.le
simpa only [jacobiTheta₂, jacobiTheta₂_fderiv, f, f'] using
hasFDerivAt_tsum_of_isPreconnected hu_sum hVo hVp hf hu hVmem hf_sum hVmem
