PointedWordMoments.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Vacuum moments of arbitrary matrix-site words

Distinct-site product moments determine repeated words as well. The algebraic reduction is shared across representations and site reindexings.

def OAI.KadisonKastler.MatrixSiteWord.letterAt line 19
theorem OAI.KadisonKastler.MatrixSiteWord.letterAt_eq line 23
def OAI.KadisonKastler.MatrixSiteWord.weight line 31
theorem OAI.KadisonKastler.MatrixSiteWord.weight_reindex line 34
theorem OAI.KadisonKastler.MatrixSiteWord.indices_reindex line 43
theorem OAI.KadisonKastler.MatrixSiteWord.nodup_indices_reindex line 47
theorem OAI.KadisonKastler.PointedMatrixSites.word_moment_of_nodup line 63
Source documentation
The finite-site moment axiom applied to a word with distinct indices.
```
theorem word_moment_of_nodup (S : PointedMatrixSites M Ω ν)
    (w : MatrixSiteWord I) (hw : (MatrixSiteWord.indices w).Nodup) :
    inner ℂ Ω (S.wordVector w) = MatrixSiteWord.weight ν w := by
…
```
Mentions: OAI.KadisonKastler.PointedMatrixSites, OAI.KadisonKastler.MatrixSiteWord, OAI.KadisonKastler.MatrixSiteWord.indices, OAI.KadisonKastler.MatrixSiteWord.weight
theorem OAI.KadisonKastler.PointedMatrixSites.word_moment_eq_of_reindex line 92
Source documentation
All vacuum word moments agree after a weight-preserving site bijection, including words that visit the same site repeatedly.
```
theorem word_moment_eq_of_reindex (S : PointedMatrixSites M Ω ν)
    (T : PointedMatrixSites N ξ η) (e : I ≃ J) (hweight : ∀ i, η (e i) = ν i)
    (w : MatrixSiteWord I) :
    inner ℂ Ω (S.wordVector w) = inner ℂ ξ (T.wordVector (MatrixSiteWord.reindex e w)) := by
…
```
Mentions: OAI.KadisonKastler.PointedMatrixSites, OAI.KadisonKastler.MatrixSiteWord, OAI.KadisonKastler.MatrixSiteWord.reindex

theorem OAI.KadisonKastler.PointedMatrixSites.word_inner_eq_of_reindex line 124

Source documentation

The shared word Gram matrix is determined by the product moments.

theorem word_inner_eq_of_reindex (S : PointedMatrixSites M Ω ν)
    (T : PointedMatrixSites N ξ η) (e : I ≃ J) (hweight : ∀ i, η (e i) = ν i)
    (w v : MatrixSiteWord I) :
    inner ℂ (S.wordVector w) (S.wordVector v) =
      inner ℂ (T.wordVector (MatrixSiteWord.reindex e w))
        (T.wordVector (MatrixSiteWord.reindex e v)) := by
…

Mentions: OAI.KadisonKastler.PointedMatrixSites, OAI.KadisonKastler.MatrixSiteWord, OAI.KadisonKastler.MatrixSiteWord.reindex