OAI/Computability/PerfectCompleteness/Reduction/FixedStoppedUsefulMass.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.FixedStoppedUsefulMass.probability_cast_array_law line 20
  2. abbrev OAI.PerfectCompleteness.FixedStoppedUsefulMass.clauses line 34
  3. abbrev OAI.PerfectCompleteness.FixedStoppedUsefulMass.Outer line 36
  4. abbrev OAI.PerfectCompleteness.FixedStoppedUsefulMass.Base line 41
  5. def OAI.PerfectCompleteness.FixedStoppedUsefulMass.flags line 46
  6. theorem OAI.PerfectCompleteness.FixedStoppedUsefulMass.flags_eq_projectionFlag line 51
  7. def OAI.PerfectCompleteness.FixedStoppedUsefulMass.outerLaw line 63
  8. def OAI.PerfectCompleteness.FixedStoppedUsefulMass.baseLaw line 67
  9. def OAI.PerfectCompleteness.FixedStoppedUsefulMass.record line 72
  10. abbrev OAI.PerfectCompleteness.FixedStoppedUsefulMass.PhysicalSample line 86
  11. abbrev OAI.PerfectCompleteness.FixedStoppedUsefulMass.OriginalSample line 91
  12. def OAI.PerfectCompleteness.FixedStoppedUsefulMass.physicalLaw line 96
  13. def OAI.PerfectCompleteness.FixedStoppedUsefulMass.physicalRecord line 103
  14. def OAI.PerfectCompleteness.FixedStoppedUsefulMass.referenceMass line 112
  15. theorem OAI.PerfectCompleteness.FixedStoppedUsefulMass.physical_fiber_probability_lower line 124
  16. theorem OAI.PerfectCompleteness.FixedStoppedUsefulMass.physical_probability_lower line 223
  17. theorem OAI.PerfectCompleteness.FixedStoppedUsefulMass.referenceMass_eq_stopped line 238
  18. theorem OAI.PerfectCompleteness.FixedStoppedUsefulMass.stopped_probability_lower line 293
  19. abbrev OAI.PerfectCompleteness.FixedStoppedUsefulMass.canonicalStrategy line 309
  20. abbrev OAI.PerfectCompleteness.FixedStoppedUsefulMass.experiment line 314
  21. abbrev OAI.PerfectCompleteness.FixedStoppedUsefulMass.OriginalFiber line 321
  22. def OAI.PerfectCompleteness.FixedStoppedUsefulMass.originalLaw line 330
  23. def OAI.PerfectCompleteness.FixedStoppedUsefulMass.originalRecord line 337
  24. def OAI.PerfectCompleteness.FixedStoppedUsefulMass.upperEvent line 341
  25. theorem OAI.PerfectCompleteness.FixedStoppedUsefulMass.lowerEvent_eq_win line 349
  26. theorem OAI.PerfectCompleteness.FixedStoppedUsefulMass.upperEvent_eq_win line 377
  27. theorem OAI.PerfectCompleteness.FixedStoppedUsefulMass.originalRecord_physicalRead line 395
  28. theorem OAI.PerfectCompleteness.FixedStoppedUsefulMass.joint_probability_eq_physical line 409
  29. theorem OAI.PerfectCompleteness.FixedStoppedUsefulMass.joint_probability_ge_of_reserve line 440
  30. theorem OAI.PerfectCompleteness.FixedStoppedUsefulMass.useful_probability_ge_of_reserve line 460