OrdinaryR.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Construction of ordinary R-polynomials, left-simple recursion, degree bounds and inverse kernels.

def OAI.KLInvariance.OrdinaryR.variableUnit line 24
theorem OAI.KLInvariance.OrdinaryR.variableUnit_val line 27
theorem OAI.KLInvariance.OrdinaryR.rValue_polynomial line 31
Source documentation
Polynomiality of the R-values is proved from the Hecke-derived recursion.
```
theorem rValue_polynomial (cs : CoxeterSystem M W) (x y : W) :
    ∃ p : ℤ[X], p.toLaurent = HeckeQ.rValue cs variableUnit x y := by
…
```
Mentions: OAI.KLInvariance.HeckeQ.rValue, OAI.KLInvariance.OrdinaryR.variableUnit
def OAI.KLInvariance.OrdinaryR.polynomial line 62
theorem OAI.KLInvariance.OrdinaryR.toLaurent_polynomial line 65
theorem OAI.KLInvariance.OrdinaryR.polynomial_diagonal line 70
theorem OAI.KLInvariance.OrdinaryR.polynomial_zero line 75
theorem OAI.KLInvariance.OrdinaryR.polynomial_recursion line 80
theorem OAI.KLInvariance.OrdinaryR.polynomial_eval line 93
Source documentation
Specializing the honest integral polynomial recovers the Hecke R-value at every unit parameter, not just the Laurent indeterminate.
```
theorem polynomial_eval {C : Type*} [CommRing C] (cs : CoxeterSystem M W)
    (q : Cˣ) (x y : W) :
    Polynomial.eval₂ (Int.castRingHom C) (q : C) (polynomial cs x y) =
      HeckeQ.rValue cs q x y := by
…
```
Mentions: OAI.KLInvariance.OrdinaryR.polynomial, OAI.KLInvariance.HeckeQ.rValue
theorem OAI.KLInvariance.OrdinaryR.polynomial_degree line 125
Source documentation
The degree bound needed for the classical polynomial reciprocity.
```
theorem polynomial_degree (cs : CoxeterSystem M W) (x y : W) :
    (polynomial cs x y).natDegree ≤ rankDifference cs x y := by
…
```
Mentions: OAI.KLInvariance.OrdinaryR.polynomial, OAI.KLInvariance.rankDifference
theorem OAI.KLInvariance.OrdinaryR.eval_variableUnit line 177
theorem OAI.KLInvariance.OrdinaryR.polynomial_kernel line 190
Source documentation
Polynomial R is a kernel for the length-reflection involution.
```
theorem polynomial_kernel (cs : CoxeterSystem M W) (x y : W) :
    ∑ z ∈ lowerFinset cs y,
      polynomial cs x z * reflect (rankDifference cs z y) (polynomial cs z y) =
      if x = y then 1 else 0 := by
…
```
Mentions: OAI.KLInvariance.lowerFinset, OAI.KLInvariance.OrdinaryR.polynomial, OAI.KLInvariance.rankDifference
def OAI.KLInvariance.properIntervalFinset line 219
theorem OAI.KLInvariance.mem_properIntervalFinset line 223
theorem OAI.KLInvariance.rankDifference_add line 228
theorem OAI.KLInvariance.reflect_finset_sum line 236
theorem OAI.KLInvariance.OrdinaryR.polynomial_kernel_reverse line 245
theorem OAI.KLInvariance.sum_proper_eq_sub line 278