§4.3, p. 41 — the induced signal action obeys the group representation law

Proved

GeomDL.GroupConv.representation_property

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

geometric-deep-learninggroup-actiongroup-representationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Let $G$ act on a domain $\Omega$ , and let $\rho(g)$ act on real-valued signals by $(\rho(g)\theta)(u)=\theta(g^{-1}\cdot u)$ . For $h,g\in G$ and any filter $\theta$ ,

\rho(h^{-1})(\rho(g)\theta)=\rho(h^{-1}g)\theta.

The book uses this law to identify the transformed filter that appears in group convolution.

Preamble

import Mathlib
import Definitions.Def_GeomDL_GroupConv_Model

Formal statement

namespace GeomDL.GroupConv

universe u v

/-- §4.3, p. 41: the signal action satisfies the representation law used in the displayed calculation. -/
theorem representation_property {G : Type u} {Ω : Type v} [Group G] [MulAction G Ω]
    (h g : G) (θ : Ω → ℝ) :
    signalAction h⁻¹ (signalAction g θ) = signalAction (h⁻¹ * g) θ := by sorry

end GeomDL.GroupConv

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §4.3, p. 41, paragraph following equation (14)

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