ExpectationWordClosure.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Extending the two-dimensional expectation range from word vectors to their tracial Hilbert closure. Orthogonal projection supplies continuity.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.expectation_span_of_word_closure line 21

Source documentation

The expectation of a Hilbert limit of word vectors still lies in the span of the unit and the specified base element.

theorem expectation_span_of_word_closure (E : TracialExpectation G.trace A)
    (hfaithful : Function.Injective G.vector) (s : P) (words : Set P)
    (hword : ∀ x ∈ words, ∃ α β : ℂ, E.map x = α • (1 : P) + β • s)
    (x : P) (hx : G.vector x ∈
      (Submodule.span ℂ (G.vector '' words)).topologicalClosure) :
    ∃ α β : ℂ, E.map x = α • (1 : P) + β • s := by
…

Mentions: OAI.KadisonSimilarity.TracialExpectation