OAI/NumberTheory/OrdinaryCorrelations/HighTrace/FirstSlot.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCorrelations.SharedSlotPatterns.support line 17
  2. lemma OAI.OrdinaryCorrelations.SharedSlotPatterns.mem_support line 19
  3. def OAI.OrdinaryCorrelations.SharedSlotPatterns.firstSlot line 22
  4. lemma OAI.OrdinaryCorrelations.SharedSlotPatterns.firstSlot_eq line 25
  5. lemma OAI.OrdinaryCorrelations.SharedSlotPatterns.firstSlot_injective line 28
  6. lemma OAI.OrdinaryCorrelations.SharedSlotPatterns.card_support_le line 34
  7. def OAI.OrdinaryCorrelations.SharedSlotPatterns.values line 37
  8. def OAI.OrdinaryCorrelations.SharedSlotPatterns.pattern line 41
  9. lemma OAI.OrdinaryCorrelations.SharedSlotPatterns.decode_pattern line 46
  10. abbrev OAI.OrdinaryCorrelations.SharedSlotPatterns.Code line 55
  11. def OAI.OrdinaryCorrelations.SharedSlotPatterns.encode line 58
  12. def OAI.OrdinaryCorrelations.SharedSlotPatterns.decode line 61
  13. lemma OAI.OrdinaryCorrelations.SharedSlotPatterns.decode_encode line 63
  14. lemma OAI.OrdinaryCorrelations.SharedSlotPatterns.encode_injective line 66
  15. lemma OAI.OrdinaryCorrelations.SharedSlotPatterns.weight_identity line 69
  16. def OAI.OrdinaryCorrelations.SharedSlotPatterns.codeWeight line 74
  17. lemma OAI.OrdinaryCorrelations.SharedSlotPatterns.codeWeight_encode line 76
  18. theorem OAI.OrdinaryCorrelations.SharedSlotPatterns.weighted_code_sum line 79