English
The composite of two heterogeneous vertex operators acting on a vector, realized as an iterated Hahn series, has coefficients given by (A ∘ B) g' = A (coeff B g' u).
Русский
Сложение двух гетерогенных вершинных операторов, действующих на вектор, реализуется как вложенная Hahn-серия; коэффициент для g' удовлетворяет (A ∘ B) g' = A (coeff B g' u).
LaTeX
$$$\mathrm{coeff}\big(\mathrm{compHahnSeries}\ A\ B\ u\big)(g') = A\big( (\mathrm{coeff}\ B\ g')\ u \big)$$$
Lean4
/-- The composite of two heterogeneous vertex operators acting on a vector, as an iterated Hahn
series. -/
@[simps]
def compHahnSeries (u : U) : HahnSeries Γ' (HahnSeries Γ W)
where
coeff g' := A (coeff B g' u)
isPWO_support' := by
refine Set.IsPWO.mono (((of R).symm (B u)).isPWO_support') ?_
simp only [coeff_apply_apply, Function.support_subset_iff, ne_eq, Function.mem_support]
intro g' hg' hAB
exact hg' (by simp [hAB])
