Prove2Me

§4.1, p. 33 — a linear map on ℝⁿ is permutation equivariant iff it is α·I + β·(1/n)𝟙𝟙ᵀ

Proved
GeomDL.Sets.linear_equivariant_iff_id_average

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

deep-setsgeometric-deep-learninglinear-algebrap2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1permutation-equivariance

Let n≥1n\ge1 and let F:Rn→Rn\mathbf F:\mathbb R^n\to\mathbb R^n be linear. Then F\mathbf F is permutation equivariant,

FPx=PFxfor every n×n permutation matrix P and every x∈Rn,\mathbf F\mathbf P x=\mathbf P\mathbf F x\quad\text{for every }n\times n\text{ permutation matrix }\mathbf P\text{ and every }x\in\mathbb R^n,

if and only if there are scalars α,β∈R\alpha,\beta\in\mathbb R with

Fx=α x+β 1n11⊤xfor all x∈Rn,\mathbf F x=\alpha\,x+\beta\,\tfrac1n\mathbf 1\mathbf 1^\top x\qquad\text{for all }x\in\mathbb R^n,

that is, F\mathbf F is a linear combination of the two generators, the identity F1x=x\mathbf F_1x=x and the average F2x=1n11⊤x\mathbf F_2x=\tfrac1n\mathbf 1\mathbf 1^\top x, all of whose entries equal 1n∑u=1nxu\tfrac1n\sum_{u=1}^n x_u.

Equivalently, the commutant of the permutation representation of Σn\Sigma_n on Rn\mathbb R^n is spanned by I\mathbf I and 11⊤\mathbf 1\mathbf 1^\top. This characterises the linear layers of Deep Sets.

Formalization Note The statement is for one feature channel (d=d′=1d=d'=1); the multi-channel form is a separate item of this mission, because the book's scalar form is false for d>1d>1. The hypothesis n≥1n\ge1 makes 1/n1/n meaningful. For n=1n=1 the two generators coincide and only existence of α,β\alpha,\beta is claimed.

Preamble
import Mathlib
import Definitions.Def_GeomDL_Sets_Defs
Formal statement
namespace GeomDL.Sets

/-- §4.1, p. 33: a linear map `F : ℝⁿ → ℝⁿ` (one channel) is permutation equivariant,
`F(Px) = P F(x)` for every permutation matrix `P`, if and only if it is a linear combination
of the identity `F₁x = x` and the average `F₂x = (1/n)𝟙𝟙ᵀx`. -/
theorem linear_equivariant_iff_id_average {n : ℕ} (hn : 0 < n)
    (F : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ)) :
    (∀ (σ : Equiv.Perm (Fin n)) (x : Fin n → ℝ), F (permVec σ x) = permVec σ (F x)) ↔
      ∃ α β : ℝ, ∀ x : Fin n → ℝ, F x = α • x + β • average x := by sorry

end GeomDL.Sets
Source
Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §4.1, p. 33, "any such map can be written as a linear combination of two generators"
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