OAI/Analysis/FactorGeneration/TracialInclusion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The restricted faithful trace and the actual P^omega -> M^omega inclusion. All constructions are on the bounded-sequence quotient.

  1. def OAI.Generator.Tracial.coordinateInclusion line 16
  2. def OAI.Generator.Tracial.restrictedTrace line 19
  3. theorem OAI.Generator.Tracial.restrictedTrace_trace line 28
  4. theorem OAI.Generator.Tracial.restrictedTrace_norm₂ line 31
  5. def OAI.Generator.Tracial.boundedInclusion line 34
  6. theorem OAI.Generator.Tracial.inclusion_traceRel_iff line 43
  7. def OAI.Generator.Tracial.quotientInclusion line 47
  8. theorem OAI.Generator.Tracial.quotientInclusion_mk line 61
  9. theorem OAI.Generator.Tracial.quotientInclusion_injective line 65
  10. theorem OAI.Generator.Tracial.quotientInclusion_trace line 74
  11. def OAI.Generator.Tracial.insideAlgebra line 85

    Source documentation

    P, as a star subalgebra of M. Its completeness is derived, not assumed.

    def insideAlgebra : StarSubalgebra ℂ M.toStarSubalgebra :=
…
  12. theorem OAI.Generator.Tracial.insideAlgebra_closed line 88
  13. instance OAI.Generator.Tracial.insideAlgebra_complete line 91