OAI/Probability/StrongRayleigh/GaussianObservation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336AdditiveD139.GaussianObservation.gaussianPDFReal_binary_shift line 15
  2. theorem OAI.Problem336AdditiveD139.GaussianObservation.gaussianPDF_binary_shift line 31
  3. def OAI.Problem336AdditiveD139.GaussianObservation.likelihood line 37
  4. lemma OAI.Problem336AdditiveD139.GaussianObservation.likelihood_pos line 40
  5. lemma OAI.Problem336AdditiveD139.GaussianObservation.measurable_likelihood line 43
  6. theorem OAI.Problem336AdditiveD139.GaussianObservation.gaussianPDFReal_product_binary_shift line 48
  7. theorem OAI.Problem336AdditiveD139.GaussianObservation.gaussianReal_binary_shift line 56
  8. theorem OAI.Problem336AdditiveD139.GaussianObservation.pi_withDensity_ofReal line 67
  9. lemma OAI.Problem336AdditiveD139.GaussianObservation.integrable_binary_likelihood line 91
  10. theorem OAI.Problem336AdditiveD139.GaussianObservation.gaussianReal_pi_binary_shift line 101