OAI/Computability/PerfectCompleteness/Algebra/AffineDecoderMeeting.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.AffineDecoderMeeting.product_probability_lower line 19
  2. def OAI.PerfectCompleteness.AffineDecoderMeeting.nativeQ line 47
  3. def OAI.PerfectCompleteness.AffineDecoderMeeting.nativeCenter line 50
  4. theorem OAI.PerfectCompleteness.AffineDecoderMeeting.candidate_mem_nativeCoset line 52
  5. theorem OAI.PerfectCompleteness.AffineDecoderMeeting.exists_candidate_of_mem_nativeCoset line 59
  6. theorem OAI.PerfectCompleteness.AffineDecoderMeeting.nativeCoset_iff_exists_candidate line 69
  7. theorem OAI.PerfectCompleteness.AffineDecoderMeeting.finrank_nativeQ_le line 77
  8. theorem OAI.PerfectCompleteness.AffineDecoderMeeting.native_point_probability_lower line 103
  9. theorem OAI.PerfectCompleteness.AffineDecoderMeeting.meeting_probability_lower line 112