@[reducible]

def kFiniteSubspace_lieRingModule {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) (_hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) (hι_stable : ∀ (X : 𝔤), ∀ v ∈ π.kFiniteSubspace K_sub, (ι X) v ∈ π.kFiniteSubspace K_sub) : LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)

@[reducible]

def kFiniteSubspace_lieModule {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) (_hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) (hι_stable : ∀ (X : 𝔤), ∀ v ∈ π.kFiniteSubspace K_sub, (ι X) v ∈ π.kFiniteSubspace K_sub) : LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)

def kFiniteSubspace_kAction {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) : Representation ℂ ↥K_sub ↥(π.kFiniteSubspace K_sub)

theorem kFiniteSubspace_kAction_locallyFinite {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) : (kFiniteSubspace_kAction π K_sub).IsLocallyFinite

def harishChandraGKModule {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) (_hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (_ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)] (hequiv : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆) : GKModule 𝔤 (↥K_sub) 𝔨 Ad ↥(π.kFiniteSubspace K_sub)

theorem peterWeyl_isotypic_embedding {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤} [LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)] (M : GKModule 𝔤 (↥K_sub) 𝔨 Ad ↥(π.kFiniteSubspace K_sub)) (hMσ : M.σ = kFiniteSubspace_kAction π K_sub) (W₀ : Submodule ℂ ↥(π.kFiniteSubspace K_sub)) (hW₀ : M.IsKIrreducible W₀) : ∃ (Wσ : Type u_4) (x : AddCommGroup Wσ) (x_1 : Module ℂ Wσ) (x_2 : TopologicalSpace Wσ) (σ : ContinuousRep (↥K_sub) Wσ) (_ : σ.IsIrreducible), Submodule.map (π.kFiniteSubspace K_sub).subtype (M.KIsotypicComponent W₀ hW₀) ≤ π.IsotypicComponent K_sub σ

