noncomputable def qInteger (d : ℕ) : PowerSeries ℤ

noncomputable def groupRingExp {P' : Type u_3} (α : P') : AddMonoidAlgebra ℤ P'

noncomputable def groupRingOneMinusExp {P' : Type u_3} [AddCommGroup P'] (α : P') : AddMonoidAlgebra ℤ P'

noncomputable def numeratorProd {P' : Type u_3} [AddCommGroup P'] (S : Finset P') : AddMonoidAlgebra ℤ P'

def groupRingCT {P' : Type u_3} [AddCommGroup P'] (f : AddMonoidAlgebra ℤ P') : ℤ

noncomputable def singleFactorCoeff {P' : Type u_3} [AddCommGroup P'] (α : P') (n : ℕ) : AddMonoidAlgebra ℤ P'

noncomputable def singleFactorPS {P' : Type u_3} [AddCommGroup P'] (α : P') : PowerSeries (AddMonoidAlgebra ℤ P')

noncomputable def fullProductPS {P' : Type u_3} [AddCommGroup P'] (S : Finset P') : PowerSeries (AddMonoidAlgebra ℤ P')

noncomputable def geomFactorCoeff {P' : Type u_3} [AddCommGroup P'] (α : P') (n : ℕ) : AddMonoidAlgebra ℤ P'

noncomputable def geomFactorPS {P' : Type u_3} [AddCommGroup P'] (α : P') : PowerSeries (AddMonoidAlgebra ℤ P')

noncomputable def geomProductPS {P' : Type u_3} [AddCommGroup P'] (S : Finset P') : PowerSeries (AddMonoidAlgebra ℤ P')

noncomputable def powerSeriesCT {P' : Type u_3} [AddCommGroup P'] (f : PowerSeries (AddMonoidAlgebra ℤ P')) : PowerSeries ℤ

noncomputable def concreteCT_fullRoots {P' : Type u_3} [AddCommGroup P'] (roots : Finset P') : PowerSeries ℤ

noncomputable def concreteCT_posRoots {P' : Type u_3} [AddCommGroup P'] (roots posRoots : Finset P') : PowerSeries ℤ

noncomputable def concreteCT_fullRoots_char {P' : Type u_3} [AddCommGroup P'] (roots : Finset P') (chi : AddMonoidAlgebra ℤ P') : PowerSeries ℤ

noncomputable def concreteCT_posRoots_lambda {P' : Type u_3} [AddCommGroup P'] (roots posRoots : Finset P') (wt : P') : PowerSeries ℤ

noncomputable def qIntegerProd (r : ℕ) (degrees : Fin r → ℕ) : PowerSeries ℤ

def gradedHilbertSeries (dimFun : ℕ → ℕ) : PowerSeries ℤ

structure KostantSetupData {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] : Type (max (max (max u_1 u_2) (u_4 + 1)) (u_5 + 1))

• cartanSubalgebra : LieSubalgebra R 𝔤
• instCartan : self.cartanSubalgebra.IsCartanSubalgebra
• instLieRingModuleSg : LieRingModule 𝔤 (SymmetricAlgebra R 𝔤)
• instLieModuleSg : LieModule R 𝔤 (SymmetricAlgebra R 𝔤)
• invariantSubalgebra : Subalgebra R (SymmetricAlgebra R 𝔤)
• invariantSubalgebra_eq (x : SymmetricAlgebra R 𝔤) : x ∈ self.invariantSubalgebra ↔ x ∈ LieModule.maxTrivSubmodule R 𝔤 (SymmetricAlgebra R 𝔤)
• harmonicSubspace : Submodule R (SymmetricAlgebra R 𝔤)
• instFreeHarmonic : Module.Free R ↥self.harmonicSubspace
• harmonicSubspaceUEA : Submodule R (UniversalEnvelopingAlgebra R 𝔤)
• pbwHarmonicEquiv : ↥self.harmonicSubspace ≃ₗ[R] ↥self.harmonicSubspaceUEA
• pbwSymmEquiv : SymmetricAlgebra R 𝔤 ≃ₗ[R] UniversalEnvelopingAlgebra R 𝔤
• pbwInvariantToCenter : ↥self.invariantSubalgebra ≃ₐ[R] ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))
• pbwSymmCompat (a : ↥self.invariantSubalgebra) (h : ↥self.harmonicSubspace) : self.pbwSymmEquiv (↑a * ↑h) = ↑(self.pbwInvariantToCenter a) * ↑(self.pbwHarmonicEquiv h)
• W : Type u_4
• instGroup : Group self.W
• instFintype : Fintype self.W
• rank : ℕ
• degrees : Fin self.rank → ℕ
• P : Type u_5
• instAddCommGroup_P : AddCommGroup self.P
• instDecEq_P : DecidableEq self.P
• roots : Finset self.P
• posRoots : Finset self.P
• posRoots_sub_roots : self.posRoots ⊆ self.roots
• dominantWeights : Set self.P
• simpleCoroots : Fin self.rank → self.P
• pairingCoroot : self.P → Fin self.rank → ℤ
• dominantWeights_spec : self.dominantWeights = {μ : self.P | ∀ (i : Fin self.rank), 0 ≤ self.pairingCoroot μ i}
• pairingCoroot_zero (i : Fin self.rank) : self.pairingCoroot 0 i = 0
• rho : self.P
• signRep : self.W → ℤ
• actionW : self.W → self.P → self.P
• weylCharacter : self.P → AddMonoidAlgebra ℤ self.P
• gradedHomDim : self.P → ℕ → ℕ
• equation12_geom_form_field (wt : self.P) : wt ∈ self.dominantWeights → ↑(Fintype.card self.W) • gradedHilbertSeries (self.gradedHomDim wt) = (∏ i : Fin self.rank, qInteger (self.degrees i)) * powerSeriesCT (geomProductPS self.roots * PowerSeries.C (numeratorProd self.roots * self.weylCharacter wt))
• cst_equiv : TensorProduct R ↥self.invariantSubalgebra ↥self.harmonicSubspace ≃ₗ[R] SymmetricAlgebra R 𝔤
• cst_equiv_apply_tmul (a : ↥self.invariantSubalgebra) (h : ↥self.harmonicSubspace) : self.cst_equiv (a ⊗ₜ[R] h) = ↑a * ↑h
• invariantPolynomial : ↥self.invariantSubalgebra ≃ₐ[R] MvPolynomial (Fin self.rank) R

theorem KostantSetupData.zero_mem_dominantWeights {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : 0 ∈ ksd.dominantWeights

theorem KostantSetupData.weylCharacter_CT {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) : wt ∈ ksd.dominantWeights → ∀ (f : AddMonoidAlgebra ℤ ksd.P), groupRingCT (numeratorProd ksd.roots * ksd.weylCharacter wt * f) = ↑(Fintype.card ksd.W) * groupRingCT (groupRingExp wt * numeratorProd ksd.posRoots * f)

theorem KostantSetupData.weylCharacter_zero_eq {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : ksd.weylCharacter 0 = Finsupp.single 0 1

theorem KostantSetupData.weylCharacterFormula {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) : wt ∈ ksd.dominantWeights → numeratorProd ksd.posRoots * ksd.weylCharacter wt = ∑ w : ksd.W, ksd.signRep w • Finsupp.single (ksd.actionW w (wt + ksd.rho) - ksd.rho) 1

theorem KostantSetupData.gradedHomDim_zero_spec {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (n : ℕ) : ksd.gradedHomDim 0 n = if n = 0 then 1 else 0

theorem singleFactorCoeff_eq_mul {P' : Type u_3} [AddCommGroup P'] (α : P') (n : ℕ) : singleFactorCoeff α n = groupRingOneMinusExp α * geomFactorCoeff α n

theorem singleFactorPS_eq {P' : Type u_3} [AddCommGroup P'] (α : P') : singleFactorPS α = PowerSeries.C (groupRingOneMinusExp α) * geomFactorPS α

theorem fullProductPS_eq_C_numeratorProd_mul_geomProductPS {P' : Type u_3} [AddCommGroup P'] (S : Finset P') : fullProductPS S = PowerSeries.C (numeratorProd S) * geomProductPS S

theorem KostantSetupData.equation12_geom_form {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) : wt ∈ ksd.dominantWeights → ↑(Fintype.card ksd.W) • gradedHilbertSeries (ksd.gradedHomDim wt) = (∏ i : Fin ksd.rank, qInteger (ksd.degrees i)) * powerSeriesCT (geomProductPS ksd.roots * PowerSeries.C (numeratorProd ksd.roots * ksd.weylCharacter wt))

theorem KostantSetupData.equation12_spec {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) : wt ∈ ksd.dominantWeights → ↑(Fintype.card ksd.W) • gradedHilbertSeries (ksd.gradedHomDim wt) = (∏ i : Fin ksd.rank, qInteger (ksd.degrees i)) * concreteCT_fullRoots_char ksd.roots (ksd.weylCharacter wt)

theorem KostantSetupData.gradedHomDim_zero {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (n : ℕ) : ksd.gradedHomDim 0 n = if n = 0 then 1 else 0

theorem KostantSetupData.equation12_hilbert_series {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) : wt ∈ ksd.dominantWeights → ↑(Fintype.card ksd.W) • gradedHilbertSeries (ksd.gradedHomDim wt) = (∏ i : Fin ksd.rank, qInteger (ksd.degrees i)) * concreteCT_fullRoots_char ksd.roots (ksd.weylCharacter wt)

def KostantSetupData.isDominant {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (μ : ksd.P) : Prop

theorem KostantSetupData.isDominant_iff_mem_dominantWeights {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (μ : ksd.P) : ksd.isDominant μ ↔ μ ∈ ksd.dominantWeights

def KostantSetupData.dotAction {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (w : ksd.W) (μ : ksd.P) : ksd.P

theorem KostantSetupData.gradedHomDim_trivial {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (n : ℕ) : ksd.gradedHomDim 0 n = if n = 0 then 1 else 0

noncomputable def KostantSetupData.hilbertSeriesHomDual {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) : PowerSeries ℤ

def KostantSetupData.actualHilbertSeriesHom {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) : PowerSeries ℤ

theorem singleFactorPS_eq_mul {P' : Type u_3} [AddCommGroup P'] (α : P') : singleFactorPS α = PowerSeries.C (groupRingOneMinusExp α) * geomFactorPS α

theorem fullProductPS_eq_numerator_mul_geom {P' : Type u_3} [DecidableEq P'] [AddCommGroup P'] (S : Finset P') : fullProductPS S = PowerSeries.C (numeratorProd S) * geomProductPS S

theorem weylCharacter_numerator_CT_groupRing {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) (hwt : wt ∈ ksd.dominantWeights) (f : AddMonoidAlgebra ℤ ksd.P) : groupRingCT (numeratorProd ksd.roots * ksd.weylCharacter wt * f) = ↑(Fintype.card ksd.W) * groupRingCT (groupRingExp wt * numeratorProd ksd.posRoots * f)

theorem weylCharacter_numerator_CT_eq {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) (hwt : wt ∈ ksd.dominantWeights) : powerSeriesCT (PowerSeries.C (numeratorProd ksd.roots * ksd.weylCharacter wt) * geomProductPS ksd.roots) = ↑(Fintype.card ksd.W) • powerSeriesCT (PowerSeries.C (groupRingExp wt * numeratorProd ksd.posRoots) * geomProductPS ksd.roots)

theorem kostant_weylCharacter_CT_eq {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) (hwt : wt ∈ ksd.dominantWeights) : ↑(Fintype.card ksd.W) • concreteCT_posRoots_lambda ksd.roots ksd.posRoots wt = concreteCT_fullRoots_char ksd.roots (ksd.weylCharacter wt)

theorem kostant_hilbert_series_core {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) (hwt : wt ∈ ksd.dominantWeights) : gradedHilbertSeries (ksd.gradedHomDim wt) = (∏ i : Fin ksd.rank, qInteger (ksd.degrees i)) * concreteCT_posRoots_lambda ksd.roots ksd.posRoots wt

theorem kostant_hilbert_series_genuine {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) (hwt : wt ∈ ksd.dominantWeights) : gradedHilbertSeries (ksd.gradedHomDim wt) = (∏ i : Fin ksd.rank, qInteger (ksd.degrees i)) * concreteCT_posRoots_lambda ksd.roots ksd.posRoots wt

theorem kostant_theorem_13_3 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) (hwt : wt ∈ ksd.dominantWeights) : ↑(Fintype.card ksd.W) • gradedHilbertSeries (ksd.gradedHomDim wt) = (∏ i : Fin ksd.rank, qInteger (ksd.degrees i)) * concreteCT_fullRoots_char ksd.roots (ksd.weylCharacter wt) ∧ gradedHilbertSeries (ksd.gradedHomDim wt) = (∏ i : Fin ksd.rank, qInteger (ksd.degrees i)) * concreteCT_posRoots_lambda ksd.roots ksd.posRoots wt ∧ ↑(Fintype.card ksd.W) • concreteCT_posRoots_lambda ksd.roots ksd.posRoots wt = concreteCT_fullRoots_char ksd.roots (ksd.weylCharacter wt)

theorem kostant_weylCharacter_zero {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : ksd.weylCharacter 0 = Finsupp.single 0 1

theorem kostant_qIntegerProd_mul_CT_posRoots_eq_one {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : (∏ i : Fin ksd.rank, qInteger (ksd.degrees i)) * concreteCT_posRoots ksd.roots ksd.posRoots = 1

theorem kostant_hilbertSeriesHomDual_zero {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : ksd.hilbertSeriesHomDual 0 = 1

def kostant_cst_mulBilinear {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : ↥ksd.invariantSubalgebra →ₗ[R] ↥ksd.harmonicSubspace →ₗ[R] SymmetricAlgebra R 𝔤

def kostant_cst_mulMap_R {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : TensorProduct R ↥ksd.invariantSubalgebra ↥ksd.harmonicSubspace →ₗ[R] SymmetricAlgebra R 𝔤

def kostant_cst_mulMap {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : TensorProduct R ↥ksd.invariantSubalgebra ↥ksd.harmonicSubspace →ₗ[↥ksd.invariantSubalgebra] SymmetricAlgebra R 𝔤

theorem kostant_cst_mulMap_bijective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : Function.Bijective ⇑(kostant_cst_mulMap ksd)

noncomputable def kostant_cst_tensor {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : TensorProduct R ↥ksd.invariantSubalgebra ↥ksd.harmonicSubspace ≃ₗ[↥ksd.invariantSubalgebra] SymmetricAlgebra R 𝔤

theorem kostant_cst_free {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : Module.Free (↥ksd.invariantSubalgebra) (SymmetricAlgebra R 𝔤)

noncomputable def kostant_Sg_tensor_decomposition {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : TensorProduct R ↥ksd.harmonicSubspace ↥ksd.invariantSubalgebra ≃ₗ[R] SymmetricAlgebra R 𝔤

theorem kostant_Sg_free_over_invariants {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : Module.Free (↥ksd.invariantSubalgebra) (SymmetricAlgebra R 𝔤)

noncomputable def kostant_Hom_Sg_linearEquiv {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (V : Type u_6) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [LieModule.IsIrreducible R 𝔤 V] [LieRingModule 𝔤 (SymmetricAlgebra R 𝔤)] [LieModule R 𝔤 (SymmetricAlgebra R 𝔤)] [Module (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)] : (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤) ≃ₗ[↥ksd.invariantSubalgebra] Fin (Module.finrank R ↥(LieModule.weightSpace V 0)) → ↥ksd.invariantSubalgebra

theorem nontrivial_of_irreducible_module (R : Type u_4) [CommRing R] (𝔤 : Type u_5) [LieRing 𝔤] [LieAlgebra R 𝔤] (V : Type u_6) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [LieModule.IsIrreducible R 𝔤 V] : Nontrivial R

theorem kostant_Hom_Sg_free_helper {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (V : Type u_6) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [LieModule.IsIrreducible R 𝔤 V] [LieRingModule 𝔤 (SymmetricAlgebra R 𝔤)] [LieModule R 𝔤 (SymmetricAlgebra R 𝔤)] [Module (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)] : Module.Free (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)

theorem kostant_Hom_Sg_rank_helper {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (V : Type u_6) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [LieModule.IsIrreducible R 𝔤 V] [LieRingModule 𝔤 (SymmetricAlgebra R 𝔤)] [LieModule R 𝔤 (SymmetricAlgebra R 𝔤)] [Module (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)] : Module.rank (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤) = ↑(Module.finrank R ↥(LieModule.weightSpace V 0))

noncomputable def kostant_Hom_Ug_linearEquiv {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (V : Type u_6) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [LieModule.IsIrreducible R 𝔤 V] [LieRingModule 𝔤 (UniversalEnvelopingAlgebra R 𝔤)] [LieModule R 𝔤 (UniversalEnvelopingAlgebra R 𝔤)] [Module (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (V →ₗ⁅R,𝔤⁆ UniversalEnvelopingAlgebra R 𝔤)] : (V →ₗ⁅R,𝔤⁆ UniversalEnvelopingAlgebra R 𝔤) ≃ₗ[↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))] Fin (Module.finrank R ↥(LieModule.weightSpace V 0)) → ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))

theorem kostant_Hom_Sg_free {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (V : Type u_4) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [LieModule.IsIrreducible R 𝔤 V] [LieRingModule 𝔤 (SymmetricAlgebra R 𝔤)] [LieModule R 𝔤 (SymmetricAlgebra R 𝔤)] [Module (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)] : Module.Free (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)

theorem kostant_Hom_Sg_rank_eq_cardinal {R : Type u_4} [CommRing R] [Nontrivial R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (V : Type u_6) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [LieModule.IsIrreducible R 𝔤 V] [LieRingModule 𝔤 (SymmetricAlgebra R 𝔤)] [LieModule R 𝔤 (SymmetricAlgebra R 𝔤)] [Module (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)] [Module.Free (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)] : Module.rank (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤) = ↑(Module.finrank R ↥(LieModule.weightSpace V 0))

noncomputable def kostant_Hom_Sg_tensorHom_equiv {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (V : Type u_4) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [LieModule.IsIrreducible R 𝔤 V] [LieRingModule 𝔤 (SymmetricAlgebra R 𝔤)] [LieModule R 𝔤 (SymmetricAlgebra R 𝔤)] [Module (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)] : (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤) ≃ₗ[↥ksd.invariantSubalgebra] Fin (Module.finrank R ↥(LieModule.weightSpace V 0)) → ↥ksd.invariantSubalgebra

noncomputable def kostant_Hom_Sg_rank_equiv {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (V : Type u_4) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [LieModule.IsIrreducible R 𝔤 V] [LieRingModule 𝔤 (SymmetricAlgebra R 𝔤)] [LieModule R 𝔤 (SymmetricAlgebra R 𝔤)] [Module (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)] [Module.Free (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)] : (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤) ≃ₗ[↥ksd.invariantSubalgebra] Fin (Module.finrank R ↥(LieModule.weightSpace V 0)) → ↥ksd.invariantSubalgebra

theorem kostant_Hom_Sg_rank {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (V : Type u_4) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [LieModule.IsIrreducible R 𝔤 V] [LieRingModule 𝔤 (SymmetricAlgebra R 𝔤)] [LieModule R 𝔤 (SymmetricAlgebra R 𝔤)] [Module (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)] [Module.Free (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤)] : Module.finrank (↥ksd.invariantSubalgebra) (V →ₗ⁅R,𝔤⁆ SymmetricAlgebra R 𝔤) = Module.finrank R ↥(LieModule.weightSpace V 0)

theorem powerSeries_zsmul_left_cancel {n : ℤ} (hn : n ≠ 0) {a b : PowerSeries ℤ} (h : n • a = n • b) : a = b

theorem weylGroup_card_ne_zero {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : ↑(Fintype.card ksd.W) ≠ 0

theorem kostant_hilbert_series_CT_eq {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (wt : ksd.P) (hwt : wt ∈ ksd.dominantWeights) : ↑(Fintype.card ksd.W) • concreteCT_posRoots_lambda ksd.roots ksd.posRoots wt = concreteCT_fullRoots_char ksd.roots (ksd.weylCharacter wt)

theorem concreteCT_fullRoots_char_one {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (roots : Finset ksd.P) : concreteCT_fullRoots_char roots (Finsupp.single 0 1) = concreteCT_fullRoots roots

theorem concreteCT_posRoots_lambda_zero {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (roots posRoots : Finset ksd.P) : concreteCT_posRoots_lambda roots posRoots 0 = concreteCT_posRoots roots posRoots

theorem kostant_hilbert_series_at_zero {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : (∏ i : Fin ksd.rank, qInteger (ksd.degrees i)) * concreteCT_fullRoots ksd.roots = ↑(Fintype.card ksd.W) • 1

theorem kostant_CT_fullRoots_eq_posRoots {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : ↑(Fintype.card ksd.W) • concreteCT_posRoots ksd.roots ksd.posRoots = concreteCT_fullRoots ksd.roots

theorem kostant_cor_134_fullRoots {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : (∏ i : Fin ksd.rank, qInteger (ksd.degrees i)) * concreteCT_fullRoots ksd.roots = ↑(Fintype.card ksd.W) • 1

theorem corollary_13_4 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : ↑(Fintype.card ksd.W) • concreteCT_posRoots ksd.roots ksd.posRoots = concreteCT_fullRoots ksd.roots ∧ (∏ i : Fin ksd.rank, qInteger (ksd.degrees i)) * concreteCT_posRoots ksd.roots ksd.posRoots = 1

noncomputable def kostant_center_is_polynomial {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) ≃ₐ[R] MvPolynomial (Fin ksd.rank) R

def pbw_mulBilinear {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) →ₗ[R] ↥ksd.harmonicSubspaceUEA →ₗ[R] UniversalEnvelopingAlgebra R 𝔤

def pbw_mulMap_R {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : TensorProduct R ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) ↥ksd.harmonicSubspaceUEA →ₗ[R] UniversalEnvelopingAlgebra R 𝔤

def pbw_mulMap {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : TensorProduct R ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) ↥ksd.harmonicSubspaceUEA →ₗ[↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))] UniversalEnvelopingAlgebra R 𝔤

theorem pbw_mulMap_bijective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : Function.Bijective ⇑(pbw_mulMap ksd)

noncomputable def pbwTensorEquivUEA {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : TensorProduct R ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) ↥ksd.harmonicSubspaceUEA ≃ₗ[↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))] UniversalEnvelopingAlgebra R 𝔤

@[reducible, inline]

noncomputable abbrev pbw_cst_tensor_UEA {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : TensorProduct R ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) ↥ksd.harmonicSubspaceUEA ≃ₗ[↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))] UniversalEnvelopingAlgebra R 𝔤

theorem pbwHarmonicFreeUEA {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : Module.Free R ↥ksd.harmonicSubspaceUEA

theorem pbw_harmonicFree_UEA {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : Module.Free R ↥ksd.harmonicSubspaceUEA

theorem pbw_free_lift {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : Module.Free (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (UniversalEnvelopingAlgebra R 𝔤)

theorem kostant_Ug_free_over_center_of_setupData {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : Module.Free (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (UniversalEnvelopingAlgebra R 𝔤)

theorem kostant_Ug_free_over_center {R : Type u_4} [CommRing R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : Module.Free (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (UniversalEnvelopingAlgebra R 𝔤)

theorem kostant_Hom_Ug_free {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (V : Type u_4) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [LieModule.IsIrreducible R 𝔤 V] [LieRingModule 𝔤 (UniversalEnvelopingAlgebra R 𝔤)] [LieModule R 𝔤 (UniversalEnvelopingAlgebra R 𝔤)] [Module (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (V →ₗ⁅R,𝔤⁆ UniversalEnvelopingAlgebra R 𝔤)] : Module.Free (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (V →ₗ⁅R,𝔤⁆ UniversalEnvelopingAlgebra R 𝔤)

theorem kostant_Hom_Ug_rank {R : Type u_4} [CommRing R] [Nontrivial R] {𝔤 : Type u_5} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) (V : Type u_6) [AddCommGroup V] [Module R V] [Module.Finite R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [LieModule.IsIrreducible R 𝔤 V] [LieRingModule 𝔤 (UniversalEnvelopingAlgebra R 𝔤)] [LieModule R 𝔤 (UniversalEnvelopingAlgebra R 𝔤)] [Module (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (V →ₗ⁅R,𝔤⁆ UniversalEnvelopingAlgebra R 𝔤)] [Module.Free (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (V →ₗ⁅R,𝔤⁆ UniversalEnvelopingAlgebra R 𝔤)] : Module.finrank (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (V →ₗ⁅R,𝔤⁆ UniversalEnvelopingAlgebra R 𝔤) = Module.finrank R ↥(LieModule.weightSpace V 0)

noncomputable def kostant_Ug_tensor_decomposition {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : TensorProduct R ↥ksd.harmonicSubspaceUEA ↥(Subalgebra.toSubmodule (Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) ≃ₗ[R] UniversalEnvelopingAlgebra R 𝔤

theorem theorem_13_5 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] (ksd : KostantSetupData) : Nonempty (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤)) ≃ₐ[R] MvPolynomial (Fin ksd.rank) R) ∧ Module.Free (↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (UniversalEnvelopingAlgebra R 𝔤)

noncomputable def KostantFqSingleFactor (q : ℝ) (z : ℂ) : ℂ

noncomputable def KostantFqProd {ι : Type u_4} {T : Type u_5} (posRoots : Finset ι) (φ : ι → T → ℂ) (q : ℝ) (x : T) : ℂ

theorem KostantFq_denom_ne_zero (q : ℝ) (z : ℂ) (hq : 0 ≤ q) (hq1 : q < 1) (hz : ‖z‖ = 1) : 1 - ↑q * z ≠ 0

theorem KostantFq_normSq_bound (q : ℝ) (z : ℂ) (hq : 0 ≤ q) (hz : ‖z‖ = 1) : Complex.normSq (1 - z) ≤ 4 * Complex.normSq (1 - ↑q * z)

theorem KostantFq_single_tendsto_one (z : ℂ) (hz1 : z ≠ 1) : Filter.Tendsto (fun (q : ℝ) => (1 - z) / (1 - ↑q * z)) (nhdsWithin 1 (Set.Ioo 0 1)) (nhds 1)

theorem tendsto_norm_sq_sub_zero_complex {α : Type u_4} {l : Filter α} {f : α → ℂ} {a : ℂ} (hf : Filter.Tendsto f l (nhds a)) : Filter.Tendsto (fun (x : α) => ‖f x - a‖ ^ 2) l (nhds 0)

theorem kostant_lemma_13_2 {ι : Type u_4} {T : Type u_5} [MeasurableSpace T] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] (posRoots : Finset ι) (φ : ι → T → ℂ) (hφ_norm : ∀ α ∈ posRoots, ∀ (x : T), ‖φ α x‖ = 1) (hφ_meas : ∀ α ∈ posRoots, Measurable (φ α)) (hφ_ne_one : ∀ α ∈ posRoots, μ {x : T | φ α x = 1} = 0) : Filter.Tendsto (fun (q : ℝ) => ∫ (x : T), ‖KostantFqProd posRoots φ q x - 1‖ ^ 2 ∂μ) (nhdsWithin 1 (Set.Ioo 0 1)) (nhds 0)