OAI/Analysis/KadisonKastler/TwoRatioRemoteBlock.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Remote copies of two-ratio matrix blocks

Both site families are shifted beyond the two specified finite stages. The shift preserves the density parameters, so the new block has exactly the old matrix moments and is independent of the prescribed local algebra.

  1. def OAI.KadisonKastler.twoRatioRemoteSites line 19
  2. theorem OAI.KadisonKastler.twoRatioRemoteSites_nodup line 22
  3. def OAI.KadisonKastler.twoRatioRemoteIndex line 25
  4. def OAI.KadisonKastler.PointedMatrixSites.twoRatioRemoteMatrix line 37
  5. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatioRemoteMatrix_algebra line 42
  6. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatioRemoteMatrix_le line 47
  7. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatioRemoteMatrix_commutes line 52
  8. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatioRemoteMatrix_moment line 57
  9. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatioRemoteMatrix_independent line 68