OAI/Analysis/KadisonSimilarity/Tracial/ConcreteTracialExpectation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact trace-pairing expectation consumed by the free-corner proof is constructed on concrete finite tracial von Neumann inclusions and transported through faithful algebra coordinates.

  1. def OAI.KadisonSimilarity.concreteTracialExpectation line 22
  2. theorem OAI.KadisonSimilarity.concreteTracialExpectation_norm_le line 32
  3. def OAI.KadisonSimilarity.TracialExpectation.comapEquiv line 44

    Source documentation

    Transport the trace-pairing characterization to the inverse image of the same concrete subalgebra. Only the actual trace identity is required.

    def TracialExpectation.comapEquiv
    {τA : A →ₗ[ℂ] ℂ} {τB : B →ₗ[ℂ] ℂ} {S : StarSubalgebra ℂ B}
    (E : TracialExpectation τB S) (e : A ≃⋆ₐ[ℂ] B)
    (hτ : ∀ a, τB (e a) = τA a) :
    TracialExpectation τA (S.comap e.toStarAlgHom) where
…

    Mentions: OAI.KadisonSimilarity.TracialExpectation