Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

§4.6, p. 65 — a polynomial filter of degree r is localised in r-hop neighbourhood

Proved
GeomDL.Filters.polynomial_filter_localised

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

geometric-deep-learninglocalityp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1polynomial-filter

Let GGG be a simple graph on the nodes {1,…,n}\{1,\dots,n\}{1,…,n}, and let W∈Rn×nW\in\mathbb R^{n\times n}W∈Rn×n be a weight matrix supported on the edges of GGG: wuv≠0w_{uv}\neq 0wuv​=0 with u≠vu\neq vu=v implies that uuu and vvv are adjacent in GGG. Let Δ=D−W\Delta=D-WΔ=D−W be the Laplacian (24), r≥0r\ge 0r≥0, and α0,…,αr∈R\alpha_0,\dots,\alpha_r\in\mathbb Rα0​,…,αr​∈R. Fix a node uuu and two feature matrices X,X′∈Rn×dX,X'\in\mathbb R^{n\times d}X,X′∈Rn×d whose rows agree at every node within rrr hops of uuu (every vvv joined to uuu by a walk of length at most rrr). Then

(∑k=0rαkΔkX)u=(∑k=0rαkΔkX′)u.\Big(\sum_{k=0}^r\alpha_k\Delta^kX\Big)_u=\Big(\sum_{k=0}^r\alpha_k\Delta^kX'\Big)_u .(k=0∑r​αk​ΔkX)u​=(k=0∑r​αk​ΔkX′)u​.

That is, the output of a degree-rrr polynomial filter at uuu depends only on the features in the rrr-hop neighbourhood of uuu. This is what makes polynomial spectral filters on graphs local, in contrast with general spectral filters and with rational filters, which have exponential decay but not local support.

Formalization Note The book's graph is the graph of the weights; here the weights may live on any graph GGG containing their support (diagonal weights are allowed and cancel in Δ\DeltaΔ), and WWW need not be symmetric. The book's setting W=W⊤W=W^\topW=W⊤, GGG the graph of WWW, is a special case.

Preamble
import Mathlib
import Definitions.Def_GeomDL_Filters_Defs
Formal statement
namespace GeomDL.Filters
open Matrix
/-- §4.6, p. 65: "since the Laplacian is local, a polynomial filter of degree `r` is localised in
`r`-hop neighbourhood". Let the weights `W` be supported on the edges of the graph `G`
(`w_uv ≠ 0` with `u ≠ v` forces `u ∼ v`). If two feature matrices `X, X'` agree on every node
within `r` hops of `u`, then `p̂(Δ)X` and `p̂(Δ)X'` agree at `u`, for every choice of
coefficients `α₀, …, α_r`. -/
theorem polynomial_filter_localised {n d : ℕ} (G : SimpleGraph (Fin n))
    (W : Matrix (Fin n) (Fin n) ℝ) (hW : ∀ u v, u ≠ v → W u v ≠ 0 → G.Adj u v)
    (r : ℕ) (α : Fin (r + 1) → ℝ) (X X' : Matrix (Fin n) (Fin d) ℝ) (u : Fin n)
    (hX : ∀ v, WithinHops G r u v → X v = X' v) :
    (polyFilter W r α * X) u = (polyFilter W r α * X') u := by sorry
end GeomDL.Filters
Source
Bronstein, Bruna, Cohen & Veličković, Geometric Deep Learning (arXiv:2104.13478v2), §4.6, p. 65, "Furthermore, since the Laplacian is local, a polynomial filter of degree r is localised in r-hop neighbourhood."
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me