OAI/Computability/PerfectCompleteness/Decoding/HierarchicalDecoderMeetingLemmas.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.HierarchicalDecoderMeeting.affine_meeting_probability_lower line 24
  2. def OAI.PerfectCompleteness.HierarchicalDecoderMeeting.useful line 71
  3. def OAI.PerfectCompleteness.HierarchicalDecoderMeeting.leftLaw line 75
  4. theorem OAI.PerfectCompleteness.HierarchicalDecoderMeeting.leftLaw_eq_affine line 82
  5. theorem OAI.PerfectCompleteness.HierarchicalDecoderMeeting.columnSpace_eq_nativeQ line 105
  6. theorem OAI.PerfectCompleteness.HierarchicalDecoderMeeting.nativeCorrection_eq_nativeCenter line 114
  7. theorem OAI.PerfectCompleteness.HierarchicalDecoderMeeting.meeting_probability_ge_coset line 125
  8. theorem OAI.PerfectCompleteness.HierarchicalDecoderMeeting.meeting_probability_lower line 154
  9. theorem OAI.PerfectCompleteness.HierarchicalFixedDecoderMeeting.kernel_finrank_ge line 212
  10. theorem OAI.PerfectCompleteness.HierarchicalFixedDecoderMeeting.repetitionsBalanced line 223
  11. theorem OAI.PerfectCompleteness.HierarchicalFixedDecoderMeeting.slice_error line 227
  12. theorem OAI.PerfectCompleteness.HierarchicalFixedDecoderMeeting.list_error line 232
  13. theorem OAI.PerfectCompleteness.HierarchicalFixedDecoderMeeting.kernel_excluded line 237
  14. theorem OAI.PerfectCompleteness.HierarchicalFixedDecoderMeeting.meeting_probability_lower line 275