OAI/Geometry/WeakHessian/Transport/PerturbedAction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.FormActionBound.symmetric_contraction_error line 23
  2. lemma OAI.WeakHessian.integral_gradient_le_regularized line 49
  3. lemma OAI.WeakHessian.cheegerHeat_diagonal_entropy_test_error line 60