theorem ContinuousRep.kFiniteSubspace_stable {G : Type uG} [Group G] [TopologicalSpace G] {V : Type u_1} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (K : Subgroup G) (g : ↥K) (v : V) (hv : v ∈ π.kFiniteSubspace K) : (π.toMonoidHom ↑g) v ∈ π.kFiniteSubspace K

theorem ContinuousRep.unitary_adjoint_eq_inv {G : Type uG} [Group G] [TopologicalSpace G] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (π : ContinuousRep G E) (hU : π.IsUnitary) (g : G) : ContinuousLinearMap.adjoint (π.toMonoidHom g) = π.toMonoidHom g⁻¹

theorem ContinuousRep.unitary_inner_invariant {G : Type uG} [Group G] [TopologicalSpace G] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (π : ContinuousRep G E) (hU : π.IsUnitary) (g : G) (v w : E) : inner ℂ ((π.toMonoidHom g) v) ((π.toMonoidHom g) w) = inner ℂ v w

theorem ContinuousRep.unitary_orthogonal_invariant {G : Type uG} [Group G] [TopologicalSpace G] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (π : ContinuousRep G E) (hU : π.IsUnitary) (W : Submodule ℂ E) (hW : ∀ (g : G), ∀ v ∈ W, (π.toMonoidHom g) v ∈ W) (g : G) (v : E) (hv : v ∈ Wᗮ) : (π.toMonoidHom g) v ∈ Wᗮ

noncomputable def ContinuousRep.orthogonalProjection_intertwines_subrep {G : Type uG} [Group G] [TopologicalSpace G] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [IsTopologicalGroup G] (π : ContinuousRep G E) (hU : π.IsUnitary) (K : Subgroup G) (W₁ W₂ : Submodule ℂ E) (hW₁ : (π.restrictSubgroup K).IsInvariantSubspace W₁) (hW₂ : (π.restrictSubgroup K).IsInvariantSubspace W₂) : RepHom ((π.restrictSubgroup K).subrepresentation W₁ hW₁) ((π.restrictSubgroup K).subrepresentation W₂ hW₂)

theorem ContinuousRep.orthogonalProjection_intertwines_subrep_val {G : Type uG} [Group G] [TopologicalSpace G] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [IsTopologicalGroup G] (π : ContinuousRep G E) (hU : π.IsUnitary) (K : Subgroup G) (W₁ W₂ : Submodule ℂ E) (hW₁ : (π.restrictSubgroup K).IsInvariantSubspace W₁) (hW₂ : (π.restrictSubgroup K).IsInvariantSubspace W₂) [W₂.HasOrthogonalProjection] (v : ↥W₁) : (π.orthogonalProjection_intertwines_subrep hU K W₁ W₂ hW₁ hW₂).toContinuousLinearMap v = W₂.orthogonalProjection ↑v

theorem ContinuousRep.continuous_inverse_of_bijective_clm {V₁ : Type u_2} [NormedAddCommGroup V₁] [NormedSpace ℂ V₁] [CompleteSpace V₁] {V₂ : Type u_3} [NormedAddCommGroup V₂] [NormedSpace ℂ V₂] [CompleteSpace V₂] (f : V₁ →L[ℂ] V₂) (hbij : Function.Bijective ⇑f) : Continuous ⇑(LinearEquiv.ofBijective (↑f) hbij).symm

