§4.6, p. 65 — a polynomial filter of degree r is localised in r-hop neighbourhood
ProvedGeomDL.Filters.polynomial_filter_localisedLet be a simple graph on the nodes , and let be a weight matrix supported on the edges of : with implies that and are adjacent in . Let be the Laplacian (24), , and . Fix a node and two feature matrices whose rows agree at every node within hops of (every joined to by a walk of length at most ). Then
That is, the output of a degree- polynomial filter at depends only on the features in the -hop neighbourhood of . 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 containing their support (diagonal weights are allowed and cancel in ), and need not be symmetric. The book's setting , the graph of , is a special case.
import Mathlib import Definitions.Def_GeomDL_Filters_Defs
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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.