OAI/Computability/DirectedFeedback/Analysis/NoiseEnumeration.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DFVSGames.Reduction.ActualSource.NoiseEnumeration line 11
  2. def OAI.DFVSGames.Reduction.ActualSource.NoiseEnumeration.ofFintype line 20
  3. theorem OAI.DFVSGames.Reduction.ActualSource.NoiseEnumeration.nonempty line 25
  4. theorem OAI.DFVSGames.Reduction.ActualSource.NoiseEnumeration.perm_univ line 31
  5. theorem OAI.DFVSGames.Reduction.ActualSource.NoiseEnumeration.length_eq_card line 37
  6. theorem OAI.DFVSGames.Reduction.ActualSource.NoiseEnumeration.sum_eq_univ line 41
  7. theorem OAI.DFVSGames.Reduction.ActualSource.NoiseEnumeration.average_eq_expect line 45
  8. def OAI.DFVSGames.Reduction.ActualGame.names line 59
  9. def OAI.DFVSGames.Reduction.ActualGame.rhs line 63
  10. abbrev OAI.DFVSGames.Reduction.ActualGame.Question line 65
  11. abbrev OAI.DFVSGames.Reduction.ActualGame.Map line 66
  12. abbrev OAI.DFVSGames.Reduction.ActualGame.Dual line 67
  13. abbrev OAI.DFVSGames.Reduction.ActualGame.Query line 68
  14. instance OAI.DFVSGames.Reduction.ActualGame.mapFintype line 70
  15. instance OAI.DFVSGames.Reduction.ActualGame.dualFintype line 74
  16. def OAI.DFVSGames.Reduction.ActualGame.canonical line 78
  17. abbrev OAI.DFVSGames.Reduction.ActualGame.Vertex line 81
  18. abbrev OAI.DFVSGames.Reduction.ActualGame.TwoSidedVertex line 82
  19. def OAI.DFVSGames.Reduction.ActualGame.vertex line 84
  20. def OAI.DFVSGames.Reduction.ActualGame.offset line 87
  21. def OAI.DFVSGames.Reduction.ActualGame.shiftQuery line 90
  22. theorem OAI.DFVSGames.Reduction.ActualGame.canonical_shiftQuery line 94
  23. theorem OAI.DFVSGames.Reduction.ActualGame.vertex_shiftQuery line 100
  24. theorem OAI.DFVSGames.Reduction.ActualGame.offset_shiftQuery line 106
  25. def OAI.DFVSGames.Reduction.ActualGame.vertexCount line 111
  26. def OAI.DFVSGames.Reduction.ActualGame.vertexEncoding line 114
  27. theorem OAI.DFVSGames.Reduction.ActualGame.vertexCount_eq_twice line 118
  28. abbrev OAI.DFVSGames.Reduction.ActualGame.Outcome line 122
  29. def OAI.DFVSGames.Reduction.ActualGame.leftQuery line 125
  30. def OAI.DFVSGames.Reduction.ActualGame.rightQuery line 128
  31. def OAI.DFVSGames.Reduction.ActualGame.edge line 132
  32. theorem OAI.DFVSGames.Reduction.ActualGame.edge_source_ne_target line 139
  33. def OAI.DFVSGames.Reduction.ActualGame.outcomes line 147
  34. theorem OAI.DFVSGames.Reduction.ActualGame.mem_outcomes line 150
  35. theorem OAI.DFVSGames.Reduction.ActualGame.outcomes_nodup line 154
  36. theorem OAI.DFVSGames.Reduction.ActualGame.outcomes_length line 157
  37. def OAI.DFVSGames.Reduction.ActualGame.outputInstance line 161
  38. theorem OAI.DFVSGames.Reduction.ActualGame.outputInstance_constraints_length line 173
  39. def OAI.DFVSGames.Reduction.ActualGame.sideLabel line 178
  40. def OAI.DFVSGames.Reduction.ActualGame.labelingOf line 183
  41. theorem OAI.DFVSGames.Reduction.ActualGame.sideLabel_labelingOf line 189
  42. def OAI.DFVSGames.Reduction.ActualGame.unfolded line 195
  43. theorem OAI.DFVSGames.Reduction.ActualGame.unfolded_equivariant line 200
  44. theorem OAI.DFVSGames.Reduction.ActualGame.edge_satisfied_iff line 210
  45. def OAI.DFVSGames.Reduction.ActualGame.acceptanceProbability line 224
  46. theorem OAI.DFVSGames.Reduction.ActualGame.acceptanceProbability_eq_test line 229
  47. theorem OAI.DFVSGames.Reduction.ActualGame.countSatisfied_map_inline_ActualGame line 241
  48. theorem OAI.DFVSGames.Reduction.ActualGame.countSatisfied_eq_sum line 249
  49. theorem OAI.DFVSGames.Reduction.ActualGame.acceptanceProbability_eq_count line 257
  50. def OAI.DFVSGames.Reduction.ActualGame.orbitBodyDecidableEq line 267
  51. def OAI.DFVSGames.Reduction.ActualGame.explicitBodies line 272
  52. def OAI.DFVSGames.Reduction.ActualGame.explicitVertexCount line 277
  53. def OAI.DFVSGames.Reduction.ActualGame.explicitVertexEncoding line 280
  54. def OAI.DFVSGames.Reduction.ActualGame.semanticToExplicitVertices line 288
  55. theorem OAI.DFVSGames.Reduction.ActualGame.semanticToExplicitVertices_apply line 292
  56. theorem OAI.DFVSGames.Reduction.ActualGame.explicitVertexCount_eq line 298
  57. def OAI.DFVSGames.Reduction.ActualGame.explicitEdge line 302
  58. theorem OAI.DFVSGames.Reduction.ActualGame.explicitEdge_eq_rename line 309
  59. def OAI.DFVSGames.Reduction.ActualGame.explicitOutcomes line 316
  60. theorem OAI.DFVSGames.Reduction.ActualGame.explicitOutcomes_nodup line 320
  61. theorem OAI.DFVSGames.Reduction.ActualGame.mem_explicitOutcomes line 325
  62. theorem OAI.DFVSGames.Reduction.ActualGame.explicitOutcomes_perm_outcomes line 330
  63. def OAI.DFVSGames.Reduction.ActualGame.outputInstanceWithEnumeration line 338
  64. theorem OAI.DFVSGames.Reduction.ActualGame.outputInstanceWithEnumeration_length line 351
  65. theorem OAI.DFVSGames.Reduction.ActualGame.explicitConstraints_perm_renamed line 358
  66. theorem OAI.DFVSGames.Reduction.ActualGame.completeAt_outputInstanceWithEnumeration_iff line 367
  67. theorem OAI.DFVSGames.Reduction.ActualGame.soundAt_outputInstanceWithEnumeration_iff line 375
  68. abbrev OAI.DFVSGames.Decoder.TableKeysGame.Question line 391
  69. abbrev OAI.DFVSGames.Decoder.TableKeysGame.Map line 392
  70. abbrev OAI.DFVSGames.Decoder.TableKeysGame.Dual line 393
  71. abbrev OAI.DFVSGames.Decoder.TableKeysGame.Query line 394
  72. abbrev OAI.DFVSGames.Decoder.TableKeysGame.canonical line 395
  73. abbrev OAI.DFVSGames.Decoder.TableKeysGame.Vertex line 397
  74. abbrev OAI.DFVSGames.Decoder.TableKeysGame.vertex line 398
  75. abbrev OAI.DFVSGames.Decoder.TableKeysGame.offset line 399
  76. abbrev OAI.DFVSGames.Decoder.TableKeysGame.shiftQuery line 400
  77. def OAI.DFVSGames.Decoder.TableKeysGame.vertexCount line 402
  78. def OAI.DFVSGames.Decoder.TableKeysGame.vertexEncoding line 405
  79. abbrev OAI.DFVSGames.Decoder.TableKeysGame.Outcome line 408
  80. abbrev OAI.DFVSGames.Decoder.TableKeysGame.leftQuery line 411
  81. abbrev OAI.DFVSGames.Decoder.TableKeysGame.rightQuery line 413
  82. def OAI.DFVSGames.Decoder.TableKeysGame.edge line 416
  83. def OAI.DFVSGames.Decoder.TableKeysGame.outcomes line 423
  84. def OAI.DFVSGames.Decoder.TableKeysGame.outputInstance line 426
  85. theorem OAI.DFVSGames.Decoder.TableKeysGame.outputInstance_constraints_length line 438
  86. def OAI.DFVSGames.Decoder.TableKeysGame.vertexLabel line 443
  87. def OAI.DFVSGames.Decoder.TableKeysGame.labelingOf line 448
  88. theorem OAI.DFVSGames.Decoder.TableKeysGame.vertexLabel_labelingOf line 453
  89. def OAI.DFVSGames.Decoder.TableKeysGame.unfolded line 459
  90. theorem OAI.DFVSGames.Decoder.TableKeysGame.unfolded_equivariant line 464
  91. theorem OAI.DFVSGames.Decoder.TableKeysGame.edge_satisfied_iff line 475
  92. def OAI.DFVSGames.Decoder.TableKeysGame.acceptanceProbability line 489
  93. theorem OAI.DFVSGames.Decoder.TableKeysGame.acceptanceProbability_eq_test line 493
  94. theorem OAI.DFVSGames.Decoder.TableKeysGame.countSatisfied_map_inline_TableKeysGame line 505
  95. theorem OAI.DFVSGames.Decoder.TableKeysGame.countSatisfied_eq_sum line 513
  96. theorem OAI.DFVSGames.Decoder.TableKeysGame.acceptanceProbability_eq_count line 521
  97. def OAI.DFVSGames.Decoder.TableKeysGame.explicitVertexCount line 531
  98. def OAI.DFVSGames.Decoder.TableKeysGame.explicitVertexEncoding line 534
  99. def OAI.DFVSGames.Decoder.TableKeysGame.semanticToExplicitVertices line 540
  100. theorem OAI.DFVSGames.Decoder.TableKeysGame.semanticToExplicitVertices_apply line 544
  101. theorem OAI.DFVSGames.Decoder.TableKeysGame.explicitVertexCount_eq line 550
  102. def OAI.DFVSGames.Decoder.TableKeysGame.explicitEdge line 554
  103. theorem OAI.DFVSGames.Decoder.TableKeysGame.explicitEdge_eq_rename line 561
  104. def OAI.DFVSGames.Decoder.TableKeysGame.outputInstanceWithEnumeration line 568
  105. theorem OAI.DFVSGames.Decoder.TableKeysGame.outputInstanceWithEnumeration_length line 581
  106. theorem OAI.DFVSGames.Decoder.TableKeysGame.explicitConstraints_perm_renamed line 588
  107. theorem OAI.DFVSGames.Decoder.TableKeysGame.completeAt_outputInstanceWithEnumeration_iff line 597
  108. theorem OAI.DFVSGames.Decoder.TableKeysGame.soundAt_outputInstanceWithEnumeration_iff line 605
  109. def OAI.DFVSGames.Decoder.TableKeysRestoration.extendedLabel line 629
  110. theorem OAI.DFVSGames.Decoder.TableKeysRestoration.extendedLabel_actual line 633
  111. def OAI.DFVSGames.Decoder.TableKeysRestoration.restoredData line 639
  112. theorem OAI.DFVSGames.Decoder.TableKeysRestoration.restoredData_actual line 643
  113. theorem OAI.DFVSGames.Decoder.TableKeysRestoration.restoredData_shift line 650
  114. def OAI.DFVSGames.Decoder.TableKeysRestoration.keyAnswer line 658
  115. theorem OAI.DFVSGames.Decoder.TableKeysRestoration.keyAnswer_actual line 664
  116. theorem OAI.DFVSGames.Decoder.TableKeysRestoration.keyAnswer_shift line 671
  117. def OAI.DFVSGames.Decoder.TableKeysRestoration.projectedAnswer line 678
  118. theorem OAI.DFVSGames.Decoder.TableKeysRestoration.projectedAnswer_pullback line 686
  119. theorem OAI.DFVSGames.Decoder.TableKeysRestoration.projectedAnswer_fold line 700
  120. theorem OAI.DFVSGames.Decoder.TableKeysPrivateRow.assemble_prod_shift line 726
  121. def OAI.DFVSGames.Decoder.TableKeysPrivateRow.rowAnswer line 742
  122. theorem OAI.DFVSGames.Decoder.TableKeysPrivateRow.rowAnswer_fold line 753
  123. theorem OAI.DFVSGames.Decoder.TableKeysPrivateRow.rowAnswer_actual line 765
  124. def OAI.DFVSGames.Decoder.TableKeysPrivateRow.targetIntercept line 780
  125. theorem OAI.DFVSGames.Decoder.TableKeysPrivateRow.affine_target_on_row line 785