@[reducible, inline]

abbrev HeckeCoeffRing : Type

noncomputable def heckeQ : HeckeCoeffRing

@[reducible, inline]

noncomputable abbrev hecke_q : HeckeCoeffRing

structure CoxeterGroupData : Type (u_1 + 1)

• W : Type u_1
• grpInst : Group self.W
• finInst : Fintype self.W
• decEq : DecidableEq self.W
• simpleReflections : Finset self.W
• length : self.W → ℕ
• length_one : self.length 1 = 0
• length_simple (s : self.W) : s ∈ self.simpleReflections → self.length s = 1
• simple_sq (s : self.W) : s ∈ self.simpleReflections → s * s = 1
• bruhatLE : self.W → self.W → Prop
• bruhatLE_dec (y w : self.W) : Decidable (self.bruhatLE y w)
• bruhat_refl (w : self.W) : self.bruhatLE w w
• bruhat_trans (x y z : self.W) : self.bruhatLE x y → self.bruhatLE y z → self.bruhatLE x z
• bruhat_antisymm (x y : self.W) : self.bruhatLE x y → self.bruhatLE y x → x = y
• bruhat_length_le (y w : self.W) : self.bruhatLE y w → self.length y ≤ self.length w
• bruhat_length_strict (y w : self.W) : self.bruhatLE y w → y ≠ w → self.length y < self.length w
• exchange_left (s : self.W) : s ∈ self.simpleReflections → ∀ (w : self.W), self.length (s * w) = self.length w + 1 ∨ self.length (s * w) + 1 = self.length w
• descentRefl : self.W → self.W
• descentRefl_simple (y : self.W) : y ≠ 1 → self.descentRefl y ∈ self.simpleReflections
• descentRefl_length (y : self.W) : y ≠ 1 → self.length (self.descentRefl y * y) < self.length y
• descentRefl_of_mul (s : self.W) : s ∈ self.simpleReflections → ∀ (w : self.W), self.length (s * w) = self.length w + 1 → self.descentRefl (s * w) = s

@[implicit_reducible]

instance instDecidableBruhatLE (C : CoxeterGroupData) (y w : C.W) : Decidable (C.bruhatLE y w)

@[reducible, inline]

abbrev HeckeAlgebra (C : CoxeterGroupData) : Type u_1

@[implicit_reducible]

noncomputable instance HeckeAlgebra.instAddCommMonoid (C : CoxeterGroupData) : AddCommMonoid (HeckeAlgebra C)

@[implicit_reducible]

noncomputable instance HeckeAlgebra.instAddCommGroup (C : CoxeterGroupData) : AddCommGroup (HeckeAlgebra C)

@[implicit_reducible]

noncomputable instance HeckeAlgebra.instModule (C : CoxeterGroupData) : Module HeckeCoeffRing (HeckeAlgebra C)

noncomputable def HeckeAlgebra.T (C : CoxeterGroupData) (w : C.W) : HeckeAlgebra C

noncomputable def simpleReflMulBasis (C : CoxeterGroupData) (s w : C.W) : HeckeAlgebra C

noncomputable def simpleActOnLinComb (C : CoxeterGroupData) (s : C.W) (f : HeckeAlgebra C) : HeckeAlgebra C

@[irreducible]

def heckeMulBasis (C : CoxeterGroupData) (w₁ w₂ : C.W) : HeckeAlgebra C

noncomputable def heckeMul (C : CoxeterGroupData) (f g : HeckeAlgebra C) : HeckeAlgebra C

theorem CoxeterGroupData.simple_cancel (C : CoxeterGroupData) (s : C.W) (hs : s ∈ C.simpleReflections) (w : C.W) : s * (s * w) = w

theorem CoxeterGroupData.length_zero_eq_one (C : CoxeterGroupData) (w : C.W) (h : C.length w = 0) : w = 1

theorem CoxeterGroupData.simple_ne_one (C : CoxeterGroupData) (s : C.W) (hs : s ∈ C.simpleReflections) : s ≠ 1

