English
If h ≠ 0 and f is periodic with period h, then cuspFunction(h, f)(qParam(h, z)) = f(z).
Русский
Если h ≠ 0 и f периодична с периодом h, то cuspFunction(h,f)(qParam(h,z)) = f(z).
LaTeX
$$$h \neq 0 \land \text{Periodic}(f,h) \Rightarrow cuspFunction(h,f)(qParam(h,z)) = f(z)$$$
Lean4
theorem eq_cuspFunction (hh : h ≠ 0) (hf : Periodic f h) (z : ℂ) : (cuspFunction h f) (𝕢 h z) = f z :=
by
have : (cuspFunction h f) (𝕢 h z) = f (invQParam h (𝕢 h z)) :=
by
rw [cuspFunction, update_of_ne, comp_apply]
exact exp_ne_zero _
obtain ⟨m, hm⟩ := qParam_left_inv_mod_period hh z
simpa only [this, hm] using hf.int_mul m z