The finite residual convolution is exactly the source's sum over i+j=n.

theorem EulerFiniteGrades.bounded_pairs_eq_antidiagonal (M n : ℕ) (hn : n ≤ M) : {ij ∈ Finset.range (M + 1) ×ˢ Finset.range (M + 1) | ij.1 + ij.2 = n} = Finset.antidiagonal n

theorem EulerFiniteGrades.convolution_eq_antidiagonal {V : Type u_1} {W : Type u_2} {Q : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup Q] [Module ℝ Q] (M n : ℕ) (hn : n ≤ M) (B : V →ₗ[ℝ] W →ₗ[ℝ] Q) (u : ℕ → V) (v : ℕ → W) : convolution M B u v n = ∑ ij ∈ Finset.antidiagonal n, (B (u ij.1)) (v ij.2)

theorem EulerFiniteGrades.convolution_eq_range {V : Type u_1} {W : Type u_2} {Q : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup Q] [Module ℝ Q] (M n : ℕ) (hn : n ≤ M) (B : V →ₗ[ℝ] W →ₗ[ℝ] Q) (u : ℕ → V) (v : ℕ → W) : convolution M B u v n = ∑ i ∈ Finset.range (n + 1), (B (u i)) (v (n - i))

theorem EulerFiniteGrades.convolution_congr_below {V : Type u_1} {W : Type u_2} {Q : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [AddCommGroup Q] [Module ℝ Q] (M n : ℕ) (hn : n ≤ M) (B : V →ₗ[ℝ] W →ₗ[ℝ] Q) (u u' : ℕ → V) (v v' : ℕ → W) (hu : ∀ i ≤ n, u i = u' i) (hv : ∀ i ≤ n, v i = v' i) : convolution M B u v n = convolution M B u' v' n

No coefficient above the target grade enters its slow convolution.