Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite diagonal and coupled coefficients

Abstract

Finite diagonal and coupled coefficients

Theorem 1.1 (Finite diagonal and coupled coefficients).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/ThreeFieldBalancedInverseKernel.balanced_inverse_coeff

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FormalSeries/ThreeFieldBalancedInverseKernel.balanced_inverse_coeff (✓ std3). ∎

Source. Repository-derived.

Commentary.

The diagonal binomial kernel consumes l degrees in both native variables. The coupled kernel consumes r and r+j degrees. Their product therefore consumes r+l and r+j+l degrees, with the sign (-1)^j.

References