theorem CoxeterGroupData.descentRefl_of_simple (C : CoxeterGroupData) (s : C.W) (hs : s ∈ C.simpleReflections) : C.descentRefl s = s

theorem simpleActOnLinComb_single (C : CoxeterGroupData) (s w : C.W) (c : HeckeCoeffRing) : simpleActOnLinComb C s (Finsupp.single w c) = c • simpleReflMulBasis C s w

theorem heckeMulBasis_one_left (C : CoxeterGroupData) (w : C.W) : heckeMulBasis C 1 w = Finsupp.single w 1

theorem heckeMulBasis_one_right (C : CoxeterGroupData) (w₁ : C.W) : heckeMulBasis C w₁ 1 = Finsupp.single w₁ 1

theorem heckeMulBasis_simple (C : CoxeterGroupData) (s : C.W) (hs : s ∈ C.simpleReflections) (w : C.W) : heckeMulBasis C s w = simpleReflMulBasis C s w

theorem simpleReflMulBasis_apply (C : CoxeterGroupData) (s y w : C.W) : (simpleReflMulBasis C s y) w = if C.length (s * y) = C.length y + 1 then if s * y = w then 1 else 0 else (if y = w then hecke_q - 1 else 0) + if s * y = w then hecke_q else 0

theorem heckeMulBasis_descent (C : CoxeterGroupData) (w₁ : C.W) (hw₁ : w₁ ≠ 1) : heckeMulBasis C (C.descentRefl w₁) (C.descentRefl w₁ * w₁) = Finsupp.single w₁ 1

theorem heckeMulBasis_unfold (C : CoxeterGroupData) (w₁ : C.W) (hw₁ : w₁ ≠ 1) (w₂ : C.W) : heckeMulBasis C w₁ w₂ = simpleActOnLinComb C (C.descentRefl w₁) (heckeMulBasis C (C.descentRefl w₁ * w₁) w₂)

theorem simpleActOnLinComb_add (C : CoxeterGroupData) (s : C.W) (f g : HeckeAlgebra C) : simpleActOnLinComb C s (f + g) = simpleActOnLinComb C s f + simpleActOnLinComb C s g

theorem simpleActOnLinComb_quadratic (C : CoxeterGroupData) (s : C.W) (hs : s ∈ C.simpleReflections) (w : C.W) : simpleActOnLinComb C s (simpleReflMulBasis C s w) = hecke_q • Finsupp.single w 1 + (hecke_q - 1) • simpleReflMulBasis C s w

theorem simpleActOnLinComb_smul (C : CoxeterGroupData) (s : C.W) (c : HeckeCoeffRing) (f : HeckeAlgebra C) : simpleActOnLinComb C s (c • f) = c • simpleActOnLinComb C s f

theorem heckeMulBasis_assoc_gen_rhs (C : CoxeterGroupData) (s : C.W) (hs : s ∈ C.simpleReflections) (w₂ w₃ : C.W) : (Finsupp.sum (heckeMulBasis C w₂ w₃) fun (v : C.W) (c : HeckeCoeffRing) => c • heckeMulBasis C s v) = simpleActOnLinComb C s (heckeMulBasis C w₂ w₃)

theorem simpleActOnLinComb_quadratic_gen (C : CoxeterGroupData) (s : C.W) (hs : s ∈ C.simpleReflections) (f : HeckeAlgebra C) : simpleActOnLinComb C s (simpleActOnLinComb C s f) = (hecke_q - 1) • simpleActOnLinComb C s f + hecke_q • f

theorem heckeMulBasis_assoc_gen (C : CoxeterGroupData) (s : C.W) (hs : s ∈ C.simpleReflections) (w₂ w₃ : C.W) : (Finsupp.sum (heckeMulBasis C s w₂) fun (v : C.W) (c : HeckeCoeffRing) => c • heckeMulBasis C v w₃) = Finsupp.sum (heckeMulBasis C w₂ w₃) fun (v : C.W) (c : HeckeCoeffRing) => c • heckeMulBasis C s v

