OAI/Computability/PerfectCompleteness/Reduction/TargetGameLemmas.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.Instance.occurrenceGame line 24
  2. theorem OAI.PerfectCompleteness.Instance.countSatisfied_eq_sum line 38
  3. theorem OAI.PerfectCompleteness.Instance.occurrenceGame_success line 48
  4. theorem OAI.PerfectCompleteness.Instance.occurrenceGame_value line 58
  5. def OAI.PerfectCompleteness.WeightRounding.paperScale line 84
  6. theorem OAI.PerfectCompleteness.WeightRounding.paperScale_positive line 86
  7. theorem OAI.PerfectCompleteness.WeightRounding.paperScale_error line 92
  8. theorem OAI.PerfectCompleteness.WeightRounding.paperScale_lt line 101
  9. theorem OAI.PerfectCompleteness.WeightRounding.paperScale_le_linear line 105
  10. structure OAI.PerfectCompleteness.WeightRounding.PositiveWeights line 115
  11. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.size_positive line 125
  12. def OAI.PerfectCompleteness.WeightRounding.PositiveWeights.floorCopies line 132
  13. def OAI.PerfectCompleteness.WeightRounding.PositiveWeights.floorTotal line 134
  14. def OAI.PerfectCompleteness.WeightRounding.PositiveWeights.remainder line 136
  15. def OAI.PerfectCompleteness.WeightRounding.PositiveWeights.multiplicity line 138
  16. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.floorCopies_le_scaled line 141
  17. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.scaled_lt_floorCopies_add_one line 145
  18. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.floorTotal_le line 149
  19. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.remainder_lt line 159
  20. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.sum_multiplicity line 176
  21. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.multiplicity_error_scaled line 187
  22. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.multiplicity_error line 198
  23. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.sum_rounded_weights line 211
  24. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.l1_error line 216
  25. def OAI.PerfectCompleteness.WeightRounding.PositiveWeights.copies line 223
  26. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.copies_length line 226
  27. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.copies_nonempty line 229
  28. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.copies_positive_support line 236
  29. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.copies_filter_length line 239
  30. def OAI.PerfectCompleteness.WeightRounding.PositiveWeights.weightedAcceptance line 248
  31. def OAI.PerfectCompleteness.WeightRounding.PositiveWeights.unweightedAcceptance line 251
  32. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.unweightedAcceptance_eq line 254
  33. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.acceptance_error line 263
  34. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.perfectCompleteness_preserved line 275
  35. def OAI.PerfectCompleteness.WeightRounding.PositiveWeights.output line 281
  36. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.output_length line 284
  37. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.output_nonempty line 288
  38. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.output_support line 294
  39. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.output_acceptance_error line 300
  40. def OAI.PerfectCompleteness.WeightRounding.PositiveWeights.paperOutput line 308
  41. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.paperOutput_length line 311
  42. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.paperOutput_nonempty line 315
  43. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.paperOutput_length_lt line 319
  44. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.paperOutput_length_le_linear line 325
  45. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.paperOutput_acceptance_error line 331
  46. theorem OAI.PerfectCompleteness.WeightRounding.PositiveWeights.paperOutput_perfectCompleteness line 339
  47. abbrev OAI.PerfectCompleteness.RoundedTarget.EndpointLabeling line 362
  48. def OAI.PerfectCompleteness.RoundedTarget.construct line 365
  49. theorem OAI.PerfectCompleteness.RoundedTarget.edge_length line 372
  50. theorem OAI.PerfectCompleteness.RoundedTarget.edge_support line 376
  51. theorem OAI.PerfectCompleteness.RoundedTarget.countSatisfied_eq_filter line 382
  52. theorem OAI.PerfectCompleteness.RoundedTarget.count_eq line 390
  53. def OAI.PerfectCompleteness.RoundedTarget.weightedSuccess line 399
  54. theorem OAI.PerfectCompleteness.RoundedTarget.rate_eq line 403
  55. theorem OAI.PerfectCompleteness.RoundedTarget.rate_error line 413
  56. theorem OAI.PerfectCompleteness.RoundedTarget.real_rate_error line 421
  57. def OAI.PerfectCompleteness.RoundedTarget.weightedGame line 434
  58. theorem OAI.PerfectCompleteness.RoundedTarget.weightedGame_success line 444
  59. def OAI.PerfectCompleteness.RoundedTarget.weightedValue line 454
  60. theorem OAI.PerfectCompleteness.RoundedTarget.weightedSuccess_le_value line 460
  61. theorem OAI.PerfectCompleteness.RoundedTarget.weightedValue_attained line 468
  62. theorem OAI.PerfectCompleteness.RoundedTarget.completeness_preserved line 478
  63. theorem OAI.PerfectCompleteness.RoundedTarget.complete_value_eq_one line 490
  64. theorem OAI.PerfectCompleteness.RoundedTarget.value_le line 498
  65. theorem OAI.PerfectCompleteness.RoundedTarget.value_distance line 520
  66. theorem OAI.PerfectCompleteness.RoundedTarget.soundAt_of_weighted_bound line 541
  67. def OAI.PerfectCompleteness.RoundedTarget.paper line 550
  68. theorem OAI.PerfectCompleteness.RoundedTarget.paper_edge_length line 554
  69. theorem OAI.PerfectCompleteness.RoundedTarget.paper_edge_length_le_linear line 558
  70. theorem OAI.PerfectCompleteness.RoundedTarget.paper_value_distance line 564
  71. theorem OAI.PerfectCompleteness.RoundedTarget.paper_value_le line 572
  72. theorem OAI.PerfectCompleteness.RoundedTarget.paper_soundAt_of_weighted_bound line 583
  73. theorem OAI.PerfectCompleteness.RoundedTarget.paper_complete_value_eq_one line 593