OAI/Probability/SKGap/Matrix/NormalLogConst.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.normalLogConst line 26
  2. def OAI.SKGap.normalLogDensity line 28
  3. lemma OAI.SKGap.exp_normalLogDensity line 30
  4. lemma OAI.SKGap.continuousOn_normalLogConst line 43
  5. lemma OAI.SKGap.normalLogDensity_sub_le line 56
  6. lemma OAI.SKGap.normalLogDensity_sum_sub_le line 73
  7. def OAI.SKGap.productNormal line 93
  8. lemma OAI.SKGap.productNormal_eq_exp line 95
  9. lemma OAI.SKGap.productNormal_nonneg line 103
  10. lemma OAI.SKGap.integrable_tiltedNormal line 106
  11. lemma OAI.SKGap.integral_tiltedNormal line 116
  12. lemma OAI.SKGap.tiltedNormal_mass_pos line 121
  13. lemma OAI.SKGap.product_tiltedNormal_integral line 130
  14. lemma OAI.SKGap.product_tiltedNormal_integrable line 141
  15. def OAI.SKGap.normalDensityError line 150
  16. lemma OAI.SKGap.normalDensityError_self line 154
  17. lemma OAI.SKGap.continuous_normalDensityError line 157
  18. theorem OAI.SKGap.finite_gaussian_test_cover line 167