structure HarishChandraPair (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] [TopologicalSpace K] [CompactSpace K] : Type (max u_1 u_2)

• 𝔨 : LieSubalgebra ℂ 𝔤
• Ad : K →* 𝔤 →ₗ[ℂ] 𝔤

def GKModule.lieIterate {𝔤 : Type u_1} [LieRing 𝔤] {V : Type u_3} [AddCommGroup V] [LieRingModule 𝔤 V] (Xs : List 𝔤) (v : V) : V

def GKModule.IsHarishChandraModule {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) : Prop

structure SemisimpleLieGroup : Type (max (u_1 + 1) (u_2 + 1))

• G : Type u_1
• instGroup : Group self.G
• instTopologicalSpace : TopologicalSpace self.G
• instIsTopologicalGroup : IsTopologicalGroup self.G
• 𝔤 : Type u_2
• instLieRing : LieRing self.𝔤
• instLieAlgebra : LieAlgebra ℝ self.𝔤
• isSemisimple : LieAlgebra.IsSemisimple ℝ self.𝔤
• lieExp : self.𝔤 → self.G
• lieExp_zero : self.lieExp 0 = One.one

@[implicit_reducible]

instance instGroupG (SG : SemisimpleLieGroup) : Group SG.G

@[implicit_reducible]

instance instTopologicalSpaceG (SG : SemisimpleLieGroup) : TopologicalSpace SG.G

instance instIsTopologicalGroupG (SG : SemisimpleLieGroup) : IsTopologicalGroup SG.G

@[implicit_reducible]

instance instLieRing𝔤 (SG : SemisimpleLieGroup) : LieRing SG.𝔤

@[implicit_reducible]

instance instLieAlgebraReal𝔤 (SG : SemisimpleLieGroup) : LieAlgebra ℝ SG.𝔤

def IsMaximalCompactSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] (K : Subgroup G) [TopologicalSpace ↥K] [CompactSpace ↥K] : Prop

theorem SemisimpleLieGroup.exists_maximalCompactSubgroup (SG : SemisimpleLieGroup) : ∃ (K : Subgroup SG.G) (x : TopologicalSpace ↥K) (x_1 : CompactSpace ↥K), IsMaximalCompactSubgroup K

theorem harishChandra_admissibility (SG : SemisimpleLieGroup) {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (π : ContinuousRep SG.G E) (K : Subgroup SG.G) [TopologicalSpace ↥K] [hK_compact : CompactSpace ↥K] (hK_max : IsMaximalCompactSubgroup K) (hirr : π.IsIrreducible) (hunit : π.IsUnitary) : π.IsAdmissible K

def GKModule.IsFiniteLength {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) : Prop