OAI/Probability/SKBarriers/Scalar/ScalarAverageCalculus.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.ScalarSpinConvex line 15
  2. theorem OAI.SK.Analytic.ScalarSpinConvex.bounds line 18
  3. def OAI.SK.Analytic.scalarStepLinear line 25
  4. theorem OAI.SK.Analytic.scalarStepLinear_apply line 28
  5. theorem OAI.SK.Analytic.scalarStep_prefixGradient line 31
  6. theorem OAI.SK.Analytic.scalarStep_prefixHessian line 44
  7. theorem OAI.SK.Analytic.scalarStep_rootGradient line 51
  8. theorem OAI.SK.Analytic.scalarStep_rootHessian line 57
  9. theorem OAI.SK.Analytic.scalarStepAverage_continuous line 65
  10. theorem OAI.SK.Analytic.scalarStepAverage_bound line 73
  11. theorem OAI.SK.Analytic.scalarStepAverage_integrable line 79
  12. theorem OAI.SK.Analytic.scalarStepAverage_variance_nonneg line 85
  13. theorem OAI.SK.Analytic.ScalarSpinConvex.scalarStep line 97
  14. theorem OAI.SK.Analytic.scalarStepAverage_cramer line 123