Model.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KLInvariance.BruhatStep line 14
Source documentation
An upward edge in the strong Bruhat graph, with left reflection labels.
Also declared: ComparatorChallenges/KLInvariance.lean:14 (same declaration text).
```
def BruhatStep (cs : CoxeterSystem M W) (x y : W) : Prop :=
…
```
def OAI.KLInvariance.BruhatLE line 18
Source documentation
The actual strong Bruhat order, not the weak order.
Also declared: ComparatorChallenges/KLInvariance.lean:18 (same declaration text).
```
def BruhatLE (cs : CoxeterSystem M W) : W → W → Prop :=
…
```
def OAI.KLInvariance.Interval line 22
Source documentation
The unlabelled interval, including both endpoints.
Also declared: ComparatorChallenges/KLInvariance.lean:22 (same declaration text).
```
def Interval (cs : CoxeterSystem M W) (u b : W) :=
…
```
instance OAI.KLInvariance.intervalOrder line 25
Also declared: ComparatorChallenges/KLInvariance.lean:25 (same declaration text).
def OAI.KLInvariance.rankDifference line 45
Source documentation
d(x,y) in the manuscript, used only for comparable endpoints.
Also declared: ComparatorChallenges/KLInvariance.lean:45 (same declaration text).
```
noncomputable def rankDifference (cs : CoxeterSystem M W) (x y : W) : ℕ :=
…
```
abbrev OAI.KLInvariance.PolynomialFamilies line 48
Also declared: ComparatorChallenges/KLInvariance.lean:48 (same declaration text).
structure OAI.KLInvariance.NormalizedKL line 55
Source documentation
Exact equal-parameter normalization in the introduction. The first family is R and the second is P. reflect d p is q^d p(q⁻¹) when p.natDegree ≤ d, which follows here from the degree bound (or the diagonal normalization). The sum is over the real Bruhat interval; its finiteness is a separate theorem, not a different definition of order.
Also declared: ComparatorChallenges/KLInvariance.lean:55 (same declaration text).
```
structure NormalizedKL (cs : CoxeterSystem M W) (RP : PolynomialFamilies W) : Prop where
…
```
Mentions: OAI.KLInvariance.PolynomialFamilies
def OAI.KLInvariance.klFamilies line 74
Source documentation
The polynomial families selected by their equal-parameter normalization.
Also declared: ComparatorChallenges/KLInvariance.lean:74 (same declaration text).
```
noncomputable def klFamilies (cs : CoxeterSystem M W) : PolynomialFamilies W :=
…
```
Mentions: OAI.KLInvariance.PolynomialFamilies
def OAI.KLInvariance.klPolynomial line 77
Also declared: ComparatorChallenges/KLInvariance.lean:77 (same declaration text).