OAI/Probability/SKBarriers/Scalar/ScalarHierarchyAverageAlgebra.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SK.Analytic.BoundedScalar line 14
  2. theorem OAI.SK.Analytic.BoundedScalar.const line 18
  3. theorem OAI.SK.Analytic.BoundedScalar.add line 21
  4. theorem OAI.SK.Analytic.BoundedScalar.const_mul line 28
  5. theorem OAI.SK.Analytic.BoundedScalar.sub line 35
  6. theorem OAI.SK.Analytic.BoundedScalar.sq line 39
  7. theorem OAI.SK.Analytic.ScalarSpinConvex.gradient_bounded line 46
  8. theorem OAI.SK.Analytic.ScalarSpinConvex.hessian_bounded line 50
  9. theorem OAI.SK.Analytic.BoundedScalar.scalarStepAverage line 54
  10. theorem OAI.SK.Analytic.scalarHierarchyAverage_bounded line 60
  11. theorem OAI.SK.Analytic.scalarHierarchyAverage_integrable line 67
  12. theorem OAI.SK.Analytic.scalarHierarchyAverage_integral line 76
  13. theorem OAI.SK.Analytic.scalarHierarchyAverage_const_mul line 84
  14. theorem OAI.SK.Analytic.scalarHierarchyAverage_add line 90
  15. theorem OAI.SK.Analytic.scalarHierarchyAverage_sub line 98
  16. theorem OAI.SK.Analytic.scalarHierarchyAverage_mono line 106
  17. theorem OAI.SK.Analytic.scalarHierarchyAverage_nonneg line 114
  18. theorem OAI.SK.Analytic.scalarHierarchyAverage_sq line 120