OAI/Probability/ThreeState/PoissonCritical.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Informative posterior mass and positive critical Poisson non-reconstruction.

  1. lemma OAI.ThreeState.normalizer_uninformative line 12
  2. lemma OAI.ThreeState.combineMessage_uninformative line 16
  3. lemma OAI.ThreeState.degreeOutput_atom line 23
  4. lemma OAI.ThreeState.densityEvolution_real line 36
  5. lemma OAI.ThreeState.poisson_power_mean line 46
  6. def OAI.ThreeState.informativeMass line 61
  7. lemma OAI.ThreeState.informativeMass_nonneg line 64
  8. lemma OAI.ThreeState.informativeMass_le_one line 67
  9. lemma OAI.ThreeState.poisson_informative_recursion line 72
  10. lemma OAI.ThreeState.integral_real_cauchy line 105
  11. lemma OAI.ThreeState.messageX_uninformative line 121
  12. lemma OAI.ThreeState.posteriorMu_sq_le_informative line 124
  13. lemma OAI.ThreeState.informativeMass_pos_of_mu_pos line 153
  14. lemma OAI.ThreeState.poisson_positive_critical_uniform line 166
  15. theorem OAI.ThreeState.poisson_positive_critical_nonreconstruction line 199