OAI/Computability/DirectedFeedback/Games/KernelCardinality.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Soundness.KernelCardinality.Kernel line 13
2. def OAI.DFVSGames.Soundness.KernelCardinality.kernelEquiv line 15
3. instance OAI.DFVSGames.Soundness.KernelCardinality.kernelFintype line 30
4. theorem OAI.DFVSGames.Soundness.KernelCardinality.kernel_card line 34
5. theorem OAI.DFVSGames.Soundness.KernelCardinality.kernel_card_of_active_card line 43
6. theorem OAI.DFVSGames.Gadget.LinearKernelCount.card_binary_space line 59
7. theorem OAI.DFVSGames.Gadget.LinearKernelCount.kernel_card_mul_pow_rank line 63
8. theorem OAI.DFVSGames.Gadget.LinearKernelCount.card_source_pos line 70
9. theorem OAI.DFVSGames.Gadget.LinearKernelCount.kernel_card_eq_pow_sub_rank line 74
10. theorem OAI.DFVSGames.Gadget.LinearKernelCount.zero_event_card_mul_pow_rank line 82
11. theorem OAI.DFVSGames.Gadget.LinearKernelCount.zero_event_card_mul_pow_le line 86
12. theorem OAI.DFVSGames.Gadget.LinearKernelCount.zero_event_finset_count_mul_pow_rank line 95
13. theorem OAI.DFVSGames.Gadget.LinearKernelCount.zero_event_finset_count_mul_pow_le line 102
14. abbrev OAI.DFVSGames.Soundness.PartnerLinear.SourceCoordinates line 120
15. abbrev OAI.DFVSGames.Soundness.PartnerLinear.Active line 121
16. abbrev OAI.DFVSGames.Soundness.PartnerLinear.Inactive line 122
17. abbrev OAI.DFVSGames.Soundness.PartnerLinear.PartnerCoordinates line 123
18. def OAI.DFVSGames.Soundness.PartnerLinear.sourceCoordinates line 125
19. def OAI.DFVSGames.Soundness.PartnerLinear.sourceFromCoordinates line 128
20. def OAI.DFVSGames.Soundness.PartnerLinear.sourceEquiv line 134
21. def OAI.DFVSGames.Soundness.PartnerLinear.partnerCoordinates line 152
22. def OAI.DFVSGames.Soundness.PartnerLinear.partnerFromCoordinates line 157
23. def OAI.DFVSGames.Soundness.PartnerLinear.partnerEquiv line 168
24. instance OAI.DFVSGames.Soundness.PartnerLinear.sourceAddCommGroup line 197
25. instance OAI.DFVSGames.Soundness.PartnerLinear.sourceModule line 200
26. instance OAI.DFVSGames.Soundness.PartnerLinear.partnerAddCommGroup line 203
27. instance OAI.DFVSGames.Soundness.PartnerLinear.partnerModule line 206
28. def OAI.DFVSGames.Soundness.PartnerLinear.sourceLinearEquiv line 209
29. def OAI.DFVSGames.Soundness.PartnerLinear.partnerLinearEquiv line 212
30. instance OAI.DFVSGames.Soundness.PartnerLinear.sourceFintype line 215
31. instance OAI.DFVSGames.Soundness.PartnerLinear.partnerFintype line 219
32. theorem OAI.DFVSGames.Soundness.PartnerLinear.source_add line 223
33. theorem OAI.DFVSGames.Soundness.PartnerLinear.source_zero line 232
34. theorem OAI.DFVSGames.Soundness.PartnerLinear.partner_add line 238
35. theorem OAI.DFVSGames.Soundness.PartnerLinear.partner_zero line 251
36. def OAI.DFVSGames.Soundness.PartnerLinear.projection line 257
37. theorem OAI.DFVSGames.Soundness.PartnerLinear.projection_apply line 266
38. theorem OAI.DFVSGames.Soundness.PartnerLinear.projection_surjective line 269
39. theorem OAI.DFVSGames.Soundness.PartnerLinear.mem_projection_ker line 272
40. instance OAI.DFVSGames.Soundness.PartnerLinear.sourceFiniteDimensional line 278
41. instance OAI.DFVSGames.Soundness.PartnerLinear.partnerFiniteDimensional line 282
42. def OAI.DFVSGames.Soundness.PartnerLinear.kernelEquiv line 286
43. theorem OAI.DFVSGames.Soundness.PartnerLinear.projection_ker_card line 293
44. theorem OAI.DFVSGames.Soundness.PartnerLinear.projection_ker_finrank line 298
45. theorem OAI.DFVSGames.Soundness.PartnerLinear.projection_ker_finrank_of_card line 305
46. theorem OAI.DFVSGames.Soundness.PartnerLinear.source_finrank line 310
47. theorem OAI.DFVSGames.Soundness.PartnerLinear.disjoint_projection_kernels line 315
48. def OAI.DFVSGames.Soundness.PartnerLinear.sourceTau line 328
49. def OAI.DFVSGames.Soundness.PartnerLinear.partnerTau line 331
50. theorem OAI.DFVSGames.Soundness.PartnerLinear.sourceTau_apply line 335
51. theorem OAI.DFVSGames.Soundness.PartnerLinear.partnerTau_apply line 336
52. theorem OAI.DFVSGames.Soundness.PartnerLinear.tau_comp_projection line 339
53. def OAI.DFVSGames.Soundness.ZeroInformation.Fibre line 353
54. def OAI.DFVSGames.Soundness.ZeroInformation.Inside line 356
55. def OAI.DFVSGames.Soundness.ZeroInformation.Outside line 358
56. def OAI.DFVSGames.Soundness.ZeroInformation.fibreInside line 361
57. def OAI.DFVSGames.Soundness.ZeroInformation.fibreOutside line 364
58. def OAI.DFVSGames.Soundness.ZeroInformation.assemble line 367
59. theorem OAI.DFVSGames.Soundness.ZeroInformation.inside_assemble line 377
60. theorem OAI.DFVSGames.Soundness.ZeroInformation.outside_assemble line 383
61. theorem OAI.DFVSGames.Soundness.ZeroInformation.assemble_split line 390
62. theorem OAI.DFVSGames.Soundness.ZeroInformation.fibre_product line 399
63. def OAI.DFVSGames.Soundness.ZeroInformation.mass line 408
64. theorem OAI.DFVSGames.Soundness.ZeroInformation.mass_scale line 412
65. theorem OAI.DFVSGames.Soundness.ZeroInformation.rectangular_mass line 418
66. theorem OAI.DFVSGames.Soundness.ZeroInformation.conditional_inside_identity line 430
67. abbrev OAI.DFVSGames.Soundness.ZeroInformation.Bits line 441
68. def OAI.DFVSGames.Soundness.ZeroInformation.zero line 443
69. def OAI.DFVSGames.Soundness.ZeroInformation.add line 445
70. def OAI.DFVSGames.Soundness.ZeroInformation.scale line 447
71. theorem OAI.DFVSGames.Soundness.ZeroInformation.scale_zero line 450
72. def OAI.DFVSGames.Soundness.ZeroInformation.rowSum line 455
73. theorem OAI.DFVSGames.Soundness.ZeroInformation.rowSum_congr line 458
74. def OAI.DFVSGames.Soundness.ZeroInformation.pullbackRow line 463
75. theorem OAI.DFVSGames.Soundness.ZeroInformation.pullbackRow_index_independent line 470
76. theorem OAI.DFVSGames.Soundness.ZeroInformation.pullbackRow_from_outside_names line 488
77. theorem OAI.DFVSGames.Soundness.ZeroInformation.zero_third_bit line 502
78. abbrev OAI.DFVSGames.Soundness.ZeroInformation.FirstRow line 506
79. abbrev OAI.DFVSGames.Soundness.ZeroInformation.SecondRow line 508
80. structure OAI.DFVSGames.Soundness.ZeroInformation.FirstInput line 511
81. structure OAI.DFVSGames.Soundness.ZeroInformation.SecondInput line 515
82. def OAI.DFVSGames.Soundness.ZeroInformation.partnerQuestion line 519
83. def OAI.DFVSGames.Soundness.ZeroInformation.partnerRow line 523
84. theorem OAI.DFVSGames.Soundness.ZeroInformation.partnerRow_pullback line 529
85. def OAI.DFVSGames.Soundness.ZeroInformation.firstInput line 536
86. def OAI.DFVSGames.Soundness.ZeroInformation.secondInput line 541
87. def OAI.DFVSGames.Soundness.ZeroInformation.decodeIndex line 547
88. theorem OAI.DFVSGames.Soundness.ZeroInformation.decodeIndex_name line 552
89. def OAI.DFVSGames.Soundness.ZeroInformation.reconstructQuestion line 561
90. theorem OAI.DFVSGames.Soundness.ZeroInformation.reconstructQuestion_actual line 564
91. def OAI.DFVSGames.Soundness.ZeroInformation.reconstructFirst line 572
92. theorem OAI.DFVSGames.Soundness.ZeroInformation.first_input_reconstruction line 580
93. def OAI.DFVSGames.Soundness.ZeroInformation.reconstructSecond line 605
94. theorem OAI.DFVSGames.Soundness.ZeroInformation.second_input_reconstruction line 611
95. def OAI.DFVSGames.Soundness.ZeroInformation.FirstPoint line 635
96. def OAI.DFVSGames.Soundness.ZeroInformation.SecondPoint line 639
97. def OAI.DFVSGames.Soundness.ZeroInformation.FirstInput.suppliedMap line 647
98. def OAI.DFVSGames.Soundness.ZeroInformation.SecondInput.suppliedMap line 651
99. def OAI.DFVSGames.Soundness.ZeroInformation.projectFull line 655
100. def OAI.DFVSGames.Soundness.ZeroInformation.projectSingles line 659
101. def OAI.DFVSGames.Soundness.ZeroInformation.partnerProjection line 663
102. theorem OAI.DFVSGames.Soundness.ZeroInformation.partnerRow_project line 675
103. theorem OAI.DFVSGames.Soundness.ZeroInformation.supplied_map_pullback line 687