OAI/Analysis/FreeEntropy/SpectralTestFunctions.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.univariateMoment line 10
  2. def OAI.FiniteEntropySeparation.commutatorMoment line 12
  3. theorem OAI.FiniteEntropySeparation.univariateMoment_continuous line 14
  4. theorem OAI.FiniteEntropySeparation.commutatorMoment_continuous line 17
  5. theorem OAI.FiniteEntropySeparation.univariateMoment_matrix line 20
  6. theorem OAI.FiniteEntropySeparation.commutatorMoment_matrix line 23
  7. theorem OAI.FiniteEntropySeparation.matrixMoment_second_hs line 40
  8. theorem OAI.FiniteEntropySeparation.matrixMoment_fourth_trace line 44
  9. theorem OAI.FiniteEntropySeparation.continuous_tuple_wordMoments line 53
  10. theorem OAI.FiniteEntropySeparation.univariateMoment_word line 58
  11. theorem OAI.FiniteEntropySeparation.commutatorMoment_word_zero line 61
  12. theorem OAI.FiniteEntropySeparation.Model.continuous_X line 69
  13. theorem OAI.FiniteEntropySeparation.Model.continuous_X_moments line 74
  14. theorem OAI.FiniteEntropySeparation.Model.X_zero line 76
  15. theorem OAI.FiniteEntropySeparation.Model.C_second line 77
  16. theorem OAI.FiniteEntropySeparation.Model.C_fourth line 80
  17. theorem OAI.FiniteEntropySeparation.Model.C_commutator line 83
  18. theorem OAI.FiniteEntropySeparation.Model.C_univariateMoment line 87