OAI/Combinatorics/EditApproximation/Refinement/PhysicalCommonSource.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The actual bounded physical program can share one source universe across incoming seed tables. Online coordinates include their requested range; group coordinates share whole-cell arrays.

  1. abbrev OAI.EditApproximation.PhysicalCommonCoordinate line 18
  2. instance OAI.EditApproximation.physicalCommonCoordinateFintype line 29
  3. instance OAI.EditApproximation.physicalCommonCoordinateMeasurable line 33
  4. instance OAI.EditApproximation.physicalCommonCoordinateSingleton line 37
  5. def OAI.EditApproximation.physicalCommonCoordinateLaw line 41
  6. instance OAI.EditApproximation.physicalCommonCoordinateLaw_probability line 48
  7. abbrev OAI.EditApproximation.PhysicalCommonDraw line 53
  8. def OAI.EditApproximation.physicalCommonLaw line 56
  9. instance OAI.EditApproximation.physicalCommonLaw_probability line 59
  10. theorem OAI.EditApproximation.physicalCommonMass_positive line 75
  11. def OAI.EditApproximation.physicalCommonSelectedOnlineKey line 80
  12. def OAI.EditApproximation.physicalCommonSelectedKey line 86
  13. theorem OAI.EditApproximation.physicalCommonSelectedKey_injective line 93
  14. theorem OAI.EditApproximation.physicalCommonSelectedOnlineKey_range line 107
  15. def OAI.EditApproximation.physicalCommonCoordinateImage line 113
  16. def OAI.EditApproximation.physicalCommonSample line 123
  17. theorem OAI.EditApproximation.physicalCommonSample_law line 129