OAI/Probability/FreeIsing/Gaussian/Likelihood.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.gaussianSignalLikelihood line 12
  2. theorem OAI.Problem367.gaussianPDFReal_signal line 15
  3. theorem OAI.Problem367.gaussianPDF_signal line 28
  4. theorem OAI.Problem367.gaussianReal_signal_withDensity line 35
  5. theorem OAI.Problem367.lintegral_pi_prod_of_measurable line 49
  6. theorem OAI.Problem367.pi_withDensity_of_probability line 64
  7. def OAI.Problem367.gaussianVectorLikelihood line 94
  8. theorem OAI.Problem367.prod_gaussianSignalLikelihood line 98
  9. theorem OAI.Problem367.gaussianPi_signal_withDensity line 109
  10. theorem OAI.Problem367.gaussianVectorLikelihood_of_sq_eq_one line 137
  11. theorem OAI.Problem367.gaussianPi_spin_withDensity line 147