OAI/Computability/MinUncut/PCP/PoweringReturn.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.PCP.PoweringReturn.portConsEquiv line 14
2. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.mean_word_cons_head line 27
3. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.mean_word_cons_tail line 35
4. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.iterateOperator_succ_right line 43
5. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.mean_wordEnd line 50
6. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.mean_pivot_endpoints line 71
7. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.mean_edge_endpoints line 113
8. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.bit_bool line 137
9. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.mean_edge_bit line 140
10. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.mean_marked_bit line 144
11. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.edgeAt_zero line 154
12. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.word_first_hit_mean line 158
13. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.word_hit_mean line 169
14. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.word_pair_hit_mean line 196
15. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.hit_mean line 254
16. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.pair_hit_mean line 270
17. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReturn.pair_event_mean line 291
18. def OAI.MinUncutGames.Foundations.PCP.PoweringOpinions.opinionAt line 312
19. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinions.opinionAt_eq_decode line 319
20. def OAI.MinUncutGames.Foundations.PCP.PoweringOpinions.honestLabels line 327
21. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinions.opinionAt_honest line 330
22. def OAI.MinUncutGames.Foundations.PCP.PoweringOpinions.sampleOpinion line 340
23. def OAI.MinUncutGames.Foundations.PCP.PoweringOpinions.decoded line 345
24. def OAI.MinUncutGames.Foundations.PCP.PoweringOpinions.matchFn line 350
25. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinions.matchFn_mem_Icc line 356
26. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinions.decoded_modal_baseline line 366
27. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinions.decoded_modal_near line 376
28. def OAI.MinUncutGames.Foundations.PCP.PoweringReach.ReachLE line 404
29. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReach.reach_refl line 407
30. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReach.reach_mono line 410
31. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReach.reach_prepend line 415
32. def OAI.MinUncutGames.Foundations.PCP.PoweringReach.reversePorts line 422
33. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReach.reversePorts_length line 426
34. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReach.walkEnd_reversePorts line 432
35. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReach.wordEnd_eq_walkEnd_ofFn line 443
36. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReach.reach_reverse line 453
37. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReach.tail_reach line 465
38. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReach.head_reach_endpoint line 479
39. def OAI.MinUncutGames.Foundations.PCP.PoweringReach.tailFromStart line 493
40. def OAI.MinUncutGames.Foundations.PCP.PoweringReach.headFromEnd line 497
41. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReach.tailFromStart_val line 501
42. theorem OAI.MinUncutGames.Foundations.PCP.PoweringReach.headFromEnd_val line 505
43. def OAI.MinUncutGames.Foundations.PCP.PoweringTest.baseGraph line 519
44. def OAI.MinUncutGames.Foundations.PCP.PoweringTest.pathAccepts line 528
45. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.pathAccepts_eq_true_iff line 536
46. abbrev OAI.MinUncutGames.Foundations.PCP.PoweringTest.Dart line 547
47. def OAI.MinUncutGames.Foundations.PCP.PoweringTest.reverseDart line 549
48. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.reverseDart_involutive line 559
49. def OAI.MinUncutGames.Foundations.PCP.PoweringTest.poweredGraph line 564
50. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.poweredGraph_tail_false line 576
51. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.poweredGraph_tail_true line 581
52. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.poweredGraph_edgeSatisfied line 586
53. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.rejection_mean_eq_path_mean line 595
54. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.pathAccepts_honest line 606
55. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.perfect_completeness line 620
56. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.preserves_satisfiability line 631
57. def OAI.MinUncutGames.Foundations.PCP.PoweringTest.decodedBad line 643
58. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.decodedBad_eq_true_iff line 647
59. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.decodedBad_rot line 653
60. def OAI.MinUncutGames.Foundations.PCP.PoweringTest.witness line 662
61. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.witness_bad line 674
62. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.witness_implies_path_rejection line 682
63. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTest.witness_implies_rejection line 709