def ContinuousRep.IsAdmissible {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [TopologicalSpace V] (π : ContinuousRep G V) (K : Subgroup G) : Prop

theorem ContinuousLinearMap.continuous_symm_of_bijective {V₁ : Type u_1} [AddCommGroup V₁] [Module ℂ V₁] [TopologicalSpace V₁] [IsTopologicalAddGroup V₁] [ContinuousSMul ℂ V₁] {V₂ : Type u_2} [AddCommGroup V₂] [Module ℂ V₂] [TopologicalSpace V₂] [IsTopologicalAddGroup V₂] [ContinuousSMul ℂ V₂] [T2Space V₂] [FiniteDimensional ℂ V₂] (f : V₁ →L[ℂ] V₂) (hf : Function.Bijective ⇑f) : Continuous ⇑(LinearEquiv.ofBijective (↑f) hf).symm

noncomputable def ContinuousLinearMap.continuousLinearEquivOfBijective {V₁ : Type u_1} [AddCommGroup V₁] [Module ℂ V₁] [TopologicalSpace V₁] [IsTopologicalAddGroup V₁] [ContinuousSMul ℂ V₁] {V₂ : Type u_2} [AddCommGroup V₂] [Module ℂ V₂] [TopologicalSpace V₂] [IsTopologicalAddGroup V₂] [ContinuousSMul ℂ V₂] [T2Space V₂] [FiniteDimensional ℂ V₂] (f : V₁ →L[ℂ] V₂) (hf : Function.Bijective ⇑f) : V₁ ≃L[ℂ] V₂

theorem ContinuousLinearMap.continuousLinearEquivOfBijective_apply {V₁ : Type u_1} [AddCommGroup V₁] [Module ℂ V₁] [TopologicalSpace V₁] [IsTopologicalAddGroup V₁] [ContinuousSMul ℂ V₁] {V₂ : Type u_2} [AddCommGroup V₂] [Module ℂ V₂] [TopologicalSpace V₂] [IsTopologicalAddGroup V₂] [ContinuousSMul ℂ V₂] [T2Space V₂] [FiniteDimensional ℂ V₂] (f : V₁ →L[ℂ] V₂) (hf : Function.Bijective ⇑f) (v : V₁) : (f.continuousLinearEquivOfBijective hf) v = f v

theorem ContinuousLinearMap.continuousLinearEquivOfBijective_coe {V₁ : Type u_1} [AddCommGroup V₁] [Module ℂ V₁] [TopologicalSpace V₁] [IsTopologicalAddGroup V₁] [ContinuousSMul ℂ V₁] {V₂ : Type u_2} [AddCommGroup V₂] [Module ℂ V₂] [TopologicalSpace V₂] [IsTopologicalAddGroup V₂] [ContinuousSMul ℂ V₂] [T2Space V₂] [FiniteDimensional ℂ V₂] (f : V₁ →L[ℂ] V₂) (hf : Function.Bijective ⇑f) : ↑(f.continuousLinearEquivOfBijective hf) = f

noncomputable def characterIntegralOperator {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) : F →L[ℂ] F

theorem characterIntegralOperator_fixes_isotypic {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) (v : F) : v ∈ π.IsotypicComponent K σ → (characterIntegralOperator π K σ hirr) v = v

theorem characterIntegralOperator_range_isotypic {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) (v : F) : (characterIntegralOperator π K σ hirr) v ∈ π.IsotypicComponent K σ

theorem characterIntegralOperator_commutes {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) (g : G) (v : F) : (characterIntegralOperator π K σ hirr) ((π.toMonoidHom g) v) = (π.toMonoidHom g) ((characterIntegralOperator π K σ hirr) v)

theorem characterIntegralOperator_annihilates {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) (W' : Submodule ℂ F) (hW' : (π.restrictSubgroup K).IsInvariantSubspace W') : ((π.restrictSubgroup K).subrepresentation W' hW').IsIrreducible → ¬Nonempty (RepEquiv ((π.restrictSubgroup K).subrepresentation W' hW') σ) → ∀ v ∈ W', (characterIntegralOperator π K σ hirr) v = 0

theorem schurProjector_exists_raw {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) : ∃ (P : F →L[ℂ] F), (∀ v ∈ π.IsotypicComponent K σ, P v = v) ∧ (∀ (v : F), P v ∈ π.IsotypicComponent K σ) ∧ (∀ (g : G) (v : F), P ((π.toMonoidHom g) v) = (π.toMonoidHom g) (P v)) ∧ ∀ (W' : Submodule ℂ F) (hW' : (π.restrictSubgroup K).IsInvariantSubspace W'), ((π.restrictSubgroup K).subrepresentation W' hW').IsIrreducible → ¬Nonempty (RepEquiv ((π.restrictSubgroup K).subrepresentation W' hW') σ) → ∀ v ∈ W', P v = 0

noncomputable def schurProjector {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) : F →L[ℂ] F

theorem schurProjector_fixes_isotypic {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) (v : F) : v ∈ π.IsotypicComponent K σ → (schurProjector π K σ hirr) v = v

theorem schurProjector_range_isotypic {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) (v : F) : (schurProjector π K σ hirr) v ∈ π.IsotypicComponent K σ

theorem schurProjector_commutes_action {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) (g : G) (v : F) : (schurProjector π K σ hirr) ((π.toMonoidHom g) v) = (π.toMonoidHom g) ((schurProjector π K σ hirr) v)

theorem schurProjector_annihilates {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) (W' : Submodule ℂ F) (hW' : (π.restrictSubgroup K).IsInvariantSubspace W') : ((π.restrictSubgroup K).subrepresentation W' hW').IsIrreducible → ¬Nonempty (RepEquiv ((π.restrictSubgroup K).subrepresentation W' hW') σ) → ∀ v ∈ W', (schurProjector π K σ hirr) v = 0

theorem schurProjector_exists {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) : ∃ (P : F →L[ℂ] F), (∀ v ∈ π.IsotypicComponent K σ, P v = v) ∧ (∀ (v : F), P v ∈ π.IsotypicComponent K σ) ∧ (∀ (g : G) (v : F), P ((π.toMonoidHom g) v) = (π.toMonoidHom g) (P v)) ∧ ∀ (W' : Submodule ℂ F) (hW' : (π.restrictSubgroup K).IsInvariantSubspace W'), ((π.restrictSubgroup K).subrepresentation W' hW').IsIrreducible → ¬Nonempty (RepEquiv ((π.restrictSubgroup K).subrepresentation W' hW') σ) → ∀ v ∈ W', P v = 0

theorem clm_commuting_preserves_smooth {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) (P : F →L[ℂ] F) (hcomm : ∀ (g : G) (v : F), P ((π.toMonoidHom g) v) = (π.toMonoidHom g) (P v)) (v : F) : v ∈ ContinuousRep.smoothSubspace I π → P v ∈ ContinuousRep.smoothSubspace I π

theorem schurProjector_commutes {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_3} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (_hirr : σ.IsIrreducible) (P : F →L[ℂ] F) (_hP_fix : ∀ v ∈ π.IsotypicComponent K σ, P v = v) (_hP_range : ∀ (v : F), P v ∈ π.IsotypicComponent K σ) (hP_comm : ∀ (g : G) (v : F), P ((π.toMonoidHom g) v) = (π.toMonoidHom g) (P v)) (g : G) (v : F) : P ((π.toMonoidHom g) v) = (π.toMonoidHom g) (P v)

theorem schurProjector_preserves_smooth {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 : Subgroup G) {Wσ : Type u_5} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) (P : F →L[ℂ] F) (hP_fix : ∀ v ∈ π.IsotypicComponent K σ, P v = v) (hP_range : ∀ (v : F), P v ∈ π.IsotypicComponent K σ) (hP_comm : ∀ (g : G) (v : F), P ((π.toMonoidHom g) v) = (π.toMonoidHom g) (P v)) (v : F) : v ∈ ContinuousRep.smoothSubspace I π → P v ∈ ContinuousRep.smoothSubspace I π

theorem isotypicProjection_continuous_and_smooth {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 : Subgroup G) {Wσ : Type u_5} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) : ∃ (P : F →L[ℂ] F), (∀ v ∈ π.IsotypicComponent K σ, P v = v) ∧ (∀ (v : F), P v ∈ π.IsotypicComponent K σ) ∧ ∀ v ∈ ContinuousRep.smoothSubspace I π, P v ∈ ContinuousRep.smoothSubspace I π

theorem smoothSubspace_dense_of_lieGroup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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] [SecondCountableTopology G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (π : ContinuousRep G F) : Dense ↑(ContinuousRep.smoothSubspace I π)

theorem smooth_dirac_approx {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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] [SecondCountableTopology G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (π : ContinuousRep G F) (v : F) : ∃ (vn : ℕ → F), (∀ (n : ℕ), vn n ∈ ContinuousRep.smoothSubspace I π) ∧ Filter.Tendsto vn Filter.atTop (nhds v)

theorem smooth_vectors_dense_in_isotypic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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] [SecondCountableTopology G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_5} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) : ↑(π.IsotypicComponent K σ) ⊆ closure ↑(ContinuousRep.smoothSubspace I π ⊓ π.IsotypicComponent K σ)

theorem isotypic_le_smooth_of_finiteDimensional {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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] [SecondCountableTopology G] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (π : ContinuousRep G F) (K : Subgroup G) {Wσ : Type u_5} [AddCommGroup Wσ] [Module ℂ Wσ] [TopologicalSpace Wσ] (σ : ContinuousRep (↥K) Wσ) (hirr : σ.IsIrreducible) (hfin : FiniteDimensional ℂ ↥(π.IsotypicComponent K σ)) : π.IsotypicComponent K σ ≤ ContinuousRep.smoothSubspace I π

theorem haar_integral_averaging_axiom {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [T2Space K] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] [FiniteDimensional ℂ W] (πW_hom : K →* W →L[ℂ] W) (U : Submodule ℂ W) (hU_inv : ∀ (g : K), ∀ v ∈ U, (πW_hom g) v ∈ U) (p₀ : W →ₗ[ℂ] ↥U) (hp₀ : ∀ (u : ↥U), p₀ ↑u = u) : ∃ (p_lin : W →ₗ[ℂ] ↥U), (∀ (u : ↥U), p_lin ↑u = u) ∧ ∀ (k : K) (v : W), ↑(p_lin ((πW_hom k) v)) = (πW_hom k) ↑(p_lin v)

theorem haar_averaging_retraction_core {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [T2Space K] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] [FiniteDimensional ℂ W] (πW : ContinuousRep K W) (U : Submodule ℂ W) (hU_inv : πW.IsInvariantSubspace U) (p₀ : W →ₗ[ℂ] ↥U) (hp₀ : ∀ (u : ↥U), p₀ ↑u = u) : ∃ (p : W →L[ℂ] ↥U), T1Space ↥U ∧ (∀ (u : ↥U), p ↑u = u) ∧ ∀ (k : K) (v : W), ↑(p ((πW.toMonoidHom k) v)) = (πW.toMonoidHom k) ↑(p v)

theorem haar_averaging_retraction {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [T2Space K] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] [FiniteDimensional ℂ W] (πW : ContinuousRep K W) (U : Submodule ℂ W) (hU_inv : πW.IsInvariantSubspace U) (p₀ : W →ₗ[ℂ] ↥U) (hp₀ : ∀ (u : ↥U), p₀ ↑u = u) : ∃ (p : W →ₗ[ℂ] ↥U), (∀ (u : ↥U), p ↑u = u) ∧ (∀ (k : K) (v : W), ↑(p ((πW.toMonoidHom k) v)) = (πW.toMonoidHom k) ↑(p v)) ∧ IsClosed ↑p.ker

theorem haar_equivariant_retraction_axiom {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [T2Space K] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] [FiniteDimensional ℂ W] (πW : ContinuousRep K W) (U : Submodule ℂ W) (hU_inv : πW.IsInvariantSubspace U) : ∃ (p : W →ₗ[ℂ] ↥U), (∀ (u : ↥U), p ↑u = u) ∧ (∀ (k : K) (v : W), ↑(p ((πW.toMonoidHom k) v)) = (πW.toMonoidHom k) ↑(p v)) ∧ IsClosed ↑p.ker

theorem haar_invariant_complement_axiom {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [T2Space K] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] [FiniteDimensional ℂ W] (πW : ContinuousRep K W) (U : Submodule ℂ W) (hU_inv : πW.IsInvariantSubspace U) : ∃ (Q : Submodule ℂ W), IsCompl U Q ∧ (∀ (k : K), ∀ v ∈ Q, (πW.toMonoidHom k) v ∈ Q) ∧ IsClosed ↑Q

theorem haar_equivariant_idempotent_projection_axiom {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [T2Space K] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] [FiniteDimensional ℂ W] (πW : ContinuousRep K W) (U : Submodule ℂ W) (hU_inv : πW.IsInvariantSubspace U) : ∃ (p : W →ₗ[ℂ] W), p ∘ₗ p = p ∧ p.range = U ∧ (∀ (k : K) (v : W), p ((πW.toMonoidHom k) v) = (πW.toMonoidHom k) (p v)) ∧ IsClosed ↑p.ker

theorem haar_invariant_complement_of_haar {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [T2Space K] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] [FiniteDimensional ℂ W] (πW : ContinuousRep K W) (U : Submodule ℂ W) (hU_inv : πW.IsInvariantSubspace U) : ∃ (Q : Submodule ℂ W), IsCompl U Q ∧ IsClosed ↑Q ∧ ∀ (k : K), ∀ v ∈ Q, (πW.toMonoidHom k) v ∈ Q

theorem haar_equivariant_projection {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [T2Space K] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] [FiniteDimensional ℂ W] (πW : ContinuousRep K W) (U : Submodule ℂ W) (hU_inv : πW.IsInvariantSubspace U) : ∃ (p : W →ₗ[ℂ] ↥U), (∀ (u : ↥U), p ↑u = u) ∧ IsClosed ↑p.ker ∧ ∀ (k : K) (v : W), ↑(p ((πW.toMonoidHom k) v)) = (πW.toMonoidHom k) ↑(p v)

theorem haar_invariant_complement {K : Type u_1} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [T2Space K] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] [FiniteDimensional ℂ W] (πW : ContinuousRep K W) (U : Submodule ℂ W) (hU_inv : πW.IsInvariantSubspace U) : ∃ (Q : Submodule ℂ W), IsCompl U Q ∧ IsClosed ↑Q ∧ ∀ (k : K), ∀ v ∈ Q, (πW.toMonoidHom k) v ∈ Q

theorem haar_equivariant_retraction {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) [CompactSpace ↥K] [T2Space ↥K] (W : Submodule ℂ F) (hW_inv : (π.restrictSubgroup K).IsInvariantSubspace W) [FiniteDimensional ℂ ↥W] (U : Submodule ℂ ↥W) (hU_inv : ((π.restrictSubgroup K).subrepresentation W hW_inv).IsInvariantSubspace U) : ∃ (p : ↥W →ₗ[ℂ] ↥U), (∀ (u : ↥U), p ↑u = u) ∧ IsClosed ↑p.ker ∧ ∀ (k : ↥K) (v : ↥W), ↑(p ((((π.restrictSubgroup K).subrepresentation W hW_inv).toMonoidHom k) v)) = (((π.restrictSubgroup K).subrepresentation W hW_inv).toMonoidHom k) ↑(p v)

theorem compact_group_invariant_complement {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) [CompactSpace ↥K] [T2Space ↥K] (W : Submodule ℂ F) (hW_inv : (π.restrictSubgroup K).IsInvariantSubspace W) [FiniteDimensional ℂ ↥W] (U : Submodule ℂ ↥W) (hU_inv : ((π.restrictSubgroup K).subrepresentation W hW_inv).IsInvariantSubspace U) : ∃ (U' : Submodule ℂ ↥W), IsCompl U U' ∧ ((π.restrictSubgroup K).subrepresentation W hW_inv).IsInvariantSubspace U'

theorem invariant_subspace_map_subtype {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) [CompactSpace ↥K] [T2Space ↥K] (W : Submodule ℂ F) (hW_inv : (π.restrictSubgroup K).IsInvariantSubspace W) [FiniteDimensional ℂ ↥W] (U : Submodule ℂ ↥W) (hU_inv : ((π.restrictSubgroup K).subrepresentation W hW_inv).IsInvariantSubspace U) : (π.restrictSubgroup K).IsInvariantSubspace (Submodule.map W.subtype U)

theorem map_subtype_lt_of_ne_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (W : Submodule R M) (U : Submodule R ↥W) (hU : U ≠ ⊤) : Submodule.map W.subtype U < W

theorem compact_group_maschke_step {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) [CompactSpace ↥K] [T2Space ↥K] (W : Submodule ℂ F) (hW_inv : (π.restrictSubgroup K).IsInvariantSubspace W) [FiniteDimensional ℂ ↥W] (hnirr : ¬((π.restrictSubgroup K).subrepresentation W hW_inv).IsIrreducible) : ∃ (W₁ : Submodule ℂ F) (W₂ : Submodule ℂ F), W₁ < W ∧ W₂ < W ∧ W₁ ⊔ W₂ = W ∧ (π.restrictSubgroup K).IsInvariantSubspace W₁ ∧ (π.restrictSubgroup K).IsInvariantSubspace W₂

theorem compact_group_complete_reducibility_in_submodule {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) [CompactSpace ↥K] [T2Space ↥K] (W : Submodule ℂ F) (hW_inv : (π.restrictSubgroup K).IsInvariantSubspace W) [FiniteDimensional ℂ ↥W] (v : F) (hv : v ∈ W) : ∃ (n : ℕ) (ws : Fin n → F), v = ∑ i : Fin n, ws i ∧ ∀ (i : Fin n), ∃ Wi ≤ W, ws i ∈ Wi ∧ ∃ (hWi : (π.restrictSubgroup K).IsInvariantSubspace Wi), ((π.restrictSubgroup K).subrepresentation Wi hWi).IsIrreducible

theorem kfinite_le_isotypic_sup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) [CompactSpace ↥K] [T2Space ↥K] (v : F) (hv : π.IsKFinite K v) : ∃ (n : ℕ) (ws : Fin n → F), v = ∑ i : Fin n, ws i ∧ ∀ (i : Fin n), ∃ (Wσ : Type uF) (x : AddCommGroup Wσ) (x_1 : Module ℂ Wσ) (x_2 : TopologicalSpace Wσ) (σ : ContinuousRep (↥K) Wσ), σ.IsIrreducible ∧ ws i ∈ π.IsotypicComponent K σ

theorem admissible_kfinite_le_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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] [SecondCountableTopology G] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (π : ContinuousRep G F) (K : Subgroup G) [CompactSpace ↥K] [T2Space ↥K] (hadm : π.IsAdmissible K) : π.kFiniteSubspace K ≤ ContinuousRep.smoothSubspace I π

