theorem CoxeterGroup.bilinForm_add_left {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (v₁ v₂ w : B → ℝ) : bilinForm M (v₁ + v₂) w = bilinForm M v₁ w + bilinForm M v₂ w

The bilinear form $B_M$ on $\mathbb{R}^B$ is additive in its left argument.

theorem CoxeterGroup.bilinForm_smul_left {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (c : ℝ) (v w : B → ℝ) : bilinForm M (c • v) w = c * bilinForm M v w

The bilinear form $B_M$ is $\mathbb{R}$-linear in its left argument.

theorem CoxeterGroup.sigma_add {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (v₁ v₂ : B → ℝ) : sigma M s (v₁ + v₂) = sigma M s v₁ + sigma M s v₂

Additivity: $\sigma_s(v_1 + v_2) = \sigma_s v_1 + \sigma_s v_2$.

theorem CoxeterGroup.sigma_smul {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (c : ℝ) (v : B → ℝ) : sigma M s (c • v) = c • sigma M s v

Homogeneity: $\sigma_s(c \cdot v) = c \cdot \sigma_s v$ for $c \in \mathbb{R}$.

noncomputable def CoxeterGroup.sigmaLinearMap {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : (B → ℝ) →ₗ[ℝ] B → ℝ

The geometric reflection $\sigma_s : \mathbb{R}^B \to \mathbb{R}^B$ associated to $s \in S$, packaged as an $\mathbb{R}$-linear map.

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

Sign flip on the simple root: $\langle \sigma_s v, \alpha_s \rangle = -\langle v, \alpha_s\rangle$.

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

Involution: $\sigma_s \circ \sigma_s = \mathrm{id}$ on $\mathbb{R}^B$.

noncomputable def CoxeterGroup.sigmaLinearEquiv {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : (B → ℝ) ≃ₗ[ℝ] B → ℝ

$\sigma_s$ as a linear automorphism of $\mathbb{R}^B$, built from the involution property.

@[simp]

theorem CoxeterGroup.sigmaLinearEquiv_apply {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (v : B → ℝ) : (sigmaLinearEquiv M s) v = sigma M s v

Unfolding lemma: sigmaLinearEquiv acts as sigma.

theorem CoxeterGroup.bilinForm_add_right {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (v w₁ w₂ : B → ℝ) : bilinForm M v (w₁ + w₂) = bilinForm M v w₁ + bilinForm M v w₂

Additivity of $B_M$ in the right argument.

theorem CoxeterGroup.bilinForm_smul_right {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (v : B → ℝ) (c : ℝ) (w : B → ℝ) : bilinForm M v (c • w) = c * bilinForm M v w

$\mathbb{R}$-linearity of $B_M$ in the right argument.

theorem CoxeterGroup.bilinForm_symm {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (v w : B → ℝ) : bilinForm M v w = bilinForm M w v

Symmetry: $B_M(v, w) = B_M(w, v)$.

theorem CoxeterGroup.sigma_preserves_form {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (v w : B → ℝ) : bilinForm M (sigma M s v) (sigma M s w) = bilinForm M v w

Each geometric reflection preserves the bilinear form: $B_M(\sigma_s v, \sigma_s w) = B_M(v, w)$.

noncomputable def CoxeterGroup.wordSigma {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : List B → (B → ℝ) → B → ℝ

Action of a word $s_1 \cdots s_k$ on $\mathbb{R}^B$ by the composition of geometric reflections $\sigma_{s_1} \circ \cdots \circ \sigma_{s_k}$.

@[simp]

theorem CoxeterGroup.wordSigma_nil {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (v : B → ℝ) : wordSigma M [] v = v

The empty word acts as the identity.

@[simp]

theorem CoxeterGroup.wordSigma_singleton {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (v : B → ℝ) : wordSigma M [s] v = sigma M s v

A length-one word acts via a single reflection.

@[simp]

theorem CoxeterGroup.wordSigma_cons {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (rest : List B) (v : B → ℝ) : wordSigma M (s :: rest) v = sigma M s (wordSigma M rest v)

Cons unfolding: $(s :: w) \cdot v = \sigma_s (w \cdot v)$.

theorem CoxeterGroup.wordSigma_append {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (w₁ w₂ : List B) (v : B → ℝ) : wordSigma M (w₁ ++ w₂) v = wordSigma M w₁ (wordSigma M w₂ v)

Concatenation respects composition: $(w_1 \!+\!\!+\, w_2) \cdot v = w_1 \cdot (w_2 \cdot v)$.

theorem CoxeterGroup.wordSigma_add {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (v₁ v₂ : B → ℝ) : wordSigma M word (v₁ + v₂) = wordSigma M word v₁ + wordSigma M word v₂

Additivity of the word action on vectors.

theorem CoxeterGroup.wordSigma_smul {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (c : ℝ) (v : B → ℝ) : wordSigma M word (c • v) = c • wordSigma M word v

Homogeneity of the word action with respect to scalar multiplication.

theorem CoxeterGroup.wordSigma_preserves_form {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (v w : B → ℝ) : bilinForm M (wordSigma M word v) (wordSigma M word w) = bilinForm M v w

Every word acts by isometries of $B_M$: $B_M(\sigma_w v, \sigma_w w') = B_M(v, w')$.

theorem CoxeterGroup.sigma_e_other {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) : sigma M s (e t) = fun (u : B) => e t u - 2 * formVal M t s * e s u

Action on a different basis vector: $\sigma_s(\alpha_t) = \alpha_t - 2\,B_M(\alpha_t,\alpha_s)\,\alpha_s$.