§4.3, p. 41 — group convolution against an invariant measure is equivariant

Proved

GeomDL.GroupConv.eq_14_equivariant

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

equivariancegeometric-deep-learninggroup-convolutionp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Let $G$ act transitively and measurably on a domain $\Omega$ , and let $\mu$ be invariant under the action. For scalar signals $x,\theta:\Omega\to\mathbb R$ , a group element $h$ , and an output index $g\in G$ , group convolution satisfies

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

Thus the convolution maps signals on $\Omega$ to signals on $G$ while respecting the two corresponding group actions.

Formalization Note In Lean the stated equality is between the first and last expressions; the middle expression is the definition of the regular action $\rho_G$ . Transitivity records the section's homogeneous-domain assumption on p. 43. The book's invariant measure is explicit, as is measurability of the action. No integrability hypothesis is added; measure-preserving reindexing preserves the integral's value, including Lean's zero value for a nonintegrable integrand.

Preamble

import Mathlib
import Definitions.Def_GeomDL_GroupConv_Model

Formal statement

namespace GeomDL.GroupConv

universe u v

/-- §4.3, equation (14) and the following displayed identity, p. 41. -/
theorem eq_14_equivariant {G : Type u} {Ω : Type v} [Group G] [MulAction G Ω]
    [MeasurableSpace G] [MeasurableSpace Ω] [MeasurableSMul G Ω]
    (μ : MeasureTheory.Measure Ω) [MeasureTheory.SMulInvariantMeasure G Ω μ]
    (htrans : ∀ a b : Ω, ∃ k : G, k • a = b)
    (h : G) (x θ : Ω → ℝ) (g : G) :
    groupConvolution μ (signalAction h x) θ g =
      regularAction h (groupConvolution μ x θ) g := by sorry

end GeomDL.GroupConv

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §4.3, equation (14) and displayed equivariance identity, p. 41

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