qExpansion_coeff — Mathlib

English

The m-th coefficient of the q-expansion qExpansion n f is the factorial-weighted m-th derivative of cuspFunction evaluated at 0.

Русский

Коэффициент m в q-разложении qExpansion n f равен (m!)^{-1} раз derivative cuspFunction n f на нуле, как в формуле: (qExpansion n f).coeff m = (m!)^{-1} · (d^m/dx^m cuspFunction n f)(0).

LaTeX

$$$ (qExpansion n f).\text{coeff} \\ m = (m!)^{-1} \cdot D^m (\text{cuspFunction } n\, f) \big|_{0}$$$

Lean4

theorem qExpansion_coeff (m : ℕ) : (qExpansion n f).coeff m = (↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction n f) 0 :=
  by simp [qExpansion]

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