OAI/Analysis/FreeEntropy/TensorLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEntropySeparation.LabelHilbert.orthogonal_embedding line 13
  2. def OAI.FiniteEntropySeparation.LabelHilbert.embedding line 22
  3. theorem OAI.FiniteEntropySeparation.LabelHilbert.embedding_single line 25
  4. def OAI.FiniteEntropySeparation.FreeTensor.signalSlice line 33
  5. theorem OAI.FiniteEntropySeparation.FreeTensor.signalSlice_single line 38
  6. theorem OAI.FiniteEntropySeparation.FreeTensor.signalSlice_basis line 45
  7. theorem OAI.FiniteEntropySeparation.FreeTensor.signalSlice_semicircular line 50
  8. theorem OAI.FiniteEntropySeparation.FreeTensor.signalSlice_word line 67
  9. theorem OAI.FiniteEntropySeparation.FreeTensor.signalSlice_vacuum_coefficient line 82
  10. theorem OAI.FiniteEntropySeparation.FreeTensor.tensor_word_moment line 96
  11. theorem OAI.FiniteEntropySeparation.FreeTensor.trace_semicircularB_pow line 109
  12. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_commutes_creationB line 115
  13. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_commutes_semicircularB line 121