def CoxeterGroup.IsPositive {B : Type u_1} (v : B → ℝ) : Prop

A vector $v : B \to \mathbb{R}$ is positive when $0 \le v(s)$ for every simple generator $s$.

def CoxeterGroup.IsNegative {B : Type u_1} (v : B → ℝ) : Prop

A vector $v : B \to \mathbb{R}$ is negative when $v(s) \le 0$ for every simple generator $s$.

theorem CoxeterGroup.neg_isPositive_iff {B : Type u_1} [DecidableEq B] [Fintype B] (v : B → ℝ) : IsPositive (-v) ↔ IsNegative v

$-v$ is positive iff $v$ is negative.

theorem CoxeterGroup.IsPositive.smul_nonneg {B : Type u_1} [DecidableEq B] [Fintype B] {v : B → ℝ} (hv : IsPositive v) {c : ℝ} (hc : 0 ≤ c) : IsPositive (c • v)

Scaling a positive vector by a nonnegative real keeps it positive.

theorem CoxeterGroup.IsPositive.add {B : Type u_1} [DecidableEq B] [Fintype B] {v w : B → ℝ} (hv : IsPositive v) (hw : IsPositive w) : IsPositive (v + w)

The sum of two positive vectors is positive.

theorem CoxeterGroup.formVal_nonpos_of_ne {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) : formVal M s t ≤ 0

For distinct simple generators $s \ne t$, the bilinear-form value $\langle e_s, e_t\rangle = -\cos(\pi/m_{st})$ is nonpositive.

theorem CoxeterGroup.sigmaLin_preserves_positive_off_diagonal {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) : IsPositive ((sigmaLin M s) (e t))

For $s \ne t$, $\sigma_s(e_t)$ is a positive root: it stays in the positive cone.

theorem CoxeterGroup.sigma_coord_ne {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (v : B → ℝ) (t : B) (hts : t ≠ s) : sigma M s v t = v t

For $t \ne s$, the $t$-coordinate of $\sigma_s(v)$ equals $v(t)$ (reflection fixes other coords).

theorem CoxeterGroup.sigma_coord_self {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (v : B → ℝ) : sigma M s v s = v s - 2 * bilinForm M v (e s)

The $s$-coordinate of $\sigma_s(v)$ is $v(s) - 2\langle v, e_s\rangle$.