qExpansionFormalMultilinearSeries_apply_norm

English

The radius of convergence of the qExpansionFormalMultilinearSeries is at least 1 (in the appropriate norm), i.e., it has radius ≥ 1.

Русский

Радиус сходимости qExpansionFormalMultilinearSeries не меньше 1 (в соответствующей норме).

LaTeX

$$$1 \le (qExpansionFormalMultilinearSeries n f).radius$$$

Lean4

theorem qExpansionFormalMultilinearSeries_apply_norm (m : ℕ) :
    ‖qExpansionFormalMultilinearSeries n f m‖ = ‖(qExpansion n f).coeff m‖ :=
  by
  rw [qExpansionFormalMultilinearSeries, ← (ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ).symm.norm_map]
  simp

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