OAI/Probability/SKBarriers/Scalar/ScalarCDFLimit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.scalarCDFValue line 15
  2. def OAI.SK.Analytic.scalarCDFGradient line 18
  3. def OAI.SK.Analytic.scalarCDFHessian line 21
  4. theorem OAI.SK.Analytic.scalarSpinTerminal_regular line 24
  5. theorem OAI.SK.Analytic.dyadicScalar_value_uniform line 27
  6. theorem OAI.SK.Analytic.dyadicScalar_value_error line 36
  7. theorem OAI.SK.Analytic.dyadicScalar_gradient_uniform line 47
  8. theorem OAI.SK.Analytic.dyadicScalar_hessian_uniform line 59
  9. theorem OAI.SK.Analytic.scalarCDFValue_hasDerivAt line 71
  10. theorem OAI.SK.Analytic.scalarCDFGradient_hasDerivAt line 79
  11. theorem OAI.SK.Analytic.scalarCDF_derivative_bounds line 87
  12. theorem OAI.SK.Analytic.scalarCDFHessian_lipschitz line 101