theorem ContinuousRep.repEquiv_of_bijective_repHom {G' : Type u_2} [Group G'] [TopologicalSpace G'] {V₁ : Type u_3} [NormedAddCommGroup V₁] [NormedSpace ℂ V₁] [CompleteSpace V₁] {V₂ : Type u_4} [NormedAddCommGroup V₂] [NormedSpace ℂ V₂] [CompleteSpace V₂] (π₁ : ContinuousRep G' V₁) (π₂ : ContinuousRep G' V₂) (T : RepHom π₁ π₂) (hbij : Function.Bijective ⇑T.toContinuousLinearMap) : Nonempty (RepEquiv π₁ π₂)

theorem ContinuousRep.repEquiv_trans {G' : Type u_2} [Group G'] [TopologicalSpace G'] {V₁ : Type u_3} [AddCommGroup V₁] [Module ℂ V₁] [TopologicalSpace V₁] {V₂ : Type u_4} [AddCommGroup V₂] [Module ℂ V₂] [TopologicalSpace V₂] {V₃ : Type u_5} [AddCommGroup V₃] [Module ℂ V₃] [TopologicalSpace V₃] {π₁ : ContinuousRep G' V₁} {π₂ : ContinuousRep G' V₂} {π₃ : ContinuousRep G' V₃} (h₁ : Nonempty (RepEquiv π₁ π₂)) (h₂ : Nonempty (RepEquiv π₂ π₃)) : Nonempty (RepEquiv π₁ π₃)

theorem ContinuousRep.repEquiv_symm {G' : Type u_2} [Group G'] [TopologicalSpace G'] {V₁ : Type u_3} [AddCommGroup V₁] [Module ℂ V₁] [TopologicalSpace V₁] {V₂ : Type u_4} [AddCommGroup V₂] [Module ℂ V₂] [TopologicalSpace V₂] {π₁ : ContinuousRep G' V₁} {π₂ : ContinuousRep G' V₂} (h : Nonempty (RepEquiv π₁ π₂)) : Nonempty (RepEquiv π₂ π₁)

theorem ContinuousRep.irreducible_subspaces_orthogonal {G : Type uG} [Group G] [TopologicalSpace G] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [IsTopologicalGroup G] {Wσ : Type u_2} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] {Wτ : Type u_3} [AddCommGroup Wτ] [Module ℂ Wτ] [TopologicalSpace Wτ] (π : ContinuousRep G E) (hU : π.IsUnitary) (K : Subgroup G) (σ : ContinuousRep (↥K) Wσ) (τ : ContinuousRep (↥K) Wτ) (W₁ W₂ : Submodule ℂ E) (hW₁ : (π.restrictSubgroup K).IsInvariantSubspace W₁) (hW₂ : (π.restrictSubgroup K).IsInvariantSubspace W₂) (hirr₁ : ((π.restrictSubgroup K).subrepresentation W₁ hW₁).IsIrreducible) (hirr₂ : ((π.restrictSubgroup K).subrepresentation W₂ hW₂).IsIrreducible) (hiso₁ : Nonempty (RepEquiv ((π.restrictSubgroup K).subrepresentation W₁ hW₁) σ)) (hiso₂ : Nonempty (RepEquiv ((π.restrictSubgroup K).subrepresentation W₂ hW₂) τ)) (hne : ¬Nonempty (RepEquiv σ τ)) : W₁ ⟂ W₂

theorem ContinuousRep.mem_orthogonal_sSup {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (T : Set (Submodule ℂ F)) (v : F) (h : ∀ W ∈ T, v ∈ Wᗮ) : v ∈ (sSup T)ᗮ

theorem ContinuousRep.sSup_orthogonal_sSup {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (S T : Set (Submodule ℂ F)) (h : ∀ U ∈ S, ∀ W ∈ T, U ⟂ W) : sSup S ⟂ sSup T

theorem ContinuousRep.isotypicComponent_orthogonal {G : Type uG} [Group G] [TopologicalSpace G] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [IsTopologicalGroup G] {Wσ : Type u_2} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] {Wτ : Type u_3} [AddCommGroup Wτ] [Module ℂ Wτ] [TopologicalSpace Wτ] (π : ContinuousRep G E) (hU : π.IsUnitary) (K : Subgroup G) (σ : ContinuousRep (↥K) Wσ) (τ : ContinuousRep (↥K) Wτ) (hne : ¬Nonempty (RepEquiv σ τ)) : π.IsotypicComponent K σ ⟂ π.IsotypicComponent K τ

noncomputable def ContinuousRep.discreteMeasureRep {G : Type uG} [Group G] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] (π : G →* V →L[ℂ] V) : MonoidAlgebra ℂ G →ₐ[ℂ] V →L[ℂ] V

theorem ContinuousRep.discreteMeasureRep_extends {G : Type uG} [Group G] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] (π : G →* V →L[ℂ] V) (g : G) : (discreteMeasureRep π) (MonoidAlgebra.single g 1) = π g

