OAI/Probability/GaussianReplacement/Mixture.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentProjection.gaussianVectorPair line 13
  2. def OAI.CurrentProjection.sphereCauchyCross line 15
  3. def OAI.CurrentProjection.ownCauchyMixture line 18
  4. lemma OAI.CurrentProjection.continuous_sphereCauchyCross line 21
  5. lemma OAI.CurrentProjection.continuous_regularizedReciprocal line 26
  6. lemma OAI.CurrentProjection.sphereCauchyCross_lower line 32
  7. lemma OAI.CurrentProjection.sphereCauchyCross_norm_integral line 36
  8. lemma OAI.CurrentProjection.sphereCauchyCross_joint_integrable line 65
  9. lemma OAI.CurrentProjection.continuous_sphereCauchyCross_slice line 79
  10. lemma OAI.CurrentProjection.integrable_ownCauchyPDF line 86
  11. lemma OAI.CurrentProjection.ownCauchyMixture_pos line 98
  12. lemma OAI.CurrentProjection.ownCauchyMixture_cross_lower line 105
  13. lemma OAI.CurrentProjection.integrable_weighted_sphereCauchy line 117
  14. lemma OAI.CurrentProjection.ownCauchyMixture_cross_upper line 134
  15. lemma OAI.CurrentProjection.ownCauchyMixture_measurable line 164
  16. lemma OAI.CurrentProjection.ownCauchyMixture_cross_integrable line 171
  17. lemma OAI.CurrentProjection.weightedCauchyCross_integral_bound line 184
  18. lemma OAI.CurrentProjection.ownCauchyMixture_cross_integral line 218
  19. def OAI.CurrentProjection.regularizedCauchyPDF line 245
  20. lemma OAI.CurrentProjection.regularizedCauchyPDF_eq line 247
  21. lemma OAI.CurrentProjection.integrable_regularizedCauchyPDF line 271
  22. lemma OAI.CurrentProjection.integral_regularizedCauchyPDF line 278
  23. lemma OAI.CurrentProjection.lintegral_regularizedCauchyPDF line 286
  24. def OAI.CurrentProjection.cauchyMixture line 292
  25. lemma OAI.CurrentProjection.cauchyMixture_at_own line 296
  26. lemma OAI.CurrentProjection.cauchyMixture_integrand_integrable line 302
  27. lemma OAI.CurrentProjection.cauchyMixture_pos line 318
  28. lemma OAI.CurrentProjection.cauchyMixture_kernel_measurable line 324
  29. lemma OAI.CurrentProjection.cauchyMixture_normalization line 335
  30. lemma OAI.CurrentProjection.ownCauchyMixture_cross_norm_integral line 355
  31. lemma OAI.CurrentProjection.regularizedScale_kernel_measurable line 380
  32. lemma OAI.CurrentProjection.ownCauchyMixture_kernel_measurable line 389
  33. lemma OAI.CurrentProjection.ownCauchyMixture_context_integrable line 401
  34. lemma OAI.CurrentProjection.regularizedScale_context_log_integrable line 417
  35. lemma OAI.CurrentProjection.ownCauchyMixture_context_bound line 430
  36. lemma OAI.CurrentProjection.reference_gibbs line 448