OAI/Probability/DirectionalWalk/PosteriorTails.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.posteriorSup line 12
  2. lemma OAI.DirectionalZeroOne.posteriorSup_bounds line 15
  3. lemma OAI.DirectionalZeroOne.posteriorMax_tendsto line 23
  4. lemma OAI.DirectionalZeroOne.measurable_posteriorSup line 29
  5. lemma OAI.DirectionalZeroOne.posteriorSup_exponential line 34
  6. def OAI.DirectionalZeroOne.goodPosteriorSet line 59
  7. def OAI.DirectionalZeroOne.clippedPosterior line 62
  8. lemma OAI.DirectionalZeroOne.measurableSet_goodPosterior line 65
  9. lemma OAI.DirectionalZeroOne.clippedPosterior_bounds line 76
  10. lemma OAI.DirectionalZeroOne.clippedPosterior_ae_eq line 88
  11. lemma OAI.DirectionalZeroOne.clippedPosterior_martingale line 95
  12. lemma OAI.DirectionalZeroOne.posteriorSup_congr_ae line 105
  13. def OAI.DirectionalZeroOne.posteriorLevel line 119
  14. lemma OAI.DirectionalZeroOne.posteriorLevel_dyadic line 121
  15. lemma OAI.DirectionalZeroOne.posteriorLevel_scale line 135
  16. def OAI.DirectionalZeroOne.posteriorExponent line 147
  17. lemma OAI.DirectionalZeroOne.posteriorExponent_pos line 149
  18. lemma OAI.DirectionalZeroOne.posteriorExponent_le line 152
  19. lemma OAI.DirectionalZeroOne.setIntegral_entropy_of_exp line 164
  20. lemma OAI.DirectionalZeroOne.posteriorSup_exponential_log line 199
  21. lemma OAI.DirectionalZeroOne.posteriorSup_exponential_log_ae line 219
  22. lemma OAI.DirectionalZeroOne.integrable_posteriorSup_ae line 235
  23. lemma OAI.DirectionalZeroOne.integrable_posteriorSup_exp_ae line 246
  24. lemma OAI.DirectionalZeroOne.posteriorSup_joint_event_weight line 259
  25. lemma OAI.DirectionalZeroOne.ae_atom_pos line 288