theorem exercise_5_8_ad_equivariance_axiom {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 : Subgroup G) (lieExp : E → G) : ∃ (Ad : ↥K → E →ₗ[ℝ] E), FiniteDimensional ℝ E ∧ (∀ (k : ↥K) (X : E) (v : F), (π.toMonoidHom ↑k) (π.derivedRep lieExp X v) = π.derivedRep lieExp ((Ad k) X) ((π.toMonoidHom ↑k) v)) ∧ ∀ (v : F) (a : ℝ) (X Y : E), π.derivedRep lieExp (a • X + Y) v = a • π.derivedRep lieExp X v + π.derivedRep lieExp Y v

theorem exercise_5_8_orbit_diff_axiom {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) (lieExp : E → G) (X : E) (u : F) : DifferentiableAt ℝ (fun (t : ℝ) => (π.toMonoidHom (lieExp (t • X))) u) 0

theorem exercise_5_8_core_axiom {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 : Subgroup G) (lieExp : E → G) : ∃ (Ad : ↥K → E →ₗ[ℝ] E), FiniteDimensional ℝ E ∧ (∀ (k : ↥K) (X : E) (v : F), (π.toMonoidHom ↑k) (π.derivedRep lieExp X v) = π.derivedRep lieExp ((Ad k) X) ((π.toMonoidHom ↑k) v)) ∧ (∀ (v : F) (a : ℝ) (X Y : E), π.derivedRep lieExp (a • X + Y) v = a • π.derivedRep lieExp X v + π.derivedRep lieExp Y v) ∧ ∀ (X : E) (u : F), DifferentiableAt ℝ (fun (t : ℝ) => (π.toMonoidHom (lieExp (t • X))) u) 0

theorem exercise_5_8_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] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) (lieExp : E → G) : ∃ (Ad : ↥K → E →ₗ[ℝ] E), FiniteDimensional ℝ E ∧ (∀ (k : ↥K) (X : E) (v : F), (π.toMonoidHom ↑k) (π.derivedRep lieExp X v) = π.derivedRep lieExp ((Ad k) X) ((π.toMonoidHom ↑k) v)) ∧ (∀ (v : F) (a : ℝ) (X Y : E), π.derivedRep lieExp (a • X + Y) v = a • π.derivedRep lieExp X v + π.derivedRep lieExp Y v) ∧ ∀ (X : E) (c : ℂ) (v w : F), π.derivedRep lieExp X (c • v + w) = c • π.derivedRep lieExp X v + π.derivedRep lieExp X w

theorem isKFinite_of_orbit_le_finiteDim {G : Type u_1} [Group G] [TopologicalSpace G] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) (w : F) (W : Submodule ℂ F) [FiniteDimensional ℂ ↥W] (hle : Submodule.span ℂ (Set.range fun (k : ↥K) => (π.toMonoidHom ↑k) w) ≤ W) : π.IsKFinite K w