OAI/Probability/ThreeState/PoissonBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Poisson posterior projection and entropy bounds.

  1. def OAI.ThreeState.offspringPosterior line 13
  2. lemma OAI.ThreeState.integral_offspringPosterior line 17
  3. lemma OAI.ThreeState.posteriorMu_le_one line 27
  4. lemma OAI.ThreeState.posteriorNu_le_one line 31
  5. lemma OAI.ThreeState.posteriorMu_offspring line 36
  6. lemma OAI.ThreeState.posteriorNu_offspring line 41
  7. lemma OAI.ThreeState.pairCorrelation_offspring line 47
  8. lemma OAI.ThreeState.poisson_projection_quadratic line 52
  9. lemma OAI.ThreeState.poisson_projection line 73
  10. lemma OAI.ThreeState.poissonAverage_eq_mean line 102
  11. lemma OAI.ThreeState.poissonAverage_zero line 111
  12. lemma OAI.ThreeState.poissonAverage_monotoneOn line 118
  13. lemma OAI.ThreeState.poisson_nu_le_fixedpoint line 134
  14. lemma OAI.ThreeState.poisson_correlation_hasDerivAt line 153
  15. lemma OAI.ThreeState.poisson_increment_bound line 177
  16. lemma OAI.ThreeState.poisson_correlation_bound line 210
  17. lemma OAI.ThreeState.poisson_entropy_bound line 233