eq_cuspFunction — Mathlib

English

For NeZero n and appropriate modular form data, cuspFunction n f evaluated at qParam(τ) equals f(τ).

Русский

Для непустого n и подходящих данных модульной формы, cuspFunction n f по qParam(τ) возвращает f(τ).

LaTeX

$$$\text{cuspFunction } n\, f\bigl( \mathbb{Q}_n(\tau) \bigr) = f(\tau)$$$

Lean4

theorem eq_cuspFunction [NeZero n] [SlashInvariantFormClass F Γ(n) k] (τ : ℍ) : cuspFunction n f (𝕢 n τ) = f τ := by
  simpa only [comp_apply, ofComplex_apply] using (periodic_comp_ofComplex n f).eq_cuspFunction (NeZero.ne _) τ

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