OAI/Geometry/WeakHessian/Entropy/TruncatedLog.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessian.truncatedLog line 47
  2. lemma OAI.WeakHessian.truncatedLog_hasDeriv line 49
  3. lemma OAI.WeakHessian.truncatedLog_deriv line 56
  4. lemma OAI.WeakHessian.truncatedLog_contDiff line 59
  5. lemma OAI.WeakHessian.truncatedLog_deriv_bound line 65
  6. lemma OAI.WeakHessian.truncatedLog_lipschitz line 70
  7. lemma OAI.WeakHessian.truncatedLog_eq line 77
  8. def OAI.WeakHessian.regularizedLog line 102
  9. def OAI.WeakHessian.regularizedEntropy line 103
  10. lemma OAI.WeakHessian.regularizedLog_zero line 105
  11. lemma OAI.WeakHessian.regularizedEntropy_zero line 107
  12. lemma OAI.WeakHessian.regularizedLog_contDiff line 109
  13. lemma OAI.WeakHessian.regularizedLog_hasDeriv line 111
  14. lemma OAI.WeakHessian.regularizedLog_deriv line 115
  15. lemma OAI.WeakHessian.regularizedLog_lipschitz line 117
  16. lemma OAI.WeakHessian.regularizedLog_eq line 123
  17. lemma OAI.WeakHessian.regularizedLog_deriv_bound line 126
  18. lemma OAI.WeakHessian.regularizedEntropy_hasDeriv line 131
  19. lemma OAI.WeakHessian.regularizedEntropy_eq line 137
  20. lemma OAI.WeakHessian.regularizedLog_memLp line 157
  21. lemma OAI.WeakHessian.regularizedEntropy_hasFDeriv line 161