OAI/Probability/GaussianReplacement/Tilt.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentProjection.compProd_withDensity_fst line 14
  2. def OAI.CurrentProjection.reciprocalKernelScale line 39
  3. lemma OAI.CurrentProjection.measurable_reciprocalKernelScale line 43
  4. lemma OAI.CurrentProjection.reciprocal_kernel_projection_moment line 47
  5. def OAI.CurrentProjection.negativeLogAbs line 132
  6. lemma OAI.CurrentProjection.measurable_negativeLogAbs line 134
  7. lemma OAI.CurrentProjection.negativeLogAbs_nonneg line 138
  8. lemma OAI.CurrentProjection.integrable_negativeLogAbs_gaussian line 140
  9. def OAI.CurrentProjection.regularizedCauchyCross line 169
  10. lemma OAI.CurrentProjection.regularizedCauchyCross_upper line 173
  11. lemma OAI.CurrentProjection.regularizedCauchyCross_lower line 214
  12. lemma OAI.CurrentProjection.log_regularizedCauchyPDF line 226
  13. abbrev OAI.CurrentProjection.standardNormalPair line 243
  14. def OAI.CurrentProjection.cauchyTiltConstant line 245
  15. lemma OAI.CurrentProjection.integrable_standardNormal_square line 248
  16. lemma OAI.CurrentProjection.integral_standardNormal_square line 251
  17. lemma OAI.CurrentProjection.integrable_regularizedCauchyCross line 256
  18. lemma OAI.CurrentProjection.integral_regularizedCauchyCross line 275
  19. lemma OAI.CurrentProjection.cauchyTiltConstant_pos line 309
  20. lemma OAI.CurrentProjection.gaussian_inner_map_scaled line 323
  21. lemma OAI.CurrentProjection.gaussian_pair_inner_map_scaled line 340
  22. lemma OAI.CurrentProjection.gaussian_regularizedCross_integrable line 349
  23. lemma OAI.CurrentProjection.gaussian_regularizedCross_integral line 365