補題
H を局所コンパクト空間 X に右から固有に作用(>>473)する
局所コンパクト群とする。
β を H の 左 Haar 測度(過去スレ012の351)とする。
f を K(X, R) (過去スレ007の708) の元とする。

η ∈ H のとき X 上の関数 δ(η)f を δ(η)f(x) = f(xη) で定義する。
このとき、
(δ(η)f)^1 = (1/Δ(η))f^1
である。
ここで、(δ(η)f)^1、f^1 は>>498で定義したものであり、
Δ は H のモジュール(過去スレ012の474)である。

証明
(δ(η)f)^1(x) = ∫ (δ(η)f)(xξ) dβ(ξ)
= ∫ f(xξη) dβ(ξ) = (1/Δ(η))∫ f(xξ) dβ(ξ) = (1/Δ(η))f^1(x)

よって、(δ(η)f)^1 = (1/Δ(η))f^1
証明終