OAI/Geometry/WeakHessian/Entropy/FiniteEntropy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessian.FiniteEntropy line 49
  2. def OAI.WeakHessian.entropyReal line 52
  3. lemma OAI.WeakHessian.entropyReal_eq_integral_density line 54
  4. lemma OAI.WeakHessian.absolutelyContinuous_exponentialMeasure line 59
  5. lemma OAI.WeakHessian.llr_exponentialMeasure line 67
  6. lemma OAI.WeakHessian.finiteEntropy_exponentialMeasure_iff line 87
  7. theorem OAI.WeakHessian.entropyReal_exponentialMeasure line 103
  8. lemma OAI.WeakHessian.llr_restrict_self line 109
  9. lemma OAI.WeakHessian.llr_normalizedRestriction line 116
  10. theorem OAI.WeakHessian.normalizedRestriction_finiteEntropy line 129
  11. theorem OAI.WeakHessian.entropyReal_normalizedRestriction line 136
  12. lemma OAI.WeakHessian.absolutelyContinuous_restrict_of_ae_mem line 143
  13. lemma OAI.WeakHessian.llr_restrict_right_of_ae_mem line 147
  14. theorem OAI.WeakHessian.entropyReal_lower_bound line 158