theorem harishChandraGKModule_isAdmissible {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) (hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)] (hequiv : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆) : (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsAdmissible

theorem kFiniteSubspace_dense_admissible {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm : π.IsAdmissible K_sub) : Dense ↑(π.kFiniteSubspace K_sub)

def iterLieAction {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {F : Type u_2} [AddCommGroup F] [Module ℂ F] (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) (Xs : List 𝔤) (v : F) : F

theorem iterLieAction_mem_kFiniteSubspace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) (hι_stable : ∀ (X : 𝔤), ∀ w ∈ π.kFiniteSubspace K_sub, (ι X) w ∈ π.kFiniteSubspace K_sub) (Xs : List 𝔤) (v : F) (hv : v ∈ π.kFiniteSubspace K_sub) : iterLieAction ι Xs v ∈ π.kFiniteSubspace K_sub

theorem iterLieAction_agree_of_eq_on_kFinite {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (ι₁ ι₂ : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) (hlie_eq : ∀ (X : 𝔤), ∀ w ∈ π.kFiniteSubspace K_sub, (ι₁ X) w = (ι₂ X) w) (hι₁_stable : ∀ (X : 𝔤), ∀ w ∈ π.kFiniteSubspace K_sub, (ι₁ X) w ∈ π.kFiniteSubspace K_sub) (hι₂_stable : ∀ (X : 𝔤), ∀ w ∈ π.kFiniteSubspace K_sub, (ι₂ X) w ∈ π.kFiniteSubspace K_sub) (Xs : List 𝔤) (v : F) (hv : v ∈ π.kFiniteSubspace K_sub) : iterLieAction ι₁ Xs v = iterLieAction ι₂ Xs v

theorem elliptic_regularity_analytic_continuation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π₁ π₂ : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (_hadm₁ : π₁.IsAdmissible K_sub) (_hadm₂ : π₂.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (ι₁ ι₂ : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) (v : F) (_hv : v ∈ π₁.kFiniteSubspace K_sub) (h : F →L[ℂ] ℂ) (hiter_eq : ∀ (Xs : List 𝔤), h (iterLieAction ι₁ Xs v) = h (iterLieAction ι₂ Xs v)) (g : G) : h ((π₁.toMonoidHom g) v) = h ((π₂.toMonoidHom g) v)

theorem analytic_matcoeff_eq_of_iterAction_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π₁ π₂ : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (_hadm₁ : π₁.IsAdmissible K_sub) (_hadm₂ : π₂.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (ι₁ ι₂ : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) (v : F) (hv : v ∈ π₁.kFiniteSubspace K_sub) (h : F →L[ℂ] ℂ) (hiter_eq : ∀ (Xs : List 𝔤), h (iterLieAction ι₁ Xs v) = h (iterLieAction ι₂ Xs v)) (g : G) : h ((π₁.toMonoidHom g) v) = h ((π₂.toMonoidHom g) v)

theorem trivialRep_isAdmissible {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (K_sub : Subgroup G) [CompactSpace ↥K_sub] : { toMonoidHom := 1, continuous_action := ⋯ }.IsAdmissible K_sub

theorem analytic_matcoeff_vanishing {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (_hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) (v : F) (_hv : v ∈ π.kFiniteSubspace K_sub) (h : F →L[ℂ] ℂ) (hvanish : ∀ (Xs : List 𝔤), h (iterLieAction ι Xs v) = 0) (g : G) : h ((π.toMonoidHom g) v) = 0

theorem separation_from_closed_submodule {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (S : Submodule ℂ F) (hS : IsClosed ↑S) (x : F) (hx : x ∉ S) : ∃ (h : F →L[ℂ] ℂ), (∀ s ∈ S, h s = 0) ∧ h x ≠ 0

theorem iterLieAction_mem_image_submodule {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {F : Type u_2} [AddCommGroup F] [Module ℂ F] {V : Submodule ℂ F} (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥V] [LieModule ℂ 𝔤 ↥V] (hι_compat : ∀ (X : 𝔤) (w : ↥V), V.subtype ⁅X, w⁆ = (ι X) (V.subtype w)) (W : Submodule ℂ ↥V) (hW_lie : ∀ (X : 𝔤), ∀ w ∈ W, ⁅X, w⁆ ∈ W) (Xs : List 𝔤) (w : ↥V) (hw : w ∈ W) : iterLieAction ι Xs (V.subtype w) ∈ Submodule.map V.subtype W

theorem analytic_matrixCoeff_eq_of_lie_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π₁ π₂ : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm₁ : π₁.IsAdmissible K_sub) (hadm₂ : π₂.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (ι₁ ι₂ : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) (hlie_eq : ∀ (X : 𝔤), ∀ v ∈ π₁.kFiniteSubspace K_sub, (ι₁ X) v = (ι₂ X) v) (hι₂_stable : ∀ (X : 𝔤), ∀ w ∈ π₁.kFiniteSubspace K_sub, (ι₂ X) w ∈ π₁.kFiniteSubspace K_sub) (h : F →L[ℂ] ℂ) (g : G) (v : F) (hv : v ∈ π₁.kFiniteSubspace K_sub) : h ((π₁.toMonoidHom g) v) = h ((π₂.toMonoidHom g) v)

theorem harish_chandra_analyticity_matrixCoeff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π₁ π₂ : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm₁ : π₁.IsAdmissible K_sub) (hadm₂ : π₂.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (ι₁ ι₂ : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) (hlie_eq : ∀ (X : 𝔤), ∀ v ∈ π₁.kFiniteSubspace K_sub, (ι₁ X) v = (ι₂ X) v) (hι₂_stable : ∀ (X : 𝔤), ∀ w ∈ π₁.kFiniteSubspace K_sub, (ι₂ X) w ∈ π₁.kFiniteSubspace K_sub) (hK_eq : ∀ (k : ↥K_sub), ∀ v ∈ π₁.kFiniteSubspace K_sub, (π₁.toMonoidHom ↑k) v = (π₂.toMonoidHom ↑k) v) (h : F →L[ℂ] ℂ) (g : G) (v : F) (hv : v ∈ π₁.kFiniteSubspace K_sub) : h ((π₁.toMonoidHom g) v) = h ((π₂.toMonoidHom g) v)

theorem gAction_on_kFinite_determined_by_gkModule {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π₁ π₂ : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm₁ : π₁.IsAdmissible K_sub) (hadm₂ : π₂.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (ι₁ ι₂ : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥(π₁.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π₁.kFiniteSubspace K_sub)] [LieRingModule 𝔤 ↥(π₂.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π₂.kFiniteSubspace K_sub)] (hequiv₁ : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π₁ K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π₁ K_sub) k) v⁆) (hequiv₂ : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π₂.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π₂ K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π₂ K_sub) k) v⁆) (hkfin_eq : ↑(π₁.kFiniteSubspace K_sub) = ↑(π₂.kFiniteSubspace K_sub)) (hlie_eq : ∀ (X : 𝔤), ∀ v ∈ π₁.kFiniteSubspace K_sub, (ι₁ X) v = (ι₂ X) v) (hι₂_stable : ∀ (X : 𝔤), ∀ w ∈ π₁.kFiniteSubspace K_sub, (ι₂ X) w ∈ π₁.kFiniteSubspace K_sub) (hK_eq : ∀ (k : ↥K_sub), ∀ v ∈ π₁.kFiniteSubspace K_sub, (π₁.toMonoidHom ↑k) v = (π₂.toMonoidHom ↑k) v) (g : G) (v : F) : v ∈ π₁.kFiniteSubspace K_sub → (π₁.toMonoidHom g) v = (π₂.toMonoidHom g) v

theorem gAction_determined_by_gkModule {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π₁ π₂ : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (_hK_max : IsMaximalCompactSubgroup K_sub) (hadm₁ : π₁.IsAdmissible K_sub) (hadm₂ : π₂.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (ι₁ ι₂ : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥(π₁.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π₁.kFiniteSubspace K_sub)] [LieRingModule 𝔤 ↥(π₂.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π₂.kFiniteSubspace K_sub)] (hequiv₁ : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π₁ K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π₁ K_sub) k) v⁆) (hequiv₂ : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π₂.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π₂ K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π₂ K_sub) k) v⁆) (hkfin_eq : ↑(π₁.kFiniteSubspace K_sub) = ↑(π₂.kFiniteSubspace K_sub)) (hlie_eq : ∀ (X : 𝔤), ∀ v ∈ π₁.kFiniteSubspace K_sub, (ι₁ X) v = (ι₂ X) v) (hι₂_stable : ∀ (X : 𝔤), ∀ w ∈ π₁.kFiniteSubspace K_sub, (ι₂ X) w ∈ π₁.kFiniteSubspace K_sub) (hK_eq : ∀ (k : ↥K_sub), ∀ v ∈ π₁.kFiniteSubspace K_sub, (π₁.toMonoidHom ↑k) v = (π₂.toMonoidHom ↑k) v) : π₁ = π₂

theorem continuous_map_eq_of_eq_on_kFinite {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm : π.IsAdmissible K_sub) {W : Type u_5} [NormedAddCommGroup W] [NormedSpace ℂ W] (f g : F →L[ℂ] W) (heq : ∀ v ∈ π.kFiniteSubspace K_sub, f v = g v) : f = g

theorem derived_rep_preserves_closed_ginvariant_subspace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) (hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) (U : Submodule ℂ F) (hU : π.IsInvariantSubspace U) (X : 𝔤) (v : F) : v ∈ U → (ι X) v ∈ U

theorem lie_action_preserves_invariant_subspace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) (hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)] (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) (hι_compat : ∀ (X : 𝔤) (w : ↥(π.kFiniteSubspace K_sub)), (π.kFiniteSubspace K_sub).subtype ⁅X, w⁆ = (ι X) ((π.kFiniteSubspace K_sub).subtype w)) (U : Submodule ℂ F) (hU : π.IsInvariantSubspace U) (hι_inv : ∀ (X : 𝔤), ∀ v ∈ U, (ι X) v ∈ U) (X : 𝔤) (w : ↥(π.kFiniteSubspace K_sub)) (hw : (π.kFiniteSubspace K_sub).subtype w ∈ U) : (π.kFiniteSubspace K_sub).subtype ⁅X, w⁆ ∈ U