theorem finsupp_sum_comm_smul {W : Type u_1} {R : Type u_2} [CommRing R] (g : W → W →₀ R) (outer : W →₀ R) (inner : W → W →₀ R) : (outer.sum fun (v : W) (c : R) => c • (inner v).sum fun (u : W) (d : R) => d • g u) = (outer.sum fun (v : W) (c : R) => c • inner v).sum fun (u : W) (d : R) => d • g u

theorem heckeMulBasis_assoc (C : CoxeterGroupData) (w₁ w₂ w₃ : C.W) : (Finsupp.sum (heckeMulBasis C w₁ w₂) fun (v : C.W) (c : HeckeCoeffRing) => c • heckeMulBasis C v w₃) = Finsupp.sum (heckeMulBasis C w₂ w₃) fun (v : C.W) (c : HeckeCoeffRing) => c • heckeMulBasis C w₁ v

@[implicit_reducible]

noncomputable instance HeckeAlgebra.instRing (C : CoxeterGroupData) : Ring (HeckeAlgebra C)

noncomputable def HeckeAlgebra.ofScalar (C : CoxeterGroupData) (a : HeckeCoeffRing) : HeckeAlgebra C

noncomputable def heckeAlgebraMap (C : CoxeterGroupData) : HeckeCoeffRing →+* HeckeAlgebra C

@[implicit_reducible]

noncomputable instance HeckeAlgebra.instAlgebra (C : CoxeterGroupData) : Algebra HeckeCoeffRing (HeckeAlgebra C)

theorem heckeMul_single_single (C : CoxeterGroupData) (w₁ w₂ : C.W) (r₁ r₂ : HeckeCoeffRing) : heckeMul C (Finsupp.single w₁ r₁) (Finsupp.single w₂ r₂) = (r₁ * r₂) • heckeMulBasis C w₁ w₂

theorem heckeMul_add_left (C : CoxeterGroupData) (f₁ f₂ g : HeckeAlgebra C) : heckeMul C (f₁ + f₂) g = heckeMul C f₁ g + heckeMul C f₂ g

theorem heckeMul_add_right (C : CoxeterGroupData) (f g₁ g₂ : HeckeAlgebra C) : heckeMul C f (g₁ + g₂) = heckeMul C f g₁ + heckeMul C f g₂

noncomputable def heckeStdBasis (C : CoxeterGroupData) : Module.Basis C.W HeckeCoeffRing (HeckeAlgebra C)

@[reducible, inline]

noncomputable abbrev hecke_std_basis (C : CoxeterGroupData) : Module.Basis C.W HeckeCoeffRing (HeckeAlgebra C)

theorem heckeStdBasis_eq_T (C : CoxeterGroupData) (w : C.W) : (heckeStdBasis C) w = HeckeAlgebra.T C w

theorem heckeStdBasis_coe_eq_T (C : CoxeterGroupData) : ⇑(heckeStdBasis C) = HeckeAlgebra.T C

theorem hecke_basis (C : CoxeterGroupData) : LinearIndependent HeckeCoeffRing (HeckeAlgebra.T C) ∧ Submodule.span HeckeCoeffRing (Set.range (HeckeAlgebra.T C)) = ⊤

theorem hecke_basis_injective (C : CoxeterGroupData) : Function.Injective (HeckeAlgebra.T C)

noncomputable def coeffInvolution : HeckeCoeffRing → HeckeCoeffRing

theorem coeffInvolution_involutive : Function.Involutive coeffInvolution

theorem coeffInvolution_T (n : ℤ) : coeffInvolution (LaurentPolynomial.T n) = LaurentPolynomial.T (-n)

def negAddHom : ℤ →+ ℤ

noncomputable def coeffInvolutionRingHom : HeckeCoeffRing →+* HeckeCoeffRing

