OAI/Analysis/FreeEntropy/SignalCovariance.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEntropySeparation.FreeSeries.cumulants_one line 13
  2. theorem OAI.FiniteEntropySeparation.FreeSeries.cumulants_two line 17
  3. theorem OAI.FiniteEntropySeparation.FreeSeries.residual_short line 24
  4. theorem OAI.FiniteEntropySeparation.FreeSeries.residual_long line 33
  5. def OAI.FiniteEntropySeparation.Model.variance line 45
  6. theorem OAI.FiniteEntropySeparation.Model.variance_nonneg line 46
  7. theorem OAI.FiniteEntropySeparation.Model.fockMoments_one line 49
  8. theorem OAI.FiniteEntropySeparation.Model.fockMoments_two line 54
  9. theorem OAI.FiniteEntropySeparation.Model.C_centered line 59
  10. theorem OAI.FiniteEntropySeparation.Model.C_offDiagonal line 67
  11. theorem OAI.FiniteEntropySeparation.Model.C_covariance line 84
  12. theorem OAI.FiniteEntropySeparation.Model.signalCumulants_centered line 92
  13. theorem OAI.FiniteEntropySeparation.Model.signalCumulants_covariance line 95
  14. theorem OAI.FiniteEntropySeparation.Model.variance_last_le_one line 98
  15. theorem OAI.FiniteEntropySeparation.Model.variance_castSucc line 105
  16. theorem OAI.FiniteEntropySeparation.Model.variance_le_one line 113