noncomputable def convolution {K : Type u_1} [Group K] [MeasurableSpace K] (μ : MeasureTheory.Measure K) (φ₁ φ₂ : K → ℂ) : K → ℂ

theorem conj_trace_clm {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] [CompleteSpace V] (f : V →L[ℂ] V) : (starRingEnd ℂ) ((LinearMap.trace ℂ V) ↑f) = (LinearMap.trace ℂ V) ↑(ContinuousLinearMap.adjoint f)

theorem adjoint_comp_endo {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (f g : V →L[ℂ] V) : ContinuousLinearMap.adjoint (f.comp g) = (ContinuousLinearMap.adjoint g).comp (ContinuousLinearMap.adjoint f)

theorem unitary_inv_eq_adjoint {G : Type u_2} [Group G] {W : Type u_3} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] (ρ_hom : G →* W →L[ℂ] W) (hU : ∀ (g : G), ContinuousLinearMap.adjoint (ρ_hom g) * ρ_hom g = 1 ∧ ρ_hom g * ContinuousLinearMap.adjoint (ρ_hom g) = 1) (g : G) : ρ_hom g⁻¹ = ContinuousLinearMap.adjoint (ρ_hom g)

theorem key_trace_identity {G : Type u_2} [Group G] {W : Type u_3} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [FiniteDimensional ℂ W] [CompleteSpace W] (ρ_hom : G →* W →L[ℂ] W) (hU : ∀ (g : G), ContinuousLinearMap.adjoint (ρ_hom g) * ρ_hom g = 1 ∧ ρ_hom g * ContinuousLinearMap.adjoint (ρ_hom g) = 1) (A : W →L[ℂ] W) (z y : G) : (LinearMap.trace ℂ W) ↑(A.comp (ρ_hom (z * y⁻¹))) = (starRingEnd ℂ) ((LinearMap.trace ℂ W) ↑((ContinuousLinearMap.adjoint (A.comp (ρ_hom z))).comp (ρ_hom y)))

noncomputable def KFiniteFunctionSubspace {K : Type u_1} [Group K] [TopologicalSpace K] [CompactSpace K] : Submodule ℂ (K → ℂ)

theorem matrixCoefficient_mem_KFiniteFunctionSubspace {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasurableSpace K] [BorelSpace K] {W : Type} [AddCommGroup W] [Module ℂ W] [TopologicalSpace W] [FiniteDimensional ℂ W] (ρ : ContinuousRep K W) (φ : W →L[ℂ] ℂ) (v : W) : ContinuousRep.matrixCoefficient K ρ φ v ∈ KFiniteFunctionSubspace

theorem isKFiniteFunction_mem_KFiniteFunctionSubspace {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasurableSpace K] [BorelSpace K] (p : K → ℂ) (hp : PlancherelCompact.IsKFiniteFunction K p) : p ∈ KFiniteFunctionSubspace