OAI/Analysis/KadisonKastler/ProjectionStrataCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Unitary coordinates for the original spectral subspace

The original isometric embedding and the assembled measurable rank strata have the same range. Their comparison is the required genuine unitary.

  1. theorem OAI.KadisonKastler.projectionStrataSynthesis_restrict line 27
  2. def OAI.KadisonKastler.projectionStrataCoordinates line 43
  3. theorem OAI.KadisonKastler.projectionStrataCoordinates_intertwines line 49
  4. theorem OAI.KadisonKastler.projectionStrataCoordinates_fiber_ae line 54