theorem gkSubmodule_image_maps_into_closure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)] (hequiv : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆) (hι_compat : ∀ (X : 𝔤) (w : ↥(π.kFiniteSubspace K_sub)), (π.kFiniteSubspace K_sub).subtype ⁅X, w⁆ = (ι X) ((π.kFiniteSubspace K_sub).subtype w)) (W : Submodule ℂ ↥(π.kFiniteSubspace K_sub)) (hW : (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsSubmodule W) : have S := Submodule.map (π.kFiniteSubspace K_sub).subtype W; ∀ (g : G), ∀ v ∈ S, (π.toMonoidHom g) v ∈ S.topologicalClosure

theorem closure_gkSubmodule_gInvariant {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)] (hequiv : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆) (hι_compat : ∀ (X : 𝔤) (w : ↥(π.kFiniteSubspace K_sub)), (π.kFiniteSubspace K_sub).subtype ⁅X, w⁆ = (ι X) ((π.kFiniteSubspace K_sub).subtype w)) (W : Submodule ℂ ↥(π.kFiniteSubspace K_sub)) (hW : (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsSubmodule W) : have S := Submodule.map (π.kFiniteSubspace K_sub).subtype W; ∀ (g : G), ∀ v ∈ S.topologicalClosure, (π.toMonoidHom g) v ∈ S.topologicalClosure

theorem peterWeyl_finsupp_projector {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) (v : F) (hv : v ∈ π.kFiniteSubspace K_sub) : ∃ (c : ↥K_sub →₀ ℂ), (c.sum fun (k : ↥K_sub) (a : ℂ) => a • π.toMonoidHom ↑k) v = v ∧ ∀ {F₂ : Type u_3} [inst : NormedAddCommGroup F₂] [inst_1 : NormedSpace ℂ F₂] (π₂ : ContinuousRep G F₂), FiniteDimensional ℂ ↥(↑(c.sum fun (k : ↥K_sub) (a : ℂ) => a • π₂.toMonoidHom ↑k)).range ∧ ∀ (k : ↥K_sub), (c.sum fun (k : ↥K_sub) (a : ℂ) => a • π₂.toMonoidHom ↑k).comp (π₂.toMonoidHom ↑k) = (π₂.toMonoidHom ↑k).comp (c.sum fun (k : ↥K_sub) (a : ℂ) => a • π₂.toMonoidHom ↑k)

theorem isotypicProjector_finiteRange_fix_commute {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) (v : F) (hv : v ∈ π.kFiniteSubspace K_sub) : ∃ (P : F →L[ℂ] F), FiniteDimensional ℂ ↥(↑P).range ∧ P v = v ∧ (∀ (k : ↥K_sub), P.comp (π.toMonoidHom ↑k) = (π.toMonoidHom ↑k).comp P) ∧ ∀ (S : Submodule ℂ F), (∀ (k : ↥K_sub), ∀ s ∈ S, (π.toMonoidHom ↑k) s ∈ S) → ∀ s ∈ S, s ∈ π.kFiniteSubspace K_sub → P s ∈ S

theorem closure_kFinite_roundtrip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) (hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)] (hequiv : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆) (W : Submodule ℂ ↥(π.kFiniteSubspace K_sub)) (hW : (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsSubmodule W) : have S := Submodule.map (π.kFiniteSubspace K_sub).subtype W; ∀ (v : ↥(π.kFiniteSubspace K_sub)), ↑v ∈ S.topologicalClosure → v ∈ W

theorem kFinite_dense_in_invariant_subspace_submodule {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm : π.IsAdmissible K_sub) (U : Submodule ℂ F) (hU : π.IsInvariantSubspace U) : have S := Submodule.map (π.kFiniteSubspace K_sub).subtype (Submodule.comap (π.kFiniteSubspace K_sub).subtype U); S.topologicalClosure = U

theorem gkSubmodule_closure_correspondence {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)] (hequiv : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆) (hι_compat : ∀ (X : 𝔤) (w : ↥(π.kFiniteSubspace K_sub)), (π.kFiniteSubspace K_sub).subtype ⁅X, w⁆ = (ι X) ((π.kFiniteSubspace K_sub).subtype w)) : have M := harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv; (∀ (U : Submodule ℂ F), π.IsInvariantSubspace U → M.IsSubmodule (Submodule.comap (π.kFiniteSubspace K_sub).subtype U)) ∧ (∀ (W : Submodule ℂ ↥(π.kFiniteSubspace K_sub)), M.IsSubmodule W → ∃ (U : Submodule ℂ F), π.IsInvariantSubspace U ∧ Submodule.comap (π.kFiniteSubspace K_sub).subtype U = W) ∧ ∀ (U₁ U₂ : Submodule ℂ F), π.IsInvariantSubspace U₁ → π.IsInvariantSubspace U₂ → Submodule.comap (π.kFiniteSubspace K_sub).subtype U₁ = Submodule.comap (π.kFiniteSubspace K_sub).subtype U₂ → U₁ = U₂

