opaque principalSymbolOn (N : ℕ) (D : (EuclideanSpace ℝ (Fin N) → ℝ) →ₗ[ℝ] EuclideanSpace ℝ (Fin N) → ℝ) : EuclideanSpace ℝ (Fin N) → EuclideanSpace ℝ (Fin N) → ℝ

def IsEllipticOnOpen (N : ℕ) (D : (EuclideanSpace ℝ (Fin N) → ℝ) →ₗ[ℝ] EuclideanSpace ℝ (Fin N) → ℝ) (U : Set (EuclideanSpace ℝ (Fin N))) : Prop

opaque HasAnalyticCoefficientsOn (N : ℕ) (D : (EuclideanSpace ℝ (Fin N) → ℝ) →ₗ[ℝ] EuclideanSpace ℝ (Fin N) → ℝ) (U : Set (EuclideanSpace ℝ (Fin N))) : Prop

theorem elliptic_regularity {N : ℕ} (U : Set (EuclideanSpace ℝ (Fin N))) (hU : IsOpen U) (D : (EuclideanSpace ℝ (Fin N) → ℝ) →ₗ[ℝ] EuclideanSpace ℝ (Fin N) → ℝ) (helliptic : IsEllipticOnOpen N D U) (hanalytic_coeff : HasAnalyticCoefficientsOn N D U) (f : EuclideanSpace ℝ (Fin N) → ℝ) (hsmooth : ContDiffOn ℝ (↑⊤) f U) (hsol : ∀ x ∈ U, D f x = 0) : AnalyticOnNhd ℝ f U

opaque principalSymbolManifold {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] (D : (X → ℝ) →ₗ[ℝ] X → ℝ) : X → E → ℝ

def IsEllipticAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] (D : (X → ℝ) →ₗ[ℝ] X → ℝ) (x : X) : Prop

def IsEllipticOnManifold {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] (D : (X → ℝ) →ₗ[ℝ] X → ℝ) : Prop

opaque HasLocallyAnalyticCoeffs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] (D : (X → ℝ) →ₗ[ℝ] X → ℝ) : Prop

def IsEllipticWithAnalyticCoeffs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] (D : (X → ℝ) →ₗ[ℝ] X → ℝ) : Prop

theorem elliptic_regularity_manifold {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] (D : (X → ℝ) →ₗ[ℝ] X → ℝ) (hD : IsEllipticWithAnalyticCoeffs I D) (f : X → ℝ) (hsmooth : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hsol : ∀ (x : X), D f x = 0) (x : X) : ∃ s ∈ nhds (↑I (↑(chartAt H x) x)), AnalyticOnNhd ℝ (f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) s

def ContinuousRep.IsWeaklyAnalyticVector {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] {F : Type uFsec} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (v : F) : Prop

def ContinuousRep.weaklyAnalyticSet {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] {F : Type uFsec} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) : Set F

structure ContinuousRep.SemisimpleLieGroupData {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (G : Type u_6) [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] : Type (max (uLie + 1) u_6)

• lieAlg : Type uLie
• instLieRing : LieRing self.lieAlg
• instLieAlgebra : LieAlgebra ℝ self.lieAlg
• lieExp : self.lieAlg → G
• isSemisimple : LieAlgebra.IsSemisimple ℝ self.lieAlg
• connected : ConnectedSpace G
• t2 : T2Space G

structure ContinuousRep.IsSemisimpleLieGroup {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (G : Type u_6) [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] : Prop

• connected : ConnectedSpace G
• t2 : T2Space G
• exists_lieAlg : ∃ (𝔤 : Type uLie) (x : LieRing 𝔤) (instLA : LieAlgebra ℝ 𝔤) (exp : 𝔤 → G), LieAlgebra.IsSemisimple ℝ 𝔤

theorem ContinuousRep.casimir_exists_nonzero_kEquivariant {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_6} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℂ F] [Nontrivial F] (π : ContinuousRep G F) (K : Subgroup G) (_hG_ss : IsSemisimpleLieGroup I G) [CompactSpace ↥K] (_hK_max : IsMaximalCompactSubgroup K) : ∃ (b : F →ₗ[ℂ] F), b ≠ 0 ∧ (∀ (k : ↥K) (w : F), b ((π.toMonoidHom ↑k) w) = (π.toMonoidHom ↑k) (b w)) ∧ ∀ v ∈ π.kFiniteSubspace K, b v ∈ Submodule.span ℂ (Set.range fun (k : ↥K) => (π.toMonoidHom ↑k) v)

theorem ContinuousRep.kEquivariant_preserves_kOrbitSpan {G : Type u_4} [Group G] [TopologicalSpace G] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) [CompactSpace ↥K] (b : F →ₗ[ℂ] F) (hb_comm : ∀ (k : ↥K) (w : F), b ((π.toMonoidHom ↑k) w) = (π.toMonoidHom ↑k) (b w)) (v : F) (hbv : b v ∈ Submodule.span ℂ (Set.range fun (k : ↥K) => (π.toMonoidHom ↑k) v)) (w : F) : w ∈ Submodule.span ℂ (Set.range fun (k : ↥K) => (π.toMonoidHom ↑k) v) → b w ∈ Submodule.span ℂ (Set.range fun (k : ↥K) => (π.toMonoidHom ↑k) v)

