OAI/Analysis/KadisonKastler/SpatialModularCoisometries.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Modular coisometries after adjoining an arbitrary tensor factor

These are the concrete sequences used in the state-shifting argument. Their scaling identity is for the modular conjugation of the full product, so no tensor-product formula for that conjugation is assumed.

  1. theorem OAI.KadisonKastler.PointedMatrixSites.exists_spatial_scaling_conjugations line 31
  2. theorem OAI.KadisonKastler.PointedMatrixSites.exists_spatial_modular_coisometries line 78