OAI/Computability/DirectedFeedback/Games/Explicit.lean

GitHub source file

136 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Reduction.Explicit.pairs line 11
  2. theorem OAI.DFVSGames.Reduction.Explicit.length_pairs line 14
  3. theorem OAI.DFVSGames.Reduction.Explicit.mem_pairs line 23
  4. def OAI.DFVSGames.Reduction.Explicit.words line 27
  5. theorem OAI.DFVSGames.Reduction.Explicit.length_words line 31
  6. theorem OAI.DFVSGames.Reduction.Explicit.mem_words line 39
  7. abbrev OAI.DFVSGames.Reduction.Explicit.CoordinateOutcome line 67
  8. def OAI.DFVSGames.Reduction.Explicit.edgeOutcomes line 69
  9. def OAI.DFVSGames.Reduction.Explicit.edgeCount line 74
  10. theorem OAI.DFVSGames.Reduction.Explicit.length_edgeOutcomes line 77
  11. theorem OAI.DFVSGames.Reduction.Explicit.edgeCount_pos line 85
  12. theorem OAI.DFVSGames.Reduction.Explicit.edgeOutcomes_nonempty line 89
  13. theorem OAI.DFVSGames.Reduction.Explicit.edgeCount_mono line 96
  14. theorem OAI.DFVSGames.Reduction.Explicit.product_pow line 101
  15. theorem OAI.DFVSGames.Reduction.Explicit.edgeCount_polynomial_bound line 109
  16. theorem OAI.DFVSGames.Reduction.ActualEnumeration.nodup_pairs line 135
  17. def OAI.DFVSGames.Reduction.ActualEnumeration.functions line 138
  18. theorem OAI.DFVSGames.Reduction.ActualEnumeration.length_functions line 143
  19. theorem OAI.DFVSGames.Reduction.ActualEnumeration.mem_functions line 149
  20. theorem OAI.DFVSGames.Reduction.ActualEnumeration.nodup_functions line 159
  21. abbrev OAI.DFVSGames.Reduction.ActualEnumeration.Coefficients line 175
  22. def OAI.DFVSGames.Reduction.ActualEnumeration.fromCoefficients line 177
  23. def OAI.DFVSGames.Reduction.ActualEnumeration.toCoefficients line 187
  24. theorem OAI.DFVSGames.Reduction.ActualEnumeration.to_fromCoefficients line 190
  25. theorem OAI.DFVSGames.Reduction.ActualEnumeration.from_toCoefficients line 199
  26. def OAI.DFVSGames.Reduction.ActualEnumeration.coefficientEquiv line 205
  27. def OAI.DFVSGames.Reduction.ActualEnumeration.allLinearMaps line 211
  28. theorem OAI.DFVSGames.Reduction.ActualEnumeration.length_allLinearMaps line 214
  29. theorem OAI.DFVSGames.Reduction.ActualEnumeration.mem_allLinearMaps line 221
  30. theorem OAI.DFVSGames.Reduction.ActualEnumeration.nodup_allLinearMaps line 228
  31. theorem OAI.DFVSGames.Reduction.ActualEnumeration.cardinal_linearMaps line 233
  32. def OAI.DFVSGames.Reduction.ActualEnumeration.vectors line 243
  33. theorem OAI.DFVSGames.Reduction.ActualEnumeration.length_vectors line 246
  34. theorem OAI.DFVSGames.Reduction.ActualEnumeration.mem_vectors line 249
  35. theorem OAI.DFVSGames.Reduction.ActualEnumeration.nodup_vectors line 253
  36. abbrev OAI.DFVSGames.Reduction.ActualEnumeration.Ambient line 256
  37. def OAI.DFVSGames.Reduction.ActualEnumeration.ambientVectors line 259
  38. theorem OAI.DFVSGames.Reduction.ActualEnumeration.length_ambientVectors line 261
  39. theorem OAI.DFVSGames.Reduction.ActualEnumeration.mem_ambientVectors line 264
  40. theorem OAI.DFVSGames.Reduction.ActualEnumeration.nodup_ambientVectors line 267
  41. abbrev OAI.DFVSGames.Reduction.ActualEnumeration.Query line 270
  42. def OAI.DFVSGames.Reduction.ActualEnumeration.queries line 272
  43. theorem OAI.DFVSGames.Reduction.ActualEnumeration.mem_queries line 275
  44. theorem OAI.DFVSGames.Reduction.ActualEnumeration.nodup_queries line 279
  45. theorem OAI.DFVSGames.Reduction.ActualEnumeration.length_queries line 283
  46. abbrev OAI.DFVSGames.Reduction.ActualEnumeration.Outcome line 288
  47. def OAI.DFVSGames.Reduction.ActualEnumeration.outcomes line 292
  48. theorem OAI.DFVSGames.Reduction.ActualEnumeration.length_outcomes line 297
  49. theorem OAI.DFVSGames.Reduction.ActualEnumeration.mem_outcomes line 307
  50. theorem OAI.DFVSGames.Reduction.ActualEnumeration.nodup_outcomes line 316
  51. def OAI.DFVSGames.Reduction.ActualEnumeration.indexedOutcomes line 324
  52. theorem OAI.DFVSGames.Reduction.ActualEnumeration.length_indexedOutcomes line 328
  53. theorem OAI.DFVSGames.Reduction.ActualEnumeration.mem_indexedOutcomes line 333
  54. theorem OAI.DFVSGames.Reduction.ActualEnumeration.nodup_indexedOutcomes line 340
  55. theorem OAI.DFVSGames.Reduction.ActualEnumeration.indexedOutcomes_nonempty line 345
  56. theorem OAI.DFVSGames.Reduction.ActualEnumeration.length_indexedOutcomes_polynomial_bound line 352
  57. def OAI.DFVSGames.Decoder.PaddedLaw.pushforwardWeight line 380
  58. theorem OAI.DFVSGames.Decoder.PaddedLaw.pushforwardWeight_pi line 383
  59. theorem OAI.DFVSGames.Decoder.PaddedLaw.pushforwardWeight_joint_uniform_intercept line 395
  60. abbrev OAI.DFVSGames.Decoder.PaddedLaw.BlockDraw line 422
  61. def OAI.DFVSGames.Decoder.PaddedLaw.decodeSlot line 424
  62. theorem OAI.DFVSGames.Decoder.PaddedLaw.slotIndex_decodeSlot line 427
  63. def OAI.DFVSGames.Decoder.PaddedLaw.blockAmbient line 430
  64. def OAI.DFVSGames.Decoder.PaddedLaw.blockSlopes line 434
  65. def OAI.DFVSGames.Decoder.PaddedLaw.blockThird line 437
  66. theorem OAI.DFVSGames.Decoder.PaddedLaw.blockSlopes_full line 440
  67. theorem OAI.DFVSGames.Decoder.PaddedLaw.blockSlopes_first line 444
  68. theorem OAI.DFVSGames.Decoder.PaddedLaw.blockSlopes_second line 449
  69. theorem OAI.DFVSGames.Decoder.PaddedLaw.blockSlopes_third line 454
  70. def OAI.DFVSGames.Decoder.PaddedLaw.singletonPositions line 458
  71. def OAI.DFVSGames.Decoder.PaddedLaw.drawSlots line 461
  72. def OAI.DFVSGames.Decoder.PaddedLaw.drawCoefficients line 466
  73. def OAI.DFVSGames.Decoder.PaddedLaw.paddedMap line 478
  74. theorem OAI.DFVSGames.Decoder.PaddedLaw.ambientCoefficients_draw line 484
  75. def OAI.DFVSGames.Decoder.PaddedLaw.interceptShift line 496
  76. theorem OAI.DFVSGames.Decoder.PaddedLaw.paddedMap_toCoefficients line 499
  77. theorem OAI.DFVSGames.Decoder.PaddedLaw.uniform_rawMaps line 516
  78. abbrev OAI.DFVSGames.Decoder.PaddedLaw.RawTuple line 521
  79. def OAI.DFVSGames.Decoder.PaddedLaw.rawTupleEquiv line 524
  80. def OAI.DFVSGames.Decoder.PaddedLaw.tupleDraw line 545
  81. theorem OAI.DFVSGames.Decoder.PaddedLaw.tupleDraw_ambient line 551
  82. theorem OAI.DFVSGames.Decoder.PaddedLaw.paddedMap_tupleDraw line 561
  83. theorem OAI.DFVSGames.Decoder.PaddedLaw.uniform_fixed_projection_tuple line 576
  84. def OAI.DFVSGames.Decoder.PaddedLaw.blockWeights line 587
  85. theorem OAI.DFVSGames.Decoder.PaddedLaw.blockWeights_isProbability line 592
  86. theorem OAI.DFVSGames.Decoder.PaddedLaw.blockWeights_slopes line 606
  87. def OAI.DFVSGames.Decoder.PaddedLaw.drawWeights line 634
  88. def OAI.DFVSGames.Decoder.PaddedLaw.paddedWeights line 637
  89. theorem OAI.DFVSGames.Decoder.PaddedLaw.paddedWeights_eq line 641
  90. theorem OAI.DFVSGames.Decoder.PaddedLaw.uniformWeights_prod line 664
  91. theorem OAI.DFVSGames.Decoder.PaddedLaw.totalVariation_uniform_front line 668
  92. theorem OAI.DFVSGames.Decoder.PaddedLaw.paddedWeights_totalVariation_eq_slope line 679
  93. theorem OAI.DFVSGames.Decoder.PaddedLaw.paddedWeights_totalVariation line 695
  94. abbrev OAI.DFVSGames.Decoder.PaddedLaw.ProjectionChoice line 703
  95. def OAI.DFVSGames.Decoder.PaddedLaw.choiceWeight line 705
  96. theorem OAI.DFVSGames.Decoder.PaddedLaw.choiceWeight_isProbability line 709
  97. def OAI.DFVSGames.Decoder.PaddedLaw.blockKernel line 720
  98. def OAI.DFVSGames.Decoder.PaddedLaw.choiceTupleWeight line 725
  99. theorem OAI.DFVSGames.Decoder.PaddedLaw.choiceTupleWeight_isProbability line 728
  100. def OAI.DFVSGames.Decoder.PaddedLaw.kernelTupleWeight line 733
  101. theorem OAI.DFVSGames.Decoder.PaddedLaw.blockWeights_choice_mixture line 737
  102. theorem OAI.DFVSGames.Decoder.PaddedLaw.independent_blockWeights_mixture line 743
  103. theorem OAI.DFVSGames.Decoder.PaddedLaw.drawWeights_choice_mixture line 754
  104. theorem OAI.DFVSGames.Decoder.PaddedLaw.draw_expectation_choice_mixture line 763
  105. def OAI.DFVSGames.Decoder.PaddedLaw.ChoiceValue line 777
  106. instance OAI.DFVSGames.Decoder.PaddedLaw.choiceValueFintype line 781
  107. def OAI.DFVSGames.Decoder.PaddedLaw.choiceEmbed line 784
  108. theorem OAI.DFVSGames.Decoder.PaddedLaw.blockKernel_uniform_pushforward line 789
  109. theorem OAI.DFVSGames.Decoder.PaddedLaw.pushforwardWeight_pi_dep line 806
  110. theorem OAI.DFVSGames.Decoder.PaddedLaw.uniformWeights_pi line 819
  111. theorem OAI.DFVSGames.Decoder.PaddedLaw.kernelTuple_uniform_pushforward line 826
  112. theorem OAI.DFVSGames.Decoder.PaddedLaw.sum_pushforwardWeight_mul line 843
  113. theorem OAI.DFVSGames.Decoder.PaddedLaw.sum_uniformWeights_mul line 853
  114. def OAI.DFVSGames.Decoder.PaddedLaw.choiceMask line 859
  115. def OAI.DFVSGames.Decoder.PaddedLaw.choiceSlot line 862
  116. def OAI.DFVSGames.Decoder.PaddedLaw.choiceSlots line 866
  117. theorem OAI.DFVSGames.Decoder.PaddedLaw.not_mem_choiceMask line 869
  118. def OAI.DFVSGames.Decoder.PaddedLaw.fullChoiceValue line 873
  119. def OAI.DFVSGames.Decoder.PaddedLaw.singleChoiceValue line 877
  120. def OAI.DFVSGames.Decoder.PaddedLaw.readChoiceValue line 881
  121. theorem OAI.DFVSGames.Decoder.PaddedLaw.readChoiceValue_roundtrip line 888
  122. theorem OAI.DFVSGames.Decoder.PaddedLaw.readChoiceValue_full line 894
  123. theorem OAI.DFVSGames.Decoder.PaddedLaw.readChoiceValue_single line 901
  124. def OAI.DFVSGames.Decoder.PaddedLaw.choiceValuesToRawTuple line 908
  125. def OAI.DFVSGames.Decoder.PaddedLaw.rawTupleToChoiceValues line 914
  126. def OAI.DFVSGames.Decoder.PaddedLaw.choiceValuesRawTupleEquiv line 920
  127. theorem OAI.DFVSGames.Decoder.PaddedLaw.restoreChoiceDraw line 942
  128. theorem OAI.DFVSGames.Decoder.PaddedLaw.tupleDraw_choiceValues line 951
  129. theorem OAI.DFVSGames.Decoder.PaddedLaw.fixed_choice_kernel_map_expectation line 963
  130. theorem OAI.DFVSGames.Decoder.PaddedLaw.actual_projection_mixture_expectation line 1004
  131. theorem OAI.DFVSGames.Decoder.PaddedLaw.uniform_rawMap_pair line 1017
  132. def OAI.DFVSGames.Decoder.PaddedLaw.paddedMapWeights line 1028
  133. theorem OAI.DFVSGames.Decoder.PaddedLaw.paddedMapWeights_eq line 1033
  134. theorem OAI.DFVSGames.Decoder.PaddedLaw.uniform_sourceMap_coordinates line 1047
  135. theorem OAI.DFVSGames.Decoder.PaddedLaw.paddedMapWeights_totalVariation_eq_slope line 1054
  136. theorem OAI.DFVSGames.Decoder.PaddedLaw.paddedMapWeights_totalVariation line 1081