OAI/Computability/DirectedFeedback/Games/Overlay.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.PCP.Overlay.originalPortGraph line 16
  2. def OAI.DFVSGames.Foundations.PCP.Overlay.rotate line 20
  3. theorem OAI.DFVSGames.Foundations.PCP.Overlay.rotate_involutive line 25
  4. def OAI.DFVSGames.Foundations.PCP.Overlay.portGraph line 34
  5. theorem OAI.DFVSGames.Foundations.PCP.Overlay.portGraph_rot_inl line 42
  6. theorem OAI.DFVSGames.Foundations.PCP.Overlay.portGraph_rot_inr line 47
  7. def OAI.DFVSGames.Foundations.PCP.Overlay.constraintGraph line 52
  8. theorem OAI.DFVSGames.Foundations.PCP.Overlay.constraintGraph_tail line 66
  9. theorem OAI.DFVSGames.Foundations.PCP.Overlay.constraintGraph_portGraph line 69
  10. theorem OAI.DFVSGames.Foundations.PCP.Overlay.edgeSatisfied_inl line 73
  11. theorem OAI.DFVSGames.Foundations.PCP.Overlay.edgeSatisfied_inr line 83
  12. theorem OAI.DFVSGames.Foundations.PCP.Overlay.complete line 87
  13. theorem OAI.DFVSGames.Foundations.PCP.Overlay.satisfiable_iff line 97
  14. theorem OAI.DFVSGames.Foundations.PCP.Overlay.rejectionCount_eq line 109
  15. theorem OAI.DFVSGames.Foundations.PCP.Overlay.card_ports line 118
  16. theorem OAI.DFVSGames.Foundations.PCP.Overlay.card_darts line 121
  17. theorem OAI.DFVSGames.Foundations.PCP.Overlay.operator_mix line 130
  18. theorem OAI.DFVSGames.Foundations.PCP.Overlay.energy_convex_mix line 149
  19. theorem OAI.DFVSGames.Foundations.PCP.Overlay.energy_bound line 164
  20. theorem OAI.DFVSGames.Foundations.PCP.Overlay.energy_bound_three_quarters line 199
  21. theorem OAI.DFVSGames.Foundations.PCP.Overlay.spectralCertificate_seven_eighths line 218
  22. theorem OAI.DFVSGames.Foundations.PCP.Overlay.constraintGraph_spectralCertificate line 231
  23. def OAI.DFVSGames.Foundations.PCP.LazySmoothing.bitCount line 248
  24. def OAI.DFVSGames.Foundations.PCP.LazySmoothing.binomialMean line 251
  25. def OAI.DFVSGames.Foundations.PCP.LazySmoothing.splitTape line 254
  26. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.bitCount_succ line 262
  27. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.mean_congr line 266
  28. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.mean_const line 271
  29. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.mean_add line 274
  30. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.mean_sub line 278
  31. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.mean_mul line 282
  32. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.mean_zero line 286
  33. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.expect_bool line 289
  34. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.mean_succ line 293
  35. def OAI.DFVSGames.Foundations.PCP.LazySmoothing.score line 304
  36. def OAI.DFVSGames.Foundations.PCP.LazySmoothing.scoreMean line 306
  37. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.scoreMean_zero line 309
  38. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.scoreMean_succ line 312
  39. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.score_identity line 331
  40. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.score_mean_zero line 341
  41. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.score_second_moment line 348
  42. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.score_difference line 367
  43. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.adjacent_difference_sq line 373
  44. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.adjacent_difference_le line 407
  45. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.mean_shift_le line 420
  46. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.mean_ordered_difference_le line 439
  47. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.mean_window_le line 445
  48. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.square_window_le line 467
  49. theorem OAI.DFVSGames.Foundations.PCP.LazySmoothing.modal_transfer line 493
  50. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.lazyRotate line 516
  51. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.lazyRotate_involutive line 520
  52. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.lazyGraph line 528
  53. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.lazyGraph_rot_false line 536
  54. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.lazyGraph_rot_true line 539
  55. theorem OAI.DFVSGames.Foundations.PCP.PoweringLazy.operator_binomialMean line 550
  56. theorem OAI.DFVSGames.Foundations.PCP.PoweringLazy.averagingOperator_lazy line 558
  57. theorem OAI.DFVSGames.Foundations.PCP.PoweringLazy.iterate_lazy_eq_binomialMean line 570
  58. theorem OAI.DFVSGames.Foundations.PCP.PoweringLazy.iterate_mem_Icc line 584
  59. theorem OAI.DFVSGames.Foundations.PCP.PoweringLazy.lazy_endpoint_modal_transfer line 599
  60. def OAI.DFVSGames.Foundations.PCP.LazyConstraint.constraintGraph line 619
  61. theorem OAI.DFVSGames.Foundations.PCP.LazyConstraint.constraintGraph_tail line 631
  62. theorem OAI.DFVSGames.Foundations.PCP.LazyConstraint.constraintGraph_reverse line 634
  63. theorem OAI.DFVSGames.Foundations.PCP.LazyConstraint.constraintGraph_portGraph line 637
  64. theorem OAI.DFVSGames.Foundations.PCP.LazyConstraint.edgeSatisfied_false line 641
  65. theorem OAI.DFVSGames.Foundations.PCP.LazyConstraint.edgeSatisfied_true line 645
  66. theorem OAI.DFVSGames.Foundations.PCP.LazyConstraint.complete line 654
  67. theorem OAI.DFVSGames.Foundations.PCP.LazyConstraint.complete_iff line 664
  68. theorem OAI.DFVSGames.Foundations.PCP.LazyConstraint.satisfiable_iff line 675
  69. theorem OAI.DFVSGames.Foundations.PCP.LazyConstraint.rejectionCount_eq line 683
  70. theorem OAI.DFVSGames.Foundations.PCP.LazyConstraint.card_ports line 692
  71. theorem OAI.DFVSGames.Foundations.PCP.LazyConstraint.card_darts line 696
  72. theorem OAI.DFVSGames.Foundations.PCP.LazyConstraint.rejection_density_eq_half line 700
  73. def OAI.DFVSGames.Foundations.PCP.ConstraintGraph.rejectionCounts line 722
  74. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.rejectionCounts_nonempty line 726
  75. def OAI.DFVSGames.Foundations.PCP.ConstraintGraph.minimumRejections line 731
  76. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.minimumRejections_le line 734
  77. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.exists_minimizer line 739
  78. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.le_minimumRejections_iff line 746
  79. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.minimumRejections_le_card line 756
  80. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.rejectionCount_eq_zero_iff line 763
  81. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.minimumRejections_eq_zero_iff line 778
  82. def OAI.DFVSGames.Foundations.PCP.ConstraintGraph.gap line 788
  83. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.gap_nonnegative line 791
  84. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.gap_le_one line 794
  85. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.gap_eq_zero_iff line 800
  86. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.le_gap_iff line 806
  87. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.inverse_card_le_gap_of_unsatisfiable line 819
  88. def OAI.DFVSGames.Foundations.PCP.ConstraintGraph.reindex line 833
  89. def OAI.DFVSGames.Foundations.PCP.ConstraintGraph.labelingEquiv line 847
  90. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.reindex_edgeSatisfied line 853
  91. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.reindex_rejectionCount line 860
  92. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.rejectionCounts_reindex line 884
  93. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.minimumRejections_reindex line 901
  94. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.gap_reindex line 907
  95. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.satisfiable_reindex line 913