OAI/Probability/GaussianInformation/Kernel/GaussianReference.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ReferenceGaussian.Mat line 15
  2. abbrev OAI.ReferenceGaussian.Vec line 16
  3. def OAI.ReferenceGaussian.applyRows line 17
  4. lemma OAI.ReferenceGaussian.applyRows_sub line 20
  5. lemma OAI.ReferenceGaussian.continuous_applyRows line 25
  6. def OAI.ReferenceGaussian.atDensity line 30
  7. lemma OAI.ReferenceGaussian.atDensity_pos line 33
  8. lemma OAI.ReferenceGaussian.continuous_atDensity line 36
  9. lemma OAI.ReferenceGaussian.continuous_log_atDensity line 41
  10. def OAI.ReferenceGaussian.densityBound line 45
  11. lemma OAI.ReferenceGaussian.densityBound_pos line 46
  12. lemma OAI.ReferenceGaussian.atDensity_le line 49
  13. lemma OAI.ReferenceGaussian.integrable_atDensity line 65
  14. lemma OAI.ReferenceGaussian.integral_atDensity_pos line 76
  15. lemma OAI.ReferenceGaussian.integral_density_y line 86
  16. lemma OAI.ReferenceGaussian.lintegral_density_y line 99
  17. def OAI.ReferenceGaussian.mixture line 106
  18. lemma OAI.ReferenceGaussian.measurable_mixture line 110
  19. lemma OAI.ReferenceGaussian.mixture_nonneg line 118
  20. lemma OAI.ReferenceGaussian.mixture_lower line 125
  21. lemma OAI.ReferenceGaussian.mixture_pos line 133
  22. lemma OAI.ReferenceGaussian.lintegral_mixture line 139