analyticAt_cuspFunction_zero — Mathlib

English

If f is modular of level Γ(n) with finite index and 0 < Im τ in appropriate domain, then the composed function f ∘ ofComplex is bounded towards I∞.

Русский

Для модулярной формы f на Γ(n) с конечным индексом композиция f ∘ ofComplex остаётся ограниченной в бесконечности.

LaTeX

$$$\text{BoundedAtFilter}(I_∞, f \circ \mathrm{ofComplex})$$$

Lean4

theorem analyticAt_cuspFunction_zero [NeZero n] [ModularFormClass F Γ(n) k] : AnalyticAt ℂ (cuspFunction n f) 0 :=
  DifferentiableOn.analyticAt (fun q hq ↦ (differentiableAt_cuspFunction _ _ hq).differentiableWithinAt)
    (by simpa only [ball_zero_eq] using Metric.ball_mem_nhds (0 : ℂ) zero_lt_one)

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