OAI/Computability/PerfectCompleteness/Decoding/FixedSourceLowerCollision.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.FixedSourceLowerCollision.Questions line 35
  2. abbrev OAI.PerfectCompleteness.FixedSourceLowerCollision.Table line 38
  3. abbrev OAI.PerfectCompleteness.FixedSourceLowerCollision.TableFamily line 59
  4. def OAI.PerfectCompleteness.FixedSourceLowerCollision.first line 67
  5. def OAI.PerfectCompleteness.FixedSourceLowerCollision.second line 71
  6. def OAI.PerfectCompleteness.FixedSourceLowerCollision.markedProbability line 77
  7. def OAI.PerfectCompleteness.FixedSourceLowerCollision.uniformProbability line 85
  8. def OAI.PerfectCompleteness.FixedSourceLowerCollision.tableLaw line 103
  9. theorem OAI.PerfectCompleteness.FixedSourceLowerCollision.supported_row line 110
  10. theorem OAI.PerfectCompleteness.FixedSourceLowerCollision.supported_uniform_le line 121
  11. theorem OAI.PerfectCompleteness.FixedSourceLowerCollision.expectation_add_const line 176
  12. theorem OAI.PerfectCompleteness.FixedSourceLowerCollision.mean_marked_le line 182