ncoeff_eq_zero_of_lt_order — Mathlib

English

If the order is greater than a given bound, the corresponding coefficient vanishes: for suitable h, (A[[n]]) x = 0.

Русский

При достаточно больших порядках соответствующий коэффициент обнуляется: при подходящем ограничении h выполняется (A[[n]]) x = 0.

LaTeX

$$$(A[[n]]) x = 0\quad \text{if } -n-1 < \mathrm{order}\big((HahnModule.of R)^{-1}(A x)\big)$$$

Lean4

theorem ncoeff_eq_zero_of_lt_order (A : VertexOperator R V) (n : ℤ) (x : V)
    (h : -n - 1 < HahnSeries.order ((HahnModule.of R).symm (A x))) : (A[[n]]) x = 0 :=
  by
  simp only [ncoeff, HVertexOperator.coeff, LinearMap.coe_mk, AddHom.coe_mk]
  exact HahnSeries.coeff_eq_zero_of_lt_order h

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