OAI/Probability/SpanningForest/FinitePosterior.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.FinitePosterior.mixtureDensity line 14
  2. lemma OAI.Problem336.FinitePosterior.measurable_mixtureDensity line 18
  3. theorem OAI.Problem336.FinitePosterior.marginal_eq_withDensity line 23
  4. lemma OAI.Problem336.FinitePosterior.mixtureDensity_ne_top line 43
  5. lemma OAI.Problem336.FinitePosterior.mixtureDensity_ne_zero_of_positive line 51
  6. lemma OAI.Problem336.FinitePosterior.mixtureDensity_toReal line 62
  7. theorem OAI.Problem336.FinitePosterior.likelihood_rnDeriv_marginal line 70
  8. theorem OAI.Problem336.FinitePosterior.posterior_singleton_formula line 89
  9. theorem OAI.Problem336.FinitePosterior.posterior_mean_formula line 111
  10. theorem OAI.Problem336.FinitePosterior.condExp_eq_posterior_mean line 129
  11. theorem OAI.Problem336.FinitePosterior.condExp_eq_likelihood_ratio line 146
  12. theorem OAI.Problem336.FinitePosterior.condExp_eq_posterior_mean_of_jointLaw line 163
  13. theorem OAI.Problem336.FinitePosterior.condExp_eq_likelihood_ratio_of_jointLaw line 194