eq_cuspFunction — Mathlib

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

Похожие утверждения