def ContinuousRep.IsotypicComponentHom {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] [IsTopologicalGroup G] {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (π : ContinuousRep G V) (K : Subgroup G) (σ : ContinuousRep (↥K) Wσ) : Submodule ℂ V

def ContinuousRep.isotypicEvaluation {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] [IsTopologicalGroup G] {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (π : ContinuousRep G V) (K : Subgroup G) (σ : ContinuousRep (↥K) Wσ) (T : RepHom σ (π.restrictSubgroup K)) (u : Wσ) : V

noncomputable def ContinuousRep.matrixCoefficient (K : Type u_2) [Group K] [TopologicalSpace K] {Wρ : Type u_3} [AddCommGroup Wρ] [Module ℂ Wρ] [TopologicalSpace Wρ] (ρ : ContinuousRep K Wρ) (φ : Wρ →L[ℂ] ℂ) (v : Wρ) : K → ℂ

noncomputable def ContinuousRep.MatrixCoefficientSubspace (K : Type u_2) [Group K] [TopologicalSpace K] {Wρ : Type u_3} [AddCommGroup Wρ] [Module ℂ Wρ] [TopologicalSpace Wρ] (ρ : ContinuousRep K Wρ) : Submodule ℂ (K → ℂ)

structure ContinuousRep.IrrFinDimRep (K : Type u_2) [Group K] [TopologicalSpace K] [CompactSpace K] : Type (max 1 u_2)

• carrier : Type
• instNACG : NormedAddCommGroup self.carrier
• instIPS : InnerProductSpace ℂ self.carrier
• instFD : FiniteDimensional ℂ self.carrier
• instCS : CompleteSpace self.carrier
• rep : ContinuousRep K self.carrier
• irred : self.rep.IsIrreducible
• unitary : self.rep.IsUnitary
• instNT : Nontrivial self.carrier

noncomputable def ContinuousRep.IrrFinDimRep.dim {K : Type u_2} [Group K] [TopologicalSpace K] [CompactSpace K] (ρ : IrrFinDimRep K) : ℕ

@[reducible, inline]

noncomputable abbrev ContinuousRep.L2 (K : Type u_2) [MeasurableSpace K] (μ : MeasureTheory.Measure K) : AddSubgroup (K →ₘ[μ] ℂ)

def ContinuousRep.leftTranslationCM (K : Type u_2) [Group K] [TopologicalSpace K] [IsTopologicalGroup K] : C(K, C(K, K))

def ContinuousRep.leftRegularRep (K : Type u_2) [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasurableSpace K] [BorelSpace K] (μ : MeasureTheory.Measure K) [μ.IsHaarMeasure] : ContinuousRep K ↥(L2 K μ)

noncomputable def ContinuousRep.matrixCoefficientEmbed (K : Type u_2) [Group K] [TopologicalSpace K] [CompactSpace K] [MeasurableSpace K] (μ : MeasureTheory.Measure K) (ρ : IrrFinDimRep K) : EuclideanSpace ℂ (Fin ρ.dim × Fin ρ.dim) →ₗᵢ[ℂ] ↥(L2 K μ)

noncomputable def ContinuousRep.normalizedMatrixCoeffBasis (K : Type u_2) [Group K] [TopologicalSpace K] [CompactSpace K] [MeasurableSpace K] (μ : MeasureTheory.Measure K) : HilbertBasis ((ρ : IrrFinDimRep K) × Fin ρ.dim × Fin ρ.dim) ℂ ↥(L2 K μ)

theorem ContinuousRep.peterWeyl_orthonormal_basis (K : Type u_2) [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasurableSpace K] [BorelSpace K] (μ : MeasureTheory.Measure K) [μ.IsHaarMeasure] (i : (ρ : IrrFinDimRep K) × Fin ρ.dim × Fin ρ.dim) : (normalizedMatrixCoeffBasis K μ) i ∈ (leftRegularRep K μ).kFiniteSubspace ⊤

theorem ContinuousRep.peterWeyl_density (K : Type u_2) [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasurableSpace K] [BorelSpace K] (μ : MeasureTheory.Measure K) [μ.IsHaarMeasure] : Dense ↑((leftRegularRep K μ).kFiniteSubspace ⊤)

theorem ContinuousRep.peterWeyl_decomposition (K : Type u_2) [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasurableSpace K] [BorelSpace K] (μ : MeasureTheory.Measure K) [μ.IsHaarMeasure] : IsHilbertSum ℂ (fun (ρ : IrrFinDimRep K) => EuclideanSpace ℂ (Fin ρ.dim × Fin ρ.dim)) (matrixCoefficientEmbed K μ)

theorem ContinuousRep.peterWeyl_L2_approx (K : Type u_2) [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [MeasurableSpace K] [BorelSpace K] (μ : MeasureTheory.Measure K) [μ.IsHaarMeasure] (f : ↥(L2 K μ)) (ε : ℝ) : 0 < ε → ∃ g ∈ (leftRegularRep K μ).kFiniteSubspace ⊤, dist f g < ε