OAI/Computability/PerfectCompleteness/Sampling/StoppedProjectedGlobalLawLemmas.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.Context line 21
  2. abbrev OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.Outer line 24
  3. def OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.projectedSlots line 27
  4. theorem OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.projectedSlots_eq line 32
  5. abbrev OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.Sample line 45
  6. abbrev OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.ExperimentSample line 50
  7. def OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.read line 58
  8. def OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.law line 70
  9. abbrev OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.experiment line 77
  10. def OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.experimentLaw line 81
  11. theorem OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.fiber_probability line 86
  12. theorem OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.probability_read line 120
  13. theorem OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.read_law line 152
  14. theorem OAI.PerfectCompleteness.StoppedProjectedGlobalLaw.arrays_read line 162
  15. abbrev OAI.PerfectCompleteness.StoppedProjectedPhysicalLaw.Outer line 201
  16. abbrev OAI.PerfectCompleteness.StoppedProjectedPhysicalLaw.Sample line 204
  17. def OAI.PerfectCompleteness.StoppedProjectedPhysicalLaw.read line 208
  18. def OAI.PerfectCompleteness.StoppedProjectedPhysicalLaw.law line 218
  19. theorem OAI.PerfectCompleteness.StoppedProjectedPhysicalLaw.read_law line 223
  20. theorem OAI.PerfectCompleteness.StoppedProjectedPhysicalLaw.expectation_read line 237
  21. theorem OAI.PerfectCompleteness.StoppedProjectedPhysicalLaw.probability_read line 247
  22. theorem OAI.PerfectCompleteness.StoppedProjectedPhysicalLaw.arrays_read_heq line 258