OAI/Probability/SKRatio/Entropy/GaussianChannel.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Observation.Channel.reference line 13
  2. instance OAI.SKRatio.Observation.Channel.reference_probability line 16
  3. lemma OAI.SKRatio.Observation.Channel.integrable_exp_linear line 19
  4. lemma OAI.SKRatio.Observation.Channel.integral_exp_linear line 24
  5. def OAI.SKRatio.Observation.Channel.normSq line 36
  6. def OAI.SKRatio.Observation.Channel.mean line 38
  7. def OAI.SKRatio.Observation.Channel.secondMoment line 40
  8. def OAI.SKRatio.Observation.Channel.likelihood line 42
  9. def OAI.SKRatio.Observation.Channel.density line 45
  10. lemma OAI.SKRatio.Observation.Channel.likelihood_pos line 49
  11. lemma OAI.SKRatio.Observation.Channel.integrable_likelihood line 53
  12. lemma OAI.SKRatio.Observation.Channel.integral_likelihood line 63
  13. lemma OAI.SKRatio.Observation.Channel.density_jensen line 73
  14. lemma OAI.SKRatio.Observation.Channel.density_pos line 89
  15. lemma OAI.SKRatio.Observation.Channel.integrable_density line 92
  16. lemma OAI.SKRatio.Observation.Channel.integral_density line 96
  17. def OAI.SKRatio.Observation.Channel.interaction line 103
  18. lemma OAI.SKRatio.Observation.Channel.interaction_sum line 106
  19. lemma OAI.SKRatio.Observation.Channel.signed_sum_left line 117
  20. lemma OAI.SKRatio.Observation.Channel.signed_sum_right line 128
  21. lemma OAI.SKRatio.Observation.Channel.signed_sum_product line 135
  22. lemma OAI.SKRatio.Observation.Channel.signed_interaction line 140
  23. lemma OAI.SKRatio.Observation.Channel.interaction_remainder_bound line 160
  24. def OAI.SKRatio.Observation.Channel.pairShift line 170
  25. def OAI.SKRatio.Observation.Channel.pairKernel line 173
  26. lemma OAI.SKRatio.Observation.Channel.integrable_pairKernel line 176
  27. lemma OAI.SKRatio.Observation.Channel.integral_pairKernel line 184
  28. lemma OAI.SKRatio.Observation.Channel.likelihood_pair line 194
  29. def OAI.SKRatio.Observation.Channel.majorant line 204
  30. lemma OAI.SKRatio.Observation.Channel.majorant_eq_sum line 207
  31. lemma OAI.SKRatio.Observation.Channel.majorant_nonneg line 221
  32. lemma OAI.SKRatio.Observation.Channel.integrable_majorant line 224
  33. lemma OAI.SKRatio.Observation.Channel.integral_majorant line 231
  34. lemma OAI.SKRatio.Observation.Channel.interaction_exp_sum_bound line 241
  35. def OAI.SKRatio.Observation.Channel.quadraticIntegrand line 267
  36. lemma OAI.SKRatio.Observation.Channel.quadraticIntegrand_nonneg line 270
  37. lemma OAI.SKRatio.Observation.Channel.quadraticIntegrand_le_majorant line 273
  38. lemma OAI.SKRatio.Observation.Channel.continuous_likelihood line 283
  39. lemma OAI.SKRatio.Observation.Channel.continuous_density line 287
  40. lemma OAI.SKRatio.Observation.Channel.continuous_quadraticIntegrand line 291
  41. lemma OAI.SKRatio.Observation.Channel.integrable_quadraticIntegrand line 299
  42. theorem OAI.SKRatio.Observation.Channel.quadratic_bound line 306
  43. def OAI.SKRatio.Observation.Channel.posterior line 318
  44. lemma OAI.SKRatio.Observation.Channel.posterior_avg_weight line 326
  45. lemma OAI.SKRatio.Observation.Channel.integrable_posterior_avg_weight line 335
  46. lemma OAI.SKRatio.Observation.Channel.integral_posterior_avg_weight line 340
  47. lemma OAI.SKRatio.Observation.Channel.scalar_entropy_nonneg line 347
  48. lemma OAI.SKRatio.Observation.Channel.scalar_entropy_le_square line 352
  49. def OAI.SKRatio.Observation.Channel.divergenceIntegrand line 356
  50. lemma OAI.SKRatio.Observation.Channel.divergenceIntegrand_eq line 359
  51. lemma OAI.SKRatio.Observation.Channel.divergenceIntegrand_nonneg line 366
  52. lemma OAI.SKRatio.Observation.Channel.density_sub line 372
  53. lemma OAI.SKRatio.Observation.Channel.divergenceIntegrand_le_quadratic line 376
  54. lemma OAI.SKRatio.Observation.Channel.continuous_divergenceIntegrand line 386
  55. lemma OAI.SKRatio.Observation.Channel.integrable_divergenceIntegrand line 394
  56. lemma OAI.SKRatio.Observation.Channel.prior_sub_l1 line 402
  57. lemma OAI.SKRatio.Observation.Channel.prior_sub_sum line 408
  58. theorem OAI.SKRatio.Observation.Channel.entropy_step_bound line 411
  59. lemma OAI.SKRatio.Observation.Channel.integrable_relativeEntropy line 429
  60. lemma OAI.SKRatio.Observation.Channel.integral_relativeEntropy line 440
  61. lemma OAI.SKRatio.Observation.Channel.mean_abs_le line 451
  62. lemma OAI.SKRatio.Observation.Channel.normSq_nonneg line 461
  63. lemma OAI.SKRatio.Observation.Channel.normSq_le line 464
  64. lemma OAI.SKRatio.Observation.Channel.interaction_abs_le line 471
  65. theorem OAI.SKRatio.Observation.Channel.exists_interaction_bound line 497
  66. lemma OAI.SKRatio.Observation.Channel.reweight_density line 508
  67. lemma OAI.SKRatio.Observation.Channel.posterior_avg_eq_density_ratio line 518
  68. lemma OAI.SKRatio.Observation.Channel.posterior_entropy_identity line 524
  69. lemma OAI.SKRatio.Observation.Channel.integrable_posterior_entropy_weight line 537
  70. lemma OAI.SKRatio.Observation.Channel.integral_posterior_entropy line 544
  71. theorem OAI.SKRatio.Observation.Channel.entropy_retention line 561