English
For the left-regular representation of G, the operator norm is given by a particular explicit decomposition: it is the composition of a left-scalar action with a linear combination built from a single basis vector, reflecting a standard decomposition formula for the left-regular action.
Русский
Для левого регулярного представления G норму оператора можно выразить через явное разложение: это композиция левого умножения и линейной комбинации по базису, отражающая стандартную формулу для левого регулярного действия.
LaTeX
$$$ (leftRegular k G).norm = (LinearMap.lsmul k _)^{\\!\\!}.flip((leftRegular k G).norm (\\text{single } 1 1)) \\circ_\\ell linearCombination_k (\\cdot) (1) $$$
Lean4
theorem leftRegular_norm_apply :
(leftRegular k G).norm =
(LinearMap.lsmul k _).flip ((leftRegular k G).norm (single 1 1)) ∘ₗ linearCombination _ (fun _ => 1) :=
by
ext i : 2
simpa [Representation.norm] using Finset.sum_bijective _ (Group.mulRight_bijective i) (by simp_all) (by simp_all)