theorem coeffInvolution_eq_ringHom (a : HeckeCoeffRing) : coeffInvolution a = coeffInvolutionRingHom a

theorem coeffInvolution_mul (a b : HeckeCoeffRing) : coeffInvolution (a * b) = coeffInvolution a * coeffInvolution b

theorem coeffInvolution_zero : coeffInvolution 0 = 0

theorem coeffInvolution_add (a b : HeckeCoeffRing) : coeffInvolution (a + b) = coeffInvolution a + coeffInvolution b

@[irreducible]

def RPoly (C : CoxeterGroupData) (x y : C.W) : Polynomial ℤ

noncomputable def polyEvalQInv (p : Polynomial ℤ) : HeckeCoeffRing

noncomputable def D_on_basis (C : CoxeterGroupData) (w : C.W) : HeckeAlgebra C

noncomputable def HeckeAlgebra.D (C : CoxeterGroupData) : HeckeAlgebra C → HeckeAlgebra C

theorem HeckeAlgebra.D_zero (C : CoxeterGroupData) : D C 0 = 0

theorem HeckeAlgebra.D_add (C : CoxeterGroupData) (f g : HeckeAlgebra C) : D C (f + g) = D C f + D C g

theorem HeckeAlgebra.D_single (C : CoxeterGroupData) (w : C.W) (c : HeckeCoeffRing) : D C (Finsupp.single w c) = coeffInvolution c • D_on_basis C w

theorem HeckeAlgebra.D_semilinear (C : CoxeterGroupData) (a : HeckeCoeffRing) (h : HeckeAlgebra C) : D C (a • h) = coeffInvolution a • D C h

noncomputable def HeckeAlgebra.D_addHom (C : CoxeterGroupData) : HeckeAlgebra C →+ HeckeAlgebra C

theorem HeckeAlgebra.D_finset_sum (C : CoxeterGroupData) {ι : Type u_1} (s : Finset ι) (f : ι → HeckeAlgebra C) : D C (∑ i ∈ s, f i) = ∑ i ∈ s, D C (f i)

noncomputable def D_coeff (C : CoxeterGroupData) (x w : C.W) : HeckeCoeffRing

theorem finset_sum_single {α : Type u_1} [DecidableEq α] {β : Type u_2} [AddCommMonoid β] {ι : Type u_3} (s : Finset ι) (y : α) (f : ι → β) : ∑ i ∈ s, Finsupp.single y (f i) = Finsupp.single y (∑ i ∈ s, f i)

theorem smul_D_on_basis (C : CoxeterGroupData) (c : HeckeCoeffRing) (x : C.W) : c • D_on_basis C x = ∑ y : C.W, Finsupp.single y (c * D_coeff C y x)

theorem RPoly_unfold_lt (C : CoxeterGroupData) (x y : C.W) (hy : y ≠ 1) (hlt : C.length (C.descentRefl y * x) < C.length x) : RPoly C x y = RPoly C (C.descentRefl y * x) (C.descentRefl y * y)

theorem RPoly_unfold_ge (C : CoxeterGroupData) (x y : C.W) (hy : y ≠ 1) (hge : ¬C.length (C.descentRefl y * x) < C.length x) : RPoly C x y = (Polynomial.X - Polynomial.C 1) * RPoly C x (C.descentRefl y * y) + Polynomial.X * RPoly C (C.descentRefl y * x) (C.descentRefl y * y)

theorem RPoly_orthog (C : CoxeterGroupData) (w y : C.W) : ∑ z : C.W, coeffInvolution (D_coeff C z w) * D_coeff C y z = if y = w then 1 else 0

theorem sum_single_ite_eq (C : CoxeterGroupData) (w : C.W) : ∑ y : C.W, Finsupp.single y (if y = w then 1 else 0) = Finsupp.single w 1

theorem HeckeAlgebra.D_D_on_basis (C : CoxeterGroupData) (w : C.W) : D C (D_on_basis C w) = T C w

