OAI/Analysis/HardSphere/Allocation/PhysicalLabelLaw.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.HardSphere.Groups.labelOptionSpace line 16
  2. instance OAI.HardSphere.Groups.labelOptionSingletons line 17
  3. def OAI.HardSphere.Groups.paddedLabels line 21
  4. lemma OAI.HardSphere.Groups.paddedLabels_nonempty line 24
  5. def OAI.HardSphere.Groups.uniformLabels line 29
  6. instance OAI.HardSphere.Groups.uniformLabels_probability line 31
  7. lemma OAI.HardSphere.Groups.uniformLabels_supported line 35
  8. def OAI.HardSphere.Groups.branchAccessible line 42
  9. lemma OAI.HardSphere.Groups.branchAccessible_measurable line 48
  10. def OAI.HardSphere.Groups.physicalLabelAt line 54
  11. instance OAI.HardSphere.Groups.physicalLabelAt_markov line 61
  12. def OAI.HardSphere.Groups.physicalLabels line 66
  13. instance OAI.HardSphere.Groups.physicalLabels_markov line 70
  14. lemma OAI.HardSphere.Groups.physicalLabels_supported line 79
  15. lemma OAI.HardSphere.Groups.physicalBranchLaw_ae line 104
  16. lemma OAI.HardSphere.Groups.physicalBranchLaw_allocation line 134
  17. lemma OAI.HardSphere.Groups.physicalBranchLaw_multiplicity line 143
  18. lemma OAI.HardSphere.Groups.datum_norm_geometry_measurableSet line 156
  19. lemma OAI.HardSphere.Groups.datum_sep_geometry_measurableSet line 166
  20. lemma OAI.HardSphere.Groups.datum_geometry_measurableSet line 176
  21. lemma OAI.HardSphere.Groups.physicalBranchLaw_geometry line 196
  22. lemma OAI.HardSphere.Groups.branchAccessible_card line 209
  23. lemma OAI.HardSphere.Groups.branchAccessible_supply line 228