OAI/Analysis/KadisonKastler/CyclicGramEquivalence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Cyclic Hilbert identifications from matching finite Gram matrices

The pointed matrix-product reindexing identifies finite word vectors. That identification extends from their dense linear spans to the Hilbert spaces.

  1. theorem OAI.KadisonKastler.norm_linearCombination_eq_of_gram line 21
  2. def OAI.KadisonKastler.cyclicGramEquivalence line 36

    Source documentation

    The Hilbert-space identification of two dense families with identical Gram matrices, including the prescribed action on each family vector.

    def cyclicGramEquivalence (v : I → H) (w : I → K)
    (hv : DenseRange (Finsupp.linearCombination ℂ v))
    (hw : DenseRange (Finsupp.linearCombination ℂ w))
    (h : ∀ i j, inner ℂ (v i) (v j) = inner ℂ (w i) (w j)) : H ≃ₗᵢ[ℂ] K :=
…
  3. theorem OAI.KadisonKastler.cyclicGramEquivalence_linearCombination line 44
  4. theorem OAI.KadisonKastler.cyclicGramEquivalence_apply line 52