Quadratic norm identity for star-algebra representations

A star-algebra homomorphism from any complex star algebra to bounded operators on a Hilbert space sends f⋆ * f to the operator (π f)† (π f). Consequently its diagonal matrix element is the squared norm of π f ξ. This identity does not require a topology, commutativity, or a C⋆-norm on the domain.

theorem StarAlgHom.norm_sq_apply_eq_re_inner_star_mul {A : Type u_1} {H : Type u_2} [Semiring A] [StarRing A] [Algebra ℂ A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (ξ : H) (f : A) : ‖(π f) ξ‖ ^ 2 = RCLike.re (inner ℂ ξ ((π (star f * f)) ξ))

The squared norm of a represented vector equals the real part of its quadratic matrix coefficient, for a representation of any complex star algebra.