OAI/Computability/PerfectCompleteness/Algebra/DecoderRankSplit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.DecoderRankSplit.F2 line 16
  2. def OAI.PerfectCompleteness.DecoderRankSplit.meeting line 22
  3. def OAI.PerfectCompleteness.DecoderRankSplit.nativeRank line 29
  4. def OAI.PerfectCompleteness.DecoderRankSplit.low line 38
  5. def OAI.PerfectCompleteness.DecoderRankSplit.highAgrees line 42
  6. theorem OAI.PerfectCompleteness.DecoderRankSplit.highAgrees_eq_true line 46
  7. theorem OAI.PerfectCompleteness.DecoderRankSplit.decide_and_comm line 52
  8. theorem OAI.PerfectCompleteness.DecoderRankSplit.meeting_low line 56
  9. theorem OAI.PerfectCompleteness.DecoderRankSplit.probability_split line 66
  10. theorem OAI.PerfectCompleteness.DecoderRankSplit.pair_probability_split line 85