OAI/Analysis/KadisonSimilarity/FreeProduct/CompressionProjectionTransport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal inclusion projections in the head tensor coordinates.

  1. theorem OAI.KadisonSimilarity.isometryRangeProjection_comp line 15
  2. theorem OAI.KadisonSimilarity.isometryRangeProjection_complement line 23
  3. theorem OAI.KadisonSimilarity.firstLetterProjection_of_inclusion line 48

    Source documentation

    Factoring the inclusion through the vacuum insertion gives the exact first-letter projection used in the compression model.

    theorem firstLetterProjection_of_inclusion
    (Ω : E) (j : F →ₗᵢ[ℂ] K) (v : F →ₗᵢ[ℂ] HilbertTensor E K)
    (hv : v.toContinuousLinearMap = (hilbertTensorInsert Ω).comp j.toContinuousLinearMap) :
    firstLetterProjection Ω (isometryRangeProjection j) = isometryRangeProjection v := by
…

    Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.firstLetterProjection, OAI.KadisonSimilarity.isometryRangeProjection