theorem ContinuousRep.discreteMeasureRep_unique {G : Type uG} [Group G] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] (π : G →* V →L[ℂ] V) (φ : MonoidAlgebra ℂ G →ₐ[ℂ] V →L[ℂ] V) (hφ : ∀ (g : G), φ (MonoidAlgebra.single g 1) = π g) : φ = discreteMeasureRep π

class ContinuousRep.CompactlySupportedMeasureAlgebra (G : Type uG) [Group G] [TopologicalSpace G] (M : Type uM) [Ring M] [Algebra ℂ M] [TopologicalSpace M] : Type (max uG uM)

• dirac : G →* M
• discrete_in_closure (m : M) : m ∈ closure (Set.range ⇑((MonoidAlgebra.lift ℂ M G) dirac))
• total_variation_cont (f : G → ℝ) (_hf : Continuous f) (_hf_nn : ∀ (g : G), 0 ≤ f g) : Continuous fun (μ : MonoidAlgebra ℂ G) => Finsupp.sum μ fun (g : G) (c : ℂ) => ‖c‖ * f g

theorem ContinuousRep.total_variation_eval_cont {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [inst : CompactlySupportedMeasureAlgebra G M] (f : G → ℝ) (hf : Continuous f) (hf_nn : ∀ (g : G), 0 ≤ f g) : Continuous fun (μ : MonoidAlgebra ℂ G) => Finsupp.sum μ fun (g : G) (c : ℂ) => ‖c‖ * f g

theorem ContinuousRep.rep_lift_opNorm_le {G : Type u_1} [Group G] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] (π : G →* V →L[ℂ] V) (μ : MonoidAlgebra ℂ G) : ‖((MonoidAlgebra.lift ℂ (V →L[ℂ] V) G) π) μ‖ ≤ Finsupp.sum μ fun (g : G) (c : ℂ) => ‖c‖ * ‖π g‖

theorem ContinuousRep.total_variation_eval_continuous {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [CompactlySupportedMeasureAlgebra G M] (f : G → ℝ) (hf : Continuous f) (hf_nn : ∀ (g : G), 0 ≤ f g) : Continuous fun (μ : MonoidAlgebra ℂ G) => Finsupp.sum μ fun (g : G) (c : ℂ) => ‖c‖ * f g

theorem ContinuousRep.rep_continuous_theorem {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousMul M] [CompactlySupportedMeasureAlgebra G M] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] (π : G →* V →L[ℂ] V) (hcont_norm : Continuous fun (g : G) => ‖π g‖) : Continuous ⇑((MonoidAlgebra.lift ℂ (V →L[ℂ] V) G) π)

theorem ContinuousRep.discrete_measures_sequentially_dense {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [inst : CompactlySupportedMeasureAlgebra G M] [FrechetUrysohnSpace M] (m : M) : m ∈ seqClosure (Set.range ⇑((MonoidAlgebra.lift ℂ M G) CompactlySupportedMeasureAlgebra.dirac))

theorem ContinuousRep.CompactlySupportedMeasureAlgebra.discrete_dense {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [inst : CompactlySupportedMeasureAlgebra G M] [FrechetUrysohnSpace M] : Dense (Set.range ⇑((MonoidAlgebra.lift ℂ M G) dirac))

theorem ContinuousRep.blt_alg_hom_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Semiring α] [Semiring β] [Semiring γ] [Algebra ℂ α] [Algebra ℂ β] [Algebra ℂ γ] [TopologicalSpace β] [ContinuousAdd β] [ContinuousMul β] [TopologicalSpace γ] [T2Space γ] [ContinuousAdd γ] [ContinuousMul γ] (ι : α →ₐ[ℂ] β) (f : α →ₐ[ℂ] γ) (h_dense : Dense (Set.range ⇑ι)) (g_fun : β → γ) (hg_cont : Continuous g_fun) (hg_ext : ∀ (x : α), g_fun (ι x) = f x) : ∃ (g : β →ₐ[ℂ] γ), Continuous ⇑g ∧ ∀ (x : α), g (ι x) = f x

theorem ContinuousRep.CompactlySupportedMeasureAlgebra.alg_hom_extend {G : Type uG} [Group G] [TopologicalSpace G] {M : Type uM} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousMul M] [inst : CompactlySupportedMeasureAlgebra G M] {A : Type u_1} [Ring A] [Algebra ℂ A] [inst_top_A : TopologicalSpace A] [inst_unif_A : UniformSpace A] [CompleteSpace A] [T2Space A] [ContinuousAdd A] [ContinuousMul A] [IsUniformAddGroup A] (f : MonoidAlgebra ℂ G →ₐ[ℂ] A) (h_dense : Dense (Set.range ⇑((MonoidAlgebra.lift ℂ M G) dirac))) (h_cont : Continuous ⇑f) (h_top_eq : inst_top_A = inst_unif_A.toTopologicalSpace := by rfl) : ∃ (g : M →ₐ[ℂ] A), Continuous ⇑g ∧ ∀ (μ : MonoidAlgebra ℂ G), g (((MonoidAlgebra.lift ℂ M G) dirac) μ) = f μ

