OAI/Probability/SKBarriers/Scalar/ScalarListBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.scalarIncrementChain_lipschitz line 16
  2. theorem OAI.SK.Analytic.scalarIncrementChain_spin_convex line 22
  3. theorem OAI.SK.Analytic.scalarIncrementChain_hessian_lipschitz line 30
  4. theorem OAI.SK.Analytic.scalarIncrementAverage_bounded line 36
  5. theorem OAI.SK.Analytic.scalarIncrementAverage_abs_le line 41
  6. theorem OAI.SK.Analytic.scalarIncrementAverage_nonneg line 47
  7. theorem OAI.SK.Analytic.weightedAverage_nonneg line 53
  8. def OAI.SK.Analytic.weightedMomentBound line 62
  9. theorem OAI.SK.Analytic.weightedMomentBound_nonneg line 64
  10. theorem OAI.SK.Analytic.weightedAverage_abs_le line 68
  11. theorem OAI.SK.Analytic.weightedAverage_bounded line 78