OAI/Analysis/KadisonSimilarity/FreeProduct/SymmetryWordAlgebra.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonSimilarity.SymmetryWordAlgebra.wordSpan line 18
2. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.word_mem line 20
3. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.one_mem line 23
4. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.symmetry_mem line 26
5. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.other_mul_false_word line 34

   Source documentation

   Centering an arbitrary other-factor letter provides its normal form before a word starting with the symmetry.

   theorem other_mul_false_word (d : P) (hd : d ∈ D) {xs : List P}
       (hw : CenteredSymmetryWord τ D s false xs) :
       d * xs.prod ∈ wordSpan τ D s := by
   …

   Mentions: OAI.KadisonSimilarity.CenteredSymmetryWord, OAI.KadisonSimilarity.SymmetryWordAlgebra.wordSpan

6. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.other_mul_word line 49
7. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.other_mul_mem line 61
8. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.other_mem line 72
9. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.symmetry_mul_word line 78
10. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.symmetry_mul_mem line 90
11. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.word_mul_mem line 101
12. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.mul_mem line 112
13. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.star_word_mem line 125
14. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.star_mem line 138
15. def OAI.KadisonSimilarity.SymmetryWordAlgebra.spanStarAlgebra line 147
16. theorem OAI.KadisonSimilarity.SymmetryWordAlgebra.generated_le_span line 158
17. theorem OAI.KadisonSimilarity.TracialCornerGeometry.symmetry_word_density_of_generated_density line 173
18. theorem OAI.KadisonSimilarity.TracialCornerGeometry.expectation_span_of_generated_symmetry_algebra line 202

    Source documentation

    The base expectation of the actual generated von Neumann algebra has the range needed in the Fourier argument. Only ordinary generated-algebra L² density remains, rather than an assumed range formula.

    theorem expectation_span_of_generated_symmetry_algebra
        (A D S : StarSubalgebra ℂ P) (E : TracialExpectation G.trace A)
        (hf : Function.Injective G.vector) (hτ : G.trace 1 = 1)
        (hfree : ScalarFree G.trace D A) (s : P) (hs : s ∈ A)
        (hs0 : G.trace s = 0) (hsq : s * s = 1) (hstar : star s = s)
        (hdense : ∀ x, x ∈ S → G.vector x ∈ (Submodule.span ℂ
          (G.vector '' (StarAlgebra.adjoin ℂ ((D : Set P) ∪ {s}) : Set P))).topologicalClosure)
        (x : P) (hx : x ∈ S) :
        ∃ α β : ℂ, E.map x = α • (1 : P) + β • s := by
    …

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