OAI/Analysis/KadisonKastler/RelativeMatrixPreparation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A nearby relative matrix stage containing an almost-central projection

Relative Powers–Størmer converts state approximation into approximation on the original Hilbert space. The resulting stage extends the initial one.

  1. theorem OAI.KadisonKastler.TypeIIIFactor.exists_relative_matrix_state_of_projection_gap line 24
  2. theorem OAI.KadisonKastler.TypeIIIFactor.exists_relative_matrix_stage_near_projection line 64