OAI/Computability/PerfectCompleteness/Sampling/StoppedUsefulPairLaw.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.StoppedUsefulPairLaw.Descriptor line 26
  2. def OAI.PerfectCompleteness.StoppedUsefulPairLaw.externalLaw line 31
  3. def OAI.PerfectCompleteness.StoppedUsefulPairLaw.background line 46
  4. def OAI.PerfectCompleteness.StoppedUsefulPairLaw.scalarValue line 55
  5. def OAI.PerfectCompleteness.StoppedUsefulPairLaw.nativeScalarLaw line 64
  6. def OAI.PerfectCompleteness.StoppedUsefulPairLaw.scalarLaw line 72
  7. def OAI.PerfectCompleteness.StoppedUsefulPairLaw.readout line 81
  8. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.scalarValue_law line 89
  9. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.readout_law line 101
  10. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.background_readout line 114
  11. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.matrix_readout line 131
  12. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.assembled_arrays line 154
  13. abbrev OAI.PerfectCompleteness.StoppedUsefulPairLaw.Sample line 171
  14. def OAI.PerfectCompleteness.StoppedUsefulPairLaw.directionLaw line 177
  15. def OAI.PerfectCompleteness.StoppedUsefulPairLaw.actualLaw line 183
  16. def OAI.PerfectCompleteness.StoppedUsefulPairLaw.observe line 191
  17. def OAI.PerfectCompleteness.StoppedUsefulPairLaw.liftFresh line 202
  18. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.liftFresh_law line 211
  19. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.descriptor_chain_law line 231
  20. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.observe_law line 292
  21. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.replacement_matrix line 347
  22. def OAI.PerfectCompleteness.StoppedUsefulPairLaw.actualPair line 371
  23. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.pairRecord_observe line 384
  24. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.actualPair_law line 404
  25. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.stoppedProjectedPair_eq line 423
  26. theorem OAI.PerfectCompleteness.StoppedUsefulPairLaw.stoppedProjectedPair_law line 432