qExpansionFormalMultilinearSeries_radius

English

The formal multilinear series evaluated at m coheres with the m-th coefficient of the qExpansion n f via a canonical isomorphism.

Русский

Формальная многообразная серия согласуется с коэффициентом qExpansion через каноническое изоморование.

LaTeX

$$$qExpansionFormalMultilinearSeries\; n\; f (m) = \text{coeff}_{m}(qExpansion n f)$$$

Lean4

theorem qExpansionFormalMultilinearSeries_radius [NeZero n] [ModularFormClass F Γ(n) k] :
    1 ≤ (qExpansionFormalMultilinearSeries n f).radius :=
  by
  refine le_of_forall_lt_imp_le_of_dense fun r hr ↦ ?_
  lift r to NNReal using hr.ne_top
  apply FormalMultilinearSeries.le_radius_of_summable
  simp only [qExpansionFormalMultilinearSeries_apply_norm]
  rw [← r.abs_eq]
  simp_rw [← Real.norm_eq_abs, ← Complex.norm_real, ← norm_pow, ← norm_mul]
  exact (hasSum_qExpansion_of_abs_lt n f (q := r) (by simpa using hr)).summable.norm

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