OAI/Probability/SKBarriers/Replicas/MatrixGuerraKernel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.matrixInner line 15
  2. def OAI.SK.Analytic.matrixSquare line 17
  3. theorem OAI.SK.Analytic.matrixSquare_sub line 19
  4. theorem OAI.SK.Analytic.matrixSquare_nonneg line 28
  5. theorem OAI.SK.Analytic.matrixCovariance_lower line 31
  6. def OAI.SK.Analytic.factorPath line 37
  7. theorem OAI.SK.Analytic.factorPath_last line 41
  8. theorem OAI.SK.Analytic.factorPath_inner line 45
  9. def OAI.SK.Analytic.matrixHamiltonianObservables line 64
  10. def OAI.SK.Analytic.matrixFieldObservables line 67
  11. theorem OAI.SK.Analytic.matrixHamiltonianObservables_covariance line 72
  12. theorem OAI.SK.Analytic.matrixFieldObservables_covariance line 81
  13. theorem OAI.SK.Analytic.matrixFieldObservables_prefix line 91
  14. theorem OAI.SK.Analytic.matrixFiniteInterpolation line 102