OAI/Probability/GaussianReplacement/CriticalEntropy.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.criticalRefinement line 13
  2. lemma OAI.CurrentProjection.measurable_criticalRefinement line 18
  3. lemma OAI.CurrentProjection.posterior_sphere_growth line 27
  4. lemma OAI.CurrentProjection.criticalRefinement_size line 38
  5. lemma OAI.CurrentProjection.criticalRefinement_entropy line 76
  6. lemma OAI.CurrentProjection.llr_chain_ae line 119
  7. lemma OAI.CurrentProjection.density_log_integrable_and_gibbs line 132
  8. lemma OAI.CurrentProjection.klDiv_chain_finite line 152
  9. lemma OAI.CurrentProjection.density_gibbs_integrable line 163
  10. lemma OAI.CurrentProjection.cross_llr_integrable line 196
  11. lemma OAI.CurrentProjection.llr_of_two_densities line 215
  12. lemma OAI.CurrentProjection.volume_ae_exactDensity_rnDeriv line 244
  13. lemma OAI.CurrentProjection.labelLaw_withDensity_exact line 257
  14. lemma OAI.CurrentProjection.map_fiber_withDensity line 263
  15. def OAI.CurrentProjection.projectionJoint line 284
  16. lemma OAI.CurrentProjection.projectionJoint_withDensity line 288
  17. lemma OAI.CurrentProjection.gaussian_inner_sq_integrable line 298
  18. lemma OAI.CurrentProjection.gaussian_inner_sq_integral line 302
  19. def OAI.CurrentProjection.projectionSquare line 308
  20. lemma OAI.CurrentProjection.projectionSquare_nonneg line 310
  21. lemma OAI.CurrentProjection.projectionSquare_integrable line 313
  22. lemma OAI.CurrentProjection.projectionSquare_integral line 319
  23. def OAI.CurrentProjection.normalizer line 327
  24. def OAI.CurrentProjection.radiusVariance line 329
  25. lemma OAI.CurrentProjection.radiusVariance_ne_zero line 331
  26. def OAI.CurrentProjection.gaussianProductPDF line 336
  27. lemma OAI.CurrentProjection.gaussianProductPDF_pos line 339
  28. lemma OAI.CurrentProjection.measurable_gaussianProductPDF line 345
  29. lemma OAI.CurrentProjection.integrable_gaussianProductPDF line 350
  30. lemma OAI.CurrentProjection.integral_gaussianProductPDF line 354
  31. lemma OAI.CurrentProjection.normalizer_pos line 361
  32. lemma OAI.CurrentProjection.log_gaussianProductPDF line 365
  33. lemma OAI.CurrentProjection.log_normalizer_le line 377
  34. def OAI.CurrentProjection.coverPDF line 390
  35. lemma OAI.CurrentProjection.coverPDF_pos line 393
  36. lemma OAI.CurrentProjection.measurable_coverPDF line 398
  37. lemma OAI.CurrentProjection.integral_coverPDF line 415
  38. lemma OAI.CurrentProjection.integrable_coverPDF line 424
  39. lemma OAI.CurrentProjection.lintegral_coverPDF line 428
  40. lemma OAI.CurrentProjection.gaussianProductPDF_le_exp line 434
  41. lemma OAI.CurrentProjection.log_coverPDF_upper line 440
  42. lemma OAI.CurrentProjection.neg_log_coverPDF_le line 452
  43. lemma OAI.CurrentProjection.projectionSquare_joint_integrable line 472
  44. lemma OAI.CurrentProjection.log_coverPDF_integrable_rows line 497
  45. lemma OAI.CurrentProjection.log_coverPDF_joint_integrable line 508
  46. lemma OAI.CurrentProjection.integral_neg_log_coverPDF_rows_le line 520
  47. lemma OAI.CurrentProjection.integral_neg_log_coverPDF_le line 540
  48. instance OAI.CurrentProjection.projectionJoint_probability line 557
  49. lemma OAI.CurrentProjection.projection_cover_entropy line 564