§3.1, pp. 14–15 — the action on signals is linear, g.(αx + βx′) = α(g.x) + β(g.x′)

Proved

GeomDL.Blueprint.act_linear

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

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

Let a group $\mathfrak G$ act on a domain $\Omega$ , and let $\mathfrak G$ act on real signals $x : \Omega \to \mathbb R$ by $(\mathfrak g . x)(u) = x(\mathfrak g^{-1} u)$ . Then the action is linear: for every $\mathfrak g \in \mathfrak G$ , all scalars $\alpha, \beta \in \mathbb R$ and all signals $x, x'$ ,

\mathfrak g . (\alpha x + \beta x') = \alpha (\mathfrak g . x) + \beta (\mathfrak g . x') .

Linearity is what makes the action on signals a group representation.

Preamble

import Mathlib
import Definitions.Def_GeomDL_Blueprint_Defs

Formal statement

namespace GeomDL.Blueprint

/-- Bronstein et al., §3.1, pp. 14–15: the action (3) on real signals is linear, in the sense that
`g.(αx + βx′) = α(g.x) + β(g.x′)` for any scalars `α, β` and signals `x, x′`. -/
theorem act_linear {G Ω : Type*} [Group G] [MulAction G Ω]
    (g : G) (α β : ℝ) (x x' : Ω → ℝ) :
    act g (α • x + β • x') = α • act g x + β • act g x' := by sorry

end GeomDL.Blueprint

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §3.1, display at the top of p. 15 (sentence begins on p. 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