English
Let f: Z → End_R(V) be an endomorphism-valued function such that for every x ∈ V there exists n ∈ Z with f(m)(x) = 0 for all m < n. Then there exists a VertexOperator R V whose coefficients reproduce f, i.e., for all x ∈ V and all n ∈ Z, the n-th coefficient of the operator acting on x equals f(n) x.
Русский
Пусть f: Z → End_R(V) задана как функция, принимающая целочисленные индексы в конечные линейные преобразования V, и для каждого x ∈ V существует n ∈ Z такое, что f(m)(x) = 0 для всех m < n. Тогда существует вершиной оператор над R и V, чьи коэффициенты восстанавливают f: для всех x ∈ V и всех n ∈ Z n-й коэффициент оператора, действующий на x, равен f(n) x.
LaTeX
$$$\\exists VO\\in \\mathrm{VertexOperator}(R,V)$ such that (\\forall x\\in V)(\\forall n\\in \\mathbb{Z}): (\\mathrm{coeff}_n(VO))(x) = f(n)x$$$
Lean4
/-- Given an endomorphism-valued function on integers satisfying a pointwise bounded-pole condition,
we produce a vertex operator. -/
noncomputable def of_coeff (f : ℤ → Module.End R V) (hf : ∀ x : V, ∃ n : ℤ, ∀ m : ℤ, m < n → f m x = 0) :
VertexOperator R V :=
HVertexOperator.of_coeff f
(fun x =>
HahnSeries.suppBddBelow_supp_PWO (fun n => f n x)
(HahnSeries.forallLTEqZero_supp_BddBelow (fun n => f n x) (Exists.choose (hf x)) (Exists.choose_spec (hf x))))
