OAI/Combinatorics/EditApproximation/Refinement/PhysicalLocalProgramLaw.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A single bounded-key product supplies both online and whole-cell streams. Restriction to the complete program preserves their joint law, including independence between the two kinds of stream.

  1. abbrev OAI.EditApproximation.PhysicalLocalProgramKey line 13
  2. abbrev OAI.EditApproximation.PhysicalLocalProgramCoordinate line 23
  3. instance OAI.EditApproximation.physicalLocalProgramCoordinateFintype line 29
  4. instance OAI.EditApproximation.physicalLocalProgramCoordinateMeasurableSpace line 34
  5. instance OAI.EditApproximation.physicalLocalProgramCoordinateMeasurableSingleton line 39
  6. def OAI.EditApproximation.physicalLocalProgramCoordinateLaw line 46
  7. instance OAI.EditApproximation.physicalLocalProgramCoordinateLaw_probability line 55
  8. abbrev OAI.EditApproximation.PhysicalLocalProgramDraw line 62
  9. def OAI.EditApproximation.physicalLocalProgramDrawLaw line 65
  10. def OAI.EditApproximation.physicalLocalProgramOldKey line 69
  11. theorem OAI.EditApproximation.physicalLocalProgramOldKey_injective line 77
  12. def OAI.EditApproximation.physicalLocalProgramCoordinateImage line 98
  13. def OAI.EditApproximation.physicalLocalProgramToComplete line 109
  14. theorem OAI.EditApproximation.physicalLocalProgramDrawLaw_map line 115