OAI/Analysis/KadisonSimilarity/FreeProduct/CanonicalFreeFactorComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Projection comparison for the actual canonical generated free product. The source normality and its dense matrix tower construct the orthogonal unitaries; freeness proves scalar center; the normal range gives comparison.

  1. theorem OAI.KadisonSimilarity.canonicalFreeFactorComparison line 36

    Source documentation

    Projection comparison follows from the faithful normal source, freeness and normality of the generated model.

    theorem canonicalFreeFactorComparison
    (hfree : ScalarFree τ.toLinearMap φ.range ψ.range)
    (hsource : τR.gnsStarAlgHom.range =
      (representationVonNeumannAlgebra τR.gnsStarAlgHom).toStarSubalgebra)
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop)
    (hnormal : ∃ N : VonNeumannAlgebra (canonicalGeneratedTrace τ htr φ ψ).GNS,
      (G).left.range = N.toStarSubalgebra) : (G).LocalFreeCornerPublishedInputs := by
…

    Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.canonicalGeneratedTrace