OAI/Computability/PerfectCompleteness/Sampling/FixedStoppedPhysicalLawLemmas.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.clauses line 24
  2. def OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.designated line 26
  3. def OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.flag line 30
  4. abbrev OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.Prefixes line 34
  5. abbrev OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.Context line 35
  6. def OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.path line 37
  7. abbrev OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.ChildSample line 41
  8. abbrev OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.Sample line 48
  9. abbrev OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.PhysicalSample line 51
  10. def OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.childLaw line 56
  11. def OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.law line 64
  12. def OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.read line 68
  13. abbrev OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.physicalLaw line 85
  14. theorem OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.expectation_read line 93
  15. theorem OAI.PerfectCompleteness.FixedStoppedPhysicalLaw.read_law line 169
  16. def OAI.PerfectCompleteness.FixedStoppedNativeLaw.sourceSampleEquiv line 203
  17. theorem OAI.PerfectCompleteness.FixedStoppedNativeLaw.sourceSampleEquiv_law line 212
  18. abbrev OAI.PerfectCompleteness.FixedStoppedNativeLaw.Context line 232
  19. abbrev OAI.PerfectCompleteness.FixedStoppedNativeLaw.setup line 234
  20. abbrev OAI.PerfectCompleteness.FixedStoppedNativeLaw.Sample line 238
  21. theorem OAI.PerfectCompleteness.FixedStoppedNativeLaw.path_eq line 241
  22. def OAI.PerfectCompleteness.FixedStoppedNativeLaw.childRead line 249
  23. theorem OAI.PerfectCompleteness.FixedStoppedNativeLaw.childRead_law line 256
  24. def OAI.PerfectCompleteness.FixedStoppedNativeLaw.law line 265
  25. def OAI.PerfectCompleteness.FixedStoppedNativeLaw.sourceRead line 270
  26. theorem OAI.PerfectCompleteness.FixedStoppedNativeLaw.sourceRead_law line 274
  27. def OAI.PerfectCompleteness.FixedStoppedNativeLaw.read line 293
  28. theorem OAI.PerfectCompleteness.FixedStoppedNativeLaw.read_law line 298
  29. theorem OAI.PerfectCompleteness.FixedStoppedNativeLaw.expectation_read line 307