GeneratedWordDensity.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Ordinary algebraic generation implies density of centered reduced words. This is an algebraic centering argument, independent of freeness.

theorem OAI.KadisonSimilarity.alternatingProduct_cons line 13
def OAI.KadisonSimilarity.CenteredWordSpan.words line 25
def OAI.KadisonSimilarity.CenteredWordSpan.span line 31
theorem OAI.KadisonSimilarity.CenteredWordSpan.word_mem line 33
theorem OAI.KadisonSimilarity.CenteredWordSpan.base_mem line 39
theorem OAI.KadisonSimilarity.CenteredWordSpan.one_mem line 43
theorem OAI.KadisonSimilarity.CenteredWordSpan.other_mul_word line 45

theorem OAI.KadisonSimilarity.CenteredWordSpan.base_mul_word line 54

Source documentation

Centering the first two letters reduces all remaining products to a shorter word.

theorem base_mul_word (hτ : τ 1 = 1) (n : ℕ) (x : A) (d : D) (b : A)
    (a : Fin n → A) (c : Fin n → D)
    (ha : ∀ i, τ (a i : P) = 0) (hc : ∀ i, τ (c i : P) = 0) :
    (x : P) * ((d : P) * alternatingProduct (fun i => (a i : P))
      (fun i => (c i : P)) * (b : P)) ∈ span τ A D := by
…

Mentions: OAI.KadisonSimilarity.alternatingProduct, OAI.KadisonSimilarity.CenteredWordSpan.span

theorem OAI.KadisonSimilarity.CenteredWordSpan.factor_mul line 117
Source documentation
Left multiplication by either generating algebra preserves the full span.
```
theorem factor_mul (hτ : τ 1 = 1) {x y : P}
    (hx : x ∈ (A : Set P) ∪ (D : Set P)) (hy : y ∈ span τ A D) :
    x * y ∈ span τ A D := by
…
```
Mentions: OAI.KadisonSimilarity.CenteredWordSpan.span
def OAI.KadisonSimilarity.CenteredWordSpan.preservingAlgebra line 131
Source documentation
The elements preserving a given word span form an ordinary subalgebra.
```
def preservingAlgebra : Subalgebra ℂ P where
…
```
theorem OAI.KadisonSimilarity.CenteredWordSpan.generated_mem line 145
Source documentation
Centered normal forms span the ordinary star algebra generated by the factors.
```
theorem generated_mem (hτ : τ 1 = 1) {x : P} (hx : x ∈ factorAlgebra A D) :
    x ∈ span τ A D := by
…
```
Mentions: OAI.KadisonSimilarity.CenteredWordSpan.span
theorem OAI.KadisonSimilarity.TracialCornerGeometry.vector_mem_reducedWordSpan line 161
theorem OAI.KadisonSimilarity.TracialCornerGeometry.reducedWordGenerated_of_factorsTraciallyGenerate line 174
Source documentation
No additional density assumption on centered normal forms is needed once the two ordinary factor algebras generate the tracial Hilbert space.
```
theorem reducedWordGenerated_of_factorsTraciallyGenerate (hτ : G.trace 1 = 1)
    (hgen : G.FactorsTraciallyGenerate A D) : ReducedWordGenerated G A D := by
…
```
Mentions: OAI.KadisonSimilarity.ReducedWordGenerated