theorem ContinuousRep.casimir_exists_nonzero_kInvariant_aux {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_6} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℂ F] [Nontrivial F] (π : ContinuousRep G F) (K : Subgroup G) (hG_ss : IsSemisimpleLieGroup I G) [CompactSpace ↥K] (hK_max : IsMaximalCompactSubgroup K) : ∃ (b : F →ₗ[ℂ] F), b ≠ 0 ∧ (∀ (k : ↥K) (w : F), b ((π.toMonoidHom ↑k) w) = (π.toMonoidHom ↑k) (b w)) ∧ ∀ v ∈ π.kFiniteSubspace K, ∀ w ∈ Submodule.span ℂ (Set.range fun (k : ↥K) => (π.toMonoidHom ↑k) v), b w ∈ Submodule.span ℂ (Set.range fun (k : ↥K) => (π.toMonoidHom ↑k) v)

theorem ContinuousRep.exists_kInvariant_laplacian_endomorphism {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_6} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℂ F] [Nontrivial F] (π : ContinuousRep G F) (K : Subgroup G) (hG_ss : IsSemisimpleLieGroup I G) [CompactSpace ↥K] (hK_max : IsMaximalCompactSubgroup K) (v : F) (hv : v ∈ π.kFiniteSubspace K) : ∃ (b : F →ₗ[ℂ] F), b ≠ 0 ∧ ∀ w ∈ Submodule.span ℂ (Set.range fun (k : ↥K) => (π.toMonoidHom ↑k) v), b w ∈ Submodule.span ℂ (Set.range fun (k : ↥K) => (π.toMonoidHom ↑k) v)

theorem ContinuousRep.orbit_map_smooth_of_kfinite {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_6} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] [SecondCountableTopology G] {F : Type uFsec} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (π : ContinuousRep G F) (K : Subgroup G) [CompactSpace ↥K] [T2Space ↥K] (hadm : π.IsAdmissible K) (v : F) (hv : v ∈ π.kFiniteSubspace K) : ContMDiff I (modelWithCornersSelf ℝ F) (↑⊤) (π.orbitMap v)

theorem ContinuousRep.matrix_coeff_smooth_kfinite {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_6} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] [SecondCountableTopology G] {F : Type uFsec} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (π : ContinuousRep G F) (K : Subgroup G) [CompactSpace ↥K] [T2Space ↥K] (hadm : π.IsAdmissible K) (v : F) (hv : v ∈ π.kFiniteSubspace K) (h : F →L[ℂ] ℂ) : ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ fun (g : G) => (h ((π.toMonoidHom g) v)).re

theorem ContinuousRep.laplacian_polynomial_elliptic_analytic_sorry {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_6} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] (K : Subgroup G) (hG_ss : IsSemisimpleLieGroup I G) [CompactSpace ↥K] (hK_max : IsMaximalCompactSubgroup K) {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (b : F →ₗ[ℂ] F) (P : Polynomial ℂ) (hP : P ≠ 0) : ∃ (D : (G → ℝ) →ₗ[ℝ] G → ℝ), IsEllipticWithAnalyticCoeffs I D ∧ ∀ (v : F) (h : F →L[ℂ] ℂ) (x : G), D (fun (g : G) => (h ((π.toMonoidHom g) v)).re) x = (h ((π.toMonoidHom x) (((Polynomial.aeval b) P) v))).re

theorem ContinuousRep.polynomial_in_laplacian_elliptic_analytic_aux {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_6} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] (K : Subgroup G) (hG_ss : IsSemisimpleLieGroup I G) [CompactSpace ↥K] (hK_max : IsMaximalCompactSubgroup K) {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (b : F →ₗ[ℂ] F) (P : Polynomial ℂ) (hP : P ≠ 0) : ∃ (D : (G → ℝ) →ₗ[ℝ] G → ℝ), IsEllipticWithAnalyticCoeffs I D ∧ ∀ (v : F) (h : F →L[ℂ] ℂ) (x : G), D (fun (g : G) => (h ((π.toMonoidHom g) v)).re) x = (h ((π.toMonoidHom x) (((Polynomial.aeval b) P) v))).re

theorem ContinuousRep.laplacian_polynomial_is_elliptic_with_analytic_coeffs {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_6} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) (hG_ss : IsSemisimpleLieGroup I G) [CompactSpace ↥K] (hK_max : IsMaximalCompactSubgroup K) (b : F →ₗ[ℂ] F) (P : Polynomial ℂ) (hP : P ≠ 0) : ∃ (D : (G → ℝ) →ₗ[ℝ] G → ℝ), IsEllipticWithAnalyticCoeffs I D ∧ ∀ (v : F) (h : F →L[ℂ] ℂ) (x : G), D (fun (g : G) => (h ((π.toMonoidHom g) v)).re) x = (h ((π.toMonoidHom x) (((Polynomial.aeval b) P) v))).re

