WeightSpaceWordSpan.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Generalized weight spaces in a homogeneous word basis

theorem OAI.PolycyclicRecognition.genWeightSpace_le_span_basis_by_weight line 19

Source documentation

In a basis of generalized weight vectors, any chosen collection of weight spaces lies in the span of the basis vectors with those weights.

theorem genWeightSpace_le_span_basis_by_weight
    (b : Basis J ℝ M) (χ : J → Weight ℝ H M)
    (hb : ∀ j, b j ∈ genWeightSpace M (χ j))
    (selected : Weight ℝ H M → Prop) (α : Weight ℝ H M) (hα : selected α) :
    (genWeightSpace M α).toSubmodule ≤ Submodule.span ℝ (b '' {j | selected (χ j)}) := by
…