noncomputable def mkBoundedPoly (bound : ℕ) (coeffs : ℕ → ℤ) : Polynomial ℤ

theorem mkBoundedPoly_natDegree_le (bound : ℕ) (coeffs : ℕ → ℤ) : (mkBoundedPoly bound coeffs).natDegree ≤ bound

theorem poly_eq_mkBoundedPoly_of_deg_le (p : Polynomial ℤ) (bound : ℕ) (hdeg : p.natDegree ≤ bound) : p = mkBoundedPoly bound fun (j : ℕ) => p.coeff j

theorem mkBoundedPoly_congr (bound : ℕ) (f g : ℕ → ℤ) (h : ∀ j ≤ bound, f j = g j) : mkBoundedPoly bound f = mkBoundedPoly bound g

noncomputable def middleCoeffs (C : CoxeterGroupData) (y _w : C.W) (rec_val : C.W → Polynomial ℤ) : Polynomial ℤ

noncomputable def self_dual_coeffs (C : CoxeterGroupData) (y w : C.W) (_bound : ℕ) (rec_val : C.W → Polynomial ℤ) : ℕ → ℤ

@[irreducible]

def KazhdanLusztigPoly (C : CoxeterGroupData) (y w : C.W) : Polynomial ℤ

theorem kl_poly_zero_unless_bruhat_le (C : CoxeterGroupData) (y w : C.W) : ¬C.bruhatLE y w → KazhdanLusztigPoly C y w = 0

theorem kl_poly_diag (C : CoxeterGroupData) (w : C.W) : KazhdanLusztigPoly C w w = 1

theorem kazhdan_lusztig_conjecture_nonneg (C : CoxeterGroupData) (y w : C.W) (n : ℕ) : 0 ≤ (KazhdanLusztigPoly C y w).coeff n

structure CoxeterWeylCompatibility {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (C : CoxeterGroupData) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) : Type (max u_3 u_4)

• ι : C.W ≃* wg.W

