structure JantzenFiltrationData (R : Type u_1) [CommRing R] (V₀ : Type u_3) [AddCommGroup V₀] [Module R V₀] : Type u_3

• level : ℕ → Submodule R V₀
• level_zero : self.level 0 = ⊤
• antitone : Antitone self.level
• iInf_eq_bot : ⨅ (m : ℕ), self.level m = ⊥

structure VermaJantzenFiltration (R : Type u_1) [CommRing R] (𝔤 : Type u_2) [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (M : Type u_mod) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVM : IsVermaModule Δ M wt) : Type u_mod

• level : ℕ → LieSubmodule R 𝔤 M
• level_zero : self.level 0 = ⊤
• antitone : Antitone self.level
• iInf_eq_bot : ⨅ (i : ℕ), self.level i = ⊥
• level_one_is_maximal : self.level 1 ≠ ⊤ ∧ ∀ (N : LieSubmodule R 𝔤 M), N ≠ ⊤ → N ≤ self.level 1

theorem VermaJantzenFiltration.level_one_ne_top {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] {wt : ↥Δ.𝔥 →ₗ[R] R} {hVM : IsVermaModule Δ M wt} (filt : VermaJantzenFiltration R 𝔤 M wt hVM) : filt.level 1 ≠ ⊤

theorem VermaJantzenFiltration.level_one_max {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] {wt : ↥Δ.𝔥 →ₗ[R] R} {hVM : IsVermaModule Δ M wt} (filt : VermaJantzenFiltration R 𝔤 M wt hVM) (N : LieSubmodule R 𝔤 M) (hN : N ≠ ⊤) : N ≤ filt.level 1

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

• corootPairing : (↥Δ.𝔥 →ₗ[R] R) → (↥Δ.𝔥 →ₗ[R] R) → R

def RootCorootData.ofPositiveRootData {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) : RootCorootData rd

def dotReflectedWeight {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (wg : WeylGroupData Δ) (cd : RootCorootData rd) (lam α : ↥Δ.𝔥 →ₗ[R] R) : ↥Δ.𝔥 →ₗ[R] R

structure FormalCharacterData {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (M : Type u_mod') [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (hVM : IsVermaModule Δ M wt) : Type (max (max (max u_1 u_2) (u_ch' + 1)) u_mod')

• CharGroup : Type u_ch'
• instACG : AddCommGroup self.CharGroup
• chSub : LieSubmodule R 𝔤 M → self.CharGroup
• chVerma : (↥Δ.𝔥 →ₗ[R] R) → self.CharGroup
• ch_top : self.chSub ⊤ = self.chVerma wt
• ch_bot : self.chSub ⊥ = 0

noncomputable def jantzenSumRoots {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (wg : WeylGroupData Δ) (cd : RootCorootData rd) (lam : ↥Δ.𝔥 →ₗ[R] R) : Finset (↥Δ.𝔥 →ₗ[R] R)