§4.2, p. 37 — shift equivariance of convolution, SC(θ)x = C(θ)Sx

Proved

GeomDL.Grids.shift_equivariance

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

circulant-matrixequivariancegeometric-deep-learningp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1shift-operator

Let $n \ge 1$ and let $R$ be a commutative ring. For every filter $\theta = (\theta_0, \dots, \theta_{n-1})$ and every signal $x$ on $\mathbb Z_n$ , the convolution operator $C(\theta)$ commutes with the right shift $S$ :

S\,C(\theta)\,x = C(\theta)\,S\,x .

This is the translation (shift) equivariance of convolution: shifting the input and then convolving gives the same result as convolving and then shifting. It is the easy half of the characterisation of circulant matrices as the matrices commuting with $S$ .

Preamble

import Mathlib
import Definitions.Def_GeomDL_Grids_Defs

open Matrix

Formal statement

namespace GeomDL.Grids
/-- Bronstein et al. §4.2, p. 37: shift equivariance of the convolution operator,
`SC(θ)x = C(θ)Sx` for every filter `θ` and every signal `x`. -/
theorem shift_equivariance {R : Type*} [CommRing R] {n : ℕ} [NeZero n]
    (θ x : ZMod n → R) :
    shift R n *ᵥ (circulant θ *ᵥ x) = circulant θ *ᵥ (shift R n *ᵥ x) := by sorry
end GeomDL.Grids

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §4.2, p. 37, display "SC(θ)x = C(θ)Sx"

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph