OAI/Probability/SKGap/Posterior/History.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKGap.GaussianHistory.History line 13
  2. instance OAI.SKGap.GaussianHistory.historyMeasurable line 17
  3. instance OAI.SKGap.GaussianHistory.historyTopology line 24
  4. instance OAI.SKGap.GaussianHistory.historySecondCountable line 31
  5. instance OAI.SKGap.GaussianHistory.historyBorel line 38
  6. def OAI.SKGap.GaussianHistory.reference line 45
  7. instance OAI.SKGap.GaussianHistory.reference_probability line 49
  8. def OAI.SKGap.GaussianHistory.likelihood line 56
  9. lemma OAI.SKGap.GaussianHistory.likelihood_pos line 60
  10. lemma OAI.SKGap.GaussianHistory.continuous_likelihood line 65
  11. lemma OAI.SKGap.GaussianHistory.integrable_likelihood line 71
  12. lemma OAI.SKGap.GaussianHistory.integral_likelihood line 78
  13. def OAI.SKGap.GaussianHistory.density line 88
  14. lemma OAI.SKGap.GaussianHistory.density_pos line 91
  15. lemma OAI.SKGap.GaussianHistory.continuous_density line 102
  16. lemma OAI.SKGap.GaussianHistory.integrable_density line 105
  17. lemma OAI.SKGap.GaussianHistory.integral_density line 109
  18. def OAI.SKGap.GaussianHistory.posterior line 116
  19. lemma OAI.SKGap.GaussianHistory.density_zero line 121
  20. lemma OAI.SKGap.GaussianHistory.posterior_zero line 124
  21. lemma OAI.SKGap.GaussianHistory.density_succ line 130
  22. lemma OAI.SKGap.GaussianHistory.posterior_succ line 139
  23. lemma OAI.SKGap.GaussianHistory.posterior_avg_weight line 149
  24. lemma OAI.SKGap.GaussianHistory.integrable_posterior_avg_weight line 156
  25. lemma OAI.SKGap.GaussianHistory.integral_posterior_avg_weight line 161
  26. lemma OAI.SKGap.GaussianHistory.density_le line 168
  27. lemma OAI.SKGap.GaussianHistory.exists_domination line 175
  28. def OAI.SKGap.GaussianHistory.relativeEntropyIntegrand line 184
  29. def OAI.SKGap.GaussianHistory.divergenceIntegrand line 187
  30. lemma OAI.SKGap.GaussianHistory.divergenceIntegrand_eq line 190
  31. lemma OAI.SKGap.GaussianHistory.divergenceIntegrand_nonneg line 197
  32. lemma OAI.SKGap.GaussianHistory.continuous_log_ratio line 203
  33. lemma OAI.SKGap.GaussianHistory.continuous_relativeEntropyIntegrand line 209
  34. lemma OAI.SKGap.GaussianHistory.continuous_divergenceIntegrand line 213
  35. lemma OAI.SKGap.GaussianHistory.integrable_divergenceIntegrand line 218
  36. lemma OAI.SKGap.GaussianHistory.integrable_relativeEntropyIntegrand line 232
  37. def OAI.SKGap.GaussianHistory.entropy line 241
  38. lemma OAI.SKGap.GaussianHistory.entropy_eq_divergence line 244
  39. lemma OAI.SKGap.GaussianHistory.entropy_nonneg line 257
  40. lemma OAI.SKGap.GaussianHistory.entropy_zero line 262
  41. lemma OAI.SKGap.GaussianHistory.integrable_lift line 266
  42. lemma OAI.SKGap.GaussianHistory.integral_lift line 293
  43. lemma OAI.SKGap.GaussianHistory.relativeEntropy_succ line 304
  44. theorem OAI.SKGap.GaussianHistory.entropy_succ line 317
  45. def OAI.SKGap.GaussianHistory.law line 349
  46. lemma OAI.SKGap.GaussianHistory.law_probability line 352
  47. lemma OAI.SKGap.GaussianHistory.integral_law line 359
  48. lemma OAI.SKGap.GaussianHistory.integrable_law_iff line 366
  49. def OAI.SKGap.GaussianHistory.eventProbability line 373
  50. lemma OAI.SKGap.GaussianHistory.eventProbability_nonneg line 376
  51. lemma OAI.SKGap.GaussianHistory.eventProbability_eq line 379
  52. lemma OAI.SKGap.GaussianHistory.scalar_entropy_fenchel line 385
  53. theorem OAI.SKGap.GaussianHistory.entropy_event_bound line 394