OAI/Analysis/HardSphere/Geometry/LocalCheck.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HardSphere.Comparison.LocalCheck line 15
  2. def OAI.HardSphere.Comparison.retainedEvent line 25
  3. def OAI.HardSphere.Comparison.insertionEvent line 28
  4. lemma OAI.HardSphere.Comparison.measurableSet_retainedEvent line 32
  5. lemma OAI.HardSphere.Comparison.measurableSet_insertionEvent line 45
  6. lemma OAI.HardSphere.Comparison.retainedEvent_insert line 61
  7. lemma OAI.HardSphere.Comparison.retainedEvent_update line 75
  8. def OAI.HardSphere.Comparison.checkWeight line 86
  9. lemma OAI.HardSphere.Comparison.measurable_checkWeight line 89
  10. lemma OAI.HardSphere.Comparison.checkWeight_le_one line 93
  11. def OAI.HardSphere.Comparison.UniformInsertion line 98
  12. lemma OAI.HardSphere.Comparison.insertion_integral_lower line 104
  13. def OAI.HardSphere.Comparison.checkNormalizer line 121
  14. lemma OAI.HardSphere.Comparison.checkNormalizer_insert_lower line 124
  15. lemma OAI.HardSphere.Comparison.checkWeight_depends line 139
  16. lemma OAI.HardSphere.Comparison.checkNormalizer_const line 151
  17. lemma OAI.HardSphere.Comparison.checkNormalizer_empty line 160
  18. lemma OAI.HardSphere.Comparison.checkNormalizer_le_one line 168
  19. lemma OAI.HardSphere.Comparison.checkNormalizer_union_lower line 175
  20. lemma OAI.HardSphere.Comparison.checkNormalizer_pos line 195
  21. lemma OAI.HardSphere.Comparison.checkWeight_antitone line 203
  22. lemma OAI.HardSphere.Comparison.checkNormalizer_antitone line 212
  23. def OAI.HardSphere.Comparison.SeparatedChecks line 226
  24. lemma OAI.HardSphere.Comparison.checkWeight_union line 231
  25. lemma OAI.HardSphere.Comparison.checkNormalizer_union_eq_mul line 246
  26. lemma OAI.HardSphere.Comparison.checkNormalizer_far_lower line 278
  27. lemma OAI.HardSphere.Comparison.lmarginal_eq_const_of_depends line 288
  28. lemma OAI.HardSphere.Comparison.lmarginal_of_disjoint_depends line 300
  29. lemma OAI.HardSphere.Comparison.lmarginal_mul_disjoint line 316
  30. lemma OAI.HardSphere.Comparison.lmarginal_prod_coordinates line 345
  31. lemma OAI.HardSphere.Comparison.checkNormalizer_delete_le line 368