Prove2Me

§4.1, eq. (6), p. 32 — the sum readout φ(Σᵤ ψ(xᵤ)) is permutation invariant

Proved
GeomDL.Sets.eq_6_invariant

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

deep-setsgeometric-deep-learningp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1permutation-invariance

Let X∈Rn×d\mathbf X\in\mathbb R^{n\times d} have rows x1,…,xn\mathbf x_1,\dots,\mathbf x_n, let ψ:Rd→M\psi:\mathbb R^d\to M take values in a commutative additive monoid MM, and let ϕ:M→Y\phi:M\to Y be arbitrary. Define

f(X)=ϕ(∑u∈Vψ(xu)).f(\mathbf X)=\phi\Big(\sum_{u\in\mathcal V}\psi(\mathbf x_u)\Big).

Then ff is permutation invariant: f(PX)=f(X)f(\mathbf P\mathbf X)=f(\mathbf X) for every n×nn\times n permutation matrix P\mathbf P.

This is the book's first example of a permutation-invariant function on sets, the readout of Deep Sets.

Formalization Note PX\mathbf P\mathbf X reorders the rows of X\mathbf X, row uu of PX\mathbf P\mathbf X being row σ−1(u)\sigma^{-1}(u) of X\mathbf X; the statement quantifies over all σ∈Σn\sigma\in\Sigma_n.

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

/-- §4.1, eq. (6), p. 32: `f(X) = φ(∑_{u ∈ V} ψ(x_u))` is permutation invariant,
`f(PX) = f(X)` for every permutation matrix `P` (rows of `PX` reordered by `σ⁻¹`). -/
theorem eq_6_invariant {n d : ℕ} {M Y : Type*} [AddCommMonoid M] (φ : M → Y)
    (ψ : (Fin d → ℝ) → M) :
    IsPermInvariant (sumReadout φ ψ : Matrix (Fin n) (Fin d) ℝ → Y) := by sorry

end GeomDL.Sets
Source
Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §4.1, eq. (6), p. 32
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