OAI/Probability/GaussianReplacement/Reference.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentProjection.sphere_own_density_moment line 15
  2. lemma OAI.CurrentProjection.sphere_moment_log_bound line 41
  3. lemma OAI.CurrentProjection.sphere_label_entropy_finite line 63
  4. def OAI.CurrentProjection.conditionalReferenceKL line 105
  5. lemma OAI.CurrentProjection.conditionalReferenceKL_chain line 108
  6. lemma OAI.CurrentProjection.conditionalReferenceKL_add_condition line 130
  7. lemma OAI.CurrentProjection.conditionalMutualInformation_symm line 158
  8. lemma OAI.CurrentProjection.conditionalReferenceKL_finite_condition line 188
  9. def OAI.CurrentProjection.gaussianLabels line 214
  10. instance OAI.CurrentProjection.gaussianLabels_probability line 216
  11. lemma OAI.CurrentProjection.gaussianLabels_density line 220
  12. lemma OAI.CurrentProjection.log_gaussianLabelsPDF line 242
  13. lemma OAI.CurrentProjection.projectionSquare_sphere_joint_integrable line 247
  14. lemma OAI.CurrentProjection.projectionSquare_sphere_joint_integral line 265
  15. lemma OAI.CurrentProjection.gaussian_log_reference_projection line 273
  16. lemma OAI.CurrentProjection.sphere_projection_reference_finite line 299
  17. lemma OAI.CurrentProjection.weighted_log_integral line 343
  18. def OAI.CurrentProjection.regularizedReciprocal line 379
  19. def OAI.CurrentProjection.regularizedScale line 382
  20. lemma OAI.CurrentProjection.sphere_subtype_dist_le_two line 385
  21. lemma OAI.CurrentProjection.regularizedReciprocal_pos line 389
  22. lemma OAI.CurrentProjection.regularizedReciprocal_bounds line 392
  23. lemma OAI.CurrentProjection.integrable_regularizedReciprocal line 401
  24. lemma OAI.CurrentProjection.regularizedScale_bounds line 409
  25. lemma OAI.CurrentProjection.log_regularizedReciprocal line 419