OAI/Probability/FreeIsing/Posterior/PathPosteriorResponse.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.PathPosterior.interaction line 12
  2. def OAI.Problem367.PathPosterior.spin line 15
  3. def OAI.Problem367.PathPosterior.childFields line 18
  4. theorem OAI.Problem367.PathPosterior.childFields_fin line 21
  5. theorem OAI.Problem367.PathPosterior.energy_eq_fieldEnergy line 26
  6. theorem OAI.Problem367.PathPosterior.mean_eq_fieldMean line 35
  7. def OAI.Problem367.PathPosterior.rootMean line 51
  8. def OAI.Problem367.PathPosterior.rootField line 54
  9. theorem OAI.Problem367.PathPosterior.rootMean_eq_tanh line 57
  10. theorem OAI.Problem367.PathPosterior.rootMean_mem_Ioo line 62
  11. theorem OAI.Problem367.PathPosterior.rootField_eq line 67
  12. theorem OAI.Problem367.PathPosterior.endpoint_covariance line 71
  13. theorem OAI.Problem367.PathPosterior.hasDerivAt_rootMean_endpoint line 82
  14. theorem OAI.Problem367.PathPosterior.hasDerivAt_rootField_endpoint line 99
  15. theorem OAI.Problem367.PathPosterior.hasDerivAt_rootField_endpoint_at line 121
  16. theorem OAI.Problem367.PathPosterior.response_mem_Icc line 140
  17. theorem OAI.Problem367.PathPosterior.lipschitzWith_rootField_endpoint line 158