OAI/Computability/MinUncut/PCP/Overlay.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.PCP.Overlay.originalPortGraph line 15
2. def OAI.MinUncutGames.Foundations.PCP.Overlay.rotate line 19
3. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.rotate_involutive line 24
4. def OAI.MinUncutGames.Foundations.PCP.Overlay.portGraph line 33
5. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.portGraph_rot_inl line 41
6. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.portGraph_rot_inr line 46
7. def OAI.MinUncutGames.Foundations.PCP.Overlay.constraintGraph line 51
8. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.constraintGraph_tail line 65
9. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.constraintGraph_portGraph line 68
10. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.edgeSatisfied_inl line 72
11. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.edgeSatisfied_inr line 82
12. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.complete line 86
13. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.satisfiable_iff line 96
14. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.rejectionCount_eq line 108
15. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.card_ports line 117
16. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.card_darts line 120
17. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.operator_mix line 131
18. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.energy_convex_mix line 150
19. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.energy_bound line 165
20. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.energy_bound_three_quarters line 200
21. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.spectralCertificate_seven_eighths line 219
22. theorem OAI.MinUncutGames.Foundations.PCP.Overlay.constraintGraph_spectralCertificate line 232
23. def OAI.MinUncutGames.Foundations.PCP.LazySmoothing.bitCount line 251
24. def OAI.MinUncutGames.Foundations.PCP.LazySmoothing.binomialMean line 254
25. def OAI.MinUncutGames.Foundations.PCP.LazySmoothing.splitTape line 257
26. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.bitCount_succ line 265
27. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.mean_congr line 269
28. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.mean_const line 274
29. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.mean_add line 277
30. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.mean_sub line 281
31. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.mean_mul line 285
32. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.mean_zero line 289
33. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.expect_bool line 292
34. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.mean_succ line 296
35. def OAI.MinUncutGames.Foundations.PCP.LazySmoothing.score line 307
36. def OAI.MinUncutGames.Foundations.PCP.LazySmoothing.scoreMean line 309
37. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.scoreMean_zero line 312
38. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.scoreMean_succ line 315
39. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.score_identity line 334
40. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.score_mean_zero line 344
41. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.score_second_moment line 351
42. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.score_difference line 370
43. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.adjacent_difference_sq line 376
44. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.adjacent_difference_le line 410
45. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.mean_shift_le line 423
46. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.mean_ordered_difference_le line 442
47. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.mean_window_le line 448
48. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.square_window_le line 470
49. theorem OAI.MinUncutGames.Foundations.PCP.LazySmoothing.modal_transfer line 496
50. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.lazyRotate line 519
51. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.lazyRotate_involutive line 523
52. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.lazyGraph line 531
53. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.lazyGraph_rot_false line 539
54. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.lazyGraph_rot_true line 542
55. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLazy.operator_binomialMean line 553
56. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLazy.averagingOperator_lazy line 561
57. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLazy.iterate_lazy_eq_binomialMean line 573
58. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLazy.iterate_mem_Icc line 587
59. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLazy.lazy_endpoint_modal_transfer line 602
60. def OAI.MinUncutGames.Foundations.PCP.LazyConstraint.constraintGraph line 623
61. theorem OAI.MinUncutGames.Foundations.PCP.LazyConstraint.constraintGraph_tail line 635
62. theorem OAI.MinUncutGames.Foundations.PCP.LazyConstraint.constraintGraph_reverse line 638
63. theorem OAI.MinUncutGames.Foundations.PCP.LazyConstraint.constraintGraph_portGraph line 641
64. theorem OAI.MinUncutGames.Foundations.PCP.LazyConstraint.edgeSatisfied_false line 645
65. theorem OAI.MinUncutGames.Foundations.PCP.LazyConstraint.edgeSatisfied_true line 649
66. theorem OAI.MinUncutGames.Foundations.PCP.LazyConstraint.complete line 658
67. theorem OAI.MinUncutGames.Foundations.PCP.LazyConstraint.complete_iff line 668
68. theorem OAI.MinUncutGames.Foundations.PCP.LazyConstraint.satisfiable_iff line 679
69. theorem OAI.MinUncutGames.Foundations.PCP.LazyConstraint.rejectionCount_eq line 687
70. theorem OAI.MinUncutGames.Foundations.PCP.LazyConstraint.card_ports line 696
71. theorem OAI.MinUncutGames.Foundations.PCP.LazyConstraint.card_darts line 700
72. theorem OAI.MinUncutGames.Foundations.PCP.LazyConstraint.rejection_density_eq_half line 704