OAI/Probability/SKGap/Localization/DivergenceIntegrand.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.GaussianStep.var_eq line 12
  2. lemma OAI.SKGap.GaussianStep.var_le_square line 17
  3. lemma OAI.SKGap.GaussianStep.l1_square_le_avg_square line 20
  4. lemma OAI.SKGap.GaussianStep.centered_l1_bound line 35
  5. lemma OAI.SKGap.GaussianStep.posterior_avg_weight line 39
  6. lemma OAI.SKGap.GaussianStep.integrable_posterior_avg_weight line 48
  7. lemma OAI.SKGap.GaussianStep.integral_posterior_avg_weight line 53
  8. lemma OAI.SKGap.GaussianStep.posterior_variance_identity line 60
  9. lemma OAI.SKGap.GaussianStep.integrable_posterior_variance_weight line 71
  10. lemma OAI.SKGap.GaussianStep.integral_posterior_variance line 76
  11. theorem OAI.SKGap.GaussianStep.variance_step_bound line 84
  12. lemma OAI.SKGap.GaussianStep.scalar_entropy_nonneg line 95
  13. lemma OAI.SKGap.GaussianStep.scalar_entropy_le_square line 100
  14. def OAI.SKGap.GaussianStep.divergenceIntegrand line 104
  15. lemma OAI.SKGap.GaussianStep.divergenceIntegrand_eq line 107
  16. lemma OAI.SKGap.GaussianStep.divergenceIntegrand_nonneg line 114
  17. lemma OAI.SKGap.GaussianStep.density_sub line 120
  18. lemma OAI.SKGap.GaussianStep.divergenceIntegrand_le_quadratic line 124
  19. lemma OAI.SKGap.GaussianStep.continuous_divergenceIntegrand line 134
  20. lemma OAI.SKGap.GaussianStep.integrable_divergenceIntegrand line 142
  21. lemma OAI.SKGap.GaussianStep.prior_sub_l1 line 150
  22. lemma OAI.SKGap.GaussianStep.prior_sub_sum line 156
  23. theorem OAI.SKGap.GaussianStep.entropy_step_bound line 159
  24. lemma OAI.SKGap.GaussianStep.integrable_relativeEntropy line 177
  25. lemma OAI.SKGap.GaussianStep.integral_relativeEntropy line 188
  26. def OAI.SKGap.GaussianStep.squarePrior line 199
  27. lemma OAI.SKGap.GaussianStep.squarePrior_density line 204
  28. lemma OAI.SKGap.GaussianStep.posterior_square_pos line 216
  29. lemma OAI.SKGap.GaussianStep.squarePrior_posterior line 223
  30. lemma OAI.SKGap.GaussianStep.avg_add line 235
  31. lemma OAI.SKGap.GaussianStep.avg_const_mul line 239
  32. lemma OAI.SKGap.GaussianStep.avg_nonneg line 243
  33. def OAI.SKGap.GaussianStep.cond line 246
  34. lemma OAI.SKGap.GaussianStep.cond_flip line 249
  35. lemma OAI.SKGap.GaussianStep.avg_flip line 253
  36. lemma OAI.SKGap.GaussianStep.conditional_orthogonal line 259
  37. lemma OAI.SKGap.GaussianStep.conditional_minimal line 273
  38. def OAI.SKGap.GaussianStep.energy line 285
  39. lemma OAI.SKGap.GaussianStep.energy_nonneg line 288
  40. lemma OAI.SKGap.GaussianStep.avg_sum line 291
  41. lemma OAI.SKGap.GaussianStep.posterior_mass_pos line 296
  42. lemma OAI.SKGap.GaussianStep.posterior_energy_bound line 300
  43. lemma OAI.SKGap.GaussianStep.continuous_posterior_mass line 308
  44. lemma OAI.SKGap.GaussianStep.continuous_posterior_cond line 313
  45. lemma OAI.SKGap.GaussianStep.continuous_posterior_energy line 323
  46. lemma OAI.SKGap.GaussianStep.integrable_posterior_energy_weight line 332
  47. theorem OAI.SKGap.GaussianStep.energy_step_bound line 342
  48. lemma OAI.SKGap.GaussianStep.gibbsPrior_avg line 357
  49. lemma OAI.SKGap.GaussianStep.gibbsPrior_var line 360
  50. lemma OAI.SKGap.GaussianStep.gibbsPrior_cond line 363
  51. lemma OAI.SKGap.GaussianStep.gibbsPrior_energy line 371