structure GKModuleIso {𝔤 : 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] {W : Type u_4} [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] (M : GKModule 𝔤 K 𝔨 Ad V) (N : GKModule 𝔤 K 𝔨 Ad W) : Type (max u_3 u_4)

• toLinearEquiv : V ≃ₗ[ℂ] W
• lie_comm (X : 𝔤) (v : V) : self.toLinearEquiv ⁅X, v⁆ = ⁅X, self.toLinearEquiv v⁆
• group_comm (k : K) (v : V) : self.toLinearEquiv ((M.σ k) v) = (N.σ k) (self.toLinearEquiv v)

def InfinitesimallyEquivalent {𝔤 : 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₁] {V₂ : Type u_4} [AddCommGroup V₂] [Module ℂ V₂] [LieRingModule 𝔤 V₂] [LieModule ℂ 𝔤 V₂] (M₁ : GKModule 𝔤 K 𝔨 Ad V₁) (M₂ : GKModule 𝔤 K 𝔨 Ad V₂) : Prop

structure GKModule.IsUnitary {𝔤 : 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) : Type u_3

• form : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ
• conj_symm (v w : V) : (self.form w) v = (starRingEnd ℂ) ((self.form v) w)
• re_nonneg (v : V) : 0 ≤ ((self.form v) v).re
• definite (v : V) : (self.form v) v = 0 → v = 0
• pos_def (v : V) : v ≠ 0 → 0 < ((self.form v) v).re
• K_invariant (k : K) (v w : V) : (self.form ((M.σ k) v)) ((M.σ k) w) = (self.form v) w
• lie_invariant (X : 𝔤) (v w : V) : (self.form ⁅X, v⁆) w + (self.form v) ⁅X, w⁆ = 0

def GKModule.IsUnitary.mk' {𝔤 : 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) (form : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ) (conj_symm : ∀ (v w : V), (form w) v = (starRingEnd ℂ) ((form v) w)) (pos_def : ∀ (v : V), v ≠ 0 → 0 < ((form v) v).re) (K_invariant : ∀ (k : K) (v w : V), (form ((M.σ k) v)) ((M.σ k) w) = (form v) w) (lie_invariant : ∀ (X : 𝔤) (v w : V), (form ⁅X, v⁆) w + (form v) ⁅X, w⁆ = 0) : M.IsUnitary

noncomputable def GKModule.IsUnitary.toInnerProductSpaceCore {𝔤 : 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} (hu : M.IsUnitary) : InnerProductSpace.Core ℂ V

structure Globalization (G : Type u_1) [Group G] [TopologicalSpace G] {K : Type u_2} [Group K] (K_sub : K →* G) {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_4} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) : Type (max (max (max u_1 u_3) u_4) (u_5 + 1))

• Ŵ : Type u_5
• instNACG : NormedAddCommGroup self.Ŵ
• instIPS : InnerProductSpace ℂ self.Ŵ
• instCS : CompleteSpace self.Ŵ
• π : ContinuousRep G self.Ŵ
• isUnitary : self.π.IsUnitary
• isIrreducible : self.π.IsIrreducible
• ι : V →ₗ[ℂ] self.Ŵ
• ι_injective : Function.Injective ⇑self.ι
• K_compat (k : K) (v : V) : self.ι ((M.σ k) v) = (self.π.toMonoidHom (K_sub k)) (self.ι v)
• lie_action_Ŵ : 𝔤 → self.Ŵ → self.Ŵ
• lie_compat_ι (X : 𝔤) (v : V) : self.ι ⁅X, v⁆ = self.lie_action_Ŵ X (self.ι v)
• kfin_image : Set.range ⇑self.ι = ↑(self.π.kFiniteSubspace K_sub.range)

noncomputable def hilbertCompletionBundle {𝔤 : 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) (_hunit : M.IsUnitary) : (W : Type u_4) ×' (nacg : NormedAddCommGroup W) ×' (ips : InnerProductSpace ℂ W) ×' (_ : CompleteSpace W) ×' (emb : V →ₗ[ℂ] W) ×' Function.Injective ⇑emb

noncomputable def hilbertCompletionType {𝔤 : 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) (hunit : M.IsUnitary) : Type u_4

@[reducible]

noncomputable def hilbertCompletion_instNACG {𝔤 : 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) (hunit : M.IsUnitary) : NormedAddCommGroup (hilbertCompletionType M hunit)

@[reducible]

noncomputable def hilbertCompletion_instIPS {𝔤 : 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) (hunit : M.IsUnitary) : InnerProductSpace ℂ (hilbertCompletionType M hunit)

@[reducible]

noncomputable def hilbertCompletion_instCS {𝔤 : 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) (hunit : M.IsUnitary) : CompleteSpace (hilbertCompletionType M hunit)

noncomputable def hilbertCompletion_embedding {𝔤 : 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) (hunit : M.IsUnitary) : V →ₗ[ℂ] hilbertCompletionType M hunit

theorem hilbertCompletionRepBundle_axiom (G : Type u_1) [Group G] [TopologicalSpace G] {K : Type u_2} [Group K] (K_sub : K →* G) {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_4} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hunit : M.IsUnitary) : Nonempty (Globalization G K_sub M)

