OAI/Probability/SKBarriers/Hierarchy/RootCalculus.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.rootGradient line 16
  2. def OAI.SK.Analytic.rootHessian line 19
  3. def OAI.SK.Analytic.RootSpinCurvature line 22
  4. theorem OAI.SK.Analytic.RootSpinCurvature.bounds line 25
  5. theorem OAI.SK.Analytic.RootSpinCurvature.gaussianStep line 33
  6. theorem OAI.SK.Analytic.rootGradient_continuous line 39
  7. theorem OAI.SK.Analytic.rootHessian_continuous line 43
  8. theorem OAI.SK.Analytic.rootLine_hasDerivAt line 48
  9. theorem OAI.SK.Analytic.rootGradientLine_hasDerivAt line 56
  10. theorem OAI.SK.Analytic.rootShift_value_bound line 67
  11. theorem OAI.SK.Analytic.rootShift_gradient_bound line 77
  12. theorem OAI.SK.Analytic.rootGradient_fst line 87
  13. theorem OAI.SK.Analytic.rootGradient_penalty_succ line 98