@[reducible]

noncomputable def ContinuousRep.weakTopologyOnDiscreteMeasures {G : Type uG} [Group G] [TopologicalSpace G] {M : Type u_1} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [CompactlySupportedMeasureAlgebra G M] : TopologicalSpace (MonoidAlgebra ℂ G)

theorem ContinuousRep.continuous_opNorm_of_jointly_continuous {G : Type uG} [Group G] [TopologicalSpace G] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : G →* V →L[ℂ] V) (hcont : Continuous fun (p : G × V) => (π p.1) p.2) : Continuous fun (g : G) => ‖π g‖

theorem ContinuousRep.continuous_opNorm_of_jointly_continuous_general {G' : Type u_2} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] [LocallyCompactSpace G'] [SecondCountableTopology G'] {V' : Type u_3} [NormedAddCommGroup V'] [NormedSpace ℂ V'] [CompleteSpace V'] (π : G' →* V' →L[ℂ] V') (hcont : Continuous fun (p : G' × V') => (π p.1) p.2) : Continuous fun (g : G') => ‖π g‖

theorem ContinuousRep.discreteMeasureRep_continuous_to_opnorm {G : Type uG} [Group G] [TopologicalSpace G] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] {M : Type u_1} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousMul M] [CompactlySupportedMeasureAlgebra G M] (π : G →* V →L[ℂ] V) (hcont : Continuous fun (p : G × V) => (π p.1) p.2) [FiniteDimensional ℂ V] : Continuous ⇑(discreteMeasureRep π)

theorem ContinuousRep.discreteMeasureRep_weakly_continuous {G : Type uG} [Group G] [TopologicalSpace G] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] {M : Type u_1} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousMul M] [CompactlySupportedMeasureAlgebra G M] (π : G →* V →L[ℂ] V) (hcont : Continuous fun (p : G × V) => (π p.1) p.2) [FiniteDimensional ℂ V] : Continuous fun (p : MonoidAlgebra ℂ G × V) => ((discreteMeasureRep π) p.1) p.2

theorem ContinuousRep.discreteMeasureRep_BLT_extension {G : Type uG} [Group G] [TopologicalSpace G] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] {M : Type u_1} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousMul M] [CompactlySupportedMeasureAlgebra G M] (π : G →* V →L[ℂ] V) (hcont : Continuous fun (p : G × V) => (π p.1) p.2) [FiniteDimensional ℂ V] (h_dense : Dense (Set.range ⇑((MonoidAlgebra.lift ℂ M G) CompactlySupportedMeasureAlgebra.dirac))) : ∃ (π_ext : M →ₐ[ℂ] V →L[ℂ] V), Continuous ⇑π_ext ∧ ∀ (μ : MonoidAlgebra ℂ G), π_ext (((MonoidAlgebra.lift ℂ M G) CompactlySupportedMeasureAlgebra.dirac) μ) = (discreteMeasureRep π) μ

theorem ContinuousRep.measureRep_exists_extension {G : Type uG} [Group G] [TopologicalSpace G] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] {M : Type u_1} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousMul M] [CompactlySupportedMeasureAlgebra G M] [FrechetUrysohnSpace M] (π : G →* V →L[ℂ] V) (hcont : Continuous fun (p : G × V) => (π p.1) p.2) [FiniteDimensional ℂ V] : ∃ (π_ext : M →ₐ[ℂ] V →L[ℂ] V), Continuous ⇑π_ext ∧ (∀ (g : G), π_ext (CompactlySupportedMeasureAlgebra.dirac g) = π g) ∧ ∀ (μ : MonoidAlgebra ℂ G), π_ext (((MonoidAlgebra.lift ℂ M G) CompactlySupportedMeasureAlgebra.dirac) μ) = (discreteMeasureRep π) μ

