OAI/Analysis/Steinitz/FilteredBody.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Filtered-body energy and the predictor slab budget.

  1. def OAI.GaussianEvents.openConstraints line 14
  2. lemma OAI.GaussianEvents.openConstraints_open line 16
  3. lemma OAI.GaussianEvents.openConstraints_convex line 20
  4. lemma OAI.GaussianEvents.openConstraints_symmetric line 26
  5. lemma OAI.GaussianEvents.openConstraints_zero line 31
  6. def OAI.EuclideanSteinitz.Filter.bodyRate line 40
  7. lemma OAI.EuclideanSteinitz.Filter.bodyRate_nonneg line 41
  8. def OAI.EuclideanSteinitz.Filter.applicationDomain line 42
  9. lemma OAI.EuclideanSteinitz.Filter.applicationDomain_open line 48
  10. lemma OAI.EuclideanSteinitz.Filter.applicationDomain_convex line 52
  11. lemma OAI.EuclideanSteinitz.Filter.applicationDomain_bounded line 56
  12. lemma OAI.EuclideanSteinitz.Filter.applicationDomain_symmetric line 60
  13. lemma OAI.EuclideanSteinitz.Filter.applicationDomain_zero line 66
  14. lemma OAI.EuclideanSteinitz.Filter.slabs_rate line 75
  15. lemma OAI.EuclideanSteinitz.Filter.applicationDomain_survival line 85
  16. def OAI.EuclideanSteinitz.Filter.bodyScale line 159
  17. lemma OAI.EuclideanSteinitz.Filter.bodyScale_pos line 160
  18. lemma OAI.EuclideanSteinitz.Filter.bodyScale_ge_one line 161
  19. lemma OAI.EuclideanSteinitz.Filter.bodyScale_bound line 162
  20. lemma OAI.EuclideanSteinitz.Filter.applicationDomain_good line 167