English
Given a SlashInvariantFormClass f of level Γ(n) and weight k, the function f ∘ ofComplex is periodic with period n; i.e., f( z + n ) equals f(z) after appropriate action.
Русский
У функции f ∘ ofComplex есть период n: f( z + n ) повторяет значения через соответствующее действие.
LaTeX
$$$\text{Periodic }(f \circ \mathrm{ofComplex})\, n$$$
Lean4
theorem periodic_comp_ofComplex [SlashInvariantFormClass F Γ(n) k] : Periodic (f ∘ ofComplex) n :=
by
intro w
by_cases hw : 0 < im w
· have : 0 < im (w + n) := by simp only [add_im, natCast_im, add_zero, hw]
simp only [comp_apply, ofComplex_apply_of_im_pos this, ofComplex_apply_of_im_pos hw]
convert SlashInvariantForm.vAdd_width_periodic n k 1 f ⟨w, hw⟩ using 2
simp only [Int.cast_one, mul_one, UpperHalfPlane.ext_iff, coe_mk_subtype, coe_vadd, ofReal_natCast, add_comm]
· have : im (w + n) ≤ 0 := by simpa only [add_im, natCast_im, add_zero, not_lt] using hw
simp only [comp_apply, ofComplex_apply_of_im_nonpos this, ofComplex_apply_of_im_nonpos (not_lt.mp hw)]
