OAI/Analysis/KadisonKastler/ProductBoundaryAlgebra.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Algebraic identities for first-coordinate boundary descent

  1. theorem OAI.KadisonKastler.firstBoundaryLiftL_const line 17
  2. theorem OAI.KadisonKastler.firstBoundaryLiftL_mul line 27
  3. theorem OAI.KadisonKastler.firstBoundaryLiftL_nonnegative_iff line 39
  4. theorem OAI.KadisonKastler.firstBoundaryLiftL_fixed line 57
  5. theorem OAI.KadisonKastler.firstBoundaryLiftL_intertwine line 73
  6. theorem OAI.KadisonKastler.FirstBoundaryProjection.norm_le line 96
  7. theorem OAI.KadisonKastler.FirstBoundaryProjection.positive line 100
  8. theorem OAI.KadisonKastler.FirstBoundaryProjection.lift_retract line 105
  9. theorem OAI.KadisonKastler.FirstBoundaryProjection.map_const line 110
  10. theorem OAI.KadisonKastler.FirstBoundaryProjection.module_map line 115
  11. theorem OAI.KadisonKastler.FirstBoundaryProjection.natural line 123