theorem harishChandra_preserves_irreducibility {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm : π.IsAdmissible K_sub) (hirr : π.IsIrreducible) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)] (hequiv : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆) (hι_compat : ∀ (X : 𝔤) (w : ↥(π.kFiniteSubspace K_sub)), (π.kFiniteSubspace K_sub).subtype ⁅X, w⁆ = (ι X) ((π.kFiniteSubspace K_sub).subtype w)) (hι_preserves : ∀ (U : Submodule ℂ F), π.IsInvariantSubspace U → ∀ (X : 𝔤), ∀ v ∈ U, (ι X) v ∈ U) : (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsIrreducibleGKModule

theorem harishChandra_reflects_irreducibility {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)] (hequiv : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆) (hι_compat : ∀ (X : 𝔤) (w : ↥(π.kFiniteSubspace K_sub)), (π.kFiniteSubspace K_sub).subtype ⁅X, w⁆ = (ι X) ((π.kFiniteSubspace K_sub).subtype w)) (hι_preserves : ∀ (U : Submodule ℂ F), π.IsInvariantSubspace U → ∀ (X : 𝔤), ∀ v ∈ U, (ι X) v ∈ U) (hirr_gk : (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsIrreducibleGKModule) : π.IsIrreducible

theorem harishChandra_irreducibility_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)] (hequiv : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆) (hι_compat : ∀ (X : 𝔤) (w : ↥(π.kFiniteSubspace K_sub)), (π.kFiniteSubspace K_sub).subtype ⁅X, w⁆ = (ι X) ((π.kFiniteSubspace K_sub).subtype w)) (hι_preserves : ∀ (U : Submodule ℂ F), π.IsInvariantSubspace U → ∀ (X : 𝔤), ∀ v ∈ U, (ι X) v ∈ U) : π.IsIrreducible ↔ (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsIrreducibleGKModule

theorem repHom_maps_kFinite {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F₁ : Type u_2} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] {F₂ : Type u_3} [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] (π₁ : ContinuousRep G F₁) (π₂ : ContinuousRep G F₂) (K_sub : Subgroup G) (T : RepHom π₁ π₂) (v : F₁) (hv : v ∈ π₁.kFiniteSubspace K_sub) : T.toContinuousLinearMap v ∈ π₂.kFiniteSubspace K_sub

