equivariantProjection_apply — Mathlib

English

For v ∈ W, the equivariant projection equals the average of the g-conjugates applied to v, i.e., (π.equivariantProjection G) v = |G|^{-1} ∑_{g∈G} (π.conjugate g) v.

Русский

Для v ∈ W проекция-эквиариватна: (π.equivariantProjection G) v = |G|^{-1} ∑_{g∈G} (π^g) v.

LaTeX

$$$\pi.equivariantProjection G v = \mathrm{Ring.inverse} (Fintype.card G : k) \cdot \sum_{g : G} π.conjugate g v$$$

Lean4

theorem equivariantProjection_apply (v : W) :
    π.equivariantProjection G v = Ring.inverse (Fintype.card G : k) • ∑ g : G, π.conjugate g v := by
  simp only [equivariantProjection, smul_apply, sumOfConjugatesEquivariant_apply]

Похожие утверждения