OAI/Computability/DirectedFeedback/RankGraph/Clone100Counting.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Outer.Clone100Counting.Index line 55
  2. abbrev OAI.DFVSGames.Outer.Clone100Counting.Triple line 56
  3. def OAI.DFVSGames.Outer.Clone100Counting.sign line 58
  4. def OAI.DFVSGames.Outer.Clone100Counting.bias line 60
  5. def OAI.DFVSGames.Outer.Clone100Counting.majorityBit line 62
  6. theorem OAI.DFVSGames.Outer.Clone100Counting.majority_aligned_nonneg line 64
  7. def OAI.DFVSGames.Outer.Clone100Counting.parityIndicator line 71
  8. theorem OAI.DFVSGames.Outer.Clone100Counting.parityIndicator_nonneg line 74
  9. theorem OAI.DFVSGames.Outer.Clone100Counting.parityIndicator_le_one line 79
  10. theorem OAI.DFVSGames.Outer.Clone100Counting.parityIndicator_eq line 84
  11. def OAI.DFVSGames.Outer.Clone100Counting.unconditionedScore line 90
  12. theorem OAI.DFVSGames.Outer.Clone100Counting.independent_product_sum line 93
  13. theorem OAI.DFVSGames.Outer.Clone100Counting.unconditionedScore_eq line 102
  14. theorem OAI.DFVSGames.Outer.Clone100Counting.unconditionedScore_le_one line 122
  15. theorem OAI.DFVSGames.Outer.Clone100Counting.signed_product_of_failure line 130
  16. theorem OAI.DFVSGames.Outer.Clone100Counting.unconditionedScore_le_half_of_failure line 136
  17. theorem OAI.DFVSGames.Outer.Clone100Counting.unconditionedScore_le line 147
  18. theorem OAI.DFVSGames.Outer.Clone100Counting.condition_970200_le line 167
  19. def OAI.DFVSGames.Outer.Clone100Counting.conditionedScore line 186
  20. theorem OAI.DFVSGames.Outer.Clone100Counting.conditionedScore_le line 191
  21. abbrev OAI.DFVSGames.Outer.Clone100Triples.Index line 212
  22. abbrev OAI.DFVSGames.Outer.Clone100Triples.Triple line 213
  23. def OAI.DFVSGames.Outer.Clone100Triples.good line 215
  24. instance OAI.DFVSGames.Outer.Clone100Triples.(instance at line 218) line 218
  25. abbrev OAI.DFVSGames.Outer.Clone100Triples.GoodTriple line 220
  26. def OAI.DFVSGames.Outer.Clone100Triples.toEmbedding line 222
  27. def OAI.DFVSGames.Outer.Clone100Triples.fromEmbedding line 231
  28. def OAI.DFVSGames.Outer.Clone100Triples.embeddingEquiv line 239
  29. theorem OAI.DFVSGames.Outer.Clone100Triples.card_goodTriple line 249
  30. theorem OAI.DFVSGames.Outer.Clone100Triples.card_triple line 253
  31. instance OAI.DFVSGames.Outer.Clone100Triples.(instance at line 256) line 256
  32. def OAI.DFVSGames.Outer.Clone100.triples line 272
  33. theorem OAI.DFVSGames.Outer.Clone100.triples_length line 274
  34. def OAI.DFVSGames.Outer.Clone100.clone line 277
  35. theorem OAI.DFVSGames.Outer.Clone100.clone_distinct line 280
  36. theorem OAI.DFVSGames.Outer.Clone100.clone_lift line 288
  37. def OAI.DFVSGames.Outer.Clone100.nameEquiv line 291
  38. def OAI.DFVSGames.Outer.Clone100.equation line 293
  39. theorem OAI.DFVSGames.Outer.Clone100.equation_distinct line 298
  40. def OAI.DFVSGames.Outer.Clone100.equations line 307
  41. theorem OAI.DFVSGames.Outer.Clone100.equations_length line 311
  42. theorem OAI.DFVSGames.Outer.Clone100.equations_nonempty line 320
  43. def OAI.DFVSGames.Outer.Clone100.clonedInput line 326
  44. def OAI.DFVSGames.Outer.Clone100.clonedSource line 331
  45. theorem OAI.DFVSGames.Outer.Clone100.clonedSource_distinct line 334
  46. def OAI.DFVSGames.Outer.Clone100.lift line 350
  47. theorem OAI.DFVSGames.Outer.Clone100.equation_lift line 353
  48. theorem OAI.DFVSGames.Outer.Clone100.completeness_count line 357
  49. def OAI.DFVSGames.Outer.Clone100.success line 370
  50. theorem OAI.DFVSGames.Outer.Clone100.completeness line 373
  51. theorem OAI.DFVSGames.Outer.Clone100.count_as_sum_inline_Clone100 line 381
  52. def OAI.DFVSGames.Outer.Clone100.majority line 387
  53. theorem OAI.DFVSGames.Outer.Clone100.equation_count_le line 390
  54. theorem OAI.DFVSGames.Outer.Clone100.soundness_count line 413
  55. theorem OAI.DFVSGames.Outer.Clone100.soundness line 427
  56. theorem OAI.DFVSGames.Outer.Clone100.soundness_four_fifths line 445
  57. theorem OAI.DFVSGames.Outer.Clone100.clonedInput_bits_length_le line 454
  58. def OAI.DFVSGames.Outer.SourceIncidence.incidence line 479
  59. theorem OAI.DFVSGames.Outer.SourceIncidence.names_distinct line 483
  60. theorem OAI.DFVSGames.Outer.SourceIncidence.uniform_probability_eq_expect_inline_SourceIncidence line 490
  61. theorem OAI.DFVSGames.Outer.SourceIncidence.paritySuccess_eq line 502
  62. theorem OAI.DFVSGames.Outer.SourceIncidence.paritySuccess_input line 522
  63. def OAI.DFVSGames.Outer.SourceIncidence.input line 532
  64. def OAI.DFVSGames.Outer.SourceIncidence.source line 536
  65. theorem OAI.DFVSGames.Outer.SourceIncidence.source_distinct line 539
  66. theorem OAI.DFVSGames.Outer.SourceIncidence.source_complete line 543
  67. theorem OAI.DFVSGames.Outer.SourceIncidence.source_sound line 560
  68. def OAI.DFVSGames.Outer.SourceIncidence.ordinaryGame line 576
  69. theorem OAI.DFVSGames.Outer.SourceIncidence.ordinaryGame_projection line 580
  70. theorem OAI.DFVSGames.Outer.SourceIncidence.ordinaryGame_sound line 584
  71. def OAI.DFVSGames.Explicit.MachineClone100Table.cloneEquationWords line 604
  72. inductive OAI.DFVSGames.Explicit.MachineClone100Model.Tape line 622
  73. abbrev OAI.DFVSGames.Explicit.MachineClone100Model.Context line 626
  74. abbrev OAI.DFVSGames.Explicit.MachineClone100Model.State line 627
  75. abbrev OAI.DFVSGames.Explicit.MachineClone100Model.Alphabet line 628
  76. inductive OAI.DFVSGames.Explicit.MachineClone100Model.Label line 630
  77. def OAI.DFVSGames.Explicit.MachineClone100Model.defaultControl line 646
  78. def OAI.DFVSGames.Explicit.MachineClone100Model.initialState line 647
  79. def OAI.DFVSGames.Explicit.MachineClone100Model.headerTape line 649
  80. def OAI.DFVSGames.Explicit.MachineClone100Model.contextSource line 651
  81. def OAI.DFVSGames.Explicit.MachineClone100Model.contextScale line 655
  82. def OAI.DFVSGames.Explicit.MachineClone100Model.tripleField line 659
  83. def OAI.DFVSGames.Explicit.MachineClone100Model.contextOffset line 666
  84. def OAI.DFVSGames.Explicit.MachineClone100Model.affineEmit line 670
  85. def OAI.DFVSGames.Explicit.MachineClone100Model.emission line 674
  86. def OAI.DFVSGames.Explicit.MachineClone100Model.contextNext line 677
  87. def OAI.DFVSGames.Explicit.MachineClone100Model.cleanupNext line 684
  88. def OAI.DFVSGames.Explicit.MachineClone100Model.drain line 687
  89. def OAI.DFVSGames.Explicit.MachineClone100Model.program line 694
  90. def OAI.DFVSGames.Explicit.MachineClone100Model.machine line 717
  91. theorem OAI.DFVSGames.Explicit.MachineClone100Context.contextSource_ne_scratch line 741
  92. theorem OAI.DFVSGames.Explicit.MachineClone100Context.contextSource_ne_reversed line 749
  93. def OAI.DFVSGames.Explicit.MachineClone100Context.contextTapes line 757
  94. theorem OAI.DFVSGames.Explicit.MachineClone100Context.contextTapes_reversed line 763
  95. theorem OAI.DFVSGames.Explicit.MachineClone100Context.contextTapes_other line 770
  96. theorem OAI.DFVSGames.Explicit.MachineClone100Context.contextTapes_source line 776
  97. theorem OAI.DFVSGames.Explicit.MachineClone100Context.contextTapes_scratch line 781
  98. theorem OAI.DFVSGames.Explicit.MachineClone100Context.setupStep line 786
  99. theorem OAI.DFVSGames.Explicit.MachineClone100Context.contextTrace line 792
  100. def OAI.DFVSGames.Explicit.MachineClone100Context.contextInTime line 815
  101. theorem OAI.DFVSGames.Explicit.MachineClone100Context.contextInTime_steps line 826