def repHom_restrict_kFinite {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F₁ : Type u_2} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] {F₂ : Type u_3} [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] (π₁ : ContinuousRep G F₁) (π₂ : ContinuousRep G F₂) (K_sub : Subgroup G) (T : RepHom π₁ π₂) : ↥(π₁.kFiniteSubspace K_sub) →ₗ[ℂ] ↥(π₂.kFiniteSubspace K_sub)

theorem kEquivariant_finiteRange_maps_to_kFinite {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) (P : F →L[ℂ] F) (hfin : FiniteDimensional ℂ ↥(↑P).range) (hcomm : ∀ (k : ↥K_sub), P.comp (π.toMonoidHom ↑k) = (π.toMonoidHom ↑k).comp P) (w : F) : P w ∈ π.kFiniteSubspace K_sub

theorem finsupp_rep_intertwines {G : Type u_1} [Group G] [TopologicalSpace G] {F₂ : Type u_2} [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] {F₃ : Type u_3} [NormedAddCommGroup F₃] [NormedSpace ℂ F₃] (π₂ : ContinuousRep G F₂) (π₃ : ContinuousRep G F₃) (S : RepHom π₂ π₃) (K_sub : Subgroup G) (c : ↥K_sub →₀ ℂ) (w : F₂) : S.toContinuousLinearMap ((c.sum fun (k : ↥K_sub) (a : ℂ) => a • π₂.toMonoidHom ↑k) w) = (c.sum fun (k : ↥K_sub) (a : ℂ) => a • π₃.toMonoidHom ↑k) (S.toContinuousLinearMap w)

theorem peter_weyl_surjective_kfinite_lift {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F₂ : Type u_2} [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] {F₃ : Type u_3} [NormedAddCommGroup F₃] [NormedSpace ℂ F₃] (π₂ : ContinuousRep G F₂) (π₃ : ContinuousRep G F₃) (K_sub : Subgroup G) (S : RepHom π₂ π₃) (hS_surj : Function.Surjective ⇑S.toContinuousLinearMap) (v₃ : F₃) (hv₃ : v₃ ∈ π₃.kFiniteSubspace K_sub) : ∃ w ∈ π₂.kFiniteSubspace K_sub, S.toContinuousLinearMap w = v₃

theorem surjective_repHom_kFinite {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F₂ : Type u_2} [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] {F₃ : Type u_3} [NormedAddCommGroup F₃] [NormedSpace ℂ F₃] (π₂ : ContinuousRep G F₂) (π₃ : ContinuousRep G F₃) (K_sub : Subgroup G) (S : RepHom π₂ π₃) (hS_surj : Function.Surjective ⇑S.toContinuousLinearMap) (v₃ : F₃) (hv₃ : v₃ ∈ π₃.kFiniteSubspace K_sub) : ∃ w ∈ π₂.kFiniteSubspace K_sub, S.toContinuousLinearMap w = v₃

