OAI/Analysis/FreeEntropy/Signal.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEntropySeparation.norm_sum_sq_orthogonal line 12
  2. abbrev OAI.FiniteEntropySeparation.FreeTensor.groupUnitary line 29
  3. theorem OAI.FiniteEntropySeparation.FreeTensor.groupUnitary_zero line 33
  4. theorem OAI.FiniteEntropySeparation.FreeTensor.groupUnitary_add line 37
  5. theorem OAI.FiniteEntropySeparation.FreeTensor.star_groupUnitary line 42
  6. def OAI.FiniteEntropySeparation.FreeTensor.characterProjection line 45
  7. theorem OAI.FiniteEntropySeparation.FreeTensor.groupUnitary_mul_characterProjection line 49
  8. theorem OAI.FiniteEntropySeparation.FreeTensor.characterProjection_mul line 65
  9. theorem OAI.FiniteEntropySeparation.FreeTensor.star_characterProjection line 86
  10. theorem OAI.FiniteEntropySeparation.FreeTensor.sum_characterProjection line 100
  11. theorem OAI.FiniteEntropySeparation.FreeTensor.characterProjection_mem line 108
  12. theorem OAI.FiniteEntropySeparation.FreeTensor.trace_groupUnitary line 116
  13. theorem OAI.FiniteEntropySeparation.FreeTensor.trace_characterProjection line 121
  14. def OAI.FiniteEntropySeparation.FreeTensor.spectralSignal line 127
  15. theorem OAI.FiniteEntropySeparation.FreeTensor.spectralSignal_selfAdjoint line 131
  16. theorem OAI.FiniteEntropySeparation.FreeTensor.spectralSignal_mem line 137
  17. theorem OAI.FiniteEntropySeparation.FreeTensor.spectralSignal_pow line 143
  18. theorem OAI.FiniteEntropySeparation.FreeTensor.trace_spectralSignal_pow line 158
  19. theorem OAI.FiniteEntropySeparation.FreeTensor.characterProjection_orthogonal line 165
  20. theorem OAI.FiniteEntropySeparation.FreeTensor.spectralSignal_norm_le line 172