Multiplication across a finite interval of nonnegative degrees

theorem MagnitudeConjecture.Graded.VectorGrading.interval_convolution {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) (hneg : ∀ d < 0, R.component d = ⊥) (m : ℕ) (r t : Fin (m + 1)) (a b : A) : (R.projection (↑↑r - ↑↑t)) (a * b) = ∑ s : Fin (m + 1), (R.projection (↑↑r - ↑↑s)) a * (R.projection (↑↑s - ↑↑t)) b

The product coefficient between interval degrees is the sum over intermediate interval degrees: no term can leave the interval and then return.