OAI/Computability/PerfectCompleteness/Decoding/DecoderTableCoupling.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.DecoderTableCoupling.probability_eq_expectation line 18
  2. theorem OAI.PerfectCompleteness.DecoderTableCoupling.table_eq_product line 24
  3. theorem OAI.PerfectCompleteness.DecoderTableCoupling.pair_law_of_ne line 28
  4. def OAI.PerfectCompleteness.DecoderTableCoupling.definedEqual line 49
  5. theorem OAI.PerfectCompleteness.DecoderTableCoupling.definedEqual_none_left line 53
  6. theorem OAI.PerfectCompleteness.DecoderTableCoupling.definedEqual_none_right line 57
  7. theorem OAI.PerfectCompleteness.DecoderTableCoupling.definedEqual_self line 61
  8. theorem OAI.PerfectCompleteness.DecoderTableCoupling.definedEqual_collision line 65
  9. def OAI.PerfectCompleteness.DecoderTableCoupling.freshCollision line 68
  10. def OAI.PerfectCompleteness.DecoderTableCoupling.frozenCollision line 71
  11. theorem OAI.PerfectCompleteness.DecoderTableCoupling.frozenCollision_of_ne line 74
  12. theorem OAI.PerfectCompleteness.DecoderTableCoupling.frozenCollision_self line 80
  13. theorem OAI.PerfectCompleteness.DecoderTableCoupling.product_probability_first line 87
  14. theorem OAI.PerfectCompleteness.DecoderTableCoupling.freshCollision_self_le line 98
  15. theorem OAI.PerfectCompleteness.DecoderTableCoupling.freshCollision_le_frozenCollision line 109
  16. theorem OAI.PerfectCompleteness.DecoderTableCoupling.mean_freshCollision_le_frozen line 118
  17. theorem OAI.PerfectCompleteness.DecoderTableCoupling.freshCollision_le_of_supported_tables line 135