OAI/Analysis/HardSphere/Allocation/WeightedExpose.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Comparison.allocationBase line 18
  2. instance OAI.HardSphere.Comparison.allocationBase_sfinite line 21
  3. lemma OAI.HardSphere.Comparison.allocationBase_sum line 27
  4. lemma OAI.HardSphere.Comparison.allocation_branch_sum line 40
  5. lemma OAI.HardSphere.Comparison.allocated_exposure_reconstruct line 54
  6. lemma OAI.HardSphere.genuine_ground_allocated_exposure line 84
  7. lemma OAI.HardSphere.allocated_physical_fiber line 106
  8. def OAI.HardSphere.Groups.ownPath line 140
  9. lemma OAI.HardSphere.Groups.ownPath_measurable line 144
  10. lemma OAI.HardSphere.Groups.ownPath_eq line 149
  11. def OAI.HardSphere.Groups.ownEligible line 154
  12. lemma OAI.HardSphere.Groups.ownEligible_measurable line 159
  13. def OAI.HardSphere.Groups.eligibilityFlag line 169
  14. lemma OAI.HardSphere.Groups.eligibilityFlag_measurable line 173
  15. lemma OAI.HardSphere.Groups.exposed_endpoints line 185
  16. def OAI.HardSphere.Groups.recordedList line 213
  17. lemma OAI.HardSphere.Groups.recordedList_measurable line 217
  18. lemma OAI.HardSphere.Groups.recordedList_eq line 243