theorem theorem_6_16_irreducibility {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K_sub : Subgroup G) [CompactSpace ↥K_sub] (hadm : π.IsAdmissible K_sub) (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F) [LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)] (hequiv : ∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)), ((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆) (hι_compat : ∀ (X : 𝔤) (w : ↥(π.kFiniteSubspace K_sub)), (π.kFiniteSubspace K_sub).subtype ⁅X, w⁆ = (ι X) ((π.kFiniteSubspace K_sub).subtype w)) (hι_preserves : ∀ (U : Submodule ℂ F), π.IsInvariantSubspace U → ∀ (X : 𝔤), ∀ v ∈ U, (ι X) v ∈ U) : π.IsIrreducible ↔ (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsIrreducibleGKModule

structure UnitaryRepEquiv {G : Type u_1} [Group G] [TopologicalSpace G] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {W : Type u_3} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] (π₁ : ContinuousRep G V) (π₂ : ContinuousRep G W) extends RepEquiv π₁ π₂ : Type (max u_2 u_3)

• toContinuousLinearEquiv : V ≃L[ℂ] W
• intertwines (g : G) : (↑self.toContinuousLinearEquiv).comp (π₁.toMonoidHom g) = (π₂.toMonoidHom g).comp ↑self.toContinuousLinearEquiv
• inner_preserving (v w : V) : inner ℂ (self.toContinuousLinearEquiv v) (self.toContinuousLinearEquiv w) = inner ℂ v w

theorem prop_7_1_schur_and_equivariance {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F₁ : Type u_4} [NormedAddCommGroup F₁] [InnerProductSpace ℂ F₁] [CompleteSpace F₁] {F₂ : Type u_5} [NormedAddCommGroup F₂] [InnerProductSpace ℂ F₂] [CompleteSpace F₂] (π₁ : ContinuousRep G F₁) (π₂ : ContinuousRep G F₂) (K_sub : Subgroup G) [hK_compact : CompactSpace ↥K_sub] (hadm₁ : π₁.IsAdmissible K_sub) (hadm₂ : π₂.IsAdmissible K_sub) (hunit₁ : π₁.IsUnitary) (hunit₂ : π₂.IsUnitary) (𝔤 : Type u_6) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤) (ι₁ : 𝔤 →ₗ⁅ℂ⁆ F₁ →ₗ[ℂ] F₁) (ι₂ : 𝔤 →ₗ⁅ℂ⁆ F₂ →ₗ[ℂ] F₂) [LieRingModule 𝔤 ↥(π₁.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π₁.kFiniteSubspace K_sub)] [LieRingModule 𝔤 ↥(π₂.kFiniteSubspace K_sub)] [LieModule ℂ 𝔤 ↥(π₂.kFiniteSubspace K_sub)] (A : ↥(π₁.kFiniteSubspace K_sub) ≃ₗ[ℂ] ↥(π₂.kFiniteSubspace K_sub)) (hA_lie : ∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), A ⁅X, v⁆ = ⁅X, A v⁆) (hA_K : ∀ (k : ↥K_sub) (v : ↥(π₁.kFiniteSubspace K_sub)), A (((kFiniteSubspace_kAction π₁ K_sub) k) v) = ((kFiniteSubspace_kAction π₂ K_sub) k) (A v)) (h_dense₁ : DenseRange ⇑(π₁.kFiniteSubspace K_sub).subtype) (h_dense₂ : DenseRange ⇑(π₂.kFiniteSubspace K_sub).subtype) : ∃ (h_norm : ∀ (x : ↥(π₁.kFiniteSubspace K_sub)), ‖(π₂.kFiniteSubspace K_sub).subtype (A x)‖ = ‖(π₁.kFiniteSubspace K_sub).subtype x‖), ∀ (g : G) (v : F₁), (A.extendOfIsometry (π₁.kFiniteSubspace K_sub).subtype (π₂.kFiniteSubspace K_sub).subtype h_dense₁ h_dense₂ h_norm) ((π₁.toMonoidHom g) v) = (π₂.toMonoidHom g) ((A.extendOfIsometry (π₁.kFiniteSubspace K_sub).subtype (π₂.kFiniteSubspace K_sub).subtype h_dense₁ h_dense₂ h_norm) v)