OAI/Analysis/KadisonKastler/FreeDiagonalLetters.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Centered letters for the finite-diagonal free-product representation

These are the coefficient and covariance identities used to construct the creation operators in the Ricard--Xu representation. No word-norm estimate or free-product representation is assumed.

  1. def OAI.KadisonKastler.diagonalLinearCombination line 21
  2. theorem OAI.KadisonKastler.diagonal_projection_product line 24
  3. theorem OAI.KadisonKastler.diagonalLinearCombination_mul line 33
  4. theorem OAI.KadisonKastler.star_diagonalLinearCombination line 47
  5. theorem OAI.KadisonKastler.trace_diagonalLinearCombination line 55
  6. def OAI.KadisonKastler.diagonalCentered line 63
  7. def OAI.KadisonKastler.diagonalCenteredCoefficient line 66
  8. theorem OAI.KadisonKastler.sum_diagonalCenteredCoefficient line 69
  9. theorem OAI.KadisonKastler.diagonalCentered_eq_linearCombination line 76
  10. theorem OAI.KadisonKastler.star_diagonalCentered line 85
  11. theorem OAI.KadisonKastler.trace_diagonalCentered line 90
  12. theorem OAI.KadisonKastler.trace_diagonalCentered_covariance line 96
  13. theorem OAI.KadisonKastler.diagonalCentered_mul line 115