OAI/Computability/PerfectCompleteness/Decoding/HierarchicalDecoderTables.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.HierarchicalDecoderTables.constant_row_event_eq line 24
  2. theorem OAI.PerfectCompleteness.HierarchicalDecoderTables.table_admissible_of_constant_probability_one line 33
  3. theorem OAI.PerfectCompleteness.HierarchicalDecoderTables.hit_square_le_of_constant_probability_one line 45
  4. abbrev OAI.PerfectCompleteness.HierarchicalDecoderTables.Advice line 78
  5. abbrev OAI.PerfectCompleteness.HierarchicalDecoderTables.LowerH line 95
  6. abbrev OAI.PerfectCompleteness.HierarchicalDecoderTables.Answer line 98
  7. def OAI.PerfectCompleteness.HierarchicalDecoderTables.fullRank line 105
  8. def OAI.PerfectCompleteness.HierarchicalDecoderTables.decode line 110
  9. def OAI.PerfectCompleteness.HierarchicalDecoderTables.responseLaw line 116
  10. def OAI.PerfectCompleteness.HierarchicalDecoderTables.Valid line 123
  11. theorem OAI.PerfectCompleteness.HierarchicalDecoderTables.decode_valid line 132
  12. theorem OAI.PerfectCompleteness.HierarchicalDecoderTables.responseLaw_valid line 149
  13. def OAI.PerfectCompleteness.HierarchicalDecoderTables.tableLaw line 166
  14. def OAI.PerfectCompleteness.HierarchicalDecoderTables.upperTableLaw line 173
  15. theorem OAI.PerfectCompleteness.HierarchicalDecoderTables.upperTableLaw_pushforward line 180
  16. theorem OAI.PerfectCompleteness.HierarchicalDecoderTables.supported_table_valid line 191
  17. theorem OAI.PerfectCompleteness.HierarchicalDecoderTables.hit_square_le line 214