§4.2, p. 37 — C(θ)x = x ⋆ θ, and the shift S = C(0, 1, 0, …, 0) moves vectors right: (Sx)_u = x_{u−1}

Proved

GeomDL.Grids.circulant_mulVec_eq_conv

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

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

Let $n \ge 1$ , let $R$ be a commutative ring, and index vectors by $\mathbb Z_n$ . Circulant matrices are convolutions: for every filter $\theta$ and every signal $x$ ,

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

Moreover the circulant matrix $S = C(0, 1, 0, \dots, 0)$ shifts vectors to the right by one position:

(Sx)_u = x_{u-1 \bmod n} \qquad \text{for all } u \in \mathbb Z_n .

The first identity justifies calling circulant matrices convolution operators; the second fixes the direction of the shift used throughout the section.

Preamble

import Mathlib
import Definitions.Def_GeomDL_Grids_Defs

open Matrix

Formal statement

namespace GeomDL.Grids
/-- Bronstein et al. §4.2, p. 37: `C(θ)x = x ⋆ θ`, and the circulant matrix `S` of
`θ = (0, 1, 0, …, 0)ᵀ` shifts vectors to the right by one position: `(Sx)_u = x_{u-1}`. -/
theorem circulant_mulVec_eq_conv {R : Type*} [CommRing R] {n : ℕ} [NeZero n] :
    (∀ θ x : ZMod n → R, circulant θ *ᵥ x = conv x θ) ∧
      ∀ (x : ZMod n → R) (u : ZMod n), (shift R n *ᵥ x) u = x (u - 1) := by sorry
end GeomDL.Grids

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §4.2, p. 37, "as one has C(θ)x = x ⋆ θ" and "shifts vectors to the right by one position" (convolution display on p. 36)

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