§4.1, eq. (7), p. 33 — the shared node-wise linear map F_Θ(X) = XΘ is permutation equivariant

Proved

GeomDL.Sets.eq_7_equivariant

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

geometric-deep-learningp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1permutation-equivariance

Let $\boldsymbol\Theta\in\mathbb R^{d\times d'}$ and define $\mathbf F_{\boldsymbol\Theta}:\mathbb R^{n\times d}\to\mathbb R^{n\times d'}$ by

\mathbf F_{\boldsymbol\Theta}(\mathbf X)=\mathbf X\boldsymbol\Theta .

Then

$\mathbf F_{\boldsymbol\Theta}$ is permutation equivariant: $\mathbf F_{\boldsymbol\Theta}(\mathbf P\mathbf X)=\mathbf P\,\mathbf F_{\boldsymbol\Theta}(\mathbf X)$ for every permutation matrix $\mathbf P$ ;
the $u$ -th row of $\mathbf F_{\boldsymbol\Theta}(\mathbf X)$ is the latent feature $\mathbf h_u=\boldsymbol\Theta^\top\mathbf x_u$ .

This is the simplest permutation-equivariant layer: the same linear map applied to every node.

Preamble

import Mathlib
import Definitions.Def_GeomDL_Sets_Defs

Formal statement

namespace GeomDL.Sets

/-- §4.1, eq. (7), p. 33: the shared node-wise linear transform `F_Θ(X) = XΘ`,
`Θ ∈ ℝ^{d×d'}`, is permutation equivariant, `F_Θ(PX) = P F_Θ(X)`, and its rows are the
latent features `h_u = Θᵀ x_u`. -/
theorem eq_7_equivariant {n d d' : ℕ} (Θ : Matrix (Fin d) (Fin d') ℝ) :
    IsPermEquivariant (nodeLinear Θ : Matrix (Fin n) (Fin d) ℝ → Matrix (Fin n) (Fin d') ℝ) ∧
      ∀ (X : Matrix (Fin n) (Fin d) ℝ) (u : Fin n), nodeLinear Θ X u = (Matrix.transpose Θ).mulVec (X u) := by sorry

end GeomDL.Sets

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §4.1, eq. (7), p. 33

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