OAI/Probability/PosteriorReplicas/Gaussian/GaussianLogMoment.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PosteriorReplicas.log_le_square_tangent line 13
  2. lemma OAI.PosteriorReplicas.norm_gramSchmidt_le_norm line 21
  3. def OAI.PosteriorReplicas.gramVolume line 28
  4. lemma OAI.PosteriorReplicas.gramVolume_eq_prod line 31
  5. lemma OAI.PosteriorReplicas.measurable_gramVolume line 35
  6. lemma OAI.PosteriorReplicas.gramVolume_pos line 40
  7. lemma OAI.PosteriorReplicas.log_gramVolume_eq_sum line 45
  8. lemma OAI.PosteriorReplicas.log_gramVolume_le_tangent line 49
  9. lemma OAI.PosteriorReplicas.abs_log_gramVolume_le line 60
  10. lemma OAI.PosteriorReplicas.gaussian_integrable_norm_sq line 74
  11. lemma OAI.PosteriorReplicas.gaussian_integral_norm_sq line 77
  12. lemma OAI.PosteriorReplicas.gaussianPi_integrable_norm_sq line 104
  13. lemma OAI.PosteriorReplicas.gaussianPi_integral_norm_sq line 109
  14. lemma OAI.PosteriorReplicas.gaussian_integrable_inv_gramVolume line 118
  15. lemma OAI.PosteriorReplicas.gaussian_integrable_log_gramVolume line 130
  16. lemma OAI.PosteriorReplicas.gaussian_integral_log_gramVolume_le line 141