OAI/Geometry/WeakHessian/Entropy/FisherRoot.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessian.regularizedRoot line 17
  2. lemma OAI.WeakHessian.regularizedRoot_hasDeriv line 19
  3. lemma OAI.WeakHessian.regularizedRoot_deriv line 27
  4. lemma OAI.WeakHessian.regularizedRoot_contDiff line 31
  5. lemma OAI.WeakHessian.regularizedRoot_zero line 38
  6. lemma OAI.WeakHessian.regularizedRoot_deriv_bound line 40
  7. lemma OAI.WeakHessian.regularizedRoot_lipschitz line 46
  8. lemma OAI.WeakHessian.regularizedRoot_eq line 52
  9. lemma OAI.WeakHessian.regularizedRoot_bounds line 65
  10. lemma OAI.WeakHessian.regularizedRoot_tendsto line 77
  11. lemma OAI.WeakHessian.Sobolev.sqrt_of_fisher line 87