theorem ContinuousRep.laplacian_annihilates_matrix_coeff {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_6} [Group G] [TopologicalSpace G] [ChartedSpace H G] [LieGroup I ⊤ G] [IsTopologicalGroup G] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℂ F] (π : ContinuousRep G F) (K : Subgroup G) (_hG_ss : IsSemisimpleLieGroup I G) [CompactSpace ↥K] (_hK_max : IsMaximalCompactSubgroup K) (b : F →ₗ[ℂ] F) (v : F) (h : F →L[ℂ] ℂ) (P : Polynomial ℂ) (hPv : ((Polynomial.aeval b) P) v = 0) (D : (G → ℝ) →ₗ[ℝ] G → ℝ) (hD_compat : ∀ (v : F) (h : F →L[ℂ] ℂ) (x : G), D (fun (g : G) => (h ((π.toMonoidHom g) v)).re) x = (h ((π.toMonoidHom x) (((Polynomial.aeval b) P) v))).re) (x : G) : D (fun (g : G) => (h ((π.toMonoidHom g) v)).re) x = 0

noncomputable def ContinuousRep.restrictEndomorphism {F : Type uFsec} [NormedAddCommGroup F] [NormedSpace ℂ F] (b : F →ₗ[ℂ] F) (W : Submodule ℂ F) (hb : ∀ w ∈ W, b w ∈ W) : ↥W →ₗ[ℂ] ↥W

theorem ContinuousRep.restrictEndomorphism_pow_coe {F : Type uFsec} [NormedAddCommGroup F] [NormedSpace ℂ F] (b : F →ₗ[ℂ] F) (W : Submodule ℂ F) (hb : ∀ w ∈ W, b w ∈ W) (n : ℕ) (w : ↥W) : ↑((restrictEndomorphism b W hb ^ n) w) = (b ^ n) ↑w

theorem ContinuousRep.aeval_restrictEndomorphism_coe {F : Type uFsec} [NormedAddCommGroup F] [NormedSpace ℂ F] (b : F →ₗ[ℂ] F) (W : Submodule ℂ F) (hb : ∀ w ∈ W, b w ∈ W) (P : Polynomial ℂ) (w : ↥W) : ↑(((Polynomial.aeval (restrictEndomorphism b W hb)) P) w) = ((Polynomial.aeval b) P) ↑w

theorem ContinuousRep.cayley_hamilton_annihilation {F : Type uFsec} [NormedAddCommGroup F] [NormedSpace ℂ F] (b : F →ₗ[ℂ] F) (W : Submodule ℂ F) [FiniteDimensional ℂ ↥W] (hb : ∀ w ∈ W, b w ∈ W) (v : F) (hv : v ∈ W) : ∃ (P : Polynomial ℂ), P ≠ 0 ∧ ((Polynomial.aeval b) P) v = 0

theorem ContinuousRep.exists_elliptic_annihilating_matrix_coeff {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] {F : Type uFsec} [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [SecondCountableTopology G] [CompleteSpace F] [IsTopologicalGroup G] [Nontrivial F] (π : ContinuousRep G F) (K : Subgroup G) (hG_ss : IsSemisimpleLieGroup I G) [CompactSpace ↥K] [T2Space ↥K] (hK_max : IsMaximalCompactSubgroup K) (hadm : π.IsAdmissible K) (v : F) (hv : v ∈ π.kFiniteSubspace K) (h : F →L[ℂ] ℂ) : ∃ (D : (G → ℝ) →ₗ[ℝ] G → ℝ), IsEllipticWithAnalyticCoeffs I D ∧ (ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ fun (g : G) => (h ((π.toMonoidHom g) v)).re) ∧ ∀ (x : G), D (fun (g : G) => (h ((π.toMonoidHom g) v)).re) x = 0

theorem ContinuousRep.harish_chandra_analyticity {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] {F : Type uFsec} [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [SecondCountableTopology G] [CompleteSpace F] [IsTopologicalGroup G] (π : ContinuousRep G F) (K : Subgroup G) (hG_ss : IsSemisimpleLieGroup I G) [CompactSpace ↥K] [T2Space ↥K] (hK_max : IsMaximalCompactSubgroup K) (hadm : π.IsAdmissible K) (v : F) (hv : v ∈ π.kFiniteSubspace K) : IsWeaklyAnalyticVector I π v

theorem ContinuousRep.theorem_6_3_harish_chandra_analyticity {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] {F : Type uFsec} [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [SecondCountableTopology G] [CompleteSpace F] [IsTopologicalGroup G] (π : ContinuousRep G F) (K : Subgroup G) (hG_ss : IsSemisimpleLieGroup I G) [CompactSpace ↥K] [T2Space ↥K] (hK_max : IsMaximalCompactSubgroup K) (hadm : π.IsAdmissible K) (v : F) (hv : v ∈ π.kFiniteSubspace K) : IsWeaklyAnalyticVector I π v