OAI/Probability/FreeIsing/Posterior/GaussianEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.FinitePosterior.integral_fieldSquareGradient_mul_noise line 15
  2. def OAI.Problem367.FinitePosterior.finiteStandardObservation line 43
  3. lemma OAI.Problem367.FinitePosterior.measurable_finiteStandardObservation line 47
  4. theorem OAI.Problem367.FinitePosterior.integrable_bounded_test line 54
  5. theorem OAI.Problem367.FinitePosterior.integrable_finiteStandardNoise line 65
  6. theorem OAI.Problem367.FinitePosterior.integrable_finiteStandardGradient line 72
  7. theorem OAI.Problem367.FinitePosterior.integrable_finiteStandardHessian line 84
  8. theorem OAI.Problem367.FinitePosterior.integrable_finiteStandardGradient_mul_noise line 97
  9. theorem OAI.Problem367.FinitePosterior.integral_finiteStandardGradient_mul_noise line 112
  10. theorem OAI.Problem367.FinitePosterior.hasDerivAt_finiteStandardEnergy_of_posterior_test line 131
  11. theorem OAI.Problem367.FinitePosterior.hasDerivAt_finiteStandardEnergy line 218