OAI/Computability/BinPacking/PCP/PoweringFinalConstants.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGames.Foundations.PCP.PoweringNumeric.min_density_ratio line 15
  2. theorem OAI.BinPackingGames.Foundations.PCP.PoweringNumeric.count_moment_ratio_lower line 41
  3. def OAI.BinPackingGames.Foundations.PCP.PoweringSoundness.center line 75
  4. theorem OAI.BinPackingGames.Foundations.PCP.PoweringSoundness.le_center line 77
  5. def OAI.BinPackingGames.Foundations.PCP.PoweringSoundness.gain line 85
  6. def OAI.BinPackingGames.Foundations.PCP.PoweringSoundness.decodedError line 92
  7. def OAI.BinPackingGames.Foundations.PCP.PoweringSoundness.poweredRejection line 97
  8. theorem OAI.BinPackingGames.Foundations.PCP.PoweringSoundness.witness_bit_eq line 103
  9. theorem OAI.BinPackingGames.Foundations.PCP.PoweringSoundness.modal_witness_mean line 116
  10. theorem OAI.BinPackingGames.Foundations.PCP.PoweringSoundness.rejection_lower_bound line 141
  11. theorem OAI.BinPackingGames.Foundations.PCP.PoweringGap.gain_nonneg line 242
  12. theorem OAI.BinPackingGames.Foundations.PCP.PoweringGap.uniform_count_gap line 251
  13. def OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.wordEquiv line 314
  14. def OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.walkEquiv line 320
  15. def OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.addressEquiv line 323
  16. def OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.labelEquiv line 329
  17. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.wordEnd_map line 341
  18. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.endpoint_map line 349
  19. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.reach_iff line 353
  20. def OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.ballEquiv line 364
  21. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.wordToBall_map line 370
  22. def OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.pullSelector line 376
  23. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.decode_pullSelector line 384
  24. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.decode_transport line 390
  25. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.opinionAt_pullSelector line 400
  26. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.advanceTail_map line 413
  27. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.edgeAt_map line 421
  28. def OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.pullAccepts line 436
  29. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.pathAccepts_map line 439
  30. def OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.dartEquiv line 465
  31. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.edgeSatisfied_map line 468
  32. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.rejectionCount_map line 481
  33. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.satisfiable_iff line 502
  34. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.pullReverse line 519
  35. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.base_edgeSatisfied_map line 525
  36. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.base_rejectionCount_map line 535
  37. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.uniform_count_gap line 563
  38. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap line 602
  39. theorem OAI.BinPackingGames.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap_at line 641
  40. abbrev OAI.BinPackingGames.Foundations.PCP.PoweringFinalConstants.Alphabet line 665
  41. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFinalConstants.card_alphabet line 667
  42. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFinalConstants.card_alphabet_eq_final line 670
  43. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFinalConstants.center_eq line 673
  44. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFinalConstants.walkLength_eq line 679
  45. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFinalConstants.spectral_denominator_eq line 685
  46. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFinalConstants.gain_eq line 689
  47. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFinalConstants.gain_card_eq line 707
  48. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFinalConstants.scaled_bound_eq line 713
  49. theorem OAI.BinPackingGames.Foundations.PCP.PoweringFinalConstants.composed_scaled_gap line 723