FreeWordExpectation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The base expectation kills every reduced word starting in the other free factor. This is derived from scalar freeness by trace tests.

theorem OAI.KadisonSimilarity.TracialExpectation.map_reduced_word line 18
Source documentation
A reduced word beginning in the other factor has zero base expectation, including when its final letter belongs to the base algebra.
```
theorem map_reduced_word (E : TracialExpectation τ A)
    (hfaithful : ∀ x, τ (star x * x) = 0 → x = 0)
    (hτ : τ 1 = 1) (hfree : ScalarFree τ D A)
    (x : P) (xs : List P) (hword : AlternatingCenteredWord τ D A true (x :: xs)) :
    E.map ((x :: xs).prod) = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.TracialExpectation, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.AlternatingCenteredWord

theorem OAI.KadisonSimilarity.TracialExpectation.map_base_mul_reduced_word line 41

Source documentation

A base letter at the front of such a word is removed by bimodularity.

theorem map_base_mul_reduced_word (E : TracialExpectation τ A)
    (hfaithful : ∀ x, τ (star x * x) = 0 → x = 0)
    (hτ : τ 1 = 1) (hfree : ScalarFree τ D A)
    (a : P) (ha : a ∈ A) (x : P) (xs : List P)
    (hword : AlternatingCenteredWord τ D A true (x :: xs)) :
    E.map (a * (x :: xs).prod) = 0 := by
…

Mentions: OAI.KadisonSimilarity.TracialExpectation, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.AlternatingCenteredWord