OAI/Computability/DirectedFeedback/Games/CanonicalAddress.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Reduction.CanonicalAddress.radix line 29
  2. theorem OAI.DFVSGames.Reduction.CanonicalAddress.radix_eq_foldl line 31
  3. theorem OAI.DFVSGames.Reduction.CanonicalAddress.radix_nil line 37
  4. theorem OAI.DFVSGames.Reduction.CanonicalAddress.radix_append_word line 39
  5. theorem OAI.DFVSGames.Reduction.CanonicalAddress.radix_lt_pow_length line 43
  6. theorem OAI.DFVSGames.Reduction.CanonicalAddress.radix_injective_of_length_eq line 50
  7. def OAI.DFVSGames.Reduction.CanonicalAddress.base line 61
  8. theorem OAI.DFVSGames.Reduction.CanonicalAddress.base_eq line 63
  9. theorem OAI.DFVSGames.Reduction.CanonicalAddress.one_lt_base line 67
  10. theorem OAI.DFVSGames.Reduction.CanonicalAddress.bodyWords_lt_base line 74
  11. def OAI.DFVSGames.Reduction.CanonicalAddress.capacity line 78
  12. theorem OAI.DFVSGames.Reduction.CanonicalAddress.capacity_pos line 80
  13. def OAI.DFVSGames.Reduction.CanonicalAddress.bodyAddress line 83
  14. theorem OAI.DFVSGames.Reduction.CanonicalAddress.bodyAddress_val line 89
  15. theorem OAI.DFVSGames.Reduction.CanonicalAddress.bodyAddress_injective line 92
  16. theorem OAI.DFVSGames.Reduction.CanonicalAddress.bodyAddress_eq_iff line 100
  17. def OAI.DFVSGames.Reduction.CanonicalAddress.capacityPolynomial line 103
  18. theorem OAI.DFVSGames.Reduction.CanonicalAddress.capacityPolynomial_eval line 106
  19. def OAI.DFVSGames.Integration.NoiseTables.reindex line 121
  20. theorem OAI.DFVSGames.Integration.NoiseTables.reindex_stabilityError line 130
  21. theorem OAI.DFVSGames.Integration.NoiseTables.reindex_kernelProbability line 137
  22. structure OAI.DFVSGames.Integration.NoiseTables.Table line 148
  23. def OAI.DFVSGames.Integration.NoiseTables.Table.gadget line 154
  24. def OAI.DFVSGames.Integration.NoiseTables.Table.ofEnumeration line 163
  25. theorem OAI.DFVSGames.Integration.NoiseTables.Table.ofEnumeration_length line 167
  26. def OAI.DFVSGames.Integration.NoiseTables.Table.positionEquiv line 171
  27. theorem OAI.DFVSGames.Integration.NoiseTables.Table.noise_positionEquiv line 177
  28. theorem OAI.DFVSGames.Integration.NoiseTables.Table.stabilityError_ofEnumeration line 184
  29. theorem OAI.DFVSGames.Integration.NoiseTables.Table.kernelProbability_ofEnumeration line 194
  30. theorem OAI.DFVSGames.Integration.NoiseTables.Table.guarantees_ofEnumeration line 204
  31. def OAI.DFVSGames.Integration.TableReduction.tableEnumeration line 236
  32. def OAI.DFVSGames.Integration.TableReduction.tableSkeleton line 242
  33. def OAI.DFVSGames.Integration.TableReduction.output line 245
  34. theorem OAI.DFVSGames.Integration.TableReduction.output_eq_with_witness line 249
  35. theorem OAI.DFVSGames.Integration.TableReduction.completeAt_output_iff line 255
  36. theorem OAI.DFVSGames.Integration.TableReduction.soundAt_output_iff line 263
  37. theorem OAI.DFVSGames.Integration.TableReduction.edge_ofEnumeration line 271
  38. theorem OAI.DFVSGames.Integration.TableReduction.acceptance_ofEnumeration line 279
  39. theorem OAI.DFVSGames.Integration.TableReduction.rate_ofEnumeration line 291
  40. theorem OAI.DFVSGames.Integration.TableReduction.completeAt_ofEnumeration_iff line 300
  41. theorem OAI.DFVSGames.Integration.TableReduction.soundAt_ofEnumeration_iff line 312
  42. def OAI.DFVSGames.Integration.VertexEmbedding.embedConstraint line 334
  43. theorem OAI.DFVSGames.Integration.VertexEmbedding.embedConstraint_satisfied line 340
  44. theorem OAI.DFVSGames.Integration.VertexEmbedding.embedConstraint_permutation line 344
  45. theorem OAI.DFVSGames.Integration.VertexEmbedding.count_map line 347
  46. def OAI.DFVSGames.Integration.VertexEmbedding.embedInstance line 356
  47. theorem OAI.DFVSGames.Integration.VertexEmbedding.embedInstance_vertices line 362
  48. theorem OAI.DFVSGames.Integration.VertexEmbedding.embedInstance_constraints line 366
  49. theorem OAI.DFVSGames.Integration.VertexEmbedding.embedInstance_length line 370
  50. theorem OAI.DFVSGames.Integration.VertexEmbedding.count_embed line 374
  51. theorem OAI.DFVSGames.Integration.VertexEmbedding.satisfactionRate_embed line 380
  52. def OAI.DFVSGames.Integration.VertexEmbedding.extendLabeling line 388
  53. theorem OAI.DFVSGames.Integration.VertexEmbedding.extendLabeling_apply line 393
  54. theorem OAI.DFVSGames.Integration.VertexEmbedding.extendLabeling_comp line 402
  55. theorem OAI.DFVSGames.Integration.VertexEmbedding.soundAt_embed line 408
  56. theorem OAI.DFVSGames.Integration.VertexEmbedding.completeAt_embed line 416
  57. theorem OAI.DFVSGames.Integration.VertexEmbedding.completeAt_embed_iff line 424
  58. theorem OAI.DFVSGames.Integration.VertexEmbedding.soundAt_embed_iff line 434
  59. theorem OAI.DFVSGames.Integration.VertexEmbedding.isTranslationInstance_embed_iff line 443
  60. abbrev OAI.DFVSGames.Decoder.TableKeysAddressGame.vertexCount line 466
  61. def OAI.DFVSGames.Decoder.TableKeysAddressGame.vertexAddress line 469
  62. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.vertexAddress_injective line 472
  63. def OAI.DFVSGames.Decoder.TableKeysAddressGame.queryAddress line 478
  64. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.vertexAddress_query line 482
  65. def OAI.DFVSGames.Decoder.TableKeysAddressGame.explicitToAddress line 487
  66. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.explicitToAddress_injective line 491
  67. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.explicitToAddress_apply line 496
  68. def OAI.DFVSGames.Decoder.TableKeysAddressGame.semanticToAddress line 502
  69. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.semanticToAddress_injective line 506
  70. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.semanticToAddress_apply line 511
  71. def OAI.DFVSGames.Decoder.TableKeysAddressGame.addressEdge line 517
  72. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.addressEdge_eq_embed line 525
  73. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.addressEdge_eq_semantic_embed line 532
  74. def OAI.DFVSGames.Decoder.TableKeysAddressGame.outputInstance line 539
  75. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.outputInstance_eq_embed line 550
  76. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.outputInstance_length line 559
  77. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.outputInstance_count line 566
  78. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.completeAt_outputInstance_iff_explicit line 577
  79. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.soundAt_outputInstance_iff_explicit line 584
  80. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.completeAt_outputInstance_iff line 591
  81. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.soundAt_outputInstance_iff line 598
  82. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.outputInstance_translations line 605
  83. def OAI.DFVSGames.Decoder.TableKeysAddressGame.tableOutput line 622
  84. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.tableOutput_eq_with_witness line 627
  85. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.completeAt_tableOutput_iff line 634
  86. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.soundAt_tableOutput_iff line 642
  87. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.tableOutput_translations line 650
  88. theorem OAI.DFVSGames.Decoder.TableKeysAddressGame.vertexCount_eq_polynomial line 655
  89. theorem OAI.DFVSGames.Decoder.MatrixGap.address_rate_eq_semantic_acceptance line 674
  90. theorem OAI.DFVSGames.Decoder.MatrixGap.address_value_le_of_semantic_acceptance line 700
  91. theorem OAI.DFVSGames.Decoder.MatrixGap.semantic_acceptance_le_address_value line 739
  92. theorem OAI.DFVSGames.Decoder.MatrixGap.address_value_ge_of_near_assignment line 764
  93. structure OAI.DFVSGames.Decoder.MatrixGap.Parameters line 804
  94. theorem OAI.DFVSGames.Decoder.MatrixGap.semantic_rate_le_address_value line 819
  95. def OAI.DFVSGames.Decoder.MatrixGap.Parameters.output line 832
  96. theorem OAI.DFVSGames.Decoder.MatrixGap.Parameters.completeness line 835
  97. theorem OAI.DFVSGames.Decoder.MatrixGap.Parameters.output_translations line 843