theorem CoxeterGroup.wordSigma_linear_combination {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (word : List B) (v : B → ℝ) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) : wordSigma M word v = v s • wordSigma M word (e s) + v t • wordSigma M word (e t)

If $v$ is supported on $\{s, t\}$, then $\sigma_w(v) = v_s \cdot \sigma_w \alpha_s + v_t \cdot \sigma_w \alpha_t$.

theorem CoxeterGroup.alternating_word_canonical {B : Type u_1} [DecidableEq B] [Fintype B] (s t : B) (hst : s ≠ t) (word : List B) (halt : ∀ b ∈ word, b = s ∨ b = t) (hchain : List.Chain' (fun (x1 x2 : B) => x1 ≠ x2) word) (hlast : word = [] ∨ ∃ (h : word ≠ []), word.getLast h = t) : (∃ (k : ℕ), word = altWordEven s t k) ∨ ∃ (k : ℕ), word = t :: altWordEven s t k

A word on $\{s, t\}$ with consecutive entries distinct and last letter $t$ is canonical: of the form $stst\cdots$ of even length or $tsts\cdots t$ of odd length.

theorem CoxeterGroup.parabolic_pos_of_canon {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (word : List B) (hlen : word.length < M.M s t ∨ M.M s t = 0) (hcanon : (∃ (k : ℕ), word = altWordEven s t k) ∨ ∃ (k : ℕ), word = t :: altWordEven s t k) : IsPositive (wordSigma M word (e s))

Positivity for canonical alternating words on $\{s, t\}$: dispatches to the dihedral even/odd cases.

theorem CoxeterGroup.parabolic_pos {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (word : List B) (halt : ∀ b ∈ word, b = s ∨ b = t) (hlen : word.length < M.M s t ∨ M.M s t = 0) (hchain : List.Chain' (fun (x1 x2 : B) => x1 ≠ x2) word) (hlast : word = [] ∨ ∃ (h : word ≠ []), word.getLast h = t) : IsPositive (wordSigma M word (e s))

Positivity in the rank-2 parabolic $W_{\{s,t\}}$: any alternating word $w$ of length $< m(s,t)$ (or any length if $m(s,t) = 0$) gives $\sigma_w(\alpha_s) \geq 0$.

theorem CoxeterGroup.parabolic_pos_vector_of_both_positive {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (word : List B) (hpos_s : IsPositive (wordSigma M word (e s))) (hpos_t : IsPositive (wordSigma M word (e t))) (v : B → ℝ) (hpos : IsPositive v) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) : IsPositive (wordSigma M word v)

If $\sigma_w(\alpha_s)$ and $\sigma_w(\alpha_t)$ are positive vectors and $v \geq 0$ is supported on $\{s, t\}$, then $\sigma_w(v) \geq 0$.