theorem schur_orthogonality_different_reps {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasurableSpace K] [BorelSpace K] (μ : MeasureTheory.Measure K) [μ.IsHaarMeasure] (ρ₁ ρ₂ : ContinuousRep.IrrFinDimRep K) (hne : IsEmpty (RepEquiv ρ₁.rep ρ₂.rep)) (v₁ w₁ : ρ₁.carrier) (v₂ w₂ : ρ₂.carrier) : ∫ (g : K), inner ℂ ((ρ₁.rep.toMonoidHom g) v₁) w₁ * (starRingEnd ℂ) (inner ℂ ((ρ₂.rep.toMonoidHom g) v₂) w₂) ∂μ = 0

theorem schur_orthogonality_same_rep {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasurableSpace K] [BorelSpace K] (μ : MeasureTheory.Measure K) [μ.IsHaarMeasure] (ρ : ContinuousRep.IrrFinDimRep K) (v₁ v₂ w₁ w₂ : ρ.carrier) : ∫ (g : K), inner ℂ ((ρ.rep.toMonoidHom g) v₁) w₁ * (starRingEnd ℂ) (inner ℂ ((ρ.rep.toMonoidHom g) v₂) w₂) ∂μ = inner ℂ v₁ v₂ * (starRingEnd ℂ) (inner ℂ w₁ w₂) / ↑(Module.finrank ℂ ρ.carrier)

noncomputable def matrixCoefficientOfEnd {K : Type u_1} [Group K] [TopologicalSpace K] {W : Type u_2} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [FiniteDimensional ℂ W] [CompleteSpace W] (ρ : ContinuousRep K W) (A : W →L[ℂ] W) : K → ℂ

theorem trace_eq_sum_inner {ι : Type u_2} [Fintype ι] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (b : OrthonormalBasis ι ℂ E) (L : E →ₗ[ℂ] E) : (LinearMap.trace ℂ E) L = ∑ i : ι, inner ℂ (b i) (L (b i))

theorem schur_orthogonality_end {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasurableSpace K] [BorelSpace K] (μ : MeasureTheory.Measure K) [μ.IsHaarMeasure] (ρ : ContinuousRep.IrrFinDimRep K) (A B : ρ.carrier →L[ℂ] ρ.carrier) : ∫ (g : K), matrixCoefficientOfEnd ρ.rep A g * (starRingEnd ℂ) (matrixCoefficientOfEnd ρ.rep B g) ∂μ = (LinearMap.trace ℂ ρ.carrier) ↑(A.comp (ContinuousLinearMap.adjoint B)) / ↑(Module.finrank ℂ ρ.carrier)