structure KostantPartitionFn {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) : Type (max u_1 u_2)

• K : (↥Δ.𝔥 →ₗ[R] R) → ℕ
• K_zero : self.K 0 = 1
• K_zero_outside (β : ↥Δ.𝔥 →ₗ[R] R) : ¬rd.IsInQPlus β → self.K β = 0

structure ShapovalovDeterminantData {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (wg : WeylGroupData Δ) (cd : RootCorootData rd) (kpf : KostantPartitionFn rd) : Type (max u_1 u_2)

• shapovalovForm (β lam : ↥Δ.𝔥 →ₗ[R] R) : Matrix (Fin (kpf.K β)) (Fin (kpf.K β)) R
• D : (↥Δ.𝔥 →ₗ[R] R) → (↥Δ.𝔥 →ₗ[R] R) → R
• D_eq_det (β lam : ↥Δ.𝔥 →ₗ[R] R) : self.D β lam = (self.shapovalovForm β lam).det
• D_formula (β : ↥Δ.𝔥 →ₗ[R] R) : rd.IsInQPlus β → ∀ (N : ℕ), (∀ α ∈ rd.posRoots, ∀ (n : ℕ), N < n → kpf.K (β - n • α) = 0) → ∃ (c : R), c ≠ 0 ∧ ∀ (lam : ↥Δ.𝔥 →ₗ[R] R), self.D β lam = c * ∏ α ∈ rd.posRoots, ∏ n ∈ Finset.Icc 1 N, (cd.corootPairing (lam + wg.ρ) α - ↑n) ^ kpf.K (β - n • α)