theorem ContinuousRep.measureRep_continuous_bilinear {G : Type uG} [Group G] [TopologicalSpace G] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] {M : Type u_1} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [CompactlySupportedMeasureAlgebra G M] (π : G →* V →L[ℂ] V) (hcont : Continuous fun (p : G × V) => (π p.1) p.2) [FiniteDimensional ℂ V] (π_ext : M →ₐ[ℂ] V →L[ℂ] V) (h_extends : ∀ (g : G), π_ext (CompactlySupportedMeasureAlgebra.dirac g) = π g) (hcont_ext : Continuous ⇑π_ext) : Continuous fun (p : M × V) => (π_ext p.1) p.2

theorem ContinuousRep.measureRep_continuous_extension {G : Type uG} [Group G] [TopologicalSpace G] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] {M : Type u_1} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousMul M] [CompactlySupportedMeasureAlgebra G M] [FrechetUrysohnSpace M] (π : G →* V →L[ℂ] V) (hcont : Continuous fun (p : G × V) => (π p.1) p.2) [FiniteDimensional ℂ V] : ∃ (π_ext : M →ₐ[ℂ] V →L[ℂ] V), (∀ (g : G), π_ext (CompactlySupportedMeasureAlgebra.dirac g) = π g) ∧ Continuous ⇑π_ext ∧ Continuous fun (p : M × V) => (π_ext p.1) p.2

theorem ContinuousRep.corollary_3_8 {G : Type uG} [Group G] [TopologicalSpace G] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] {M : Type u_1} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousMul M] [CompactlySupportedMeasureAlgebra G M] [FrechetUrysohnSpace M] [IsTopologicalGroup G] [LocallyCompactSpace G] [SecondCountableTopology G] (π : G →* V →L[ℂ] V) (hcont : Continuous fun (p : G × V) => (π p.1) p.2) [CompleteSpace V] : (∃ (π_ext : M →ₐ[ℂ] V →L[ℂ] V), (∀ (g : G), π_ext (CompactlySupportedMeasureAlgebra.dirac g) = π g) ∧ Continuous ⇑π_ext ∧ Continuous fun (p : M × V) => (π_ext p.1) p.2) ∧ ∀ (φ₁ φ₂ : M →ₐ[ℂ] V →L[ℂ] V), (∀ (g : G), φ₁ (CompactlySupportedMeasureAlgebra.dirac g) = π g) → (∀ (g : G), φ₂ (CompactlySupportedMeasureAlgebra.dirac g) = π g) → (Continuous fun (p : M × V) => (φ₁ p.1) p.2) → (Continuous fun (p : M × V) => (φ₂ p.1) p.2) → φ₁ = φ₂

theorem ContinuousRep.measureRep_unique_extension {G : Type uG} [Group G] [TopologicalSpace G] {V : Type uG} [NormedAddCommGroup V] [NormedSpace ℂ V] {M : Type u_1} [Ring M] [Algebra ℂ M] [TopologicalSpace M] [CompactlySupportedMeasureAlgebra G M] [FrechetUrysohnSpace M] (π : G →* V →L[ℂ] V) (hcont : Continuous fun (p : G × V) => (π p.1) p.2) [CompleteSpace V] (φ₁ φ₂ : M →ₐ[ℂ] V →L[ℂ] V) (h₁ : ∀ (g : G), φ₁ (CompactlySupportedMeasureAlgebra.dirac g) = π g) (h₂ : ∀ (g : G), φ₂ (CompactlySupportedMeasureAlgebra.dirac g) = π g) (hcont₁ : Continuous fun (p : M × V) => (φ₁ p.1) p.2) (hcont₂ : Continuous fun (p : M × V) => (φ₂ p.1) p.2) : φ₁ = φ₂

def ContinuousRep.IsKFiniteFunc {G : Type uG} [Group G] (K : Subgroup G) (f : ↥K → ℂ) : Prop

