OAI/Computability/PerfectCompleteness/Decoding/FixedSourceChildCollision.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.FixedSourceChildCollision.Calls line 22
  2. abbrev OAI.PerfectCompleteness.FixedSourceChildCollision.Questions line 24
  3. abbrev OAI.PerfectCompleteness.FixedSourceChildCollision.Native line 28
  4. abbrev OAI.PerfectCompleteness.FixedSourceChildCollision.Form line 32
  5. abbrev OAI.PerfectCompleteness.FixedSourceChildCollision.Sample line 35
  6. def OAI.PerfectCompleteness.FixedSourceChildCollision.markedLaw line 38
  7. def OAI.PerfectCompleteness.FixedSourceChildCollision.uniformLaw line 45
  8. def OAI.PerfectCompleteness.FixedSourceChildCollision.restrictedEvent line 56
  9. def OAI.PerfectCompleteness.FixedSourceChildCollision.fullEvent line 62
  10. theorem OAI.PerfectCompleteness.FixedSourceChildCollision.expectation_add_const line 66
  11. theorem OAI.PerfectCompleteness.FixedSourceChildCollision.restricted_probability_le line 72