OAI/Computability/DirectedFeedback/Games/ConditionalIncidences.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Soundness.ConditionalIncidences.PositionInside line 14
2. abbrev OAI.DFVSGames.Soundness.ConditionalIncidences.PositionOutside line 15
3. abbrev OAI.DFVSGames.Soundness.ConditionalIncidences.Draw line 16
4. abbrev OAI.DFVSGames.Soundness.ConditionalIncidences.InsideDraw line 17
5. def OAI.DFVSGames.Soundness.ConditionalIncidences.incidence line 19
6. def OAI.DFVSGames.Soundness.ConditionalIncidences.insideDraw line 22
7. def OAI.DFVSGames.Soundness.ConditionalIncidences.outsideRecord line 25
8. abbrev OAI.DFVSGames.Soundness.ConditionalIncidences.ObservationFibre line 29
9. abbrev OAI.DFVSGames.Soundness.ConditionalIncidences.OutsideFibre line 33
10. instance OAI.DFVSGames.Soundness.ConditionalIncidences.observationFibreFintype line 38
11. instance OAI.DFVSGames.Soundness.ConditionalIncidences.outsideFibreFintype line 42
12. def OAI.DFVSGames.Soundness.ConditionalIncidences.observationFibreEquiv line 46
13. def OAI.DFVSGames.Soundness.ConditionalIncidences.average line 70
14. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.average_equiv line 73
15. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.average_product_left line 78
16. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.average_product_mul line 89
17. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.average_coordinate_product line 99
18. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.uniform_conditional_ratio line 107
19. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.conditional_inside_average line 121
20. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.conditional_incidence_average line 141
21. abbrev OAI.DFVSGames.Soundness.ConditionalIncidences.RawSlot line 153
22. abbrev OAI.DFVSGames.Soundness.ConditionalIncidences.RawCoefficients line 156
23. def OAI.DFVSGames.Soundness.ConditionalIncidences.zeroSet line 158
24. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.mem_zeroSet line 162
25. abbrev OAI.DFVSGames.Soundness.ConditionalIncidences.RawSample line 167
26. abbrev OAI.DFVSGames.Soundness.ConditionalIncidences.RawObservationFibre line 170
27. instance OAI.DFVSGames.Soundness.ConditionalIncidences.rawObservationFibreFintype line 176
28. def OAI.DFVSGames.Soundness.ConditionalIncidences.rawObservationFibreEquiv line 182
29. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.raw_conditional_inside_average line 194
30. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.raw_conditional_ratio line 214
31. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.raw_conditional_incidence_average line 227
32. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.raw_conditional_product_incidence line 239
33. def OAI.DFVSGames.Soundness.PartnerMapCoordinates.activeOf line 274
34. def OAI.DFVSGames.Soundness.PartnerMapCoordinates.inactiveOfOutside line 276
35. def OAI.DFVSGames.Soundness.PartnerMapCoordinates.activeOfInside line 279
36. def OAI.DFVSGames.Soundness.PartnerMapCoordinates.outsideOfInactive line 282
37. def OAI.DFVSGames.Soundness.PartnerMapCoordinates.insideOfActive line 285
38. def OAI.DFVSGames.Soundness.PartnerMapCoordinates.tupleToRaw line 288
39. def OAI.DFVSGames.Soundness.PartnerMapCoordinates.tupleFromRaw line 295
40. def OAI.DFVSGames.Soundness.PartnerMapCoordinates.tupleRawEquiv line 301
41. def OAI.DFVSGames.Soundness.PartnerMapCoordinates.pointEquiv line 331
42. theorem OAI.DFVSGames.Soundness.PartnerMapCoordinates.pointEquiv_none line 334
43. theorem OAI.DFVSGames.Soundness.PartnerMapCoordinates.pointEquiv_full_first line 337
44. theorem OAI.DFVSGames.Soundness.PartnerMapCoordinates.pointEquiv_full_second line 341
45. theorem OAI.DFVSGames.Soundness.PartnerMapCoordinates.pointEquiv_single line 345
46. def OAI.DFVSGames.Soundness.PartnerMapCoordinates.partnerBasis line 351
47. def OAI.DFVSGames.Soundness.PartnerMapCoordinates.mapEquiv line 356
48. def OAI.DFVSGames.Soundness.PartnerMapCoordinates.coefficients line 359
49. theorem OAI.DFVSGames.Soundness.PartnerMapCoordinates.map_coefficients line 362
50. theorem OAI.DFVSGames.Soundness.PartnerMapCoordinates.coefficients_map line 366
51. theorem OAI.DFVSGames.Soundness.PartnerMapCoordinates.mapEquiv_apply line 370
52. theorem OAI.DFVSGames.Soundness.PartnerMapCoordinates.mapEquiv_expansion line 375
53. theorem OAI.DFVSGames.Soundness.PartnerMapCoordinates.every_map_expansion line 387
54. theorem OAI.DFVSGames.Soundness.PartnerMapCoordinates.pullback_expansion line 392
55. instance OAI.DFVSGames.Soundness.PartnerMapCoordinates.partnerMapsFintype line 411
56. theorem OAI.DFVSGames.Soundness.PartnerMapCoordinates.uniform_coefficients_maps line 416
57. theorem OAI.DFVSGames.Soundness.PartnerMapCoordinates.uniform_map_coefficients_product line 421
58. abbrev OAI.DFVSGames.Soundness.IncidenceExtraction.Triple line 438
59. def OAI.DFVSGames.Soundness.IncidenceExtraction.xorTriple line 440
60. structure OAI.DFVSGames.Soundness.IncidenceExtraction.Incidence line 442
61. def OAI.DFVSGames.Soundness.IncidenceExtraction.Incidence.accepts line 446
62. def OAI.DFVSGames.Soundness.IncidenceExtraction.Incidence.namedAccepts line 451
63. theorem OAI.DFVSGames.Soundness.IncidenceExtraction.Incidence.accepts_implies_namedAccepts line 456
64. theorem OAI.DFVSGames.Soundness.IncidenceExtraction.Incidence.namedAccepts_iff_accepts line 462
65. structure OAI.DFVSGames.Soundness.IncidenceExtraction.FullPoint line 473
66. def OAI.DFVSGames.Soundness.IncidenceExtraction.FullPoint.valid line 477
67. structure OAI.DFVSGames.Soundness.IncidenceExtraction.PartnerPoint line 482
68. def OAI.DFVSGames.Soundness.IncidenceExtraction.AugmentedAccepts line 486
69. def OAI.DFVSGames.Soundness.IncidenceExtraction.RepeatedAccepts line 493
70. theorem OAI.DFVSGames.Soundness.IncidenceExtraction.augmented_accepts_implies_repeated_accepts line 499
71. theorem OAI.DFVSGames.Soundness.IncidenceExtraction.augmented_accepts_implies_named_repeated_accepts line 514
72. structure OAI.DFVSGames.Soundness.IncidenceExtraction.Game line 533
73. structure OAI.DFVSGames.Soundness.IncidenceExtraction.Strategies line 536
74. def OAI.DFVSGames.Soundness.IncidenceExtraction.Strategies.wins line 540
75. structure OAI.DFVSGames.Soundness.IncidenceExtraction.LocalSimulation line 544
76. def OAI.DFVSGames.Soundness.IncidenceExtraction.LocalSimulation.induced line 556
77. theorem OAI.DFVSGames.Soundness.IncidenceExtraction.LocalSimulation.induced_wins line 566
78. theorem OAI.DFVSGames.Soundness.IncidenceExtraction.LocalSimulation.seeded_induced_wins line 577
79. def OAI.DFVSGames.Soundness.ConcreteExtraction.slotIndex line 594
80. def OAI.DFVSGames.Soundness.ConcreteExtraction.tripleCoordinates line 599
81. theorem OAI.DFVSGames.Soundness.ConcreteExtraction.parity_coordinates line 602
82. theorem OAI.DFVSGames.Soundness.ConcreteExtraction.retained_coordinates line 605
83. def OAI.DFVSGames.Soundness.ConcreteExtraction.fullPoint line 609
84. def OAI.DFVSGames.Soundness.ConcreteExtraction.partnerPoint line 613
85. theorem OAI.DFVSGames.Soundness.ConcreteExtraction.actual_projection_accepts line 617
86. theorem OAI.DFVSGames.Soundness.ConcreteExtraction.actual_projection_implies_named_repetition line 640
87. abbrev OAI.DFVSGames.Reduction.ActualHomogeneous.E line 663
88. abbrev OAI.DFVSGames.Reduction.ActualHomogeneous.Ambient line 664
89. def OAI.DFVSGames.Reduction.ActualHomogeneous.tau line 668
90. def OAI.DFVSGames.Reduction.ActualHomogeneous.hBasis line 669
91. def OAI.DFVSGames.Reduction.ActualHomogeneous.firstBasis line 670
92. def OAI.DFVSGames.Reduction.ActualHomogeneous.secondBasis line 671
93. def OAI.DFVSGames.Reduction.ActualHomogeneous.coordinateBasis line 672
94. theorem OAI.DFVSGames.Reduction.ActualHomogeneous.tau_hBasis line 675
95. theorem OAI.DFVSGames.Reduction.ActualHomogeneous.tau_firstBasis line 676
96. theorem OAI.DFVSGames.Reduction.ActualHomogeneous.tau_secondBasis line 677
97. theorem OAI.DFVSGames.Reduction.ActualHomogeneous.pair_fst_ite line 679
98. theorem OAI.DFVSGames.Reduction.ActualHomogeneous.pair_snd_ite line 681
99. theorem OAI.DFVSGames.Reduction.ActualHomogeneous.coordinate_decomposition line 684
100. theorem OAI.DFVSGames.Reduction.ActualHomogeneous.linearMap_expansion line 694
101. def OAI.DFVSGames.Reduction.ActualHomogeneous.homogeneous line 701
102. def OAI.DFVSGames.Reduction.ActualHomogeneous.embed line 721
103. theorem OAI.DFVSGames.Reduction.ActualHomogeneous.embed_mem line 735
104. def OAI.DFVSGames.Reduction.ActualHomogeneous.equivalence line 744
105. theorem OAI.DFVSGames.Reduction.ActualHomogeneous.finrank_E line 766
106. theorem OAI.DFVSGames.Reduction.ActualHomogeneous.finrank_homogeneous line 769