theorem globalization_rep_admissible_axiom {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Type u_2} [Group K] {K_sub : K →* G} {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_4} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] {M : GKModule 𝔤 K 𝔨 Ad V} (G_glob : Globalization G K_sub M) (hirr : M.IsIrreducibleGKModule) (hunit : M.IsUnitary) : G_glob.π.IsAdmissible K_sub.range

theorem gk_morphism_norm_bound_axiom {G : Type u_1} [Group G] [TopologicalSpace G] {K : Type u_2} [Group K] {K_sub : K →* G} [CompactSpace ↥K_sub.range] {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V₁ : Type u_4} [AddCommGroup V₁] [Module ℂ V₁] [LieRingModule 𝔤 V₁] [LieModule ℂ 𝔤 V₁] {V₂ : Type u_5} [AddCommGroup V₂] [Module ℂ V₂] [LieRingModule 𝔤 V₂] [LieModule ℂ 𝔤 V₂] (M₁ : GKModule 𝔤 K 𝔨 Ad V₁) (M₂ : GKModule 𝔤 K 𝔨 Ad V₂) (G₁ : Globalization G K_sub M₁) (G₂ : Globalization G K_sub M₂) (φ : GKModuleHom M₁ M₂) : ∃ (C : ℝ), ∀ (v : V₁), ‖G₂.ι (φ.toLinearMap v)‖ ≤ C * ‖G₁.ι v‖

theorem gk_morphism_extension_equivariant_axiom {G : Type u_1} [Group G] [TopologicalSpace G] {K : Type u_2} [Group K] {K_sub : K →* G} [CompactSpace ↥K_sub.range] {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V₁ : Type u_4} [AddCommGroup V₁] [Module ℂ V₁] [LieRingModule 𝔤 V₁] [LieModule ℂ 𝔤 V₁] {V₂ : Type u_5} [AddCommGroup V₂] [Module ℂ V₂] [LieRingModule 𝔤 V₂] [LieModule ℂ 𝔤 V₂] (M₁ : GKModule 𝔤 K 𝔨 Ad V₁) (M₂ : GKModule 𝔤 K 𝔨 Ad V₂) (G₁ : Globalization G K_sub M₁) (G₂ : Globalization G K_sub M₂) (φ : GKModuleHom M₁ M₂) (T : G₁.Ŵ → G₂.Ŵ) (hT_cont : Continuous T) (hT_ext : ∀ (v : V₁), T (G₁.ι v) = G₂.ι (φ.toLinearMap v)) (g : G) (w : G₁.Ŵ) : T ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T w)

theorem harish_chandra_globalization_exists {G : Type u_1} [Group G] [TopologicalSpace G] {K : Type u_2} [Group K] {K_sub : K →* G} {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_4} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hunit : M.IsUnitary) : Nonempty (Globalization G K_sub M)

theorem harish_chandra_globalization_admissible {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Type u_2} [Group K] {K_sub : K →* G} {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_4} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) (hirr : M.IsIrreducibleGKModule) (hunit : M.IsUnitary) (G_glob : Globalization G K_sub M) : G_glob.π.IsAdmissible K_sub.range

theorem Globalization.ι_denseRange {G : Type u_1} [Group G] [TopologicalSpace G] {K : Type u_2} [Group K] {K_sub : K →* G} [CompactSpace ↥K_sub.range] {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_4} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) (G_glob : Globalization G K_sub M) : DenseRange ⇑G_glob.ι

theorem globalization_hom_extension {G : Type u_1} [Group G] [TopologicalSpace G] {K : Type u_2} [Group K] {K_sub : K →* G} [CompactSpace ↥K_sub.range] {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V₁ : Type u_4} [AddCommGroup V₁] [Module ℂ V₁] [LieRingModule 𝔤 V₁] [LieModule ℂ 𝔤 V₁] {V₂ : Type u_5} [AddCommGroup V₂] [Module ℂ V₂] [LieRingModule 𝔤 V₂] [LieModule ℂ 𝔤 V₂] (M₁ : GKModule 𝔤 K 𝔨 Ad V₁) (M₂ : GKModule 𝔤 K 𝔨 Ad V₂) (G₁ : Globalization G K_sub M₁) (G₂ : Globalization G K_sub M₂) (φ : GKModuleHom M₁ M₂) : ∃ (T : G₁.Ŵ → G₂.Ŵ), Continuous T ∧ (∀ (g : G) (w : G₁.Ŵ), T ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T w)) ∧ ∀ (v : V₁), T (G₁.ι v) = G₂.ι (φ.toLinearMap v)

theorem harish_chandra_globalization_unique {G : Type u_1} [Group G] [TopologicalSpace G] {K : Type u_2} [Group K] {K_sub : K →* G} [CompactSpace ↥K_sub.range] {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_4} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) (_hirr : M.IsIrreducibleGKModule) (_hunit : M.IsUnitary) (G₁ : Globalization G K_sub M) (G₂ : Globalization G K_sub M) : ∃ (U : G₁.Ŵ → G₂.Ŵ), Function.Bijective U ∧ (∀ (g : G) (w : G₁.Ŵ), U ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (U w)) ∧ ∀ (v : V), U (G₁.ι v) = G₂.ι v