OAI/Computability/VertexCover/PCP/RoundSize.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.card_padded_alphabet line 39
  2. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.card_powered_dart line 46
  3. opaque OAI.UniqueGames.Foundations.PCP.RoundSize.lockedNat line 53
  4. def OAI.UniqueGames.Foundations.PCP.RoundSize.poweredAlphabetSize line 55
  5. def OAI.UniqueGames.Foundations.PCP.RoundSize.poweredDartFactor line 59
  6. def OAI.UniqueGames.Foundations.PCP.RoundSize.sizeFactor line 62
  7. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.poweredAlphabetSize_eq line 66
  8. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.poweredDartFactor_eq line 70
  9. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.sizeFactor_eq line 74
  10. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.coefficient_positive line 78
  11. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.poweredAlphabet_card line 83
  12. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.sizeFactor_positive line 92
  13. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.factor_total line 98
  14. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.nat_card_output_vertex line 101
  15. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.nat_card_output_dart line 109
  16. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.nat_card_output_total_le line 116
  17. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.poweredDart_card line 128
  18. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.output_vertex_card line 139
  19. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.output_dart_card line 154
  20. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.output_total_le_darts line 166
  21. theorem OAI.UniqueGames.Foundations.PCP.RoundSize.output_total_le line 192