theorem ContinuousRep.finite_of_allKFiniteFunc {G : Type uG} [Group G] [TopologicalSpace G] (K : Subgroup G) [CompactSpace ↥K] (hall : ∀ (f : ↥K → ℂ), IsKFiniteFunc K f) : Finite ↥K

theorem ContinuousRep.haarConvolution_infinite_case_exists {G : Type u_2} [Group G] [TopologicalSpace G] {V : Type u_3} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (K : Subgroup G) [CompactSpace ↥K] (hnotall : ¬∀ (f : ↥K → ℂ), IsKFiniteFunc K f) : ∃ (R : (↥K → ℂ) → V → V), (∀ (f : ↥K → ℂ) (v : V), IsKFiniteFunc K f → R f v ∈ π.kFiniteSubspace K) ∧ (∀ (v : V), ∀ U ∈ nhds v, ∃ (f : ↥K → ℂ), R f v ∈ U) ∧ ∀ (f : ↥K → ℂ) (v : V), ∀ U ∈ nhds (R f v), ∃ (g : ↥K → ℂ), IsKFiniteFunc K g ∧ R g v ∈ U

theorem ContinuousRep.measureRep_exists {G : Type uG} [Group G] [TopologicalSpace G] {V : Type u_1} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (K : Subgroup G) [CompactSpace ↥K] : ∃ (R : (↥K → ℂ) → V → V), (∀ (f : ↥K → ℂ) (v : V), IsKFiniteFunc K f → R f v ∈ π.kFiniteSubspace K) ∧ (∀ (v : V), ∀ U ∈ nhds v, ∃ (f : ↥K → ℂ), R f v ∈ U) ∧ ∀ (f : ↥K → ℂ) (v : V), ∀ U ∈ nhds (R f v), ∃ (g : ↥K → ℂ), IsKFiniteFunc K g ∧ R g v ∈ U

theorem ContinuousRep.kFiniteSubspace_dense {G : Type uG} [Group G] [TopologicalSpace G] {V : Type u_1} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (K : Subgroup G) [CompactSpace ↥K] : Dense ↑(π.kFiniteSubspace K)

theorem ContinuousRep.isotypicComponent_hasOrthogonalProjection {G : Type uG} [Group G] [TopologicalSpace G] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [IsTopologicalGroup G] [CompactSpace G] {Wσ : Type u_2} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (π : ContinuousRep G E) (K : Subgroup G) [CompactSpace ↥K] (σ : ContinuousRep (↥K) Wσ) : (π.IsotypicComponent K σ).HasOrthogonalProjection

instance ContinuousRep.isotypicComponent_instHasOrthogonalProjection {G : Type uG} [Group G] [TopologicalSpace G] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [IsTopologicalGroup G] [CompactSpace G] {Wσ : Type u_2} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (π : ContinuousRep G E) (K : Subgroup G) [CompactSpace ↥K] (σ : ContinuousRep (↥K) Wσ) : (π.IsotypicComponent K σ).HasOrthogonalProjection

noncomputable def ContinuousRep.isotypicProjection {G : Type uG} [Group G] [TopologicalSpace G] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [IsTopologicalGroup G] [CompactSpace G] {Wσ : Type u_2} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (π : ContinuousRep G E) (K : Subgroup G) [CompactSpace ↥K] (σ : ContinuousRep (↥K) Wσ) : E →L[ℂ] E

theorem ContinuousRep.isotypicProjection_idempotent {G : Type uG} [Group G] [TopologicalSpace G] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [IsTopologicalGroup G] [CompactSpace G] {Wσ : Type u_2} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (π : ContinuousRep G E) (_hU : π.IsUnitary) (K : Subgroup G) [CompactSpace ↥K] (σ : ContinuousRep (↥K) Wσ) : (π.isotypicProjection K σ).comp (π.isotypicProjection K σ) = π.isotypicProjection K σ

theorem ContinuousRep.isotypicProjection_range {G : Type uG} [Group G] [TopologicalSpace G] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [IsTopologicalGroup G] [CompactSpace G] {Wσ : Type u_2} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (π : ContinuousRep G E) (_hU : π.IsUnitary) (K : Subgroup G) [CompactSpace ↥K] (σ : ContinuousRep (↥K) Wσ) : (↑(π.isotypicProjection K σ)).range = π.IsotypicComponent K σ