OAI/Computability/PerfectCompleteness/Decoding/HierarchicalAllDecoderTables.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.HierarchicalAllDecoderTables.row_probability_of_raw line 18
  2. abbrev OAI.PerfectCompleteness.HierarchicalAllDecoderTables.Background line 41
  3. abbrev OAI.PerfectCompleteness.HierarchicalAllDecoderTables.Input line 43
  4. instance OAI.PerfectCompleteness.HierarchicalAllDecoderTables.inputFintype line 53
  5. abbrev OAI.PerfectCompleteness.HierarchicalAllDecoderTables.UpperAnswer line 62
  6. def OAI.PerfectCompleteness.HierarchicalAllDecoderTables.upperKernel line 77
  7. def OAI.PerfectCompleteness.HierarchicalAllDecoderTables.upperTableLaw line 82
  8. def OAI.PerfectCompleteness.HierarchicalAllDecoderTables.decodeTable line 86
  9. def OAI.PerfectCompleteness.HierarchicalAllDecoderTables.responseLaw line 93
  10. def OAI.PerfectCompleteness.HierarchicalAllDecoderTables.tableLaw line 100
  11. theorem OAI.PerfectCompleteness.HierarchicalAllDecoderTables.upperTableLaw_pushforward line 106
  12. theorem OAI.PerfectCompleteness.HierarchicalAllDecoderTables.supported_upper_table_valid line 118
  13. theorem OAI.PerfectCompleteness.HierarchicalAllDecoderTables.upperTableLaw_valid line 131
  14. def OAI.PerfectCompleteness.HierarchicalAllDecoderTables.RowValid line 140
  15. theorem OAI.PerfectCompleteness.HierarchicalAllDecoderTables.responseLaw_valid line 145
  16. theorem OAI.PerfectCompleteness.HierarchicalAllDecoderTables.supported_table_valid line 169
  17. theorem OAI.PerfectCompleteness.HierarchicalAllDecoderTables.tableLaw_valid line 180
  18. theorem OAI.PerfectCompleteness.HierarchicalAllDecoderTables.decoded_supported_table_valid line 190