noncomputable def categoryOMultiplicity {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (C : CoxeterGroupData) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (compat : CoxeterWeylCompatibility C rd wg) (lam : ↥Δ.𝔥 →ₗ[R] R) (y w : C.W) : ℕ

@[reducible, inline]

noncomputable abbrev categoryO_multiplicity {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (C : CoxeterGroupData) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (compat : CoxeterWeylCompatibility C rd wg) (lam : ↥Δ.𝔥 →ₗ[R] R) (y w : C.W) : ℕ

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

theorem kazhdan_lusztig_conjecture_multiplicity {R : Type u_1} [Field R] [IsAlgClosed R] [CharZero R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (C : CoxeterGroupData) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (compat : CoxeterWeylCompatibility C rd wg) (lam : ↥Δ.𝔥 →ₗ[R] R) (hlam_dr : IsDominantRegularWeight rd wg lam) (y w : C.W) : ↑(categoryOMultiplicity C rd wg compat lam y w) = Polynomial.eval 1 (KazhdanLusztigPoly C y w)

theorem kl_poly_longest (C : CoxeterGroupData) (w₀ : C.W) (hw₀ : ∀ (w : C.W), C.bruhatLE w w₀) (y : C.W) : KazhdanLusztigPoly C y w₀ = 1

noncomputable def polyToHeckeCoeff (p : Polynomial ℤ) : HeckeCoeffRing

noncomputable def KLBasisElement (C : CoxeterGroupData) (w : C.W) : HeckeAlgebra C

theorem kl_coeff_self_dual_identity (C : CoxeterGroupData) (x w : C.W) : ∑ y : C.W, coeffInvolution (LaurentPolynomial.T (-↑(C.length w)) * polyToHeckeCoeff (KazhdanLusztigPoly C y w)) * D_coeff C x y = LaurentPolynomial.T (-↑(C.length w)) * polyToHeckeCoeff (KazhdanLusztigPoly C x w)

theorem klp_unfold (C : CoxeterGroupData) (y w : C.W) (hle : C.bruhatLE y w) (hne : y ≠ w) : KazhdanLusztigPoly C y w = mkBoundedPoly ((C.length w - C.length y - 1) / 2) (self_dual_coeffs C y w ((C.length w - C.length y - 1) / 2) fun (z : C.W) => if C.bruhatLE y z ∧ z ≠ y ∧ C.bruhatLE z w then KazhdanLusztigPoly C z w else 0)

theorem self_dual_implies_coeff_eq (C : CoxeterGroupData) (Q : C.W → C.W → Polynomial ℤ) (hQ_zero : ∀ (y w : C.W), ¬C.bruhatLE y w → Q y w = 0) (hQ_diag : ∀ (w : C.W), Q w w = 1) (hQ_deg : ∀ (y w : C.W), C.bruhatLE y w → y ≠ w → (Q y w).natDegree ≤ (C.length w - C.length y - 1) / 2) (hQ_self_dual : ∀ (w : C.W), HeckeAlgebra.D C (∑ y : C.W, Finsupp.single y (LaurentPolynomial.T (-↑(C.length w)) * polyToHeckeCoeff (Q y w))) = ∑ y : C.W, Finsupp.single y (LaurentPolynomial.T (-↑(C.length w)) * polyToHeckeCoeff (Q y w))) (y w : C.W) (hle : C.bruhatLE y w) (hne : y ≠ w) (j : ℕ) (hj : j ≤ (C.length w - C.length y - 1) / 2) : (Q y w).coeff j = (middleCoeffs C y w fun (z : C.W) => if C.bruhatLE y z ∧ z ≠ y ∧ C.bruhatLE z w then Q z w else 0).coeff j

theorem self_dual_implies_recursion (C : CoxeterGroupData) (Q : C.W → C.W → Polynomial ℤ) (hQ_zero : ∀ (y w : C.W), ¬C.bruhatLE y w → Q y w = 0) (hQ_diag : ∀ (w : C.W), Q w w = 1) (hQ_deg : ∀ (y w : C.W), C.bruhatLE y w → y ≠ w → (Q y w).natDegree ≤ (C.length w - C.length y - 1) / 2) (hQ_self_dual : ∀ (w : C.W), HeckeAlgebra.D C (∑ y : C.W, Finsupp.single y (LaurentPolynomial.T (-↑(C.length w)) * polyToHeckeCoeff (Q y w))) = ∑ y : C.W, Finsupp.single y (LaurentPolynomial.T (-↑(C.length w)) * polyToHeckeCoeff (Q y w))) (y w : C.W) (hle : C.bruhatLE y w) (hne : y ≠ w) : Q y w = mkBoundedPoly ((C.length w - C.length y - 1) / 2) (self_dual_coeffs C y w ((C.length w - C.length y - 1) / 2) fun (z : C.W) => if C.bruhatLE y z ∧ z ≠ y ∧ C.bruhatLE z w then Q z w else 0)

theorem kl_poly_unique (C : CoxeterGroupData) (Q : C.W → C.W → Polynomial ℤ) (hQ_zero : ∀ (y w : C.W), ¬C.bruhatLE y w → Q y w = 0) (hQ_diag : ∀ (w : C.W), Q w w = 1) (hQ_deg : ∀ (y w : C.W), C.bruhatLE y w → y ≠ w → (Q y w).natDegree ≤ (C.length w - C.length y - 1) / 2) (hQ_recursion : ∀ (y w : C.W), C.bruhatLE y w → y ≠ w → Q y w = mkBoundedPoly ((C.length w - C.length y - 1) / 2) (self_dual_coeffs C y w ((C.length w - C.length y - 1) / 2) fun (z : C.W) => if C.bruhatLE y z ∧ z ≠ y ∧ C.bruhatLE z w then Q z w else 0)) (y w : C.W) : Q y w = KazhdanLusztigPoly C y w